added Pointed algebraic structure, (raw) bundle and homomorphism

CHANGELOG.md

@@ -835,6 +835,8 @@ Major improvements
   * `RawRing`
   * `RawQuasigroup`
   * `RawLoop`
+* A new definition is also introduced: 
+  *  `RawPointed`
 * A new module `Algebra.Lattice.Bundles.Raw` is also introduced.
   * `RawLattice` has been moved from `Algebra.Lattice.Bundles` to this new module.
 
@@ -1563,6 +1565,7 @@ Other minor changes
 
 * Added new definitions to `Algebra.Bundles`:
   ```agda
+  record Pointed c ℓ : Set (suc (c ⊔ ℓ))
   record UnitalMagma c ℓ : Set (suc (c ⊔ ℓ))
   record InvertibleMagma c ℓ : Set (suc (c ⊔ ℓ))
   record InvertibleUnitalMagma c ℓ : Set (suc (c ⊔ ℓ))
@@ -1756,6 +1759,7 @@ Other minor changes
 
 * Added new definitions to `Algebra.Structures`:
   ```agda
+  record IsPointed (e : A) : Set (a ⊔ ℓ)
   record IsUnitalMagma (_∙_ : Op₂ A) (ε : A) : Set (a ⊔ ℓ)
   record IsInvertibleMagma (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ)
   record IsInvertibleUnitalMagma (_∙_ : Op₂ A) (ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ)
