Torsion-free groups (#813)

This PR adds the notion of torsion element of a group and and the notion
of torsion-free group to the library. Furthermore, it adds a short
discussion on the notion of elements of finite order, which looks too
strong from a constructive point of view.

---------

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

src/elementary-number-theory.lagda.md

@@ -88,6 +88,7 @@ open import elementary-number-theory.multiplicative-units-integers public
 open import elementary-number-theory.multiplicative-units-modular-arithmetic public
 open import elementary-number-theory.multiset-coefficients public
 open import elementary-number-theory.natural-numbers public
+open import elementary-number-theory.nonzero-integers public
 open import elementary-number-theory.nonzero-natural-numbers public
 open import elementary-number-theory.ordinal-induction-natural-numbers public
 open import elementary-number-theory.parity-natural-numbers public

src/elementary-number-theory/divisibility-integers.lagda.md

@@ -14,6 +14,7 @@ open import elementary-number-theory.equality-integers
 open import elementary-number-theory.integers
 open import elementary-number-theory.multiplication-integers
 open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.nonzero-integers
 
 open import foundation.action-on-identifications-functions
 open import foundation.binary-relations

src/elementary-number-theory/integer-fractions.lagda.md

@@ -10,6 +10,7 @@ module elementary-number-theory.integer-fractions where
 open import elementary-number-theory.greatest-common-divisor-integers
 open import elementary-number-theory.integers
 open import elementary-number-theory.multiplication-integers
+open import elementary-number-theory.nonzero-integers
 
 open import foundation.action-on-identifications-functions
 open import foundation.binary-relations

src/elementary-number-theory/integers.lagda.md

@@ -66,9 +66,6 @@ zero-ℤ = inr (inl star)
 
 is-zero-ℤ : ℤ → UU lzero
 is-zero-ℤ x = (x ＝ zero-ℤ)
-
-is-nonzero-ℤ : ℤ → UU lzero
-is-nonzero-ℤ k = ¬ (is-zero-ℤ k)
 ```
 
 ### Inclusion of the positive integers
@@ -94,9 +91,6 @@ int-ℕ (succ-ℕ n) = in-pos n
 is-injective-int-ℕ : is-injective int-ℕ
 is-injective-int-ℕ {zero-ℕ} {zero-ℕ} refl = refl
 is-injective-int-ℕ {succ-ℕ x} {succ-ℕ y} refl = refl
-
-is-nonzero-int-ℕ : (n : ℕ) → is-nonzero-ℕ n → is-nonzero-ℤ (int-ℕ n)
-is-nonzero-int-ℕ zero-ℕ H p = H refl
 ```
 
 ### Induction principle on the type of integers
@@ -334,9 +328,6 @@ is-positive-int-positive-ℤ = pr2
 is-nonnegative-is-positive-ℤ : {x : ℤ} → is-positive-ℤ x → is-nonnegative-ℤ x
 is-nonnegative-is-positive-ℤ {inr (inr x)} H = H
 
-is-nonzero-is-positive-ℤ : (x : ℤ) → is-positive-ℤ x → is-nonzero-ℤ x
-is-nonzero-is-positive-ℤ (inr (inr x)) H ()
-
 is-positive-eq-ℤ : {x y : ℤ} → x ＝ y → is-positive-ℤ x → is-positive-ℤ y
 is-positive-eq-ℤ {x} refl = id
 

src/elementary-number-theory/multiplication-integers.lagda.md

@@ -15,6 +15,7 @@ open import elementary-number-theory.inequality-integers
 open import elementary-number-theory.integers
 open import elementary-number-theory.multiplication-natural-numbers
 open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.nonzero-integers
 
 open import foundation.action-on-identifications-binary-functions
 open import foundation.action-on-identifications-functions

src/elementary-number-theory/nonzero-integers.lagda.md

@@ -0,0 +1,92 @@
+# Nonzero integers
+
+```agda
+module elementary-number-theory.nonzero-integers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.integers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.negation
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+An [integer](elementary-number-theory.integers.md) `k` is said to be **nonzero**
+if the [proposition](foundation.propositions.md)
+
+```text
+  ¬ (k ＝ 0)
+```
+
+holds.
+
+## Definition
+
+### The predicate of being a nonzero integer
+
+```agda
+is-nonzero-prop-ℤ : ℤ → Prop lzero
+is-nonzero-prop-ℤ k = neg-Prop' (k ＝ zero-ℤ)
+
+is-nonzero-ℤ : ℤ → UU lzero
+is-nonzero-ℤ k = type-Prop (is-nonzero-prop-ℤ k)
+
+is-prop-is-nonzero-ℤ : (k : ℤ) → is-prop (is-nonzero-ℤ k)
+is-prop-is-nonzero-ℤ k = is-prop-type-Prop (is-nonzero-prop-ℤ k)
+```
+
+### The nonzero integers
+
+```agda
+nonzero-ℤ : UU lzero
+nonzero-ℤ = type-subtype is-nonzero-prop-ℤ
+
+module _
+  (k : nonzero-ℤ)
+  where
+
+  int-nonzero-ℤ : ℤ
+  int-nonzero-ℤ = pr1 k
+
+  is-nonzero-nonzero-ℤ : is-nonzero-ℤ int-nonzero-ℤ
+  is-nonzero-nonzero-ℤ = pr2 k
+```
+
+### The nonzero integer `1`
+
+```agda
+is-nonzero-one-ℤ : is-nonzero-ℤ one-ℤ
+is-nonzero-one-ℤ ()
+
+one-nonzero-ℤ : nonzero-ℤ
+pr1 one-nonzero-ℤ = one-ℤ
+pr2 one-nonzero-ℤ = is-nonzero-one-ℤ
+```
+
+## Properties
+
+### The inclusion of natural numbers into integers maps nonzero natural numbers to nonzero integers
+
+```agda
+is-nonzero-int-ℕ : (n : ℕ) → is-nonzero-ℕ n → is-nonzero-ℤ (int-ℕ n)
+is-nonzero-int-ℕ zero-ℕ H p = H refl
+```
+
+### Positive integers are nonzero
+
+```agda
+is-nonzero-is-positive-ℤ : (x : ℤ) → is-positive-ℤ x → is-nonzero-ℤ x
+is-nonzero-is-positive-ℤ (inr (inr x)) H ()
+```

src/elementary-number-theory/nonzero-natural-numbers.lagda.md

@@ -18,6 +18,15 @@ open import foundation.universe-levels
 
 ## Idea
 
+A [natural number](elementary-number-theory.natural-numbers.md) `n` is said to
+be **nonzero** if the [proposition](foundation.propositions.md)
+
+```text
+  ¬ (n ＝ 0)
+```
+
+holds. This condition was already defined in the file
+[`elementary-number-theory.natural-numbers`](elementary-number-theory.natural-numbers.md).
 The type of nonzero natural numbers consists of natural numbers equipped with a
 proof that they are nonzero.
 
@@ -34,20 +43,34 @@ nat-nonzero-ℕ = pr1
 
 is-nonzero-nat-nonzero-ℕ : (n : nonzero-ℕ) → is-nonzero-ℕ (nat-nonzero-ℕ n)
 is-nonzero-nat-nonzero-ℕ = pr2
+```
 
+### The nonzero natural number `1`
+
+```agda
 one-nonzero-ℕ : nonzero-ℕ
 pr1 one-nonzero-ℕ = 1
 pr2 one-nonzero-ℕ = is-nonzero-one-ℕ
+```
 
+### The successor function on the nonzero natural numbers
+
+```agda
 succ-nonzero-ℕ : nonzero-ℕ → nonzero-ℕ
 pr1 (succ-nonzero-ℕ (pair x _)) = succ-ℕ x
 pr2 (succ-nonzero-ℕ (pair x _)) = is-nonzero-succ-ℕ x
+```
 
+### The successor function from the natural numbers to the nonzero natural numbers
+
+```agda
 succ-nonzero-ℕ' : ℕ → nonzero-ℕ
 pr1 (succ-nonzero-ℕ' n) = succ-ℕ n
 pr2 (succ-nonzero-ℕ' n) = is-nonzero-succ-ℕ n
 ```
 
+### The quotient of a nonzero natural number by a divisor
+
 ```agda
 quotient-div-nonzero-ℕ :
   (d : ℕ) (x : nonzero-ℕ) (H : div-ℕ d (pr1 x)) → nonzero-ℕ

src/group-theory.lagda.md

@@ -51,6 +51,7 @@ open import group-theory.dependent-products-semigroups public
 open import group-theory.dihedral-group-construction public
 open import group-theory.dihedral-groups public
 open import group-theory.e8-lattice public
+open import group-theory.elements-of-finite-order-groups public
 open import group-theory.embeddings-abelian-groups public
 open import group-theory.embeddings-groups public
 open import group-theory.endomorphism-rings-abelian-groups public
@@ -164,6 +165,8 @@ open import group-theory.substitution-functor-group-actions public
 open import group-theory.surjective-group-homomorphisms public
 open import group-theory.symmetric-concrete-groups public
 open import group-theory.symmetric-groups public
+open import group-theory.torsion-elements-groups public
+open import group-theory.torsion-free-groups public
 open import group-theory.torsors public
 open import group-theory.transitive-concrete-group-actions public
 open import group-theory.transitive-group-actions public

src/group-theory/elements-of-finite-order-groups.lagda.md

@@ -0,0 +1,60 @@
+# Elements of finite order
+
+```agda
+module group-theory.elements-of-finite-order-groups where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.group-of-integers
+open import elementary-number-theory.nonzero-integers
+
+open import foundation.existential-quantification
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import group-theory.groups
+open import group-theory.orders-of-elements-groups
+open import group-theory.subgroups
+open import group-theory.subgroups-generated-by-elements-groups
+```
+
+</details>
+
+## Idea
+
+An element `x` of a [group](group-theory.groups.md) `G` is said to be of
+**finite order** if the [subgroup](group-theory.subgroups.md) `order x` of
+[`ℤ`](elementary-number-theory.group-of-integers.md) is
+[generated by](group-theory.subgroups-generated-by-elements-groups.md) a
+[nonzero integer](elementary-number-theory.nonzero-integers.md).
+
+Note that the condition of being of finite order is slightly stronger than the
+condition of being a [torsion element](group-theory.torsion-elements-groups.md).
+The latter condition merely asserts that there
+[exists](foundation.existential-quantification.md) a nonzero integer in the
+subgroup `order x` of `ℤ`.
+
+## Definitions
+
+### The predicate of being an element of finite order
+
+```agda
+module _
+  {l1 : Level} (G : Group l1) (x : type-Group G)
+  where
+
+  has-finite-order-element-prop-Group : Prop l1
+  has-finite-order-element-prop-Group =
+    ∃-Prop
+      ( nonzero-ℤ)
+      ( λ k →
+        has-same-elements-Subgroup ℤ-Group
+          ( subgroup-element-Group ℤ-Group (int-nonzero-ℤ k))
+          ( subgroup-order-element-Group G x))
+```
+
+## See also
+
+- [Torsion elements](group-theory.torsion-elements-groups.md) of groups.

src/group-theory/subgroups.lagda.md

@@ -376,6 +376,13 @@ module _
   {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G)
   where
 
+  has-same-elements-prop-Subgroup :
+    {l3 : Level} → Subgroup l3 G → Prop (l1 ⊔ l2 ⊔ l3)
+  has-same-elements-prop-Subgroup K =
+    has-same-elements-subtype-Prop
+      ( subset-Subgroup G H)
+      ( subset-Subgroup G K)
+
   has-same-elements-Subgroup :
     {l3 : Level} → Subgroup l3 G → UU (l1 ⊔ l2 ⊔ l3)
   has-same-elements-Subgroup K =