extensionality for functors

Stream: new members

[Justus Springer]

Hi,
correct me if I'm wrong: In mathlib, there seems to be no extensionality Lemma for functors.
Moreover, I noticed that I can't even state extensionality for functors without getting a type error:

import category_theory.functor

open category_theory

variables (C D : Type*) [category C] [category D]

--doesn't even typecheck
example (F G : C ⥤ D) (h₁ : F.obj = G.obj) (h₂ : F.map = G.map) : F = G := sorry

and it makes sense, because the types of F.map and G.map are a priori different, but of course they actually aren't because I'm requiring F.obj = G.obj as a hypothesis as well. I remember seeing issues like this in a CS class on Coq once, where because of dependently typed hypothesis, we couldn't even state a particular Lemma. Unfortunately, I don't remember how we worked around this problem, if we did...

Is there a workaround? And how can I prove that two functors are equal, or is this something that we shouldn't even do in mathlib?

[Markus Himmel]

We actually do have docs#category_theory.functor.ext, which uses docs#category_theory.eq_to_hom to work around the problem you described. As you already guessed, this is rarely a good idea. In the vast majority of cases, it is much better to instead provide a natural isomorphism between the two functors.

[Markus Himmel]

More generally, unless your category is some kind of partial order, the moment when you start talking about equality of objects, it is probably a good idea to think about whether there is a better approach that avoids this (and talks about isomorphisms instead).

[Eric Wieser]

Note that you can state the lemma by using docs#heq (==) between the maps

[Justus Springer]

Oh, I didn't see that one, thanks!

[Justus Springer]

Markus Himmel said:

More generally, unless your category is some kind of partial order, the moment when you start talking about equality of objects, it is probably a good idea to think about whether there is a better approach that avoids this (and talks about isomorphisms instead).

If we are talking about paper-math, I 100% agree with this statement. But I thought since Lean doesn't have univalence, isomorphisms would be a pain to work with, since we can't rewrite with them. Is this not the case?

[Justus Springer]

I don't have any experience with isomorphisms in Lean yet, so any additional information about how to properly use them would be nice :)

[Markus Himmel]

They're not exactly fun to work with, but I would argue that dealing with heq or eq_to_hom is even worse. In my experience, with well-chosen simp lemmas, many isomorphisms that could potentially be annoying are almost invisible.

[Adam Topaz]

We also have docs#category_theory.functor.hext if you REALLY want to worry about heq

[Adam Topaz]

These are not marked with @[ext] because you should think twice about using them :wink:

[Eric Wieser]

How does Coq handle heq?

[Mario Carneiro]

Not very well, because it doesn't have proof irrelevance

[Mario Carneiro]

It's possible to define, of course, but it doesn't have a lot of the properties you would want. It's better to use pathovers as in HoTT

[Mario Carneiro]

inductive path {α} (F : α → Type) {a} (fa : F a) : ∀ {b}, F b → a = b → Prop
| refl : path fa rfl

notation a `=[`F`;`p`]` b := path F a b p

[Eric Wieser]

I remember seeing a thread about paths a while ago; has it been concluded they're less convenient to work with than heq, or has no one really tried them out seriously in lean?

[Mario Carneiro]

No one has tried them out seriously. I think they would be better than heq, but not as good as avoiding them entirely using sigma-type encodings

[Mario Carneiro]

One problem with pathovers is that you eventually find yourself needing pathoverovers too

[Eric Wieser]

Is path F a b p different to eq.rec a p = b other than having F explicit unlike the C of docs#eq.rec?

[Eric Wieser]

I tried out using eq.rec instead of ==, but the elaborator makes it harder for me than I'd like:

/-- With `heq` -/
example {α : Sort*} {β : α → Sort*} {γ : Π a, β a → Sort*}
  (x y : Σ a b, γ a b) (h1 : x.1 = y.1) (h2 : x.2.1 == y.2.1) (h3 : x.2.2 == y.2.2) :
  x = y :=
begin
  cases x, cases y, cases x_snd, cases y_snd, cases h1, cases h2, cases h3, refl
end

