Add new operations (cf. RawQuasigroup) to IsGroup

CHANGELOG.md

@@ -41,6 +41,11 @@ Deprecated names
   1×-identityʳ  ↦  ×-homo-1
   ```
 
+* In `Algebra.Structures.IsGroup`:
+  ```agda
+  _-_  ↦  _//_
+  ```
+
 * In `Data.Nat.Divisibility.Core`:
   ```agda
   *-pres-∣  ↦  Data.Nat.Divisibility.*-pres-∣
@@ -135,6 +140,32 @@ Additions to existing modules
   rawModule          : RawModule R c ℓ
   ```
 
+* In `Algebra.Properties.Group`:
+  ```agda
+  isQuasigroup    : IsQuasigroup _∙_ _\\_ _//_
+  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
+  ```
+
+* In `Algebra.Properties.Loop`:
+  ```agda
+  identityˡ-unique : x ∙ y ≈ y → x ≈ ε
+  identityʳ-unique : x ∙ y ≈ x → y ≈ ε
+  identity-unique  : Identity x _∙_ → x ≈ ε
+  ```
+
 * In `Algebra.Construct.Terminal`:
   ```agda
   rawNearSemiring : RawNearSemiring c ℓ
@@ -154,6 +185,16 @@ Additions to existing modules
   idem-×-homo-* : (_*_ IdempotentOn x) → (m × x) * (n × x) ≈ (m ℕ.* n) × x
   ```
 
+* In `Algebra.Structures.IsGroup`:
+  ```agda
+  infixl 6 _//_
+  _//_ : Op₂ A
+  x // y = x ∙ (y ⁻¹)
+  infixr 6 _\\_
+  _\\_ : Op₂ A
+  x \\ y = (x ⁻¹) ∙ y
+  ```
+
 * In `Data.Container.Indexed.Core`:
   ```agda
   Subtrees o c = (r : Response c) → X (next c r)

src/Algebra/Properties/Group.agda

@@ -10,99 +10,133 @@ open import Algebra.Bundles
 
 module Algebra.Properties.Group {g₁ g₂} (G : Group g₁ g₂) where
 
+import Algebra.Properties.Loop as LoopProperties
+import Algebra.Properties.Quasigroup as QuasigroupProperties
+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
-open import Function.Base using (_$_; _⟨_⟩_)
-open import Data.Product.Base using (_,_; proj₂)
 
-ε⁻¹≈ε : ε ⁻¹ ≈ ε
-ε⁻¹≈ε = begin
-  ε ⁻¹      ≈⟨ sym $ identityʳ (ε ⁻¹) ⟩
-  ε ⁻¹ ∙ ε  ≈⟨ inverseˡ ε ⟩
-  ε         ∎
-
-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 ⁻¹ ∎
-
-  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) ∎
-
-∙-cancelˡ : LeftCancellative _∙_
-∙-cancelˡ x y z eq = begin
-              y  ≈⟨ right-helper x y ⟩
-  x ⁻¹ ∙ (x ∙ y) ≈⟨ ∙-congˡ eq ⟩
-  x ⁻¹ ∙ (x ∙ z) ≈⟨ right-helper x z ⟨
-              z  ∎
-
-∙-cancelʳ : RightCancellative _∙_
-∙-cancelʳ x y z eq = begin
-  y            ≈⟨ left-helper y x ⟩
-  y ∙ x ∙ x ⁻¹ ≈⟨ ∙-congʳ eq ⟩
-  z ∙ x ∙ x ⁻¹ ≈⟨ left-helper z x ⟨
-  z            ∎
-
-∙-cancel : Cancellative _∙_
-∙-cancel = ∙-cancelˡ , ∙-cancelʳ
-
-⁻¹-involutive : ∀ x → x ⁻¹ ⁻¹ ≈ x
-⁻¹-involutive x = begin
-  x ⁻¹ ⁻¹              ≈⟨ identityʳ _ ⟨
-  x ⁻¹ ⁻¹ ∙ ε          ≈⟨ ∙-congˡ $ inverseˡ _ ⟨
-  x ⁻¹ ⁻¹ ∙ (x ⁻¹ ∙ x) ≈⟨ right-helper (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 ⁻¹ ∎ )
+\\-cong₂ : Congruent₂ _\\_
+\\-cong₂ x≈y u≈v = ∙-cong (⁻¹-cong x≈y) u≈v
 
