diff --git a/CHANGELOG.md b/CHANGELOG.md index 76ca38cd42..305c68f923 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -835,6 +835,8 @@ Major improvements * `RawRing` * `RawQuasigroup` * `RawLoop` +* A new definition is also introduced: + * `RawPointed` * A new module `Algebra.Lattice.Bundles.Raw` is also introduced. * `RawLattice` has been moved from `Algebra.Lattice.Bundles` to this new module. @@ -1563,6 +1565,7 @@ Other minor changes * Added new definitions to `Algebra.Bundles`: ```agda + record Pointed c ℓ : Set (suc (c ⊔ ℓ)) record UnitalMagma c ℓ : Set (suc (c ⊔ ℓ)) record InvertibleMagma c ℓ : Set (suc (c ⊔ ℓ)) record InvertibleUnitalMagma c ℓ : Set (suc (c ⊔ ℓ)) @@ -1756,6 +1759,7 @@ Other minor changes * Added new definitions to `Algebra.Structures`: ```agda + record IsPointed (e : A) : Set (a ⊔ ℓ) record IsUnitalMagma (_∙_ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) record IsInvertibleMagma (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) record IsInvertibleUnitalMagma (_∙_ : Op₂ A) (ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ) @@ -1786,6 +1790,9 @@ Other minor changes * Added new records to `Algebra.Morphism.Structures`: ```agda + record IsPointedHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) + record IsPointedMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) + record IsPointedIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) record IsQuasigroupHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) record IsQuasigroupMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) record IsQuasigroupIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index 2598fde953..5a62509b1f 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -23,11 +23,31 @@ open import Level -- Re-export definitions of 'raw' bundles open Raw public - using (RawMagma; RawMonoid; RawGroup + using (RawPointed; RawMagma; RawMonoid; RawGroup ; RawNearSemiring; RawSemiring ; RawRingWithoutOne; RawRing ; RawQuasigroup; RawLoop) +------------------------------------------------------------------------ +-- Bundles with 1 element +------------------------------------------------------------------------ + +record Pointed c ℓ : Set (suc (c ⊔ ℓ)) where + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + pt₀ : Carrier + isPointed : IsPointed _≈_ pt₀ + + open IsPointed isPointed public + + rawPointed : RawPointed _ _ + rawPointed = record { _≈_ = _≈_; pt₀ = pt₀ } + + open RawPointed rawPointed public + using (_≉_) + ------------------------------------------------------------------------ -- Bundles with 1 binary operation ------------------------------------------------------------------------ diff --git a/src/Algebra/Bundles/Raw.agda b/src/Algebra/Bundles/Raw.agda index e7f9be1349..bdfb2bf802 100644 --- a/src/Algebra/Bundles/Raw.agda +++ b/src/Algebra/Bundles/Raw.agda @@ -17,6 +17,21 @@ open import Relation.Nullary.Negation.Core using (¬_) -- Raw bundles with 1 binary operation ------------------------------------------------------------------------ +record RawPointed c ℓ : Set (suc (c ⊔ ℓ)) where + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + pt₀ : Carrier + + infix 4 _≉_ + _≉_ : Rel Carrier _ + x ≉ y = ¬ (x ≈ y) + +------------------------------------------------------------------------ +-- Raw bundles with 1 binary operation +------------------------------------------------------------------------ + record RawMagma c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ diff --git a/src/Algebra/Morphism/Construct/Composition.agda b/src/Algebra/Morphism/Construct/Composition.agda index 991fb93433..8fea828b0e 100644 --- a/src/Algebra/Morphism/Construct/Composition.agda +++ b/src/Algebra/Morphism/Construct/Composition.agda @@ -21,6 +21,46 @@ private variable a b c ℓ₁ ℓ₂ ℓ₃ : Level +------------------------------------------------------------------------ +-- Pointeds + +module _ {P₁ : RawPointed a ℓ₁} + {P₂ : RawPointed b ℓ₂} + {P₃ : RawPointed c ℓ₃} + (open RawPointed) + (≈₃-trans : Transitive (_≈_ P₃)) + {f : Carrier P₁ → Carrier P₂} + {g : Carrier P₂ → Carrier P₃} + where + + isPointedHomomorphism + : IsPointedHomomorphism P₁ P₂ f + → IsPointedHomomorphism P₂ P₃ g + → IsPointedHomomorphism P₁ P₃ (g ∘ f) + isPointedHomomorphism f-homo g-homo = record + { isRelHomomorphism = isRelHomomorphism F.isRelHomomorphism G.isRelHomomorphism + ; homo = ≈₃-trans (G.⟦⟧-cong F.homo) G.homo + } where module F = IsPointedHomomorphism f-homo; module G = IsPointedHomomorphism g-homo + + isPointedMonomorphism + : IsPointedMonomorphism P₁ P₂ f + → IsPointedMonomorphism P₂ P₃ g + → IsPointedMonomorphism P₁ P₃ (g ∘ f) + isPointedMonomorphism f-mono g-mono = record + { isPointedHomomorphism = isPointedHomomorphism F.isPointedHomomorphism G.isPointedHomomorphism + ; injective = F.injective ∘ G.injective + } where module F = IsPointedMonomorphism f-mono; module G = IsPointedMonomorphism g-mono + + isPointedIsomorphism + : IsPointedIsomorphism P₁ P₂ f + → IsPointedIsomorphism P₂ P₃ g + → IsPointedIsomorphism P₁ P₃ (g ∘ f) + isPointedIsomorphism f-iso g-iso = record + { isPointedMonomorphism = isPointedMonomorphism F.isPointedMonomorphism G.isPointedMonomorphism + ; surjective = Func.surjective (_≈_ P₁) _ _ ≈₃-trans G.⟦⟧-cong F.surjective G.surjective + } where module F = IsPointedIsomorphism f-iso; module G = IsPointedIsomorphism g-iso + + ------------------------------------------------------------------------ -- Magmas diff --git a/src/Algebra/Morphism/Construct/Identity.agda b/src/Algebra/Morphism/Construct/Identity.agda index 5ea2571de0..f5eee85291 100644 --- a/src/Algebra/Morphism/Construct/Identity.agda +++ b/src/Algebra/Morphism/Construct/Identity.agda @@ -10,7 +10,8 @@ module Algebra.Morphism.Construct.Identity where open import Algebra.Bundles open import Algebra.Morphism.Structures - using ( module MagmaMorphisms + using ( module PointedMorphisms + ; module MagmaMorphisms ; module MonoidMorphisms ; module GroupMorphisms ; module NearSemiringMorphisms @@ -30,6 +31,30 @@ private variable c ℓ : Level +------------------------------------------------------------------------ +-- Pointeds + +module _ (P : RawPointed c ℓ) (open RawPointed P) (refl : Reflexive _≈_) where + open PointedMorphisms P P + + isPointedHomomorphism : IsPointedHomomorphism id + isPointedHomomorphism = record + { isRelHomomorphism = isRelHomomorphism _ + ; homo = refl + } + + isPointedMonomorphism : IsPointedMonomorphism id + isPointedMonomorphism = record + { isPointedHomomorphism = isPointedHomomorphism + ; injective = id + } + + isPointedIsomorphism : IsPointedIsomorphism id + isPointedIsomorphism = record + { isPointedMonomorphism = isPointedMonomorphism + ; surjective = _, refl + } + ------------------------------------------------------------------------ -- Magmas diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda index 525cbf5da0..0a13d43eca 100644 --- a/src/Algebra/Morphism/Structures.agda +++ b/src/Algebra/Morphism/Structures.agda @@ -21,6 +21,55 @@ private variable a b ℓ₁ ℓ₂ : Level +------------------------------------------------------------------------ +-- Morphisms over pointed structures +------------------------------------------------------------------------ + +module PointedMorphisms (P₁ : RawPointed a ℓ₁) (P₂ : RawPointed b ℓ₂) where + + open RawPointed P₁ renaming (Carrier to A; _≈_ to _≈₁_; pt₀ to pt₁) + open RawPointed P₂ renaming (Carrier to B; _≈_ to _≈₂_; pt₀ to pt₂) + open MorphismDefinitions A B _≈₂_ + open FunctionDefinitions _≈₁_ _≈₂_ + + + record IsPointedHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where + field + isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧ + homo : Homomorphic₀ ⟦_⟧ pt₁ pt₂ + + open IsRelHomomorphism isRelHomomorphism public + renaming (cong to ⟦⟧-cong) + + record IsPointedMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where + field + isPointedHomomorphism : IsPointedHomomorphism ⟦_⟧ + injective : Injective ⟦_⟧ + + open IsPointedHomomorphism isPointedHomomorphism public + + isRelMonomorphism : IsRelMonomorphism _≈₁_ _≈₂_ ⟦_⟧ + isRelMonomorphism = record + { isHomomorphism = isRelHomomorphism + ; injective = injective + } + + + record IsPointedIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where + field + isPointedMonomorphism : IsPointedMonomorphism ⟦_⟧ + surjective : Surjective ⟦_⟧ + + open IsPointedMonomorphism isPointedMonomorphism public + + isRelIsomorphism : IsRelIsomorphism _≈₁_ _≈₂_ ⟦_⟧ + isRelIsomorphism = record + { isMonomorphism = isRelMonomorphism + ; surjective = surjective + } + + + ------------------------------------------------------------------------ -- Morphisms over magma-like structures ------------------------------------------------------------------------ @@ -697,6 +746,7 @@ module LoopMorphisms (L₁ : RawLoop a ℓ₁) (L₂ : RawLoop b ℓ₂) where ------------------------------------------------------------------------ -- Re-export contents of modules publicly +open PointedMorphisms public open MagmaMorphisms public open MonoidMorphisms public open GroupMorphisms public diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 0a904276db..dff27f8a08 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -25,6 +25,19 @@ import Algebra.Consequences.Setoid as Consequences open import Data.Product using (_,_; proj₁; proj₂) open import Level using (_⊔_) +------------------------------------------------------------------------ +-- Structures with 1 element +------------------------------------------------------------------------ + +record IsPointed (e : A) : Set (a ⊔ ℓ) where + field + isEquivalence : IsEquivalence _≈_ + + open IsEquivalence isEquivalence public + + setoid : Setoid a ℓ + setoid = record { isEquivalence = isEquivalence } + ------------------------------------------------------------------------ -- Structures with 1 binary operation ------------------------------------------------------------------------