diff --git a/CHANGELOG.md b/CHANGELOG.md index 62f9b4b8e5..1a9908e933 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -75,6 +75,11 @@ Deprecated names New modules ----------- +* Bundled morphisms between (raw) algebraic structures: + ``` + Algebra.Morphism.Bundles + ``` + * Properties of `IdempotentCommutativeMonoid`s refactored out from `Algebra.Solver.IdempotentCommutativeMonoid`: ```agda Algebra.Properties.IdempotentCommutativeMonoid @@ -101,6 +106,93 @@ New modules Additions to existing modules ----------------------------- +* In `Algebra.Bundles.KleeneAlgebra`: + ```agda + rawKleeneAlgebra : RawKleeneAlgebra _ _ + ``` + +* In `Algebra.Bundles.Raw.RawRingWithoutOne` + ```agda + rawNearSemiring : RawNearSemiring c ℓ + ``` + +* Exporting more `Raw` substructures from `Algebra.Bundles.Ring`: + ```agda + rawNearSemiring : RawNearSemiring _ _ + rawRingWithoutOne : RawRingWithoutOne _ _ + +-rawGroup : RawGroup _ _ + ``` + +* Exporting `RawRingWithoutOne` and `(Raw)NearSemiring` subbundles from + `Algebra.Bundles.RingWithoutOne`: + ```agda + nearSemiring : NearSemiring _ _ + rawNearSemiring : RawNearSemiring _ _ + rawRingWithoutOne : RawRingWithoutOne _ _ + ``` + +* In `Algebra.Morphism.Construct.Composition`: + ```agda + magmaHomomorphism : MagmaHomomorphism M₁.rawMagma M₂.rawMagma → + MagmaHomomorphism M₂.rawMagma M₃.rawMagma → + MagmaHomomorphism M₁.rawMagma M₃.rawMagma + monoidHomomorphism : MonoidHomomorphism M₁.rawMonoid M₂.rawMonoid → + MonoidHomomorphism M₂.rawMonoid M₃.rawMonoid → + MonoidHomomorphism M₁.rawMonoid M₃.rawMonoid + groupHomomorphism : GroupHomomorphism M₁.rawGroup M₂.rawGroup → + GroupHomomorphism M₂.rawGroup M₃.rawGroup → + GroupHomomorphism M₁.rawGroup M₃.rawGroup + nearSemiringHomomorphism : NearSemiringHomomorphism M₁.rawNearSemiring M₂.rawNearSemiring → + NearSemiringHomomorphism M₂.rawNearSemiring M₃.rawNearSemiring → + NearSemiringHomomorphism M₁.rawNearSemiring M₃.rawNearSemiring + semiringHomomorphism : SemiringHomomorphism M₁.rawSemiring M₂.rawSemiring → + SemiringHomomorphism M₂.rawSemiring M₃.rawSemiring → + SemiringHomomorphism M₁.rawSemiring M₃.rawSemiring + kleeneAlgebraHomomorphism : KleeneAlgebraHomomorphism M₁.rawKleeneAlgebra M₂.rawKleeneAlgebra → + KleeneAlgebraHomomorphism M₂.rawKleeneAlgebra M₃.rawKleeneAlgebra → + KleeneAlgebraHomomorphism M₁.rawKleeneAlgebra M₃.rawKleeneAlgebra + nearSemiringHomomorphism : NearSemiringHomomorphism M₁.rawNearSemiring M₂.rawNearSemiring → + NearSemiringHomomorphism M₂.rawNearSemiring M₃.rawNearSemiring → + NearSemiringHomomorphism M₁.rawNearSemiring M₃.rawNearSemiring + ringWithoutOneHomomorphism : RingWithoutOneHomomorphism M₁.rawRingWithoutOne M₂.rawRingWithoutOne → + RingWithoutOneHomomorphism M₂.rawRingWithoutOne M₃.rawRingWithoutOne → + RingWithoutOneHomomorphism M₁.rawRingWithoutOne M₃.rawRingWithoutOne + ringHomomorphism : RingHomomorphism M₁.rawRing M₂.rawRing → + RingHomomorphism M₂.rawRing M₃.rawRing → + RingHomomorphism M₁.rawRing M₃.rawRing + quasigroupHomomorphism : QuasigroupHomomorphism M₁.rawQuasigroup M₂.rawQuasigroup → + QuasigroupHomomorphism M₂.rawQuasigroup M₃.rawQuasigroup → + QuasigroupHomomorphism M₁.rawQuasigroup M₃.rawQuasigroup + loopHomomorphism : LoopHomomorphism M₁.rawLoop M₂.rawLoop → + LoopHomomorphism M₂.rawLoop M₃.rawLoop → + LoopHomomorphism M₁.rawLoop M₃.rawLoop + ``` + +* In `Algebra.Morphism.Construct.Identity`: + ```agda + magmaHomomorphism : MagmaHomomorphism M.rawMagma M.rawMagma + monoidHomomorphism : MonoidHomomorphism M.rawMonoid M.rawMonoid + groupHomomorphism : GroupHomomorphism M.rawGroup M.rawGroup + nearSemiringHomomorphism : NearSemiringHomomorphism M.raw M.raw + semiringHomomorphism : SemiringHomomorphism M.rawNearSemiring M.rawNearSemiring + kleeneAlgebraHomomorphism : KleeneAlgebraHomomorphism M.rawKleeneAlgebra M.rawKleeneAlgebra + nearSemiringHomomorphism : NearSemiringHomomorphism M.rawNearSemiring M.rawNearSemiring + ringWithoutOneHomomorphism : RingWithoutOneHomomorphism M.rawRingWithoutOne M.rawRingWithoutOne + ringHomomorphism : RingHomomorphism M.rawRing M.rawRing + quasigroupHomomorphism : QuasigroupHomomorphism M.rawQuasigroup M.rawQuasigroup + loopHomomorphism : LoopHomomorphism M.rawLoop M.rawLoop + ``` + +* In `Algebra.Morphism.Structures.RingMorphisms` + ```agda + isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism ⟦_⟧ + ``` + +* In `Algebra.Morphism.Structures.RingWithoutOneMorphisms` + ```agda + isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧ + ``` + * Properties of non-divisibility in `Algebra.Properties.Magma.Divisibility`: ```agda ∤-respˡ-≈ : _∤_ Respectsˡ _≈_ @@ -118,6 +210,11 @@ Additions to existing modules Env = Vec Carrier ``` +* In `Algebra.Structures.RingWithoutOne`: + ```agda + isNearSemiring : IsNearSemiring _ _ + ``` + * In `Data.List.Membership.Setoid.Properties`: ```agda Any-∈-swap : Any (_∈ ys) xs → Any (_∈ xs) ys diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index d96584a733..88b195ec7d 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -873,6 +873,16 @@ record KleeneAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where ; rawSemiring; semiring ) + rawKleeneAlgebra : RawKleeneAlgebra _ _ + rawKleeneAlgebra = record + { _≈_ = _≈_ + ; _+_ = _+_ + ; _*_ = _*_ + ; _⋆ = _⋆ + ; 0# = 0# + ; 1# = 1# + } + record Quasiring c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _*_ infixl 6 _+_ @@ -931,20 +941,33 @@ record RingWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where open IsRingWithoutOne isRingWithoutOne public + nearSemiring : NearSemiring _ _ + nearSemiring = record { isNearSemiring = isNearSemiring } + + open NearSemiring nearSemiring public + using (*-semigroup; *-magma) + +-abelianGroup : AbelianGroup _ _ +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup } - *-semigroup : Semigroup _ _ - *-semigroup = record { isSemigroup = *-isSemigroup } - open AbelianGroup +-abelianGroup public - using () renaming (group to +-group; invertibleMagma to +-invertibleMagma; invertibleUnitalMagma to +-invertibleUnitalMagma) + using () + renaming (group to +-group; + invertibleMagma to +-invertibleMagma; + invertibleUnitalMagma to +-invertibleUnitalMagma) + + rawRingWithoutOne : RawRingWithoutOne _ _ + rawRingWithoutOne = record + { _≈_ = _≈_ + ; _+_ = _+_ + ; _*_ = _*_ + ; -_ = -_ + ; 0# = 0# + } + + open RawRingWithoutOne rawRingWithoutOne public + using (+-rawGroup; *-rawMagma; rawNearSemiring) - open Semigroup *-semigroup public - using () renaming - ( rawMagma to *-rawMagma - ; magma to *-magma - ) ------------------------------------------------------------------------ -- Bundles with 2 binary operations, 1 unary operation & 2 elements diff --git a/src/Algebra/Bundles/Raw.agda b/src/Algebra/Bundles/Raw.agda index 5c99d02790..1947e3846d 100644 --- a/src/Algebra/Bundles/Raw.agda +++ b/src/Algebra/Bundles/Raw.agda @@ -174,6 +174,17 @@ record RawRingWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where -_ : Op₁ Carrier 0# : Carrier + rawNearSemiring : RawNearSemiring c ℓ + rawNearSemiring = record + { _≈_ = _≈_ + ; _+_ = _+_ + ; _*_ = _*_ + ; 0# = 0# + } + + open RawNearSemiring rawNearSemiring public + using (_≉_; *-rawMagma; +-rawMagma; +-rawMonoid) + +-rawGroup : RawGroup c ℓ +-rawGroup = record { _≈_ = _≈_ @@ -182,15 +193,6 @@ record RawRingWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where ; _⁻¹ = -_ } - open RawGroup +-rawGroup public - using (_≉_) renaming (rawMagma to +-rawMagma; rawMonoid to +-rawMonoid) - - *-rawMagma : RawMagma c ℓ - *-rawMagma = record - { _≈_ = _≈_ - ; _∙_ = _*_ - } - ------------------------------------------------------------------------ -- Raw bundles with 2 binary operations, 1 unary operation & 2 elements ------------------------------------------------------------------------ diff --git a/src/Algebra/Morphism/Bundles.agda b/src/Algebra/Morphism/Bundles.agda new file mode 100644 index 0000000000..62f7287d0d --- /dev/null +++ b/src/Algebra/Morphism/Bundles.agda @@ -0,0 +1,257 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Bundled definitions of homomorphisms between algebras +-- +-- NB indexed by Raw bundles, just as IsXHomomorphism is +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Algebra.Morphism.Bundles where + +open import Algebra.Bundles.Raw +open import Algebra.Morphism.Structures +open import Level using (Level; suc; _⊔_) +--open import Relation.Binary.Morphism using (IsRelHomomorphism) +--open import Relation.Binary.Morphism.Bundles using (SetoidHomomorphism) + +private + variable + ℓ a ℓa b ℓb : Level + + +------------------------------------------------------------------------ +-- Morphisms between Magmas +------------------------------------------------------------------------ + +record MagmaHomomorphism + (A : RawMagma a ℓa) (B : RawMagma b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) + where + private + module A = RawMagma A + module B = RawMagma B + + field + ⟦_⟧ : A.Carrier → B.Carrier + + isMagmaHomomorphism : IsMagmaHomomorphism A B ⟦_⟧ + + open IsMagmaHomomorphism isMagmaHomomorphism public + +------------------------------------------------------------------------ +-- Morphisms between Monoids +------------------------------------------------------------------------ + +record MonoidHomomorphism + (A : RawMonoid a ℓa) (B : RawMonoid b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) + where + private + module A = RawMonoid A + module B = RawMonoid B + + field + ⟦_⟧ : A.Carrier → B.Carrier + + isMonoidHomomorphism : IsMonoidHomomorphism A B ⟦_⟧ + + open IsMonoidHomomorphism isMonoidHomomorphism public + + magmaHomomorphism : MagmaHomomorphism A.rawMagma B.rawMagma + magmaHomomorphism = record { isMagmaHomomorphism = isMagmaHomomorphism } + +------------------------------------------------------------------------ +-- Morphisms between Groups +------------------------------------------------------------------------ + +record GroupHomomorphism + (A : RawGroup a ℓa) (B : RawGroup b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) + where + private + module A = RawGroup A + module B = RawGroup B + + field + ⟦_⟧ : A.Carrier → B.Carrier + + isGroupHomomorphism : IsGroupHomomorphism A B ⟦_⟧ + + open IsGroupHomomorphism isGroupHomomorphism public + + monoidHomomorphism : MonoidHomomorphism A.rawMonoid B.rawMonoid + monoidHomomorphism = record { isMonoidHomomorphism = isMonoidHomomorphism } + + open MonoidHomomorphism monoidHomomorphism public + using (magmaHomomorphism) + +------------------------------------------------------------------------ +-- Morphisms between NearSemirings +------------------------------------------------------------------------ + +record NearSemiringHomomorphism + (A : RawNearSemiring a ℓa) (B : RawNearSemiring b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) + where + private + module A = RawNearSemiring A + module B = RawNearSemiring B + + field + ⟦_⟧ : A.Carrier → B.Carrier + + isNearSemiringHomomorphism : IsNearSemiringHomomorphism A B ⟦_⟧ + + open IsNearSemiringHomomorphism isNearSemiringHomomorphism public + + +-monoidHomomorphism : MonoidHomomorphism A.+-rawMonoid B.+-rawMonoid + +-monoidHomomorphism = record { isMonoidHomomorphism = +-isMonoidHomomorphism } + + *-magmaHomomorphism : MagmaHomomorphism A.*-rawMagma B.*-rawMagma + *-magmaHomomorphism = record { isMagmaHomomorphism = *-isMagmaHomomorphism } + + open MonoidHomomorphism +-monoidHomomorphism public + using () + renaming (magmaHomomorphism to +-magmaHomomorphism) + +------------------------------------------------------------------------ +-- Morphisms between Semirings +------------------------------------------------------------------------ + +record SemiringHomomorphism + (A : RawSemiring a ℓa) (B : RawSemiring b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) + where + private + module A = RawSemiring A + module B = RawSemiring B + + field + ⟦_⟧ : A.Carrier → B.Carrier + + isSemiringHomomorphism : IsSemiringHomomorphism A B ⟦_⟧ + + open IsSemiringHomomorphism isSemiringHomomorphism public + + nearSemiringHomomorphism : NearSemiringHomomorphism A.rawNearSemiring B.rawNearSemiring + nearSemiringHomomorphism = record { isNearSemiringHomomorphism = isNearSemiringHomomorphism } + + open NearSemiringHomomorphism nearSemiringHomomorphism public + using (*-magmaHomomorphism; +-monoidHomomorphism; +-magmaHomomorphism) + + *-monoidHomomorphism : MonoidHomomorphism A.*-rawMonoid B.*-rawMonoid + *-monoidHomomorphism = record { isMonoidHomomorphism = *-isMonoidHomomorphism } + +------------------------------------------------------------------------ +-- Morphisms between KleeneAlgebras +------------------------------------------------------------------------ + +record KleeneAlgebraHomomorphism + (A : RawKleeneAlgebra a ℓa) (B : RawKleeneAlgebra b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) + where + private + module A = RawKleeneAlgebra A + module B = RawKleeneAlgebra B + + field + ⟦_⟧ : A.Carrier → B.Carrier + isKleeneAlgebraHomomorphism : IsKleeneAlgebraHomomorphism A B ⟦_⟧ + + open IsKleeneAlgebraHomomorphism isKleeneAlgebraHomomorphism public + + semiringHomomorphism : SemiringHomomorphism A.rawSemiring B.rawSemiring + semiringHomomorphism = record { isSemiringHomomorphism = isSemiringHomomorphism } + + open SemiringHomomorphism semiringHomomorphism public + hiding (*-isMagmaHomomorphism; *-isMonoidHomomorphism) + +------------------------------------------------------------------------ +-- Morphisms between RingWithoutOnes +------------------------------------------------------------------------ + +record RingWithoutOneHomomorphism (A : RawRingWithoutOne a ℓa) (B : RawRingWithoutOne b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where + private + module A = RawRingWithoutOne A + module B = RawRingWithoutOne B + + field + ⟦_⟧ : A.Carrier → B.Carrier + isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism A B ⟦_⟧ + + open IsRingWithoutOneHomomorphism isRingWithoutOneHomomorphism public + + nearSemiringHomomorphism : NearSemiringHomomorphism A.rawNearSemiring B.rawNearSemiring + nearSemiringHomomorphism = record { isNearSemiringHomomorphism = isNearSemiringHomomorphism } + + open NearSemiringHomomorphism nearSemiringHomomorphism public + using (*-magmaHomomorphism; +-magmaHomomorphism; +-monoidHomomorphism) + + +-groupHomomorphism : GroupHomomorphism A.+-rawGroup B.+-rawGroup + +-groupHomomorphism = record { isGroupHomomorphism = +-isGroupHomomorphism } + +------------------------------------------------------------------------ +-- Morphisms between Rings +------------------------------------------------------------------------ + +record RingHomomorphism (A : RawRing a ℓa) (B : RawRing b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where + private + module A = RawRing A + module B = RawRing B + + field + ⟦_⟧ : A.Carrier → B.Carrier + isRingHomomorphism : IsRingHomomorphism A B ⟦_⟧ + + open IsRingHomomorphism isRingHomomorphism public + + ringWithoutOneHomomorphism : RingWithoutOneHomomorphism A.rawRingWithoutOne B.rawRingWithoutOne + ringWithoutOneHomomorphism = record { isRingWithoutOneHomomorphism = isRingWithoutOneHomomorphism } + + open RingWithoutOneHomomorphism ringWithoutOneHomomorphism public + using (+-groupHomomorphism) + + semiringHomomorphism : SemiringHomomorphism A.rawSemiring B.rawSemiring + semiringHomomorphism = record { isSemiringHomomorphism = isSemiringHomomorphism } + + open SemiringHomomorphism semiringHomomorphism public + using ( nearSemiringHomomorphism + ; *-monoidHomomorphism; *-magmaHomomorphism + ; +-monoidHomomorphism; +-magmaHomomorphism) + +------------------------------------------------------------------------ +-- Morphisms between Quasigroups +------------------------------------------------------------------------ + +record QuasigroupHomomorphism + (A : RawQuasigroup a ℓa) (B : RawQuasigroup b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) + where + private + module A = RawQuasigroup A + module B = RawQuasigroup B + + field + ⟦_⟧ : A.Carrier → B.Carrier + isQuasigroupHomomorphism : IsQuasigroupHomomorphism A B ⟦_⟧ + + open IsQuasigroupHomomorphism isQuasigroupHomomorphism public + + magmaHomomorphism : MagmaHomomorphism A.∙-rawMagma B.∙-rawMagma + magmaHomomorphism = record { isMagmaHomomorphism = ∙-isMagmaHomomorphism } + +------------------------------------------------------------------------ +-- Morphisms between Loops +------------------------------------------------------------------------ + +record LoopHomomorphism + (A : RawLoop a ℓa) (B : RawLoop b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) + where + private + module A = RawLoop A + module B = RawLoop B + + field + ⟦_⟧ : A.Carrier → B.Carrier + isLoopHomomorphism : IsLoopHomomorphism A B ⟦_⟧ + + open IsLoopHomomorphism isLoopHomomorphism public + + quasigroupHomomorphism : QuasigroupHomomorphism A.rawQuasigroup B.rawQuasigroup + quasigroupHomomorphism = record { isQuasigroupHomomorphism = isQuasigroupHomomorphism } + diff --git a/src/Algebra/Morphism/Construct/Composition.agda b/src/Algebra/Morphism/Construct/Composition.agda index 17d5f2798b..9a420f3000 100644 --- a/src/Algebra/Morphism/Construct/Composition.agda +++ b/src/Algebra/Morphism/Construct/Composition.agda @@ -9,6 +9,7 @@ module Algebra.Morphism.Construct.Composition where open import Algebra.Bundles +open import Algebra.Morphism.Bundles open import Algebra.Morphism.Structures open import Function.Base using (_∘_) import Function.Construct.Composition as Func @@ -20,6 +21,7 @@ private variable a b c ℓ₁ ℓ₂ ℓ₃ : Level + ------------------------------------------------------------------------ -- Magmas @@ -423,3 +425,187 @@ module _ {K₁ : RawKleeneAlgebra a ℓ₁} ; surjective = Func.surjective (_≈_ K₁) (_≈_ K₂) (_≈_ K₃) F.surjective G.surjective } where module F = IsKleeneAlgebraIsomorphism f-iso; module G = IsKleeneAlgebraIsomorphism g-iso +----------------------------------------------------------------------- +-- Bundled morphisms between algebras +------------------------------------------------------------------------ + +-- Magma + +module _ {M₁ : Magma a ℓ₁} {M₂ : Magma b ℓ₂} {M₃ : Magma c ℓ₃} where + + private + module M₁ = Magma M₁ + module M₂ = Magma M₂ + module M₃ = Magma M₃ + + magmaHomomorphism : (h : MagmaHomomorphism M₁.rawMagma M₂.rawMagma) → + (k : MagmaHomomorphism M₂.rawMagma M₃.rawMagma) → + MagmaHomomorphism M₁.rawMagma M₃.rawMagma + magmaHomomorphism h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isMagmaHomomorphism = isMagmaHomomorphism M₃.trans H.isMagmaHomomorphism K.isMagmaHomomorphism + } + where + module H = MagmaHomomorphism h + module K = MagmaHomomorphism k + +-- Monoid + +module _ {M₁ : Monoid a ℓ₁} {M₂ : Monoid b ℓ₂} {M₃ : Monoid c ℓ₃} where + + private + module M₁ = Monoid M₁ + module M₂ = Monoid M₂ + module M₃ = Monoid M₃ + + monoidHomomorphism : (h : MonoidHomomorphism M₁.rawMonoid M₂.rawMonoid) → + (k : MonoidHomomorphism M₂.rawMonoid M₃.rawMonoid) → + MonoidHomomorphism M₁.rawMonoid M₃.rawMonoid + monoidHomomorphism h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isMonoidHomomorphism = isMonoidHomomorphism M₃.trans H.isMonoidHomomorphism K.isMonoidHomomorphism + } + where + module H = MonoidHomomorphism h + module K = MonoidHomomorphism k + +-- Group + +module _ {M₁ : Group a ℓ₁} {M₂ : Group b ℓ₂} {M₃ : Group c ℓ₃} where + + private + module M₁ = Group M₁ + module M₂ = Group M₂ + module M₃ = Group M₃ + + groupHomomorphism : (h : GroupHomomorphism M₁.rawGroup M₂.rawGroup) → + (k : GroupHomomorphism M₂.rawGroup M₃.rawGroup) → + GroupHomomorphism M₁.rawGroup M₃.rawGroup + groupHomomorphism h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isGroupHomomorphism = isGroupHomomorphism M₃.trans H.isGroupHomomorphism K.isGroupHomomorphism + } + where + module H = GroupHomomorphism h + module K = GroupHomomorphism k + +-- NearSemiring + +module _ {M₁ : NearSemiring a ℓ₁} {M₂ : NearSemiring b ℓ₂} {M₃ : NearSemiring c ℓ₃} where + + private + module M₁ = NearSemiring M₁ + module M₂ = NearSemiring M₂ + module M₃ = NearSemiring M₃ + + nearSemiringHomomorphism : (h : NearSemiringHomomorphism M₁.rawNearSemiring M₂.rawNearSemiring) → + (k : NearSemiringHomomorphism M₂.rawNearSemiring M₃.rawNearSemiring) → + NearSemiringHomomorphism M₁.rawNearSemiring M₃.rawNearSemiring + nearSemiringHomomorphism h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isNearSemiringHomomorphism = isNearSemiringHomomorphism M₃.trans H.isNearSemiringHomomorphism K.isNearSemiringHomomorphism + } + where + module H = NearSemiringHomomorphism h + module K = NearSemiringHomomorphism k + +-- Semiring + +module _ {M₁ : Semiring a ℓ₁} {M₂ : Semiring b ℓ₂} {M₃ : Semiring c ℓ₃} where + + private + module M₁ = Semiring M₁ + module M₂ = Semiring M₂ + module M₃ = Semiring M₃ + + semiringHomomorphism : (h : SemiringHomomorphism M₁.rawSemiring M₂.rawSemiring) → + (k : SemiringHomomorphism M₂.rawSemiring M₃.rawSemiring) → + SemiringHomomorphism M₁.rawSemiring M₃.rawSemiring + semiringHomomorphism h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isSemiringHomomorphism = isSemiringHomomorphism M₃.trans H.isSemiringHomomorphism K.isSemiringHomomorphism + } + where + module H = SemiringHomomorphism h + module K = SemiringHomomorphism k + +-- RingWithoutOne + +module _ {M₁ : RingWithoutOne a ℓ₁} {M₂ : RingWithoutOne b ℓ₂} {M₃ : RingWithoutOne c ℓ₃} where + + private + module M₁ = RingWithoutOne M₁ + module M₂ = RingWithoutOne M₂ + module M₃ = RingWithoutOne M₃ + + ringWithoutOneHomomorphism : (h : RingWithoutOneHomomorphism M₁.rawRingWithoutOne M₂.rawRingWithoutOne) → + (k : RingWithoutOneHomomorphism M₂.rawRingWithoutOne M₃.rawRingWithoutOne) → + RingWithoutOneHomomorphism M₁.rawRingWithoutOne M₃.rawRingWithoutOne + ringWithoutOneHomomorphism h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isRingWithoutOneHomomorphism = isRingWithoutOneHomomorphism M₃.trans H.isRingWithoutOneHomomorphism K.isRingWithoutOneHomomorphism + } + where + module H = RingWithoutOneHomomorphism h + module K = RingWithoutOneHomomorphism k + +-- Ring + +module _ {M₁ : Ring a ℓ₁} {M₂ : Ring b ℓ₂} {M₃ : Ring c ℓ₃} where + + private + module M₁ = Ring M₁ + module M₂ = Ring M₂ + module M₃ = Ring M₃ + + ringHomomorphism : (h : RingHomomorphism M₁.rawRing M₂.rawRing) → + (k : RingHomomorphism M₂.rawRing M₃.rawRing) → + RingHomomorphism M₁.rawRing M₃.rawRing + ringHomomorphism h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isRingHomomorphism = isRingHomomorphism M₃.trans H.isRingHomomorphism K.isRingHomomorphism + } + where + module H = RingHomomorphism h + module K = RingHomomorphism k + +-- Quasigroup + +module _ {M₁ : Quasigroup a ℓ₁} {M₂ : Quasigroup b ℓ₂} {M₃ : Quasigroup c ℓ₃} where + + private + module M₁ = Quasigroup M₁ + module M₂ = Quasigroup M₂ + module M₃ = Quasigroup M₃ + + quasigroupHomomorphism : (h : QuasigroupHomomorphism M₁.rawQuasigroup M₂.rawQuasigroup) → + (k : QuasigroupHomomorphism M₂.rawQuasigroup M₃.rawQuasigroup) → + QuasigroupHomomorphism M₁.rawQuasigroup M₃.rawQuasigroup + quasigroupHomomorphism h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isQuasigroupHomomorphism = isQuasigroupHomomorphism M₃.trans H.isQuasigroupHomomorphism K.isQuasigroupHomomorphism + } + where + module H = QuasigroupHomomorphism h + module K = QuasigroupHomomorphism k + +-- Loop + +module _ {M₁ : Loop a ℓ₁} {M₂ : Loop b ℓ₂} {M₃ : Loop c ℓ₃} where + + private + module M₁ = Loop M₁ + module M₂ = Loop M₂ + module M₃ = Loop M₃ + + loopHomomorphism : (h : LoopHomomorphism M₁.rawLoop M₂.rawLoop) → + (k : LoopHomomorphism M₂.rawLoop M₃.rawLoop) → + LoopHomomorphism M₁.rawLoop M₃.rawLoop + loopHomomorphism h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isLoopHomomorphism = isLoopHomomorphism M₃.trans H.isLoopHomomorphism K.isLoopHomomorphism + } + where + module H = LoopHomomorphism h + module K = LoopHomomorphism k + diff --git a/src/Algebra/Morphism/Construct/Identity.agda b/src/Algebra/Morphism/Construct/Identity.agda index 881a8cf15c..d6032ecbe7 100644 --- a/src/Algebra/Morphism/Construct/Identity.agda +++ b/src/Algebra/Morphism/Construct/Identity.agda @@ -9,6 +9,7 @@ module Algebra.Morphism.Construct.Identity where open import Algebra.Bundles +open import Algebra.Morphism.Bundles open import Algebra.Morphism.Structures using ( module MagmaMorphisms ; module MonoidMorphisms @@ -21,7 +22,6 @@ open import Algebra.Morphism.Structures ; module LoopMorphisms ; module KleeneAlgebraMorphisms ) -open import Data.Product.Base using (_,_) open import Function.Base using (id) import Function.Construct.Identity as Id open import Level using (Level) @@ -32,6 +32,7 @@ private variable c ℓ : Level + ------------------------------------------------------------------------ -- Magmas @@ -274,3 +275,138 @@ module _ (K : RawKleeneAlgebra c ℓ) (open RawKleeneAlgebra K) (refl : Reflexiv ; surjective = Id.surjective _ } + +------------------------------------------------------------------------ +--- Bundled morphisms between algebras +----------------------------------------------------------------------- + +-- Magma + +module _ (M : Magma c ℓ) where + + open Magma M using (rawMagma; refl) + open MagmaMorphisms rawMagma rawMagma + + magmaHomomorphism : MagmaHomomorphism rawMagma rawMagma + magmaHomomorphism = record + { ⟦_⟧ = id + ; isMagmaHomomorphism = isMagmaHomomorphism rawMagma refl + } + +-- Monoid + +module _ (M : Monoid c ℓ) where + + open Monoid M using (rawMonoid; refl) + open MonoidMorphisms rawMonoid rawMonoid + + monoidHomomorphism : MonoidHomomorphism rawMonoid rawMonoid + monoidHomomorphism = record + { ⟦_⟧ = id + ; isMonoidHomomorphism = isMonoidHomomorphism rawMonoid refl + } + +-- Group + +module _ (M : Group c ℓ) where + + open Group M using (rawGroup; refl) + open GroupMorphisms rawGroup rawGroup + + groupHomomorphism : GroupHomomorphism rawGroup rawGroup + groupHomomorphism = record + { ⟦_⟧ = id + ; isGroupHomomorphism = isGroupHomomorphism rawGroup refl + } + +-- NearSemiring + +module _ (M : NearSemiring c ℓ) where + + open NearSemiring M using (rawNearSemiring; refl) + open NearSemiringMorphisms rawNearSemiring rawNearSemiring + + nearSemiringHomomorphism : NearSemiringHomomorphism rawNearSemiring rawNearSemiring + nearSemiringHomomorphism = record + { ⟦_⟧ = id + ; isNearSemiringHomomorphism = isNearSemiringHomomorphism rawNearSemiring refl + } + +-- Semiring + +module _ (M : Semiring c ℓ) where + + open Semiring M using (rawSemiring; refl) + open SemiringMorphisms rawSemiring rawSemiring + + semiringHomomorphism : SemiringHomomorphism rawSemiring rawSemiring + semiringHomomorphism = record + { ⟦_⟧ = id + ; isSemiringHomomorphism = isSemiringHomomorphism rawSemiring refl + } + +-- KleeneAlgebra + +module _ (M : KleeneAlgebra c ℓ) where + + open KleeneAlgebra M using (rawKleeneAlgebra; refl) + open KleeneAlgebraMorphisms rawKleeneAlgebra rawKleeneAlgebra + + kleeneAlgebraHomomorphism : KleeneAlgebraHomomorphism rawKleeneAlgebra rawKleeneAlgebra + kleeneAlgebraHomomorphism = record + { ⟦_⟧ = id + ; isKleeneAlgebraHomomorphism = isKleeneAlgebraHomomorphism rawKleeneAlgebra refl + } + +-- RingWithoutOne + +module _ (M : RingWithoutOne c ℓ) where + + open RingWithoutOne M using (rawRingWithoutOne; refl) + open RingWithoutOneMorphisms rawRingWithoutOne rawRingWithoutOne + + ringWithoutOneHomomorphism : RingWithoutOneHomomorphism rawRingWithoutOne rawRingWithoutOne + ringWithoutOneHomomorphism = record + { ⟦_⟧ = id + ; isRingWithoutOneHomomorphism = isRingWithoutOneHomomorphism rawRingWithoutOne refl + } + +-- Ring + +module _ (M : Ring c ℓ) where + + open Ring M using (rawRing; refl) + open RingMorphisms rawRing rawRing + + ringHomomorphism : RingHomomorphism rawRing rawRing + ringHomomorphism = record + { ⟦_⟧ = id + ; isRingHomomorphism = isRingHomomorphism rawRing refl + } + +-- Quasigroup + +module _ (M : Quasigroup c ℓ) where + + open Quasigroup M using (rawQuasigroup; refl) + open QuasigroupMorphisms rawQuasigroup rawQuasigroup + + quasigroupHomomorphism : QuasigroupHomomorphism rawQuasigroup rawQuasigroup + quasigroupHomomorphism = record + { ⟦_⟧ = id + ; isQuasigroupHomomorphism = isQuasigroupHomomorphism rawQuasigroup refl + } + +-- Loop + +module _ (M : Loop c ℓ) where + + open Loop M using (rawLoop; refl) + open LoopMorphisms rawLoop rawLoop + + loopHomomorphism : LoopHomomorphism rawLoop rawLoop + loopHomomorphism = record + { ⟦_⟧ = id + ; isLoopHomomorphism = isLoopHomomorphism rawLoop refl + } + diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda index c352904be7..08d091d72a 100644 --- a/src/Algebra/Morphism/Structures.agda +++ b/src/Algebra/Morphism/Structures.agda @@ -405,17 +405,20 @@ module RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRi ( Carrier to A; _≈_ to _≈₁_ ; _*_ to _*₁_ ; *-rawMagma to *-rawMagma₁ - ; +-rawGroup to +-rawGroup₁) + ; +-rawGroup to +-rawGroup₁ + ; rawNearSemiring to rawNearSemiring₁) open RawRingWithoutOne R₂ renaming ( Carrier to B; _≈_ to _≈₂_ ; _*_ to _*₂_ ; *-rawMagma to *-rawMagma₂ - ; +-rawGroup to +-rawGroup₂) + ; +-rawGroup to +-rawGroup₂ + ; rawNearSemiring to rawNearSemiring₂) private module + = GroupMorphisms +-rawGroup₁ +-rawGroup₂ module * = MagmaMorphisms *-rawMagma₁ *-rawMagma₂ + module +* = NearSemiringMorphisms rawNearSemiring₁ rawNearSemiring₂ open MorphismDefinitions A B _≈₂_ @@ -425,7 +428,13 @@ module RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRi *-homo : Homomorphic₂ ⟦_⟧ _*₁_ _*₂_ open +.IsGroupHomomorphism +-isGroupHomomorphism public - renaming (homo to +-homo; ε-homo to 0#-homo; isMagmaHomomorphism to +-isMagmaHomomorphism) + renaming (homo to +-homo; ε-homo to 0#-homo; isMagmaHomomorphism to +-isMagmaHomomorphism; isMonoidHomomorphism to +-isMonoidHomomorphism) + + isNearSemiringHomomorphism : +*.IsNearSemiringHomomorphism ⟦_⟧ + isNearSemiringHomomorphism = record + { +-isMonoidHomomorphism = +-isMonoidHomomorphism + ; *-homo = *-homo + } *-isMagmaHomomorphism : *.IsMagmaHomomorphism ⟦_⟧ *-isMagmaHomomorphism = record @@ -489,6 +498,7 @@ module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where open RawRing R₁ renaming ( Carrier to A; _≈_ to _≈₁_ ; -_ to -₁_ + ; rawRingWithoutOne to rawRingWithoutOne₁ ; rawSemiring to rawSemiring₁ ; *-rawMonoid to *-rawMonoid₁ ; +-rawGroup to +-rawGroup₁) @@ -496,12 +506,14 @@ module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where open RawRing R₂ renaming ( Carrier to B; _≈_ to _≈₂_ ; -_ to -₂_ + ; rawRingWithoutOne to rawRingWithoutOne₂ ; rawSemiring to rawSemiring₂ ; *-rawMonoid to *-rawMonoid₂ ; +-rawGroup to +-rawGroup₂) module + = GroupMorphisms +-rawGroup₁ +-rawGroup₂ module * = MonoidMorphisms *-rawMonoid₁ *-rawMonoid₂ + module *+0 = RingWithoutOneMorphisms rawRingWithoutOne₁ rawRingWithoutOne₂ open MorphismDefinitions A B _≈₂_ open SemiringMorphisms rawSemiring₁ rawSemiring₂ @@ -520,6 +532,12 @@ module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where ; ⁻¹-homo = -‿homo } + isRingWithoutOneHomomorphism : *+0.IsRingWithoutOneHomomorphism ⟦_⟧ + isRingWithoutOneHomomorphism = record + { +-isGroupHomomorphism = +-isGroupHomomorphism + ; *-homo = *-homo + } + record IsRingMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isRingHomomorphism : IsRingHomomorphism ⟦_⟧ diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index b58245e6df..9653c6d895 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -770,24 +770,17 @@ record IsRingWithoutOne (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ zero : Zero 0# * zero = zeroˡ , zeroʳ - *-isMagma : IsMagma * - *-isMagma = record - { isEquivalence = isEquivalence - ; ∙-cong = *-cong - } - - *-isSemigroup : IsSemigroup * - *-isSemigroup = record - { isMagma = *-isMagma - ; assoc = *-assoc + isNearSemiring : IsNearSemiring + * 0# + isNearSemiring = record + { +-isMonoid = +-isMonoid + ; *-cong = *-cong + ; *-assoc = *-assoc + ; distribʳ = distribʳ + ; zeroˡ = zeroˡ } - open IsSemigroup *-isSemigroup public - using () - renaming - ( ∙-congˡ to *-congˡ - ; ∙-congʳ to *-congʳ - ) + open IsNearSemiring isNearSemiring public + using (*-isMagma; *-isSemigroup; *-congˡ; *-congʳ) ------------------------------------------------------------------------ -- Structures with 2 binary operations, 1 unary operation & 2 elements @@ -928,7 +921,7 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where } open IsSemiring isSemiring public - using (isNearSemiring; isSemiringWithoutOne) + using (isSemiringWithoutOne) record IsCommutativeRing