From ad219357602ff53eefd2906a817227581e2f7ecf Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 14 Feb 2024 20:56:10 +0000 Subject: [PATCH] added unique morphisms --- CHANGELOG.md | 6 ++ src/Algebra/Construct/Terminal.agda | 2 +- src/Algebra/Morphism/Construct/Initial.agda | 73 +++++++++++++++ src/Algebra/Morphism/Construct/Terminal.agda | 98 ++++++++++++++++++++ 4 files changed, 178 insertions(+), 1 deletion(-) create mode 100644 src/Algebra/Morphism/Construct/Initial.agda create mode 100644 src/Algebra/Morphism/Construct/Terminal.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 7fa21bf90e..7ae7926863 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -48,6 +48,12 @@ New modules * `Algebra.Module.Bundles.Raw`: raw bundles for module-like algebraic structures +* The unique morphism from the initial, resp. terminal, algebra: + ```agda + Algebra.Morphism.Construct.Initial + Algebra.Morphism.Construct.Terminal + ``` + Additions to existing modules ----------------------------- diff --git a/src/Algebra/Construct/Terminal.agda b/src/Algebra/Construct/Terminal.agda index 4a6f1decfe..005b47eaf7 100644 --- a/src/Algebra/Construct/Terminal.agda +++ b/src/Algebra/Construct/Terminal.agda @@ -27,7 +27,7 @@ module 𝕆ne where Carrier : Set c Carrier = ⊤ - _≈_ : Rel Carrier ℓ + _≈_ : Rel Carrier ℓ _ ≈ _ = ⊤ ------------------------------------------------------------------------ diff --git a/src/Algebra/Morphism/Construct/Initial.agda b/src/Algebra/Morphism/Construct/Initial.agda new file mode 100644 index 0000000000..cdba43115c --- /dev/null +++ b/src/Algebra/Morphism/Construct/Initial.agda @@ -0,0 +1,73 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- The unique morphism from the initial object, +-- for each of the relevant categories. Since +-- `Semigroup` and `Band` are simply `Magma`s +-- satisfying additional properties, it suffices to +-- define the morphism on the underlying `RawMagma`. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Level using (Level) + +module Algebra.Morphism.Construct.Initial {c ℓ : Level} where + +open import Algebra.Bundles using (Magma) +open import Algebra.Bundles.Raw using (RawMagma) +open import Algebra.Construct.Initial {c} {ℓ} +import Algebra.Morphism.Definitions as MorphismDefinitions +open import Algebra.Morphism.Structures using (module MagmaMorphisms) +open import Function.Definitions using (Injective) +import Relation.Binary.Morphism.Definitions as Definitions +open import Relation.Binary.Morphism.Structures + +private + variable + m ℓm : Level + + +------------------------------------------------------------------------ +-- The underlying data of the morphism + +module ℤeroMorphism (M : RawMagma m ℓm) where + + open RawMagma M + open MorphismDefinitions ℤero.Carrier Carrier _≈_ + + zero : ℤero.Carrier → Carrier + zero () + + cong : Definitions.Homomorphic₂ ℤero.Carrier Carrier ℤero._≈_ _≈_ zero + cong {x = ()} + + isRelHomomorphism : IsRelHomomorphism ℤero._≈_ _≈_ zero + isRelHomomorphism = record { cong = cong } + + homo : Homomorphic₂ zero ℤero._∙_ _∙_ + homo () + + injective : Injective ℤero._≈_ _≈_ zero + injective {x = ()} + +------------------------------------------------------------------------ +-- Magma + +module _ (M : Magma m ℓm) where + + private module M = Magma M + open MagmaMorphisms rawMagma M.rawMagma + open ℤeroMorphism M.rawMagma + + isMagmaHomomorphism : IsMagmaHomomorphism zero + isMagmaHomomorphism = record + { isRelHomomorphism = isRelHomomorphism + ; homo = homo + } + + isMagmaMonomorphism : IsMagmaMonomorphism zero + isMagmaMonomorphism = record + { isMagmaHomomorphism = isMagmaHomomorphism + ; injective = injective + } diff --git a/src/Algebra/Morphism/Construct/Terminal.agda b/src/Algebra/Morphism/Construct/Terminal.agda new file mode 100644 index 0000000000..986a778977 --- /dev/null +++ b/src/Algebra/Morphism/Construct/Terminal.agda @@ -0,0 +1,98 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- The unique morphism to the terminal object, +-- for each of the relevant categories. Since +-- each terminal algebra builds on `Monoid`, +-- possibly with additional (trivial) operations, +-- satisfying additional properties, it suffices to +-- define the morphism on the underlying `RawMonoid` +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Level using (Level) + +module Algebra.Morphism.Construct.Terminal {c ℓ : Level} where + +open import Algebra.Bundles using (Monoid; Group) +open import Algebra.Bundles.Raw using (RawMonoid; RawGroup) +open import Algebra.Construct.Terminal {c} {ℓ} +import Algebra.Morphism.Definitions as MorphismDefinitions +open import Algebra.Morphism.Structures + using ( module MagmaMorphisms + ; module MonoidMorphisms + ; module GroupMorphisms + ) +open import Data.Product.Base using (_,_) +open import Function.Definitions using (StrictlySurjective) +import Relation.Binary.Morphism.Definitions as Definitions +open import Relation.Binary.Morphism.Structures + +private + variable + a ℓa : Level + + +------------------------------------------------------------------------ +-- The underlying data of the morphism + +module 𝕆neMorphism (M : RawMonoid a ℓa) where + + open RawMonoid M + open MorphismDefinitions Carrier 𝕆ne.Carrier 𝕆ne._≈_ + + one : Carrier → 𝕆ne.Carrier + one _ = _ + + cong : Definitions.Homomorphic₂ Carrier 𝕆ne.Carrier _≈_ 𝕆ne._≈_ one + cong _ = _ + + isRelHomomorphism : IsRelHomomorphism _≈_ 𝕆ne._≈_ one + isRelHomomorphism = record { cong = cong } + + homo : Homomorphic₂ one _∙_ _ + homo _ = _ + + ε-homo : Homomorphic₀ one ε _ + ε-homo = _ + + strictlySurjective : StrictlySurjective 𝕆ne._≈_ one + strictlySurjective _ = ε , _ + +------------------------------------------------------------------------ +-- Monoid + +module _ (M : Monoid a ℓa) where + + private module M = Monoid M + open MonoidMorphisms M.rawMonoid rawMonoid + open MagmaMorphisms M.rawMagma rawMagma + open 𝕆neMorphism M.rawMonoid + + isMagmaHomomorphism : IsMagmaHomomorphism one + isMagmaHomomorphism = record + { isRelHomomorphism = isRelHomomorphism + ; homo = homo + } + + isMonoidHomomorphism : IsMonoidHomomorphism one + isMonoidHomomorphism = record + { isMagmaHomomorphism = isMagmaHomomorphism + ; ε-homo = ε-homo + } + +------------------------------------------------------------------------ +-- Group + +module _ (G : Group a ℓa) where + + private module G = Group G + open GroupMorphisms G.rawGroup rawGroup + open 𝕆neMorphism G.rawMonoid + + isGroupHomomorphism : IsGroupHomomorphism one + isGroupHomomorphism = record + { isMonoidHomomorphism = isMonoidHomomorphism G.monoid + ; ⁻¹-homo = λ _ → _ + }