Character module of a module

For commutative ring R and an R-module M and an injective module D, its character module M⋆ is defined to be R-linear maps M ⟶ D.

M⋆ also has an R-module structure given by (r • f) m = f (r • m).

Main results

• CharacterModuleFunctor : the contravariant functor of R-modules where M ↦ M⋆ and an R-linear map l : M ⟶ N induces an R-linear map l⋆ : f ↦ f ∘ l where f : N⋆.
• LinearMap.dual_surjective_of_injective : If l is injective then l⋆ is surjective, in another word taking character module as a functor sends monos to epis.
• CharacterModule.homEquiv : there is a bijection between linear map Hom(N, M⋆) and (N ⊗ M)⋆ given by curry and uncurry.

def CharacterModule (A : Type uA) [AddCommGroup A] : Type uA

The character module of an abelian group A in the unit rational circle is A⋆ := Hom_ℤ(A, ℚ ⧸ ℤ).

instance CharacterModule.instFunLikeAddCircleRatOfNat (A : Type uA) [AddCommGroup A] : FunLike (CharacterModule A) A (AddCircle 1)

instance CharacterModule.instLinearMapClassIntAddCircleRatOfNat (A : Type uA) [AddCommGroup A] : LinearMapClass (CharacterModule A) ℤ A (AddCircle 1)

instance CharacterModule.instAddCommGroup (A : Type uA) [AddCommGroup A] : AddCommGroup (CharacterModule A)

theorem CharacterModule.ext (A : Type uA) [AddCommGroup A] {c c' : CharacterModule A} (h : ∀ (x : A), c x = c' x) : c = c'

