Ext and Tor

Stream: maths

[Kevin Buzzard]

Thanks to Scott's efforts, backed up by the LTE project and Adam and Johan, we now have Ext and Tor, which means that homological algebra in Lean is looking like a real possibility. However am I right in thinking that we still don't have the construction of a long exact sequence of cohomology from a short exact sequence of complexes? How far are we from this? Is the issue that we can't face proving things like the snake lemma for a general abelian category?

[Adam Topaz]

I think a more pressing issue is developing more of the API for Ext. The fact that it's contravariant in the first variable makes the definition pretty annoying.

I started toward this by adding some isomorphisms between things like kernel f and cokernel f.op in category_theory/abelian/opposite, but there are more similarly silly things to add

[Adam Topaz]

For the long exact sequence, it seems we should seriously think about formalizing (universal) delta functors

[Kevin Buzzard]

The thing about short exact sequence of complexes gives long exact sequence of cohomology seems to me to be far more trivial than universal delta functors

[Kevin Buzzard]

By the way, can we now define something like singular cohomology as a derived functor? If we define an etale morphism of rings can we define etale cohomology of schemes? How big is the gap?

[Adam Topaz]

We don't have injective resolutions yet, unfortunately, and to compute sheaf-like cohomology theories we probably want to take an injective resolution of the sheaf

[Kevin Buzzard]

Aah -- both Ext and Tor can be computed using projective resolutions? Wait -- I'm now confused. We have injective resolutions in general in the sense that we can just take projective resolutions in the opposite category. Oh -- I'm unconfused .The point must be that we can't show that the specific sheaf categories have enough injectives.

[Kevin Buzzard]

I see -- so just because we have Ext and Tor in some huge generality doesn't actually imply that we have Ext and Tor for the category of R-modules!

[Adam Topaz]

I think we know that R-mod has enough projectives.

[Adam Topaz]

Well, at least it should be easy enough to show :)

[Adam Topaz]

docs#Module.Module_enough_projectives

[Adam Topaz]

And docs#Module.category_theory.abelian

[Adam Topaz]

So these are the two instances we need to be able to compute Ext and Tor as they're currently defined (for modules)

[Kevin Buzzard]

I see. And for sheaves the analogous instances are still missing (and would make a nice project, probably!)

[Kevin Buzzard]

Furthermore we'll need enough injectives for R-Mod in order to check that the other definition of Ext coincides with the one we have.

[Heather Macbeth]

I am very interested in this conversation but need some translation ... does this mean we are within reach of sheaf cohomology?

[Heather Macbeth]

And when we get to the bare definition of sheaf cohomology, will it be usable for topological purposes (like, take the cohomology of the sheaf of locally constant functions to some coefficient ring, know some useful facts about it) or is there more work to do after that?

[Heather Macbeth]

Random example: how far away would it be to compute the cohomology of the sphere?

[Heather Macbeth]

Or even of $\mathbb{R}^n$?

[Kevin Buzzard]

Oh dear, I'm not sure we're going to be computing anything any time soon :-) Right now I am proposing an extremely long-winded way of defining cohomology groups by saying "we know what H^0 is, and now apply some derived functor magic".

[Heather Macbeth]

But that means that it is within reach to have a definition of the cohomology of $\mathbb{R}^n$ or $S^n$ (via sheaf cohomology of a sheaf of locally constant functions), it's just that we won't immediately be able to prove anything using this definition. Is that right?

[Adam Topaz]

I think we're actually closer to defining singular cohomology as bona fide singular cohomology (i.e. via the simplicial construction)

[Kevin Buzzard]

One thing which I think might be super-hard with this approach is changing X. It's all focussed on changing F.

[Kevin Buzzard]

Right. The machine should spit out a bunch of groups H^i(X,F) and also a construction of a long exact sequence of cohomology associated to a short exact sequence of sheaves, and if we're lucky then later on it might also spit out a theorem of the form "if you can come up with some other construction of H^n which agrees with the derived nonsense on H^0 and also has some nice long exact sequence properties then it will be isomorphic to the derived nonsense"

[Kevin Buzzard]

Right -- I have a branch which defines group cohomology as cocycles over coboundaries, and one could certainly imagine computing e.g. H^1(S_3,Z/2Z) this way. But I've never PR'ed it because Scott suggested that I related it to the abstract nonsense stuff, which needs a bunch of machinery which we didn't seem to have.

[Adam Topaz]

FWIW right now I'm having issues even convincing lean that Module A has enough projectives (because of universes :sad: )

[Kevin Buzzard]

The road is still long :-)

[Adam Topaz]

Ok, at least lean understands that I'm allowed to (noncomputably) compute Ext M N:

import category_theory.abelian.ext
import algebra.category.Module.projective
import algebra.category.Module.abelian

universe u

