From ee0a8b2cae797a0872b731703de0a7332d932eec Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Na=C3=AFm=20Favier?= Date: Mon, 26 Aug 2024 19:33:38 +0200 Subject: [PATCH] def: order and torsion --- src/Algebra/Group/Instances/Integers.lagda.md | 82 +++++++++++++++++++ src/Data/Int/Properties.lagda.md | 17 ++++ src/Data/Nat/Order.lagda.md | 72 ++++++++-------- 3 files changed, 136 insertions(+), 35 deletions(-) diff --git a/src/Algebra/Group/Instances/Integers.lagda.md b/src/Algebra/Group/Instances/Integers.lagda.md index 1b1b16c72..a3299cb49 100644 --- a/src/Algebra/Group/Instances/Integers.lagda.md +++ b/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"} + + + +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) +``` diff --git a/src/Data/Int/Properties.lagda.md b/src/Data/Int/Properties.lagda.md index 81b827501..ced6cc3c2 100644 --- a/src/Data/Int/Properties.lagda.md +++ b/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 ``` diff --git a/src/Data/Nat/Order.lagda.md b/src/Data/Nat/Order.lagda.md index 5d4186564..108334fc3 100644 --- a/src/Data/Nat/Order.lagda.md +++ b/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,14 +256,14 @@ 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 @@ -271,30 +271,32 @@ 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 ```