transporting definitions and theorems along isomorphisms.

[kbuzzard]

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.

[digama0]

As I've mentioned in that thread and others, a major component to turning this into a tactic is delineating how precisely it should work. What information is tracked, what does the user supply, how do facts come together to prove the goal? A few "by hand" proofs in a formulaic style also help for getting the hang of how a computer might automate the steps.

[semorrison]

At least for the first paragraph, certainly you should be proving Spec is a functor, and then just use Spec.on_iso f, where f : R ≅ S, an isomorphism in the category of rings. Here Spec.on_iso f : Spec R ≅ Spec S, and that unpacks into a pair of functions, proofs that they are continuous, and proofs they are inverses. functor.on_iso is in mathlib.

[semorrison]

For the exact sequence argument, I would propose we write iso_induction, which lets us take a hypothesis f : X ≅ Y, and write iso_induction f. This will attempt to eradicate any mention of Y from the context, replacing it with X, and replacing every map into or out of Y with their compositions with the appropriate direction of f.

This is by analogy with what happens when we write induction h, when h : a = b.

[semorrison]

There are many different things one would want iso_induction to do, and I think it would be helpful to assemble some test cases for it. Here are two:

import category_theory.isomorphism
import category_theory.types

open category_theory

universes u v

variables (C : Type u) [𝒞 : category.{u v} C]
include 𝒞

example (X Y Z : C) (α : X ≅ Y) (f : Y ⟶ Z) : X ⟶ Z :=
begin
  iso_induction α,
  exact f,
end

variables (D : Type u) [𝒟 : category.{u v} D]
include 𝒟

example (F G : C ⥤ D) (α : F ≅ G) (X : C) (Y : D) (f : G X ⟶ Y) : F X ⟶ Y :=
begin
  iso_induction α,
  exact f,
end

[semorrison]

I just created a branch iso_induction on leanprover-community, which contains those test cases. Of course they fail, because iso_induction doesn't even exist.

If anyone wants to add more test cases, I think that would be really helpful. A lot of the problem here is that we don't know exactly what we even want.

[kbuzzard]

A three-term complex is three abelian groups A,B,C and two group homomorphisms f:A->B and g:B->C such that the image of f is a subset (and hence a subgroup) of the kernel of g. The standard notation for a three-term complex is just A->B->C. The cohomology of a complex is the quotient group ker(g)/im(f).

There is an obvious notion of an isomorphism of three-term complexes. Complexes A->B->C and A'->B'->C' are isomorphic if there are isomorphisms i:A->A' and j:B->B' and k:C->C' such that both squares commute (f'i=jf and g'j=kg). A mathematician would say that isomorphic three-term complexes trivially have isomorphic cohomology.

In Lean I would instinctively work with the (perhaps constructively stronger) notion of an equiv of three-term complexes, and my claim is that equiv three-term complexes trivially have equiv cohomology, and I could envisage one proof being a rewrite of all three equivs.

Note that one could instead ask for something stronger. One could define a morphism between three-term complexes and ask whether this induces a morphism on the cohomology in a natural way (which it does). But my feeling is that this statement has some sort of content -- it is a relatively simple diagram chase. Given this stronger statement one could deduce that equiv three-term complexes have equiv cohomology via some formal argument.

However, the statement that isomorphic complexes have isomorphic cohomology is, I believe, of a fundamentally simpler nature. Am I wrong here? The reason that equiv complexes have equiv cohomology is that the construction of the cohomology of a complex descends to a construction on isomorphism classes because it uses things like image and kernel and quotient which are themselves isomorphism-invariant. In case it is not completely clear what I mean here, I mean that one could talk about an equiv of group homomorphisms; group homs A->B and A'->B' are equiv if there's an equiv A=A' and B=B' making the square commute. The kernels and images and coimages are then all equiv.

[semorrison]

@kbuzzard, I'm having trouble understanding the point you're making. I just want to say that cohomology is a functor from three-term complexes to abelian groups. Then isomorphisms of three-term complexes have isomorphic cohomologies, via functor.on_iso.

At the beginning of your last paragraph, did you mean the statement that equiv complexes have equiv cohomology ...? I'm finding your usage of 'isomorphism' and 'equiv' pretty confusing; it seems in one paragraph ("Note that ...") you're making a distinction between these terms, then in next you're using them interchangeably.