variables {A : Type u} [comm_ring A] (M N : Module.{u} A)

set_option pp.universes true

instance : category_theory.enough_projectives (Module.{u} A) :=
Module.Module_enough_projectives.{u}

noncomputable
example {n} : Module.{u} A := ((Ext A (Module.{u} A) n).obj (opposite.op M)).obj N

[Kevin Buzzard]

Can you prove that Ext^0 is isomorphic to Hom?

[Adam Topaz]

No

[Kevin Buzzard]

OK so in summary, there's still a bit of work to do :-)

[Reid Barton]

What's max of u and u and u and u and u and u and u and u and u and u?

[Heather Macbeth]

Adam Topaz said:

I think we're actually closer to defining singular cohomology as bona fide singular cohomology (i.e. via the simplicial construction)

I haven't really followed this, can you catch me up? Has the theory developed in algebraic_topology.simplicial_set been related to topological spaces yet?

[Adam Topaz]

@Heather Macbeth not yet, but it's very doable.

[Adam Topaz]

I think Johan had some code in this direction in his old simplicial set branch?

[Heather Macbeth]

OK, that's great!

[Reid Barton]

#144

[Heather Macbeth]

So, how far is mathlib along this roadmap laid out by Reid in 2018? :(

[Kevin Buzzard]

Well, the module refactor got done :-) And we have at least 1, 4, and the beginning of 6, and probably some more. Maybe it's time for Patrick's big push?

[Adam Topaz]

5 is also done and the second half of 6 is done in LTE in essentially sufficient generality, so it shouldn't be too hard to port to mathlib. Seems to me that item 2 is the main thing we're missing

[Bhavik Mehta]

We also have the restricted yoneda embedding and its adjoint, so I think 2 is the only missing bit

[Adam Topaz]

#8305 <-- this gives items 2 and 3

[Adam Topaz]

I updated #8305 with the geometric realization and the associated adjunction.

[Adam Topaz]

(both come for free using restricted Yoneda)

[Johan Commelin]

How hard is it to show that the geometric realization of common objects is what we think it is?

[Adam Topaz]

It's defined as some giant colimit. We should at least show that the representable simplicial sets go where we expect.

[Adam Topaz]

But I think this will be challenging

[Reid Barton]

You should follow https://kerodon.net/tag/001X (starting with the definition there)

[Johan Commelin]

Yeah, I'm afraid that it will be quite a long journey.

[Johan Commelin]

I have done part of this on branch#sset, but I didn't yet show that the adjunction gives an is_geometric_realization.

[Adam Topaz]

Nevermind, it was easy using more general yoneda nonsense.

[Adam Topaz]

Pushed as sSet.to_Top_simplex

[Adam Topaz]

And since we know that geometric realization is a left adjoint, hence preserves colimits, it should be reasonable to compute the geometric realization of any simplicial set which you write down as a colimit of representables.

[Adam Topaz]

In case anyone is curious, here's a construction of integral singular homology of a topological space:

import algebraic_topology.Moore_complex
import algebraic_topology.simplicial_set
import algebra.category.Module.abelian
import algebra.homology.homology

variables (X : Top.{0})

open category_theory algebraic_topology

noncomputable
def singular_homology (n : ℕ) : Module ℤ :=
let sing := Top.to_sSet.obj X,
    Zsing := ((simplicial_object.whiskering _ _).obj (Module.free ℤ)).obj sing in
(normalized_Moore_complex.obj Zsing).homology n

I realized there are some universe restrictions on Top.to_sSet which I'll try to fix at some point, so for now this only works for X : Top.{0}.

[Adam Topaz]

Also, this uses the normalized Moore complex, which we have in mathlib, but if I recall correctly this is homotopy equivalent to the alternating face map complex, so should yield the same homology.

[Heather Macbeth]

@Adam Topaz This is great!

[Heather Macbeth]

What would need to be done to be able to prove something like

example : singular_homology (Top.of punit) 3 = 0 := sorry

[Adam Topaz]

Good question! We could probably come up with an ad-hoc proof of this, but it would be better to develop more of the homotopy theory of the situation, so that we can compute the singular homology of the geometric realization of a simplicial set without first passing to Top. In this case, Top.of punit is the geometric realization of the simplicial 0-simplex, whose homology should be easy to calculate.

[Heather Macbeth]

Does that mean, you're saying that it should be easier to compute, for sing : sSet.{0}, the quantity

let Zsing := ((simplicial_object.whiskering _ _).obj (Module.free ℤ)).obj sing in
(normalized_Moore_complex.obj Zsing).homology n

than to add the extra layer of letting sing := Top.to_sSet.obj X in the above definition?

[Adam Topaz]

