# mathlib3documentation

group_theory.torsion

# 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_torsion a predicate asserting G is torsion, i.e. that all elements are of finite order.
• comm_group.torsion G, the torsion subgroup of an abelian group G
• comm_monoid.torsion G, the above stated for commutative monoids
• monoid.is_torsion_free, asserting no nontrivial elements have finite order in G
• add_monoid.is_torsion and add_monoid.is_torsion_free the 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
def monoid.is_torsion (G : Type u_1) [monoid G] :
Prop

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

Equations
Prop

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

Equations
@[simp]
(g : G),

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

@[simp]
theorem monoid.not_is_torsion_iff (G : Type u_1) [monoid G] :
(g : G),

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

Equations
noncomputable def is_torsion.group {G : Type u_1} [monoid G] (tG : monoid.is_torsion G) :

Torsion monoids are really groups.

Equations
theorem is_torsion.subgroup {G : Type u_1} [group G] (tG : monoid.is_torsion G) (H : subgroup G) :

Subgroups of torsion groups are torsion groups.

theorem is_torsion.of_surjective {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G →* H} (hf : function.surjective f) (tG : monoid.is_torsion G) :

The image of a surjective torsion group homomorphism is torsion.

theorem add_is_torsion.of_surjective {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G →+ H} (hf : function.surjective f) (tG : add_monoid.is_torsion G) :

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

theorem is_torsion.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.is_torsion H) (tN : monoid.is_torsion N) :

Torsion groups are closed under extensions.

theorem add_is_torsion.extension_closed {G : Type u_1} {H : Type u_2} [add_group G] {N : add_subgroup G} [add_group H] {f : G →+ H} (hN : N = f.ker) (tH : add_monoid.is_torsion H) (tN : add_monoid.is_torsion N) :

Additive torsion groups are closed under extensions.

theorem is_torsion.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.is_torsion N) :

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

theorem add_is_torsion.quotient_iff {G : Type u_1} {H : Type u_2} [add_group G] {N : add_subgroup G} [add_group H] {f : G →+ H} (hf : function.surjective f) (hN : N = f.ker) (tN : add_monoid.is_torsion N) :

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

theorem exponent_exists.is_torsion {G : Type u_1} [group G] (h : monoid.exponent_exists G) :

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.

theorem is_torsion.exponent_exists {G : Type u_1} [group G] (tG : monoid.is_torsion G) (bounded : (set.range (λ (g : G), order_of g)).finite) :

The group exponent exists for any bounded torsion group.

theorem is_torsion_of_finite {G : Type u_1} [group G] [finite G] :

Finite groups are torsion groups.

theorem add_monoid.is_torsion.module_of_torsion (R : Type u_3) (M : Type u_4) [semiring R] [ M] (tR : add_monoid.is_torsion R) :

theorem add_monoid.is_torsion.module_of_finite (R : Type u_3) (M : Type u_4) [ring R] [finite R] [ M] :

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

def comm_monoid.torsion (G : Type u_1) [comm_monoid G] :

The torsion submonoid of a commutative monoid.

(Note that by monoid.is_torsion.group torsion monoids are truthfully groups.)

Equations

The torsion submonoid of an additive commutative monoid.

Equations

Torsion submonoids are torsion.

def comm_monoid.primary_component (G : Type u_1) [comm_monoid G] (p : ) [hp : fact (nat.prime p)] :

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

Equations
def add_comm_monoid.primary_component (G : Type u_1) (p : ) [hp : fact (nat.prime p)] :

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

Equations
@[simp]
theorem comm_monoid.primary_component_coe (G : Type u_1) [comm_monoid G] (p : ) [hp : fact (nat.prime p)] :
= {g : G | (n : ), = p ^ n}
@[simp]
theorem add_comm_monoid.primary_component_coe (G : Type u_1) (p : ) [hp : fact (nat.prime p)] :
= {g : G | (n : ), = p ^ n}
theorem add_comm_monoid.primary_component.exists_order_of_eq_prime_nsmul {G : Type u_1} {p : } [hp : fact (nat.prime p)] (g : ) :
(n : ), = p ^ n

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

theorem comm_monoid.primary_component.exists_order_of_eq_prime_pow {G : Type u_1} [comm_monoid G] {p : } [hp : fact (nat.prime p)] (g : ) :
(n : ), = p ^ n

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

theorem add_comm_monoid.primary_component.disjoint {G : Type u_1} {p : } [hp : fact (nat.prime p)] {p' : } [hp' : fact (nat.prime p')] (hne : p p') :

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

theorem comm_monoid.primary_component.disjoint {G : Type u_1} [comm_monoid G] {p : } [hp : fact (nat.prime p)] {p' : } [hp' : fact (nat.prime p')] (hne : p p') :

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

@[simp]

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

@[simp]

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
@[simp]
def torsion.of_torsion (G : Type u_1) [comm_monoid G] :

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

Equations
@[simp]

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

Equations
def comm_group.torsion (G : Type u_1) [comm_group G] :

The torsion subgroup of an abelian group.

Equations
def add_comm_group.torsion (G : Type u_1)  :

The torsion subgroup of an additive abelian group.

Equations

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.

def comm_group.primary_component (G : Type u_1) [comm_group G] (p : ) [hp : fact (nat.prime p)] :

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

Equations
def add_comm_group.primary_component (G : Type u_1) (p : ) [hp : fact (nat.prime p)] :

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

Equations
@[simp]
theorem comm_group.primary_component_coe (G : Type u_1) [comm_group G] (p : ) [hp : fact (nat.prime p)] :
@[simp]
theorem add_comm_group.primary_component_coe (G : Type u_1) (p : ) [hp : fact (nat.prime p)] :
theorem comm_group.primary_component.is_p_group {G : Type u_1} [comm_group G] {p : } [hp : fact (nat.prime p)] :

The p-primary component is a p group.

def monoid.is_torsion_free (G : Type u_1) [monoid G] :
Prop

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

Equations
Prop

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

Equations
@[simp]
theorem monoid.not_is_torsion_free_iff (G : Type u_1) [monoid G] :
(g : G), g 1

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

@[simp]
(g : G), g 0

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

A nontrivial additive torsion group is not torsion-free.

theorem is_torsion.not_torsion_free {G : Type u_1} [group G] [hN : nontrivial G] :

A nontrivial torsion group is not torsion-free.

theorem is_torsion_free.not_torsion {G : Type u_1} [group G] [hN : nontrivial G] :

A nontrivial torsion-free group is not torsion.

A nontrivial torsion-free additive group is not torsion.

theorem is_torsion_free.subgroup {G : Type u_1} [group G] (tG : monoid.is_torsion_free G) (H : subgroup G) :

Subgroups of torsion-free groups are torsion-free.

theorem is_torsion_free.prod {η : Type u_1} {Gs : η Type u_2} [Π (i : η), group (Gs i)] (tfGs : (i : η), monoid.is_torsion_free (Gs i)) :
monoid.is_torsion_free (Π (i : η), Gs i)

Direct products of torsion free groups are torsion free.

theorem add_monoid.is_torsion_free.prod {η : Type u_1} {Gs : η Type u_2} [Π (i : η), add_group (Gs i)] (tfGs : (i : η), ) :

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.