long exact sequence of cohomology

Stream: maths

[Kevin Buzzard]

I need practical advice. As part of his work on group cohomology, @Shenyang Wu has three complexes of groups and a short exact sequence between those complexes, and he needs the standard result that we have an induced long exact sequence of cohomology. He is going to end up writing code which looks like the following:

import tactic


@[derive has_le]
def add_subgroup (A : Type) [add_comm_group A] := set A -- actual def suppressed

def monoid_hom.ker {A B : Type} [add_comm_group A] [add_comm_group B]
  (f : A →+ B) : add_subgroup A := sorry -- actual def suppressed

def subquotient {A : Type} [add_comm_group A] (X Y : add_subgroup A)
  : Type := sorry -- subgroup Y/X

instance {A : Type} [add_comm_group A] (X Y : add_subgroup A) :
  add_comm_group (subquotient X Y) := sorry

open function set monoid_hom

variables
  {A : ℕ → Type} [∀ n, add_comm_group (A n)] (dA : ∀ n, A n →+ A (n + 1))
  {B : ℕ → Type} [∀ n, add_comm_group (B n)] (dB : ∀ n, B n →+ B (n + 1))
  {C : ℕ → Type} [∀ n, add_comm_group (C n)] (dC : ∀ n, C n →+ C (n + 1))
  (f : ∀ n, A n →+ B n) (hf : ∀ n, (f (n + 1)).comp (dA n) = (dB n).comp (f n))
  (g : ∀ n, B n →+ C n) (hg : ∀ n, (g (n + 1)).comp (dB n) = (dC n).comp (g n))
  (exact1 : ∀ n, injective (f n))
  (exact2 : ∀ n, range (f n) = ker (g n))
  (exact3 : ∀ n, surjective (g n))

--include exact1 exact2 etc etc

@[derive add_comm_group]
def H {A : ℕ → Type} [∀ n, add_comm_group (A n)] (dA : ∀ n, A n →+ A (n + 1)) (n : ℕ) :=
  subquotient (ker (dA (n + 1))) (range (dA n))

def LES1 (n : ℕ) : H dA n →+ H dB n := sorry
def LES2 (n : ℕ) : H dB n →+ H dC n := sorry
def LES3 (n : ℕ) : H dC n →+ H dA (n + 1) := sorry

theorem exact1 (n : ℕ) : range (LES1 dA dB n) = ker (LES2 dB dC n) := sorry
theorem exact2 (n : ℕ) : range (LES2 dB dC n) = ker (LES3 dA dC n) := sorry
theorem exact3 (n : ℕ) : range (LES3 dA dC n) = ker (LES1 dA dB (n + 1)) := sorry

Indeed, once the sorries are gone, he's basically finished his project.

Now it would be nice to have such a result in mathlib but I am beginning now to think that this is the time to start using category theory. Would I be right in thinking that mathlib would not be particularly interested in a formalisation of the result as it stands above?

I guess the correct generality for this result is to use succ_strinstead of nat (any type with a successor function) and to formalise everything in the context of...what? Do we have abelian categories in mathlib? Is it even worth doing this in Ab or is even this unwise? People will want it for R-mod soon enough.

[Johan Commelin]

I'm afraid I can't give advice... I can only say that I ran into some DTT annoyances when I tried to build complexes and exact sequences in Ab.

[Kevin Buzzard]

But did you notice that I only ever added 1? My impression is that the DTT annoyances show up when a + b isn't defeq to b + a. For the result above I only need succ n so I am cautiously optimistic. Can you remember any more details about your problems? @Floris van Doorn suggested I use succ_str when we were talking about this in Bonn (because actually I want $-1$-cocycles to be 0 so I can say things about $H^0$) but my memory with the dga exercise was that we wanted much more than what I need above.

[Kevin Buzzard]

link to CDGA conversation

[Kevin Buzzard]

I think the problem there was the multiplication map $A_i\times A_j\to A_{i+j}$.

[Markus Himmel]

Regarding abelian categories: As far as I know, we are waiting for @Scott Morrison's work on enriched categories until work on abelian categories in mathlib can start. I have defined abelian categories over at https://github.com/TwoFX/lean-homological-algebra as part of my (ongoing) BSc project with @Sebastian Ullrich and have proved some results about them, but it is currently completely unpolished.

[Kevin Buzzard]

I know what an abelian category is but I do not know what an enriched category is. Why can't we just define abelian categories as some typeclass on categories? Oh -- enriched means that the hom sets have extra structure like an ab group?

[Kevin Buzzard]

oh wooah, thanks for that link, you have done a ton of stuff.

[Kevin Buzzard]

