The torsion subgroup under a product decomposition

Let A be an abelian group isomorphic to Multiplicative (M × T), where M is a torsion-free additive group and T is a torsion additive group. Then the torsion subgroup of A is exactly the preimage of the factor T, and the quotient A ⧸ torsion A is identified with M. The torsion-factor identification needs only additive monoid structures on the factors; the quotient construction additionally uses an additive group structure on M.

These are the statements behind the uniqueness clauses of the structure theorems for finitely generated abelian groups and for topologically finitely generated abelian pro-p groups: in a decomposition A ≅ M × T of this shape the factor T is the torsion subgroup and M is the torsion-free quotient, so both are determined by A up to isomorphism. The topological version of the quotient identification is TauCeti.quotientTorsionContinuousMulEquiv in TauCeti.Topology.Algebra.Group.Torsion.

Main definitions

• TauCeti.subsingleton_of_mulEquiv: if A is torsion-free, the factor T is trivial (this needs no torsion-freeness hypothesis on M).
• TauCeti.mem_torsion_iff_of_mulEquiv: an element is torsion exactly when its M-coordinate vanishes.
• TauCeti.torsionMulEquiv: the torsion subgroup of A is isomorphic to T.
• TauCeti.natCard_torsion_of_mulEquiv, TauCeti.finite_torsion_of_mulEquiv, TauCeti.isCyclic_torsion_of_mulEquiv: the torsion subgroup of A has the cardinality of T, and it is finite, respectively cyclic, when T is.
• TauCeti.torsionFactorAddEquiv: two decompositions of A have isomorphic torsion factors.
• TauCeti.quotientTorsionMulEquiv: the quotient of A by its torsion subgroup is isomorphic to M.

p-primary torsion abelian groups

An additive commutative group M is p-primary torsion when every element is annihilated by some power of p, that is, when Mathlib's p-primary component AddCommGroup.primaryComponent M p is all of M. This is the additive counterpart of Mathlib's IsPGroup, and it is the class of coefficient modules that cohomological dimension at p is tested on.

Unlike a bound on the exponent, the condition is elementwise: for prime p, ⨁ₖ ZMod (p ^ k) is p-primary torsion but is killed by no single power of p.

Main results

• TauCeti.IsPPrimaryTorsion: every element of M lies in the p-primary component.
• TauCeti.isPPrimaryTorsion_iff: every element is killed by some power of p.
• TauCeti.isPPrimaryTorsion_additive_iff: for a multiplicative group M, Additive M is p-primary torsion exactly when M is a p-group.
• TauCeti.IsPPrimaryTorsion.of_injective, TauCeti.IsPPrimaryTorsion.of_surjective: the condition passes to subgroups and to quotients.
• TauCeti.IsPPrimaryTorsion.isAddTorsion: a p-primary torsion group is torsion when p ≠ 0.
• TauCeti.IsPPrimaryTorsion.exists_pow_smul_eq_zero: a finite p-primary torsion group is annihilated by one power of p.
• TauCeti.exists_mem_primaryComponent_apply_eq: for prime p, a p-primary image of an element of finite order is already the image of a p-primary element.

theorem TauCeti.subsingleton_of_mulEquiv {A : Type u_1} {M : Type u_2} {T : Type u_3} [AddMonoid M] [AddMonoid T] [Monoid A] [IsMulTorsionFree A] (hT : IsAddTorsion T) (e : A ≃* Multiplicative (M × T)) : Subsingleton T

Under an isomorphism A ≃* Multiplicative (M × T) with T torsion, if A is torsion-free then the factor T is trivial: every element of T embeds as a torsion element of A.

theorem TauCeti.mem_torsion_iff_of_mulEquiv {A : Type u_1} {M : Type u_2} {T : Type u_3} [AddMonoid M] [AddMonoid T] [CommGroup A] [IsAddTorsionFree M] (hT : IsAddTorsion T) (e : A ≃* Multiplicative (M × T)) {x : A} : x ∈ CommGroup.torsion A ↔ (Multiplicative.toAdd (e x)).1 = 0

