## Stream: Is there code for X?

### Topic: quotient by monoid action

#### Kyle Miller (Sep 23 2020 at 08:40):

It's complicated to describe in this case. The best I can come up with is this: The forgetful functor from sets with a group action to sets with a monoid action has a left adjoint. (It's a souped up version of the groupification functor from monoids to groups.) The equivalence relation is "essentially" the equivalence relation induced by the group action via this left adjoint (by this I mean they have the same quotients, but there can be some analogues of zero divisors which will complicate things). I don't know if any of this makes sense.

This was an educational exercise in universal algebra, and I think I've verified that it all works (formalized in Lean!) while also proving some universal properties along the way. I defined the universal enveloping group of a monoid (the non-commutative version of the Grothendieck group; I found the nomenclature in Bergman's book "An Invitation to General Algebra and Universal Constructions"), showed it was the universal group that factors homomorphisms from a monoid to a group, defined a "universal enveloping group action" associated to a monoid action, which factors homomorphisms of monoid actions to group actions, then defined two quotients. The first was quot (λ (x y : α), ∃ (a : M), x = a • y) and the second was the quotient of the universal enveloping group action by the universal enveloping group. Lastly, I showed there was an equivalence between these two quotients.

The code is too big for posting here, so here's a link to a gist: https://gist.github.com/kmill/af2bbe856ea66e147ef699365a85b763

I didn't show anything was functorial or explicitly adjoint.

#### Kyle Miller (Sep 23 2020 at 08:42):

After all this, it seems to me it's all just a fancy way of saying that equivalence relation you're quotienting by is the one generated by (λ (x y : α), ∃ (a : M), x = a • y) :smile:

#### Kevin Buzzard (Sep 23 2020 at 11:05):

Universal enveloping algebras are important in the theory of Lie algebras and associative algebras; there was a recent PR by Oliver Nash about them. The reason I mention this is that when we were starting on schemes I needed localisation of rings and Kenny Lau formalised it and got it into mathlib, and then later on we realised that localisation started earlier in the story and there should be a localisation theory for monoids, which Amelia Livingston wrote and it involved a major refactor of localisation of rings.

#### Kevin Buzzard (Sep 23 2020 at 11:06):

If there's some sort of analogous story here, where the universal enveloping group should be done before the universal enveloping algebra, or perhaps some more general theory of universal enveloping stuff should be developed, then now would be a good time to figure out how to formalise this stuff in a good generality as far as mathlib goes.

#### Kevin Buzzard (Sep 23 2020 at 11:08):

Just thinking about it now, I was very enthusiastic when Oliver mentioned universal enveloping algebras to me (because I need them for the Langlands program in order to state the definition of an automorphic form) but now I'm worried we've "started too far down the line" like we did when localising rings instead of monoids. Note that Oliver's PR is still open (he's having a Lean break right now before he comes to work for me doing Lean full time in April :D)

#### Scott Morrison (Sep 23 2020 at 11:11):

@Oliver Nash's PR (#4041) is still in progress --- we did a refactor of @Adam Topaz's construction of the tensor algebra as a quotient of the free algebra first. The universal enveloping algebra construction will then be done as a quotient of the tensor algebra, I guess.

#### Oliver Nash (Sep 23 2020 at 11:13):

I actually had a go at rebasing that PR on top of the refactored ring_quot and tensor_algebra stuff yesterday evening and ran into annoying issues with typeclass inference.

#### Oliver Nash (Sep 23 2020 at 11:17):

The issue is that the tensor algebra only has the structure of a semiring but I need the actual ring structure on the quotient. This is theoretically fine because our scalars contain -1 and so we get the subtraction by multiplying by that. But there are then two semiring structures: the original one and the one provided by ring.to_semiring, and they're not definitionally equal.

#### Oliver Nash (Sep 23 2020 at 11:18):

And for the Lie algebra stuff to work, the algebra structure should use the semiring structure from ring.to_semiring but the algebra structure on tensor_algebra is the other one.

