The torsion of a representation, and the connecting map of multiplication by a scalar

For a representation ρ of a monoid G on a module V over a commutative ring k and an element r : k, every operator ρ g is k-linear and so preserves the r-torsion V[r] = Submodule.torsionBy k V r. The representation therefore restricts to it; this is Representation.torsionBy, the kernel counterpart of the reduction Representation.quotSMulTop on the cokernel V ⧸ rV. An intertwining map restricts to the torsion (Representation.IntertwiningMap.torsionBy), as it reduces modulo r (Representation.IntertwiningMap.quotSMulTop).

For a short exact sequence 0 → V₁ → V₂ → V₃ → 0 of representations, the snake lemma for multiplication by r gives the six-term exact sequence

0 → V₁[r] → V₂[r] → V₃[r] → V₁ ⧸ rV₁ → V₂ ⧸ rV₂ → V₃ ⧸ rV₃ → 0

of TauCeti/Algebra/Module/Torsion/Snake.lean. Each g : G acts on the short exact sequence by a morphism of short exact sequences, so naturality of the connecting map (TauCeti.torsionByδ_comp_torsionByMap) makes it intertwining (Representation.IntertwiningMap.torsionByδ): the whole six-term sequence is a sequence of representations. For k = ℤ, r = ℓ a prime and G a group acting on abelian groups, this is the sequence of G-modules behind the comparison of V ⧸ ℓV with V[ℓ] in Neukirch–Schmidt–Wingberg, Cohomology of Number Fields, (7.3.3).

Main definitions

• Representation.torsionBy: the representation induced by ρ on the r-torsion V[r].
• Representation.IntertwiningMap.torsionBy: the restriction of an intertwining map to the r-torsion.
• Representation.IntertwiningMap.torsionByδ: the connecting map V₃[r] → V₁ ⧸ rV₁ of a short exact sequence of representations, as an intertwining map.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Springer (2008), §VII.3, (7.3.3).

noncomputable def Representation.torsionBy {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (r : k) : Representation k G ↥(Submodule.torsionBy k V r)

The representation induced by ρ on the r-torsion V[r] = Submodule.torsionBy k V r: Mathlib's subrepresentation on the G-stable submodule V[r]. Its operators are the restrictions TauCeti.torsionByMap r (ρ g) (Representation.torsionBy_apply).

@[simp]

theorem Representation.torsionBy_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (r : k) (g : G) : (ρ.torsionBy r) g = TauCeti.torsionByMap r (ρ g)

The operators of ρ.torsionBy r are the restrictions TauCeti.torsionByMap r (ρ g).

theorem Representation.coe_torsionBy_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (r : k) (g : G) (x : ↥(Submodule.torsionBy k V r)) : ↑(((ρ.torsionBy r) g) x) = (ρ g) ↑x

ρ.torsionBy r g acts on an r-torsion vector as ρ g.

noncomputable def Representation.IntertwiningMap.torsionBy {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] {W : Type u_4} [AddCommGroup W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} (f : ρ.IntertwiningMap σ) (r : k) : (ρ.torsionBy r).IntertwiningMap (σ.torsionBy r)

Restriction of an intertwining map to the r-torsion: TauCeti.torsionByMap r f intertwines ρ.torsionBy r and σ.torsionBy r.

@[simp]

theorem Representation.IntertwiningMap.toLinearMap_torsionBy {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] {W : Type u_4} [AddCommGroup W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} (f : ρ.IntertwiningMap σ) (r : k) : (f.torsionBy r).toLinearMap = TauCeti.torsionByMap r f.toLinearMap

The linear map underlying the restriction of an intertwining map is TauCeti.torsionByMap.

noncomputable def Representation.IntertwiningMap.torsionByδ {k : Type u_1} {G : Type u_2} [CommRing k] [Monoid G] {V₁ : Type u_5} {V₂ : Type u_6} {V₃ : Type u_7} [AddCommGroup V₁] [Module k V₁] [AddCommGroup V₂] [Module k V₂] [AddCommGroup V₃] [Module k V₃] {ρ₁ : Representation k G V₁} {ρ₂ : Representation k G V₂} {ρ₃ : Representation k G V₃} {f : ρ₁.IntertwiningMap ρ₂} {g : ρ₂.IntertwiningMap ρ₃} (r : k) (hfg : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) : (ρ₃.torsionBy r).IntertwiningMap (ρ₁.quotSMulTop r)

The connecting map of a short exact sequence of representations for multiplication by r: the snake-lemma map TauCeti.torsionByδ r : V₃[r] → V₁ ⧸ rV₁ of 0 → V₁ → V₂ → V₃ → 0 intertwines ρ₃.torsionBy r and ρ₁.quotSMulTop r. Each γ : G acts on the sequence by the morphism (ρ₁ γ, ρ₂ γ, ρ₃ γ), which the connecting map commutes with by naturality.

@[simp]

theorem Representation.IntertwiningMap.toLinearMap_torsionByδ {k : Type u_1} {G : Type u_2} [CommRing k] [Monoid G] {V₁ : Type u_5} {V₂ : Type u_6} {V₃ : Type u_7} [AddCommGroup V₁] [Module k V₁] [AddCommGroup V₂] [Module k V₂] [AddCommGroup V₃] [Module k V₃] {ρ₁ : Representation k G V₁} {ρ₂ : Representation k G V₂} {ρ₃ : Representation k G V₃} {f : ρ₁.IntertwiningMap ρ₂} {g : ρ₂.IntertwiningMap ρ₃} (r : k) (hfg : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) : (torsionByδ r hfg hf hg).toLinearMap = TauCeti.torsionByδ r hfg hf hg

The linear map underlying the connecting map of representations is TauCeti.torsionByδ.