long exact sequences

Stream: maths

[Kevin Buzzard]

So I've been thinking about how to state the following fundamental theorem: if we have a short exact sequence of complexes of objects in an abelian category (say), then we get an associated long exact sequence of cohomology groups.

I spent a while yesterday playing with Johan's differential_object I V category. Here V is an abelian category (or in practice something a bit weaker) and I is an index set. The objects in this differential object category are just I-indexed families of elements of V (i.e. a function I -> V) equipped with maps d i j : V i -> V j for all i and j. I want to add the further axiom that d^2=0 whenever it makes sense. I am even tempted by the idea of having some abstract morphism type M like I, equipped with two maps s : M -> I and t : M -> Iand then you get d (s m) (t m) : V (s m) -> V (t m). In the traditional example I = M = integers, and s(m)=m and t(m) is either m+1 or m-1 depending on whether you're doing homology or cohomology. But I want to keep the axiom "d^2=0 whenever it makes sense" (I don't want to use this model for double complexes, double complexes should have two d's I think).

If subobjects in V form a complete lattice (eg Ab, R-mod...), then one can take the cohomology of one of these crazy complexes A to get an I-indexed family H: you look at all the maps with target A and take the join of their images; this is a subobject of the meet of all the kernels of maps out of I, so you can take the quotient. Note that this quotient object H i doesn't have a d any more, it's not an object of the category, it's just an I-indexed family of objects in V. So what can we do with it?

A morphism A -> B in this category is one which commutes with all the d's in M. This H construction is functorial with respect to these morphism in the sense that for all i we get an induced H i A -> H i B.

A short exact sequence 0 -> A -> B -> C -> 0 in the complex category is a collection of short exact sequences indexed by I and commuting with all the d's in M. You can think about it as a family of injections A i -> B i and a family of surjections B i -> C i and images equals kernels. I am guessing that the H-construction is "exact in the middle" (even in this generality, but I might be wrong). It is certainly true if the maps s and t are injective -- this is what the traditional proof boils down to : the join of the images is just one image and the meet of the kernels is just one kernel.

Finally, it seems to me that if 0 -> A -> B -> C -> 0 is short exact in this complex category, then for any m : i -> j you get a map from Delta_m : H i C to H j A. I didn't check this. Again if S and T are injective, H i B -> H i C -> H j A -> H j B is exact, and I don't know if this is true in general.

Thought of in this way, the long exact sequence is in some sense a red herring. It just becomes a combination of these two other theorems.

[Kevin Buzzard]

So one could argue that the long exact sequence of cohomology associated to a short exact sequence of complexes was really a construction and three theorems, and one does not have to even worry about how to talk about a long exact sequence of cohomology groups. I mean, when do we really use this long exact sequence? We just say things like "oh and H^2(A)=0 by a theorem of Grothendieck so this map on H^1's is surjective". It's not like we take the long exact sequence itself and then tensor it with something to make a complex and then do cohomology again. For example last week I thought "I need the long exact sequence for Tor to prove this theorem about flatness" but actually I just need some very specific assertion of the form "Tor_1(B)->Tor_1(C)->Tor_0(A)->Tor_0(B) is exact".

So here's what things look like abstractly. Say h,i,j are three indices in I and say h R i and i R j are true, so there are d maps A_h -> A_i and A_i -> A_j with d^2=0 if A is any complex. If we have a triple (h,i,j) like this, we can form H^i(A), meaning ker (A_i -> A_j) / range (A_h -> A_i). It depends on the triple.

Definition 1) If A -> B is a morphism of complexes, and (h,i,j) is a triple as above, then there's an associated morphism of cohomology groups H^i(A) -> H^i(B).

Theorem 2) If 0 -> A -> B -> C is exact then H^i(A) -> H^i(B) -> H^i(C) is exact.

Definition 3) If 0 -> A -> B -> C -> 0 is exact and we throw in another index k with j -> k, so we now have two triples (h,i,j) and (i,j,k), then there's an associated map delta_{i,j} : H^i(C) -> H^j(A).

Theorem 4: with (h,i,j,k) as above, H^i(B)->H^i(C)--(delta)-->H^j(A)->H^j(B) is exact.

Those are the only theorems you ever need when you're actually using the long exact sequence in practice. Theorem 2 gives you what we call "exactness at H^i(B)" and theorem 4 gives you "exactness at H^j(A) and H^i(C)". You can now package this data up any way you like (e.g. fin 3 x Z or N or whatever) but these theorems are the interface that we want I think.

There is a variant when you let e.g. h vary so you're considering lots of maps d : A_h -> A_i, and it all works the same, you just replace all the A_h with their direct sum. Similarly letting j vary just replaces things with their direct product.

An issue I can see looming: how are we actually going to define these cohomology groups in the lawless complex situation? It's all very well having d's everywhere, but are we really going to take the meet of the kernels and quotient out by the join of the images?

[Johan Commelin]