Well, what I mean is that when X is isomorphic to sSet.to_Top.obj Y for some explicit Y, then we should prove that singular_homology X is isomorphic to the homology of normalized_Moore_complex.obj $ ((simplicial_object.whiskering _ _).obj (Module.free ℤ)).obj Y.

In the case of X = Top.of punit, we have X isomorphic to sSet.to_Top.obj (sSet.standard_simplex.obj [0]).

[Scott Morrison]

I'm so pleased it's possible to define singular_homology out of already available general machinery. :-)

[Kevin Buzzard]

But how hard is it to prove that it's isomorphic to some derived functor definition?

[Patrick Massot]

Is this definition functorial? I mean, do we get for each n a functor from Top to Module ℤ? Then the next step is of course to compute the homology of spheres (without cheating, starting with the sphere defined using Euclidean geometry, not as an abstract simplicial set).

[Adam Topaz]

@Patrick Massot yes, it's completely functorial, although I didn't formulate it in this way (but as you can see in the code I just applied a bunch of functors, except for the last homology step, for which we can use the functorial version docs#homology_functor instead).

[Oliver Nash]

Adam Topaz said:

In case anyone is curious, here's a construction of integral singular homology of a topological space:

I had forgotten about this and I see we can now even do this:

import algebraic_topology.alternating_face_map_complex
import algebraic_topology.simplicial_set
import algebra.category.Module.abelian
import algebra.category.Module.adjunctions
import algebra.homology.homology

noncomputable theory

open algebraic_topology

def singular_homology (X : Type) [topological_space X] (n : ℕ) : Module ℤ :=
((alternating_face_map_complex _).obj $ Top.to_sSet.obj (Top.of X) ⋙ Module.free ℤ).homology n

I hadn't appreciated how far we'd come till today.

[Kevin Buzzard]

How far are we from being able to do it in Lean 4?

[Oliver Nash]

Not far I think. I believe just these are required:

• https://leanprover-community.github.io/mathlib-port-status/file/algebra/category/Module/adjunctions
• https://leanprover-community.github.io/mathlib-port-status/file/algebra/category/Module/abelian

I don't have a sense for how much work that it is but it's 14 files (of which 5 are in progress).

[Adam Topaz]

Here's the functorial version :)

import algebraic_topology.alternating_face_map_complex
import algebraic_topology.simplicial_set
import algebra.category.Module.abelian
import algebra.category.Module.adjunctions
import algebra.homology.homology
open category_theory

noncomputable
def integral_singular_homology (n : ℕ) : Top.{0} ⥤ Module ℤ :=
Top.to_sSet ⋙ ((simplicial_object.whiskering _ _).obj (Module.free ℤ)) ⋙
  algebraic_topology.alternating_face_map_complex _ ⋙ homology_functor _ _ n

[Kevin Buzzard]

Does this mean Canada is cancelled?

[Kevin Buzzard]

I guess there are other cohomology theories...

[Kevin Buzzard]

Now can you prove H^37(point)=0?

[Kevin Buzzard]

Even better, can you do H^{37](empty set)?

[Patrick Massot]

Indeed we certainly can't claim to have singular homology if we cannot prove anything with it. Proving Brouwer's fiexed point theorem or invariance of domain with this definition would be convincing for instance.

[Adam Topaz]

I think that’s essentially the definition that @Brendan Seamas Murphy used in his project

[Kevin Buzzard]

With group cohomology I think the conclusion we came to was that you have to either make lots of definitions and prove they're all the same, or make one definition and enough API for it so that it looks like it's lots of definitions (e.g. even if you don't define it as cocycles over coboundaries you'll still need a map from cocycles to it and a proof that it's surjective and the kernel is the coboundaries)

[Scott Morrison]

In terms of making this happen in Lean 4 faster, #19034 does a split that should help by a few days (i.e. conceivably ready for Banff).

[Scott Morrison]

#19035 does another split. With these two we should be able to port algebra.category.Module.adjunctions almost immediately.

[Matthew Ballard]

Adam Topaz said:

I think that’s essentially the definition that Brendan Seamas Murphy used in his project

For reference

[Oliver Nash]

Matthew Ballard said:

For reference

I didn’t know about this. Is it sorry-free? (On phone it would check myself.) Is there a reason why it’s not marked here: https://leanprover-community.github.io/100-missing.html ?

[Matthew Ballard]

I am pretty sure it is sorry-free. I would check for myself but my Lean 3 machine is not taking my calls right now.

I remember there being an effort to get it up there. I am surprised it isn't.

[Matthew Ballard]

#maths > Completed proof of the Brouwer Fixed Point Theorem is the relevant thread here

[Matthew Ballard]

Ha. You confused me with that link to the missing ones: it is here https://leanprover-community.github.io/100.html

[Scott Morrison]

!4#4115 is on the increasingly short path to @Adam Topaz's example above, and ready for review.

[Adam Topaz]

delegated!