Tidy up and expand morphism hierarchies

CHANGELOG.md

@@ -218,8 +218,10 @@ New modules
 -----------
 The following new modules have been added to the library:
   ```
-  Algebra.Morphism.RawMagma
-  Algebra.Morphism.RawMonoid
+  Algebra.Morphism.Definitions
+  Algebra.Morphism.Structures
+  Algebra.Morphism.MagmaMonomorphism
+  Algebra.Morphism.MonoidMonomorphism
 
   Algebra.Properties.Semigroup
   Algebra.Properties.CommutativeSemigroup
@@ -275,8 +277,10 @@ The following new modules have been added to the library:
   Relation.Binary.Reasoning.PartialSetoid
 
   Relation.Binary.Morphism
-  Relation.Binary.Morphism.RawOrder
-  Relation.Binary.Morphism.RawRelation
+  Relation.Binary.Morphism.Definitions
+  Relation.Binary.Morphism.Structures
+  Relation.Binary.Morphism.RelMonomorphism
+  Relation.Binary.Morphism.OrderMonomorphism
 
   Relation.Nullary.Reflects
   ```

src/Algebra/Morphism.agda

@@ -8,94 +8,30 @@
 
 module Algebra.Morphism where
 
+import Algebra.Morphism.Definitions as MorphismDefinitions
 open import Relation.Binary
 open import Algebra
 import Algebra.Properties.Group as GroupP
 open import Function
 open import Level
 import Relation.Binary.Reasoning.Setoid as EqR
 
-------------------------------------------------------------------------
--- Basic definitions
-
-module Definitions {f t ℓ}
-                   (From : Set f) (To : Set t) (_≈_ : Rel To ℓ) where
-  Morphism : Set _
-  Morphism = From → To
-
-  Homomorphic₀ : Morphism → From → To → Set _
-  Homomorphic₀ ⟦_⟧ ∙ ∘ = ⟦ ∙ ⟧ ≈ ∘
-
-  Homomorphic₁ : Morphism → Fun₁ From → Op₁ To → Set _
-  Homomorphic₁ ⟦_⟧ ∙_ ∘_ = ∀ x → ⟦ ∙ x ⟧ ≈ (∘ ⟦ x ⟧)
-
-  Homomorphic₂ : Morphism → Fun₂ From → Op₂ To → Set _
-  Homomorphic₂ ⟦_⟧ _∙_ _∘_ =
-    ∀ x y → ⟦ x ∙ y ⟧ ≈ (⟦ x ⟧ ∘ ⟦ y ⟧)
+private
+  variable
+    a b ℓ₁ ℓ₂ : Level
+    A : Set a
+    B : Set b
 
 ------------------------------------------------------------------------
--- Raw structure homomorphisms
-
-module _ {c₁ ℓ₁ c₂ ℓ₂}
-         (From : RawMagma c₁ ℓ₁)
-         (To   : RawMagma c₂ ℓ₂) where
-
-  private
-    module F = RawMagma From
-    module T = RawMagma To
-  open Definitions F.Carrier T.Carrier T._≈_
-
-  record IsRawMagmaMorphism (⟦_⟧ : Morphism) :
-         Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
-    field
-      F-isMagma : IsMagma F._≈_ F._∙_
-      T-isMagma : IsMagma T._≈_ T._∙_
-      ⟦⟧-cong : ⟦_⟧ Preserves F._≈_ ⟶ T._≈_
-      ∙-homo  : Homomorphic₂ ⟦_⟧ F._∙_ T._∙_
-
-    open IsMagma F-isMagma public using ()
-      renaming
-      ( ∙-cong  to F-∙-cong
-      ; ∙-congˡ to F-∙-congˡ
-      ; ∙-congʳ to F-∙-congʳ
-      ; setoid  to F-setoid
-      )
-
-    open IsMagma T-isMagma public using ()
-      renaming
-      ( ∙-cong  to T-∙-cong
-      ; ∙-congˡ to T-∙-congˡ
-      ; ∙-congʳ to T-∙-congʳ
-      ; setoid  to T-setoid
-      )
-
-  IsRawMagmaMorphism-syntax = IsRawMagmaMorphism
-  syntax IsRawMagmaMorphism-syntax From To F = F Is From -RawMagma⟶ To
-
-
-module _ {c₁ ℓ₁ c₂ ℓ₂}
-         (From : RawMonoid c₁ ℓ₁)
-         (To   : RawMonoid c₂ ℓ₂) where
-
-  private
-    module F = RawMonoid From
-    module T = RawMonoid To
-  open Definitions F.Carrier T.Carrier T._≈_
-
-  record IsRawMonoidMorphism (⟦_⟧ : Morphism) :
-         Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
-    field
-      magma-homo : IsRawMagmaMorphism F.rawMagma T.rawMagma ⟦_⟧
-      ε-homo     : Homomorphic₀ ⟦_⟧ F.ε T.ε
-
-    open IsRawMagmaMorphism magma-homo public
+--
 
