Torsion groups

This file defines torsion groups, i.e. groups where all elements have finite order.

Main definitions

• Monoid.IsTorsion a predicate asserting G is torsion, i.e. that all elements are of finite order.
• CommGroup.torsion G, the torsion subgroup of an abelian group G
• CommMonoid.torsion G, the above stated for commutative monoids
• Monoid.IsTorsionFree, asserting no nontrivial elements have finite order in G
• AddMonoid.IsTorsion and AddMonoid.IsTorsionFree the additive versions of the above

Implementation

All torsion monoids are really groups (which is proven here as Monoid.IsTorsion.group), but since the definition can be stated on monoids it is implemented on Monoid to match other declarations in the group theory library.

Tags

periodic group, aperiodic group, torsion subgroup, torsion abelian group

Future work

• generalize to π-torsion(-free) groups for a set of primes π
• free, free solvable and free abelian groups are torsion free
• complete direct and free products of torsion free groups are torsion free
• groups which are residually finite p-groups with respect to 2 distinct primes are torsion free

def Monoid.IsTorsion (G : Type u_1) [Monoid G] : Prop

A predicate on a monoid saying that all elements are of finite order.

def AddMonoid.IsTorsion (G : Type u_1) [AddMonoid G] : Prop

A predicate on an additive monoid saying that all elements are of finite order.

@[simp]

theorem Monoid.not_isTorsion_iff (G : Type u_1) [Monoid G] : ¬IsTorsion G ↔ ∃ (g : G), ¬IsOfFinOrder g

A monoid is not a torsion monoid if it has an element of infinite order.

@[simp]

theorem AddMonoid.not_isTorsion_iff (G : Type u_1) [AddMonoid G] : ¬IsTorsion G ↔ ∃ (g : G), ¬IsOfFinAddOrder g

An additive monoid is not a torsion monoid if it has an element of infinite order.

noncomputable def IsTorsion.group {G : Type u_1} [Monoid G] (tG : Monoid.IsTorsion G) : Group G

Torsion monoids are really groups.

noncomputable def IsTorsion.addGroup {G : Type u_1} [AddMonoid G] (tG : AddMonoid.IsTorsion G) : AddGroup G

Torsion additive monoids are really additive groups

theorem IsTorsion.subgroup {G : Type u_1} [Group G] (tG : Monoid.IsTorsion G) (H : Subgroup G) : Monoid.IsTorsion ↥H

Subgroups of torsion groups are torsion groups.

theorem IsTorsion.addSubgroup {G : Type u_1} [AddGroup G] (tG : AddMonoid.IsTorsion G) (H : AddSubgroup G) : AddMonoid.IsTorsion ↥H

Subgroups of additive torsion groups are additive torsion groups.

theorem IsTorsion.of_surjective {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G →* H} (hf : Function.Surjective ⇑f) (tG : Monoid.IsTorsion G) : Monoid.IsTorsion H

The image of a surjective torsion group homomorphism is torsion.

theorem AddIsTorsion.of_surjective {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G →+ H} (hf : Function.Surjective ⇑f) (tG : AddMonoid.IsTorsion G) : AddMonoid.IsTorsion H

The image of a surjective additive torsion group homomorphism is torsion.

theorem IsTorsion.extension_closed {G : Type u_1} {H : Type u_2} [Group G] {N : Subgroup G} [Group H] {f : G →* H} (hN : N = f.ker) (tH : Monoid.IsTorsion H) (tN : Monoid.IsTorsion ↥N) : Monoid.IsTorsion G

Torsion groups are closed under extensions.

theorem AddIsTorsion.extension_closed {G : Type u_1} {H : Type u_2} [AddGroup G] {N : AddSubgroup G} [AddGroup H] {f : G →+ H} (hN : N = f.ker) (tH : AddMonoid.IsTorsion H) (tN : AddMonoid.IsTorsion ↥N) : AddMonoid.IsTorsion G

Additive torsion groups are closed under extensions.

theorem IsTorsion.quotient_iff {G : Type u_1} {H : Type u_2} [Group G] {N : Subgroup G} [Group H] {f : G →* H} (hf : Function.Surjective ⇑f) (hN : N = f.ker) (tN : Monoid.IsTorsion ↥N) : Monoid.IsTorsion H ↔ Monoid.IsTorsion G

