From 4c2a9c60b5d47653fe2a96c6d78e57e70ab3eb6e Mon Sep 17 00:00:00 2001 From: Akshobhya K M Date: Sat, 18 Mar 2023 16:35:00 -0400 Subject: [PATCH 1/4] merge master --- CHANGELOG.md | 4 ++ src/Algebra/Bundles.agda | 2 +- src/Algebra/Bundles/Raw.agda | 30 +++++++++++++ .../Morphism/Construct/Composition.agda | 40 +++++++++++++++++ src/Algebra/Morphism/Construct/Identity.agda | 26 +++++++++++ src/Algebra/Morphism/Structures.agda | 43 +++++++++++++++++++ 6 files changed, 144 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index edb69c4b8f..2280df4067 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -835,6 +835,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. @@ -1830,6 +1831,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 2598fde953..18b73065fe 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..ad96333fb5 100644 --- a/src/Algebra/Bundles/Raw.agda +++ b/src/Algebra/Bundles/Raw.agda @@ -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 991fb93433..acdcf19c90 100644 --- a/src/Algebra/Morphism/Construct/Composition.agda +++ b/src/Algebra/Morphism/Construct/Composition.agda @@ -384,3 +384,43 @@ module _ {L₁ : RawLoop a ℓ₁} { isLoopMonomorphism = isLoopMonomorphism F.isLoopMonomorphism G.isLoopMonomorphism ; surjective = Func.surjective (_≈_ L₁) (_≈_ L₂) (_≈_ L₃) ≈₃-trans G.⟦⟧-cong 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₃) ≈₃-trans G.⟦⟧-cong 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 5ea2571de0..668c199eb2 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 using (_,_) open import Function.Base using (id) @@ -247,3 +248,28 @@ module _ (L : RawLoop c ℓ) (open RawLoop L) (refl : Reflexive _≈_) where { isLoopMonomorphism = isLoopMonomorphism ; surjective = _, refl } + +------------------------------------------------------------------------ +-- 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 = _, refl + } + diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda index 525cbf5da0..6f4791fd7d 100644 --- a/src/Algebra/Morphism/Structures.agda +++ b/src/Algebra/Morphism/Structures.agda @@ -694,6 +694,48 @@ 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 FunctionDefinitions _≈₁_ _≈₂_ + 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 @@ -706,3 +748,4 @@ open RingWithoutOneMorphisms public open RingMorphisms public open QuasigroupMorphisms public open LoopMorphisms public +open KleeneAlgebraMorphisms public From cd066846067fd65355cd7cf3c17ba395b1cac391 Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Fri, 11 Aug 2023 14:01:09 +0100 Subject: [PATCH 2/4] Update Raw.agda Deleting spurious whitespace --- src/Algebra/Bundles/Raw.agda | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/src/Algebra/Bundles/Raw.agda b/src/Algebra/Bundles/Raw.agda index ad96333fb5..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 @@ -292,13 +292,13 @@ record RawKleeneAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where infixl 6 _+_ infix 4 _≈_ field - Carrier : Set c - _≈_ : Rel Carrier ℓ - _+_ : Op₂ Carrier - _*_ : Op₂ Carrier - _⋆ : Op₁ Carrier - 0# : Carrier - 1# : Carrier + Carrier : Set c + _≈_ : Rel Carrier ℓ + _+_ : Op₂ Carrier + _*_ : Op₂ Carrier + _⋆ : Op₁ Carrier + 0# : Carrier + 1# : Carrier rawSemiring : RawSemiring c ℓ rawSemiring = record From 873ee2860f054f6ffca00fc230d1465050165346 Mon Sep 17 00:00:00 2001 From: Akshobhya K M Date: Fri, 1 Sep 2023 13:16:11 -0400 Subject: [PATCH 3/4] fix morphism --- src/Algebra/Morphism/Structures.agda | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda index 43ac948740..e73fa7e9e6 100644 --- a/src/Algebra/Morphism/Structures.agda +++ b/src/Algebra/Morphism/Structures.agda @@ -703,7 +703,6 @@ module KleeneAlgebraMorphisms (R₁ : RawKleeneAlgebra a ℓ₁) (R₂ : RawKlee ) open MorphismDefinitions A B _≈₂_ - open FunctionDefinitions _≈₁_ _≈₂_ open SemiringMorphisms rawSemiring₁ rawSemiring₂ record IsKleeneAlgebraHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where @@ -716,14 +715,14 @@ module KleeneAlgebraMorphisms (R₁ : RawKleeneAlgebra a ℓ₁) (R₂ : RawKlee record IsKleeneAlgebraMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isKleeneAlgebraHomomorphism : IsKleeneAlgebraHomomorphism ⟦_⟧ - injective : Injective ⟦_⟧ + injective : Injective _≈₁_ _≈₂_ ⟦_⟧ open IsKleeneAlgebraHomomorphism isKleeneAlgebraHomomorphism public record IsKleeneAlgebraIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isKleeneAlgebraMonomorphism : IsKleeneAlgebraMonomorphism ⟦_⟧ - surjective : Surjective ⟦_⟧ + surjective : Surjective _≈₁_ _≈₂_ ⟦_⟧ open IsKleeneAlgebraMonomorphism isKleeneAlgebraMonomorphism public From 98c98835c1a705f91957110ecce989fbe5fe2af2 Mon Sep 17 00:00:00 2001 From: Akshobhya K M Date: Fri, 1 Sep 2023 14:16:31 -0400 Subject: [PATCH 4/4] fix composition and identity morphism --- src/Algebra/Morphism/Construct/Composition.agda | 2 +- src/Algebra/Morphism/Construct/Identity.agda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Morphism/Construct/Composition.agda b/src/Algebra/Morphism/Construct/Composition.agda index 55c47e07b8..17d5f2798b 100644 --- a/src/Algebra/Morphism/Construct/Composition.agda +++ b/src/Algebra/Morphism/Construct/Composition.agda @@ -420,6 +420,6 @@ module _ {K₁ : RawKleeneAlgebra a ℓ₁} → IsKleeneAlgebraIsomorphism K₁ K₃ (g ∘ f) isKleeneAlgebraIsomorphism f-iso g-iso = record { isKleeneAlgebraMonomorphism = isKleeneAlgebraMonomorphism F.isKleeneAlgebraMonomorphism G.isKleeneAlgebraMonomorphism - ; surjective = Func.surjective (_≈_ K₁) (_≈_ K₂) (_≈_ K₃) ≈₃-trans G.⟦⟧-cong F.surjective G.surjective + ; 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 576c97155c..881a8cf15c 100644 --- a/src/Algebra/Morphism/Construct/Identity.agda +++ b/src/Algebra/Morphism/Construct/Identity.agda @@ -271,6 +271,6 @@ module _ (K : RawKleeneAlgebra c ℓ) (open RawKleeneAlgebra K) (refl : Reflexiv isKleeneAlgebraIsomorphism : IsKleeneAlgebraIsomorphism id isKleeneAlgebraIsomorphism = record { isKleeneAlgebraMonomorphism = isKleeneAlgebraMonomorphism - ; surjective = _, refl + ; surjective = Id.surjective _ }