diff --git a/CHANGELOG.md b/CHANGELOG.md index 812fe00b6c..3f90a17923 100644 --- a/CHANGELOG.md +++ b/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`: diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index f20cf1ad03..40e0fc5176 100644 --- a/src/Algebra/Bundles.agda +++ b/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 diff --git a/src/Algebra/Bundles/Raw.agda b/src/Algebra/Bundles/Raw.agda index e7f9be1349..14527a53a6 100644 --- a/src/Algebra/Bundles/Raw.agda +++ b/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 + ) diff --git a/src/Algebra/Morphism/Construct/Composition.agda b/src/Algebra/Morphism/Construct/Composition.agda index 5087de2ae3..17d5f2798b 100644 --- a/src/Algebra/Morphism/Construct/Composition.agda +++ b/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 + diff --git a/src/Algebra/Morphism/Construct/Identity.agda b/src/Algebra/Morphism/Construct/Identity.agda index 63e95e54e6..881a8cf15c 100644 --- a/src/Algebra/Morphism/Construct/Identity.agda +++ b/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 _ + } + diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda index eb8970ba5c..e73fa7e9e6 100644 --- a/src/Algebra/Morphism/Structures.agda +++ b/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