Add Quasigroup and Loop morphisms (#1647)

Author: Akshobhya1234

CHANGELOG.md

@@ -652,6 +652,16 @@ Other minor changes
   ```
   and their corresponding algebraic substructures.
 
+* Added new records to `Algebra.Morphism.Structures`:
+  ```agda
+  record IsQuasigroupHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂)
+  record IsQuasigroupMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂)
+  record IsQuasigroupIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
+  record IsLoopHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂)
+  record IsLoopMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂)
+  record IsLoopIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) 
+  ```
+
 * Added new functions in `Data.Fin.Base`:
   ```
   finToFun  : Fin (n ^ m) → (Fin m → Fin n)

src/Algebra/Bundles.agda

@@ -886,7 +886,7 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
 -- Bundles with 3 binary operations
 ------------------------------------------------------------------------
 
-record RawQuasiGroup c ℓ : Set (suc (c ⊔ ℓ)) where
+record RawQuasigroup c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _∙_
   infixl 7 _\\_
   infixl 7 _//_
@@ -934,15 +934,15 @@ record Quasigroup c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open IsQuasigroup isQuasigroup public
 
-  rawQuasiGroup : RawQuasiGroup c ℓ
-  rawQuasiGroup = record
+  rawQuasigroup : RawQuasigroup c ℓ
+  rawQuasigroup = record
     { _≈_  = _≈_
     ; _∙_  = _∙_
     ; _\\_  = _\\_
     ; _//_  = _//_
     }
 
