Type classes to bundled structures

Stream: new members

[Nicolò Cavalleri]

I read somewhere that mathlib has been moving from type classes to bundled structures. I don't understand what this mean, can someone explain this to me and make me an explicit example?

[Kevin Buzzard]

we use monoid_hom not is_monoid_hom, and have been doing so for some time.

[Nicolò Cavalleri]

Ok I believe I joined the community after this change had already happened... before there was a class is_monoid_hom? Why would you ever do that? I mean what was the advantage of that?

[Kevin Buzzard]

there is a class is_monoid_hom! In the undeprecate branch I'm changing it to a structure. You seem to be speaking as if it is well-known how to do monoid homomorphisms in Lean's type theory. This was not always the case.

[Kevin Buzzard]

We tried is_monoid_hom first, and then monoid_hom, and the latter worked better so that's the one we've been using.

[Nicolò Cavalleri]

Oh I see I guess I just have the perspective from the future but I would see things differently if I were not used to bundled morphisms

[Kevin Buzzard]

Right. When we were building the algebra hierarchy I was asking questions like "so how do we do group homomorphisms", expecting the answer to be well-known, and it turned out that the answer was that one has to experiment to find out. I was very surprised! As a mathematician I just expected everything to be very well-understood, but this was not the case at all.

[Kevin Buzzard]

Even if you look at how they're done in Coq, this doesn't tell you how to do them in Lean, because they emphasize canonical structures and we emphasize type class inference etc.

[Nicolò Cavalleri]

I still don't see why would you make is_monoid_hom a class instead of a structure : Prop in case you want it to be a proposition instead of bundling it

[Kevin Buzzard]

Because you want the composite of two monoid homomorphisms to automatically be a monoid homomorphism.

[Kevin Buzzard]

However it turned out that type class inference would often not fire, and then it turned out that dot notation was super-powerful, and so the bundled version won.

[Kevin Buzzard]

There are still many is_monoid_homs in mathlib, although there are far fewer in the undeprecate branch.

[Kevin Buzzard]

There are also many is_ring_hom, is_submonoid, is_subgroup, is_subring and is_subfields.

[Kevin Buzzard]

I'll push the many hours of work I've done on this branch today so you can see an update :-)

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib/compare/undeprecate

[Yakov Pechersky]

Consider something like polynomial.coeff p n. The way that coeff is defined is separate from the proofs that it's a hom. So one might use is_ring_hom to prove some lemmas, let's say about sums. Sometimes the definition of the function (the data) can come much earlier than the proofs that it's a hom.

[Yakov Pechersky]

Another example is matrix.adjugate. Proving that it's a monoid_hom is more complex than just defining the adjugate.