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, ℚ ⧸ ℤ).

Equations

• CharacterModule A = (A →+ AddCircle 1)

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

Equations

• CharacterModule.instFunLikeAddCircleRatOfNat A = { coe := fun (c : CharacterModule A) => (↑c).toFun, coe_injective' := ⋯ }

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

Equations

• ⋯ = ⋯

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

Equations

• CharacterModule.instAddCommGroup A = inferInstanceAs (AddCommGroup (A →+ AddCircle 1))

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

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

Equations

• CharacterModule.instModule R A = Module.compHom (A →+ AddCircle 1) (RingEquiv.toOpposite R).toRingHom

@[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⋆.

Equations

• CharacterModule.dual f = { toFun := fun (L : CharacterModule B) => AddMonoidHom.comp L f.toAddMonoidHom, map_add' := ⋯, map_smul' := ⋯ }

@[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) : (CharacterModule.dual f) L = AddMonoidHom.comp L f.toAddMonoidHom

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 ⇑(CharacterModule.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.

Equations

• CharacterModule.congr e = LinearEquiv.ofLinear (CharacterModule.dual ↑e.symm) (CharacterModule.dual ↑e) ⋯ ⋯

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.

Equations

• CharacterModule.uncurry = { toFun := fun (c : A →ₗ[R] CharacterModule B) => TensorProduct.liftAddHom c.toAddMonoidHom ⋯, map_add' := ⋯, map_smul' := ⋯ }

@[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) : CharacterModule.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).

Equations

• One or more equations did not get rendered due to their size.

@[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) : (CharacterModule.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.

Equations

• CharacterModule.homEquiv = LinearEquiv.ofLinear CharacterModule.uncurry CharacterModule.curry ⋯ ⋯

@[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) : ((CharacterModule.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) : (CharacterModule.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') : ↑CharacterModule.homEquiv.symm ∘ₗ CharacterModule.dual (LinearMap.rTensor B f) ∘ₗ ↑CharacterModule.homEquiv = LinearMap.lcomp R (CharacterModule B) f

@[reducible, inline]

abbrev CharacterModule.int : Type

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

Equations

• CharacterModule.int = CharacterModule ℤ

@[reducible, inline]

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

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

Equations

• CharacterModule.int.divByNat n = (LinearMap.toSpanSingleton ℤ (ℚ ⧸ AddSubgroup.zmultiples 1) ↑(↑n)⁻¹).toAddMonoidHom

theorem CharacterModule.int.divByNat_self (n : ℕ) : (CharacterModule.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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CharacterModule.intSpanEquivQuotAddOrderOf_symm_apply_coe {A : Type uA} [AddCommGroup A] (a : A) (a✝ : ℤ ⧸ Ideal.span {↑(addOrderOf a)}) : ↑((CharacterModule.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})) : (CharacterModule.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) : (CharacterModule.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.

Equations

• One or more equations did not get rendered due to their size.

theorem CharacterModule.eq_zero_of_ofSpanSingleton_apply_self {A : Type uA} [AddCommGroup A] (a : A) (h : (CharacterModule.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 ⇑(CharacterModule.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)