quotient by monoid action

Stream: Is there code for X?

[Kyle Miller]

Adam Topaz said:

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]

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]

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]

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]

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]

@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]

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]

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]

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]

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]

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]

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

[Oliver Nash]

Understood, and agreed.

[Reid Barton]

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]

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]

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]

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]

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]

@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]

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]

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]

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]

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]

Adam Topaz said:

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]

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]

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

[Oliver Nash]

Ha! I agree with his sentiments.

[Kyle Miller]

(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]

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]

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

[Oliver Nash]

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

[Adam Topaz]

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]

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

[Adam Topaz]

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]

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]

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]

@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]

(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]

How do adjoints work for 2-categories?

[Adam Topaz]

Kevin Buzzard said:

How do adjoints work for 2-categories?

There are various versions. https://ncatlab.org/nlab/show/2-adjunction

[Adam Topaz]

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

[Kevin Buzzard]

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]

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

[Adam Topaz]

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

[Kevin Buzzard]

TIL localisation of a category is naturally an infinity category

[Kevin Buzzard]

(was watching the MSRI lectures by Carlos Simpson)

[Adam Topaz]

Kevin Buzzard said:

TIL localisation of a category is naturally an infinity category

Oh, how does this work?

[Adam Topaz]

And which lectures?

[Kevin Buzzard]

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

[Adam Topaz]

Found it: https://docs.google.com/viewer?url=https://www.msri.org/workshops/862/schedules/25985/documents/50141/assets/85626

[Adam Topaz]

section 2.

[Kevin Buzzard]

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]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Johan Commelin]

Adam Topaz said:

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]

Adam Topaz said:

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]

Adam Topaz said:

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]

Adam Topaz said:

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.