Skip to content

Module morphisms polymorphic in the underlying ring structure #2810

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
Taneb wants to merge 3 commits into from
Closed

Module morphisms polymorphic in the underlying ring structure #2810

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
9990e42
Subtraction binary operator in modules
Taneb Aug 15, 2025
201fc4a
Module morphisms polymorphic in the underlying ring
Taneb Aug 15, 2025
b376a6e
Follow on changes that oughtn't be necessary
Taneb Aug 15, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions src/Algebra/Module/Construct/DirectProduct.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -184,7 +184,7 @@ leftModule : {R : Ring r ℓr} →
LeftModule R m′ ℓm′ →
LeftModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
leftModule M N = record
{ -ᴹ_ = map M.-ᴹ_ N.-ᴹ_
{ -ᴹ_ = map (M.-ᴹ_) (N.-ᴹ_)
Copy link
Copy Markdown
Collaborator

@jamesmckinna jamesmckinna Feb 9, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do the parentheses help here? I'm not convinced...

Copy link
Copy Markdown
Member Author

@Taneb Taneb Feb 9, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's been a while, but I think without them Agda doesn't know if I mean that or a use of the _-ᴹ_ operator

Copy link
Copy Markdown
Collaborator

@jamesmckinna jamesmckinna Feb 9, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah... I see, but still worth thinking about the earlier comment about having a small PR adding that subtraction operator in its own right?

; isLeftModule = record
{ isLeftSemimodule = LeftSemimodule.isLeftSemimodule
(leftSemimodule M.leftSemimodule N.leftSemimodule)
Expand All @@ -200,7 +200,7 @@ rightModule : {R : Ring r ℓr} →
RightModule R m′ ℓm′ →
RightModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
rightModule M N = record
{ -ᴹ_ = map M.-ᴹ_ N.-ᴹ_
{ -ᴹ_ = map (M.-ᴹ_) (N.-ᴹ_)
; isRightModule = record
{ isRightSemimodule = RightSemimodule.isRightSemimodule
(rightSemimodule M.rightSemimodule N.rightSemimodule)
Expand All @@ -216,7 +216,7 @@ bimodule : {R : Ring r ℓr} {S : Ring s ℓs} →
Bimodule R S m′ ℓm′ →
Bimodule R S (m ⊔ m′) (ℓm ⊔ ℓm′)
bimodule M N = record
{ -ᴹ_ = map M.-ᴹ_ N.-ᴹ_
{ -ᴹ_ = map (M.-ᴹ_) (N.-ᴹ_)
; isBimodule = record
{ isBisemimodule = Bisemimodule.isBisemimodule
(bisemimodule M.bisemimodule N.bisemimodule)
Expand Down
2 changes: 1 addition & 1 deletion src/Algebra/Module/Morphism/BimoduleMonomorphism.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ module Algebra.Module.Morphism.BimoduleMonomorphism
(isBimoduleMonomorphism : IsBimoduleMonomorphism M N ⟦_⟧)
where

open IsBimoduleMonomorphism isBimoduleMonomorphism
open IsBimoduleMonomorphism M N isBimoduleMonomorphism
private
module M = RawBimodule M
module N = RawBimodule N
Expand Down
2 changes: 1 addition & 1 deletion src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ module Algebra.Module.Morphism.BisemimoduleMonomorphism
(isBisemimoduleMonomorphism : IsBisemimoduleMonomorphism M N ⟦_⟧)
where

open IsBisemimoduleMonomorphism isBisemimoduleMonomorphism
open IsBisemimoduleMonomorphism M N isBisemimoduleMonomorphism
private
module M = RawBisemimodule M
module N = RawBisemimodule N
Expand Down
48 changes: 24 additions & 24 deletions src/Algebra/Module/Morphism/Construct/Composition.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,23 +39,23 @@ module _
isLeftSemimoduleHomomorphism f-homo g-homo = record
{ +ᴹ-isMonoidHomomorphism = isMonoidHomomorphism ≈ᴹ₃-trans F.+ᴹ-isMonoidHomomorphism G.+ᴹ-isMonoidHomomorphism
; *ₗ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x))
} where module F = IsLeftSemimoduleHomomorphism f-homo; module G = IsLeftSemimoduleHomomorphism g-homo
} where module F = IsLeftSemimoduleHomomorphism M₁ M₂ f-homo; module G = IsLeftSemimoduleHomomorphism M₂ M₃ g-homo
Copy link
Copy Markdown
Collaborator

@jamesmckinna jamesmckinna Feb 9, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So I agree with you that it's annoying to have to be explicit with these arguments... I suppose that's one way of nudging the typechecker to know which scalars are involved at a given call-/use- site in this new setup, but perhaps simply supplying the R/S arguments would be the other way to do it?


isLeftSemimoduleMonomorphism : IsLeftSemimoduleMonomorphism M₁ M₂ f →
IsLeftSemimoduleMonomorphism M₂ M₃ g →
IsLeftSemimoduleMonomorphism M₁ M₃ (g ∘ f)
isLeftSemimoduleMonomorphism f-mono g-mono = record
{ isLeftSemimoduleHomomorphism = isLeftSemimoduleHomomorphism F.isLeftSemimoduleHomomorphism G.isLeftSemimoduleHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsLeftSemimoduleMonomorphism f-mono; module G = IsLeftSemimoduleMonomorphism g-mono
} where module F = IsLeftSemimoduleMonomorphism M₁ M₂ f-mono; module G = IsLeftSemimoduleMonomorphism M₂ M₃ g-mono

isLeftSemimoduleIsomorphism : IsLeftSemimoduleIsomorphism M₁ M₂ f →
IsLeftSemimoduleIsomorphism M₂ M₃ g →
IsLeftSemimoduleIsomorphism M₁ M₃ (g ∘ f)
isLeftSemimoduleIsomorphism f-iso g-iso = record
{ isLeftSemimoduleMonomorphism = isLeftSemimoduleMonomorphism F.isLeftSemimoduleMonomorphism G.isLeftSemimoduleMonomorphism
; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective
} where module F = IsLeftSemimoduleIsomorphism f-iso; module G = IsLeftSemimoduleIsomorphism g-iso
} where module F = IsLeftSemimoduleIsomorphism M₁ M₂ f-iso; module G = IsLeftSemimoduleIsomorphism M₂ M₃ g-iso

module _
{R : Set r}
Expand All @@ -74,23 +74,23 @@ module _
isLeftModuleHomomorphism f-homo g-homo = record
{ +ᴹ-isGroupHomomorphism = isGroupHomomorphism ≈ᴹ₃-trans F.+ᴹ-isGroupHomomorphism G.+ᴹ-isGroupHomomorphism
; *ₗ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x))
} where module F = IsLeftModuleHomomorphism f-homo; module G = IsLeftModuleHomomorphism g-homo
} where module F = IsLeftModuleHomomorphism M₁ M₂ f-homo; module G = IsLeftModuleHomomorphism M₂ M₃ g-homo

isLeftModuleMonomorphism : IsLeftModuleMonomorphism M₁ M₂ f →
IsLeftModuleMonomorphism M₂ M₃ g →
IsLeftModuleMonomorphism M₁ M₃ (g ∘ f)
isLeftModuleMonomorphism f-mono g-mono = record
{ isLeftModuleHomomorphism = isLeftModuleHomomorphism F.isLeftModuleHomomorphism G.isLeftModuleHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsLeftModuleMonomorphism f-mono; module G = IsLeftModuleMonomorphism g-mono
} where module F = IsLeftModuleMonomorphism M₁ M₂ f-mono; module G = IsLeftModuleMonomorphism M₂ M₃ g-mono

isLeftModuleIsomorphism : IsLeftModuleIsomorphism M₁ M₂ f →
IsLeftModuleIsomorphism M₂ M₃ g →
IsLeftModuleIsomorphism M₁ M₃ (g ∘ f)
isLeftModuleIsomorphism f-iso g-iso = record
{ isLeftModuleMonomorphism = isLeftModuleMonomorphism F.isLeftModuleMonomorphism G.isLeftModuleMonomorphism
; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective
} where module F = IsLeftModuleIsomorphism f-iso; module G = IsLeftModuleIsomorphism g-iso
} where module F = IsLeftModuleIsomorphism M₁ M₂ f-iso; module G = IsLeftModuleIsomorphism M₂ M₃ g-iso

module _
{R : Set r}
Expand All @@ -109,23 +109,23 @@ module _
isRightSemimoduleHomomorphism f-homo g-homo = record
{ +ᴹ-isMonoidHomomorphism = isMonoidHomomorphism ≈ᴹ₃-trans F.+ᴹ-isMonoidHomomorphism G.+ᴹ-isMonoidHomomorphism
; *ᵣ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x))
} where module F = IsRightSemimoduleHomomorphism f-homo; module G = IsRightSemimoduleHomomorphism g-homo
} where module F = IsRightSemimoduleHomomorphism M₁ M₂ f-homo; module G = IsRightSemimoduleHomomorphism M₂ M₃ g-homo