#### Oliver Nash (Sep 23 2020 at 11:20):

I'm fairly sure I can massage this all into a good form, especially as corresponding problems must arise anywhere in the linear algebra parts of the library where we use subtraction, but I couldn't quite get it to work yesterday

#### Oliver Nash (Sep 23 2020 at 11:22):

Finally, I take the point Kevin is making about the lessons learned from ring localisation (I am aware of this history though I didn't follow it in detail). I'll have a little time again this evening and will look again, bearing in mind that it might be worth holding off till some more basic universal enveloping structure is in place.

#### Kevin Buzzard (Sep 23 2020 at 11:28):

I'm definitely not saying "we're doing it wrong", I'm just saying "let's check we're doing it right".

#### Oliver Nash (Sep 23 2020 at 11:28):

Understood, and agreed.

#### Reid Barton (Sep 23 2020 at 13:05):

The Lie bracket uses both multiplication and subtraction, so I don't think the enveloping algebra of a Lie algebra is a special case of something for a "Lie monoid" the same way that localization for rings was a special case of localization for monoids.

#### Reid Barton (Sep 23 2020 at 13:11):

On the other hand localization of commutative monoids and this "universal enveloping group of a monoid" are both instances of "invert some elements of a monoid". But the commutative localization is really a special case that has extra properties, so it's worth keeping even if we also have general noncommutative localizations.

#### Reid Barton (Sep 23 2020 at 13:13):

One of my slow-moving side projects is to extend the commutative localization to Ore localizations in the noncommutative case, which have the same extra properties, and also extend it to localizations of modules--the construction for modules is the same as for the monoids themselves so I guess it should be possible to take the localization of modules as the starting point, and then equip it with a monoid structure.

#### Adam Topaz (Sep 23 2020 at 14:07):

I'm confused about the semiring vs ring issue... The only additional data is negation, which you define as scalar multiplication by -1. Presumably you would extend the existing semiring structure, right? So why are the two semiring instances not defeq?

#### Adam Topaz (Sep 23 2020 at 14:11):

A good analogous case of this, which I assume is in mathlib, is the fact that a semimodule over a ring is an add_comm_group, and not just an add_comm_monoid. How does mathlib handle this case? (Assuming it does at all!)

#### Oliver Nash (Sep 23 2020 at 20:36):

@Adam Topaz I believe the problem is that ring does not extend semiring. I don't understand the details of Lean's unification well enough to know for sure but it might be down to the fact that semiring carries zero_mul and mul_zero around with it. Check out ring.to_semiring: https://github.com/leanprover-community/mathlib/blob/7cf8fa629b389ac6e6615f0361225c515272fe98/src/algebra/ring/basic.lean#L413

#### Oliver Nash (Sep 23 2020 at 20:39):

Anyway I've got 30 minutes to look at this again now so hopefully I'll be able to bottom out. I agree with Reid that there is no case to be made for a weird Lie monoid structure.

#### Oliver Nash (Sep 23 2020 at 20:43):

Though it occurs to me that a horrendous workaround for my semiring issue (which I don't seriously propose) would be to avoid having to define a ring structure on the tensor algebra by quotienting by the relation generated by: i(⁅x, y⁆) + i(y)i(x) ∼ i(x)i(y).

#### Adam Topaz (Sep 23 2020 at 20:53):

Oliver Nash said:

Though it occurs to me that a horrendous workaround for my semiring issue (which I don't seriously propose) would be to avoid having to define a ring structure on the tensor algebra by quotienting by the relation generated by: i(⁅x, y⁆) + i(y)i(x) ∼ i(x)i(y).

This seems like a good solution to me! All the conditions for a Lie algebra can be written using addition only anyway :)

#### Adam Topaz (Sep 23 2020 at 20:54):

But the ring/semiring thing seems like a more serious problem, doesn't it? The same issue would pop up whenever you have a semiring which just so happens to be a ring with respect to negation defined somehow.

#### Oliver Nash (Sep 23 2020 at 20:57):

But the ring/semiring thing seems like a more serious problem, doesn't it? The same issue would pop up whenever you have a semiring which just so happens to be a ring with respect to negation defined somehow.

It does indeed seem more serious. I'm currently working to make sure I have understood this correctly, and think about what to do if so.

#### Adam Topaz (Sep 23 2020 at 20:59):

Maybe I should mention that I originally defined the tensor algebra over rings, but then switched to semirings because it felt like "a generalization"...

#### Adam Topaz (Sep 23 2020 at 21:01):

I blame @Johan Commelin https://github.com/leanprover-community/mathlib/pull/3531#discussion_r460123649
:stuck_out_tongue_wink:

#### Oliver Nash (Sep 23 2020 at 21:03):

Ha! I agree with his sentiments.

#### Kyle Miller (Sep 23 2020 at 21:11):

(Regarding the code I wrote, I'm happy enough with it just being an exercise, but if mathlib doesn't already have the universal enveloping group of a monoid, which I couldn't easily find already, I'm willing to clean it up for a PR. It would be cool if there were an automatic generator for this stuff [wasn't there a post a month ago about this?], but for now I suppose grad student labor suffices.)

@Adam Topaz Was there an abstract nonsense reason for the quotients being equal? Is it that in each case the quotient is the coinvariants, which is a colimit, so the group-action-ification functor, which is left adjoint, preserves it?

#### Adam Topaz (Sep 23 2020 at 21:13):

Kyle Miller said:

Adam Topaz Was there an abstract nonsense reason for the quotients being equal? Is it that in each case the quotient is the coinvariants, which is a colimit, so the group-action-ification functor, which is left adjoint, preserves it?

Mumble mumble mumble left adjoint mumble mumble.

#### Adam Topaz (Sep 23 2020 at 21:13):

I don't know, it seemed obvious that the construction should work.

#### Oliver Nash (Sep 23 2020 at 21:14):

@Kyle Miller I for one think it would be worth turning that gist into a PR.

#### Adam Topaz (Sep 23 2020 at 21:15):

I guess in some sense eqv_gen is the left adjoint of the forgetful functor from equivalence relations to relations, groupification is the left adjoint of the forgetful functor from groups to monoids,.

#### Adam Topaz (Sep 23 2020 at 21:16):

Oh, and I certainly agree that the groupification should be in mathlib :)

#### Adam Topaz (Sep 23 2020 at 21:18):

And yes, it would be cool if we had an automatic generator. This is a special case of a forgetful functor associated to a morphism of theories in the sense of universal algebra, and these always have left adjoints.

#### Kyle Miller (Sep 23 2020 at 21:23):

While working on this, it felt like I was doing one of your Math 250B assignments again, but perhaps a bit more satisfying since it's formally verified (though I don't remember us covering any universal algebra -- I'd just sat in for a couple of Prof. Bergman's lectures and glance at his book occasionally)

#### Kyle Miller (Sep 23 2020 at 21:26):

A tangential question I've had in the back of my mind for a while: could anyone point me toward the state-of-the-art in deriving a confluent rewrite system from a list of axioms? I know a little about the Knuth-Bendix algorithm, though I haven't seen a version of it for tree rewriting, only monoid/group word rewriting. For axiom sets for which the algorithm succeeds, it might be a nice way to generate simp lemmas.

#### Adam Topaz (Sep 23 2020 at 22:08):

@Kyle Miller I'm pretty sure the "general nonsense" argument you mentioned using the fact that the quotient can be seen as a colimit will work. I wonder how one might formalize this in lean? The first step is that it's the colimit of a functor from $\mathcal{C}_M$ to $\mathrm{Type}$ where $\mathcal{C}_M$ is the category with one object $\star$ and where $\operatorname{Hom}(\star,\star) = M$ as a monoid. Does mathlib have the construction of such a category assocaited to a monoid?

#### Adam Topaz (Sep 23 2020 at 22:09):

(Note that there is a left adjoint from the 2-category of groupoids to the 2-category of categories, and the groupification is a special case of this :smile: )

#### Kevin Buzzard (Sep 23 2020 at 22:31):

How do adjoints work for 2-categories?

#### Adam Topaz (Sep 23 2020 at 22:32):

Kevin Buzzard said:

How do adjoints work for 2-categories?

#### Adam Topaz (Sep 23 2020 at 22:33):

I guess I'm thinking of a "strict 2-adjunction" in this case?

#### Kevin Buzzard (Sep 23 2020 at 22:34):

Yeah the reason I asked was that I could naively imagine more than one definition -- and indeed there seems to be more than one definition :-)

#### Adam Topaz (Sep 23 2020 at 22:34):

I should probably open a PR for this:
https://github.com/leanprover-community/mathlib/blob/cat_localization/src/category_theory/localization.lean

#### Adam Topaz (Sep 23 2020 at 22:35):

But it's already a month behind, so it might already be broken with up-to-date mathlib.

#### Kevin Buzzard (Sep 23 2020 at 22:35):

TIL localisation of a category is naturally an infinity category

#### Kevin Buzzard (Sep 23 2020 at 22:35):

(was watching the MSRI lectures by Carlos Simpson)

#### Adam Topaz (Sep 23 2020 at 22:36):

Kevin Buzzard said:

TIL localisation of a category is naturally an infinity category

Oh, how does this work?

#### Adam Topaz (Sep 23 2020 at 22:37):

And which lectures?

#### Kevin Buzzard (Sep 23 2020 at 22:38):

He gave a series of lectures on infinity categories at MSRI a few years ago, I'll dig out the link

section 2.

#### Kevin Buzzard (Sep 23 2020 at 22:40):

Apparently what people like me who only know about categories think of as localisation of a category at a collection of morphisms is actually a composition of true localisation (an infinity category) followed by 1-truncation (replace Hom(X,Y) by the set of isom classes)

#### Kevin Buzzard (Sep 23 2020 at 22:41):

Yes that link is exactly it -- I was watching the videos whilst exercising :-)

