Add new operations (cf. RawQuasigroup) to IsGroup

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-∣
@@ -76,6 +81,34 @@ Additions to existing modules
   rawModule          : RawModule R c ℓ
   ```
 
+* In `Algebra.Properties.Group`:
+  ```agda
+  isQuasigroup    : IsQuasigroup _∙_ _\\_ _//_
+  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
+  ```
+
+* 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 _//_
+  _//_ : Op₂ A
+  x // y = x ∙ (y ⁻¹)
+  infixr 6 _\\_
+  _\\_ : Op₂ A
+  x \\ y = (x ⁻¹) ∙ y
+  ```
+
 * In `Data.Fin.Properties`:
   ```agda
   nonZeroIndex : Fin n → ℕ.NonZero n

src/Algebra/Properties/Group.agda

@@ -11,98 +11,115 @@ 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
-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 ⟨
+  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 = \\-cong₂
+  ; //-cong = //-cong₂
+  ; leftDivides = leftDividesˡ , leftDividesʳ
+  ; rightDivides = 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)
+
+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ʳ _)
 
 ε⁻¹≈ε : ε ⁻¹ ≈ ε
-ε⁻¹≈ε = 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 ⁻¹ ∎ )
+ε⁻¹≈ε = sym $ inverseˡ-unique _ _ (identityˡ ε)
 
-⁻¹-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 ⁻¹) ∎ )
+⁻¹-selfInverse : SelfInverse _⁻¹
+⁻¹-selfInverse {x} {y} eq = sym $ inverseˡ-unique x y $ begin
+  x ∙ y    ≈⟨ ∙-congˡ eq ⟨
+  x ∙ x ⁻¹ ≈⟨ inverseʳ x  ⟩
+  ε        ∎
 
-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 ⟩
-  ε              ∎
+⁻¹-involutive : Involutive _⁻¹
+⁻¹-involutive = selfInverse⇒involutive ⁻¹-selfInverse
 
-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 ⟩
-  ε              ∎
+⁻¹-injective : Injective _≈_ _≈_ _⁻¹
+⁻¹-injective = selfInverse⇒injective ⁻¹-selfInverse
 
-identity-unique : ∀ {x} → Identity x _∙_ → x ≈ ε
-identity-unique {x} id = identityˡ-unique x x (proj₂ id x)
+isLoop : IsLoop _∙_ _\\_ _//_ ε
+isLoop = record { isQuasigroup = isQuasigroup ; identity = identity }
 
-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 ⁻¹ ∎
+loop : Loop _ _
+loop = record { isLoop = isLoop }
 
-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 ⁻¹    ∎
+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 ∙ 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       ∎

src/Algebra/Structures.agda

@@ -253,9 +253,22 @@ record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) w
 
   open IsMonoid isMonoid public
 
+  infixr 6 _\\_
+  _\\_ : Op₂ A
+  x \\ y = (x ⁻¹) ∙ y
+
+  infixl 6 _//_
+  _//_ : Op₂ A
+  x // y = x ∙ (y ⁻¹)
+
+  -- Deprecated.
   infixl 6 _-_
   _-_ : Op₂ A
-  x - y = x ∙ (y ⁻¹)
+  _-_ = _//_
+  {-# WARNING_ON_USAGE _-_
+  "Warning: _-_ was deprecated in v2.1.
+  Please use _//_ instead. "
+  #-}
 
   inverseˡ : LeftInverse ε _⁻¹ _∙_
   inverseˡ = proj₁ inverse
@@ -291,7 +304,7 @@ record IsAbelianGroup (∙ : Op₂ A)
     isGroup : IsGroup ∙ ε ⁻¹
     comm    : Commutative ∙
 
-  open IsGroup isGroup public
+  open IsGroup isGroup public renaming (_//_ to _-_) hiding (_\\_; _-_)
 
   isCommutativeMonoid : IsCommutativeMonoid ∙ ε
   isCommutativeMonoid = record