-  IsRawMonoidMorphism-syntax = IsRawMonoidMorphism
-  syntax IsRawMonoidMorphism-syntax From To F = F Is From -RawMonoid⟶ To
+module Definitions {a b ℓ₁} (A : Set a) (B : Set b) (_≈_ : Rel B ℓ₁) where
+  open MorphismDefinitions A B _≈_ public
 
+open import Algebra.Morphism.Structures public
 
 ------------------------------------------------------------------------
--- Structure homomorphisms
+-- Bundle homomorphisms
 
 module _ {c₁ ℓ₁ c₂ ℓ₂}
          (From : Semigroup c₁ ℓ₁)

src/Algebra/Morphism/Definitions.agda

@@ -0,0 +1,33 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Basic definitions for morphisms between algebraic structures
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary.Core
+
+module Algebra.Morphism.Definitions
+  {a} (A : Set a)     -- The domain of the morphism
+  {b} (B : Set b)     -- The codomain of the morphism
+  {ℓ} (_≈_ : Rel B ℓ)  -- The equality relation over the codomain
+  where
+
+open import Algebra.Core
+open import Function.Core
+
+------------------------------------------------------------------------
+-- Basic definitions
+
+Morphism : Set _
+Morphism = A → B
+
+Homomorphic₀ : Morphism → A → B → Set _
+Homomorphic₀ ⟦_⟧ ∙ ∘ = ⟦ ∙ ⟧ ≈ ∘
+
+Homomorphic₁ : Morphism → Fun₁ A → Op₁ B → Set _
+Homomorphic₁ ⟦_⟧ ∙_ ∘_ = ∀ x → ⟦ ∙ x ⟧ ≈ (∘ ⟦ x ⟧)
+
+Homomorphic₂ : Morphism → Fun₂ A → Op₂ B → Set _
+Homomorphic₂ ⟦_⟧ _∙_ _∘_ = ∀ x y → ⟦ x ∙ y ⟧ ≈ (⟦ x ⟧ ∘ ⟦ y ⟧)

src/Algebra/Morphism/MagmaMonomorphism.agda

