Agda-stdlib: Add module homomorphisms

[conal]

Are there supporting definitions for module homomorphisms (likewise for left semimodule, etc)? I been searching and haven’t found them yet.

[conal]

I’m not finding semiring homomorphisms either. Maybe work in progress?

[gallais]

Ping @wenkokke @laMudri

[laMudri]

As far as I know, there's no work in progress in the literal sense. I think with algebraic stuff, making just the definitions you need is quite easy, but developing a coherent hierarchy can be unexpectedly difficult (and also tedious).

I think, if I were to make a stdlib-worthy definition of module homomorphisms, I'd start with the double category of bimodules. That is, we define how to fill a square:

  R ──────→ S
  │         │
f │    F    │ g
  ↓         ↓
  R′──────→ S′
       N

where R, R′, S, and S′ are (semi)rings, f and g are ring homomorphisms, and M and N are bimodules between the rings suggested in the diagram. The filler F maps elements of M to elements of N, and IIRC obeys laws F 0 = 0, F (x + y) = F x + F y, F (r *ₗ x) = f r *ₗ F x, and F (x *ᵣ s) = F x *ᵣ g s. nLab calls this an “intertwiner”, which might be a good enough name.

The usual (“globular”) definition of homomorphism between R-S-bimodules is the definition of intertwiner instantiated with f = id {R} and g = id {S}. The indirection shouldn't cause any problems, because identity homomorphisms should be definitional identities.

[MatthewDaggitt]

Are there supporting definitions for module homomorphisms (likewise for left semimodule, etc)?

As @laMudri says, no not yet. They would live under Algebra.Module.Morphism...

I’m not finding semiring homomorphisms either. Maybe work in progress?

Yup, they are missing. Feel free to add them!

[conal]

Yup, they are missing. Feel free to add them!

I’d like to give it a go.

I see that there are five abstractions to handle: SemiringWithoutAnnihilatingZero, Semiring, CommutativeSemiring, Ring, CommutativeRing. I can start with SemiringWithoutAnnihilatingZero and make a PR to ask for feedback; then when it’s looking good, add the other four. How does this plan sound?

[conal]

I think these five would go into Algebra.Morphism.

[conal]

Make that four, since IsRingMorphism is already there.

[conal]

I'm going to stop trying to count. I keep finding others.

[MatthewDaggitt]

I see that there are five abstractions to handle: SemiringWithoutAnnihilatingZero, Semiring, CommutativeSemiring, Ring, CommutativeRing. I can start with SemiringWithoutAnnihilatingZero and make a PR to ask for feedback; then when it’s looking good, add the other four. How does this plan sound?

Hmm but the morphisms only really care about structure, not the laws. So for example SemiringWithoutAnnihilatingZero, Semiring and CommutativeSemiring would all share the same Semiring(Homo/Mono/Iso)Morphism structures, in the same way that Monoid/IdempotentMonoid, CommutativeIdempotentMonoid all share the same Monoid(Homo/Mono/Iso)Morphism in https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Morphism/Structures.agda.

So I think there's only really three morphism structures missing:

• Lattices
• Semirings
• NearSemirings

but yes feel free to do one and submit a PR for feedback :+1:

[conal]

… So I think there’s only really three morphism structures missing: ...

Make sense. Thank you.

Question: how do IsMonoidMorphism (in Algebra.Morphism) and IsMonoidHomomorphism (in Algebra.Morphism.Structures) relate to each other (and likewise for other such pairs)?

[MatthewDaggitt]

Question: how do IsMonoidMorphism (in Algebra.Morphism) and IsMonoidHomomorphism (in Algebra.Morphism.Structures) relate to each other (and likewise for other such pairs)?

Ah yes, the definitions in Algebra.Morphism should be considered deprecated. Once we've transferred across semirings and (near) semirings, we'll have completely replicated it's functionality and so we can officially deprecate it. Apologies for the poor documentation.