for_mathlib/imker

Stream: condensed mathematics

[Kevin Buzzard]

So truncation has been split into imker and truncation, and I've been working on imker a bit today. I've abstracted out the one remaining lemma we need to make the file sorry-free:

import category_theory.abelian.basic
import algebra.homology.homology

open category_theory category_theory.limits

variables (𝓐 : Type*) [category 𝓐] [abelian 𝓐]

lemma homology_functor.is_iso_of_is_zero_of_is_zero_of_is_zero {ι : Type*} {c : complex_shape ι}
  {i j : ι} (hij : c.rel i j) {C₁ C₂ : homological_complex 𝓐 c} (h1from : C₁.d_from j = 0)
  (h2to : C₂.d_to j = 0) (h2from : C₂.d_from j = 0) (isomap : cokernel (C₁.d_to j) ≅ C₂.X j)
  {f : C₁ ⟶ C₂} (hf : f.f j = cokernel.π (C₁.d_to j) ≫ isomap.hom) :
is_iso ((homology_functor 𝓐 c j).map f) :=
begin
  sorry
end

I haven't started trying to prove this yet. It looks like this is pretty much the same question as one I've been struggling with for a couple of days now but it's actually a bit easier because, for example, it doesn't mention kernel_subobjects. I plan on working more on this (in fact I plan on working on it until it's done) so if anyone else wants to leap in and have a go then please let me know so we don't duplicate work. If anyone has any suggestions I'd be interested to hear them; it's getting to the point where this should be becoming easy (I hope).

[Johan Commelin]

I guess if you specialize to ℤ-indexed gadgets your life becomes easier.

[Johan Commelin]

Because then you can assume that d_from and d_to are isomorphic to actual ds.

[Kevin Buzzard]

I'm not convinced this makes things easier, because d_from is just a map from a thing to a thing, and d is just a map from a thing to a thing. Here's an example of the problems I face here: I can't rewrite.

lemma homology_functor.is_iso_of_is_zero_of_is_zero_of_is_zero {ι : Type*} {c : complex_shape ι}
  {i j : ι} (hij : c.rel i j) {C₁ C₂ : homological_complex 𝓐 c} (h1from : C₁.d_from j = 0)
  (h2to : C₂.d_to j = 0) (h2from : C₂.d_from j = 0) (isomap : cokernel (C₁.d_to j) ≅ C₂.X j)
  {f : C₁ ⟶ C₂} (hf : f.f j = cokernel.π (C₁.d_to j) ≫ isomap.hom) :
is_iso ((homology_functor 𝓐 c j).map f) :=
begin
  simp,
  delta homology.map,
  dsimp,
  simp_rw h2to, -- fails :-(
end

I'm not convinced that it being d would make anything any different here.

[Kevin Buzzard]

Basically there are four maps at play, two d_froms and two d_tos, and we explicitly have hypotheses about every one of them. It's using them which is hard. Would it be any easier if they were d's? I'm not convinced. We have hij so we could make d_from into a d and if you want to add a hypothesis hjk : j + 1 = k this is fine because it's true in the application (even though it clearly is not relevant here because both d_from maps are zero).

[Kevin Buzzard]

I don't know whether it's relevant but this is one of those situations where if you put pp.all on then the size of the terms makes Mario shudder (and we're not even seeing the ten ...s at the end)

[Johan Commelin]

I think you are discovering more reasons why we need to refactor homology and give it a proper API with clearly defined API boundaries.

[Kevin Buzzard]

lemma homology_functor.is_iso_of_is_zero_of_is_zero_of_is_zero_Johan_variant
  {i j k : ℤ} (hij : i + 1 = j) (hjk : j + 1 = k)
  {C₁ C₂ : homological_complex 𝓐 (complex_shape.up ℤ)} (h1from : C₁.d j k = 0)
  (h2to : C₂.d i j = 0) (h2from : C₂.d j k = 0) (isomap : cokernel (C₁.d i j) ≅ C₂.X j)
  {f : C₁ ⟶ C₂} (hf : f.f j = cokernel.π (C₁.d i j) ≫ isomap.hom) :
is_iso ((homology_functor 𝓐 (complex_shape.up ℤ) j).map f) :=
begin
  simp,
  delta homology.map,
  dsimp, -- there are now d_to's anyway
  simp_rw homological_complex.d_to, -- fails
end

I tried it anyway. I don't know whether I'm supposed to unfolding homology.map but it unfolds into d_from and d_to anyway, and I still can't rewrite. I like a challenge, I'll think about this more tomorrow.

[Kevin Buzzard]

I should say that if I can rewrite then we get image_to_kernel 0 (C₂.d_from j) _ and then rw image_to_kernel_zero_left, means we can use cokernel.π_zero_is_iso and then cancel the isomorphism, making the question simpler.

[Kevin Buzzard]

aah, progress! I can't do the rewrite because the type of the term image_to_kernel f g w depends on f. Now I think I know how to fix it. Expect more excitingly slow progress tomorrow :-)

[Kevin Buzzard]

We have cokernel_iso_of_eq : f = g → (cokernel f ≅ cokernel g). I'm now wondering whether we need 100 more lemmas of this form.

[Kevin Buzzard]

We even have docs#category_theory.limits.cokernel_iso_of_eq_hom_comp_desc -- maybe we have them all already ;-) OK I'm back on track!

[Johan Commelin]

@Kevin Buzzard I've just written a def has_homology + a bunch of API.

[Johan Commelin]

I'm now trying to build LTE

[Johan Commelin]

If it all works, I hope this will allow you to monster golf your proof.

[Johan Commelin]

I haven't pushed yet, but I wanted to let you know. I've already golfed several annoying homology proofs in LTE.

[Kevin Buzzard]

Thanks! I need to do admin all morning but will hopefully be back to this this afternoon

[Kevin Buzzard]

I pushed some progress towards the imker lemma last night

[Johan Commelin]

I have pushed to the has-homology branch. I need to bring my son to a friend now. Will be back soon.

[Johan Commelin]

Ok, it compiles, merged into master and pushed.

[Kevin Buzzard]

Thanks! Will look later

[Kevin Buzzard]

I pushed some more API to the has_homology file. In particular: you related has_homology and homology; I've just related has_homology.map and homology.map and so now the problem I had (showing a homology.map is an isomorphism, which was going to be feasible but very slow going) can hopefully be reduced to showing that a has_homology.map is an isomorphism, and if we play our cards right this latter isomorphism might be the identity (as opposed to the original one, which was definitionally very very far from the identity!).

[Kevin Buzzard]

OK so imker is sorry-free! has_homology was indeed the missing piece of the puzzle.

I have never used abelian categories before; my recent efforts in LTE are my way of learning them. On the way to filling in these imker sorries I had to prove about 25 really basic lemmas about abelian categories: you can see them here. Probably every single one of them is true for a weaker class of category. I couldn't find any of these. Does this mean that (a) I shouldn't be using these lemmas at all (i.e. I'm thinking about category theory in the wrong way), (b) these lemmas are there but I'm just not finding them or (c) this is just missing API which should be PRed to mathlib? Some stuff seemed so basic.

[Adam Topaz]

I think some of the lemmas are probably not required.
When dealing with things that are limits and colimits we generally use some combination of ext, dsimp, simp to close such goals.
For example:

lemma cokernel.desc_comp_left {V : Type*} [category V]
  [abelian V] {A B C D : V} {f : A ⟶ B} {g : B ⟶ C} {e : C ⟶ D} (w : f ≫ g = 0) :
  (cokernel.desc f g w) ≫ e =
  (cokernel.desc f (g ≫ e) (by rw [← category.assoc, w, zero_comp])) :=
begin
  ext, simp,
end

works. And presumably your lemma

lemma cokernel.desc_spec {V : Type*} [category V]
  [abelian V] {A B C : V} {f : A ⟶ B} {g : B ⟶ C} (w : f ≫ g = 0)
  (c : cokernel f ⟶ C) : (cokernel.π f ≫ c = g) ↔ c = cokernel.desc f g w :=

isn't really necessary.

[Adam Topaz]

I'm quite surprised the epi_iff lemmas you proved are not in mathlib.

[Adam Topaz]

If they're really missing, then those should certainly be PRed eventually.

[Kevin Buzzard]

They might be there; I think typeclass inference might be interfering with my search. Oh wow what is this ext trick??

[Adam Topaz]

These are limits and colimits, and the ext applies a docs#category_theory.limits.colimit.hom_ext essentially

[Adam Topaz]

If you have more complicated limits, you may need an intros after the ext.

[Kevin Buzzard]

I have no idea how to work with limits. I think this is one of the reasons I've found category theory so hard. I've only had to use kernels and cokernels so far and here there has been bespoke API which I've found very easy to use. I'll try and understand what's going on! Thanks!

[Adam Topaz]

Note that your desc_spec lemma is essentially a version of docs#category_theory.limits.is_colimit.uniq

[Adam Topaz]

The lemma saying something about the composition of cokernel.\pi with cokernel.desc is essentially docs#category_theory.limits.is_colimit.fac

[Adam Topaz]

The map cokernel.desc itself is docs#category_theory.limits.is_colimit.desc etc.

[Kevin Buzzard]

Yeah I never think about what these things "actually are", I just want the lemmas. This is really bending my idea of what ext means!

[Adam Topaz]

Those are for situations where you have a is_colimit C for some cocone C. If you're dealing with the "colimit" itself (i.e. the noncomputable thing obtained by exists.some) then we have the associated defs/lemmas docs#category_theory.limits.colimit.hom_ext docs#category_theory.limits.colimit.\iota_desc (fix the unicode...) docs#category_theory.limits.colimit.desc etc.

[Kevin Buzzard]

I think you're saying that some stuff I want is special cases of statements about limits and for psychological reasons I've been avoiding thinking about things in this way; I don't ever think of a kernel as an equaliser, for example. I think of it as something with an API

[Adam Topaz]

And that's the right way to think of it! But you should keep in mind that the API mimics the limits api and try to use that because the simp lemmas have been set up to work well as such.