@@ -1786,6 +1790,9 @@ Other minor changes
 
 * Added new records to `Algebra.Morphism.Structures`:
   ```agda
+  record IsPointedHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂)
+  record IsPointedMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂)
+  record IsPointedIsomorphism  (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
   record IsQuasigroupHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂)
   record IsQuasigroupMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂)
   record IsQuasigroupIsomorphism  (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)

src/Algebra/Bundles.agda

@@ -23,11 +23,31 @@ open import Level
 -- Re-export definitions of 'raw' bundles
 
 open Raw public
-  using (RawMagma; RawMonoid; RawGroup
+  using (RawPointed; RawMagma; RawMonoid; RawGroup
         ; RawNearSemiring; RawSemiring
         ; RawRingWithoutOne; RawRing
         ; RawQuasigroup; RawLoop)
 
+------------------------------------------------------------------------
+-- Bundles with 1 element
+------------------------------------------------------------------------
+
+record Pointed c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  4 _≈_
+  field
+    Carrier   : Set c
+    _≈_       : Rel Carrier ℓ
+    pt₀       : Carrier
+    isPointed : IsPointed _≈_ pt₀
+
+  open IsPointed isPointed public
+
+  rawPointed : RawPointed _ _
+  rawPointed = record { _≈_ = _≈_; pt₀ = pt₀ }
+
+  open RawPointed rawPointed public
+    using (_≉_)
+
 ------------------------------------------------------------------------
 -- Bundles with 1 binary operation
 ------------------------------------------------------------------------

src/Algebra/Bundles/Raw.agda

@@ -17,6 +17,21 @@ open import Relation.Nullary.Negation.Core using (¬_)
 -- Raw bundles with 1 binary operation
 ------------------------------------------------------------------------
 
+record RawPointed c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  4 _≈_
+  field
+    Carrier : Set c
+    _≈_     : Rel Carrier ℓ
+    pt₀     : Carrier
+
+  infix 4 _≉_
+  _≉_ : Rel Carrier _
+  x ≉ y = ¬ (x ≈ y)
+
+------------------------------------------------------------------------
+-- Raw bundles with 1 binary operation
+------------------------------------------------------------------------
+
 record RawMagma c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _∙_
   infix  4 _≈_

src/Algebra/Morphism/Construct/Composition.agda

@@ -21,6 +21,46 @@ private
   variable
     a b c ℓ₁ ℓ₂ ℓ₃ : Level
 
+------------------------------------------------------------------------
+-- Pointeds
+
+module _ {P₁ : RawPointed a ℓ₁}
+         {P₂ : RawPointed b ℓ₂}
+         {P₃ : RawPointed c ℓ₃}
+         (open RawPointed)
+         (≈₃-trans : Transitive (_≈_ P₃))
+         {f : Carrier P₁ → Carrier P₂}
+         {g : Carrier P₂ → Carrier P₃}
+         where
+
+  isPointedHomomorphism
+    : IsPointedHomomorphism P₁ P₂ f
+    → IsPointedHomomorphism P₂ P₃ g
+    → IsPointedHomomorphism P₁ P₃ (g ∘ f)
+  isPointedHomomorphism f-homo g-homo = record
+    { isRelHomomorphism = isRelHomomorphism F.isRelHomomorphism G.isRelHomomorphism
+    ; homo              = ≈₃-trans (G.⟦⟧-cong F.homo) G.homo
+    } where module F = IsPointedHomomorphism f-homo; module G = IsPointedHomomorphism g-homo
+
+  isPointedMonomorphism
+    : IsPointedMonomorphism P₁ P₂ f
+    → IsPointedMonomorphism P₂ P₃ g
+    → IsPointedMonomorphism P₁ P₃ (g ∘ f)
+  isPointedMonomorphism f-mono g-mono = record
+    { isPointedHomomorphism = isPointedHomomorphism F.isPointedHomomorphism G.isPointedHomomorphism
+    ; injective           = F.injective ∘ G.injective
+    } where module F = IsPointedMonomorphism f-mono; module G = IsPointedMonomorphism g-mono
+
+  isPointedIsomorphism
+    : IsPointedIsomorphism P₁ P₂ f
+    → IsPointedIsomorphism P₂ P₃ g
+    → IsPointedIsomorphism P₁ P₃ (g ∘ f)
+  isPointedIsomorphism f-iso g-iso = record
+    { isPointedMonomorphism = isPointedMonomorphism F.isPointedMonomorphism G.isPointedMonomorphism
+    ; surjective          = Func.surjective (_≈_ P₁) _ _ ≈₃-trans G.⟦⟧-cong F.surjective G.surjective
+    } where module F = IsPointedIsomorphism f-iso; module G = IsPointedIsomorphism g-iso
+
+
 ------------------------------------------------------------------------
 -- Magmas
 

src/Algebra/Morphism/Construct/Identity.agda

@@ -10,7 +10,8 @@ module Algebra.Morphism.Construct.Identity where
 
 open import Algebra.Bundles
 open import Algebra.Morphism.Structures
-  using ( module MagmaMorphisms
+  using ( module PointedMorphisms
+        ; module MagmaMorphisms
         ; module MonoidMorphisms
         ; module GroupMorphisms
         ; module NearSemiringMorphisms
@@ -30,6 +31,30 @@ private
   variable
     c ℓ : Level
 
+------------------------------------------------------------------------
+-- Pointeds
+
+module _ (P : RawPointed c ℓ) (open RawPointed P) (refl : Reflexive _≈_) where
+  open PointedMorphisms P P
+
+  isPointedHomomorphism : IsPointedHomomorphism id
+  isPointedHomomorphism = record
+    { isRelHomomorphism = isRelHomomorphism _
+    ; homo              = refl
+    }
+
+  isPointedMonomorphism : IsPointedMonomorphism id
+  isPointedMonomorphism = record
+    { isPointedHomomorphism = isPointedHomomorphism
+    ; injective = id
+    }
+
+  isPointedIsomorphism : IsPointedIsomorphism id
+  isPointedIsomorphism = record
+    { isPointedMonomorphism = isPointedMonomorphism
+    ; surjective = _, refl
+    }
+
 ------------------------------------------------------------------------
 -- Magmas
 

src/Algebra/Morphism/Structures.agda

@@ -21,6 +21,55 @@ private
   variable
     a b ℓ₁ ℓ₂ : Level
 
+------------------------------------------------------------------------
+-- Morphisms over pointed structures
+------------------------------------------------------------------------
+
+module PointedMorphisms (P₁ : RawPointed a ℓ₁) (P₂ : RawPointed b ℓ₂) where
+
+  open RawPointed P₁ renaming (Carrier to A; _≈_ to _≈₁_; pt₀ to pt₁)
+  open RawPointed P₂ renaming (Carrier to B; _≈_ to _≈₂_; pt₀ to pt₂)
+  open MorphismDefinitions A B _≈₂_
+  open FunctionDefinitions _≈₁_ _≈₂_
+
+
+  record IsPointedHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧
+      homo              : Homomorphic₀ ⟦_⟧ pt₁ pt₂
+
+    open IsRelHomomorphism isRelHomomorphism public
+      renaming (cong to ⟦⟧-cong)
+
+  record IsPointedMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      isPointedHomomorphism : IsPointedHomomorphism ⟦_⟧
+      injective             : Injective ⟦_⟧
+
+    open IsPointedHomomorphism isPointedHomomorphism public
+
+    isRelMonomorphism : IsRelMonomorphism _≈₁_ _≈₂_ ⟦_⟧
+    isRelMonomorphism = record
+      { isHomomorphism = isRelHomomorphism
+      ; injective      = injective
+      }
+
+
+  record IsPointedIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      isPointedMonomorphism : IsPointedMonomorphism ⟦_⟧
+      surjective          : Surjective ⟦_⟧
+
+    open IsPointedMonomorphism isPointedMonomorphism public
+
+    isRelIsomorphism : IsRelIsomorphism _≈₁_ _≈₂_ ⟦_⟧
+    isRelIsomorphism = record
+      { isMonomorphism = isRelMonomorphism
+      ; surjective     = surjective
+      }
+
+
+
 ------------------------------------------------------------------------
 -- Morphisms over magma-like structures
 ------------------------------------------------------------------------
@@ -697,6 +746,7 @@ module LoopMorphisms (L₁ : RawLoop a ℓ₁) (L₂ : RawLoop b ℓ₂) where
 ------------------------------------------------------------------------
 -- Re-export contents of modules publicly
 
+open PointedMorphisms public
 open MagmaMorphisms public
 open MonoidMorphisms public
 open GroupMorphisms public

src/Algebra/Structures.agda

@@ -25,6 +25,19 @@ import Algebra.Consequences.Setoid as Consequences
 open import Data.Product using (_,_; proj₁; proj₂)
 open import Level using (_⊔_)
 
+------------------------------------------------------------------------
+-- Structures with 1 element
+------------------------------------------------------------------------
+
+record IsPointed (e : A) : Set (a ⊔ ℓ) where
+  field
+    isEquivalence : IsEquivalence _≈_
+
+  open IsEquivalence isEquivalence public
+
+  setoid : Setoid a ℓ
+  setoid = record { isEquivalence = isEquivalence }
+
 ------------------------------------------------------------------------
 -- Structures with 1 binary operation
 ------------------------------------------------------------------------