From 4529e73b3dbf4531a70c72f11eef3fc584a18f2f Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Sat, 16 Mar 2024 02:28:35 +0000 Subject: [PATCH] Add unique morphisms from/to `Initial` and `Terminal` algebras (#2296) * added unique morphisms * refactored for uniformity's sake * exploit the uniformity * add missing instances * finish up, for now * `CHANGELOG` * `CHANGELOG` * `TheMorphism` * comment * comment * comment * `The` to `Unique` * lifted out istantiated `import` * blank line * note on instantiated `import`s * parametrise on the `Raw` bundle * parametrise on the `Raw` bundle * Rerranged to get rid of lots of boilerplate --------- Co-authored-by: MatthewDaggitt --- CHANGELOG.md | 12 +++ doc/style-guide.md | 4 + src/Algebra/Construct/Initial.agda | 4 +- src/Algebra/Construct/Terminal.agda | 12 ++- src/Algebra/Construct/Zero.agda | 4 +- src/Algebra/Morphism/Construct/Initial.agda | 62 ++++++++++++++ src/Algebra/Morphism/Construct/Terminal.agda | 88 ++++++++++++++++++++ 7 files changed, 179 insertions(+), 7 deletions(-) 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 82c677d186..b780aa6e1f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -50,6 +50,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 + ``` + * Nagata's construction of the "idealization of a module": ```agda Algebra.Module.Construct.Idealization @@ -117,6 +123,12 @@ Additions to existing modules rawModule : RawModule R c ℓ ``` +* In `Algebra.Construct.Terminal`: + ```agda + rawNearSemiring : RawNearSemiring c ℓ + nearSemiring : NearSemiring c ℓ + ``` + * In `Algebra.Properties.Monoid.Mult`: ```agda ×-homo-0 : ∀ x → 0 × x ≈ 0# diff --git a/doc/style-guide.md b/doc/style-guide.md index b2ee87d8ee..254a7ec071 100644 --- a/doc/style-guide.md +++ b/doc/style-guide.md @@ -131,6 +131,10 @@ automate most of this. open SetoidEquality S ``` +* If importing a parametrised module, qualified or otherwise, with its + parameters instantiated, then such 'instantiated imports' should be placed + *after* the main block of `import`s, and *before* any `variable` declarations. + * Naming conventions for qualified `import`s: if importing a module under a root of the form `Data.X` (e.g. the `Base` module for basic operations, or `Properties` for lemmas about them etc.) then conventionally, the diff --git a/src/Algebra/Construct/Initial.agda b/src/Algebra/Construct/Initial.agda index 99d80b98a3..57648d6735 100644 --- a/src/Algebra/Construct/Initial.agda +++ b/src/Algebra/Construct/Initial.agda @@ -4,8 +4,8 @@ -- Instances of algebraic structures where the carrier is ⊥. -- In mathematics, this is usually called 0. -- --- From monoids up, these are zero-objects – i.e, the initial --- object is the terminal object in the relevant category. +-- From monoids up, these are zero-objects – i.e, the terminal +-- object is *also* the initial object in the relevant category. ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} diff --git a/src/Algebra/Construct/Terminal.agda b/src/Algebra/Construct/Terminal.agda index 4a6f1decfe..202982da50 100644 --- a/src/Algebra/Construct/Terminal.agda +++ b/src/Algebra/Construct/Terminal.agda @@ -1,8 +1,8 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Instances of algebraic structures where the carrier is ⊤. --- In mathematics, this is usually called 0 (1 in the case of Group). +-- Instances of algebraic structures where the carrier is ⊤. In +-- mathematics, this is usually called 0 (1 in the case of Monoid, Group). -- -- From monoids up, these are zero-objects – i.e, both the initial -- and the terminal object in the relevant category. @@ -27,7 +27,7 @@ module 𝕆ne where Carrier : Set c Carrier = ⊤ - _≈_ : Rel Carrier ℓ + _≈_ : Rel Carrier ℓ _ ≈ _ = ⊤ ------------------------------------------------------------------------ @@ -42,6 +42,9 @@ rawMonoid = record { 𝕆ne } rawGroup : RawGroup c ℓ rawGroup = record { 𝕆ne } +rawNearSemiring : RawNearSemiring c ℓ +rawNearSemiring = record { 𝕆ne } + rawSemiring : RawSemiring c ℓ rawSemiring = record { 𝕆ne } @@ -78,6 +81,9 @@ group = record { 𝕆ne } abelianGroup : AbelianGroup c ℓ abelianGroup = record { 𝕆ne } +nearSemiring : NearSemiring c ℓ +nearSemiring = record { 𝕆ne } + semiring : Semiring c ℓ semiring = record { 𝕆ne } diff --git a/src/Algebra/Construct/Zero.agda b/src/Algebra/Construct/Zero.agda index 912c3c1e8d..38bfb59b13 100644 --- a/src/Algebra/Construct/Zero.agda +++ b/src/Algebra/Construct/Zero.agda @@ -1,8 +1,8 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Instances of algebraic structures where the carrier is ⊤. --- In mathematics, this is usually called 0 (1 in the case of Group). +-- Instances of algebraic structures where the carrier is ⊤. In +-- mathematics, this is usually called 0 (1 in the case of Monoid, Group). -- -- From monoids up, these are are zero-objects – i.e, both the initial -- and the terminal object in the relevant category. diff --git a/src/Algebra/Morphism/Construct/Initial.agda b/src/Algebra/Morphism/Construct/Initial.agda new file mode 100644 index 0000000000..916e181030 --- /dev/null +++ b/src/Algebra/Morphism/Construct/Initial.agda @@ -0,0 +1,62 @@ +------------------------------------------------------------------------ +-- 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.Raw using (RawMagma) +open import Algebra.Morphism.Structures +open import Function.Definitions using (Injective) +import Relation.Binary.Morphism.Definitions as Rel +open import Relation.Binary.Morphism.Structures +open import Relation.Binary.Core using (Rel) + +open import Algebra.Construct.Initial {c} {ℓ} + +private + variable + a m ℓm : Level + A : Set a + ≈ : Rel A ℓm + +------------------------------------------------------------------------ +-- The unique morphism + +zero : ℤero.Carrier → A +zero () + +------------------------------------------------------------------------ +-- Basic properties + +cong : (≈ : Rel A ℓm) → Rel.Homomorphic₂ ℤero.Carrier A ℤero._≈_ ≈ zero +cong _ {x = ()} + +injective : (≈ : Rel A ℓm) → Injective ℤero._≈_ ≈ zero +injective _ {x = ()} + +------------------------------------------------------------------------ +-- Morphism structures + +isMagmaHomomorphism : (M : RawMagma m ℓm) → + IsMagmaHomomorphism rawMagma M zero +isMagmaHomomorphism M = record + { isRelHomomorphism = record { cong = cong (RawMagma._≈_ M) } + ; homo = λ() + } + +isMagmaMonomorphism : (M : RawMagma m ℓm) → + IsMagmaMonomorphism rawMagma M zero +isMagmaMonomorphism M = record + { isMagmaHomomorphism = isMagmaHomomorphism M + ; injective = injective (RawMagma._≈_ M) + } diff --git a/src/Algebra/Morphism/Construct/Terminal.agda b/src/Algebra/Morphism/Construct/Terminal.agda new file mode 100644 index 0000000000..227ebf2887 --- /dev/null +++ b/src/Algebra/Morphism/Construct/Terminal.agda @@ -0,0 +1,88 @@ +------------------------------------------------------------------------ +-- 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.Raw + using (RawMagma; RawMonoid; RawGroup; RawNearSemiring; RawSemiring; RawRing) +open import Algebra.Morphism.Structures + +open import Data.Product.Base using (_,_) +open import Function.Definitions using (StrictlySurjective) +import Relation.Binary.Morphism.Definitions as Rel +open import Relation.Binary.Morphism.Structures + +open import Algebra.Construct.Terminal {c} {ℓ} + +private + variable + a ℓa : Level + A : Set a + +------------------------------------------------------------------------ +-- The unique morphism + +one : A → 𝕆ne.Carrier +one _ = _ + +------------------------------------------------------------------------ +-- Basic properties + +strictlySurjective : A → StrictlySurjective 𝕆ne._≈_ one +strictlySurjective x _ = x , _ + +------------------------------------------------------------------------ +-- Homomorphisms + +isMagmaHomomorphism : (M : RawMagma a ℓa) → + IsMagmaHomomorphism M rawMagma one +isMagmaHomomorphism M = record + { isRelHomomorphism = record { cong = _ } + ; homo = _ + } + +isMonoidHomomorphism : (M : RawMonoid a ℓa) → + IsMonoidHomomorphism M rawMonoid one +isMonoidHomomorphism M = record + { isMagmaHomomorphism = isMagmaHomomorphism (RawMonoid.rawMagma M) + ; ε-homo = _ + } + +isGroupHomomorphism : (G : RawGroup a ℓa) → + IsGroupHomomorphism G rawGroup one +isGroupHomomorphism G = record + { isMonoidHomomorphism = isMonoidHomomorphism (RawGroup.rawMonoid G) + ; ⁻¹-homo = λ _ → _ + } + +isNearSemiringHomomorphism : (N : RawNearSemiring a ℓa) → + IsNearSemiringHomomorphism N rawNearSemiring one +isNearSemiringHomomorphism N = record + { +-isMonoidHomomorphism = isMonoidHomomorphism (RawNearSemiring.+-rawMonoid N) + ; *-homo = λ _ _ → _ + } + +isSemiringHomomorphism : (S : RawSemiring a ℓa) → + IsSemiringHomomorphism S rawSemiring one +isSemiringHomomorphism S = record + { isNearSemiringHomomorphism = isNearSemiringHomomorphism (RawSemiring.rawNearSemiring S) + ; 1#-homo = _ + } + +isRingHomomorphism : (R : RawRing a ℓa) → IsRingHomomorphism R rawRing one +isRingHomomorphism R = record + { isSemiringHomomorphism = isSemiringHomomorphism (RawRing.rawSemiring R) + ; -‿homo = λ _ → _ + }