mathlib

mathlib copied to clipboard

There's a construction called Spec which eats a commutative ring R and spits out a topological space Spec R. To a mathematician it is trivially true that if we have an isomorphism f : R -> S then we get an induced isomorphism Spec R -> Spec S. In Lean one would formalise this as follows: if we have an equiv between R and S such that both morphisms are ring homomorphisms, then we get an induced equiv between Spec R and Spec S such that both maps are continuous.

Currently in Lean this seems to be hard to do. I believe Simon Hudon had some ideas about this in the (huge) thread

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.22canonically.22.20identifying.20two.20types

Example quote from April 27 -- I asked how to prove in Lean that if A->B->C was an exact sequence of abelian groups and we had isomorphisms A=A' and B=B' and C=C' then the induced exact sequence A'->B'->C' was exact, and Kenny wrote a 70 line proof. But in my mind the proof should be rw [iA,iB,iC] with iA the isomorphism A=A' etc. We could talk about homotopy type theory here, but that is not relevant to this issue.

My understanding of that thread was that Simon started talking about a tactic which would prove things like this, and then Scott got involved and suggested things like @[derive transportable] and this:

https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/.22canonically.22.20identifying.20two.20types/near/125774155

...but then Mario pointed out subtleties and Johannes later on (perhaps in another thread) suggested that perhaps transfer(?) could already do a lot of this, and then I think the momentum died down.

This issue is to put on record that seems to be a hole in Lean of the "easy in maths" form, and for someone like me who markets Lean to mathematicians, these holes are embarrassing.