@[ext]
def sigma_ext_rec {α : Sort*} {β : α → Sort*} :
  ∀ {x y : Σ a, β a} (h1 : x.fst = y.fst) (h2 : h1.rec x.2 = y.2), x = y
| ⟨x1, x2⟩ ⟨y1, xy⟩ rfl rfl := rfl

/-- With `eq.rec` -/
example {α : Sort*} {β : α → Sort*} {γ : Π a, β a → Sort*}
  (x y : Σ a b, γ a b)
  (h1 : x.1 = y.1)
  -- `(h1.rec x.2).1 = y.2.1` isn't accepted by the elaborator
  (h2 : (eq.rec x.2 h1 : Σ a, γ y.1 a).1 = y.2.1)
  -- `h2.rec (h1.rec x.2).2 = y.2.2` isn't accepted by the elaborator
  (h3 : (eq.rec (eq.rec x.2 h1 : Σ a, γ y.1 a).2 h2 : γ y.1 y.2.1) = y.2.2) :
  x = y :=
begin
  -- the previous proof would work too
  ext, exact h3,
end

[Junyan Xu]

I guess it's still preferable to replace isomorphisms by equalities whenever possible? For example I was just able to get :

lemma map_id' : map (𝟙 X) = 𝟭 (opens X) :=
by { unfold map, congr, ext, refl, ext }

in place of https://leanprover-community.github.io/mathlib_docs/topology/category/Top/opens.html#topological_space.opens.map_id
I'm looking into this because I want to prove an equality involving pushforward of sheaves, in turn because I want to show any pushforward of a sheaf is a sheaf (using the pairwise_intersection condition), where I'd like to show two cones (implemented as natural transformation between functors) inside is_limit are equal.