theorem CharacterModule.ext_iff {A : Type uA} [AddCommGroup A] {c c' : CharacterModule A} : c = c' ↔ ∀ (x : A), c x = c' x

instance CharacterModule.instModule (R : Type uR) [CommRing R] (A : Type uA) [AddCommGroup A] [Module R A] : Module R (CharacterModule A)

@[simp]

theorem CharacterModule.smul_apply {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] [Module R A] (c : CharacterModule A) (r : R) (a : A) : (r • c) a = c (r • a)

def CharacterModule.dual {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {B : Type uB} [AddCommGroup B] [Module R A] [Module R B] (f : A →ₗ[R] B) : CharacterModule B →ₗ[R] CharacterModule A

Given an abelian group homomorphism f : A → B, f⋆(L) := L ∘ f defines a linear map from B⋆ to A⋆.

@[simp]

theorem CharacterModule.dual_apply {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {B : Type uB} [AddCommGroup B] [Module R A] [Module R B] (f : A →ₗ[R] B) (L : CharacterModule B) : (dual f) L = AddMonoidHom.comp L f.toAddMonoidHom

@[simp]

theorem CharacterModule.dual_zero {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {B : Type uB} [AddCommGroup B] [Module R A] [Module R B] : dual 0 = 0

theorem CharacterModule.dual_comp {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {B : Type uB} [AddCommGroup B] [Module R A] [Module R B] {C : Type u_2} [AddCommGroup C] [Module R C] (f : A →ₗ[R] B) (g : B →ₗ[R] C) : dual (g ∘ₗ f) = dual f ∘ₗ dual g

theorem CharacterModule.dual_injective_of_surjective {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {B : Type uB} [AddCommGroup B] [Module R A] [Module R B] (f : A →ₗ[R] B) (hf : Function.Surjective ⇑f) : Function.Injective ⇑(dual f)

theorem CharacterModule.dual_surjective_of_injective {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {B : Type uB} [AddCommGroup B] [Module R A] [Module R B] (f : A →ₗ[R] B) (hf : Function.Injective ⇑f) : Function.Surjective ⇑(dual f)

def CharacterModule.congr {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {B : Type uB} [AddCommGroup B] [Module R A] [Module R B] (e : A ≃ₗ[R] B) : CharacterModule A ≃ₗ[R] CharacterModule B

Two isomorphic modules have isomorphic character modules.

noncomputable def CharacterModule.uncurry {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {B : Type uB} [AddCommGroup B] [Module R A] [Module R B] : (A →ₗ[R] CharacterModule B) →ₗ[R] CharacterModule (TensorProduct R A B)

Any linear map L : A → B⋆ induces a character in (A ⊗ B)⋆ by a ⊗ b ↦ L a b.

@[simp]

theorem CharacterModule.uncurry_apply {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {B : Type uB} [AddCommGroup B] [Module R A] [Module R B] (c : A →ₗ[R] CharacterModule B) : uncurry c = TensorProduct.liftAddHom c.toAddMonoidHom ⋯

noncomputable def CharacterModule.curry {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {B : Type uB} [AddCommGroup B] [Module R A] [Module R B] : CharacterModule (TensorProduct R A B) →ₗ[R] A →ₗ[R] CharacterModule B

Any character c in (A ⊗ B)⋆ induces a linear map A → B⋆ by a ↦ b ↦ c (a ⊗ b).

@[simp]

theorem CharacterModule.curry_apply_apply {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {B : Type uB} [AddCommGroup B] [Module R A] [Module R B] (c : CharacterModule (TensorProduct R A B)) (x✝ : A) : (curry c) x✝ = AddMonoidHom.comp c ↑((TensorProduct.mk R A B) x✝)

noncomputable def CharacterModule.homEquiv {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {B : Type uB} [AddCommGroup B] [Module R A] [Module R B] : (A →ₗ[R] CharacterModule B) ≃ₗ[R] CharacterModule (TensorProduct R A B)

Linear maps into a character module are exactly characters of the tensor product.

@[simp]

theorem CharacterModule.homEquiv_symm_apply_apply_apply {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {B : Type uB} [AddCommGroup B] [Module R A] [Module R B] (a : CharacterModule (TensorProduct R A B)) (x✝ : A) (a✝ : B) : ((homEquiv.symm a) x✝) a✝ = a (x✝ ⊗ₜ[R] a✝)

@[simp]

theorem CharacterModule.homEquiv_apply_apply {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {B : Type uB} [AddCommGroup B] [Module R A] [Module R B] (c : A →ₗ[R] CharacterModule B) (x : (addConGen (TensorProduct.Eqv R A B)).Quotient) : (homEquiv c) x = AddCon.liftOn x ⇑(FreeAddMonoid.lift fun (mn : A × B) => (c.toAddMonoidHom mn.1) mn.2) ⋯

theorem CharacterModule.dual_rTensor_conj_homEquiv {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] (A' : Type u_1) [AddCommGroup A'] {B : Type uB} [AddCommGroup B] [Module R A] [Module R A'] [Module R B] (f : A →ₗ[R] A') : ↑homEquiv.symm ∘ₗ dual (LinearMap.rTensor B f) ∘ₗ ↑homEquiv = LinearMap.lcomp R (CharacterModule B) f

@[reducible, inline]

abbrev CharacterModule.int : Type

ℤ⋆, the character module of ℤ in the unit rational circle.

@[reducible, inline]

abbrev CharacterModule.int.divByNat (n : ℕ) : CharacterModule.int

Given n : ℕ, the map m ↦ m / n.

theorem CharacterModule.int.divByNat_self (n : ℕ) : (int.divByNat n) ↑n = 0

noncomputable def CharacterModule.intSpanEquivQuotAddOrderOf {A : Type uA} [AddCommGroup A] (a : A) : ↥(Submodule.span ℤ {a}) ≃ₗ[ℤ] ℤ ⧸ Ideal.span {↑(addOrderOf a)}

The ℤ-submodule spanned by a single element a is isomorphic to the quotient of ℤ by the ideal generated by the order of a.

@[simp]

theorem CharacterModule.intSpanEquivQuotAddOrderOf_symm_apply_coe {A : Type uA} [AddCommGroup A] (a : A) (a✝ : ℤ ⧸ Ideal.span {↑(addOrderOf a)}) : ↑((intSpanEquivQuotAddOrderOf a).symm a✝) = ↑((LinearMap.toSpanSingleton ℤ A a).quotKerEquivRange (((LinearMap.ker (LinearMap.toSpanSingleton ℤ A a)).quotEquivOfEq (Ideal.span {↑(addOrderOf a)}) ⋯).symm a✝))

@[simp]

theorem CharacterModule.intSpanEquivQuotAddOrderOf_apply {A : Type uA} [AddCommGroup A] (a : A) (a✝ : ↥(Submodule.span ℤ {a})) : (intSpanEquivQuotAddOrderOf a) a✝ = ((LinearMap.ker (LinearMap.toSpanSingleton ℤ A a)).quotEquivOfEq (Ideal.span {↑(addOrderOf a)}) ⋯) ((LinearMap.toSpanSingleton ℤ A a).quotKerEquivRange.symm ((LinearEquiv.ofEq (Submodule.span ℤ {a}) (LinearMap.range (LinearMap.toSpanSingleton ℤ A a)) ⋯) a✝))

theorem CharacterModule.intSpanEquivQuotAddOrderOf_apply_self {A : Type uA} [AddCommGroup A] (a : A) : (intSpanEquivQuotAddOrderOf a) ⟨a, ⋯⟩ = Submodule.Quotient.mk 1

noncomputable def CharacterModule.ofSpanSingleton {A : Type uA} [AddCommGroup A] (a : A) : CharacterModule ↥(Submodule.span ℤ {a})

For an abelian group A and an element a ∈ A, there is a character c : ℤ ∙ a → ℚ ⧸ ℤ given by m • a ↦ m / n where n is the smallest positive integer such that n • a = 0 and when such n does not exist, c is defined by m • a ↦ m / 2.

theorem CharacterModule.eq_zero_of_ofSpanSingleton_apply_self {A : Type uA} [AddCommGroup A] (a : A) (h : (ofSpanSingleton a) ⟨a, ⋯⟩ = 0) : a = 0

theorem CharacterModule.exists_character_apply_ne_zero_of_ne_zero {A : Type uA} [AddCommGroup A] {a : A} (ne_zero : a ≠ 0) : ∃ (c : CharacterModule A), c a ≠ 0

theorem CharacterModule.eq_zero_of_character_apply {A : Type uA} [AddCommGroup A] {a : A} (h : ∀ (c : CharacterModule A), c a = 0) : a = 0

theorem CharacterModule.dual_surjective_iff_injective {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {A' : Type u_1} [AddCommGroup A'] [Module R A] [Module R A'] {f : A →ₗ[R] A'} : Function.Surjective ⇑(dual f) ↔ Function.Injective ⇑f

theorem rTensor_injective_iff_lcomp_surjective {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {A' : Type u_1} [AddCommGroup A'] {B : Type uB} [AddCommGroup B] [Module R A] [Module R A'] [Module R B] {f : A →ₗ[R] A'} : Function.Injective ⇑(LinearMap.rTensor B f) ↔ Function.Surjective ⇑(LinearMap.lcomp R (CharacterModule B) f)

theorem CharacterModule.surjective_of_dual_injective {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {A' : Type u_1} [AddCommGroup A'] [Module R A] [Module R A'] (f : A →ₗ[R] A') (hf : Function.Injective ⇑(dual f)) : Function.Surjective ⇑f

theorem CharacterModule.dual_injective_iff_surjective {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {A' : Type u_1} [AddCommGroup A'] [Module R A] [Module R A'] {f : A →ₗ[R] A'} : Function.Injective ⇑(dual f) ↔ Function.Surjective ⇑f

theorem CharacterModule.dual_bijective_iff_bijective {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {A' : Type u_1} [AddCommGroup A'] [Module R A] [Module R A'] {f : A →ₗ[R] A'} : Function.Bijective ⇑(dual f) ↔ Function.Bijective ⇑f