The image of a quotient is torsion iff the group is torsion.

theorem AddIsTorsion.quotient_iff {G : Type u_1} {H : Type u_2} [AddGroup G] {N : AddSubgroup G} [AddGroup H] {f : G →+ H} (hf : Function.Surjective ⇑f) (hN : N = f.ker) (tN : AddMonoid.IsTorsion ↥N) : AddMonoid.IsTorsion H ↔ AddMonoid.IsTorsion G

The image of a quotient is additively torsion iff the group is torsion.

theorem ExponentExists.isTorsion {G : Type u_1} [Group G] (h : Monoid.ExponentExists G) : Monoid.IsTorsion G

If a group exponent exists, the group is torsion.

theorem ExponentExists.is_add_torsion {G : Type u_1} [AddGroup G] (h : AddMonoid.ExponentExists G) : AddMonoid.IsTorsion G

If a group exponent exists, the group is additively torsion.

theorem IsTorsion.exponentExists {G : Type u_1} [Group G] (tG : Monoid.IsTorsion G) (bounded : (Set.range fun (g : G) => orderOf g).Finite) : Monoid.ExponentExists G

The group exponent exists for any bounded torsion group.

theorem IsAddTorsion.exponentExists {G : Type u_1} [AddGroup G] (tG : AddMonoid.IsTorsion G) (bounded : (Set.range fun (g : G) => addOrderOf g).Finite) : AddMonoid.ExponentExists G

The group exponent exists for any bounded additive torsion group.

theorem isTorsion_of_finite {G : Type u_1} [Group G] [Finite G] : Monoid.IsTorsion G

Finite groups are torsion groups.

theorem is_add_torsion_of_finite {G : Type u_1} [AddGroup G] [Finite G] : AddMonoid.IsTorsion G

Finite additive groups are additive torsion groups.

theorem not_isMulTorsionFree_of_isTorsion {G : Type u_1} [CommGroup G] [Nontrivial G] (hG : Monoid.IsTorsion G) : ¬IsMulTorsionFree G

A nontrivial torsion abelian group is not torsion-free.

theorem not_isAddTorsionFree_of_isTorsion {G : Type u_1} [AddCommGroup G] [Nontrivial G] (hG : AddMonoid.IsTorsion G) : ¬IsAddTorsionFree G

A nontrivial additive torsion abelian group is not torsion-free.

theorem not_isTorsion_of_isMulTorsionFree {G : Type u_1} [CommGroup G] [Nontrivial G] [IsMulTorsionFree G] : ¬Monoid.IsTorsion G

A nontrivial torsion-free abelian group is not torsion.

theorem not_isTorsion_of_isAddTorsionFree {G : Type u_1} [AddCommGroup G] [Nontrivial G] [IsAddTorsionFree G] : ¬AddMonoid.IsTorsion G

A nontrivial additive torsion-free abelian group is not torsion.

theorem AddMonoid.IsTorsion.module_of_torsion (R : Type u_3) (M : Type u_4) [AddCommMonoid M] [Semiring R] [Module R M] (tR : IsTorsion R) : IsTorsion M

A module whose scalars are additively torsion is additively torsion.

theorem AddMonoid.IsTorsion.module_of_finite (R : Type u_3) (M : Type u_4) [AddCommMonoid M] [Ring R] [Finite R] [Module R M] : IsTorsion M

A module with a finite ring of scalars is additively torsion.

def CommMonoid.torsion (G : Type u_1) [CommMonoid G] : Submonoid G

The torsion submonoid of a commutative monoid.

(Note that by Monoid.IsTorsion.group torsion monoids are truthfully groups.)

def AddCommMonoid.addTorsion (G : Type u_1) [AddCommMonoid G] : AddSubmonoid G

The torsion submonoid of an additive commutative monoid.

theorem CommMonoid.torsion.isTorsion {G : Type u_1} [CommMonoid G] : Monoid.IsTorsion ↥(torsion G)

Torsion submonoids are torsion.

theorem AddCommMonoid.addTorsion.isTorsion {G : Type u_1} [AddCommMonoid G] : AddMonoid.IsTorsion ↥(addTorsion G)

Additive torsion submonoids are additively torsion.