isRightSemimoduleMonomorphism : IsRightSemimoduleMonomorphism M₁ M₂ f →
IsRightSemimoduleMonomorphism M₂ M₃ g →
IsRightSemimoduleMonomorphism M₁ M₃ (g ∘ f)
isRightSemimoduleMonomorphism f-mono g-mono = record
{ isRightSemimoduleHomomorphism = isRightSemimoduleHomomorphism F.isRightSemimoduleHomomorphism G.isRightSemimoduleHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsRightSemimoduleMonomorphism f-mono; module G = IsRightSemimoduleMonomorphism g-mono
} where module F = IsRightSemimoduleMonomorphism M₁ M₂ f-mono; module G = IsRightSemimoduleMonomorphism M₂ M₃ g-mono

isRightSemimoduleIsomorphism : IsRightSemimoduleIsomorphism M₁ M₂ f →
IsRightSemimoduleIsomorphism M₂ M₃ g →
IsRightSemimoduleIsomorphism M₁ M₃ (g ∘ f)
isRightSemimoduleIsomorphism f-iso g-iso = record
{ isRightSemimoduleMonomorphism = isRightSemimoduleMonomorphism F.isRightSemimoduleMonomorphism G.isRightSemimoduleMonomorphism
; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective
} where module F = IsRightSemimoduleIsomorphism f-iso; module G = IsRightSemimoduleIsomorphism g-iso
} where module F = IsRightSemimoduleIsomorphism M₁ M₂ f-iso; module G = IsRightSemimoduleIsomorphism M₂ M₃ g-iso