Under an isomorphism A ≃* Multiplicative (M × T) with M torsion-free and T torsion, an element of A is torsion exactly when its M-coordinate vanishes.

def TauCeti.torsionMulEquiv {A : Type u_1} {M : Type u_2} {T : Type u_3} [AddMonoid M] [AddMonoid T] [CommGroup A] [IsAddTorsionFree M] (hT : IsAddTorsion T) (e : A ≃* Multiplicative (M × T)) : ↥(CommGroup.torsion A) ≃* Multiplicative T

Under an isomorphism A ≃* Multiplicative (M × T) with M torsion-free and T torsion, the torsion subgroup of A is the factor T.

Equations

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

@[simp]

theorem TauCeti.torsionMulEquiv_apply {A : Type u_1} {M : Type u_2} {T : Type u_3} [AddMonoid M] [AddMonoid T] [CommGroup A] [IsAddTorsionFree M] (hT : IsAddTorsion T) (e : A ≃* Multiplicative (M × T)) (x : ↥(CommGroup.torsion A)) : (torsionMulEquiv hT e) x = Multiplicative.ofAdd (Multiplicative.toAdd (e ↑x)).2

@[simp]

theorem TauCeti.coe_torsionMulEquiv_symm_apply {A : Type u_1} {M : Type u_2} {T : Type u_3} [AddMonoid M] [AddMonoid T] [CommGroup A] [IsAddTorsionFree M] (hT : IsAddTorsion T) (e : A ≃* Multiplicative (M × T)) (t : Multiplicative T) : ↑((torsionMulEquiv hT e).symm t) = e.symm (Multiplicative.ofAdd (0, Multiplicative.toAdd t))

def TauCeti.torsionFactorAddEquiv {A : Type u_1} {M : Type u_2} {T : Type u_3} [AddMonoid M] [AddMonoid T] [CommGroup A] [IsAddTorsionFree M] {M' : Type u_4} {T' : Type u_5} [AddMonoid M'] [IsAddTorsionFree M'] [AddMonoid T'] (hT : IsAddTorsion T) (hT' : IsAddTorsion T') (e : A ≃* Multiplicative (M × T)) (e' : A ≃* Multiplicative (M' × T')) : T ≃+ T'

Two decompositions of A as torsion-free times torsion have isomorphic torsion factors: both are the torsion subgroup of A.

Equations

• TauCeti.torsionFactorAddEquiv hT hT' e e' = AddEquiv.toMultiplicative.symm ((TauCeti.torsionMulEquiv hT e).symm.trans (TauCeti.torsionMulEquiv hT' e'))

@[simp]

