From 6791f975a98ffb1af9c73f3e0883f90d92a4ba5a Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 11 Jan 2024 09:39:41 +0000 Subject: [PATCH 01/19] added new operations to `IsGroup` --- CHANGELOG.md | 10 ++++++++++ src/Algebra/Structures.agda | 11 +++++++++-- 2 files changed, 19 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5b3079dee4..749afef5d4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -32,6 +32,16 @@ New modules Additions to existing modules ----------------------------- +* In `Algebra.Structures.IsGroup`: + ```agda + infixl 6 _∙⁻¹_ + infixr 6 _⁻¹∙_ + _∙⁻¹_ : Op₂ A + x ∙⁻¹ y = x ∙ (y ⁻¹) + _⁻¹∙_ : Op₂ A + x ⁻¹∙ y = (x ⁻¹) ∙ y + ``` + * In `Data.Fin.Properties`: ```agda nonZeroIndex : Fin n → ℕ.NonZero n diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 44208367ea..1d62bee391 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -253,9 +253,16 @@ record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) w open IsMonoid isMonoid public + infixl 6 _∙⁻¹_ + infixr 6 _⁻¹∙_ + _∙⁻¹_ : Op₂ A + x ∙⁻¹ y = x ∙ (y ⁻¹) + _⁻¹∙_ : Op₂ A + x ⁻¹∙ y = (x ⁻¹) ∙ y + infixl 6 _-_ _-_ : Op₂ A - x - y = x ∙ (y ⁻¹) + _-_ = _∙⁻¹_ inverseˡ : LeftInverse ε _⁻¹ _∙_ inverseˡ = proj₁ inverse @@ -291,7 +298,7 @@ record IsAbelianGroup (∙ : Op₂ A) isGroup : IsGroup ∙ ε ⁻¹ comm : Commutative ∙ - open IsGroup isGroup public + open IsGroup isGroup public hiding (_∙⁻¹_; _⁻¹∙_) isCommutativeMonoid : IsCommutativeMonoid ∙ ε isCommutativeMonoid = record From cb62d7f37620c33351c36e0eae4faf74d845f693 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 28 Jan 2024 13:55:56 +0000 Subject: [PATCH 02/19] fixed notations --- CHANGELOG.md | 14 +++++++++----- src/Algebra/Structures.agda | 20 ++++++++++++-------- 2 files changed, 21 insertions(+), 13 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index d8e7fdca10..a12deb7d77 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -25,6 +25,11 @@ Deprecated modules Deprecated names ---------------- +* In `Algebra.Structures.IsGroup`: + ```agda + _-_ ↦ _//_ + ``` + * In `Data.Nat.Divisibility.Core`: ```agda *-pres-∣ ↦ Data.Nat.Divisibility.*-pres-∣ @@ -78,12 +83,11 @@ Additions to existing modules * In `Algebra.Structures.IsGroup`: ```agda - infixl 6 _∙⁻¹_ + infixl 6 _//_ infixr 6 _⁻¹∙_ - _∙⁻¹_ : Op₂ A - x ∙⁻¹ y = x ∙ (y ⁻¹) - _⁻¹∙_ : Op₂ A - x ⁻¹∙ y = (x ⁻¹) ∙ y + _//_ _\\_ : Op₂ A + x // y = x ∙ (y ⁻¹) + x \\ y = (x ⁻¹) ∙ y * In `Data.Fin.Properties`: ```agda diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 1d62bee391..662ac57202 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -253,16 +253,20 @@ record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) w open IsMonoid isMonoid public - infixl 6 _∙⁻¹_ - infixr 6 _⁻¹∙_ - _∙⁻¹_ : Op₂ A - x ∙⁻¹ y = x ∙ (y ⁻¹) - _⁻¹∙_ : Op₂ A - x ⁻¹∙ y = (x ⁻¹) ∙ y + infixl 6 _//_ + infixr 6 _\\_ + _//_ _\\_ : Op₂ A + x // y = x ∙ (y ⁻¹) + x \\ y = (x ⁻¹) ∙ y + -- Deprecated. infixl 6 _-_ _-_ : Op₂ A - _-_ = _∙⁻¹_ + _-_ = _//_ + {-# WARNING_ON_USAGE _-_ + "Warning: _-_ was deprecated in v2.1. + Please use _//_ instead. " + #-} inverseˡ : LeftInverse ε _⁻¹ _∙_ inverseˡ = proj₁ inverse @@ -298,7 +302,7 @@ record IsAbelianGroup (∙ : Op₂ A) isGroup : IsGroup ∙ ε ⁻¹ comm : Commutative ∙ - open IsGroup isGroup public hiding (_∙⁻¹_; _⁻¹∙_) + open IsGroup isGroup public renaming (_//_ to _-_) hiding (_\\_; _-_) isCommutativeMonoid : IsCommutativeMonoid ∙ ε isCommutativeMonoid = record From 4a8e21891d3e3a854b2e5e4a875e3f771b2b6897 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 28 Jan 2024 15:29:34 +0000 Subject: [PATCH 03/19] fixed `CHANGELOG` --- CHANGELOG.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index a12deb7d77..28b474aea5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -81,6 +81,12 @@ Additions to existing modules rawModule : RawModule R c ℓ ``` +* In `Algebra.Properties.Group`: + ```agda + isQuasigroup : IsQuasigroup _∙_ _\\_ _//_ + isLoop : IsLoop _∙_ _\\_ _//_ ε + ``` + * In `Algebra.Structures.IsGroup`: ```agda infixl 6 _//_ @@ -88,6 +94,7 @@ Additions to existing modules _//_ _\\_ : Op₂ A x // y = x ∙ (y ⁻¹) x \\ y = (x ⁻¹) ∙ y + ``` * In `Data.Fin.Properties`: ```agda From 0696b58a93feb8ee07eae37acf2ac569dcf83125 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 28 Jan 2024 17:55:41 +0000 Subject: [PATCH 04/19] refactoring `Group` properties: added `isQuasigroup` and `isLoop` --- src/Algebra/Properties/Group.agda | 63 ++++++++++++++++++++++++++----- 1 file changed, 53 insertions(+), 10 deletions(-) diff --git a/src/Algebra/Properties/Group.agda b/src/Algebra/Properties/Group.agda index 31f9aedf39..c821b7364b 100644 --- a/src/Algebra/Properties/Group.agda +++ b/src/Algebra/Properties/Group.agda @@ -12,6 +12,7 @@ module Algebra.Properties.Group {g₁ g₂} (G : Group g₁ g₂) where open Group G open import Algebra.Definitions _≈_ +open import Algebra.Structures _≈_ using (IsLoop; IsQuasigroup) open import Relation.Binary.Reasoning.Setoid setoid open import Function.Base using (_$_; _⟨_⟩_) open import Data.Product.Base using (_,_; proj₂) @@ -22,21 +23,53 @@ open import Data.Product.Base using (_,_; proj₂) ε ⁻¹ ∙ ε ≈⟨ inverseˡ ε ⟩ ε ∎ +leftDividesˡ : ∀ x y → x ∙ (x \\ y) ≈ y +leftDividesˡ x y = begin + x ∙ (x \\ y) ≈⟨ assoc x (x ⁻¹) y ⟨ + x ∙ x ⁻¹ ∙ y ≈⟨ ∙-congʳ (inverseʳ x) ⟩ + ε ∙ y ≈⟨ identityˡ y ⟩ + y ∎ + +leftDividesʳ : ∀ x y → x \\ x ∙ y ≈ y +leftDividesʳ x y = begin + x \\ x ∙ y ≈⟨ assoc (x ⁻¹) x y ⟨ + x ⁻¹ ∙ x ∙ y ≈⟨ ∙-congʳ (inverseˡ x) ⟩ + ε ∙ y ≈⟨ identityˡ y ⟩ + y ∎ + +rightDividesˡ : ∀ x y → (y // x) ∙ x ≈ y +rightDividesˡ x y = begin + (y // x) ∙ x ≈⟨ assoc y (x ⁻¹) x ⟩ + y ∙ (x ⁻¹ ∙ x) ≈⟨ ∙-congˡ (inverseˡ x) ⟩ + y ∙ ε ≈⟨ identityʳ y ⟩ + y ∎ + +rightDividesʳ : ∀ x y → y ∙ x // x ≈ y +rightDividesʳ x y = begin + y ∙ x // x ≈⟨ assoc y x (x ⁻¹) ⟩ + y ∙ (x // x) ≈⟨ ∙-congˡ (inverseʳ x) ⟩ + y ∙ ε ≈⟨ identityʳ y ⟩ + y ∎ + +isQuasigroup : IsQuasigroup _∙_ _\\_ _//_ +isQuasigroup = record + { isMagma = isMagma + ; \\-cong = λ x≈y u≈v → ∙-cong (⁻¹-cong x≈y) u≈v + ; //-cong = λ x≈y u≈v → ∙-cong x≈y (⁻¹-cong u≈v) + ; leftDivides = leftDividesˡ , leftDividesʳ + ; rightDivides = rightDividesˡ , rightDividesʳ + } + +isLoop : IsLoop _∙_ _\\_ _//_ ε +isLoop = record { isQuasigroup = isQuasigroup ; identity = identity } + private left-helper : ∀ x y → x ≈ (x ∙ y) ∙ y ⁻¹ - left-helper x y = begin - x ≈⟨ sym (identityʳ x) ⟩ - x ∙ ε ≈⟨ ∙-congˡ $ sym (inverseʳ y) ⟩ - x ∙ (y ∙ y ⁻¹) ≈⟨ sym (assoc x y (y ⁻¹)) ⟩ - (x ∙ y) ∙ y ⁻¹ ∎ + left-helper x y = sym (rightDividesʳ y x) right-helper : ∀ x y → y ≈ x ⁻¹ ∙ (x ∙ y) - right-helper x y = begin - y ≈⟨ sym (identityˡ y) ⟩ - ε ∙ y ≈⟨ ∙-congʳ $ sym (inverseˡ x) ⟩ - (x ⁻¹ ∙ x) ∙ y ≈⟨ assoc (x ⁻¹) x y ⟩ - x ⁻¹ ∙ (x ∙ y) ∎ + right-helper x y = sym (leftDividesʳ x y) ∙-cancelˡ : LeftCancellative _∙_ ∙-cancelˡ x y z eq = begin @@ -106,3 +139,13 @@ inverseʳ-unique x y eq = begin y ≈⟨ sym (⁻¹-involutive y) ⟩ y ⁻¹ ⁻¹ ≈⟨ ⁻¹-cong (sym (inverseˡ-unique x y eq)) ⟩ x ⁻¹ ∎ +{- +\\≗//⇒comm : (∀ {x y} → x \\ y ≈ x // y) → Commutative _∙_ +\\≗//⇒comm \\≗// x y = begin + x ∙ y ≈⟨ {!inverseʳ y!} ⟩ + {!!} ≈⟨ {!!} ⟩ + {!!} ≈⟨ {!!} ⟩ + {!!} ≈⟨ {!!} ⟩ + {!!} ≈⟨ {!!} ⟩ + y ∙ x ∎ +-} From ac8addefec8c026159b76aabf0b6fcb93ff06292 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 28 Jan 2024 22:52:42 +0000 Subject: [PATCH 05/19] refactoring `*-helper` lemmas --- src/Algebra/Properties/Group.agda | 28 ++++++++++------------------ 1 file changed, 10 insertions(+), 18 deletions(-) diff --git a/src/Algebra/Properties/Group.agda b/src/Algebra/Properties/Group.agda index c821b7364b..80f577f85d 100644 --- a/src/Algebra/Properties/Group.agda +++ b/src/Algebra/Properties/Group.agda @@ -63,26 +63,18 @@ isQuasigroup = record isLoop : IsLoop _∙_ _\\_ _//_ ε isLoop = record { isQuasigroup = isQuasigroup ; identity = identity } -private - - left-helper : ∀ x y → x ≈ (x ∙ y) ∙ y ⁻¹ - left-helper x y = sym (rightDividesʳ y x) - - right-helper : ∀ x y → y ≈ x ⁻¹ ∙ (x ∙ y) - right-helper x y = sym (leftDividesʳ x y) - ∙-cancelˡ : LeftCancellative _∙_ ∙-cancelˡ x y z eq = begin - y ≈⟨ right-helper x y ⟩ + y ≈⟨ leftDividesʳ x y ⟨ x ⁻¹ ∙ (x ∙ y) ≈⟨ ∙-congˡ eq ⟩ - x ⁻¹ ∙ (x ∙ z) ≈⟨ right-helper x z ⟨ + x ⁻¹ ∙ (x ∙ z) ≈⟨ leftDividesʳ x z ⟩ z ∎ ∙-cancelʳ : RightCancellative _∙_ ∙-cancelʳ x y z eq = begin - y ≈⟨ left-helper y x ⟩ + y ≈⟨ rightDividesʳ x y ⟨ y ∙ x ∙ x ⁻¹ ≈⟨ ∙-congʳ eq ⟩ - z ∙ x ∙ x ⁻¹ ≈⟨ left-helper z x ⟨ + z ∙ x ∙ x ⁻¹ ≈⟨ rightDividesʳ x z ⟩ z ∎ ∙-cancel : Cancellative _∙_ @@ -92,7 +84,7 @@ private ⁻¹-involutive x = begin x ⁻¹ ⁻¹ ≈⟨ identityʳ _ ⟨ x ⁻¹ ⁻¹ ∙ ε ≈⟨ ∙-congˡ $ inverseˡ _ ⟨ - x ⁻¹ ⁻¹ ∙ (x ⁻¹ ∙ x) ≈⟨ right-helper (x ⁻¹) x ⟨ + x ⁻¹ ⁻¹ ∙ (x ⁻¹ ∙ x) ≈⟨ leftDividesʳ (x ⁻¹) x ⟩ x ∎ ⁻¹-injective : ∀ {x y} → x ⁻¹ ≈ y ⁻¹ → x ≈ y @@ -106,21 +98,21 @@ private ⁻¹-anti-homo-∙ x y = ∙-cancelˡ _ _ _ ( begin x ∙ y ∙ (x ∙ y) ⁻¹ ≈⟨ inverseʳ _ ⟩ ε ≈⟨ inverseʳ _ ⟨ - x ∙ x ⁻¹ ≈⟨ ∙-congʳ (left-helper x y) ⟩ + x ∙ x ⁻¹ ≈⟨ ∙-congʳ (rightDividesʳ y x) ⟨ (x ∙ y) ∙ y ⁻¹ ∙ x ⁻¹ ≈⟨ assoc (x ∙ y) (y ⁻¹) (x ⁻¹) ⟩ x ∙ y ∙ (y ⁻¹ ∙ x ⁻¹) ∎ ) identityˡ-unique : ∀ x y → x ∙ y ≈ y → x ≈ ε identityˡ-unique x y eq = begin - x ≈⟨ left-helper x y ⟩ + x ≈⟨ rightDividesʳ y x ⟨ (x ∙ y) ∙ y ⁻¹ ≈⟨ ∙-congʳ eq ⟩ y ∙ y ⁻¹ ≈⟨ inverseʳ y ⟩ ε ∎ identityʳ-unique : ∀ x y → x ∙ y ≈ x → y ≈ ε identityʳ-unique x y eq = begin - y ≈⟨ right-helper x y ⟩ - x ⁻¹ ∙ (x ∙ y) ≈⟨ refl ⟨ ∙-cong ⟩ eq ⟩ + y ≈⟨ leftDividesʳ x y ⟨ + x ⁻¹ ∙ (x ∙ y) ≈⟨ ∙-congˡ eq ⟩ x ⁻¹ ∙ x ≈⟨ inverseˡ x ⟩ ε ∎ @@ -129,7 +121,7 @@ identity-unique {x} id = identityˡ-unique x x (proj₂ id x) inverseˡ-unique : ∀ x y → x ∙ y ≈ ε → x ≈ y ⁻¹ inverseˡ-unique x y eq = begin - x ≈⟨ left-helper x y ⟩ + x ≈⟨ rightDividesʳ y x ⟨ (x ∙ y) ∙ y ⁻¹ ≈⟨ ∙-congʳ eq ⟩ ε ∙ y ⁻¹ ≈⟨ identityˡ (y ⁻¹) ⟩ y ⁻¹ ∎ From deffa514bd592730030f1fc7a0bd46e0e9bfc871 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 29 Jan 2024 05:26:09 +0000 Subject: [PATCH 06/19] fixed `CHANGELOG` --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 28b474aea5..904727e9a8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -90,7 +90,7 @@ Additions to existing modules * In `Algebra.Structures.IsGroup`: ```agda infixl 6 _//_ - infixr 6 _⁻¹∙_ + infixr 6 _\\_ _//_ _\\_ : Op₂ A x // y = x ∙ (y ⁻¹) x \\ y = (x ⁻¹) ∙ y From 61cd6614d61c27a5eaf345ea81ca7e3077acae79 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 29 Jan 2024 05:28:56 +0000 Subject: [PATCH 07/19] lemma relating quasigroup operations and `Commutative` property --- CHANGELOG.md | 1 + src/Algebra/Properties/Group.agda | 45 ++++++++++++++++--------------- 2 files changed, 24 insertions(+), 22 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 904727e9a8..811a949e9d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -85,6 +85,7 @@ Additions to existing modules ```agda isQuasigroup : IsQuasigroup _∙_ _\\_ _//_ isLoop : IsLoop _∙_ _\\_ _//_ ε + \\≗//ᵒ⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_ ``` * In `Algebra.Structures.IsGroup`: diff --git a/src/Algebra/Properties/Group.agda b/src/Algebra/Properties/Group.agda index 80f577f85d..d87862c9d0 100644 --- a/src/Algebra/Properties/Group.agda +++ b/src/Algebra/Properties/Group.agda @@ -17,12 +17,6 @@ open import Relation.Binary.Reasoning.Setoid setoid open import Function.Base using (_$_; _⟨_⟩_) open import Data.Product.Base using (_,_; proj₂) -ε⁻¹≈ε : ε ⁻¹ ≈ ε -ε⁻¹≈ε = begin - ε ⁻¹ ≈⟨ sym $ identityʳ (ε ⁻¹) ⟩ - ε ⁻¹ ∙ ε ≈⟨ inverseˡ ε ⟩ - ε ∎ - leftDividesˡ : ∀ x y → x ∙ (x \\ y) ≈ y leftDividesˡ x y = begin x ∙ (x \\ y) ≈⟨ assoc x (x ⁻¹) y ⟨ @@ -63,6 +57,12 @@ isQuasigroup = record isLoop : IsLoop _∙_ _\\_ _//_ ε isLoop = record { isQuasigroup = isQuasigroup ; identity = identity } +ε⁻¹≈ε : ε ⁻¹ ≈ ε +ε⁻¹≈ε = begin + ε ⁻¹ ≈⟨ identityʳ (ε ⁻¹) ⟨ + ε ⁻¹ ∙ ε ≈⟨ inverseˡ ε ⟩ + ε ∎ + ∙-cancelˡ : LeftCancellative _∙_ ∙-cancelˡ x y z eq = begin y ≈⟨ leftDividesʳ x y ⟨ @@ -88,19 +88,19 @@ isLoop = record { isQuasigroup = isQuasigroup ; identity = identity } x ∎ ⁻¹-injective : ∀ {x y} → x ⁻¹ ≈ y ⁻¹ → x ≈ y -⁻¹-injective {x} {y} eq = ∙-cancelʳ _ _ _ ( begin +⁻¹-injective {x} {y} eq = ∙-cancelʳ _ _ _ $ begin x ∙ x ⁻¹ ≈⟨ inverseʳ x ⟩ ε ≈⟨ inverseʳ y ⟨ y ∙ y ⁻¹ ≈⟨ ∙-congˡ eq ⟨ - y ∙ x ⁻¹ ∎ ) + y ∙ x ⁻¹ ∎ ⁻¹-anti-homo-∙ : ∀ x y → (x ∙ y) ⁻¹ ≈ y ⁻¹ ∙ x ⁻¹ -⁻¹-anti-homo-∙ x y = ∙-cancelˡ _ _ _ ( begin +⁻¹-anti-homo-∙ x y = ∙-cancelˡ _ _ _ $ begin x ∙ y ∙ (x ∙ y) ⁻¹ ≈⟨ inverseʳ _ ⟩ ε ≈⟨ inverseʳ _ ⟨ x ∙ x ⁻¹ ≈⟨ ∙-congʳ (rightDividesʳ y x) ⟨ (x ∙ y) ∙ y ⁻¹ ∙ x ⁻¹ ≈⟨ assoc (x ∙ y) (y ⁻¹) (x ⁻¹) ⟩ - x ∙ y ∙ (y ⁻¹ ∙ x ⁻¹) ∎ ) + x ∙ y ∙ (y ⁻¹ ∙ x ⁻¹) ∎ identityˡ-unique : ∀ x y → x ∙ y ≈ y → x ≈ ε identityˡ-unique x y eq = begin @@ -128,16 +128,17 @@ inverseˡ-unique x y eq = begin inverseʳ-unique : ∀ x y → x ∙ y ≈ ε → y ≈ x ⁻¹ inverseʳ-unique x y eq = begin - y ≈⟨ sym (⁻¹-involutive y) ⟩ - y ⁻¹ ⁻¹ ≈⟨ ⁻¹-cong (sym (inverseˡ-unique x y eq)) ⟩ + y ≈⟨ ⁻¹-involutive y ⟨ + y ⁻¹ ⁻¹ ≈⟨ ⁻¹-cong (inverseˡ-unique x y eq) ⟨ x ⁻¹ ∎ -{- -\\≗//⇒comm : (∀ {x y} → x \\ y ≈ x // y) → Commutative _∙_ -\\≗//⇒comm \\≗// x y = begin - x ∙ y ≈⟨ {!inverseʳ y!} ⟩ - {!!} ≈⟨ {!!} ⟩ - {!!} ≈⟨ {!!} ⟩ - {!!} ≈⟨ {!!} ⟩ - {!!} ≈⟨ {!!} ⟩ - y ∙ x ∎ --} + +\\≗//ᵒ⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_ +\\≗//ᵒ⇒comm \\≗//ᵒ x y = begin + x ∙ y ≈⟨ identityʳ _ ⟨ + (x ∙ y) ∙ ε ≈⟨ ∙-congˡ (inverseˡ x) ⟨ + (x ∙ y) ∙ (x ⁻¹ ∙ x) ≈⟨ assoc (x ∙ y) (x ⁻¹) x ⟨ + (x ∙ y) ∙ x ⁻¹ ∙ x ≈⟨ ∙-congʳ (assoc x y (x ⁻¹)) ⟩ + x ∙ (y // x) ∙ x ≈⟨ ∙-congʳ (∙-congˡ (\\≗//ᵒ x y)) ⟨ + x ∙ (x \\ y) ∙ x ≈⟨ ∙-congʳ (leftDividesˡ x y) ⟩ + y ∙ x ∎ + From 5593a51192130db0b83caebcb58c773e5a66c58f Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 29 Jan 2024 18:35:34 +0000 Subject: [PATCH 08/19] simplified proof --- src/Algebra/Properties/Group.agda | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/Algebra/Properties/Group.agda b/src/Algebra/Properties/Group.agda index d87862c9d0..fde16f104e 100644 --- a/src/Algebra/Properties/Group.agda +++ b/src/Algebra/Properties/Group.agda @@ -134,11 +134,9 @@ inverseʳ-unique x y eq = begin \\≗//ᵒ⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_ \\≗//ᵒ⇒comm \\≗//ᵒ x y = begin - x ∙ y ≈⟨ identityʳ _ ⟨ - (x ∙ y) ∙ ε ≈⟨ ∙-congˡ (inverseˡ x) ⟨ - (x ∙ y) ∙ (x ⁻¹ ∙ x) ≈⟨ assoc (x ∙ y) (x ⁻¹) x ⟨ - (x ∙ y) ∙ x ⁻¹ ∙ x ≈⟨ ∙-congʳ (assoc x y (x ⁻¹)) ⟩ - x ∙ (y // x) ∙ x ≈⟨ ∙-congʳ (∙-congˡ (\\≗//ᵒ x y)) ⟨ + x ∙ y ≈⟨ ∙-congˡ (rightDividesˡ x y) ⟨ + x ∙ ((y // x) ∙ x) ≈⟨ ∙-congˡ (∙-congʳ (\\≗//ᵒ x y)) ⟨ + x ∙ ((x \\ y) ∙ x) ≈⟨ assoc x (x \\ y) x ⟨ x ∙ (x \\ y) ∙ x ≈⟨ ∙-congʳ (leftDividesˡ x y) ⟩ y ∙ x ∎ From 6576f410093d2e9318df7c396dd097284f2eeeaa Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 29 Jan 2024 19:07:09 +0000 Subject: [PATCH 09/19] =?UTF-8?q?added=20converse=20property=20to=20\?= =?UTF-8?q?=C2=ACAlgebra.Properties.AbelianGroup`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- CHANGELOG.md | 5 +++++ src/Algebra/Properties/AbelianGroup.agda | 10 ++++++++++ 2 files changed, 15 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 811a949e9d..71d87c77b3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -81,6 +81,11 @@ Additions to existing modules rawModule : RawModule R c ℓ ``` +* In `Algebra.Properties.AbelianGroup`: + ```agda + \\≗//ᵒ : ∀ x y → x \\ y ≈ y // x + ``` + * In `Algebra.Properties.Group`: ```agda isQuasigroup : IsQuasigroup _∙_ _\\_ _//_ diff --git a/src/Algebra/Properties/AbelianGroup.agda b/src/Algebra/Properties/AbelianGroup.agda index 87c6b7c6b9..256a074679 100644 --- a/src/Algebra/Properties/AbelianGroup.agda +++ b/src/Algebra/Properties/AbelianGroup.agda @@ -36,3 +36,13 @@ xyx⁻¹≈y x y = begin x ⁻¹ ∙ y ⁻¹ ≈⟨ ⁻¹-anti-homo-∙ y x ⟨ (y ∙ x) ⁻¹ ≈⟨ ⁻¹-cong $ comm y x ⟩ (x ∙ y) ⁻¹ ∎ + +module _ where + open IsGroup isGroup using (_//_; _\\_) + + \\≗//ᵒ : ∀ x y → x \\ y ≈ y // x + \\≗//ᵒ x y = begin + x \\ y ≈⟨ refl ⟩ + x ⁻¹ ∙ y ≈⟨ comm _ _ ⟩ + y ∙ x ⁻¹ ≈⟨ refl ⟩ + y // x ∎ From 59eb92180eaa9937d429075814cf884398fdea31 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 30 Jan 2024 14:52:21 +0000 Subject: [PATCH 10/19] moved lemma --- CHANGELOG.md | 6 +----- src/Algebra/Properties/AbelianGroup.agda | 10 ---------- src/Algebra/Properties/Group.agda | 6 ++++++ 3 files changed, 7 insertions(+), 15 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 71d87c77b3..16f5daabfe 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -81,16 +81,12 @@ Additions to existing modules rawModule : RawModule R c ℓ ``` -* In `Algebra.Properties.AbelianGroup`: - ```agda - \\≗//ᵒ : ∀ x y → x \\ y ≈ y // x - ``` - * In `Algebra.Properties.Group`: ```agda isQuasigroup : IsQuasigroup _∙_ _\\_ _//_ isLoop : IsLoop _∙_ _\\_ _//_ ε \\≗//ᵒ⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_ + comm⇒\\≗//ᵒ : ∀ x y → x \\ y ≈ y // x ``` * In `Algebra.Structures.IsGroup`: diff --git a/src/Algebra/Properties/AbelianGroup.agda b/src/Algebra/Properties/AbelianGroup.agda index 256a074679..87c6b7c6b9 100644 --- a/src/Algebra/Properties/AbelianGroup.agda +++ b/src/Algebra/Properties/AbelianGroup.agda @@ -36,13 +36,3 @@ xyx⁻¹≈y x y = begin x ⁻¹ ∙ y ⁻¹ ≈⟨ ⁻¹-anti-homo-∙ y x ⟨ (y ∙ x) ⁻¹ ≈⟨ ⁻¹-cong $ comm y x ⟩ (x ∙ y) ⁻¹ ∎ - -module _ where - open IsGroup isGroup using (_//_; _\\_) - - \\≗//ᵒ : ∀ x y → x \\ y ≈ y // x - \\≗//ᵒ x y = begin - x \\ y ≈⟨ refl ⟩ - x ⁻¹ ∙ y ≈⟨ comm _ _ ⟩ - y ∙ x ⁻¹ ≈⟨ refl ⟩ - y // x ∎ diff --git a/src/Algebra/Properties/Group.agda b/src/Algebra/Properties/Group.agda index fde16f104e..f7f3bf6773 100644 --- a/src/Algebra/Properties/Group.agda +++ b/src/Algebra/Properties/Group.agda @@ -140,3 +140,9 @@ inverseʳ-unique x y eq = begin x ∙ (x \\ y) ∙ x ≈⟨ ∙-congʳ (leftDividesˡ x y) ⟩ y ∙ x ∎ +comm⇒\\≗//ᵒ : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x +comm⇒\\≗//ᵒ comm x y = begin + x \\ y ≈⟨ refl ⟩ + x ⁻¹ ∙ y ≈⟨ comm _ _ ⟩ + y ∙ x ⁻¹ ≈⟨ refl ⟩ + y // x ∎ From ca6b6f54f6d28ccbbe6662ad44baf81bc192a5be Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 30 Jan 2024 15:01:21 +0000 Subject: [PATCH 11/19] indentation; congruence lemmas --- src/Algebra/Properties/Group.agda | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/src/Algebra/Properties/Group.agda b/src/Algebra/Properties/Group.agda index f7f3bf6773..8ed55f28ae 100644 --- a/src/Algebra/Properties/Group.agda +++ b/src/Algebra/Properties/Group.agda @@ -17,6 +17,12 @@ open import Relation.Binary.Reasoning.Setoid setoid open import Function.Base using (_$_; _⟨_⟩_) open import Data.Product.Base using (_,_; proj₂) +\\-cong₂ : Congruent₂ _\\_ +\\-cong₂ x≈y u≈v = ∙-cong (⁻¹-cong x≈y) u≈v + +//-cong₂ : Congruent₂ _//_ +//-cong₂ x≈y u≈v = ∙-cong x≈y (⁻¹-cong u≈v) + leftDividesˡ : ∀ x y → x ∙ (x \\ y) ≈ y leftDividesˡ x y = begin x ∙ (x \\ y) ≈⟨ assoc x (x ⁻¹) y ⟨ @@ -47,12 +53,12 @@ rightDividesʳ x y = begin isQuasigroup : IsQuasigroup _∙_ _\\_ _//_ isQuasigroup = record - { isMagma = isMagma - ; \\-cong = λ x≈y u≈v → ∙-cong (⁻¹-cong x≈y) u≈v - ; //-cong = λ x≈y u≈v → ∙-cong x≈y (⁻¹-cong u≈v) - ; leftDivides = leftDividesˡ , leftDividesʳ - ; rightDivides = rightDividesˡ , rightDividesʳ - } + { isMagma = isMagma + ; \\-cong = \\-cong₂ + ; //-cong = //-cong₂ + ; leftDivides = leftDividesˡ , leftDividesʳ + ; rightDivides = rightDividesˡ , rightDividesʳ + } isLoop : IsLoop _∙_ _\\_ _//_ ε isLoop = record { isQuasigroup = isQuasigroup ; identity = identity } From a5ef9a13a91f8bd4444d7060e381b802775ec3f8 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 30 Jan 2024 15:09:27 +0000 Subject: [PATCH 12/19] untangled operation definitions --- src/Algebra/Structures.agda | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 662ac57202..bb28e89882 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -253,12 +253,14 @@ record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) w open IsMonoid isMonoid public - infixl 6 _//_ infixr 6 _\\_ - _//_ _\\_ : Op₂ A - x // y = x ∙ (y ⁻¹) + _\\_ : Op₂ A x \\ y = (x ⁻¹) ∙ y + infixl 6 _//_ + _//_ : Op₂ A + x // y = x ∙ (y ⁻¹) + -- Deprecated. infixl 6 _-_ _-_ : Op₂ A From 68e4bd6bff974d4ecf61c4a603dc19a2baa59bea Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 30 Jan 2024 15:11:45 +0000 Subject: [PATCH 13/19] untangled operation definitions in `CHANGELOG` --- CHANGELOG.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 16f5daabfe..c4ca1f6541 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -92,9 +92,10 @@ Additions to existing modules * In `Algebra.Structures.IsGroup`: ```agda infixl 6 _//_ - infixr 6 _\\_ - _//_ _\\_ : Op₂ A + _//_ : Op₂ A x // y = x ∙ (y ⁻¹) + infixr 6 _\\_ + _\\_ : Op₂ A x \\ y = (x ⁻¹) ∙ y ``` From a40e3c8490bdaa6aab6a87027a656822ccb02295 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 30 Jan 2024 23:57:36 +0000 Subject: [PATCH 14/19] fixed names --- CHANGELOG.md | 4 ++-- src/Algebra/Properties/Group.agda | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index c4ca1f6541..80ef2f2016 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -85,8 +85,8 @@ Additions to existing modules ```agda isQuasigroup : IsQuasigroup _∙_ _\\_ _//_ isLoop : IsLoop _∙_ _\\_ _//_ ε - \\≗//ᵒ⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_ - comm⇒\\≗//ᵒ : ∀ x y → x \\ y ≈ y // x + \\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_ + comm⇒\\≗flip-// : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x ``` * In `Algebra.Structures.IsGroup`: diff --git a/src/Algebra/Properties/Group.agda b/src/Algebra/Properties/Group.agda index 8ed55f28ae..beed665d4c 100644 --- a/src/Algebra/Properties/Group.agda +++ b/src/Algebra/Properties/Group.agda @@ -138,16 +138,16 @@ inverseʳ-unique x y eq = begin y ⁻¹ ⁻¹ ≈⟨ ⁻¹-cong (inverseˡ-unique x y eq) ⟨ x ⁻¹ ∎ -\\≗//ᵒ⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_ -\\≗//ᵒ⇒comm \\≗//ᵒ x y = begin +\\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_ +\\≗flip-//⇒comm \\≗//ᵒ x y = begin x ∙ y ≈⟨ ∙-congˡ (rightDividesˡ x y) ⟨ x ∙ ((y // x) ∙ x) ≈⟨ ∙-congˡ (∙-congʳ (\\≗//ᵒ x y)) ⟨ x ∙ ((x \\ y) ∙ x) ≈⟨ assoc x (x \\ y) x ⟨ x ∙ (x \\ y) ∙ x ≈⟨ ∙-congʳ (leftDividesˡ x y) ⟩ y ∙ x ∎ -comm⇒\\≗//ᵒ : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x -comm⇒\\≗//ᵒ comm x y = begin +comm⇒\\≗flip-// : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x +comm⇒\\≗flip-// comm x y = begin x \\ y ≈⟨ refl ⟩ x ⁻¹ ∙ y ≈⟨ comm _ _ ⟩ y ∙ x ⁻¹ ≈⟨ refl ⟩ From 1295962bcce443dbdd564be3805fdbd00d2bb3dc Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 31 Jan 2024 10:53:37 +0000 Subject: [PATCH 15/19] reflexive reasoning; tightened imports --- src/Algebra/Properties/Group.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Algebra/Properties/Group.agda b/src/Algebra/Properties/Group.agda index beed665d4c..62773fa5a4 100644 --- a/src/Algebra/Properties/Group.agda +++ b/src/Algebra/Properties/Group.agda @@ -14,7 +14,7 @@ open Group G open import Algebra.Definitions _≈_ open import Algebra.Structures _≈_ using (IsLoop; IsQuasigroup) open import Relation.Binary.Reasoning.Setoid setoid -open import Function.Base using (_$_; _⟨_⟩_) +open import Function.Base using (_$_) open import Data.Product.Base using (_,_; proj₂) \\-cong₂ : Congruent₂ _\\_ @@ -148,7 +148,7 @@ inverseʳ-unique x y eq = begin comm⇒\\≗flip-// : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x comm⇒\\≗flip-// comm x y = begin - x \\ y ≈⟨ refl ⟩ + x \\ y ≡⟨⟩ x ⁻¹ ∙ y ≈⟨ comm _ _ ⟩ - y ∙ x ⁻¹ ≈⟨ refl ⟩ + y ∙ x ⁻¹ ≡⟨⟩ y // x ∎ From 4e6c575e072edc2b5ca490a11f063b8d4e5f838c Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 3 Feb 2024 13:50:12 +0000 Subject: [PATCH 16/19] refactoring to push properties into `Loop`, and re-export them from there and `Quasigroup` --- CHANGELOG.md | 13 ++++++-- src/Algebra/Properties/Group.agda | 49 ++++++++++--------------------- src/Algebra/Properties/Loop.agda | 23 +++++++++++++-- 3 files changed, 47 insertions(+), 38 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 80ef2f2016..1d8b572e54 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -83,12 +83,21 @@ Additions to existing modules * In `Algebra.Properties.Group`: ```agda - isQuasigroup : IsQuasigroup _∙_ _\\_ _//_ - isLoop : IsLoop _∙_ _\\_ _//_ ε + isQuasigroup : IsQuasigroup _∙_ _\\_ _//_ + quasigroup : Quasigroup _ _ + isLoop : IsLoop _∙_ _\\_ _//_ ε + loop : Loop _ _ \\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_ comm⇒\\≗flip-// : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x ``` +* In `Algebra.Properties.Loop`: + ```agda + identityˡ-unique : x ∙ y ≈ y → x ≈ ε + identityʳ-unique : x ∙ y ≈ x → y ≈ ε + identity-unique : Identity x _∙_ → x ≈ ε + ``` + * In `Algebra.Structures.IsGroup`: ```agda infixl 6 _//_ diff --git a/src/Algebra/Properties/Group.agda b/src/Algebra/Properties/Group.agda index 62773fa5a4..3b9d85d857 100644 --- a/src/Algebra/Properties/Group.agda +++ b/src/Algebra/Properties/Group.agda @@ -12,6 +12,8 @@ module Algebra.Properties.Group {g₁ g₂} (G : Group g₁ g₂) where open Group G open import Algebra.Definitions _≈_ +import Algebra.Properties.Loop as LoopProperties +import Algebra.Properties.Quasigroup as QuasigroupProperties open import Algebra.Structures _≈_ using (IsLoop; IsQuasigroup) open import Relation.Binary.Reasoning.Setoid setoid open import Function.Base using (_$_) @@ -60,32 +62,28 @@ isQuasigroup = record ; rightDivides = rightDividesˡ , rightDividesʳ } +quasigroup : Quasigroup _ _ +quasigroup = record { isQuasigroup = isQuasigroup } + +open QuasigroupProperties quasigroup public + using () + renaming (cancelˡ to ∙-cancelˡ; cancelʳ to ∙-cancelʳ; cancel to ∙-cancel) + isLoop : IsLoop _∙_ _\\_ _//_ ε isLoop = record { isQuasigroup = isQuasigroup ; identity = identity } +loop : Loop _ _ +loop = record { isLoop = isLoop } + +open LoopProperties loop public + using (identityˡ-unique; identityʳ-unique; identity-unique) + ε⁻¹≈ε : ε ⁻¹ ≈ ε ε⁻¹≈ε = begin ε ⁻¹ ≈⟨ identityʳ (ε ⁻¹) ⟨ ε ⁻¹ ∙ ε ≈⟨ inverseˡ ε ⟩ ε ∎ -∙-cancelˡ : LeftCancellative _∙_ -∙-cancelˡ x y z eq = begin - y ≈⟨ leftDividesʳ x y ⟨ - x ⁻¹ ∙ (x ∙ y) ≈⟨ ∙-congˡ eq ⟩ - x ⁻¹ ∙ (x ∙ z) ≈⟨ leftDividesʳ x z ⟩ - z ∎ - -∙-cancelʳ : RightCancellative _∙_ -∙-cancelʳ x y z eq = begin - y ≈⟨ rightDividesʳ x y ⟨ - y ∙ x ∙ x ⁻¹ ≈⟨ ∙-congʳ eq ⟩ - z ∙ x ∙ x ⁻¹ ≈⟨ rightDividesʳ x z ⟩ - z ∎ - -∙-cancel : Cancellative _∙_ -∙-cancel = ∙-cancelˡ , ∙-cancelʳ - ⁻¹-involutive : ∀ x → x ⁻¹ ⁻¹ ≈ x ⁻¹-involutive x = begin x ⁻¹ ⁻¹ ≈⟨ identityʳ _ ⟨ @@ -108,23 +106,6 @@ isLoop = record { isQuasigroup = isQuasigroup ; identity = identity } (x ∙ y) ∙ y ⁻¹ ∙ x ⁻¹ ≈⟨ assoc (x ∙ y) (y ⁻¹) (x ⁻¹) ⟩ x ∙ y ∙ (y ⁻¹ ∙ x ⁻¹) ∎ -identityˡ-unique : ∀ x y → x ∙ y ≈ y → x ≈ ε -identityˡ-unique x y eq = begin - x ≈⟨ rightDividesʳ y x ⟨ - (x ∙ y) ∙ y ⁻¹ ≈⟨ ∙-congʳ eq ⟩ - y ∙ y ⁻¹ ≈⟨ inverseʳ y ⟩ - ε ∎ - -identityʳ-unique : ∀ x y → x ∙ y ≈ x → y ≈ ε -identityʳ-unique x y eq = begin - y ≈⟨ leftDividesʳ x y ⟨ - x ⁻¹ ∙ (x ∙ y) ≈⟨ ∙-congˡ eq ⟩ - x ⁻¹ ∙ x ≈⟨ inverseˡ x ⟩ - ε ∎ - -identity-unique : ∀ {x} → Identity x _∙_ → x ≈ ε -identity-unique {x} id = identityˡ-unique x x (proj₂ id x) - inverseˡ-unique : ∀ x y → x ∙ y ≈ ε → x ≈ y ⁻¹ inverseˡ-unique x y eq = begin x ≈⟨ rightDividesʳ y x ⟨ diff --git a/src/Algebra/Properties/Loop.agda b/src/Algebra/Properties/Loop.agda index 1ecb2c52f4..3e7cd5f242 100644 --- a/src/Algebra/Properties/Loop.agda +++ b/src/Algebra/Properties/Loop.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Some basic properties of Quasigroup +-- Some basic properties of Loop ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} @@ -12,8 +12,9 @@ module Algebra.Properties.Loop {l₁ l₂} (L : Loop l₁ l₂) where open Loop L open import Algebra.Definitions _≈_ -open import Relation.Binary.Reasoning.Setoid setoid open import Algebra.Properties.Quasigroup +open import Data.Product.Base using (proj₂) +open import Relation.Binary.Reasoning.Setoid setoid x//x≈ε : ∀ x → x // x ≈ ε x//x≈ε x = begin @@ -38,3 +39,21 @@ x//ε≈x x = begin x // ε ≈⟨ sym (identityʳ (x // ε)) ⟩ (x // ε) ∙ ε ≈⟨ rightDividesˡ ε x ⟩ x ∎ + +identityˡ-unique : ∀ x y → x ∙ y ≈ y → x ≈ ε +identityˡ-unique x y eq = begin + x ≈⟨ rightDividesʳ y x ⟨ + (x ∙ y) // y ≈⟨ //-congʳ eq ⟩ + y // y ≈⟨ x//x≈ε y ⟩ + ε ∎ + +identityʳ-unique : ∀ x y → x ∙ y ≈ x → y ≈ ε +identityʳ-unique x y eq = begin + y ≈⟨ leftDividesʳ x y ⟨ + x \\ (x ∙ y) ≈⟨ \\-congˡ eq ⟩ + x \\ x ≈⟨ x\\x≈ε x ⟩ + ε ∎ + +identity-unique : ∀ {x} → Identity x _∙_ → x ≈ ε +identity-unique {x} id = identityˡ-unique x x (proj₂ id x) + From c937948a9bba28669a4e6502de38deffc2528f2e Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 3 Feb 2024 14:25:30 +0000 Subject: [PATCH 17/19] further refactoring --- src/Algebra/Properties/Group.agda | 25 +++++++++---------------- src/Algebra/Properties/Loop.agda | 16 +++++++--------- src/Algebra/Properties/Quasigroup.agda | 8 ++++---- 3 files changed, 20 insertions(+), 29 deletions(-) diff --git a/src/Algebra/Properties/Group.agda b/src/Algebra/Properties/Group.agda index 3b9d85d857..005f88078b 100644 --- a/src/Algebra/Properties/Group.agda +++ b/src/Algebra/Properties/Group.agda @@ -15,9 +15,9 @@ open import Algebra.Definitions _≈_ import Algebra.Properties.Loop as LoopProperties import Algebra.Properties.Quasigroup as QuasigroupProperties open import Algebra.Structures _≈_ using (IsLoop; IsQuasigroup) -open import Relation.Binary.Reasoning.Setoid setoid +open import Data.Product.Base using (_,_) open import Function.Base using (_$_) -open import Data.Product.Base using (_,_; proj₂) +open import Relation.Binary.Reasoning.Setoid setoid \\-cong₂ : Congruent₂ _\\_ \\-cong₂ x≈y u≈v = ∙-cong (⁻¹-cong x≈y) u≈v @@ -66,7 +66,7 @@ quasigroup : Quasigroup _ _ quasigroup = record { isQuasigroup = isQuasigroup } open QuasigroupProperties quasigroup public - using () + using (x≈z//y; y≈x\\z) renaming (cancelˡ to ∙-cancelˡ; cancelʳ to ∙-cancelʳ; cancel to ∙-cancel) isLoop : IsLoop _∙_ _\\_ _//_ ε @@ -84,6 +84,12 @@ open LoopProperties loop public ε ⁻¹ ∙ ε ≈⟨ inverseˡ ε ⟩ ε ∎ +inverseˡ-unique : ∀ x y → x ∙ y ≈ ε → x ≈ y ⁻¹ +inverseˡ-unique x y eq = trans (x≈z//y x y ε eq) (identityˡ _) + +inverseʳ-unique : ∀ x y → x ∙ y ≈ ε → y ≈ x ⁻¹ +inverseʳ-unique x y eq = trans (y≈x\\z x y ε eq) (identityʳ _) + ⁻¹-involutive : ∀ x → x ⁻¹ ⁻¹ ≈ x ⁻¹-involutive x = begin x ⁻¹ ⁻¹ ≈⟨ identityʳ _ ⟨ @@ -106,19 +112,6 @@ open LoopProperties loop public (x ∙ y) ∙ y ⁻¹ ∙ x ⁻¹ ≈⟨ assoc (x ∙ y) (y ⁻¹) (x ⁻¹) ⟩ x ∙ y ∙ (y ⁻¹ ∙ x ⁻¹) ∎ -inverseˡ-unique : ∀ x y → x ∙ y ≈ ε → x ≈ y ⁻¹ -inverseˡ-unique x y eq = begin - x ≈⟨ rightDividesʳ y x ⟨ - (x ∙ y) ∙ y ⁻¹ ≈⟨ ∙-congʳ eq ⟩ - ε ∙ y ⁻¹ ≈⟨ identityˡ (y ⁻¹) ⟩ - y ⁻¹ ∎ - -inverseʳ-unique : ∀ x y → x ∙ y ≈ ε → y ≈ x ⁻¹ -inverseʳ-unique x y eq = begin - y ≈⟨ ⁻¹-involutive y ⟨ - y ⁻¹ ⁻¹ ≈⟨ ⁻¹-cong (inverseˡ-unique x y eq) ⟨ - x ⁻¹ ∎ - \\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_ \\≗flip-//⇒comm \\≗//ᵒ x y = begin x ∙ y ≈⟨ ∙-congˡ (rightDividesˡ x y) ⟨ diff --git a/src/Algebra/Properties/Loop.agda b/src/Algebra/Properties/Loop.agda index 3e7cd5f242..69bb59ace5 100644 --- a/src/Algebra/Properties/Loop.agda +++ b/src/Algebra/Properties/Loop.agda @@ -12,7 +12,7 @@ module Algebra.Properties.Loop {l₁ l₂} (L : Loop l₁ l₂) where open Loop L open import Algebra.Definitions _≈_ -open import Algebra.Properties.Quasigroup +open import Algebra.Properties.Quasigroup quasigroup open import Data.Product.Base using (proj₂) open import Relation.Binary.Reasoning.Setoid setoid @@ -42,17 +42,15 @@ x//ε≈x x = begin identityˡ-unique : ∀ x y → x ∙ y ≈ y → x ≈ ε identityˡ-unique x y eq = begin - x ≈⟨ rightDividesʳ y x ⟨ - (x ∙ y) // y ≈⟨ //-congʳ eq ⟩ - y // y ≈⟨ x//x≈ε y ⟩ - ε ∎ + x ≈⟨ x≈z//y x y y eq ⟩ + y // y ≈⟨ x//x≈ε y ⟩ + ε ∎ identityʳ-unique : ∀ x y → x ∙ y ≈ x → y ≈ ε identityʳ-unique x y eq = begin - y ≈⟨ leftDividesʳ x y ⟨ - x \\ (x ∙ y) ≈⟨ \\-congˡ eq ⟩ - x \\ x ≈⟨ x\\x≈ε x ⟩ - ε ∎ + y ≈⟨ y≈x\\z x y x eq ⟩ + x \\ x ≈⟨ x\\x≈ε x ⟩ + ε ∎ identity-unique : ∀ {x} → Identity x _∙_ → x ≈ ε identity-unique {x} id = identityˡ-unique x x (proj₂ id x) diff --git a/src/Algebra/Properties/Quasigroup.agda b/src/Algebra/Properties/Quasigroup.agda index 335a9ea7a3..e8c7516978 100644 --- a/src/Algebra/Properties/Quasigroup.agda +++ b/src/Algebra/Properties/Quasigroup.agda @@ -17,14 +17,14 @@ open import Data.Product.Base using (_,_) cancelˡ : LeftCancellative _∙_ cancelˡ x y z eq = begin - y ≈⟨ sym( leftDividesʳ x y) ⟩ + y ≈⟨ leftDividesʳ x y ⟨ x \\ (x ∙ y) ≈⟨ \\-congˡ eq ⟩ x \\ (x ∙ z) ≈⟨ leftDividesʳ x z ⟩ z ∎ cancelʳ : RightCancellative _∙_ cancelʳ x y z eq = begin - y ≈⟨ sym( rightDividesʳ x y) ⟩ + y ≈⟨ rightDividesʳ x y ⟨ (y ∙ x) // x ≈⟨ //-congʳ eq ⟩ (z ∙ x) // x ≈⟨ rightDividesʳ x z ⟩ z ∎ @@ -34,12 +34,12 @@ cancel = cancelˡ , cancelʳ y≈x\\z : ∀ x y z → x ∙ y ≈ z → y ≈ x \\ z y≈x\\z x y z eq = begin - y ≈⟨ sym (leftDividesʳ x y) ⟩ + y ≈⟨ leftDividesʳ x y ⟨ x \\ (x ∙ y) ≈⟨ \\-congˡ eq ⟩ x \\ z ∎ x≈z//y : ∀ x y z → x ∙ y ≈ z → x ≈ z // y x≈z//y x y z eq = begin - x ≈⟨ sym (rightDividesʳ y x) ⟩ + x ≈⟨ rightDividesʳ y x ⟨ (x ∙ y) // y ≈⟨ //-congʳ eq ⟩ z // y ∎ From dc0ccd88d9436b12d3e2eaf4ddfb5810f819bb4a Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 3 Feb 2024 17:21:41 +0000 Subject: [PATCH 18/19] final refactoring --- CHANGELOG.md | 1 + src/Algebra/Properties/Group.agda | 49 +++++++++++++++---------------- src/Algebra/Properties/Loop.agda | 10 +++---- 3 files changed, 29 insertions(+), 31 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 1d8b572e54..4752c66334 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -87,6 +87,7 @@ Additions to existing modules quasigroup : Quasigroup _ _ isLoop : IsLoop _∙_ _\\_ _//_ ε loop : Loop _ _ + ⁻¹-selfInverse : SelfInverse _⁻¹ \\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_ comm⇒\\≗flip-// : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x ``` diff --git a/src/Algebra/Properties/Group.agda b/src/Algebra/Properties/Group.agda index 005f88078b..e344de66b9 100644 --- a/src/Algebra/Properties/Group.agda +++ b/src/Algebra/Properties/Group.agda @@ -11,12 +11,14 @@ open import Algebra.Bundles module Algebra.Properties.Group {g₁ g₂} (G : Group g₁ g₂) where open Group G +open import Algebra.Consequences.Setoid setoid open import Algebra.Definitions _≈_ import Algebra.Properties.Loop as LoopProperties import Algebra.Properties.Quasigroup as QuasigroupProperties open import Algebra.Structures _≈_ using (IsLoop; IsQuasigroup) open import Data.Product.Base using (_,_) open import Function.Base using (_$_) +open import Function.Definitions open import Relation.Binary.Reasoning.Setoid setoid \\-cong₂ : Congruent₂ _\\_ @@ -69,6 +71,27 @@ open QuasigroupProperties quasigroup public using (x≈z//y; y≈x\\z) renaming (cancelˡ to ∙-cancelˡ; cancelʳ to ∙-cancelʳ; cancel to ∙-cancel) +inverseˡ-unique : ∀ x y → x ∙ y ≈ ε → x ≈ y ⁻¹ +inverseˡ-unique x y eq = trans (x≈z//y x y ε eq) (identityˡ _) + +inverseʳ-unique : ∀ x y → x ∙ y ≈ ε → y ≈ x ⁻¹ +inverseʳ-unique x y eq = trans (y≈x\\z x y ε eq) (identityʳ _) + +ε⁻¹≈ε : ε ⁻¹ ≈ ε +ε⁻¹≈ε = sym $ inverseˡ-unique _ _ (identityˡ ε) + +⁻¹-selfInverse : SelfInverse _⁻¹ +⁻¹-selfInverse {x} {y} eq = sym $ inverseˡ-unique x y $ begin + x ∙ y ≈⟨ ∙-congˡ eq ⟨ + x ∙ x ⁻¹ ≈⟨ inverseʳ x ⟩ + ε ∎ + +⁻¹-involutive : Involutive _⁻¹ +⁻¹-involutive = selfInverse⇒involutive ⁻¹-selfInverse + +⁻¹-injective : Injective _≈_ _≈_ _⁻¹ +⁻¹-injective = selfInverse⇒injective ⁻¹-selfInverse + isLoop : IsLoop _∙_ _\\_ _//_ ε isLoop = record { isQuasigroup = isQuasigroup ; identity = identity } @@ -78,32 +101,6 @@ loop = record { isLoop = isLoop } open LoopProperties loop public using (identityˡ-unique; identityʳ-unique; identity-unique) -ε⁻¹≈ε : ε ⁻¹ ≈ ε -ε⁻¹≈ε = begin - ε ⁻¹ ≈⟨ identityʳ (ε ⁻¹) ⟨ - ε ⁻¹ ∙ ε ≈⟨ inverseˡ ε ⟩ - ε ∎ - -inverseˡ-unique : ∀ x y → x ∙ y ≈ ε → x ≈ y ⁻¹ -inverseˡ-unique x y eq = trans (x≈z//y x y ε eq) (identityˡ _) - -inverseʳ-unique : ∀ x y → x ∙ y ≈ ε → y ≈ x ⁻¹ -inverseʳ-unique x y eq = trans (y≈x\\z x y ε eq) (identityʳ _) - -⁻¹-involutive : ∀ x → x ⁻¹ ⁻¹ ≈ x -⁻¹-involutive x = begin - x ⁻¹ ⁻¹ ≈⟨ identityʳ _ ⟨ - x ⁻¹ ⁻¹ ∙ ε ≈⟨ ∙-congˡ $ inverseˡ _ ⟨ - x ⁻¹ ⁻¹ ∙ (x ⁻¹ ∙ x) ≈⟨ leftDividesʳ (x ⁻¹) x ⟩ - x ∎ - -⁻¹-injective : ∀ {x y} → x ⁻¹ ≈ y ⁻¹ → x ≈ y -⁻¹-injective {x} {y} eq = ∙-cancelʳ _ _ _ $ begin - x ∙ x ⁻¹ ≈⟨ inverseʳ x ⟩ - ε ≈⟨ inverseʳ y ⟨ - y ∙ y ⁻¹ ≈⟨ ∙-congˡ eq ⟨ - y ∙ x ⁻¹ ∎ - ⁻¹-anti-homo-∙ : ∀ x y → (x ∙ y) ⁻¹ ≈ y ⁻¹ ∙ x ⁻¹ ⁻¹-anti-homo-∙ x y = ∙-cancelˡ _ _ _ $ begin x ∙ y ∙ (x ∙ y) ⁻¹ ≈⟨ inverseʳ _ ⟩ diff --git a/src/Algebra/Properties/Loop.agda b/src/Algebra/Properties/Loop.agda index 69bb59ace5..46ed1e7f7c 100644 --- a/src/Algebra/Properties/Loop.agda +++ b/src/Algebra/Properties/Loop.agda @@ -18,25 +18,25 @@ open import Relation.Binary.Reasoning.Setoid setoid x//x≈ε : ∀ x → x // x ≈ ε x//x≈ε x = begin - x // x ≈⟨ //-congʳ (sym (identityˡ x)) ⟩ + x // x ≈⟨ //-congʳ (identityˡ x) ⟨ (ε ∙ x) // x ≈⟨ rightDividesʳ x ε ⟩ ε ∎ -x\\x≈ε : ∀ x → x \\ x ≈ ε +x\\x≈ε : ∀ x → x \\ x ≈ ε x\\x≈ε x = begin - x \\ x ≈⟨ \\-congˡ (sym (identityʳ x )) ⟩ + x \\ x ≈⟨ \\-congˡ (identityʳ x ) ⟨ x \\ (x ∙ ε) ≈⟨ leftDividesʳ x ε ⟩ ε ∎ ε\\x≈x : ∀ x → ε \\ x ≈ x ε\\x≈x x = begin - ε \\ x ≈⟨ sym (identityˡ (ε \\ x)) ⟩ + ε \\ x ≈⟨ identityˡ (ε \\ x) ⟨ ε ∙ (ε \\ x) ≈⟨ leftDividesˡ ε x ⟩ x ∎ x//ε≈x : ∀ x → x // ε ≈ x x//ε≈x x = begin - x // ε ≈⟨ sym (identityʳ (x // ε)) ⟩ + x // ε ≈⟨ identityʳ (x // ε) ⟨ (x // ε) ∙ ε ≈⟨ rightDividesˡ ε x ⟩ x ∎ From 25c9ed9556870352235536840e417169436a16e2 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Sat, 16 Mar 2024 10:27:06 +0800 Subject: [PATCH 19/19] Minor naming tweaks --- CHANGELOG.md | 8 ++++ src/Algebra/Properties/Group.agda | 69 +++++++++++++++++++------------ 2 files changed, 51 insertions(+), 26 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7a6c98fe95..e81c66ef5b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -106,6 +106,14 @@ Additions to existing modules quasigroup : Quasigroup _ _ isLoop : IsLoop _∙_ _\\_ _//_ ε loop : Loop _ _ + + \\-leftDividesˡ : LeftDividesˡ _∙_ _\\_ + \\-leftDividesʳ : LeftDividesʳ _∙_ _\\_ + \\-leftDivides : LeftDivides _∙_ _\\_ + //-rightDividesˡ : RightDividesˡ _∙_ _//_ + //-rightDividesʳ : RightDividesʳ _∙_ _//_ + //-rightDivides : RightDivides _∙_ _//_ + ⁻¹-selfInverse : SelfInverse _⁻¹ \\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_ comm⇒\\≗flip-// : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x diff --git a/src/Algebra/Properties/Group.agda b/src/Algebra/Properties/Group.agda index e344de66b9..3d4a7d7713 100644 --- a/src/Algebra/Properties/Group.agda +++ b/src/Algebra/Properties/Group.agda @@ -10,15 +10,16 @@ open import Algebra.Bundles module Algebra.Properties.Group {g₁ g₂} (G : Group g₁ g₂) where -open Group G -open import Algebra.Consequences.Setoid setoid -open import Algebra.Definitions _≈_ import Algebra.Properties.Loop as LoopProperties import Algebra.Properties.Quasigroup as QuasigroupProperties -open import Algebra.Structures _≈_ using (IsLoop; IsQuasigroup) open import Data.Product.Base using (_,_) open import Function.Base using (_$_) open import Function.Definitions + +open Group G +open import Algebra.Consequences.Setoid setoid +open import Algebra.Definitions _≈_ +open import Algebra.Structures _≈_ using (IsLoop; IsQuasigroup) open import Relation.Binary.Reasoning.Setoid setoid \\-cong₂ : Congruent₂ _\\_ @@ -27,41 +28,51 @@ open import Relation.Binary.Reasoning.Setoid setoid //-cong₂ : Congruent₂ _//_ //-cong₂ x≈y u≈v = ∙-cong x≈y (⁻¹-cong u≈v) -leftDividesˡ : ∀ x y → x ∙ (x \\ y) ≈ y -leftDividesˡ x y = begin +------------------------------------------------------------------------ +-- Groups are quasi-groups + +\\-leftDividesˡ : LeftDividesˡ _∙_ _\\_ +\\-leftDividesˡ x y = begin x ∙ (x \\ y) ≈⟨ assoc x (x ⁻¹) y ⟨ x ∙ x ⁻¹ ∙ y ≈⟨ ∙-congʳ (inverseʳ x) ⟩ ε ∙ y ≈⟨ identityˡ y ⟩ y ∎ -leftDividesʳ : ∀ x y → x \\ x ∙ y ≈ y -leftDividesʳ x y = begin +\\-leftDividesʳ : LeftDividesʳ _∙_ _\\_ +\\-leftDividesʳ x y = begin x \\ x ∙ y ≈⟨ assoc (x ⁻¹) x y ⟨ x ⁻¹ ∙ x ∙ y ≈⟨ ∙-congʳ (inverseˡ x) ⟩ ε ∙ y ≈⟨ identityˡ y ⟩ y ∎ -rightDividesˡ : ∀ x y → (y // x) ∙ x ≈ y -rightDividesˡ x y = begin + +\\-leftDivides : LeftDivides _∙_ _\\_ +\\-leftDivides = \\-leftDividesˡ , \\-leftDividesʳ + +//-rightDividesˡ : RightDividesˡ _∙_ _//_ +//-rightDividesˡ x y = begin (y // x) ∙ x ≈⟨ assoc y (x ⁻¹) x ⟩ y ∙ (x ⁻¹ ∙ x) ≈⟨ ∙-congˡ (inverseˡ x) ⟩ y ∙ ε ≈⟨ identityʳ y ⟩ y ∎ -rightDividesʳ : ∀ x y → y ∙ x // x ≈ y -rightDividesʳ x y = begin +//-rightDividesʳ : RightDividesʳ _∙_ _//_ +//-rightDividesʳ x y = begin y ∙ x // x ≈⟨ assoc y x (x ⁻¹) ⟩ y ∙ (x // x) ≈⟨ ∙-congˡ (inverseʳ x) ⟩ y ∙ ε ≈⟨ identityʳ y ⟩ y ∎ +//-rightDivides : RightDivides _∙_ _//_ +//-rightDivides = //-rightDividesˡ , //-rightDividesʳ + isQuasigroup : IsQuasigroup _∙_ _\\_ _//_ isQuasigroup = record { isMagma = isMagma ; \\-cong = \\-cong₂ ; //-cong = //-cong₂ - ; leftDivides = leftDividesˡ , leftDividesʳ - ; rightDivides = rightDividesˡ , rightDividesʳ + ; leftDivides = \\-leftDivides + ; rightDivides = //-rightDivides } quasigroup : Quasigroup _ _ @@ -71,6 +82,21 @@ open QuasigroupProperties quasigroup public using (x≈z//y; y≈x\\z) renaming (cancelˡ to ∙-cancelˡ; cancelʳ to ∙-cancelʳ; cancel to ∙-cancel) +------------------------------------------------------------------------ +-- Groups are loops + +isLoop : IsLoop _∙_ _\\_ _//_ ε +isLoop = record { isQuasigroup = isQuasigroup ; identity = identity } + +loop : Loop _ _ +loop = record { isLoop = isLoop } + +open LoopProperties loop public + using (identityˡ-unique; identityʳ-unique; identity-unique) + +------------------------------------------------------------------------ +-- Other properties + inverseˡ-unique : ∀ x y → x ∙ y ≈ ε → x ≈ y ⁻¹ inverseˡ-unique x y eq = trans (x≈z//y x y ε eq) (identityˡ _) @@ -92,29 +118,20 @@ inverseʳ-unique x y eq = trans (y≈x\\z x y ε eq) (identityʳ _) ⁻¹-injective : Injective _≈_ _≈_ _⁻¹ ⁻¹-injective = selfInverse⇒injective ⁻¹-selfInverse -isLoop : IsLoop _∙_ _\\_ _//_ ε -isLoop = record { isQuasigroup = isQuasigroup ; identity = identity } - -loop : Loop _ _ -loop = record { isLoop = isLoop } - -open LoopProperties loop public - using (identityˡ-unique; identityʳ-unique; identity-unique) - ⁻¹-anti-homo-∙ : ∀ x y → (x ∙ y) ⁻¹ ≈ y ⁻¹ ∙ x ⁻¹ ⁻¹-anti-homo-∙ x y = ∙-cancelˡ _ _ _ $ begin x ∙ y ∙ (x ∙ y) ⁻¹ ≈⟨ inverseʳ _ ⟩ ε ≈⟨ inverseʳ _ ⟨ - x ∙ x ⁻¹ ≈⟨ ∙-congʳ (rightDividesʳ y x) ⟨ + x ∙ x ⁻¹ ≈⟨ ∙-congʳ (//-rightDividesʳ y x) ⟨ (x ∙ y) ∙ y ⁻¹ ∙ x ⁻¹ ≈⟨ assoc (x ∙ y) (y ⁻¹) (x ⁻¹) ⟩ x ∙ y ∙ (y ⁻¹ ∙ x ⁻¹) ∎ \\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_ \\≗flip-//⇒comm \\≗//ᵒ x y = begin - x ∙ y ≈⟨ ∙-congˡ (rightDividesˡ x y) ⟨ + x ∙ y ≈⟨ ∙-congˡ (//-rightDividesˡ x y) ⟨ x ∙ ((y // x) ∙ x) ≈⟨ ∙-congˡ (∙-congʳ (\\≗//ᵒ x y)) ⟨ x ∙ ((x \\ y) ∙ x) ≈⟨ assoc x (x \\ y) x ⟨ - x ∙ (x \\ y) ∙ x ≈⟨ ∙-congʳ (leftDividesˡ x y) ⟩ + x ∙ (x \\ y) ∙ x ≈⟨ ∙-congʳ (\\-leftDividesˡ x y) ⟩ y ∙ x ∎ comm⇒\\≗flip-// : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x