Torsion-free groups

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-06.
Last modified on 2024-04-25.

module group-theory.torsion-free-groups where
open import
open import elementary-number-theory.nonzero-integers

open import foundation.action-on-identifications-functions
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.existential-quantification
open import foundation.fundamental-theorem-of-identity-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.propositions
open import foundation.sets
open import foundation.singleton-subtypes
open import foundation.standard-pullbacks
open import foundation.universe-levels

open import group-theory.groups
open import group-theory.integer-powers-of-elements-groups
open import group-theory.orders-of-elements-groups
open import group-theory.subgroups
open import group-theory.torsion-elements-groups


A torsion-free group is a group G in which any element of finite order is the identity element. In other words, torsion-free groups are groups in which the condition

  ∀ (k : nonzero-ℤ), xᵏ = 1 → x = 1

holds for all elements x : G. This condition can be formulated in several equivalent ways:

  1. ∀ (k : nonzero-ℤ), xᵏ = 1 → x = 1.
  2. The subset of G of torsion elements is a singleton subtype.
  3. The map p in the pullback square
        · ---------> Prop
        | ⌟            |
       p|              | P ↦ {k : ℤ ∣ (k = 0) ∨ P}
        ∨              ∨
        G -------> Subgroup ℤ
    is an equivalence.


The predicate of being a torsion-free group

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

  is-torsion-free-prop-Group : Prop l1
  is-torsion-free-prop-Group =
      ( type-Group G)
      ( λ x 
          ( nonzero-ℤ)
          ( λ k 
              ( integer-power-Group G (int-nonzero-ℤ k) x  unit-Group G)
              ( Id-Prop (set-Group G) x (unit-Group G))))

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

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

The predicate that a group has a unique torsion element

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

  has-unique-torsion-element-prop-Group : Prop l1
  has-unique-torsion-element-prop-Group =
    is-singleton-subtype-Prop (is-torsion-element-prop-Group G)

  has-unique-torsion-element-Group : UU l1
  has-unique-torsion-element-Group =
    is-singleton-subtype (is-torsion-element-prop-Group G)

  is-prop-has-unique-torsion-element-Group :
    is-prop has-unique-torsion-element-Group
  is-prop-has-unique-torsion-element-Group =
    is-prop-is-singleton-subtype (is-torsion-element-prop-Group G)

The predicate that the first projection of the pullback of Prop lzero → Subgroup ℤ along order : G → Subgroup ℤ is an equivalence

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

  is-equiv-vertical-map-standard-pullback-subgroup-prop-prop-Group :
    Prop (lsuc l1)
  is-equiv-vertical-map-standard-pullback-subgroup-prop-prop-Group =
      ( vertical-map-standard-pullback
        { f = subgroup-order-element-Group G}
        { g = subgroup-Prop ℤ-Group})

  is-equiv-first-projection-pullback-subgroup-prop-Group : UU (lsuc l1)
  is-equiv-first-projection-pullback-subgroup-prop-Group =
    type-Prop is-equiv-vertical-map-standard-pullback-subgroup-prop-prop-Group

  is-prop-is-equiv-first-projection-pullback-subgroup-prop-Group :
    is-prop is-equiv-first-projection-pullback-subgroup-prop-Group
  is-prop-is-equiv-first-projection-pullback-subgroup-prop-Group =
      ( is-equiv-vertical-map-standard-pullback-subgroup-prop-prop-Group)


The two definitions of torsion-free groups are equivalent

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

  is-torsion-free-has-unique-torsion-element-Group :
    has-unique-torsion-element-Group G  is-torsion-free-Group G
  is-torsion-free-has-unique-torsion-element-Group H x k p =
    ap pr1 (eq-is-contr H {x , intro-exists k p} {unit-torsion-element-Group G})

    has-unique-torsion-element-is-torsion-free-Group :
      is-torsion-free-Group G  has-unique-torsion-element-Group G
    has-unique-torsion-element-is-torsion-free-Group H =
        ( λ where x refl  is-torsion-element-unit-Group G)
        ( λ x 
            ( is-set-type-Group G (unit-Group G) x)
            ( is-prop-is-torsion-element-Group G x)
            ( elim-exists
              ( Id-Prop (set-Group G) (unit-Group G) x)
              ( λ k p  inv (H x k p))))

Recent changes