@@ -0,0 +1,129 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Consequences of a monomorphism between magma-like structures
+------------------------------------------------------------------------
+
+-- See Data.Nat.Binary.Properties for examples of how this and similar
+-- modules can be used to easily translate properties between types.
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra.Core
+open import Algebra.Bundles
+open import Algebra.Morphism.Structures
+open import Relation.Binary.Core
+
+module Algebra.Morphism.MagmaMonomorphism
+  {a b ℓ₁ ℓ₂} {M₁ : RawMagma a ℓ₁} {M₂ : RawMagma b ℓ₂} {⟦_⟧}
+  (isMagmaMonomorphism : IsMagmaMonomorphism M₁ M₂ ⟦_⟧)
+  where
+
+open IsMagmaMonomorphism isMagmaMonomorphism
+open RawMagma M₁ renaming (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_)
+open RawMagma M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_)
+
+open import Algebra.Structures
+open import Algebra.Definitions
+open import Data.Product
+open import Data.Sum using (inj₁; inj₂)
+import Relation.Binary.Reasoning.Setoid as SetoidReasoning
+import Relation.Binary.Morphism.RelMonomorphism isRelMonomorphism as RelMorphism
+
+------------------------------------------------------------------------
+-- Properties
+
+module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where
+
+  open IsMagma ◦-isMagma renaming (∙-cong to ◦-cong)
+  open SetoidReasoning setoid
+
+  cong : Congruent₂ _≈₁_ _∙_
+  cong {x} {y} {u} {v} x≈y u≈v = injective (begin
+    ⟦ x ∙ u ⟧      ≈⟨  homo x u ⟩
+    ⟦ x ⟧ ◦ ⟦ u ⟧  ≈⟨  ◦-cong (⟦⟧-cong x≈y) (⟦⟧-cong u≈v) ⟩
+    ⟦ y ⟧ ◦ ⟦ v ⟧  ≈˘⟨ homo y v ⟩
+    ⟦ y ∙ v ⟧      ∎)
+
+  assoc : Associative _≈₂_ _◦_ → Associative _≈₁_ _∙_
+  assoc assoc x y z = injective (begin
+    ⟦ (x ∙ y) ∙ z ⟧          ≈⟨  homo (x ∙ y) z ⟩
+    ⟦ x ∙ y ⟧ ◦ ⟦ z ⟧        ≈⟨  ◦-cong (homo x y) refl ⟩
+    (⟦ x ⟧ ◦ ⟦ y ⟧) ◦ ⟦ z ⟧  ≈⟨  assoc ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ ⟩
+    ⟦ x ⟧ ◦ (⟦ y ⟧ ◦ ⟦ z ⟧)  ≈˘⟨ ◦-cong refl (homo y z) ⟩
+    ⟦ x ⟧ ◦ ⟦ y ∙ z ⟧        ≈˘⟨ homo x (y ∙ z) ⟩
+    ⟦ x ∙ (y ∙ z) ⟧          ∎)
+
+  comm : Commutative _≈₂_ _◦_ → Commutative _≈₁_ _∙_
+  comm comm x y = injective (begin
+    ⟦ x ∙ y ⟧      ≈⟨  homo x y ⟩
+    ⟦ x ⟧ ◦ ⟦ y ⟧  ≈⟨  comm ⟦ x ⟧ ⟦ y ⟧ ⟩
+    ⟦ y ⟧ ◦ ⟦ x ⟧  ≈˘⟨ homo y x ⟩
+    ⟦ y ∙ x ⟧      ∎)
+
+  idem : Idempotent _≈₂_ _◦_ → Idempotent _≈₁_ _∙_
+  idem idem x = injective (begin
+    ⟦ x ∙ x ⟧     ≈⟨ homo x x ⟩
+    ⟦ x ⟧ ◦ ⟦ x ⟧ ≈⟨ idem ⟦ x ⟧ ⟩
+    ⟦ x ⟧         ∎)
+
+  sel : Selective _≈₂_ _◦_ → Selective _≈₁_ _∙_
+  sel sel x y with sel ⟦ x ⟧ ⟦ y ⟧
+  ... | inj₁ x◦y≈x = inj₁ (injective (begin
+    ⟦ x ∙ y ⟧      ≈⟨ homo x y ⟩
+    ⟦ x ⟧ ◦ ⟦ y ⟧  ≈⟨ x◦y≈x ⟩
+    ⟦ x ⟧          ∎))
+  ... | inj₂ x◦y≈y = inj₂ (injective (begin
+    ⟦ x ∙ y ⟧      ≈⟨ homo x y ⟩
+    ⟦ x ⟧ ◦ ⟦ y ⟧  ≈⟨ x◦y≈y ⟩
+    ⟦ y ⟧          ∎))
+
+  cancelˡ : LeftCancellative _≈₂_ _◦_ → LeftCancellative _≈₁_ _∙_
+  cancelˡ cancelˡ x {y} {z} x∙y≈x∙z = injective (cancelˡ ⟦ x ⟧ (begin
+    ⟦ x ⟧ ◦ ⟦ y ⟧  ≈˘⟨ homo x y ⟩
+    ⟦ x ∙ y ⟧      ≈⟨  ⟦⟧-cong x∙y≈x∙z ⟩
+    ⟦ x ∙ z ⟧      ≈⟨  homo x z ⟩
+    ⟦ x ⟧ ◦ ⟦ z ⟧  ∎))
+
+  cancelʳ : RightCancellative _≈₂_ _◦_ → RightCancellative _≈₁_ _∙_
+  cancelʳ cancelʳ {x} y z y∙x≈z∙x = injective (cancelʳ ⟦ y ⟧ ⟦ z ⟧ (begin
+    ⟦ y ⟧ ◦ ⟦ x ⟧  ≈˘⟨ homo y x ⟩
+    ⟦ y ∙ x ⟧      ≈⟨  ⟦⟧-cong y∙x≈z∙x ⟩
+    ⟦ z ∙ x ⟧      ≈⟨  homo z x ⟩
+    ⟦ z ⟧ ◦ ⟦ x ⟧  ∎))
+
+  cancel : Cancellative _≈₂_ _◦_ → Cancellative _≈₁_ _∙_
+  cancel = map cancelˡ cancelʳ
+
+------------------------------------------------------------------------
+-- Structures
+
+isMagma : IsMagma _≈₂_ _◦_ → IsMagma _≈₁_ _∙_
+isMagma isMagma = record
+  { isEquivalence = RelMorphism.isEquivalence M.isEquivalence
+  ; ∙-cong        = cong isMagma
+  } where module M = IsMagma isMagma
+
+isSemigroup : IsSemigroup _≈₂_ _◦_ → IsSemigroup _≈₁_ _∙_
+isSemigroup isSemigroup = record
+  { isMagma = isMagma S.isMagma
+  ; assoc   = assoc   S.isMagma S.assoc
+  } where module S = IsSemigroup isSemigroup
+
+isBand : IsBand _≈₂_ _◦_ → IsBand _≈₁_ _∙_
+isBand isBand = record
+  { isSemigroup = isSemigroup B.isSemigroup
+  ; idem        = idem        B.isMagma B.idem
+  } where module B = IsBand isBand
+
+isSemilattice : IsSemilattice _≈₂_ _◦_ → IsSemilattice _≈₁_ _∙_
+isSemilattice isSemilattice = record
+  { isBand = isBand S.isBand
+  ; comm   = comm   S.isMagma S.comm
+  } where module S = IsSemilattice isSemilattice
+
+isSelectiveMagma : IsSelectiveMagma _≈₂_ _◦_ → IsSelectiveMagma _≈₁_ _∙_
+isSelectiveMagma isSelMagma = record
+  { isMagma = isMagma S.isMagma
+  ; sel     = sel     S.isMagma S.sel
+  } where module S = IsSelectiveMagma isSelMagma