-  open RawQuasiGroup rawQuasiGroup public
+  open RawQuasigroup rawQuasigroup public
     using (_≈_; //-rawMagma; \\-rawMagma; ∙-rawMagma)
 
   setoid : Setoid _ _
@@ -964,15 +964,15 @@ record RawLoop  c ℓ : Set (suc (c ⊔ ℓ)) where
     _//_    : Op₂ Carrier
     ε       : Carrier
 
-  rawQuasiGroup : RawQuasiGroup c ℓ
-  rawQuasiGroup = record
+  rawQuasigroup : RawQuasigroup c ℓ
+  rawQuasigroup = record
     { _≈_ = _≈_
     ; _∙_ = _∙_
     ; _\\_ = _\\_
     ; _//_ = _//_
     }
 
-  open RawQuasiGroup rawQuasiGroup public
+  open RawQuasigroup rawQuasigroup public
     using (_≉_ ; ∙-rawMagma; \\-rawMagma; //-rawMagma)
 
 record Loop  c ℓ : Set (suc (c ⊔ ℓ)) where

src/Algebra/Morphism/Structures.agda

@@ -464,6 +464,149 @@ module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where
       using ()
       renaming (isMagmaIsomorphism to *-isMagmaIsomorphisn)
 
+------------------------------------------------------------------------
+-- Morphisms over quasigroup-like structures
+------------------------------------------------------------------------
+module QuasigroupMorphisms (Q₁ : RawQuasigroup a ℓ₁) (Q₂ : RawQuasigroup b ℓ₂) where
+
+  open RawQuasigroup Q₁ renaming (Carrier to A; ∙-rawMagma to ∙-rawMagma₁;
+                                  \\-rawMagma to \\-rawMagma₁; //-rawMagma to //-rawMagma₁;
+                                  _≈_ to _≈₁_; _∙_ to _∙₁_; _\\_ to _\\₁_; _//_ to _//₁_)
+  open RawQuasigroup Q₂ renaming (Carrier to B; ∙-rawMagma to ∙-rawMagma₂;
+                                  \\-rawMagma to \\-rawMagma₂; //-rawMagma to //-rawMagma₂;
+                                  _≈_ to _≈₂_; _∙_ to _∙₂_; _\\_ to _\\₂_; _//_ to _//₂_)
+
+  module ∙  = MagmaMorphisms ∙-rawMagma₁ ∙-rawMagma₂
+  module \\ = MagmaMorphisms \\-rawMagma₁ \\-rawMagma₂
+  module // = MagmaMorphisms //-rawMagma₁ //-rawMagma₂
+
+  open MorphismDefinitions A B _≈₂_
+  open FunctionDefinitions _≈₁_ _≈₂_
+
+  record IsQuasigroupHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧
+      ∙-homo            : Homomorphic₂ ⟦_⟧ _∙₁_ _∙₂_
+      \\-homo           : Homomorphic₂ ⟦_⟧ _\\₁_ _\\₂_
+      //-homo           : Homomorphic₂ ⟦_⟧ _//₁_ _//₂_
+
+    open IsRelHomomorphism isRelHomomorphism public
+      renaming (cong to ⟦⟧-cong)
+
+    ∙-isMagmaHomomorphism : ∙.IsMagmaHomomorphism ⟦_⟧
+    ∙-isMagmaHomomorphism = record
+      { isRelHomomorphism = isRelHomomorphism
+      ; homo = ∙-homo
+      }
+
+    \\-isMagmaHomomorphism : \\.IsMagmaHomomorphism ⟦_⟧
+    \\-isMagmaHomomorphism = record
+      { isRelHomomorphism  = isRelHomomorphism
+      ; homo = \\-homo
+      }
+
+    //-isMagmaHomomorphism : //.IsMagmaHomomorphism ⟦_⟧
+    //-isMagmaHomomorphism = record
+      { isRelHomomorphism  = isRelHomomorphism
+      ; homo = //-homo
+      }
+
+  record IsQuasigroupMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      isQuasigroupHomomorphism : IsQuasigroupHomomorphism ⟦_⟧
+      injective                : Injective ⟦_⟧
+
+    open IsQuasigroupHomomorphism isQuasigroupHomomorphism public
+
+
+    ∙-isMagmaMonomorphism   : ∙.IsMagmaMonomorphism ⟦_⟧
+    ∙-isMagmaMonomorphism   = record
+      { isMagmaHomomorphism = ∙-isMagmaHomomorphism
+      ; injective           = injective
+      }
+
+    \\-isMagmaMonomorphism  : \\.IsMagmaMonomorphism ⟦_⟧
+    \\-isMagmaMonomorphism  = record
+      { isMagmaHomomorphism = \\-isMagmaHomomorphism
+      ; injective           = injective
+      }
+
+    //-isMagmaMonomorphism  : //.IsMagmaMonomorphism ⟦_⟧
+    //-isMagmaMonomorphism  = record
+      { isMagmaHomomorphism = //-isMagmaHomomorphism
+      ; injective           = injective
+      }
+
+    open //.IsMagmaMonomorphism //-isMagmaMonomorphism public
+      using (isRelMonomorphism)
+
+
+  record IsQuasigroupIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      isQuasigroupMonomorphism : IsQuasigroupMonomorphism ⟦_⟧
+      surjective               : Surjective ⟦_⟧
+
+    open IsQuasigroupMonomorphism isQuasigroupMonomorphism public
+
+    ∙-isMagmaIsomorphism    : ∙.IsMagmaIsomorphism ⟦_⟧
+    ∙-isMagmaIsomorphism    = record
+      { isMagmaMonomorphism = ∙-isMagmaMonomorphism
+      ; surjective          = surjective
+      }
+
+    \\-isMagmaIsomorphism   : \\.IsMagmaIsomorphism ⟦_⟧
+    \\-isMagmaIsomorphism   = record
+      { isMagmaMonomorphism = \\-isMagmaMonomorphism
+      ; surjective          = surjective
+      }
+
+    //-isMagmaIsomorphism   : //.IsMagmaIsomorphism ⟦_⟧
+    //-isMagmaIsomorphism   = record
+      { isMagmaMonomorphism = //-isMagmaMonomorphism
+      ; surjective          = surjective
+      }
+
+    open //.IsMagmaIsomorphism //-isMagmaIsomorphism public
+      using (isRelIsomorphism)
+
+------------------------------------------------------------------------
+-- Morphisms over loop-like structures
+------------------------------------------------------------------------
+
+module LoopMorphisms (L₁ : RawLoop a ℓ₁) (L₂ : RawLoop b ℓ₂) where
+
+  open RawLoop L₁ renaming (Carrier to A; ∙-rawMagma to ∙-rawMagma₁;
+                            \\-rawMagma to \\-rawMagma₁; //-rawMagma to //-rawMagma₁;
+                             _≈_ to _≈₁_; _∙_ to _∙₁_; _\\_ to _\\₁_; _//_ to _//₁_; ε to ε₁)
+  open RawLoop L₂ renaming (Carrier to B; ∙-rawMagma to ∙-rawMagma₂;
+                            \\-rawMagma to \\-rawMagma₂; //-rawMagma to //-rawMagma₂;
+                            _≈_ to _≈₂_; _∙_ to _∙₂_; _\\_ to _\\₂_; _//_ to _//₂_ ; ε to ε₂)
+  open MorphismDefinitions A B _≈₂_
+  open FunctionDefinitions _≈₁_ _≈₂_
+
+  open QuasigroupMorphisms (RawLoop.rawQuasigroup L₁) (RawLoop.rawQuasigroup L₂)
+
+  record IsLoopHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      isQuasigroupHomomorphism : IsQuasigroupHomomorphism ⟦_⟧
+      ε-homo                   : Homomorphic₀ ⟦_⟧ ε₁ ε₂
+
+    open IsQuasigroupHomomorphism isQuasigroupHomomorphism public
+
+  record IsLoopMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      isLoopHomomorphism   : IsLoopHomomorphism ⟦_⟧
+      injective            : Injective ⟦_⟧
+
+    open IsLoopHomomorphism isLoopHomomorphism public
+
+  record IsLoopIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      isLoopMonomorphism   : IsLoopMonomorphism ⟦_⟧
+      surjective           : Surjective ⟦_⟧
+
+    open IsLoopMonomorphism isLoopMonomorphism public
+
 ------------------------------------------------------------------------
 -- Re-export contents of modules publicly
 
@@ -473,3 +616,5 @@ open GroupMorphisms public
 open NearSemiringMorphisms public
 open SemiringMorphisms public
 open RingMorphisms public
+open QuasigroupMorphisms public
+open LoopMorphisms public