Proposal: Quotient of monoid

Stream: mathlib4

[Kenny Lau]

It has occurred to me that when we form quotient groups, we're basically only looking at the kernel, since that determines everything. But if we're only in a monoid, then we might want to quotient by a "monoidal relation" instead. That means, instead of looking at the information just a subgroup of G, I want to look at subset of M x M satisfying certain properties instead.

Do we have this in Mathlib, and if not, what is the correct set of properties?

[Anatole Dedecker]

Is this docs#Con and docs#Con.Quotient ?

[Kenny Lau]

thanks! that is correct.

[Notification Bot]

Kenny Lau has marked this topic as resolved.

[Kenny Lau]

@Anatole Dedecker does it also have a module version?

[Notification Bot]

Kenny Lau has marked this topic as unresolved.

[Junyan Xu]

I added a Module instance DirectLimit.instModule which should probably be generalized to any quotient by AddCon preserved by scalar multiplication ...

[Yaël Dillies]

Kenny Lau said:

Anatole Dedecker does it also have a module version?

@Eric Wieser was working on one such at some point, but I can't find it in mathlib right now

[Eric Wieser]

It's an open PR about actions on congruence relations

[Kenny Lau]

@Eric Wieser are you referring to #8658?

[Kenny Lau]

It seems like there is some conflict with the existing AddAction.QuotientAction ?

[Yaël Dillies]

Yes indeed it is meant to be a replacement of that

[Eric Wieser]

I think it might predate it

[Kenny Lau]

So what can I do about this situation?

[Eric Wieser]

I'd be happy for you to take over the PR

[Eric Wieser]

I'm afraid I don't remember if there was a technical issue or if I just lost interest

[Eric Wieser]

My guess is that we run into trouble using a typeclass on setoid relations, because r.toAddCon.toSetoid is not reducibly defeq to r.toCon.toSetoid

[Kenny Lau]

can I solve this issue by not using typeclass?

[Eric Wieser]

Unbundling congruence relations might help there, but we do want the bundled version for the lattice

[Eric Wieser]

What are you actually trying to achieve here?

[Kenny Lau]

@Eric Wieser quotient of module by congruence relation, generalisation of Submodule.quotientRel to "modules without negation"

[Kenny Lau]

see the other thread #mathlib4 > Proposal: Symmetric Tensor Power

[Kevin Buzzard]

But why do we care about modules without negation? I nowadays think that "generalisation for generalisation's sake" with no actual examples can be actively bad for the library because it causes disruption and can slow down typeclass inference with no win other than "it now works in situations that nobody needs"

[Eric Wieser]

You only need one particular Quotient then?

[Eric Wieser]

Kevin, I don't think Kenny is proposing an in-place generalization of Submodule, since that doesn't really work anyway

[Eric Wieser]

Making this generalization globally would amount to saying "stop using quotients by subgroups, work directly with the congruence relations"

[Eric Wieser]

(and adjusting the statements of things like the isomorphism theorems to match)

[Eric Wieser]

On second thoughts, I guess we could take the approach used by docs#TwoSidedIdeal, and redefine Subgroup as a Con wrapper with a membership defined by r 1 x

[Kenny Lau]

well i thought some people do use semirings and semimodules