# Torsion elements of groups

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-06.

module group-theory.torsion-elements-groups where

Imports
open import elementary-number-theory.integers
open import elementary-number-theory.nonzero-integers

open import foundation.dependent-pair-types
open import foundation.existential-quantification
open import foundation.identity-types
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels

open import group-theory.groups
open import group-theory.integer-powers-of-elements-groups


## Idea

An element x of a group G is said to be a torsion element if

  ∃ (k : nonzero-ℤ), xᵏ ＝ 1.


Note that the condition of being a torsion element is slightly weaker than the condition of being of finite order. The condition of being a torsion element holds if and only if the subgroup order x of ℤ contains a nonzero integer, while the condition of being of finite order states that the subgroup order x is generated by k for some nonzero integer k.

## Definition

### The predicate of being a torsion element

module _
{l1 : Level} (G : Group l1) (x : type-Group G)
where

is-torsion-element-prop-Group : Prop l1
is-torsion-element-prop-Group =
exists-structure-Prop
( nonzero-ℤ)
( λ k → integer-power-Group G (int-nonzero-ℤ k) x ＝ unit-Group G)

is-torsion-element-Group : UU l1
is-torsion-element-Group = type-Prop is-torsion-element-prop-Group

is-prop-is-torsion-element-Group : is-prop is-torsion-element-Group
is-prop-is-torsion-element-Group =
is-prop-type-Prop is-torsion-element-prop-Group


### The type of torsion elements of a group

module _
{l1 : Level} (G : Group l1)
where

torsion-element-Group : UU l1
torsion-element-Group = type-subtype (is-torsion-element-prop-Group G)


## Properties

### The unit element is a torsion element

module _
{l1 : Level} (G : Group l1)
where

is-torsion-element-unit-Group : is-torsion-element-Group G (unit-Group G)
is-torsion-element-unit-Group =
intro-exists
( one-nonzero-ℤ)
( integer-power-unit-Group G one-ℤ)

unit-torsion-element-Group : torsion-element-Group G
pr1 unit-torsion-element-Group = unit-Group G
pr2 unit-torsion-element-Group = is-torsion-element-unit-Group