Zulip Chat Archive

Stream: maths

Topic: Ext and Tor


Kevin Buzzard (Jul 13 2021 at 20:29):

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 (Jul 13 2021 at 20:42):

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 (Jul 13 2021 at 20:50):

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

Kevin Buzzard (Jul 13 2021 at 21:33):

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 (Jul 13 2021 at 21:34):

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 (Jul 13 2021 at 21:37):

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 (Jul 13 2021 at 22:08):

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 (Jul 13 2021 at 22:09):

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 (Jul 13 2021 at 22:09):

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

Adam Topaz (Jul 13 2021 at 22:09):

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

Adam Topaz (Jul 13 2021 at 22:11):

docs#Module.Module_enough_projectives

Adam Topaz (Jul 13 2021 at 22:14):

And docs#Module.category_theory.abelian

Adam Topaz (Jul 13 2021 at 22:14):

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 (Jul 13 2021 at 22:15):

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

Kevin Buzzard (Jul 13 2021 at 22:16):

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 (Jul 13 2021 at 22:18):

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

Heather Macbeth (Jul 13 2021 at 22:19):

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 (Jul 13 2021 at 22:20):

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

Heather Macbeth (Jul 13 2021 at 22:21):

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

Kevin Buzzard (Jul 13 2021 at 22:21):

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 (Jul 13 2021 at 22:23):

But that means that it is within reach to have a definition of the cohomology of Rn\mathbb{R}^n or SnS^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 (Jul 13 2021 at 22:24):

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

Kevin Buzzard (Jul 13 2021 at 22:25):

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

Kevin Buzzard (Jul 13 2021 at 22:25):

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 (Jul 13 2021 at 22:26):

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 (Jul 13 2021 at 22:27):

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

Kevin Buzzard (Jul 13 2021 at 22:29):

The road is still long :-)

Adam Topaz (Jul 13 2021 at 22:30):

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 (Jul 13 2021 at 22:31):

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

Adam Topaz (Jul 13 2021 at 22:31):

No

Kevin Buzzard (Jul 13 2021 at 22:32):

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

Reid Barton (Jul 13 2021 at 22:32):

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 (Jul 13 2021 at 22:32):

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 (Jul 13 2021 at 22:34):

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

Adam Topaz (Jul 13 2021 at 22:34):

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

Heather Macbeth (Jul 13 2021 at 22:35):

OK, that's great!

Reid Barton (Jul 13 2021 at 22:36):

#144

Heather Macbeth (Jul 13 2021 at 22:55):

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

Kevin Buzzard (Jul 13 2021 at 22:58):

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 (Jul 13 2021 at 23:00):

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 (Jul 14 2021 at 00:05):

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

Adam Topaz (Jul 14 2021 at 02:36):

#8305 <-- this gives items 2 and 3

Adam Topaz (Jul 14 2021 at 12:29):

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

Adam Topaz (Jul 14 2021 at 12:29):

(both come for free using restricted Yoneda)

Johan Commelin (Jul 14 2021 at 12:34):

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

Adam Topaz (Jul 14 2021 at 12:35):

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

Adam Topaz (Jul 14 2021 at 12:35):

But I think this will be challenging

Reid Barton (Jul 14 2021 at 12:36):

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

Johan Commelin (Jul 14 2021 at 12:39):

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

Johan Commelin (Jul 14 2021 at 12:39):

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 (Jul 14 2021 at 12:43):

Nevermind, it was easy using more general yoneda nonsense.

Adam Topaz (Jul 14 2021 at 12:44):

Pushed as sSet.to_Top_simplex

Adam Topaz (Jul 14 2021 at 13:25):

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 (Jul 15 2021 at 00:08):

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 (Jul 15 2021 at 00:09):

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 (Jul 15 2021 at 00:48):

@Adam Topaz This is great!

Heather Macbeth (Jul 15 2021 at 00:49):

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

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

Adam Topaz (Jul 15 2021 at 00:58):

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 (Jul 15 2021 at 01:33):

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 (Jul 15 2021 at 01:49):

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 (Jul 15 2021 at 07:45):

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

Kevin Buzzard (Jul 15 2021 at 07:47):

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

Patrick Massot (Jul 15 2021 at 07:54):

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 (Jul 15 2021 at 12:35):

@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 (May 18 2023 at 10:32):

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 (May 18 2023 at 10:55):

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

Oliver Nash (May 18 2023 at 11:00):

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

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 (May 18 2023 at 13:04):

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 (May 18 2023 at 13:14):

Does this mean Canada is cancelled?

Kevin Buzzard (May 18 2023 at 13:14):

I guess there are other cohomology theories...

Kevin Buzzard (May 18 2023 at 13:14):

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

Kevin Buzzard (May 18 2023 at 13:15):

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

Patrick Massot (May 18 2023 at 13:16):

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 (May 18 2023 at 13:22):

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

Kevin Buzzard (May 18 2023 at 13:25):

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 (May 18 2023 at 15:17):

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 (May 18 2023 at 15:54):

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

Matthew Ballard (May 18 2023 at 16:59):

Adam Topaz said:

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

For reference

Oliver Nash (May 18 2023 at 18:07):

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 (May 18 2023 at 18:09):

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 (May 18 2023 at 18:10):

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

Matthew Ballard (May 18 2023 at 18:33):

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

Scott Morrison (May 19 2023 at 15:15):

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

Adam Topaz (May 19 2023 at 16:46):

delegated!


Last updated: Dec 20 2023 at 11:08 UTC