BTW I find that initializing Lean in the file presheaf.lean (or maybe it's Top/opens.lean) cost a long time and 2-3 GB memory on my machine, even though I have freshly made .olean files with mk-cache and get-cache ...

[Scott Morrison]

No, the opposite, when talking about functors it is better to replace equalities with isomorphisms, because relying on the equalities will result in badness (either eq.rec / cast in goals, or heavy refl proofs) down the line that you don't have control over, whereas working with isomorphisms (which is admittedly more cumbersome) you at least know what you're getting into.

[Scott Morrison]

(Opening topology/sheaves/presheaf.lean after restarting the Lean server takes <5s on my machine. Top/opens.lean took more like 2s.)

[Junyan Xu]

Hmm, revert to an earlier commit fixes the problem (though it still takes several minutes to initialize on my machine, which is normal) and the memory used is now less than 1.5 GB.
I guess the problem is that I added lemmas named op_comp and comp_assoc to category_theory/opposite.lean and functor.lean and these may break some proofs in other files due to name conflict (in fact I fixed two in opposite.lean) and these broken proofs may be imported by the files opens.lean and presheaf.lean I am working on, so Lean is confused and stays in the yellow busy state. Is there an easy way to confirm this is the case? Lean doesn't output anything when busy, and mk-cache doesn't detect the problem (it doesn't abort or output anything).

Scott Morrison said:

(Opening topology/sheaves/presheaf.lean after restarting the Lean server takes <5s on my machine. Top/opens.lean took more like 2s.)

[Junyan Xu]

I guess the equalities should still be useful; one can easily construct an iso from an eq. Maybe just add a ' or _eq to the eq's name and construct the iso using it? Would you approve this kind of change?
Scott Morrison said:

No, the opposite, when talking about functors it is better to replace equalities with isomorphisms, because relying on the equalities will result in badness (either eq.rec / cast in goals, or heavy refl proofs) down the line that you don't have control over, whereas working with isomorphisms (which is admittedly more cumbersome) you at least know what you're getting into.

[Kevin Buzzard]

Compile the file you think you might have broken on the command line

[Junyan Xu]

Junyan Xu said:

I'm looking into this because I want to prove an equality involving pushforward of sheaves, in turn because I want to show any pushforward of a sheaf is a sheaf (using the pairwise_intersection condition), where I'd like to show two cones (implemented as natural transformation between functors) inside is_limit are equal.

Alright I finished the proof, but I'm not really sure how it works! Especially where the congr and convert tactics (or functor.hext which uses congr) which often reduces an eq goal to some eq goals but also some heq goals.
Although it's in mathlib that we can transfer is_limit between two isomorphic cones, we can't state that two cones / natural transformations are isomorphic before proving that they're over the same (defeq) functor / between the same two functors, and there doesn't seem to be a more sophisticated theorem that applies (maybe more higher category theory needs to be developed), so I'm content with the current approach. Would be fantastic if someone can further golf it.

[Scott Morrison]

Probably best to make a PR so others can take a look taking advantage of precompiled oleans.

[Junyan Xu]

Done (#9801)! The branch doesn't have to be in the main leanprover-community repo for oleans to be generated, right?

[Scott Morrison]

It does, unfortunately, because the oleans need to be deployed to our server.

[Scott Morrison]

I just sent you an invitation with write access to non-master branches. Could you close your PR and open a new one from a branch on the main repo?

[Andrew Yang]

On a side note, I am also actively working towards the adjunction based on the blueprints of Justus. If you are planning to your proofs into mathlib, it would be great if we could coordinate together and split the work to avoid stepping on each other's toes.

[Junyan Xu]

Scott Morrison said:

I just sent you an invitation with write access to non-master branches. Could you close your PR and open a new one from a branch on the main repo?

Thanks! I accepted and made new PR #9802

[Junyan Xu]

Andrew Yang said:

On a side note, I am also actively working towards the adjunction based on the blueprints of Justus. If you are planning to your proofs into mathlib, it would be great if we could coordinate together and split the work to avoid stepping on each other's toes.

Of course! All my current work is in the PR. Now that I proved f_* O_X is a sheaf, it's just a matter of plugging in the arguments to define the sheaf morphism in the counit of the adjunction.

[Junyan Xu]

(Yeah, I now realize the unit-counit approach is simpler and no longer pursues the hom_equiv route.)

[Andrew Yang]

As for gluing morphisms on sheaves, the equivalent formulation on my path was just finished some days ago at #9694.
I suppose it would be better to use that to avoid duplicate code.
Also IMHO the fact that the pushforward of a sheaf is a sheaf should probably go in src/topology/sheaves/stalks.lean.
(another way to show this is to show that continuous maps induces continuous functors between sites, which could potentially unlock more stuff such as pullbacks, but I doubt we would need that generality for now).

[Junyan Xu]

Congrats on your colossal series of work! If you can just prove the last theorem from basis_le.lean then I can mostly abandon the rest of the file. lim_basis_le_of_sheaf and mono_to_basis_le_of_sheaf might be useful for other purposes and it would be nice to derive these specialized versions from more general versions that you probably already proved.
The pushforward of sheaf thing doesn't involve stalks at all, so I think should just go into topology/sheaves/sheaf.lean, which should import the pairwise_intersection file and prove the is_sheaf version of the theorem. If pairwise_intersection is promoted to the official definition then there would be nothing to prove. In fact the proof is rather trivial and I expect the same for the sites version, but the type system complicates matters. I even think it should be proven by defeq under the "ideal" defeq, but Lean's algorithmic defeq doesn't recognize it. Probably Lean has problem defequating one morphism from le_supr and another from mapping le_supr by a functor (opens.map f); for sites this issue may not exist. (Or maybe the problem is elsewhere: preimage of intersection seems to be defeq, but preimage_Union seems not. opens X as subtype of set X seems fine, so seems the plift ulift to promote open set inclusion to a morphism.)

[Andrew Yang]

Oh yes I mistyped...
I meant sheaf.lean. :sweat_smile:

[Andrew Yang]

The sites version of the pushforward stuff is probably #9691.
That said, to show that continuous functions are compatible_preserving, the right way is probably to show that it preserves finite limits and to use #9519. However, Bhavik seems to have some more thoughts on flat functors, and thus it would probably take some time before It goes into mathlib.

At first glance, mono_to_basis_le_of_sheaf_condition seems to be either docs#category_theory.presieve.is_separated_for.ext or cover_dense.ext in #9694. As for lim_basis_le_of_sheaf, the sheaf condition of sites is not defined in terms of limits, and thus there probably would not be an analogue for now.

[Kevin Buzzard]

This is great that we are now beginning to be able to start defining the basic "arithmetic" of sheaves, e.g. pushing forward and pulling back. One goal would be to prove that these are adjoint functors (although strictly speaking this is a construction, not a proof).

For me a good next challenge might be to start thinking about sheaves of $\mathcal{O}_X$-modules. The reason that this will be a challenge is that my memory was that there were several competing proposals for what the definition of a sheaf of $\mathcal{O}_X$-modules should be. Choosing a definition and then trying to define pushforward and pullback, and then proving the adjointness of the corresponding constructions, would surely be worth a paper. The category of quasicoherent $\mathcal{O}_X$-modules over a scheme is a fundamental object in algebraic geometry. Me+Amelia+Kenny+Chris+Ramon+Scott's paper on the definition of a scheme got published, and I should think that the Isabelle definition of a scheme will end up published too, but if we're in an algebraic geometry race with Isabelle (which I hope we are!) then this would be a really good marker to put down. The computer scientists might complain that it's definition, definition, definition and not theorem, theorem, theorem, but algebraic geometry is a complicated subject and we need all the definitions before we can start stating the theorems. Sheaf cohomology is another definition which we will need before too long, but there have been a bunch of breakthroughs in homological algebra recently as part of LTE and so it's only a matter of time. Once we have that, then we can start stating a whole bunch of theorems, and attempting to prove them will inform our API.

[Junyan Xu]

Here it says map_comp_obj is "not quite rfl, since we don't have eta for records", but currently it can actually be proven by rfl. Is this due to some change in the kernel? map_id_obj indeed isn't rfl but almost is, as it can be proven with let ⟨_,_⟩ := U in rfl. Moreover, le_map_top can be proven simply by le_top U, and similarly the definition of the global section functor in presheafed_space.lean can omit the composition with le_top.
I'm going through these files (and presheaf.lean) to simplify many other such cases and make some additions, and I think it's a good idea to ask here to ensure that such simplifications aren't discouraged for some reason.

[Scott Morrison]

I don't think let ⟨_,_⟩ := U in rfl is substantially different than the existing proof of map_id_obj.

[Scott Morrison]

For map_comp_obj, yes, this seems to be a mistake. There's enough code using this stuff downstream that you can safely just try out the change. If nothing breaks downstream then it's fine. If something does break downstream you can improve the comment to explain what's really going on!

[Scott Morrison]

Removing the composition with le_top in the global section functor (I haven't actually looked at this recently, so take this with a grain of salt) sounds like a bad idea, however. It may be forcing Lean to do more definitional unfolding, so if it is there is may well be there to improve a performance issue. (Ideally there would be a comment explaining this if that is the case, but ....)

[Junyan Xu]

Interesting that there are such tricks that make definitions more complicated to improve performance. However it's making one of my proofs more complicated and forced me to prove a lemma stating Gamma.map f.op = f.1.c.app (op T)for a morphism f of LocallyRingedSpace while it should really be rfl. Maybe I could also submit a PR and compare the compile time?

By the way, a consequence of map_comp_obj's rfl is that the equality version of map_compis also rfl.

[Scott Morrison]

Usually you don't even need to compare overall compile times (which are noisy and hard to compare anyway). Usually a problem like this exhibits itself as a deterministic timeout, so as long as you can lean --make -T100000 src successfully you probably haven't broken anything.

[Scott Morrison]

I wrote a fair bit of this stuff, but it was a long time ago, and I remember struggling in places. I wouldn't be at all surprised if there are just mistakes.

[Junyan Xu]

Thanks this is the first time I see the compile command. I'm recently getting (100 seconds?) deterministic timeouts in my working Spec-Gamma adjunction file in VSCode and had to increase the time limit (it's in the VSCode Lean setting), but hopefully it goes away when more lemmas are placed into appropriate files.

So you think these are not due to changes in how the kernel checks defeq, and you just didn't try? In the same file, map_comp_obj_unop and op_map_comp_obj are also rfls, but not op_map_id_obj, not even let ⟨_,_⟩ := U.unop in rfl ...

[Junyan Xu]

Scott Morrison said:

I don't think let ⟨_,_⟩ := U in rfl is substantially different than the existing proof of map_id_obj.

Yes it's probably equivalent but would such term mode proof be faster in general?

[Scott Morrison]

No, I wouldn't expect it to be faster.

[Scott Morrison]

Please don't change the time limit in the VSCode extension.

[Scott Morrison]

Commit to mathlib are all compiled with that time limit in place, and you are only going to cause yourself pain to develop code with the limit raised, only to have to get it back down afterwards.

[Scott Morrison]

I'm pretty certain no kernel change could affect anything like this. It may be that some earlier definition has changed, or just I made a mistake at the time.

[Scott Morrison]

If anything you should _lower_ the time limit, to be sure that you're contributing code that still has some margin. :-)

[Kevin Buzzard]

Something which Scott doesn't seem to say but which is something I learnt from him in the past is that "trying to make the proof rfl" is something which is a great idea for simple objects but which can become an actively bad idea as your objects become more complicated. Rewriting a non-rfl proof can sometimes be much quicker than rfl once terms start getting big. My (perhaps ignorant) impression of people who work with different provers or on different kinds of questions can somehow become obsessed with making things refl perhaps because they're computer scientists so feel that everything should compute. In maths it doesn't work like that. I'd far rather have a quick rw proof than a slow refl proof because beyond some point in mathematics refl doesn't actually buy you anything.

[Scott Morrison]

Exactly. Expecting rfl proofs at some point just becomes a trap: Lean can unexpectedly go off and do very inefficient proofs by definitional unfolding. Often it's better to intentionally make definitions irreducible, or wrapped in structures, precisely so Lean can't see through them!

[Junyan Xu]

I've finished the aforementioned planned changes to presheafed_space.lean
and associated files, but Spec.lean and has_colimits.lean have some broken proofs not yet fixed, so I haven't compiled mathlib with the time limit yet. Nonetheless, here is a preview commit containing the main changes. You can see my philosophy is to prove and make use of equalities (to "collapse tower of isomorphisms") and take advantage of defeqs (which may or may not be bad, as discussed above) whenever possible, and use eq_to_hom if involved types are not defeq. As you can see the changes already resulted in a lot of simplified proofs (though I have no idea about the compile time yet), but I only made minimum changes in other files, and those proofs likely can be further optimized under the new definitions. Let me know if this seems like the right approach to you.

[Scott Morrison]

I think I'd like to see no sorries and no timeouts before having any opinion. :-)

[Scott Morrison]

(As I said before, developing with the timelimit turned off is counterproductive.)

[Junyan Xu]

I developed this on another machine where time limit wasn't turned off. I didn't get any deterministic timeouts in the files I checked, but this computer is faster (MacBook Pro 2019, 2.3GHz 8-Core Intel i9, 32 GB memory).

[Junyan Xu]

I fixed all proofs and compilation using the command you gave me finished in several minutes, so I opened PR #9972. I didn't merge latest mathlib before compiling though. Lean spat out about 20 lines of output and they are truncated to the window width so I can't see the full messages and am not sure if the compilation has been successful. Let's wait for the automated mathlib build with the PR.

[Junyan Xu]

continuous integration / Build mathlib (push) Successful in 9m

[Scott Morrison]

Looks great!!

[Scott Morrison]

Apologies if I was skeptical earlier. This is a big improvement.

[Anthony Bordg]

Kevin Buzzard said:

Me+Amelia+Kenny+Chris+Ramon+Scott's paper on the definition of a scheme got published, and I should think that the Isabelle definition of a scheme will end up published too,

@Kevin Buzzard
Hopefully, this is currently in the hands of referees.

[Anthony Bordg]

For the record, our paper Simple Type Theory is not too Simple: Grothendieck's Schemes Without Dependent Types has been published in the journal Experimental Mathematics and is open access online.