module _
{R : Set r}
Expand All @@ -144,23 +144,23 @@ module _
isRightModuleHomomorphism f-homo g-homo = record
{ +ᴹ-isGroupHomomorphism = isGroupHomomorphism ≈ᴹ₃-trans F.+ᴹ-isGroupHomomorphism G.+ᴹ-isGroupHomomorphism
; *ᵣ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x))
} where module F = IsRightModuleHomomorphism f-homo; module G = IsRightModuleHomomorphism g-homo
} where module F = IsRightModuleHomomorphism M₁ M₂ f-homo; module G = IsRightModuleHomomorphism M₂ M₃ g-homo

isRightModuleMonomorphism : IsRightModuleMonomorphism M₁ M₂ f →
IsRightModuleMonomorphism M₂ M₃ g →
IsRightModuleMonomorphism M₁ M₃ (g ∘ f)
isRightModuleMonomorphism f-mono g-mono = record
{ isRightModuleHomomorphism = isRightModuleHomomorphism F.isRightModuleHomomorphism G.isRightModuleHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsRightModuleMonomorphism f-mono; module G = IsRightModuleMonomorphism g-mono
} where module F = IsRightModuleMonomorphism M₁ M₂ f-mono; module G = IsRightModuleMonomorphism M₂ M₃ g-mono

isRightModuleIsomorphism : IsRightModuleIsomorphism M₁ M₂ f →
IsRightModuleIsomorphism M₂ M₃ g →
IsRightModuleIsomorphism M₁ M₃ (g ∘ f)
isRightModuleIsomorphism f-iso g-iso = record
{ isRightModuleMonomorphism = isRightModuleMonomorphism F.isRightModuleMonomorphism G.isRightModuleMonomorphism
; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective
} where module F = IsRightModuleIsomorphism f-iso; module G = IsRightModuleIsomorphism g-iso
} where module F = IsRightModuleIsomorphism M₁ M₂ f-iso; module G = IsRightModuleIsomorphism M₂ M₃ g-iso

