From 2eacb839005fd516675d13f563d05f96573fb807 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Fri, 9 May 2025 14:24:34 +0200 Subject: [PATCH 1/5] Adds Algebra.Morphism.Construct.DirectProduct --- CHANGELOG.md | 2 + .../Morphism/Construct/DirectProduct.agda | 66 +++++++++++++++++++ 2 files changed, 68 insertions(+) create mode 100644 src/Algebra/Morphism/Construct/DirectProduct.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 381bd0eb9c..4181d2f342 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -155,6 +155,8 @@ New modules * `Algebra.Module.Properties.{Bimodule|LeftModule|RightModule}`. +* `Algebra.Morphism.Construct.DirectProduct`. + * `Data.List.Base.{and|or|any|all}` have been lifted out into `Data.Bool.ListAction`. * `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`. diff --git a/src/Algebra/Morphism/Construct/DirectProduct.agda b/src/Algebra/Morphism/Construct/DirectProduct.agda new file mode 100644 index 0000000000..0e7fd19e8b --- /dev/null +++ b/src/Algebra/Morphism/Construct/DirectProduct.agda @@ -0,0 +1,66 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- The projection morphisms for alegraic structures arising from the +-- direct product construction +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +module Algebra.Morphism.Construct.DirectProduct where + +open import Algebra.Bundles +open import Algebra.Morphism.Structures + using ( module MagmaMorphisms + ; module MonoidMorphisms + ) +open import Data.Product +open import Level using (Level) +open import Relation.Binary.Definitions using (Reflexive) +open import Algebra.Construct.DirectProduct + +private + variable + c ℓ : Level + +------------------------------------------------------------------------ +-- Magmas + +module _ (M N : RawMagma c ℓ) (open RawMagma M) (refl : Reflexive _≈_) where + open MagmaMorphisms (rawMagma M N) M + + isMagmaHomomorphism-proj₁ : IsMagmaHomomorphism proj₁ + isMagmaHomomorphism-proj₁ = record + { isRelHomomorphism = record { cong = λ {x} {y} z → z .proj₁ } + ; homo = λ _ _ → refl + } + +module _ (M N : RawMagma c ℓ) (open RawMagma N) (refl : Reflexive _≈_) where + open MagmaMorphisms (rawMagma M N) N + + isMagmaHomomorphism-proj₂ : IsMagmaHomomorphism proj₂ + isMagmaHomomorphism-proj₂ = record + { isRelHomomorphism = record { cong = λ {x} {y} z → z .proj₂ } + ; homo = λ _ _ → refl + } + +------------------------------------------------------------------------ +-- Monoids + +module _ (M N : RawMonoid c ℓ) (open RawMonoid M) (refl : Reflexive _≈_) where + open MonoidMorphisms (rawMonoid M N) M + + isMonoidHomomorphism-proj₁ : IsMonoidHomomorphism proj₁ + isMonoidHomomorphism-proj₁ = record + { isMagmaHomomorphism = isMagmaHomomorphism-proj₁ _ _ refl + ; ε-homo = refl + } + +module _ (M N : RawMonoid c ℓ) (open RawMonoid N) (refl : Reflexive _≈_) where + open MonoidMorphisms (rawMonoid M N) N + + isMonoidHomomorphism-proj₂ : IsMonoidHomomorphism proj₂ + isMonoidHomomorphism-proj₂ = record + { isMagmaHomomorphism = isMagmaHomomorphism-proj₂ _ _ refl + ; ε-homo = refl + } From 68c8cf59a89218ef43d4994f75ea4fbe57867634 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Fri, 9 May 2025 14:34:18 +0200 Subject: [PATCH 2/5] Update src/Algebra/Morphism/Construct/DirectProduct.agda --- src/Algebra/Morphism/Construct/DirectProduct.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Morphism/Construct/DirectProduct.agda b/src/Algebra/Morphism/Construct/DirectProduct.agda index 0e7fd19e8b..cbf289032b 100644 --- a/src/Algebra/Morphism/Construct/DirectProduct.agda +++ b/src/Algebra/Morphism/Construct/DirectProduct.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- The projection morphisms for alegraic structures arising from the +-- The projection morphisms for algebraic structures arising from the -- direct product construction ------------------------------------------------------------------------ From 4a216603ff7ebd9357debe94efefa1ad131825eb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Thu, 5 Jun 2025 14:32:40 +0200 Subject: [PATCH 3/5] Address comments --- .../Morphism/Construct/DirectProduct.agda | 107 ++++++++++++------ 1 file changed, 75 insertions(+), 32 deletions(-) diff --git a/src/Algebra/Morphism/Construct/DirectProduct.agda b/src/Algebra/Morphism/Construct/DirectProduct.agda index cbf289032b..effcac0470 100644 --- a/src/Algebra/Morphism/Construct/DirectProduct.agda +++ b/src/Algebra/Morphism/Construct/DirectProduct.agda @@ -9,58 +9,101 @@ module Algebra.Morphism.Construct.DirectProduct where -open import Algebra.Bundles +open import Algebra.Bundles using (RawMagma; RawMonoid) +open import Algebra.Construct.DirectProduct using (rawMagma; rawMonoid) open import Algebra.Morphism.Structures using ( module MagmaMorphisms ; module MonoidMorphisms ) -open import Data.Product +open import Data.Product as Product + using (_,_) open import Level using (Level) open import Relation.Binary.Definitions using (Reflexive) -open import Algebra.Construct.DirectProduct +open import Relation.Binary.Morphism.Construct.Product + using (proj₁; proj₂; <_,_>) private variable - c ℓ : Level + a b c ℓ₁ ℓ₂ ℓ₃ : Level ------------------------------------------------------------------------ -- Magmas -module _ (M N : RawMagma c ℓ) (open RawMagma M) (refl : Reflexive _≈_) where - open MagmaMorphisms (rawMagma M N) M +module Magma (M : RawMagma a ℓ₁) (N : RawMagma b ℓ₂) where + open MagmaMorphisms - isMagmaHomomorphism-proj₁ : IsMagmaHomomorphism proj₁ - isMagmaHomomorphism-proj₁ = record - { isRelHomomorphism = record { cong = λ {x} {y} z → z .proj₁ } - ; homo = λ _ _ → refl - } + private + module M = RawMagma M + module N = RawMagma N -module _ (M N : RawMagma c ℓ) (open RawMagma N) (refl : Reflexive _≈_) where - open MagmaMorphisms (rawMagma M N) N + module Proj₁ (refl : Reflexive M._≈_) where - isMagmaHomomorphism-proj₂ : IsMagmaHomomorphism proj₂ - isMagmaHomomorphism-proj₂ = record - { isRelHomomorphism = record { cong = λ {x} {y} z → z .proj₂ } - ; homo = λ _ _ → refl - } + isMagmaHomomorphism : IsMagmaHomomorphism (rawMagma M N) M Product.proj₁ + isMagmaHomomorphism = record + { isRelHomomorphism = proj₁ + ; homo = λ _ _ → refl + } + + module Proj₂ (refl : Reflexive N._≈_) where + + isMagmaHomomorphism : IsMagmaHomomorphism (rawMagma M N) N Product.proj₂ + isMagmaHomomorphism = record + { isRelHomomorphism = proj₂ + ; homo = λ _ _ → refl + } + + module Pair (P : RawMagma c ℓ₃) where + + isMagmaHomomorphism : ∀ {f h} → + IsMagmaHomomorphism P M f → + IsMagmaHomomorphism P N h → + IsMagmaHomomorphism P (rawMagma M N) (Product.< f , h >) + isMagmaHomomorphism F H = record + { isRelHomomorphism = < F.isRelHomomorphism , H.isRelHomomorphism > + ; homo = λ x y → F.homo x y , H.homo x y + } + where + module F = IsMagmaHomomorphism F + module H = IsMagmaHomomorphism H ------------------------------------------------------------------------ -- Monoids -module _ (M N : RawMonoid c ℓ) (open RawMonoid M) (refl : Reflexive _≈_) where - open MonoidMorphisms (rawMonoid M N) M +module Monoid (M : RawMonoid a ℓ₁) (N : RawMonoid b ℓ₂) where + open MonoidMorphisms + + private + module M = RawMonoid M + module N = RawMonoid N + + module Proj₁ (refl : Reflexive M._≈_) where + + isMonoidHomomorphism : IsMonoidHomomorphism (rawMonoid M N) M Product.proj₁ + isMonoidHomomorphism = record + { isMagmaHomomorphism = Magma.Proj₁.isMagmaHomomorphism M.rawMagma N.rawMagma refl + ; ε-homo = refl + } + + module Proj₂ (refl : Reflexive N._≈_) where + + isMonoidHomomorphism : IsMonoidHomomorphism (rawMonoid M N) N Product.proj₂ + isMonoidHomomorphism = record + { isMagmaHomomorphism = Magma.Proj₂.isMagmaHomomorphism M.rawMagma N.rawMagma refl + ; ε-homo = refl + } - isMonoidHomomorphism-proj₁ : IsMonoidHomomorphism proj₁ - isMonoidHomomorphism-proj₁ = record - { isMagmaHomomorphism = isMagmaHomomorphism-proj₁ _ _ refl - ; ε-homo = refl - } + module Pair (P : RawMonoid c ℓ₃) where -module _ (M N : RawMonoid c ℓ) (open RawMonoid N) (refl : Reflexive _≈_) where - open MonoidMorphisms (rawMonoid M N) N + private + module P = RawMonoid P - isMonoidHomomorphism-proj₂ : IsMonoidHomomorphism proj₂ - isMonoidHomomorphism-proj₂ = record - { isMagmaHomomorphism = isMagmaHomomorphism-proj₂ _ _ refl - ; ε-homo = refl - } + isMonoidHomomorphism : ∀ {f h} → + IsMonoidHomomorphism P M f → + IsMonoidHomomorphism P N h → + IsMonoidHomomorphism P (rawMonoid M N) (Product.< f , h >) + isMonoidHomomorphism F H = record + { isMagmaHomomorphism = Magma.Pair.isMagmaHomomorphism M.rawMagma N.rawMagma P.rawMagma F.isMagmaHomomorphism H.isMagmaHomomorphism + ; ε-homo = F.ε-homo , H.ε-homo } + where + module F = IsMonoidHomomorphism F + module H = IsMonoidHomomorphism H From 7dfbf545655c26a89fac043bc488c84355002d3c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Mon, 9 Jun 2025 14:39:42 +0200 Subject: [PATCH 4/5] Add module to reexport with implicit arguments --- .../Morphism/Construct/DirectProduct.agda | 51 +++++++++++++++++-- 1 file changed, 46 insertions(+), 5 deletions(-) diff --git a/src/Algebra/Morphism/Construct/DirectProduct.agda b/src/Algebra/Morphism/Construct/DirectProduct.agda index effcac0470..c8d6095351 100644 --- a/src/Algebra/Morphism/Construct/DirectProduct.agda +++ b/src/Algebra/Morphism/Construct/DirectProduct.agda @@ -19,8 +19,7 @@ open import Data.Product as Product using (_,_) open import Level using (Level) open import Relation.Binary.Definitions using (Reflexive) -open import Relation.Binary.Morphism.Construct.Product - using (proj₁; proj₂; <_,_>) +import Relation.Binary.Morphism.Construct.Product as RP private variable @@ -40,7 +39,7 @@ module Magma (M : RawMagma a ℓ₁) (N : RawMagma b ℓ₂) where isMagmaHomomorphism : IsMagmaHomomorphism (rawMagma M N) M Product.proj₁ isMagmaHomomorphism = record - { isRelHomomorphism = proj₁ + { isRelHomomorphism = RP.proj₁ ; homo = λ _ _ → refl } @@ -48,7 +47,7 @@ module Magma (M : RawMagma a ℓ₁) (N : RawMagma b ℓ₂) where isMagmaHomomorphism : IsMagmaHomomorphism (rawMagma M N) N Product.proj₂ isMagmaHomomorphism = record - { isRelHomomorphism = proj₂ + { isRelHomomorphism = RP.proj₂ ; homo = λ _ _ → refl } @@ -59,13 +58,34 @@ module Magma (M : RawMagma a ℓ₁) (N : RawMagma b ℓ₂) where IsMagmaHomomorphism P N h → IsMagmaHomomorphism P (rawMagma M N) (Product.< f , h >) isMagmaHomomorphism F H = record - { isRelHomomorphism = < F.isRelHomomorphism , H.isRelHomomorphism > + { isRelHomomorphism = RP.< F.isRelHomomorphism , H.isRelHomomorphism > ; homo = λ x y → F.homo x y , H.homo x y } where module F = IsMagmaHomomorphism F module H = IsMagmaHomomorphism H +-- Package for export +module Magma-Export {M : RawMagma a ℓ₁} {N : RawMagma b ℓ₂} where + open Magma + + private + module M = RawMagma M + module N = RawMagma N + + module _ {refl : Reflexive M._≈_} where + proj₁ = Proj₁.isMagmaHomomorphism M M refl + + module _ {refl : Reflexive N._≈_} where + proj₂ = Proj₂.isMagmaHomomorphism M N refl + + module _ {P : RawMagma c ℓ₃} where + + private + module P = RawMagma P + + <_,_> = Pair.isMagmaHomomorphism M N P + ------------------------------------------------------------------------ -- Monoids @@ -107,3 +127,24 @@ module Monoid (M : RawMonoid a ℓ₁) (N : RawMonoid b ℓ₂) where where module F = IsMonoidHomomorphism F module H = IsMonoidHomomorphism H + +-- Package for export +module Monoid-Export {M : RawMonoid a ℓ₁} {N : RawMonoid b ℓ₂} where + open Monoid + + private + module M = RawMonoid M + module N = RawMonoid N + + module _ {refl : Reflexive M._≈_} where + proj₁ = Proj₁.isMonoidHomomorphism M M refl + + module _ {refl : Reflexive N._≈_} where + proj₂ = Proj₂.isMonoidHomomorphism M N refl + + module _ {P : RawMonoid c ℓ₃} where + + private + module P = RawMonoid P + + <_,_> = Pair.isMonoidHomomorphism M N P From 8ea743ce1571378dcfb1cb842f292e6c320b3908 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Tue, 10 Jun 2025 16:08:21 +0200 Subject: [PATCH 5/5] Removed unused private module --- src/Algebra/Morphism/Construct/DirectProduct.agda | 8 -------- 1 file changed, 8 deletions(-) diff --git a/src/Algebra/Morphism/Construct/DirectProduct.agda b/src/Algebra/Morphism/Construct/DirectProduct.agda index c8d6095351..6b6fdee047 100644 --- a/src/Algebra/Morphism/Construct/DirectProduct.agda +++ b/src/Algebra/Morphism/Construct/DirectProduct.agda @@ -80,10 +80,6 @@ module Magma-Export {M : RawMagma a ℓ₁} {N : RawMagma b ℓ₂} where proj₂ = Proj₂.isMagmaHomomorphism M N refl module _ {P : RawMagma c ℓ₃} where - - private - module P = RawMagma P - <_,_> = Pair.isMagmaHomomorphism M N P ------------------------------------------------------------------------ @@ -143,8 +139,4 @@ module Monoid-Export {M : RawMonoid a ℓ₁} {N : RawMonoid b ℓ₂} where proj₂ = Proj₂.isMonoidHomomorphism M N refl module _ {P : RawMonoid c ℓ₃} where - - private - module P = RawMonoid P - <_,_> = Pair.isMonoidHomomorphism M N P