Wait, where do the meets of kernels and joins of images come into play?

[Kevin Buzzard]

If you have a random complex with d's everywhere and you want to take its cohomology, you're forced to use all d's for images and kernels

[Johan Commelin]

Unless you define

def H (i j k) := ker (d j k) / im (d i j)

[Kevin Buzzard]

If you just want an answer which depends only on i. In practice we only ever use the variant where the answer depends on h, i, j with h+1=i and i+1=j but I was thinking more generally.

[Johan Commelin]

But I can see why you wouldn't want to do that

[Kevin Buzzard]

Right

[Johan Commelin]

Having three indices feels like it's not going to scale. So maybe the meets-and-joins idea works.

[Johan Commelin]

But just hard-coding i -1 and i + 1 will bring back all the DTT issues

[Kevin Buzzard]

If you define H (i) as meet of kernels over join of images then (in the succ-structure case) you will still be able to prove that for all h and j, there's a map from ker(d i j) to H i with kernel range(d h i)

[Johan Commelin]

Still, I keep having the feeling that we are battling against the system in a way that shouldn't be necessary.

[Kevin Buzzard]

This needs that arbitrary meets and joins of subobjects need to exist in your underlying abelian category too (is that one of the axioms? I never know what the axioms are)

[Kevin Buzzard]

I know that arbitrary products of objects might not exist (e.g. finite abelian groups), but this is something different.

[Johan Commelin]

Kevin Buzzard said:

This needs that arbitrary meets and joins of subobjects need to exist in your underlying abelian category too (is that one of the axioms? I never know what the axioms are)

Well, the meets and joins aren't that arbitrary, so we can certainly prove that these specific ones exist.

[Scott Morrison]

Have a look at category_theory.subobject to see what we have in mathlib already about the lattice structure on subobjects.

In particular from the module-doc:

We also provide the semilattice_inf_top (subobject X) instance when [has_pullback C],
and the semilattice_sup (subobject X) instance when [has_images C] [has_binary_coproducts C].

makes no mention of arbitrary meets and joins so far :-)

[Scott Morrison]

But presumably it is not hard.

[Scott Morrison]

I think one blocker might be that we don't have typeclasses for complete_semilattice_Inf and complete_semilattice_Sup, we just have their combination.

[Kevin Buzzard]

I wonder if this is just a red herring. The way I see it there are explicit lemmas involving only finitely many abelian groups and some compatible collection of indices. The idea about taking sups and infs was a way to work around this index issue -- so one could talk about the cohomology in degree n without hard wiring the numbers n-1 and n+1 into the system. But I think another way is just to use pred_succ structures

[Kevin Buzzard]

Here is what I think is the main issue. I'm talking about stating and proving the assertion that in an arbitrary ab cat, or perhaps just R-modules, that a short exact sequence of complexes produces a long exact sequence of cohomology. I think the sup and inf stuff is just a red herring now. The cohomology of the complex $A_i\to A_{i+1}\to A_{i+2}$ is a kernel modulo an image, and as far as I can see this is not going to be equal to the cohomology of $A_{(i+1)-1}\to A_{i+1}\to A_{i+2}$ in the sense of Lean. If $i,j,k$ are consecutive indexes then it looks like one might have to carry around both $i$ and $k$ when talking about $H^j$. Example: a short exact sequence $0\to A\to B\to C\to 0$ gives $H^{i,j,k}(A)\to H^{i,j,k}(B)\to H^{i,j,k}(C)$ and if you have another consecutive index l after that then you get maps $H^{i,j,k}(C)\to H^{j,k,l}(A)$.

[Kevin Buzzard]

And the theorem is that $H^{i,j,k}(B)\to H^{i,j,k}(C)\to H^{j,k,l}(A)\to H^{j,k,l}(B).$ And my feeling is that these results are all you actually need. Note that in particular I am not convinced that we need to make the long exact sequence as a complex.

[Kevin Buzzard]

I am however concerned that we will have more than one version of what a mathematician might call $H^i(A)$ which will depend on the explicit choice of predecessor and successor of i, with different choices related by eq to homs

[Ashwin Iyengar]

Out of curiosity, what's a situation where you'll want a general indexing set $I$ and not just $\mathbb{Z}$?

[Scott Morrison]

Lots of times nat is the natural indexing set.

[Scott Morrison]

e.g. the Moore complex

[Scott Morrison]

or de Rham cohomology, or ...

[Scott Morrison]

unfortunately also it appears that sometimes nat \cup {-1} is useful. :-)

[Adam Topaz]

@Kevin Buzzard perhaps the solution is the same solution as we have for everything else: make a characteristic predicate saying "this object is the i-th cohomology of this complex". Just like there is no "the localization" there is no "the i-th cohomology"

[Scott Morrison]

Maybe I am getting happier with this picture.