Oh I see, so this is a genuine hold-up? Are you saying that we don't have the definition of an additive category in mathlib? This sort of project would be perfect for finding out what kind of an API is needed for such definitions. Are you going to do the long exact sequence result I mention above? After I talked to Sebastian I talked to @Floris van Doorn for a while about how to do this sort of thing in Lean -- he did a bunch of homological algebra in Lean 2 for his thesis.

[Markus Himmel]

Kevin Buzzard said:

oh wooah, thanks for that link, you have done a ton of stuff.

Like I said, it really needs a ton of cleanup (which I am going to do in the coming days). The goal is to develop a tactic that can prove diagram lemmas like the five lemma or the snake lemma in abelian categories by chasing pseudoelements.

[Kevin Buzzard]

That sounds really ambitious!

[Patrick Massot]

That would be wonderful!

[Markus Himmel]

The current prototype of the tactic already works on modules. The following code successfully proves the four lemma:

lemma four (hα : range α = ⊤) (hβ : ker β = ⊥) (hδ : ker δ = ⊥) : ker γ = ⊥ :=
ker_eq_bot'.2 $ λ c hc, by chase c [hc] using [g, β, f', α] with b b' a' a only f a = b

[Markus Himmel]

(After many lines of declaring variables)

[Patrick Massot]

But the killer test would be to try bring it down from the category_theory folder to some concrete stuff (for instance group cohomology or singular cohomology).

[Patrick Massot]

The example you pasted above seems to be already concrete. Is it linked in any way with the abstract non-sense?

[Markus Himmel]

Patrick Massot said:

The example you pasted above seems to be already concrete. Is it linked in any way with the abstract non-sense?

Not yet. This is the prototype of the diagram chasing strategy that only works for modules. I am going to port it to abelian categories in the next few days. I do have a (manual) proof of the four lemma in abelian categories (see abfour.lean) and I do have a (very very very messy) proof that the the category Module R is abelian (see the bottom of modules.lean).

[Mario Carneiro]

what does the chase tactic do exactly?

[Markus Himmel]

Kevin Buzzard said:

Oh I see, so this is a genuine hold-up? Are you saying that we don't have the definition of an additive category in mathlib? This sort of project would be perfect for finding out what kind of an API is needed for such definitions. Are you going to do the long exact sequence result I mention above?