-⁻¹-anti-homo-∙ : ∀ x y → (x ∙ y) ⁻¹ ≈ y ⁻¹ ∙ x ⁻¹
-⁻¹-anti-homo-∙ x y = ∙-cancelˡ _ _ _ ( begin
-  x ∙ y ∙ (x ∙ y) ⁻¹    ≈⟨ inverseʳ _ ⟩
-  ε                     ≈⟨ inverseʳ _ ⟨
-  x ∙ x ⁻¹              ≈⟨ ∙-congʳ (left-helper x y) ⟩
-  (x ∙ y) ∙ y ⁻¹ ∙ x ⁻¹ ≈⟨ assoc (x ∙ y) (y ⁻¹) (x ⁻¹) ⟩
-  x ∙ y ∙ (y ⁻¹ ∙ x ⁻¹) ∎ )
+//-cong₂ : Congruent₂ _//_
+//-cong₂ x≈y u≈v = ∙-cong x≈y (⁻¹-cong u≈v)
+
+------------------------------------------------------------------------
+-- 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ʳ : LeftDividesʳ _∙_ _\\_
+\\-leftDividesʳ x y = begin
+  x \\ x ∙ y     ≈⟨ assoc (x ⁻¹) x y ⟨
+  x ⁻¹ ∙ x ∙ y   ≈⟨ ∙-congʳ (inverseˡ x) ⟩
+  ε ∙ y          ≈⟨ identityˡ y ⟩
+  y              ∎
+
+
+\\-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ʳ : 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
+  ; rightDivides = //-rightDivides
+  }
+
+quasigroup : Quasigroup _ _
+quasigroup = record { isQuasigroup = isQuasigroup }
+
+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 }
 
-identityˡ-unique : ∀ x y → x ∙ y ≈ y → x ≈ ε
-identityˡ-unique x y eq = begin
-  x              ≈⟨ left-helper x y ⟩
-  (x ∙ y) ∙ y ⁻¹ ≈⟨ ∙-congʳ eq ⟩
-       y  ∙ y ⁻¹ ≈⟨ inverseʳ y ⟩
-  ε              ∎
+loop : Loop _ _
+loop = record { isLoop = isLoop }
 
-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 ⟩
-  x ⁻¹ ∙  x      ≈⟨ inverseˡ x ⟩
-  ε              ∎
+open LoopProperties loop public
+  using (identityˡ-unique; identityʳ-unique; identity-unique)
 
-identity-unique : ∀ {x} → Identity x _∙_ → x ≈ ε
-identity-unique {x} id = identityˡ-unique x x (proj₂ id x)
+------------------------------------------------------------------------
+-- Other properties
 
 inverseˡ-unique : ∀ x y → x ∙ y ≈ ε → x ≈ y ⁻¹
-inverseˡ-unique x y eq = begin
-  x              ≈⟨ left-helper x y ⟩
-  (x ∙ y) ∙ y ⁻¹ ≈⟨ ∙-congʳ eq ⟩
-       ε  ∙ y ⁻¹ ≈⟨ identityˡ (y ⁻¹) ⟩
-            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 = begin
-  y       ≈⟨ sym (⁻¹-involutive y) ⟩
-  y ⁻¹ ⁻¹ ≈⟨ ⁻¹-cong (sym (inverseˡ-unique x y eq)) ⟩
-  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
+
+⁻¹-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 ∙ 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 // 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⇒\\≗flip-// : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x
+comm⇒\\≗flip-// comm x y = begin
+  x \\ y    ≡⟨⟩
+  x ⁻¹ ∙ y  ≈⟨ comm _ _ ⟩
+  y ∙ x ⁻¹  ≡⟨⟩
+  y // x    ∎

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,29 +12,46 @@ module Algebra.Properties.Loop {l₁ l₂} (L : Loop l₁ l₂) where
 
 open Loop L
 open import Algebra.Definitions _≈_
+open import Algebra.Properties.Quasigroup quasigroup
+open import Data.Product.Base using (proj₂)
 open import Relation.Binary.Reasoning.Setoid setoid
-open import Algebra.Properties.Quasigroup
 
 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            ∎
+
+identityˡ-unique : ∀ x y → x ∙ y ≈ y → x ≈ ε
+identityˡ-unique x y eq = begin
+  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       ≈⟨ 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)
+

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       ∎