def: order and torsion

src/Algebra/Group/Instances/Integers.lagda.md

@@ -8,9 +8,12 @@ open import Algebra.Group
 open import Cat.Functor.Adjoint
 
 open import Data.Int.Universal
+open import Data.Nat.Order
 open import Data.Int
+open import Data.Nat
 
 open is-group-hom
+open Lift
 ```
 -->
 
@@ -162,3 +165,82 @@ one generator.
 ℤ-free .Free-object.unique {G} {x} g comm =
   pow-unique G (x _) g (unext comm _)
 ```
+
+::: note
+While the notation $x^n$ for `pow`{.Agda} makes sense in
+multiplicative notation, we would instead write $n \cdot x$ in additive
+notation. In fact, we can show that $n \cdot x$ coincides with the
+multiplication $n \times x$ in the group of integers itself.
+
+```agda
+pow-ℤ : ∀ {ℓ} a b → Lift.lower (pow (ℤ {ℓ}) (lift a) b) ≡ a *ℤ b
+pow-ℤ {ℓ} a = ℤ.induction (sym (*ℤ-zeror a)) λ b →
+  lower (pow ℤ (lift a) b)        ≡ a *ℤ b      ≃⟨ ap (_+ℤ a) , equiv→cancellable (equiv≃ Lift-≃ Lift-≃ .fst (_ , Group-on.⋆-equivr (ℤ {ℓ} .snd) (lift a)) .snd) ⟩
+  lower (pow ℤ (lift a) b) +ℤ a   ≡ a *ℤ b +ℤ a ≃⟨ ∙-pre-equiv (ap lower (pow-sucr ℤ (lift a) b)) ⟩
+  lower (pow ℤ (lift a) (sucℤ b)) ≡ a *ℤ b +ℤ a ≃⟨ ∙-post-equiv (sym (*ℤ-sucr a b)) ⟩
+  lower (pow ℤ (lift a) (sucℤ b)) ≡ a *ℤ sucℤ b ≃∎
+```
+:::
+
+# Order of an element {defines="order-of-an-element"}
+
+<!--
+```agda
+module _ {ℓ} (G : Group ℓ) where
+  open Group-on (G .snd)
+```
+-->
+
+We define the **order** of an element $x : G$ of a group $G$ as the
+minimal *positive*^[Without this requirement, every element would
+trivially have order $0$!] integer $n$ such that $x^n = 1$, if it exists.
+
+In particular, if $x^n = 1$, then we have that the order of $x$ divides
+$n$. We define this notion first in the code, then use it to define the
+order of $x$.
+
+```agda
+  order-divides : ⌞ G ⌟ → Nat → Type ℓ
+  order-divides x n = pow G x (pos n) ≡ unit
+
+  has-finite-order : ⌞ G ⌟ → Type ℓ
+  has-finite-order x = minimal-solution λ n →
+    Positive n × order-divides x n
+
+  order : (x : ⌞ G ⌟) → has-finite-order x → Nat
+  order x (n , _) = n
+```
+
+::: {.definition #torsion}
+An element $x$ with finite order is also called a **torsion element**.
+A group all of whose elements are torsion is called a **torsion group**,
+while a group whose only torsion element is the unit is called
+**torsion-free**.
+:::
+
+```agda
+  is-torsion-group : Type ℓ
+  is-torsion-group = ∀ g → has-finite-order g
+
+  is-torsion-free : Type ℓ
+  is-torsion-free = ∀ g → has-finite-order g → g ≡ unit
+```
+
+::: note
+Our definition of torsion groups requires being able to compute
+the order of every element of the group. There is a weaker definition
+that only requires every element $x$ to have *some* $n$ such that
+$x^n = 1$; the two definitions are equivalent if the group is
+[[discrete]], since [[$\NN$ is well-ordered|N is well-ordered]].
+:::
+
+We quickly note that $\ZZ$ is torsion-free, since multiplication by
+a nonzero integer is injective.
+
+```agda
+ℤ-torsion-free : ∀ {ℓ} → is-torsion-free (ℤ {ℓ})
+ℤ-torsion-free (lift n) (k , (k>0 , nk≡0) , _) = ap lift $
+  *ℤ-injectiver (pos k) n 0
+    (λ p → <-not-equal k>0 (pos-injective (sym p)))
+    (sym (pow-ℤ n (pos k)) ∙ ap Lift.lower nk≡0)
+```

src/Data/Int/Properties.lagda.md

@@ -319,6 +319,10 @@ no further comments.
   assign-+ {neg} (suc x) zero = ap negsuc (+-zeror _)
   assign-+ {neg} (suc x) (suc y) = ap negsuc (+-sucr _ _)
 
+  possuc≠assign-neg : ∀ {x y} → possuc x ≠ assign neg y
+  possuc≠assign-neg {x} {zero} p = suc≠zero (pos-injective p)
+  possuc≠assign-neg {x} {suc y} p = pos≠negsuc p
+
   *ℤ-onel : ∀ x → 1 *ℤ x ≡ x
   *ℤ-onel (pos x)    = ap (assign pos) (+-zeror x) ∙ assign-pos x
   *ℤ-onel (negsuc x) = ap negsuc (+-zeror x)
@@ -451,4 +455,17 @@ no further comments.
   *ℤ-injectiver-possuc k (negsuc x) (pos y) p = absurd (negsuc≠pos (p ∙ assign-pos (y * suc k)))
   *ℤ-injectiver-possuc k (negsuc x) (negsuc y) p =
     ap (assign neg) (*-suc-inj k (suc x) (suc y) (ap suc (negsuc-injective p)))
+
+  *ℤ-injectiver-negsuc : ∀ k x y → x *ℤ negsuc k ≡ y *ℤ negsuc k → x ≡ y
+  *ℤ-injectiver-negsuc k (pos x) (pos y) p = ap pos (*-suc-inj k x y (pos-injective (negℤ-injective _ _ (sym (assign-neg _) ·· p ·· assign-neg _))))
+  *ℤ-injectiver-negsuc k posz (negsuc y) p = absurd (zero≠suc (pos-injective p))
+  *ℤ-injectiver-negsuc k (possuc x) (negsuc y) p = absurd (negsuc≠pos p)
+  *ℤ-injectiver-negsuc k (negsuc x) posz p = absurd (suc≠zero (pos-injective p))
+  *ℤ-injectiver-negsuc k (negsuc x) (possuc y) p = absurd (pos≠negsuc p)
+  *ℤ-injectiver-negsuc k (negsuc x) (negsuc y) p = ap (assign neg) (*-suc-inj k (suc x) (suc y) (ap suc (suc-inj (pos-injective p))))
+
+  *ℤ-injectiver : ∀ k x y → k ≠ 0 → x *ℤ k ≡ y *ℤ k → x ≡ y
+  *ℤ-injectiver posz x y k≠0 p = absurd (k≠0 refl)
+  *ℤ-injectiver (possuc k) x y k≠0 p = *ℤ-injectiver-possuc k x y p
+  *ℤ-injectiver (negsuc k) x y k≠0 p = *ℤ-injectiver-negsuc k x y p
 ```

src/Data/Nat/Order.lagda.md

@@ -235,7 +235,7 @@ that here (it is a more general fact about
   from {suc x} {suc y} p = s≤s (from (suc-inj p))
 ```
 
-## Well-ordering
+## Well-ordering {defines="N-is-well-ordered"}
 
 In classical mathematics, the well-ordering principle states that every
 nonempty subset of the natural numbers has a minimal element. In
@@ -256,45 +256,47 @@ implicitly appealing to path induction to reduce this to the case where
 $p, q : P(n)$] automatically have that $p = q$.
 
 ```agda
-module _ {ℓ} {P : Nat → Prop ℓ} where
-  private
-    minimal-solution : ∀ {ℓ} (P : Nat → Type ℓ) → Type _
-    minimal-solution P = Σ[ n ∈ Nat ] (P n × (∀ k → P k → n ≤ k))
-
-    minimal-solution-unique : is-prop (minimal-solution λ x → ∣ P x ∣)
-    minimal-solution-unique (n , pn , n-min) (k , pk , k-min) =
-      Σ-prop-path! (≤-antisym (n-min _ pk) (k-min _ pn))
+minimal-solution : ∀ {ℓ} (P : Nat → Type ℓ) → Type _
+minimal-solution P = Σ[ n ∈ Nat ] (P n × (∀ k → P k → n ≤ k))
+
+minimal-solution-unique
+  : ∀ {ℓ} {P : Nat → Prop ℓ}
+  → is-prop (minimal-solution λ x → ∣ P x ∣)
+minimal-solution-unique (n , pn , n-min) (k , pk , k-min) =
+  Σ-prop-path! (≤-antisym (n-min _ pk) (k-min _ pn))
 ```
 
 The step of the code that actually finds a minimal solution does not
 need $P$ to be a predicate: we only need that for actually searching for
 an inhabited subset.
 
 ```agda
-    min-suc
-      : ∀ {P : Nat → Type ℓ} → ∀ n → ¬ P 0
-      → (∀ k → P (suc k) → n ≤ k)
-      → ∀ k → P k → suc n ≤ k
-    min-suc n ¬p0 nmins zero pk           = absurd (¬p0 pk)
-    min-suc zero ¬p0 nmins (suc k) psk    = s≤s 0≤x
-    min-suc (suc n) ¬p0 nmins (suc k) psk = s≤s (nmins k psk)
-
-  ℕ-minimal-solution
-    : ∀ (P : Nat → Type ℓ)
-    → (∀ n → Dec (P n))
-    → (n : Nat) → P n
-    → minimal-solution P
-  ℕ-minimal-solution P decp zero p = 0 , p , λ k _ → 0≤x
-  ℕ-minimal-solution P decp (suc n) p = case decp zero of λ where
-    (yes p0) → 0 , p0 , λ k _ → 0≤x
-    (no ¬p0) →
-      let (a , pa , x) = ℕ-minimal-solution (P ∘ suc) (decp ∘ suc) n p
-       in suc a , pa , min-suc {P} a ¬p0 x
-
-  ℕ-well-ordered
-    : (∀ n → Dec ∣ P n ∣)
-    → ∃[ n ∈ Nat ] ∣ P n ∣
-    → Σ[ n ∈ Nat ] (∣ P n ∣ × (∀ k → ∣ P k ∣ → n ≤ k))
-  ℕ-well-ordered P-dec wit = ∥-∥-rec minimal-solution-unique
-    (λ { (n , p) → ℕ-minimal-solution _ P-dec n p }) wit
+min-suc
+  : ∀ {ℓ} {P : Nat → Type ℓ}
+  → ∀ n → ¬ P 0
+  → (∀ k → P (suc k) → n ≤ k)
+  → ∀ k → P k → suc n ≤ k
+min-suc n ¬p0 nmins zero pk           = absurd (¬p0 pk)
+min-suc zero ¬p0 nmins (suc k) psk    = s≤s 0≤x
+min-suc (suc n) ¬p0 nmins (suc k) psk = s≤s (nmins k psk)
+
+ℕ-minimal-solution
+  : ∀ {ℓ} (P : Nat → Type ℓ)
+  → (∀ n → Dec (P n))
+  → (n : Nat) → P n
+  → minimal-solution P
+ℕ-minimal-solution P decp zero p = 0 , p , λ k _ → 0≤x
+ℕ-minimal-solution P decp (suc n) p = case decp zero of λ where
+  (yes p0) → 0 , p0 , λ k _ → 0≤x
+  (no ¬p0) →
+    let (a , pa , x) = ℕ-minimal-solution (P ∘ suc) (decp ∘ suc) n p
+      in suc a , pa , min-suc {P = P} a ¬p0 x
+
+ℕ-well-ordered
+  : ∀ {ℓ} {P : Nat → Prop ℓ}
+  → (∀ n → Dec ∣ P n ∣)
+  → ∃[ n ∈ Nat ] ∣ P n ∣
+  → Σ[ n ∈ Nat ] (∣ P n ∣ × (∀ k → ∣ P k ∣ → n ≤ k))
+ℕ-well-ordered {P = P} P-dec wit = ∥-∥-rec (minimal-solution-unique {P = P})
+  (λ { (n , p) → ℕ-minimal-solution _ P-dec n p }) wit
 ```