def CommMonoid.primaryComponent (G : Type u_1) [CommMonoid G] (p : ℕ) [hp : Fact (Nat.Prime p)] : Submonoid G

The p-primary component is the submonoid of elements with order prime-power of p.

def AddCommMonoid.primaryComponent (G : Type u_1) [AddCommMonoid G] (p : ℕ) [hp : Fact (Nat.Prime p)] : AddSubmonoid G

The p-primary component is the submonoid of elements with additive order prime-power of p.

@[simp]

theorem CommMonoid.coe_primaryComponent (G : Type u_1) [CommMonoid G] (p : ℕ) [hp : Fact (Nat.Prime p)] : ↑(primaryComponent G p) = {g : G | ∃ (n : ℕ), orderOf g = p ^ n}

@[simp]

theorem AddCommMonoid.coe_primaryComponent (G : Type u_1) [AddCommMonoid G] (p : ℕ) [hp : Fact (Nat.Prime p)] : ↑(primaryComponent G p) = {g : G | ∃ (n : ℕ), addOrderOf g = p ^ n}

theorem CommMonoid.primaryComponent.exists_orderOf_eq_prime_pow {G : Type u_1} [CommMonoid G] {p : ℕ} [hp : Fact (Nat.Prime p)] (g : ↥(primaryComponent G p)) : ∃ (n : ℕ), orderOf g = p ^ n

Elements of the p-primary component have order p^n for some n.

theorem AddCommMonoid.primaryComponent.exists_orderOf_eq_prime_nsmul {G : Type u_1} [AddCommMonoid G] {p : ℕ} [hp : Fact (Nat.Prime p)] (g : ↥(primaryComponent G p)) : ∃ (n : ℕ), addOrderOf g = p ^ n

Elements of the p-primary component have additive order p^n for some n