src/Algebra/Morphism/MonoidMonomorphism.agda

@@ -0,0 +1,96 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Consequences of a monomorphism between monoid-like structures
+------------------------------------------------------------------------
+
+-- See Data.Nat.Binary.Properties for examples of how this and similar
+-- modules can be used to easily translate properties between types.
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra.Bundles
+open import Algebra.Morphism.Structures
+open import Relation.Binary.Core
+
+module Algebra.Morphism.MonoidMonomorphism
+  {a b ℓ₁ ℓ₂} {M₁ : RawMonoid a ℓ₁} {M₂ : RawMonoid b ℓ₂} {⟦_⟧}
+  (isMonoidMonomorphism : IsMonoidMonomorphism M₁ M₂ ⟦_⟧)
+  where
+
+open IsMonoidMonomorphism isMonoidMonomorphism
+open RawMonoid M₁ renaming (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_; ε to ε₁)
+open RawMonoid M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; ε to ε₂)
+
+open import Algebra.Definitions
+open import Algebra.Structures
+open import Data.Product using (map)
+open import Relation.Binary
+import Relation.Binary.Reasoning.Setoid as SetoidReasoning
+
+------------------------------------------------------------------------
+-- Re-export all properties of magma monomorphisms
+
+open import Algebra.Morphism.MagmaMonomorphism
+  isMagmaMonomorphism public
+
+------------------------------------------------------------------------
+-- Properties
+
+module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where
+
+  open IsMagma ◦-isMagma renaming (∙-cong to ◦-cong)
+  open SetoidReasoning setoid
+
+  identityˡ : LeftIdentity _≈₂_ ε₂ _◦_ → LeftIdentity _≈₁_ ε₁ _∙_
+  identityˡ idˡ x = injective (begin
+    ⟦ ε₁ ∙ x ⟧      ≈⟨ homo ε₁ x ⟩
+    ⟦ ε₁ ⟧ ◦ ⟦ x ⟧  ≈⟨ ◦-cong ε-homo refl ⟩
+    ε₂ ◦ ⟦ x ⟧      ≈⟨ idˡ ⟦ x ⟧ ⟩
+    ⟦ x ⟧           ∎)
+
+  identityʳ : RightIdentity _≈₂_ ε₂ _◦_ → RightIdentity _≈₁_ ε₁ _∙_
+  identityʳ idʳ x = injective (begin
+    ⟦ x ∙ ε₁ ⟧      ≈⟨ homo x ε₁ ⟩
+    ⟦ x ⟧ ◦ ⟦ ε₁ ⟧  ≈⟨ ◦-cong refl ε-homo ⟩
+    ⟦ x ⟧ ◦ ε₂      ≈⟨ idʳ ⟦ x ⟧ ⟩
+    ⟦ x ⟧           ∎)
+
+  identity : Identity _≈₂_ ε₂ _◦_ → Identity _≈₁_ ε₁ _∙_
+  identity = map identityˡ identityʳ
+
+  zeroˡ : LeftZero _≈₂_ ε₂ _◦_ → LeftZero _≈₁_ ε₁ _∙_
+  zeroˡ zeˡ x = injective (begin
+    ⟦ ε₁ ∙ x ⟧     ≈⟨  homo ε₁ x ⟩
+    ⟦ ε₁ ⟧ ◦ ⟦ x ⟧ ≈⟨  ◦-cong ε-homo refl ⟩
+    ε₂   ◦ ⟦ x ⟧   ≈⟨  zeˡ ⟦ x ⟧ ⟩
+    ε₂             ≈˘⟨ ε-homo ⟩
+    ⟦ ε₁ ⟧         ∎)
+
+  zeroʳ : RightZero _≈₂_ ε₂ _◦_ → RightZero _≈₁_ ε₁ _∙_
+  zeroʳ zeʳ x = injective (begin
+    ⟦ x ∙ ε₁ ⟧     ≈⟨  homo x ε₁ ⟩
+    ⟦ x ⟧ ◦ ⟦ ε₁ ⟧ ≈⟨  ◦-cong refl ε-homo ⟩
+    ⟦ x ⟧ ◦ ε₂     ≈⟨  zeʳ ⟦ x ⟧ ⟩
+    ε₂             ≈˘⟨ ε-homo ⟩
+    ⟦ ε₁ ⟧         ∎)
+
+  zero : Zero _≈₂_ ε₂ _◦_ → Zero _≈₁_ ε₁ _∙_
+  zero = map zeroˡ zeroʳ
+
+------------------------------------------------------------------------
+-- Structures
+
+isMonoid : IsMonoid _≈₂_ _◦_ ε₂ → IsMonoid _≈₁_ _∙_ ε₁
+isMonoid isMonoid = record
+  { isSemigroup = isSemigroup M.isSemigroup
+  ; identity    = identity    M.isMagma M.identity
+  } where module M = IsMonoid isMonoid
+
+isCommutativeMonoid : IsCommutativeMonoid _≈₂_ _◦_ ε₂ →
+                      IsCommutativeMonoid _≈₁_ _∙_ ε₁
+isCommutativeMonoid isCommMonoid = record
+  { isSemigroup = isSemigroup C.isSemigroup
+  ; identityˡ   = identityˡ   C.isMagma C.identityˡ
+  ; comm        = comm        C.isMagma C.comm
+  } where module C = IsCommutativeMonoid isCommMonoid