From bcef47e6dcb0f61af9b9614dfd5c1c0d18eaa732 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 24 Nov 2025 12:25:45 +0000 Subject: [PATCH 1/7] [ add ] left- and right- actions induced by a `Magma` homomorphism --- CHANGELOG.md | 6 ++++++ src/Algebra/Morphism/Structures.agda | 6 ++++++ 2 files changed, 12 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 38c13e12be..ff7916cf92 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -151,6 +151,12 @@ Additions to existing modules ⊕-∧-booleanRing : BooleanRing _ _ ``` +* In `Algebra.Morphism.Structures.IsMagmaHomomorphism`: + ```agda + ⟦_⟧∙_ : A → B → B + _∙⟦_⟧ : B → A → B + ``` + * In `Algebra.Properties.RingWithoutOne`: ```agda [-x][-y]≈xy : ∀ x y → - x * - y ≈ x * y diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda index af7e025fff..78b7230857 100644 --- a/src/Algebra/Morphism/Structures.agda +++ b/src/Algebra/Morphism/Structures.agda @@ -89,6 +89,12 @@ module MagmaMorphisms (M₁ : RawMagma a ℓ₁) (M₂ : RawMagma b ℓ₂) wher open IsRelHomomorphism isRelHomomorphism public renaming (cong to ⟦⟧-cong) + ⟦_⟧∙_ : A → B → B + ⟦ x ⟧∙ y = ⟦ x ⟧ ◦ y + + _∙⟦_⟧ : B → A → B + y ∙⟦ x ⟧ = y ◦ ⟦ x ⟧ + record IsMagmaMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field From 299caba41a05c2ca736a2b440c1d3fce04e5308e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 24 Nov 2025 13:38:31 +0000 Subject: [PATCH 2/7] fix: exports (temporary) --- src/Algebra/Morphism/Bundles.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Morphism/Bundles.agda b/src/Algebra/Morphism/Bundles.agda index 5c6a8063ae..62cfb3d3c2 100644 --- a/src/Algebra/Morphism/Bundles.agda +++ b/src/Algebra/Morphism/Bundles.agda @@ -163,7 +163,7 @@ record KleeneAlgebraHomomorphism semiringHomomorphism = record { isSemiringHomomorphism = isSemiringHomomorphism } open SemiringHomomorphism semiringHomomorphism public - hiding (*-isMagmaHomomorphism; *-isMonoidHomomorphism) + hiding (*-isMagmaHomomorphism; *-isMonoidHomomorphism; ⟦_⟧∙_; _∙⟦_⟧) ------------------------------------------------------------------------ -- Morphisms between RingWithoutOnes From 97c926fc699e54fb8d4ea623645e25252378f280 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 24 Nov 2025 23:01:34 +0000 Subject: [PATCH 3/7] rename: exports --- src/Algebra/Morphism/Structures.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda index 78b7230857..e38e2388bb 100644 --- a/src/Algebra/Morphism/Structures.agda +++ b/src/Algebra/Morphism/Structures.agda @@ -267,7 +267,7 @@ module NearSemiringMorphisms (R₁ : RawNearSemiring a ℓ₁) (R₂ : RawNearSe *-homo : Homomorphic₂ ⟦_⟧ _*₁_ _*₂_ open +.IsMonoidHomomorphism +-isMonoidHomomorphism public - renaming (homo to +-homo; ε-homo to 0#-homo; isMagmaHomomorphism to +-isMagmaHomomorphism) + renaming (homo to +-homo; ε-homo to 0#-homo; isMagmaHomomorphism to +-isMagmaHomomorphism; ⟦_⟧∙_ to ⟦_⟧+_; _∙⟦_⟧ to _+⟦_⟧) *-isMagmaHomomorphism : *.IsMagmaHomomorphism ⟦_⟧ *-isMagmaHomomorphism = record @@ -435,7 +435,7 @@ module RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRi *-homo : Homomorphic₂ ⟦_⟧ _*₁_ _*₂_ open +.IsGroupHomomorphism +-isGroupHomomorphism public - renaming (homo to +-homo; ε-homo to 0#-homo; isMagmaHomomorphism to +-isMagmaHomomorphism; isMonoidHomomorphism to +-isMonoidHomomorphism) + renaming (homo to +-homo; ε-homo to 0#-homo; isMagmaHomomorphism to +-isMagmaHomomorphism; isMonoidHomomorphism to +-isMonoidHomomorphism; ⟦_⟧∙_ to ⟦_⟧+_; _∙⟦_⟧ to _+⟦_⟧) isNearSemiringHomomorphism : +*.IsNearSemiringHomomorphism ⟦_⟧ isNearSemiringHomomorphism = record From c760a5d4a004ffc55569cfc17c65e3ac13571155 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 24 Nov 2025 23:07:52 +0000 Subject: [PATCH 4/7] rename: hide renamed exports --- src/Algebra/Morphism/Bundles.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Morphism/Bundles.agda b/src/Algebra/Morphism/Bundles.agda index 62cfb3d3c2..fca15f8024 100644 --- a/src/Algebra/Morphism/Bundles.agda +++ b/src/Algebra/Morphism/Bundles.agda @@ -163,7 +163,7 @@ record KleeneAlgebraHomomorphism semiringHomomorphism = record { isSemiringHomomorphism = isSemiringHomomorphism } open SemiringHomomorphism semiringHomomorphism public - hiding (*-isMagmaHomomorphism; *-isMonoidHomomorphism; ⟦_⟧∙_; _∙⟦_⟧) + hiding (*-isMagmaHomomorphism; *-isMonoidHomomorphism; ⟦_⟧+_; _+⟦_⟧) ------------------------------------------------------------------------ -- Morphisms between RingWithoutOnes From bb18eca471b704bab0f7772c8bfb590ebc1d5496 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 25 Nov 2025 03:19:51 +0000 Subject: [PATCH 5/7] rename: `Algebra.Module.Morphism.Structure` exports --- src/Algebra/Module/Morphism/Structures.agda | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Algebra/Module/Morphism/Structures.agda b/src/Algebra/Module/Morphism/Structures.agda index 3ef580ebea..70ef423664 100644 --- a/src/Algebra/Module/Morphism/Structures.agda +++ b/src/Algebra/Module/Morphism/Structures.agda @@ -35,7 +35,7 @@ module LeftSemimoduleMorphisms open IsMonoidHomomorphism +ᴹ-isMonoidHomomorphism public using (isRelHomomorphism; ⟦⟧-cong) - renaming (isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo) + renaming (isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⟦_⟧∙_ to ⟦_⟧+ᴹ_; _∙⟦_⟧ to _+ᴹ⟦_⟧) record IsLeftSemimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where field @@ -92,7 +92,7 @@ module LeftModuleMorphisms using (isRelHomomorphism; ⟦⟧-cong) renaming ( isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; isMonoidHomomorphism to +ᴹ-isMonoidHomomorphism ; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⁻¹-homo to -ᴹ-homo - ) + ; ⟦_⟧∙_ to ⟦_⟧+ᴹ_; _∙⟦_⟧ to _+ᴹ⟦_⟧) isLeftSemimoduleHomomorphism : IsLeftSemimoduleHomomorphism ⟦_⟧ isLeftSemimoduleHomomorphism = record @@ -162,7 +162,7 @@ module RightSemimoduleMorphisms open IsMonoidHomomorphism +ᴹ-isMonoidHomomorphism public using (isRelHomomorphism; ⟦⟧-cong) - renaming (isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo) + renaming (isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⟦_⟧∙_ to ⟦_⟧+ᴹ_; _∙⟦_⟧ to _+ᴹ⟦_⟧) record IsRightSemimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where field @@ -219,7 +219,7 @@ module RightModuleMorphisms using (isRelHomomorphism; ⟦⟧-cong) renaming ( isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; isMonoidHomomorphism to +ᴹ-isMonoidHomomorphism ; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⁻¹-homo to -ᴹ-homo - ) + ; ⟦_⟧∙_ to ⟦_⟧+ᴹ_; _∙⟦_⟧ to _+ᴹ⟦_⟧) isRightSemimoduleHomomorphism : IsRightSemimoduleHomomorphism ⟦_⟧ isRightSemimoduleHomomorphism = record { +ᴹ-isMonoidHomomorphism = +ᴹ-isMonoidHomomorphism @@ -376,7 +376,7 @@ module BimoduleMorphisms using (isRelHomomorphism; ⟦⟧-cong) renaming ( isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; isMonoidHomomorphism to +ᴹ-isMonoidHomomorphism ; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⁻¹-homo to -ᴹ-homo - ) + ; ⟦_⟧∙_ to ⟦_⟧+ᴹ_; _∙⟦_⟧ to _+ᴹ⟦_⟧) isBisemimoduleHomomorphism : IsBisemimoduleHomomorphism ⟦_⟧ isBisemimoduleHomomorphism = record From 3509702e8c79fa6e6e814647976c376a74f48f80 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 25 Nov 2025 03:29:17 +0000 Subject: [PATCH 6/7] rename: `Algebra.Lattice.Morphism.Structures` exports --- src/Algebra/Lattice/Morphism/Structures.agda | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Algebra/Lattice/Morphism/Structures.agda b/src/Algebra/Lattice/Morphism/Structures.agda index f56235c2b0..1f12d1ef9a 100644 --- a/src/Algebra/Lattice/Morphism/Structures.agda +++ b/src/Algebra/Lattice/Morphism/Structures.agda @@ -87,6 +87,7 @@ module LatticeMorphisms (L₁ : RawLattice a ℓ₁) (L₂ : RawLattice b ℓ₂ open ∧.IsMagmaMonomorphism ∧-isMagmaMonomorphism public using (isRelMonomorphism) + renaming (⟦_⟧∙_ to ⟦_⟧∧_; _∙⟦_⟧ to _∧⟦_⟧) record IsLatticeIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where From 453749bdbd856efef46686333bd2307b1ef6d8e4 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 25 Nov 2025 11:10:26 +0000 Subject: [PATCH 7/7] add: re-export multiplicative actions --- src/Algebra/Morphism/Bundles.agda | 3 ++- src/Algebra/Morphism/Structures.agda | 19 +++++++++++++++++-- 2 files changed, 19 insertions(+), 3 deletions(-) diff --git a/src/Algebra/Morphism/Bundles.agda b/src/Algebra/Morphism/Bundles.agda index fca15f8024..83ae947dc3 100644 --- a/src/Algebra/Morphism/Bundles.agda +++ b/src/Algebra/Morphism/Bundles.agda @@ -163,7 +163,8 @@ record KleeneAlgebraHomomorphism semiringHomomorphism = record { isSemiringHomomorphism = isSemiringHomomorphism } open SemiringHomomorphism semiringHomomorphism public - hiding (*-isMagmaHomomorphism; *-isMonoidHomomorphism; ⟦_⟧+_; _+⟦_⟧) + hiding (*-isMagmaHomomorphism; *-isMonoidHomomorphism + ; ⟦_⟧+_; _+⟦_⟧; ⟦_⟧*_; _*⟦_⟧) ------------------------------------------------------------------------ -- Morphisms between RingWithoutOnes diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda index e38e2388bb..e63aa1d9fe 100644 --- a/src/Algebra/Morphism/Structures.agda +++ b/src/Algebra/Morphism/Structures.agda @@ -267,7 +267,10 @@ module NearSemiringMorphisms (R₁ : RawNearSemiring a ℓ₁) (R₂ : RawNearSe *-homo : Homomorphic₂ ⟦_⟧ _*₁_ _*₂_ open +.IsMonoidHomomorphism +-isMonoidHomomorphism public - renaming (homo to +-homo; ε-homo to 0#-homo; isMagmaHomomorphism to +-isMagmaHomomorphism; ⟦_⟧∙_ to ⟦_⟧+_; _∙⟦_⟧ to _+⟦_⟧) + renaming (homo to +-homo; ε-homo to 0#-homo + ; isMagmaHomomorphism to +-isMagmaHomomorphism + ; ⟦_⟧∙_ to ⟦_⟧+_; _∙⟦_⟧ to _+⟦_⟧ + ) *-isMagmaHomomorphism : *.IsMagmaHomomorphism ⟦_⟧ *-isMagmaHomomorphism = record @@ -275,6 +278,10 @@ module NearSemiringMorphisms (R₁ : RawNearSemiring a ℓ₁) (R₂ : RawNearSe ; homo = *-homo } + open *.IsMagmaHomomorphism *-isMagmaHomomorphism public + using () + renaming (⟦_⟧∙_ to ⟦_⟧*_; _∙⟦_⟧ to _*⟦_⟧) + record IsNearSemiringMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧ @@ -435,7 +442,11 @@ module RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRi *-homo : Homomorphic₂ ⟦_⟧ _*₁_ _*₂_ open +.IsGroupHomomorphism +-isGroupHomomorphism public - renaming (homo to +-homo; ε-homo to 0#-homo; isMagmaHomomorphism to +-isMagmaHomomorphism; isMonoidHomomorphism to +-isMonoidHomomorphism; ⟦_⟧∙_ to ⟦_⟧+_; _∙⟦_⟧ to _+⟦_⟧) + renaming (homo to +-homo; ε-homo to 0#-homo + ; isMagmaHomomorphism to +-isMagmaHomomorphism + ; isMonoidHomomorphism to +-isMonoidHomomorphism + ; ⟦_⟧∙_ to ⟦_⟧+_; _∙⟦_⟧ to _+⟦_⟧ + ) isNearSemiringHomomorphism : +*.IsNearSemiringHomomorphism ⟦_⟧ isNearSemiringHomomorphism = record @@ -449,6 +460,10 @@ module RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRi ; homo = *-homo } + open *.IsMagmaHomomorphism *-isMagmaHomomorphism public + using () + renaming (⟦_⟧∙_ to ⟦_⟧*_; _∙⟦_⟧ to _*⟦_⟧) + record IsRingWithoutOneMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism ⟦_⟧