theorem CommMonoid.primaryComponent.disjoint {G : Type u_1} [CommMonoid G] {p : ℕ} [hp : Fact (Nat.Prime p)] {p' : ℕ} [hp' : Fact (Nat.Prime p')] (hne : p ≠ p') : Disjoint (primaryComponent G p) (primaryComponent G p')

The p- and q-primary components are disjoint for p ≠ q.

theorem AddCommMonoid.primaryComponent.disjoint {G : Type u_1} [AddCommMonoid G] {p : ℕ} [hp : Fact (Nat.Prime p)] {p' : ℕ} [hp' : Fact (Nat.Prime p')] (hne : p ≠ p') : Disjoint (primaryComponent G p) (primaryComponent G p')

The p- and q-primary components are disjoint for p ≠ q.

@[simp]

theorem Monoid.IsTorsion.torsion_eq_top {G : Type u_1} [CommMonoid G] (tG : IsTorsion G) : CommMonoid.torsion G = ⊤

The torsion submonoid of a torsion monoid is ⊤.

@[simp]

theorem AddMonoid.IsTorsion.torsion_eq_top {G : Type u_1} [AddCommMonoid G] (tG : IsTorsion G) : AddCommMonoid.addTorsion G = ⊤

The additive torsion submonoid of an additive torsion monoid is ⊤.

def Monoid.IsTorsion.torsionMulEquiv {G : Type u_1} [CommMonoid G] (tG : IsTorsion G) : ↥(CommMonoid.torsion G) ≃* G

A torsion monoid is isomorphic to its torsion submonoid.

def AddMonoid.IsTorsion.torsionAddEquiv {G : Type u_1} [AddCommMonoid G] (tG : IsTorsion G) : ↥(AddCommMonoid.addTorsion G) ≃+ G

An additive torsion monoid is isomorphic to its torsion submonoid.

theorem Monoid.IsTorsion.torsionMulEquiv_apply {G : Type u_1} [CommMonoid G] (tG : IsTorsion G) (a : ↥(CommMonoid.torsion G)) : tG.torsionMulEquiv a = ↑((MulEquiv.submonoidCongr ⋯) a)

theorem AddMonoid.IsTorsion.torsionAddEquiv_apply {G : Type u_1} [AddCommMonoid G] (tG : IsTorsion G) (a : ↥(AddCommMonoid.addTorsion G)) : tG.torsionAddEquiv a = ↑((AddEquiv.addSubmonoidCongr ⋯) a)

theorem Monoid.IsTorsion.torsionMulEquiv_symm_apply_coe {G : Type u_1} [CommMonoid G] (tG : IsTorsion G) (a : G) : tG.torsionMulEquiv.symm a = ⟨↑(Submonoid.topEquiv.symm a), ⋯⟩

theorem AddMonoid.IsTorsion.torsionAddEquiv_symm_apply_coe {G : Type u_1} [AddCommMonoid G] (tG : IsTorsion G) (a : G) : tG.torsionAddEquiv.symm a = ⟨↑(AddSubmonoid.topEquiv.symm a), ⋯⟩

def Torsion.ofTorsion (G : Type u_1) [CommMonoid G] : ↥(CommMonoid.torsion ↥(CommMonoid.torsion G)) ≃* ↥(CommMonoid.torsion G)

Torsion submonoids of a torsion submonoid are isomorphic to the submonoid.

def AddCommMonoid.Torsion.ofTorsion (G : Type u_1) [AddCommMonoid G] : ↥(addTorsion ↥(addTorsion G)) ≃+ ↥(addTorsion G)

Additive torsion submonoids of an additive torsion submonoid are isomorphic to the submonoid.

def CommGroup.torsion (G : Type u_1) [CommGroup G] : Subgroup G

The torsion subgroup of an abelian group.

def AddCommGroup.torsion (G : Type u_1) [AddCommGroup G] : AddSubgroup G

The torsion subgroup of an additive abelian group.

theorem CommGroup.torsion_eq_torsion_submonoid (G : Type u_1) [CommGroup G] : CommMonoid.torsion G = (torsion G).toSubmonoid

The torsion submonoid of an abelian group equals the torsion subgroup as a submonoid.

theorem AddCommGroup.add_torsion_eq_add_torsion_submonoid (G : Type u_1) [AddCommGroup G] : AddCommMonoid.addTorsion G = (torsion G).toAddSubmonoid

The additive torsion submonoid of an abelian group equals the torsion subgroup as a submonoid.

theorem CommGroup.mem_torsion (G : Type u_1) [CommGroup G] (g : G) : g ∈ torsion G ↔ IsOfFinOrder g

theorem AddCommGroup.mem_torsion (G : Type u_1) [AddCommGroup G] (g : G) : g ∈ torsion G ↔ IsOfFinAddOrder g

theorem CommGroup.isMulTorsionFree_iff_torsion_eq_bot (G : Type u_1) [CommGroup G] : IsMulTorsionFree G ↔ torsion G = ⊥

theorem AddCommGroup.isAddTorsionFree_iff_torsion_eq_bot (G : Type u_1) [AddCommGroup G] : IsAddTorsionFree G ↔ torsion G = ⊥

def CommGroup.primaryComponent (G : Type u_1) [CommGroup G] (p : ℕ) [hp : Fact (Nat.Prime p)] : Subgroup G

The p-primary component is the subgroup of elements with order prime-power of p.

def AddCommGroup.primaryComponent (G : Type u_1) [AddCommGroup G] (p : ℕ) [hp : Fact (Nat.Prime p)] : AddSubgroup G

The p-primary component is the subgroup of elements with additive order prime-power of p.

@[simp]

theorem CommGroup.coe_primaryComponent (G : Type u_1) [CommGroup G] (p : ℕ) [hp : Fact (Nat.Prime p)] : ↑(primaryComponent G p) = {g : G | ∃ (n : ℕ), orderOf g = p ^ n}

@[simp]

theorem AddCommGroup.coe_primaryComponent (G : Type u_1) [AddCommGroup G] (p : ℕ) [hp : Fact (Nat.Prime p)] : ↑(primaryComponent G p) = {g : G | ∃ (n : ℕ), addOrderOf g = p ^ n}

theorem CommGroup.primaryComponent.isPGroup {G : Type u_1} [CommGroup G] {p : ℕ} [hp : Fact (Nat.Prime p)] : IsPGroup p ↥(primaryComponent G p)

The p-primary component is a p group.

@[deprecated IsMulTorsionFree (since := "2025-04-23")]

def Monoid.IsTorsionFree (G : Type u_1) [Monoid G] : Prop

A predicate on a monoid saying that only 1 is of finite order.

This definition is mathematically incorrect for monoids which are not groups. Please use IsMulTorsionFree instead.

@[deprecated IsAddTorsionFree (since := "2025-04-23")]

def AddMonoid.IsTorsionFree (G : Type u_1) [AddMonoid G] : Prop

A predicate on an additive monoid saying that only 0 is of finite order.

This definition is mathematically incorrect for monoids which are not groups. Please use IsAddTorsionFree instead.

@[deprecated not_isMulTorsionFree_iff_isOfFinOrder (since := "2025-04-23")]

theorem Monoid.not_isTorsionFree_iff {G : Type u_1} [Monoid G] : ¬IsTorsionFree G ↔ ∃ (g : G), g ≠ 1 ∧ IsOfFinOrder g

A nontrivial monoid is not torsion-free if any nontrivial element has finite order.

@[deprecated not_isMulTorsionFree_iff_isOfFinOrder (since := "2025-04-23")]

theorem AddMonoid.not_isTorsionFree_iff {G : Type u_1} [AddMonoid G] : ¬IsTorsionFree G ↔ ∃ (g : G), g ≠ 0 ∧ IsOfFinAddOrder g

An additive monoid is not torsion free if any nontrivial element has finite order.

@[deprecated Subsingleton.to_isMulTorsionFree (since := "2025-04-23")]

theorem Monoid.isTorsionFree_of_subsingleton {G : Type u_1} [Monoid G] [Subsingleton G] : IsTorsionFree G

@[deprecated Subsingleton.to_isMulTorsionFree (since := "2025-04-23")]

theorem AddMonoid.isTorsionFree_of_subsingleton {G : Type u_1} [AddMonoid G] [Subsingleton G] : IsTorsionFree G

@[deprecated CommGroup.isMulTorsionFree_iff_torsion_eq_bot (since := "2025-04-23")]

theorem Monoid.isTorsionFree_iff_torsion_eq_bot {G : Type u_3} [CommGroup G] : IsTorsionFree G ↔ CommGroup.torsion G = ⊥

@[deprecated CommGroup.isMulTorsionFree_iff_torsion_eq_bot (since := "2025-04-23")]

theorem AddMonoid.isTorsionFree_iff_torsion_eq_bot {G : Type u_3} [AddCommGroup G] : IsTorsionFree G ↔ AddCommGroup.torsion G = ⊥

@[deprecated not_isMulTorsionFree_of_isTorsion (since := "2025-04-23")]

theorem Monoid.IsTorsion.not_torsion_free {G : Type u_1} [Group G] [hN : Nontrivial G] : IsTorsion G → ¬IsTorsionFree G

A nontrivial torsion group is not torsion-free.

@[deprecated not_isMulTorsionFree_of_isTorsion (since := "2025-04-23")]

theorem AddMonoid.IsTorsion.not_torsion_free {G : Type u_1} [AddGroup G] [hN : Nontrivial G] : IsTorsion G → ¬IsTorsionFree G

A nontrivial additive torsion group is not torsion-free.

@[deprecated not_isTorsion_of_isMulTorsionFree (since := "2025-04-23")]

theorem Monoid.IsTorsionFree.not_torsion {G : Type u_1} [Group G] [hN : Nontrivial G] : IsTorsionFree G → ¬IsTorsion G

A nontrivial torsion-free group is not torsion.

@[deprecated not_isTorsion_of_isMulTorsionFree (since := "2025-04-23")]

theorem AddMonoid.IsTorsionFree.not_torsion {G : Type u_1} [AddGroup G] [hN : Nontrivial G] : IsTorsionFree G → ¬IsTorsion G

A nontrivial torsion-free additive group is not torsion.

@[deprecated Subgroup.instIsMulTorsionFree (since := "2025-04-23")]

theorem Monoid.IsTorsionFree.subgroup {G : Type u_1} [Group G] (tG : IsTorsionFree G) (H : Subgroup G) : IsTorsionFree ↥H

Subgroups of torsion-free groups are torsion-free.

@[deprecated Subgroup.instIsMulTorsionFree (since := "2025-04-23")]

theorem AddMonoid.IsTorsionFree.addSubgroup {G : Type u_1} [AddGroup G] (tG : IsTorsionFree G) (H : AddSubgroup G) : IsTorsionFree ↥H

Subgroups of additive torsion-free groups are additively torsion-free.

@[deprecated Pi.instIsMulTorsionFree (since := "2025-04-23")]

theorem Monoid.IsTorsionFree.prod {η : Type u_3} {Gs : η → Type u_4} [(i : η) → Group (Gs i)] (tfGs : ∀ (i : η), IsTorsionFree (Gs i)) : IsTorsionFree ((i : η) → Gs i)

Direct products of torsion free groups are torsion free.

@[deprecated Pi.instIsMulTorsionFree (since := "2025-04-23")]

theorem AddMonoid.IsTorsionFree.prod {η : Type u_3} {Gs : η → Type u_4} [(i : η) → AddGroup (Gs i)] (tfGs : ∀ (i : η), IsTorsionFree (Gs i)) : IsTorsionFree ((i : η) → Gs i)

Direct products of additive torsion free groups are torsion free.

instance QuotientGroup.instIsMulTorsionFree (G : Type u_1) [CommGroup G] : IsMulTorsionFree (G ⧸ CommGroup.torsion G)

Quotienting a group by its torsion subgroup yields a torsion-free group.

instance QuotientAddGroup.instIsAddTorsionFree (G : Type u_1) [AddCommGroup G] : IsAddTorsionFree (G ⧸ AddCommGroup.torsion G)

Quotienting a group by its additive torsion subgroup yields an additive torsion-free group.

@[deprecated QuotientGroup.instIsMulTorsionFree (since := "2025-04-23")]

theorem Monoid.IsTorsionFree.quotient_torsion (G : Type u_1) [CommGroup G] : IsTorsionFree (G ⧸ CommGroup.torsion G)

Quotienting a group by its torsion subgroup yields a torsion free group.

@[deprecated QuotientGroup.instIsMulTorsionFree (since := "2025-04-23")]

theorem AddMonoid.IsTorsionFree.quotient_torsion (G : Type u_1) [AddCommGroup G] : IsTorsionFree (G ⧸ AddCommGroup.torsion G)

Quotienting a group by its additive torsion subgroup yields an additive torsion free group.

@[deprecated noZeroSMulDivisors_nat_iff_isAddTorsionFree (since := "2025-04-23")]

theorem AddMonoid.isTorsionFree_iff_noZeroSMulDivisors_nat {M : Type u_3} [AddMonoid M] : IsTorsionFree M ↔ NoZeroSMulDivisors ℕ M

@[deprecated noZeroSMulDivisors_int_iff_isAddTorsionFree (since := "2025-04-23")]

theorem AddMonoid.isTorsionFree_iff_noZeroSMulDivisors_int {G : Type u_1} [SubtractionMonoid G] : IsTorsionFree G ↔ NoZeroSMulDivisors ℤ G

@[deprecated IsAddTorsionFree.of_noZeroSMulDivisors_nat (since := "2025-04-23")]

theorem AddMonoid.IsTorsionFree.of_noZeroSMulDivisors {M : Type u_3} [AddMonoid M] [NoZeroSMulDivisors ℕ M] : IsTorsionFree M

@[deprecated IsAddTorsionFree.to_noZeroSMulDivisors_nat (since := "2025-04-23")]

theorem AddMonoid.IsTorsionFree.noZeroSMulDivisors_nat {M : Type u_3} [AddMonoid M] : IsTorsionFree M → NoZeroSMulDivisors ℕ M

Alias of the forward direction of AddMonoid.isTorsionFree_iff_noZeroSMulDivisors_nat.

@[deprecated IsAddTorsionFree.to_noZeroSMulDivisors_int (since := "2025-04-23")]

theorem AddMonoid.IsTorsionFree.noZeroSMulDivisors_int {G : Type u_1} [SubtractionMonoid G] : IsTorsionFree G → NoZeroSMulDivisors ℤ G

Alias of the forward direction of AddMonoid.isTorsionFree_iff_noZeroSMulDivisors_int.

instance instModuleQuotientAddSubgroupTorsion {R : Type u_3} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] : Module R (M ⧸ AddCommGroup.torsion M)

theorem neg_one_mem_torsion {M : Type u_3} [CommMonoid M] [HasDistribNeg M] : -1 ∈ CommMonoid.torsion M