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 ofR
-modules whereM ↦ M⋆
and anR
-linear mapl : M ⟶ N
induces anR
-linear mapl⋆ : f ↦ f ∘ l
wheref : N⋆
.LinearMap.dual_surjective_of_injective
: Ifl
is injective thenl⋆
is surjective, in another word taking character module as a functor sends monos to epis.CharacterModule.homEquiv
: there is a bijection between linear mapHom(N, M⋆)
and(N ⊗ M)⋆
given bycurry
anduncurry
.
The character module of an abelian group A
in the unit rational circle is A⋆ := Hom_ℤ(A, ℚ ⧸ ℤ)
.
Equations
- CharacterModule A = (A →+ AddCircle 1)
Instances For
Equations
- CharacterModule.instFunLikeAddCircleRatOfNat A = { coe := fun (c : CharacterModule A) => (↑c).toFun, coe_injective' := ⋯ }
Equations
Equations
- CharacterModule.instModule R A = Module.compHom (A →+ AddCircle 1) (RingEquiv.toOpposite R).toRingHom
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' := ⋯ }
Instances For
Two isomorphic modules have isomorphic character modules.
Equations
- CharacterModule.congr e = LinearEquiv.ofLinear (CharacterModule.dual ↑e.symm) (CharacterModule.dual ↑e) ⋯ ⋯
Instances For
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' := ⋯ }
Instances For
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.
Instances For
Linear maps into a character module are exactly characters of the tensor product.
Equations
- CharacterModule.homEquiv = LinearEquiv.ofLinear CharacterModule.uncurry CharacterModule.curry ⋯ ⋯
Instances For
ℤ⋆
, the character module of ℤ
in the unit rational circle.
Equations
Instances For
Given n : ℕ
, the map m ↦ m / n
.
Equations
- CharacterModule.int.divByNat n = (LinearMap.toSpanSingleton ℤ (ℚ ⧸ AddSubgroup.zmultiples 1) ↑(↑n)⁻¹).toAddMonoidHom
Instances For
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.
Instances For
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.