Even if that's what you do mean, as far as I can understand this you're still wrong. :-) When you say "equiv complexes have equiv cohomology ... because ...", the "because" is really saying "it's functorial as it's built out of smaller functorial pieces".

[semorrison]

To continue a little, in the first example above

example (X Y Z : C) (α : X ≅ Y) (f : Y ⟶ Z) : X ⟶ Z :=
begin
  iso_induction α,
  exact f,
end

the way the purported iso_induction tactic would proceed would be to invoke a bunch of "rewrite as functor application" lemmas, to take the hypothesis f : Y ⟶ Z and rewrite it as f : (yoneda Z) Y. The point here is that we have expressed the type as a functor from something to Type applied to the "something" we are trying to eliminate.

Now it's easy (and principled) to produce the new f we want, as let f' : X ⟶ Z := ((yoneda Z).map (α.symm)) f., that is, we just apply the functor to the isomorphism, and then let that eat the old value.

I'm not sure if you can continue this line of thought and reach something satisfactory for three-term complexes and cohomology, but I'll think about it.

[kbuzzard]

I am annoyed by the fact that cohomology of three term complexes, and spectrum of a ring, are functorial for general morphisms. Perhaps I need a better example to show Scott what I am talking about. I wanted to argue that whilst I know equiv R S -> equiv Spec R Spec S follows from the fact that Spec is a functor, I thought that it was less deep in some sense. I'll try and find a better example.

The notation I was trying to stick to was that "isomorphism" was mathematician's isomorphism -- i.e. a bijection with some properties, and "equiv" was Lean's equiv -- a map with another map the other way which was a two-sided identity.

[rwbarton]

Yeah it's annoying that many of these trivial facts about isomorphic things are special cases of less trivial facts which you would want to prove anyways. For example take "if f : R -> S is a ring isomorphism and R is Noetherian then S is Noetherian". Well, it's obvious. But if f is only a quotient map, it's not quite as obvious but still true. So since you were presumably going to prove the version for quotient maps eventually, you may as well prove that and then derive the version for isomorphisms as a corollary--hence you don't really need an easy way to prove "transported" statements in this case either.

I think this example is marginally better than the Spec one, in that Spec being a functor is pretty much a fundamental fact, whereas quotients of Noetherian rings being Noetherian is more like something which just happens to be true. But probably there are still better examples out there.

[kbuzzard]

I see. So in fact predicates are a much better source of these examples. How about "if X and Y are equiv topological spaces then X is compact / connected / Hausdorff / T3.8 / whatever iff Y is". I must confess that I did not need these statements directly, but they are great examples of things which are trivial to a mathematician and which I could imagine being a pain to prove in Lean.

[kbuzzard]

How about this: if R is Noetherian and isomorphic to S, then S is Noetherian. This I might well need.

[digama0]

Not good enough; you already want that statement for quotients, and isomorphisms are quotient maps. So there is another route to the theorem that you would want to have anyway.

[kbuzzard]

Kenny just gave me an example. He has proved that if S is a subring of R and R is noetherian as an S-module then R is integral over S. He now needs to prove that if S and T are subrings of R with S subset T and T is noetherian as an S-module then T is integral over S. This is more than math-trivial -- this is math-completely content free, because a mathematician cannot tell the difference between a ring and a subring.

[semorrison]

What's the difficulty? Don't you just say: "T a subring of R" implies "T a ring", "S a subset of T and a subring of R" implies "S is a subring of T", and then apply Kenny's theorem? There is a tiny piece of math content (the second implication), but I'd guess Lean will happily accept those three steps.

On Sun, Nov 11, 2018 at 7:24 AM Kevin Buzzard notifications@github.com wrote:

Kenny just gave me an example. He has proved that if S is a subring of R and R is noetherian as an S-module then R is integral over S. He now needs to prove that if S and T are subrings of R with S subset T and T is noetherian as an S-module then T is integral over S. This is more than math-trivial -- this is math-completely content free, because a mathematician cannot tell the difference between a ring and a subring.

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/leanprover/mathlib/issues/408#issuecomment-437618685, or mute the thread https://github.com/notifications/unsubscribe-auth/AAdLBKbCV8BMCktt9Dppqp5J908m9bG3ks5utzX9gaJpZM4XMiMS .

[kbuzzard]

T isn't a ring, it's a term. There's a corresponding subtype T'. But now S isn't a subring of T', S is isomorphic to a subring S' of T'. So now we need that if T is integral over S then T' is integral over S'.

