Add more properties for ordered structures.

1 files changed, 98 insertions, 0 deletions

diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Morphism/Structures.agda b/src/Helium/Algebra/Ordered/StrictTotal/Morphism/Structures.agda
new file mode 100644
index 0000000..dbce970
--- /dev/null
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Morphism/Structures.agda
@@ -0,0 +1,98 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Morphisms for ordered algebraic structures.
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+module Helium.Algebra.Ordered.StrictTotal.Morphism.Structures where
+
+import Algebra.Morphism.Definitions as MorphismDefinitions
+open import Helium.Algebra.Ordered.StrictTotal.Bundles
+open import Level using (Level; _⊔_)
+open import Relation.Binary.Morphism.Structures
+
+private
+  variable
+    a b ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level
+
+module MagmaMorphisms (M₁ : RawMagma a ℓ₁ ℓ₂) (M₂ : RawMagma b ℓ₃ ℓ₄) where
+  private
+    module M₁ = RawMagma M₁
+    module M₂ = RawMagma M₂
+
+  open M₁ using () renaming (Carrier to A)
+  open M₂ using () renaming (Carrier to B)
+  open MorphismDefinitions A B M₂._≈_
+
+  record IsMagmaHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
+    field
+      isOrderHomomorphism : IsOrderHomomorphism M₁._≈_ M₂._≈_ M₁._<_ M₂._<_ ⟦_⟧
+      homo                : Homomorphic₂ ⟦_⟧ M₁._∙_ M₂._∙_
+
+    open IsOrderHomomorphism isOrderHomomorphism public
+
+module MonoidMorphisms (M₁ : RawMonoid a ℓ₁ ℓ₂) (M₂ : RawMonoid b ℓ₃ ℓ₄) where
+  private
+    module M₁ = RawMonoid M₁
+    module M₂ = RawMonoid M₂
+
+  open M₁ using () renaming (Carrier to A)
+  open M₂ using () renaming (Carrier to B)
+  open MorphismDefinitions A B M₂._≈_
+  open MagmaMorphisms M₁.rawMagma M₂.rawMagma
+
+  record IsMonoidHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
+    field
+      isMagmaHomomorphism : IsMagmaHomomorphism ⟦_⟧
+      ε-homo              : Homomorphic₀ ⟦_⟧ M₁.ε M₂.ε
+
+    open IsMagmaHomomorphism isMagmaHomomorphism public
+
+module GroupMorphisms (G₁ : RawGroup a ℓ₁ ℓ₂) (G₂ : RawGroup b ℓ₃ ℓ₄) where
+  private
+    module G₁ = RawGroup G₁
+    module G₂ = RawGroup G₂
+
+  open G₁ using () renaming (Carrier to A)
+  open G₂ using () renaming (Carrier to B)
+  open MorphismDefinitions A B G₂._≈_
+  open MonoidMorphisms G₁.rawMonoid G₂.rawMonoid
+
+  record IsGroupHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
+    field
+      isMonoidHomomorphism : IsMonoidHomomorphism ⟦_⟧
+      ⁻¹-homo              : Homomorphic₁ ⟦_⟧ G₁._⁻¹ G₂._⁻¹
+
+    open IsMonoidHomomorphism isMonoidHomomorphism public
+
+module RingMorphisms (R₁ : RawRing a ℓ₁ ℓ₂) (R₂ : RawRing b ℓ₃ ℓ₄) where
+  private
+    module R₁ = RawRing R₁
+    module R₂ = RawRing R₂
+
+  open R₁ using () renaming (Carrier to A)
+  open R₂ using () renaming (Carrier to B)
+  open MorphismDefinitions A B R₂._≈_
+  open GroupMorphisms R₁.+-rawGroup R₂.+-rawGroup
+
+  record IsRingHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
+    field
+      +-isGroupHomomorphism : IsGroupHomomorphism ⟦_⟧
+      *-homo                : Homomorphic₂ ⟦_⟧ R₁._*_ R₂._*_
+      1#-homo               : Homomorphic₀ ⟦_⟧ R₁.1# R₂.1#
+
+    open IsGroupHomomorphism +-isGroupHomomorphism public
+      renaming
+      ( homo to +-homo
+      ; ε-homo to 0#-homo
+      ; ⁻¹-homo to -‿homo
+      ; isMagmaHomomorphism to +-isMagmaHomomorphism
+      ; isMonoidHomomorphism to +-isMonoidHomomorphism
+      )
+
+open MagmaMorphisms public
+open MonoidMorphisms public
+open GroupMorphisms public
+open RingMorphisms public