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.instFunLikeCharacterModuleAddCircleRatInstLinearOrderedAddCommGroupRatToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceInstMetricSpaceRatInstOrderTopologyRatToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceInstMetricSpaceRatInstPreorderRatOfNatInstOfNatRat (A : Type uA) [AddCommGroup A] : FunLike (CharacterModule A) A (AddCircle 1)

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

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

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

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

Equations

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

@[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)

@[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 (LinearMap.toAddMonoidHom f)

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 = { toAddHom := { toFun := fun (L : CharacterModule B) => AddMonoidHom.comp L (LinearMap.toAddMonoidHom f), map_add' := ⋯ }, map_smul' := ⋯ }

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 ↑(LinearEquiv.symm e)) (CharacterModule.dual ↑e) ⋯ ⋯

@[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 (LinearMap.toAddMonoidHom c) ⋯

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

• 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.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.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 : AddCon.Quotient (addConGen (TensorProduct.Eqv R A B))) : (CharacterModule.homEquiv c) x = AddCon.liftOn x ⇑(FreeAddMonoid.lift fun (mn : A × B) => ((LinearMap.toAddMonoidHom c) mn.1) mn.2) ⋯

@[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_1 : B), (((LinearEquiv.symm CharacterModule.homEquiv) a) x) a_1 = a (x ⊗ₜ[R] a_1)

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 ⋯ ⋯

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

@[inline, reducible]

abbrev CharacterModule.int : Type

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

Equations

• CharacterModule.int = CharacterModule ℤ

@[inline, reducible]

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

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

Equations

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

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

@[simp]

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

@[simp]

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

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.

theorem CharacterModule.intSpanEquivQuotAddOrderOf_apply_self {A : Type uA} [AddCommGroup A] (a : A) : (CharacterModule.intSpanEquivQuotAddOrderOf a) { val := a, property := ⋯ } = 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) { val := a, property := ⋯ } = 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)