module _
{R : Set r}
Expand All @@ -181,23 +181,23 @@ module _
{ +ᴹ-isMonoidHomomorphism = isMonoidHomomorphism ≈ᴹ₃-trans F.+ᴹ-isMonoidHomomorphism G.+ᴹ-isMonoidHomomorphism
; *ₗ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x))
; *ᵣ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x))
} where module F = IsBisemimoduleHomomorphism f-homo; module G = IsBisemimoduleHomomorphism g-homo
} where module F = IsBisemimoduleHomomorphism M₁ M₂ f-homo; module G = IsBisemimoduleHomomorphism M₂ M₃ g-homo

isBisemimoduleMonomorphism : IsBisemimoduleMonomorphism M₁ M₂ f →
IsBisemimoduleMonomorphism M₂ M₃ g →
IsBisemimoduleMonomorphism M₁ M₃ (g ∘ f)
isBisemimoduleMonomorphism f-mono g-mono = record
{ isBisemimoduleHomomorphism = isBisemimoduleHomomorphism F.isBisemimoduleHomomorphism G.isBisemimoduleHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsBisemimoduleMonomorphism f-mono; module G = IsBisemimoduleMonomorphism g-mono
} where module F = IsBisemimoduleMonomorphism M₁ M₂ f-mono; module G = IsBisemimoduleMonomorphism M₂ M₃ g-mono

isBisemimoduleIsomorphism : IsBisemimoduleIsomorphism M₁ M₂ f →
IsBisemimoduleIsomorphism M₂ M₃ g →
IsBisemimoduleIsomorphism M₁ M₃ (g ∘ f)
isBisemimoduleIsomorphism f-iso g-iso = record
{ isBisemimoduleMonomorphism = isBisemimoduleMonomorphism F.isBisemimoduleMonomorphism G.isBisemimoduleMonomorphism
; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective
} where module F = IsBisemimoduleIsomorphism f-iso; module G = IsBisemimoduleIsomorphism g-iso
} where module F = IsBisemimoduleIsomorphism M₁ M₂ f-iso; module G = IsBisemimoduleIsomorphism M₂ M₃ g-iso

module _
{R : Set r}
Expand All @@ -218,23 +218,23 @@ module _
{ +ᴹ-isGroupHomomorphism = isGroupHomomorphism ≈ᴹ₃-trans F.+ᴹ-isGroupHomomorphism G.+ᴹ-isGroupHomomorphism
; *ₗ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x))
; *ᵣ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x))
} where module F = IsBimoduleHomomorphism f-homo; module G = IsBimoduleHomomorphism g-homo
} where module F = IsBimoduleHomomorphism M₁ M₂ f-homo; module G = IsBimoduleHomomorphism M₂ M₃ g-homo

isBimoduleMonomorphism : IsBimoduleMonomorphism M₁ M₂ f →
IsBimoduleMonomorphism M₂ M₃ g →
IsBimoduleMonomorphism M₁ M₃ (g ∘ f)
isBimoduleMonomorphism f-mono g-mono = record
{ isBimoduleHomomorphism = isBimoduleHomomorphism F.isBimoduleHomomorphism G.isBimoduleHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsBimoduleMonomorphism f-mono; module G = IsBimoduleMonomorphism g-mono
} where module F = IsBimoduleMonomorphism M₁ M₂ f-mono; module G = IsBimoduleMonomorphism M₂ M₃ g-mono

isBimoduleIsomorphism : IsBimoduleIsomorphism M₁ M₂ f →
IsBimoduleIsomorphism M₂ M₃ g →
IsBimoduleIsomorphism M₁ M₃ (g ∘ f)
isBimoduleIsomorphism f-iso g-iso = record
{ isBimoduleMonomorphism = isBimoduleMonomorphism F.isBimoduleMonomorphism G.isBimoduleMonomorphism
; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective
} where module F = IsBimoduleIsomorphism f-iso; module G = IsBimoduleIsomorphism g-iso
} where module F = IsBimoduleIsomorphism M₁ M₂ f-iso; module G = IsBimoduleIsomorphism M₂ M₃ g-iso

