Implementation of base change

Stream: mathlib4

[Tammo Brinner]

Hello!
I am a master student in mathematics and plan to write my master thesis about the implementation of a topic of my choice in lean4. I was wondering whether it would be feasible to implement a theorem like base change in lean4 (the sheaves in topology version). I have been reading up on sheaves in lean4 and i feel like it would be managable but i am also not an expert in lean4 so i was wondering if someone has an idea whether this is doable or not. Thank you in advance!

[Kenny Lau]

what is a "theorem like base change"?

[Tammo Brinner]

Kenny Lau schrieb:

what is a "theorem like base change"?

Are you asking the precise contents of this theorem?

[Henrik Böving]

Kenny Lau said:

what is a "theorem like base change"?

it could also be read as "a theorem such as base change"

[Kenny Lau]

Tammo Brinner said:

Are you asking the precise contents of this theorem?

yes

[Riccardo Brasca]

If you are thinking about stuff like $f^\ast(R^p g_\ast \mathcal{F}) \cong ...$ then this a probably a little bit difficult to formalize (we don't have spectral sequence, and this is really not something adapted for a first project), but I may be wrong.

[Tammo Brinner]

okay let me give you the precise reference. The theorem is stated as follows:

image.png

There is also a derived version of this as Riccardo pointed out, but i just want to prove this version. I asked my professor for persmission to share his script for more context. You do not need spectral sequences for this.

[Riccardo Brasca]

Do we have lower shrink?

[Tammo Brinner]

I dont think that has been implemented, but that should not be hard.

[Tammo Brinner]

Here is the Script:
SiT_holstein.pdf

[Kevin Buzzard]

Lol that theorem is impossible to formalize as it is stated, because the word "canonical" has no formal meaning. As a warm-up exercise, would you like to state what you mean by that word? Note that the answer needs to cover every single naturality statement used in the rest of the paper after that point.

[Kevin Buzzard]

In Lean the result you quote would not be a theorem, because actually the theorem ("there exists natural isomorphisms between these two functors") is far too weak for applications; it does not tell you what the map is, only that some construction gives a nat iso. In Lean, this "theorem" would be a definition consisting of the actual map (and ideally maps in both directions) plus proof that it (they) are natural isomorphism(s), and then after that there would be more theorems (doing the heavy lifting of "canonical" by saying exactly which diagrams you are claiming will commute, rather than just leaving this as an (unreasonable) exercise for the reader).

Feel free to tell this to your professor ;-)

[Kevin Buzzard]

PS I think this would be a great project; in fact it might even teach your professor what their theorem says.

[Tammo Brinner]

Hahaha okay, i mean you are right with this. Normally, mathematicians write canonical when they mean that the map is constructed in the proof and consists of a "natural choice" of a natural transformation between these functor. If you look at the script, there is a map constructed (as per usual without checking the naturality condition). So the statement in Lean would be something like this: Given a pullback square of locally compact spaces, these compositions of functors are naturally isomorphic.
Of course now one would need to construct this natural transformation and show every square involved actually commutes.

[Kevin Buzzard]

I'll say it again: I think this is a great project. My super-pedantic comments above are just basically a joke; I think there's some very interesting content here and my impression is that we have most if not all of the prerequisites, and those that we don't have also look very much like they're in scope for mathlib.

[Kevin Buzzard]

OTOH spectral sequences are probably an MSc project in themselves!

[Johan Commelin]

I think @Joël Riou has done spectral sequence. They are somewhere in his glacier of PRs, making their way towards mathlib.

[Tammo Brinner]

Thank you for your estimation Kevin!

[Tammo Brinner]

If any other Lean expert has thoughts on this, please share them:)

[Joël Riou]

The basic formalism of sheaves allows to define a base change morphism for $(f^\star,f_\star)$ (@Christian Merten and I have some draft code in the abstract context of pseudofunctors to the bicategory of adjunctions https://github.com/leanprover-community/mathlib4/blob/22d7d35bb6e82d0f454021f64fd2f7bc61db0738/Mathlib/CategoryTheory/Bicategory/Adjunction/BaseChange.lean#L233 ; see also for example #30350 which shows that defining such pseudofunctors is very much within reach).
Then, as in this context $f_!F$ is defined as a subobject of $f_\star F$, the right way to formalize the statement would be to have a definition of $f_!$, a definition of the base change isomorphism for $(f^\star,f_!)$ and a commutative diagram saying that it is induced by the base change morphism for $(f^\star,f_\star)$ (taking into account that $f^\star$ is exact).
The homological extensions of this theory are certainly possible, but a lot of prerequisites are missing in mathlib (even though part of it, like spectral sequences, are in the branch https://github.com/joelriou/mathlib4/tree/jriou_localization).

[Tammo Brinner]

Thank you for the references, i will take a look at them soon. One thing i do not understand is why everyone thinks that spectral sequences are needed here. As far as i can tell one only needs a lot of point set topology and a fair bit of category theory and sheaf theory.

[Christian Merten]

It is only for the derived version where you need to talk about the derived functor of a composition of functors. Then you need spectral sequences or the analogous derived category formulation of the same fact.

[Tammo Brinner]

Okay that makes sense. Maybe i will get to that.