Kleene Algebra morphism with composition and identity construct

CHANGELOG.md

@@ -967,6 +967,7 @@ Major improvements
   * `RawRing`
   * `RawQuasigroup`
   * `RawLoop`
+  * `RawKleeneAlgebra`
 * A new module `Algebra.Lattice.Bundles.Raw` is also introduced.
   * `RawLattice` has been moved from `Algebra.Lattice.Bundles` to this new module.
 
@@ -2022,6 +2023,9 @@ Other minor changes
   record IsRingWithoutOneHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂)
   record IsRingWithoutOneMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂)
   record IsRingWithoutOneIsoMorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
+  record IsKleeneAlgebraHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂)
+  record IsKleeneAlgebraMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂)
+  record IsKleeneAlgebraIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
   ```
 
 * Added new proofs in `Data.Bool.Properties`:

src/Algebra/Bundles.agda

@@ -26,7 +26,7 @@ open Raw public
   using (RawMagma; RawMonoid; RawGroup
         ; RawNearSemiring; RawSemiring
         ; RawRingWithoutOne; RawRing
-        ; RawQuasigroup; RawLoop)
+        ; RawQuasigroup; RawLoop; RawKleeneAlgebra)
 
 ------------------------------------------------------------------------
 -- Bundles with 1 binary operation

src/Algebra/Bundles/Raw.agda

@@ -153,12 +153,12 @@ record RawRingWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 6 _+_
   infix  4 _≈_
   field
-    Carrier           : Set c
-    _≈_               : Rel Carrier ℓ
-    _+_               : Op₂ Carrier
-    _*_               : Op₂ Carrier
-    -_                : Op₁ Carrier
-    0#                : Carrier
+    Carrier : Set c
+    _≈_     : Rel Carrier ℓ
+    _+_     : Op₂ Carrier
+    _*_     : Op₂ Carrier
+    -_      : Op₁ Carrier
+    0#      : Carrier
 
   +-rawGroup : RawGroup c ℓ
   +-rawGroup = record
@@ -285,3 +285,33 @@ record RawLoop  c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open RawQuasigroup rawQuasigroup public
     using (_≉_ ; ∙-rawMagma; \\-rawMagma; //-rawMagma)
+
+record RawKleeneAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  8 _⋆
+  infixl 7 _*_
+  infixl 6 _+_
+  infix  4 _≈_
+  field
+    Carrier : Set c
+    _≈_     : Rel Carrier ℓ
+    _+_     : Op₂ Carrier
+    _*_     : Op₂ Carrier
+    _⋆      : Op₁ Carrier
+    0#      : Carrier
+    1#      : Carrier
+
+  rawSemiring : RawSemiring c ℓ
+  rawSemiring = record
+    { _≈_ = _≈_
+    ; _+_ = _+_
+    ; _*_ = _*_
+    ; 0#  = 0#
+    ; 1#  = 1#
+    }
+
+  open RawSemiring rawSemiring public
+    using
+    ( _≉_
+    ; +-rawMagma; +-rawMonoid
+    ; *-rawMagma; *-rawMonoid
+    )

src/Algebra/Morphism/Construct/Composition.agda

@@ -383,3 +383,43 @@ module _ {L₁ : RawLoop a ℓ₁}
     { isLoopMonomorphism = isLoopMonomorphism F.isLoopMonomorphism G.isLoopMonomorphism
     ; surjective         = Func.surjective _ _ (_≈_ L₃) F.surjective G.surjective
     } where module F = IsLoopIsomorphism f-iso; module G = IsLoopIsomorphism g-iso
+
+------------------------------------------------------------------------
+-- KleeneAlgebra
+
+module _ {K₁ : RawKleeneAlgebra a ℓ₁}
+         {K₂ : RawKleeneAlgebra b ℓ₂}
+         {K₃ : RawKleeneAlgebra c ℓ₃}
+         (open RawKleeneAlgebra)
+         (≈₃-trans : Transitive (_≈_ K₃))
+         {f : Carrier K₁ → Carrier K₂}
+         {g : Carrier K₂ → Carrier K₃}
+         where
+
+  isKleeneAlgebraHomomorphism
+    : IsKleeneAlgebraHomomorphism K₁ K₂ f
+    → IsKleeneAlgebraHomomorphism K₂ K₃ g
+    → IsKleeneAlgebraHomomorphism K₁ K₃ (g ∘ f)
+  isKleeneAlgebraHomomorphism f-homo g-homo = record
+    { isSemiringHomomorphism = isSemiringHomomorphism ≈₃-trans F.isSemiringHomomorphism G.isSemiringHomomorphism
+    ; ⋆-homo              = λ x → ≈₃-trans (G.⟦⟧-cong (F.⋆-homo x)) (G.⋆-homo (f x))
+    } where module F = IsKleeneAlgebraHomomorphism f-homo; module G = IsKleeneAlgebraHomomorphism g-homo
+
+  isKleeneAlgebraMonomorphism
+    : IsKleeneAlgebraMonomorphism K₁ K₂ f
+    → IsKleeneAlgebraMonomorphism K₂ K₃ g
+    → IsKleeneAlgebraMonomorphism K₁ K₃ (g ∘ f)
+  isKleeneAlgebraMonomorphism f-mono g-mono = record
+    { isKleeneAlgebraHomomorphism = isKleeneAlgebraHomomorphism F.isKleeneAlgebraHomomorphism G.isKleeneAlgebraHomomorphism
+    ; injective = F.injective ∘ G.injective
+    } where module F = IsKleeneAlgebraMonomorphism f-mono;  module G = IsKleeneAlgebraMonomorphism g-mono
+
+  isKleeneAlgebraIsomorphism
+    : IsKleeneAlgebraIsomorphism K₁ K₂ f
+    → IsKleeneAlgebraIsomorphism K₂ K₃ g
+    → IsKleeneAlgebraIsomorphism K₁ K₃ (g ∘ f)
+  isKleeneAlgebraIsomorphism f-iso g-iso = record
+    { isKleeneAlgebraMonomorphism = isKleeneAlgebraMonomorphism F.isKleeneAlgebraMonomorphism G.isKleeneAlgebraMonomorphism
+    ; surjective                  = Func.surjective (_≈_ K₁) (_≈_ K₂) (_≈_ K₃) F.surjective G.surjective
+    } where module F = IsKleeneAlgebraIsomorphism f-iso; module G = IsKleeneAlgebraIsomorphism g-iso
+

src/Algebra/Morphism/Construct/Identity.agda

@@ -19,6 +19,7 @@ open import Algebra.Morphism.Structures
         ; module RingMorphisms
         ; module QuasigroupMorphisms
         ; module LoopMorphisms
+        ; module KleeneAlgebraMorphisms
         )
 open import Data.Product.Base using (_,_)
 open import Function.Base using (id)
@@ -248,3 +249,28 @@ module _ (L : RawLoop c ℓ) (open RawLoop L) (refl : Reflexive _≈_) where
     { isLoopMonomorphism = isLoopMonomorphism
     ; surjective = Id.surjective _
     }
+
+------------------------------------------------------------------------
+-- KleeneAlgebra
+
+module _ (K : RawKleeneAlgebra c ℓ) (open RawKleeneAlgebra K) (refl : Reflexive _≈_) where
+  open KleeneAlgebraMorphisms K K
+
+  isKleeneAlgebraHomomorphism : IsKleeneAlgebraHomomorphism id
+  isKleeneAlgebraHomomorphism = record
+    { isSemiringHomomorphism = isSemiringHomomorphism _ refl
+    ; ⋆-homo = λ _ → refl
+    }
+
+  isKleeneAlgebraMonomorphism : IsKleeneAlgebraMonomorphism id
+  isKleeneAlgebraMonomorphism = record
+    { isKleeneAlgebraHomomorphism = isKleeneAlgebraHomomorphism
+    ; injective = id
+    }
+
+  isKleeneAlgebraIsomorphism : IsKleeneAlgebraIsomorphism id
+  isKleeneAlgebraIsomorphism = record
+    { isKleeneAlgebraMonomorphism = isKleeneAlgebraMonomorphism
+    ; surjective = Id.surjective _
+    }
+

src/Algebra/Morphism/Structures.agda

@@ -685,6 +685,47 @@ module LoopMorphisms (L₁ : RawLoop a ℓ₁) (L₂ : RawLoop b ℓ₂) where
 
     open IsLoopMonomorphism isLoopMonomorphism public
 
+------------------------------------------------------------------------
+-- Morphisms over Kleene algebra structures
+------------------------------------------------------------------------
+module KleeneAlgebraMorphisms (R₁ : RawKleeneAlgebra a ℓ₁) (R₂ : RawKleeneAlgebra b ℓ₂) where
+
+  open RawKleeneAlgebra R₁ renaming
+    ( Carrier to A; _≈_ to _≈₁_
+    ; _⋆ to _⋆₁
+    ; rawSemiring to rawSemiring₁
+    )
+
+  open RawKleeneAlgebra R₂ renaming
+    ( Carrier to B; _≈_ to _≈₂_
+    ; _⋆ to _⋆₂
+    ; rawSemiring to rawSemiring₂
+    )
+
+  open MorphismDefinitions A B _≈₂_
+  open SemiringMorphisms rawSemiring₁ rawSemiring₂
+
+  record IsKleeneAlgebraHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      isSemiringHomomorphism : IsSemiringHomomorphism ⟦_⟧
+      ⋆-homo :  Homomorphic₁ ⟦_⟧ _⋆₁ _⋆₂
+
+    open IsSemiringHomomorphism isSemiringHomomorphism public
+
+  record IsKleeneAlgebraMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      isKleeneAlgebraHomomorphism   : IsKleeneAlgebraHomomorphism ⟦_⟧
+      injective                     : Injective  _≈₁_ _≈₂_ ⟦_⟧
+
+    open IsKleeneAlgebraHomomorphism isKleeneAlgebraHomomorphism public
+
+  record IsKleeneAlgebraIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      isKleeneAlgebraMonomorphism   : IsKleeneAlgebraMonomorphism ⟦_⟧
+      surjective                    : Surjective  _≈₁_ _≈₂_ ⟦_⟧
+
+    open IsKleeneAlgebraMonomorphism isKleeneAlgebraMonomorphism public
+
 ------------------------------------------------------------------------
 -- Re-export contents of modules publicly
 
@@ -697,3 +738,4 @@ open RingWithoutOneMorphisms public
 open RingMorphisms public
 open QuasigroupMorphisms public
 open LoopMorphisms public
+open KleeneAlgebraMorphisms public