module _
{R : Set r}
Expand All @@ -252,23 +252,23 @@ module _
IsSemimoduleHomomorphism M₁ M₃ (g ∘ f)
isSemimoduleHomomorphism f-homo g-homo = record
{ isBisemimoduleHomomorphism = isBisemimoduleHomomorphism ≈ᴹ₃-trans F.isBisemimoduleHomomorphism G.isBisemimoduleHomomorphism
} where module F = IsSemimoduleHomomorphism f-homo; module G = IsSemimoduleHomomorphism g-homo
} where module F = IsSemimoduleHomomorphism M₁ M₂ f-homo; module G = IsSemimoduleHomomorphism M₂ M₃ g-homo

isSemimoduleMonomorphism : IsSemimoduleMonomorphism M₁ M₂ f →
IsSemimoduleMonomorphism M₂ M₃ g →
IsSemimoduleMonomorphism M₁ M₃ (g ∘ f)
isSemimoduleMonomorphism f-mono g-mono = record
{ isSemimoduleHomomorphism = isSemimoduleHomomorphism F.isSemimoduleHomomorphism G.isSemimoduleHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsSemimoduleMonomorphism f-mono; module G = IsSemimoduleMonomorphism g-mono
} where module F = IsSemimoduleMonomorphism M₁ M₂ f-mono; module G = IsSemimoduleMonomorphism M₂ M₃ g-mono

isSemimoduleIsomorphism : IsSemimoduleIsomorphism M₁ M₂ f →
IsSemimoduleIsomorphism M₂ M₃ g →
IsSemimoduleIsomorphism M₁ M₃ (g ∘ f)
isSemimoduleIsomorphism f-iso g-iso = record
{ isSemimoduleMonomorphism = isSemimoduleMonomorphism F.isSemimoduleMonomorphism G.isSemimoduleMonomorphism
; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective
} where module F = IsSemimoduleIsomorphism f-iso; module G = IsSemimoduleIsomorphism g-iso
} where module F = IsSemimoduleIsomorphism M₁ M₂ f-iso; module G = IsSemimoduleIsomorphism M₂ M₃ g-iso

module _
{R : Set r}
Expand All @@ -286,20 +286,20 @@ module _
IsModuleHomomorphism M₁ M₃ (g ∘ f)
isModuleHomomorphism f-homo g-homo = record
{ isBimoduleHomomorphism = isBimoduleHomomorphism ≈ᴹ₃-trans F.isBimoduleHomomorphism G.isBimoduleHomomorphism
} where module F = IsModuleHomomorphism f-homo; module G = IsModuleHomomorphism g-homo
} where module F = IsModuleHomomorphism M₁ M₂ f-homo; module G = IsModuleHomomorphism M₂ M₃ g-homo

isModuleMonomorphism : IsModuleMonomorphism M₁ M₂ f →
IsModuleMonomorphism M₂ M₃ g →
IsModuleMonomorphism M₁ M₃ (g ∘ f)
isModuleMonomorphism f-mono g-mono = record
{ isModuleHomomorphism = isModuleHomomorphism F.isModuleHomomorphism G.isModuleHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsModuleMonomorphism f-mono; module G = IsModuleMonomorphism g-mono
} where module F = IsModuleMonomorphism M₁ M₂ f-mono; module G = IsModuleMonomorphism M₂ M₃ g-mono

isModuleIsomorphism : IsModuleIsomorphism M₁ M₂ f →
IsModuleIsomorphism M₂ M₃ g →
IsModuleIsomorphism M₁ M₃ (g ∘ f)
isModuleIsomorphism f-iso g-iso = record
{ isModuleMonomorphism = isModuleMonomorphism F.isModuleMonomorphism G.isModuleMonomorphism
; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective
} where module F = IsModuleIsomorphism f-iso; module G = IsModuleIsomorphism g-iso
} where module F = IsModuleIsomorphism M₁ M₂ f-iso; module G = IsModuleIsomorphism M₂ M₃ g-iso
12 changes: 7 additions & 5 deletions src/Algebra/Module/Morphism/Definitions.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,9 @@
open import Relation.Binary.Core using (Rel)