[semorrison]

Maybe the explicit context would be helpful, here. I guess I don't know what T is noetherian as an S-module means when S and T are only subrings to begin with.

[kbuzzard]

S and T are subrings of R, and S is contained in T. So the natural inclusion from S to T is a ring homomorphism, and now T becomes a module over the ring S, so now you can start throwing around predicates for these modules is being Noetherian.

[kbuzzard]

I was thinking about some post-MSc level commutative algebra today and perhaps these gave me a bunch of other examples. Here's a bunch of predicates on Noetherian local rings: "Universally catenary", "Cohen–Macaulay", "Gorenstein", "complete intersection", "regular". Some of these are very poorly behaved with respect to morphisms, because they represent local geometric properties which will not be preserved under ring injections or surjections in general. Tell a mathematician that we can't prove that if R is regular and S is isomorphic to R then S is regular and they would suggest our system was broken. And it kind-of is -- I still believe this. So there are 5 challenges, but regular is not too hard to understand so we could start with regular.

https://en.wikipedia.org/wiki/Regular_local_ring

[semorrison]

Is even a local ring an interesting enough predicate? How well does our current infrastructure prove (S \iso T) \to (is_local_ring S \iff is_local_ring T)?

My preference here would be to have a predicate is_local on (bundled) commutative rings, and then to show that this was the "on objects" part of a functor from CommRing to Prop. One could hope that this "showing" was done with a derive handler.

I've been exploring changing Type to Sort (almost) everywhere in the category theory library, which seems likely to be a prerequisite for doing this.

[rwbarton]

I've been exploring changing Type to Sort (almost) everywhere in the category theory library, which seems likely to be a prerequisite for doing this.

I'm all for doing this! My guess is that we may run into things in core Lean which haven't been generalized to Sort, but if that's the only obstruction, we should just add Sort-versions of them to mathlib.

However, "being a local ring" is not a functor from CommRing to Prop, because f : R -> S and R local does not imply S local. Unless you meant a functor from (CommRing, iso) -> Prop, but then it's not much different than just proving the invariance under isomorphisms directly, although I suppose it could be a useful reformulation for technical reasons.

I do think "local ring" would be a good test case. I would stipulate that you have to use the "unique maximal ideal" definition, since you're going to need to be able to deal with higher-order concepts like this in order to handle other things like Krull dimension. Concretely what you would need to do for local rings is, for a ring isomorphism R ~= S, understand that set R is also isomorphic to set S, and that properties like the inclusion relation and being an ideal of R (respectively, of S) correspond on the two sides. It seems to capture most of the kinds of reasoning that one would want, while still being relatively simple.

[jcommelin]

Alternatively, apply Spec and prove that for topological spaces "having a unique closed point" is invariant under homeomorphisms.

[semorrison]

Sorry, yes, I did mean (CommRing, iso). We just need a wrapper (either isos, or perhaps core, which is used in the tensor category literature) that has a category instance that just uses the isomorphisms.

We've got a tiny stub of the typeclass functorial for decorating an object level function with the map on morphisms and evidence of functoriality.

We could add iso_functorial, for decorating a function f : C \to D with the additional data of a functor core C \func core D.

Finally, I'd want to do some experiments to see how far we could take using the typeclass mechanism to create instances of iso_functorial. It's not obvious to me at this point how far we would get. We could augment this with a derive handler that can use arbitrary meta-programming, and of course write instances entirely by hand.

On Mon, Feb 25, 2019 at 4:30 AM Johan Commelin notifications@github.com wrote:

Alternatively, apply Spec and prove that for topological spaces "having a unique closed point" is invariant under homeomorphisms.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/leanprover-community/mathlib/issues/408#issuecomment-466797252, or mute the thread https://github.com/notifications/unsubscribe-auth/AAdLBH_3pHSxy7lHYgNfN1dKF5kKMT7iks5vQswngaJpZM4XMiMS .

[kbuzzard]

OK great, "is_local" sounds like a good predicate. I would hence be interested in knowing thoughts on automation which would show that if R is local and S is isomorphic to R then S is local.

[kbuzzard]

Here's one that came up in my undergraduate exams. If R is a binary relation on a set X, and we have an equiv X <-> Y, then R should push forward to a binary relation S on Y, and if R is reflexive/symmetric/transitive then so is S. My feeling is that this proof should be generated automatically. Can this be done yet?