API for quotient semimodules?

Stream: Is there code for X?

[Robert Maxton]

Do we have any existing code for quotients of semimodules Module R Ss without AddCommGroup S? In the process of writing ⨂[R] i, A i ≃ FreeProduct R A (assuming commutativity) I've yak-shaved myself into proving the first isomorphism theorem for noncommutative semirings, and finding myself reinventing a bunch of the Submodule.Quotient API in the process.

(I'm essentially writing down an API for Ideals of Semirings that can be used with RingQuot more freely.)

[Robert Maxton]

Also @Adam Topaz how's that Lawvere theory PR coming along :p

[Adam Topaz]

Sorry! I’ve been crazy busy lately. But I’m working on it slowly but surely

[Robert Maxton]

All good, heh. I probably wouldn't be able to use it here anyway since Mathlib seems to want to avoid making everything depend on category theory for some reason... (which seems like it kind of nullifies the best strengths of category theory, that you can get a whole bunch of deep/important and very general theorems about structure without having to drill down into the structure, but oh well!)

[Robert Maxton]

But it'd be nice to be able to at least check if whatever subgoal I'm trying to prove is in fact true if I'm unsure :V

[Eric Wieser]

I think docs#AddCon.Quotient might be what you want?

[Robert Maxton]

Eric Wieser said:

I think docs#AddCon.Quotient might be what you want?

Not quite, that's too loose. I need compatibility with scalar multiplication -- semimodule, not semigroup. Thanks tho!

[Eric Wieser]

Ah right, I was tricked by the fact that quotients by _submodules_ are implemented as the quotient by the underlying subgroup. I think I have a PR somewhere that adds a typeclass indicating an action is compatible with a congruence relation

[Eric Wieser]

(if you copy the existing pattern directly, you need a smul version of each of the three existing Cons)