module Algebra.Module.Morphism.Definitions
{r} (R : Set r) -- The underlying ring
{r} (R : Set r) -- The underlying ring of the domain
{s} (S : Set s) -- The underlying ring of the codomain
([_] : R → S) -- The homomorphism between the underlying rings
Copy link
Copy Markdown
Collaborator

@jamesmckinna jamesmckinna Feb 9, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As I've indicated before, i think this design is trying to do too many things at once which could be usefully factored into smaller pieces, such as #2913 ?

Copy link
Copy Markdown
Member Author

@Taneb Taneb Feb 9, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, I've come to agree with you on this.

Copy link
Copy Markdown
Collaborator

@jamesmckinna jamesmckinna Feb 9, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK, let's see what comes out in the wash!

{a} (A : Set a) -- The domain of the morphism
{b} (B : Set b) -- The codomain of the morphism
{ℓ} (_≈_ : Rel B ℓ) -- The equality relation over the codomain
Expand All @@ -18,8 +20,8 @@ module Algebra.Module.Morphism.Definitions
open import Algebra.Module.Core using (Opₗ; Opᵣ)
open import Algebra.Morphism.Definitions A B _≈_ public

Homomorphicₗ : (A → B) → Opₗ R A → Opₗ R B → Set _
Homomorphicₗ ⟦_⟧ _∙_ _∘_ = ∀ r x → ⟦ r ∙ x ⟧ ≈ (r ∘ ⟦ x ⟧)
Homomorphicₗ : (A → B) → Opₗ R A → Opₗ S B → Set _
Homomorphicₗ ⟦_⟧ _∙_ _∘_ = ∀ r x → ⟦ r ∙ x ⟧ ≈ ([ r ] ∘ ⟦ x ⟧)

Homomorphicᵣ : (A → B) → Opᵣ R A → Opᵣ R B → Set _
Homomorphicᵣ ⟦_⟧ _∙_ _∘_ = ∀ r x → ⟦ x ∙ r ⟧ ≈ (⟦ x ⟧ ∘ r)
Homomorphicᵣ : (A → B) → Opᵣ R A → Opᵣ S B → Set _
Homomorphicᵣ ⟦_⟧ _∙_ _∘_ = ∀ r x → ⟦ x ∙ r ⟧ ≈ (⟦ x ⟧ ∘ [ r ])
2 changes: 1 addition & 1 deletion src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ module Algebra.Module.Morphism.LeftModuleMonomorphism
(isLeftModuleMonomorphism : IsLeftModuleMonomorphism M N ⟦_⟧)
where

open IsLeftModuleMonomorphism isLeftModuleMonomorphism
open IsLeftModuleMonomorphism M N isLeftModuleMonomorphism
private
module M = RawLeftModule M
module N = RawLeftModule N
Expand Down
2 changes: 1 addition & 1 deletion src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ module Algebra.Module.Morphism.LeftSemimoduleMonomorphism
(isLeftSemimoduleMonomorphism : IsLeftSemimoduleMonomorphism M₁ M₂ ⟦_⟧)
where

open IsLeftSemimoduleMonomorphism isLeftSemimoduleMonomorphism
open IsLeftSemimoduleMonomorphism M₁ M₂ isLeftSemimoduleMonomorphism
private
module M = RawLeftSemimodule M₁
module N = RawLeftSemimodule M₂
Expand Down
2 changes: 1 addition & 1 deletion src/Algebra/Module/Morphism/ModuleMonomorphism.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ module Algebra.Module.Morphism.ModuleMonomorphism
(isModuleMonomorphism : IsModuleMonomorphism M N ⟦_⟧)
where

open IsModuleMonomorphism isModuleMonomorphism
open IsModuleMonomorphism M N isModuleMonomorphism
private
module M = RawModule M
module N = RawModule N
Expand Down
Loading