That is right, there are no additive categories in mathlib, but @Scott Morrison is working on enriched categories which have additive categories as a special case (I think): see the enriched branch. My project will not contain any cohomology (it's only about defining abelian categories and (automatically) chasing pseudoelements).

[Markus Himmel]

Mario Carneiro said:

what does the chase tactic do exactly?

It chases an element along a given list of morphisms by appropriately using surjectivity and exactness assumptions. When it needs to find a preimage of some element b under a map f and it finds some assumption of the form range f = ker g, it will try to prove g b = 0 automatically. It does this by generating a ton of hypothesis about all elements it comes across and doing a depth-first search over those hypotheses while taking injective maps into account. It is very specific to diagram lemmas like the five lemma and not smart at all, but tries to exploit the fact that in the proofs of these lemmas, "there is really only one thing to do at every point" (at least that is what mathematicians claim).

[Johan Commelin]

The first thing I did when I started using Lean was prove the 5 lemma. I think it was an excellent exercise for beginners (-;

[Mario Carneiro]

isn't there a small finite number of diagram lemmas though?

[Mario Carneiro]

seems like it would be easier to just prove them all

[Markus Himmel]

Mario Carneiro said:

seems like it would be easier to just prove them all

Probably. I'm not saying that this is how diagram lemmas should be proven once they appear in mathlib. I just thought it would be fun to write a tactic.

[Mario Carneiro]

I will be curious to see what the pseudoelement version of this tactic looks like

[Markus Himmel]

As long as the proof for modules doesn't need subtraction, it won't look much different, except that instead of ker_eq_bot it will use mono_iff_injective_on_pseudoelements etc. (This is why pseudoelements are so useful). When there is subtraction involved, things get a little tricky (but the module prototype doesn't do subtraction either). Pseudoelements don't form an abelian group, but there's a construction that is like subtracting pseudoelements in some ways. I am currently not sure whether this is strong enough to prove the epi version of the four lemma in abelian categories. The usual way to prove the epi version is "by duality, the epi version follows from the mono version", but as far as I can tell, arguing using duality isn't really supported in the Lean category theory library at the moment.

[Kevin Buzzard]

It's to_additive all over again, but this time with the added complication that arrow composition gets reversed

[Mario Carneiro]

What's the problem with applying the category theorem to opposite A and then rewriting everything away?

[Markus Himmel]

Mario Carneiro said:

What's the problem with applying the category theorem to opposite A and then rewriting everything away?

I tried this, but I only got as far as showing that opposite A is a preadditive category if A is until I came to the conclusion that this is impratical. The proof was on the order of 70 lines.

[Johan Commelin]

That we don't have all those rewrite lemmas at the moment

[Mario Carneiro]

If so that's a pretty significant hole in the category theory library. I definitely expect there to be a theorem that a mono in opposite A is an epi in A, a product in opposite A is a coproduct in A, and so on. Not having that is like not having the theorem -(a + b) = -a + -b

[Scott Morrison]

Yes, there is a gaping hole regarding duality. :-(

[Reid Barton]

The hole might be larger than what is there

[Kevin Buzzard]

@Scott Morrison this enriched branch is getting pretty big and clearly a bunch of it works but there are also some sorrys. Can I help? Is there any way part of it can be PR'ed, to get the ball rolling? I would like abelian categories for several distinct reasons.

[Scott Morrison]

A lot of it is irrelevant: it was me trying to be fancy and do categories enriched in something general, rather than the useful situation of categories enriched in a concrete category.

[Scott Morrison]

Let me slice it up asap.

[Scott Morrison]

I would really like to have the fact that the forgetful functor from (Module R) to AddCommGroup is lax monoidal. This is only just now possible to do, and is meant to happen in src/category_theory/enriched/examples.lean.

[Scott Morrison]

If you wanted to have a look, the sorries in that file are the next thing to work on, in order to be able to test my enriched categories design.

[Kevin Buzzard]

"Enriched" means what? The hom sets are objects of some other category? And then some compatibility with compostion?

[Kevin Buzzard]

Oh I guess I can just read the code and see what it means :-)

[Kevin Buzzard]

I had masses of plans for the easter break and they have all fallen through! I need things to do :-)

[Scott Morrison]

Yes, that's exactly what enriched means.

[Scott Morrison]

(Enriched potentially means that you don't have have hom _sets_, just an object in some other category whose objects doesn't necessarily have underlying sets. That's _not_ what we're going to do today, and I just deleted all the work on that from enriched, and moved it to a separate branch enriched_abstract.)

[Scott Morrison]

The key example to think about is of course being enriched in Ab.

[Scott Morrison]

The first key definition is a concrete_monoidal_category, which is a monoidal category, which is concrete (i.e. has a faithful functor to Type), and the forgetful functor is _lax_ monoidal.

[Scott Morrison]

Lax monoidal means you don't have to take tensor products to tensor products, but you do have to have a map from $F(X) \otimes F(Y) \to F (X \otimes Y)$.

[Scott Morrison]

Let's check what that is for Ab: $F(X)$ is just the underlying type, and the "laxerator" is just the map building a pure tensor: $(x,y) \mapsto x \otimes y$.

[Scott Morrison]

Next we're going to define what it means for a category to be "enriched over V", where V is one of these concrete_monoidal_categorys.

[Scott Morrison]

So we have:

variables (V : Type (v+1)) [𝒱 : concrete_monoidal_category.{v} V]
variables (C : Type u) [𝒞 : category.{v} C]
include 𝒱 𝒞

class enriched_over :=
(e_hom   : C → C → V)
(notation X ` ⟶[V] ` Y:10 := e_hom X Y)
(e_id    : Π X : C, 𝟙_ V ⟶ (X ⟶[V] X))
(notation ` 𝟙[V] ` := e_id)
(e_comp  : Π X Y Z : C, (X ⟶[V] Y) ⊗ (Y ⟶[V] Z) ⟶ (X ⟶[V] Z))
(e_hom_forget : Π X Y : C, (forget V).obj (X ⟶[V] Y) ≃ (X ⟶ Y))
(e_id_forget  : Π X : C, e_hom_forget X X (as_term (𝟙[V] X)) = 𝟙 X . obviously)
(e_comp_forget : Π (X Y Z : C) (f : (forget V).obj (X ⟶[V] Y)) (g : (forget V).obj (Y ⟶[V] Z)),
  e_hom_forget X Y f ≫ e_hom_forget Y Z g = e_hom_forget X Z ((forget V).map (e_comp X Y Z) (forget.μ f g)) . obviously)

[Scott Morrison]

This says...

[Scott Morrison]

e_hom gives us an object in V for each pair of objects in C, and we introduce notation X ⟶[V] Y for this.

[Scott Morrison]

(that is, X ⟶ Y will continue to mean the plain type of morphisms, while X ⟶[V] Y will be the bundled abelian group, or whatever)

[Kevin Buzzard]

I'm staring at the definition of monoidal category right now and realising how subtle it all is. I don't know this stuff.

[Scott Morrison]

Then we need enriched identities and enriched composition, which will be morphisms in V.

[Scott Morrison]

The enriched identity is just a V-morphism 𝟙_ V ⟶ (X ⟶[V] X). We could probably simplify this even further if we restricted to the case where the forgetful functor from V to Type is assumed to be representable --- as it is for Ab, of course.

[Scott Morrison]

The enriched composition is a V-morphism (X ⟶[V] Y) ⊗ (Y ⟶[V] Z) ⟶ (X ⟶[V] Z), i.e., in the Ab case, a bilinear map.

[Scott Morrison]

Then we need an identification before the type underlying X ⟶[V] Y and X ⟶ Y itself. I wish there was a way to insist these were definitionally equal, but I think there just isn't, so we need to keep track of this iso.

[Kevin Buzzard]

I'm still stuck at lax monoidal. If I have a faithful functor to Type then $X\otimes Y$ doesn't make sense.

[Scott Morrison]

After that we need the identities saying that the enriched identity and enriched composition descend to the original one at the type level.

[Johan Commelin]

Depends on what $\otimes$ means

[Scott Morrison]

Yes --- in Type the monoidal structure is just going to be cartesian product.

[Scott Morrison]

So lax monoidal just says we have a sensible function from $F(X) \times F(Y) \to F(X \otimes Y)$, which is the "construct a pure tensor" function.

[Kevin Buzzard]

Got it.

[Scott Morrison]

The axioms for "lax monoidal" are just saying that this is appropriately associative when we do threefold products, and natural in X and Y.

[Kevin Buzzard]

I was just imagining you were going to be putting a typeclass structure on hom sets e.g. [add_comm_group (X \h Y)]

[Scott Morrison]

Well, the problem is that we need to know that composition is a morphism in the appropriate category.

[Kevin Buzzard]

This is a really complex set-up!

[Scott Morrison]

It may well be possible to do simpler things in special cases. :-) But I'm not keen to do this once for add_comm_group, and then again for module R, and then ...

[Kevin Buzzard]

Exactly.

[Scott Morrison]

We'll certainly provide that instance, when V is a bundled category.

[Scott Morrison]

So you really will be able to write f + g.

[Kevin Buzzard]

Is it common for a category to be "enriched over itself"?

[Scott Morrison]

Yes.

[Scott Morrison]

And another route is to only do this.

[Kevin Buzzard]

e.g. if R is a commutative ring I think this is how it works. But if R is a non-commutative ring then it's enriched in/over/by/with Ab

[Kevin Buzzard]

I don't know the right preposition :-)

[Scott Morrison]

I think "over" is the usual one here.

[Kevin Buzzard]

and if C is a complex of R-modules with R commutative then C is probably enriched over R-mod

[Kevin Buzzard]

so there seems to be no real benefit in self-enrichment

[Johan Commelin]

Well, there is even the Hom-complex, right?

[Johan Commelin]

aka internal hom

[Kevin Buzzard]

i.e. you can set it up but then you'd immediately want other stuff anyway

[Scott Morrison]

"Categories enriched over themselves" go by names like "closed categories", "closed monoidal categories", etc.

[Scott Morrison]

Yes, chain complexes also have internal hom, but you don't always want to think about that.

[Johan Commelin]

But you also don't always want to not think about it (-;

[Kevin Buzzard]

I am thinking about Ext and Tor (for rings), it would be good to have these, but having spent some time thinking about this recently (and bearing in mind comments Chris always makes to me at Xena about doing things in the correct generality the first time around) I think that probably the thing to aim for is abelian categories.

[Scott Morrison]

Yes, we'll have to have two versions of chain complexes, one enriched over itself, and one enriched over something smaller.

[Scott Morrison]

Yes...

[Scott Morrison]

I think defining biproducts is a good easy step on the way to abelian categories.

[Scott Morrison]

We're getting pretty close otherwise.

[Kevin Buzzard]

I guess the dream situation would be that you write Ext and Tor once, and then magically they become abelian groups if R is a non-comm ring, and R-modules if it's commutative.

[Scott Morrison]

Exactly.

[Kevin Buzzard]

and even in number theory where almost everything is commutative, you still want group cohomology, and one way of doing this is ext and tor for the non-commutative group ring.

[Scott Morrison]

Defining "normal monomorphisms" and "normal epimorphisms" needs to be done as well.

[Reid Barton]

What even are those

[Kevin Buzzard]

the kernel of an epimorphism is a normal monomorphism? ;-)

[Reid Barton]

OK, I guess in most cases (like in an abelian category) it is the same as regular monomorphism.

[Kevin Buzzard]

Oh I was just guessing!

[Reid Barton]

You were close enough

[Reid Barton]

Actually, it's the kernel of anything