The differential_object gadget with d i j : X i \hom X j, satisfying no laws except d i j \gg d j k = 0, is really talking about an object that the simultaneously graded, and has a differential satisfying d^2 = 0 on the the direct sum of all the graded pieces, but where the differential doesn't have to respect the grading.

[Scott Morrison]

You can try to take the homology here, as ker d / im d (a subquotient of the direct sum), but there's no reason to think this will be a graded object.

[Scott Morrison]

To get that you need to know that the image of d is the same thing as the direct sum of the intersections of the image of d with each graded piece.

[Scott Morrison]

(The corresponding fact for the kernel is automatic.)

[Scott Morrison]

And d respecting the grading in pretty much any way at all ensures that.

[Scott Morrison]

Now if you know that this condition is going to hold (but haven't yet got a concrete reason, like that d i j = 0 unless j = i + 1), I think you're justified in defining i-th homology as the intersection of all the kernels d i j quotiented by the join of all the images d k i... Is that really right?

[Scott Morrison]

The subobject API that Bhavik and I wrote recently is good for doing exactly this kind of thing,

[Scott Morrison]

and I'm pretty sure that just from d_comp_d we can obtain the morphism from the join of the images to the meet of the kernels.

[Scott Morrison]

using the factor_thru API provided in category_theory.subobject.

[Scott Morrison]

I guess something we are missing, discussed a few days ago, is that category_theory.subobject only has binary meets and joins at the moment.

[Scott Morrison]

So...

1. let's write complete_semilattice_Sup and complete_semilattice_Inf, slotting them in the hierarchy
2. add those instances to subobject X given suitable hypotheses on the category,
3. see if we can define homology this way?

[Bryan Gin-ge Chen]

I haven't followed all the details of the thread, but isn't any complete_semilattice_Sup a complete_lattice: https://planetmath.org/CriteriaForAPosetToBeACompleteLattice

[Bhavik Mehta]

The hypotheses on the category should be wide pullbacks and coproducts+images for _Inf and _Sup respectively

[Scott Morrison]

But does Bryan's observation apply? If you have wide_pullbacks, you get all Infs, and then for free you get all Sups?

[Scott Morrison]

(or the other way, with coproducts and images)

[Scott Morrison]

(Hooray that wide pullbacks are already here; this isn't what they were originally intended for, right?)

[Bhavik Mehta]

It's not what I explicitly intended them for, but the proof of the special adjoint functor theorem takes an Inf of subobjects, and I think I had that in mind when making wide pullbacks as well, it might even be in the module doc

[Bhavik Mehta]

I'm pretty sure Bryan's correct, though there might be some universe subtleties - having wide pullbacks or coproducts would mean type v indexed such, and if C isn't well powered (which I think isn't a notion we have) then Sub X might not be in Type v, so getting "all Infs" could be trickier than it seems

[Bhavik Mehta]

But, I think that doing this all with the assumption of well poweredness should be safe

[Scott Morrison]

Bryan Gin-ge Chen said:

I haven't followed all the details of the thread, but isn't any complete_semilattice_Sup a complete_lattice: https://planetmath.org/CriteriaForAPosetToBeACompleteLattice

As it turned out this is in mathlib: src#complete_lattice_of_Inf.

[Scott Morrison]

Bhavik Mehta said:

The hypotheses on the category should be wide pullbacks and coproducts+images for _Inf and _Sup respectively

I tried doing this on branch#subobject_complete_lattice, but ran into universe issues immediately. I could do start setting things up for [small_category C], but it's not going to work for [large_category C]. Could you take a look at some point?

[Scott Morrison]

I feel like we have to shove mono_over A down a universe level, but I don't know how to say this.

[Scott Morrison]

Oh... this is exactly being well powered.

[Bhavik Mehta]

Now the question is how do we set up well-powered categories... My first guess was to say that for every object X, there exists a small poset which is equivalent (as a poset) to the subobjects of X, but an alternative could be to say there's a small type and a surjection from mono_over such that iso subobjects go to the same place

[Scott Morrison]

#6801 and #6802

[Scott Morrison]

They are presumably totally wrong, because I have previously avoided thinking about what "well-powered" meant. :-)

[Bhavik Mehta]

I'll take a closer look in a moment but it looks very promising!

[Scott Morrison]

@Bhavik Mehta, I've used well_powered from #6802 to build the arbitrary Inf of subobjects (given wide pullbacks), and I think I've written down the correct construction for Sup (given images and coproducts), but I can't work out how to prove Sup_le.

[Scott Morrison]

Specifically, I don't even see the paper proof. Any hints?

[Scott Morrison]

This is all on branch#subobject_complete_lattice, in src/category_theory/subobject/lattice.lean. There's one sorry for the construction of the morphism, and one sorry to check a commutative diagram (presumably easy once I know the morphism).

[Scott Morrison]

Cancel that, now I get it. :-)

[Scott Morrison]

#6809 now has a complete_lattice structure on subobject X, for any well powered category with coproducts, wide pullbacks, images, and a zero object.