Equalities of morphisms

Stream: maths

[Chris Hughes]

I made a quick gist about how to prove associativity of polynomial in a very neat way using just the universal property of the free module, and defining multiplication as a bilinear map. Then using the hom_ext lemma and the lift_X lemma, and unfolding the definition of linear map composition, you can quickly a non trivial theorem if you set up the library really nicely. It is a very slow proof at the moment. It can fit onto two lines, but I wrote a longer proof to illustrate the strategy.

I think that using universal properties in the form of computation rules like lift_X and extensionality lemmas like hom_ext is a very powerful technique, and if mathlib were set up correctly we could potentially prove a lot of equalities of homomorphisms really painlessly. I think this requires some thought however. Every homomorphism that is defined needs to have rules about what it does on a basis for a free module, or what it does on the base ring and X for polynomials etc. You also need to be able to convert an equality of applied morphisms to an equality of morphisms, which might involve things like converting applied ring equivs into a composed ring hom, or some more sophisticated automation in the case of closed categories like modules to do the conversion of mul p (mul q r) into an application of a trilinear map. In the case of closed categories it also might need to be handle inheritance of universal properties, e.g. if $M$ is a free module, then $Hom(M, N)$ is a product of modules. It might need to have have some form of assoc_rw to apply things like eval_comp_C for polynomials. It also needs to be able to handle multiple universal properties at once, polynomials have a UMP in both the category of R-modules and the category of R-algebras, and the category of rings, int is both a free group and the initial ring and the initial comm ring. I feel like this might require some actual understanding of category theory to do really nicely. It also needs to be much faster than the example in the gist.

Do people have thoughts on this?

[Johan Commelin]

Is what you are describing the same technique as what I'm doing here: https://github.com/leanprover-community/lean-liquid/blob/master/src/breen_deligne/universal_map.lean#L335
There is a lot of

show foo.comp bar = blabla,
ext,
simp,

in that file.

[Chris Hughes]

I think so

[Chris Hughes]

The trouble is the appropriate simp or ext lemmas aren't always there because we haven't got strict conventions on this.

[Scott Morrison]

The whole category theory libray is designed around proving evertthing by { ext, simp, }, so I'm all in favour of this. :-)

[Eric Wieser]

I thing the convention to allow ext lemmas to enable this kind of thing is quite well established already, just not ubiquitous