#### Adam Topaz (Sep 23 2020 at 22:41):

In case anyone else is interested, here's the link to the video: https://www.msri.org/workshops/862/schedules/25985

#### Adam Topaz (Sep 23 2020 at 22:42):

So the groupification of a monoid is naturally an $\infty$-groupoid?!

#### Johan Commelin (Sep 24 2020 at 05:48):

I blame Johan Commelin https://github.com/leanprover-community/mathlib/pull/3531#discussion_r460123649
:stuck_out_tongue_wink:

I'll take the blame :expressionless: :wink:

#### Johan Commelin (Sep 24 2020 at 05:53):

Kyle Miller I'm pretty sure the "general nonsense" argument you mentioned using the fact that the quotient can be seen as a colimit will work. I wonder how one might formalize this in lean? The first step is that it's the colimit of a functor from $\mathcal{C}_M$ to $\mathrm{Type}$ where $\mathcal{C}_M$ is the category with one object $\star$ and where $\operatorname{Hom}(\star,\star) = M$ as a monoid. Does mathlib have the construction of such a category assocaited to a monoid?

Yup we have this... docs#single_obj

#### Reid Barton (Sep 24 2020 at 13:20):

So the groupification of a monoid is naturally an $\infty$-groupoid?!

In more classical language, this is the classifying space or nerve construction

#### Oliver Nash (Sep 24 2020 at 17:08):

This seems like a good solution to me! All the conditions for a Lie algebra can be written using addition only anyway :)

I decided to see how this would look and maybe it's OK after all: https://github.com/leanprover-community/mathlib/pull/4041 I still want to spend some time to understand the inference issues I encountered a bit better, but I've warmed up to what I at first thought was a dirty hack.

Last updated: May 16 2021 at 05:21 UTC