theorem TauCeti.torsionFactorAddEquiv_apply {A : Type u_1} {M : Type u_2} {T : Type u_3} [AddMonoid M] [AddMonoid T] [CommGroup A] [IsAddTorsionFree M] {M' : Type u_4} {T' : Type u_5} [AddMonoid M'] [IsAddTorsionFree M'] [AddMonoid T'] (hT : IsAddTorsion T) (hT' : IsAddTorsion T') (e : A ≃* Multiplicative (M × T)) (e' : A ≃* Multiplicative (M' × T')) (t : T) : (torsionFactorAddEquiv hT hT' e e') t = (Multiplicative.toAdd (e' (e.symm (Multiplicative.ofAdd (0, t))))).2

@[simp]

theorem TauCeti.torsionFactorAddEquiv_symm_apply {A : Type u_1} {M : Type u_2} {T : Type u_3} [AddMonoid M] [AddMonoid T] [CommGroup A] [IsAddTorsionFree M] {M' : Type u_4} {T' : Type u_5} [AddMonoid M'] [IsAddTorsionFree M'] [AddMonoid T'] (hT : IsAddTorsion T) (hT' : IsAddTorsion T') (e : A ≃* Multiplicative (M × T)) (e' : A ≃* Multiplicative (M' × T')) (t' : T') : (torsionFactorAddEquiv hT hT' e e').symm t' = (Multiplicative.toAdd (e (e'.symm (Multiplicative.ofAdd (0, t'))))).2

theorem TauCeti.natCard_torsion_of_mulEquiv {A : Type u_1} {M : Type u_2} {T : Type u_3} [AddMonoid M] [AddMonoid T] [CommGroup A] [IsAddTorsionFree M] (hT : IsAddTorsion T) (e : A ≃* Multiplicative (M × T)) : Nat.card ↥(CommGroup.torsion A) = Nat.card T

Under an isomorphism A ≃* Multiplicative (M × T) with M torsion-free and T torsion, the torsion subgroup of A has the cardinality of T.

theorem TauCeti.finite_torsion_of_mulEquiv {A : Type u_1} {M : Type u_2} {T : Type u_3} [CommGroup A] [AddMonoid M] [AddGroup T] [IsAddTorsionFree M] [Finite T] (e : A ≃* Multiplicative (M × T)) : Finite ↥(CommGroup.torsion A)

Under an isomorphism A ≃* Multiplicative (M × T) with M torsion-free and T finite, the torsion subgroup of A is finite.

theorem TauCeti.isCyclic_torsion_of_mulEquiv {A : Type u_1} {M : Type u_2} {T : Type u_3} [CommGroup A] [AddMonoid M] [AddGroup T] [IsAddTorsionFree M] [IsAddCyclic T] (hT : IsAddTorsion T) (e : A ≃* Multiplicative (M × T)) : IsCyclic ↥(CommGroup.torsion A)

Under an isomorphism A ≃* Multiplicative (M × T) with M torsion-free and T a cyclic torsion group, the torsion subgroup of A is cyclic.

noncomputable def TauCeti.quotientTorsionMulEquiv {A : Type u_1} {M : Type u_2} {T : Type u_3} [CommGroup A] [AddGroup M] [AddMonoid T] [IsAddTorsionFree M] (hT : IsAddTorsion T) (e : A ≃* Multiplicative (M × T)) : A ⧸ CommGroup.torsion A ≃* Multiplicative M

Under an isomorphism A ≃* Multiplicative (M × T) with M torsion-free and T torsion, the quotient of A by its torsion subgroup is the factor M.

Equations

• TauCeti.quotientTorsionMulEquiv hT e = QuotientGroup.liftEquiv (CommGroup.torsion A) ⋯ ⋯

@[simp]

theorem TauCeti.quotientTorsionMulEquiv_mk {A : Type u_1} {M : Type u_2} {T : Type u_3} [CommGroup A] [AddGroup M] [AddMonoid T] [IsAddTorsionFree M] (hT : IsAddTorsion T) (e : A ≃* Multiplicative (M × T)) (x : A) : (quotientTorsionMulEquiv hT e) ↑x = Multiplicative.ofAdd (Multiplicative.toAdd (e x)).1

@[simp]

theorem TauCeti.quotientTorsionMulEquiv_symm_apply {A : Type u_1} {M : Type u_2} {T : Type u_3} [CommGroup A] [AddGroup M] [AddMonoid T] [IsAddTorsionFree M] (hT : IsAddTorsion T) (e : A ≃* Multiplicative (M × T)) (v : Multiplicative M) : (quotientTorsionMulEquiv hT e).symm v = ↑(e.symm (Multiplicative.ofAdd (Multiplicative.toAdd v, 0)))

def TauCeti.IsPPrimaryTorsion (p : ℕ) (M : Type u_6) [AddCommGroup M] : Prop

An additive commutative group is p-primary torsion when every element lies in its p-primary component, that is, is annihilated by some power of p.

Equations

• TauCeti.IsPPrimaryTorsion p M = ∀ (m : M), m ∈ AddCommGroup.primaryComponent M p

theorem TauCeti.IsPPrimaryTorsion.mem {p : ℕ} {M : Type u_4} [AddCommGroup M] (h : IsPPrimaryTorsion p M) (m : M) : m ∈ AddCommGroup.primaryComponent M p

Every element of a p-primary torsion group lies in the p-primary component.

theorem TauCeti.isPPrimaryTorsion_iff {p : ℕ} {M : Type u_4} [AddCommGroup M] : IsPPrimaryTorsion p M ↔ ∀ (m : M), ∃ (k : ℕ), p ^ k • m = 0

A group is p-primary torsion exactly when every element is killed by some power of p.

theorem TauCeti.isPPrimaryTorsion_iff_primaryComponent_eq_top {p : ℕ} {M : Type u_4} [AddCommGroup M] : IsPPrimaryTorsion p M ↔ AddCommGroup.primaryComponent M p = ⊤

A group is p-primary torsion exactly when its p-primary component is everything.

theorem TauCeti.isPPrimaryTorsion_additive_iff {p : ℕ} {M : Type u_6} [CommGroup M] : IsPPrimaryTorsion p (Additive M) ↔ IsPGroup p M

For a multiplicative commutative group M, Additive M is p-primary torsion exactly when M is a p-group.

theorem TauCeti.isPPrimaryTorsion_of_natCard_eq_pow {p : ℕ} {M : Type u_4} [AddCommGroup M] {k : ℕ} (h : Nat.card M = p ^ k) : IsPPrimaryTorsion p M

A group of order p ^ k is p-primary torsion: the additive form of IsPGroup.of_card.

theorem TauCeti.IsPPrimaryTorsion.of_injective {p : ℕ} {M : Type u_4} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] {F : Type u_6} [FunLike F M N] [AddMonoidHomClass F M N] (h : IsPPrimaryTorsion p N) (f : F) (hf : Function.Injective ⇑f) : IsPPrimaryTorsion p M

A group embedding into a p-primary torsion group is p-primary torsion.

theorem TauCeti.IsPPrimaryTorsion.of_surjective {p : ℕ} {M : Type u_4} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] {F : Type u_6} [FunLike F M N] [AddMonoidHomClass F M N] (h : IsPPrimaryTorsion p M) (f : F) (hf : Function.Surjective ⇑f) : IsPPrimaryTorsion p N

The image of a p-primary torsion group under a surjective homomorphism is p-primary torsion.

theorem TauCeti.IsPPrimaryTorsion.isAddTorsion {p : ℕ} {M : Type u_4} [AddCommGroup M] (h : IsPPrimaryTorsion p M) (hp : p ≠ 0) : IsAddTorsion M

A p-primary torsion group is torsion, for p ≠ 0: the power of p killing an element is a positive natural number. The hypothesis is used, since 0 ^ k • m = 0 holds for k = 1 and every m.

theorem TauCeti.IsPPrimaryTorsion.exists_pow_smul_eq_zero {p : ℕ} {M : Type u_4} [AddCommGroup M] [Finite M] (h : IsPPrimaryTorsion p M) : ∃ (k : ℕ), ∀ (m : M), p ^ k • m = 0

A finite p-primary torsion group is annihilated by one power of p.

theorem TauCeti.exists_mem_primaryComponent_apply_eq {p : ℕ} {M : Type u_4} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] {F : Type u_6} [FunLike F M N] [AddMonoidHomClass F M N] (f : F) (hp : Nat.Prime p) {m : M} (hm : IsOfFinAddOrder m) (hfm : f m ∈ AddCommGroup.primaryComponent N p) : ∃ m' ∈ AddCommGroup.primaryComponent M p, f m' = f m

A p-primary image of an element of finite order has a p-primary preimage. For prime p, an additive homomorphism f and an element m of finite order with f m in the p-primary component, some element of the p-primary component has the same image.