Torsion groups #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines torsion groups, i.e. groups where all elements have finite order.
Main definitions #
monoid.is_torsiona predicate assertingGis torsion, i.e. that all elements are of finite order.comm_group.torsion G, the torsion subgroup of an abelian groupGcomm_monoid.torsion G, the above stated for commutative monoidsmonoid.is_torsion_free, asserting no nontrivial elements have finite order inGadd_monoid.is_torsionandadd_monoid.is_torsion_freethe additive versions of the above
Implementation #
All torsion monoids are really groups (which is proven here as monoid.is_torsion.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
A predicate on a monoid saying that all elements are of finite order.
Equations
- monoid.is_torsion G = ∀ (g : G), is_of_fin_order g
A predicate on an additive monoid saying that all elements are of finite order.
Equations
- add_monoid.is_torsion G = ∀ (g : G), is_of_fin_add_order g
An additive monoid is not a torsion monoid if it has an element of infinite order.
A monoid is not a torsion monoid if it has an element of infinite order.
Torsion additive monoids are really additive groups
Equations
- is_torsion.add_group tG = {add := add_monoid.add _inst_1, add_assoc := _, zero := add_monoid.zero _inst_1, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, neg := λ (g : G), (add_order_of g - 1) • g, sub := sub_neg_monoid.sub._default add_monoid.add add_monoid.add_assoc add_monoid.zero add_monoid.zero_add add_monoid.add_zero add_monoid.nsmul add_monoid.nsmul_zero' add_monoid.nsmul_succ' (λ (g : G), (add_order_of g - 1) • g), sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul._default add_monoid.add add_monoid.add_assoc add_monoid.zero add_monoid.zero_add add_monoid.add_zero add_monoid.nsmul add_monoid.nsmul_zero' add_monoid.nsmul_succ' (λ (g : G), (add_order_of g - 1) • g), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _}
Torsion monoids are really groups.
Equations
- is_torsion.group tG = {mul := monoid.mul _inst_1, mul_assoc := _, one := monoid.one _inst_1, one_mul := _, mul_one := _, npow := monoid.npow _inst_1, npow_zero' := _, npow_succ' := _, inv := λ (g : G), g ^ (order_of g - 1), div := div_inv_monoid.div._default monoid.mul monoid.mul_assoc monoid.one monoid.one_mul monoid.mul_one monoid.npow monoid.npow_zero' monoid.npow_succ' (λ (g : G), g ^ (order_of g - 1)), div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default monoid.mul monoid.mul_assoc monoid.one monoid.one_mul monoid.mul_one monoid.npow monoid.npow_zero' monoid.npow_succ' (λ (g : G), g ^ (order_of g - 1)), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
Subgroups of torsion groups are torsion groups.
Subgroups of additive torsion groups are additive torsion groups.
The image of a surjective torsion group homomorphism is torsion.
The image of a surjective additive torsion group homomorphism is torsion.
Torsion groups are closed under extensions.
Additive torsion groups are closed under extensions.
The image of a quotient is torsion iff the group is torsion.
The image of a quotient is additively torsion iff the group is torsion.
If a group exponent exists, the group is torsion.
If a group exponent exists, the group is additively torsion.
The group exponent exists for any bounded additive torsion group.
The group exponent exists for any bounded torsion group.
Finite groups are torsion groups.
Finite additive groups are additive torsion groups.
A module whose scalars are additively torsion is additively torsion.
A module with a finite ring of scalars is additively torsion.
The torsion submonoid of a commutative monoid.
(Note that by monoid.is_torsion.group torsion monoids are truthfully groups.)
Equations
- comm_monoid.torsion G = {carrier := {x : G | is_of_fin_order x}, mul_mem' := _, one_mem' := _}
The torsion submonoid of an additive commutative monoid.
Equations
- add_comm_monoid.add_torsion G = {carrier := {x : G | is_of_fin_add_order x}, add_mem' := _, zero_mem' := _}
Additive torsion submonoids are additively torsion.
Torsion submonoids are torsion.
The p-primary component is the submonoid of elements with order prime-power of p.
The p-primary component is the submonoid of elements with additive order prime-power of p.
Elements of the p-primary component have additive order p^n for some n
Elements of the p-primary component have order p^n for some n.
The p- and q-primary components are disjoint for p ≠ q.
The p- and q-primary components are disjoint for p ≠ q.
The additive torsion submonoid of an additive torsion monoid is ⊤.
The torsion submonoid of a torsion monoid is ⊤.
An additive torsion monoid is isomorphic to its torsion submonoid.
Equations
A torsion monoid is isomorphic to its torsion submonoid.
Equations
Torsion submonoids of a torsion submonoid are isomorphic to the submonoid.
Additive torsion submonoids of an additive torsion submonoid are isomorphic to the submonoid.
The torsion subgroup of an abelian group.
Equations
- comm_group.torsion G = {carrier := (comm_monoid.torsion G).carrier, mul_mem' := _, one_mem' := _, inv_mem' := _}
The torsion subgroup of an additive abelian group.
Equations
- add_comm_group.torsion G = {carrier := (add_comm_monoid.add_torsion G).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}
The torsion submonoid of an abelian group equals the torsion subgroup as a submonoid.
The additive torsion submonoid of an abelian group equals the torsion subgroup as a submonoid.
The p-primary component is the subgroup of elements with order prime-power of p.
Equations
- comm_group.primary_component G p = {carrier := (comm_monoid.primary_component G p).carrier, mul_mem' := _, one_mem' := _, inv_mem' := _}
The p-primary component is the subgroup of elements with additive order prime-power of p.
Equations
- add_comm_group.primary_component G p = {carrier := (add_comm_monoid.primary_component G p).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}
The p-primary component is a p group.
A predicate on a monoid saying that only 1 is of finite order.
Equations
- monoid.is_torsion_free G = ∀ (g : G), g ≠ 1 → ¬is_of_fin_order g
A predicate on an additive monoid saying that only 0 is of finite order.
Equations
- add_monoid.is_torsion_free G = ∀ (g : G), g ≠ 0 → ¬is_of_fin_add_order g
A nontrivial monoid is not torsion-free if any nontrivial element has finite order.
An additive monoid is not torsion free if any nontrivial element has finite order.
A nontrivial additive torsion group is not torsion-free.
A nontrivial torsion group is not torsion-free.
A nontrivial torsion-free group is not torsion.
A nontrivial torsion-free additive group is not torsion.
Subgroups of additive torsion-free groups are additively torsion-free.
Subgroups of torsion-free groups are torsion-free.
Direct products of torsion free groups are torsion free.
Direct products of additive torsion free groups are torsion free.
Quotienting a group by its additive torsion subgroup yields an additive torsion free group.
Quotienting a group by its torsion subgroup yields a torsion free group.