mathlib documentation

group_theory.torsion

Torsion groups #

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

Main definitions #

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 #

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
def add_monoid.is_torsion (G : Type u_1) [add_monoid G] :
Prop

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

Equations
@[simp]

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] :

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

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.

Subgroups of additive torsion groups are additive 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.

If a group exponent exists, the group is torsion.

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

theorem is_add_torsion.exponent_exists {G : Type u_1} [add_group G] (tG : add_monoid.is_torsion G) (bounded : (set.range (λ (g : G), add_order_of g)).finite) :

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 is_add_torsion_of_finite {G : Type u_1} [add_group G] [finite G] :

Finite additive groups are additive torsion groups.

A module whose scalars are additively torsion is additively torsion.

theorem add_monoid.is_torsion.module_of_finite (R : Type u_3) (M : Type u_4) [add_comm_monoid M] [ring R] [finite R] [module 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

Additive torsion submonoids are additively torsion.

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) [add_comm_monoid G] (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)] :
(comm_monoid.primary_component G p) = {g : G | ∃ (n : ), order_of g = p ^ n}
@[simp]
theorem add_comm_monoid.primary_component_coe (G : Type u_1) [add_comm_monoid G] (p : ) [hp : fact (nat.prime p)] :
(add_comm_monoid.primary_component G p) = {g : G | ∃ (n : ), add_order_of g = 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 : (comm_monoid.primary_component G p)) :
∃ (n : ), order_of g = p ^ 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.

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]

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) [add_comm_group G] :

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) [add_comm_group G] (p : ) [hp : fact (nat.prime p)] :

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

Equations

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
def add_monoid.is_torsion_free (G : Type u_1) [add_monoid G] :
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] :

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

@[simp]

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.

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 : η), add_monoid.is_torsion_free (Gs i)) :
add_monoid.is_torsion_free (Π (i : η), Gs 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.