Stream: maths

Topic: long exact sequence of cohomology

Kevin Buzzard (Mar 14 2020 at 11:31):

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

(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

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 (Mar 14 2020 at 11:39):

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 (Mar 14 2020 at 11:57):

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 (Mar 14 2020 at 12:00):

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

Markus Himmel (Mar 14 2020 at 12:01):

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 (Mar 14 2020 at 12:04):

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 (Mar 14 2020 at 12:05):

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

Kevin Buzzard (Mar 14 2020 at 12:09):

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 (Mar 14 2020 at 12:09):

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 (Mar 14 2020 at 12:10):

That sounds really ambitious!

Patrick Massot (Mar 14 2020 at 12:10):

That would be wonderful!

Markus Himmel (Mar 14 2020 at 12:11):

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 (Mar 14 2020 at 12:11):

(After many lines of declaring variables)

Patrick Massot (Mar 14 2020 at 12:11):

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 (Mar 14 2020 at 12:12):

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

Markus Himmel (Mar 14 2020 at 12:14):

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 (Mar 14 2020 at 12:21):

what does the chase tactic do exactly?

Markus Himmel (Mar 14 2020 at 12:21):

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 (Mar 14 2020 at 12:30):

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 (Mar 14 2020 at 12:32):

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 (Mar 14 2020 at 12:33):

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

Mario Carneiro (Mar 14 2020 at 12:33):

seems like it would be easier to just prove them all

Markus Himmel (Mar 14 2020 at 12:36):

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 (Mar 14 2020 at 12:37):

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

Markus Himmel (Mar 14 2020 at 12:45):

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 (Mar 14 2020 at 13:23):

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

Mario Carneiro (Mar 14 2020 at 13:25):

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

Markus Himmel (Mar 14 2020 at 13:28):

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 (Mar 14 2020 at 13:28):

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

Mario Carneiro (Mar 14 2020 at 13:43):

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 (Mar 14 2020 at 16:00):

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

Reid Barton (Mar 14 2020 at 16:39):

The hole might be larger than what is there

Kevin Buzzard (Mar 14 2020 at 17:48):

@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 (Mar 14 2020 at 17:49):

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 (Mar 14 2020 at 17:49):

Let me slice it up asap.

Scott Morrison (Mar 14 2020 at 17:51):

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 (Mar 14 2020 at 17:51):

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 (Mar 14 2020 at 17:52):

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

Kevin Buzzard (Mar 14 2020 at 17:52):

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

Kevin Buzzard (Mar 14 2020 at 17:53):

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

Scott Morrison (Mar 14 2020 at 17:57):

Yes, that's exactly what enriched means.

Scott Morrison (Mar 14 2020 at 17:58):

(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 (Mar 14 2020 at 17:58):

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

Scott Morrison (Mar 14 2020 at 18:00):

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 (Mar 14 2020 at 18:01):

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 (Mar 14 2020 at 18:02):

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 (Mar 14 2020 at 18:03):

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 (Mar 14 2020 at 18:03):

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)


This says...

Scott Morrison (Mar 14 2020 at 18:04):

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 (Mar 14 2020 at 18:04):

(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 (Mar 14 2020 at 18:05):

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 (Mar 14 2020 at 18:05):

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

Scott Morrison (Mar 14 2020 at 18:07):

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 (Mar 14 2020 at 18:07):

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 (Mar 14 2020 at 18:08):

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 (Mar 14 2020 at 18:08):

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 (Mar 14 2020 at 18:09):

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 (Mar 14 2020 at 18:09):

Depends on what $\otimes$ means

Scott Morrison (Mar 14 2020 at 18:09):

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

Scott Morrison (Mar 14 2020 at 18:10):

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.

Got it.

Scott Morrison (Mar 14 2020 at 18:11):

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 (Mar 14 2020 at 18:13):

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 (Mar 14 2020 at 18:15):

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

Kevin Buzzard (Mar 14 2020 at 18:15):

This is a really complex set-up!

Scott Morrison (Mar 14 2020 at 18:16):

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 ...

Exactly.

Scott Morrison (Mar 14 2020 at 18:16):

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

Scott Morrison (Mar 14 2020 at 18:16):

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

Kevin Buzzard (Mar 14 2020 at 18:16):

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

Yes.

Scott Morrison (Mar 14 2020 at 18:17):

And another route is to only do this.

Kevin Buzzard (Mar 14 2020 at 18:17):

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 (Mar 14 2020 at 18:17):

I don't know the right preposition :-)

Scott Morrison (Mar 14 2020 at 18:18):

I think "over" is the usual one here.

Kevin Buzzard (Mar 14 2020 at 18:18):

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

Kevin Buzzard (Mar 14 2020 at 18:18):

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

Johan Commelin (Mar 14 2020 at 18:18):

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

aka internal hom

Kevin Buzzard (Mar 14 2020 at 18:18):

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

Scott Morrison (Mar 14 2020 at 18:18):

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

Scott Morrison (Mar 14 2020 at 18:19):

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

Johan Commelin (Mar 14 2020 at 18:19):

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

Kevin Buzzard (Mar 14 2020 at 18:20):

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 (Mar 14 2020 at 18:20):

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

Yes...

Scott Morrison (Mar 14 2020 at 18:20):

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

Scott Morrison (Mar 14 2020 at 18:20):

We're getting pretty close otherwise.

Kevin Buzzard (Mar 14 2020 at 18:20):

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.

Exactly.

Kevin Buzzard (Mar 14 2020 at 18:21):

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 (Mar 14 2020 at 18:23):

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

Reid Barton (Mar 14 2020 at 18:33):

What even are those

Kevin Buzzard (Mar 14 2020 at 18:33):

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

Reid Barton (Mar 14 2020 at 18:37):

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

Kevin Buzzard (Mar 14 2020 at 19:10):

Oh I was just guessing!

Reid Barton (Mar 14 2020 at 19:11):

You were close enough

Reid Barton (Mar 14 2020 at 19:11):

Actually, it's the kernel of anything

Last updated: May 18 2021 at 06:15 UTC