for_mathlib/truncation.lean

Stream: condensed mathematics

[Kevin Buzzard]

I'm going to start working on this file now @Johan Commelin

[Kevin Buzzard]

def imker (C : cochain_complex 𝓐 ℤ) (n : ℤ) : cochain_complex 𝓐 ℤ :=
{ X := λ i, if i = n-1 then image_subobject (C.d_to n) else
              if i = n then kernel_subobject (C.d_from n) else
                (has_zero_object.has_zero 𝓐).zero,
  d := λ i j, if hi : i = n - 1 then if hj : j = n then by
       { rw if_pos hi, rw if_pos hj,
         rw if_neg (show j ≠ n - 1, by {rw hj, linarith }),
         exact image_to_kernel _ _ (homological_complex.d_to_comp_d_from _ n)} else 0 else 0,
  shape' := begin
    rintro i j (h : _ ≠ _),
    split_ifs with hi,
    { simp only [eq_mpr_eq_cast, cast_cast, dite_eq_right_iff],
      rintro rfl,
      exact (h (add_eq_of_eq_sub hi)).elim, },
    { refl },
  end,
  d_comp_d' := begin
    rintro i j k (rfl : _ = _) (rfl : _ = _),
    split_ifs with hi,
    { subst hi,
      rw dif_pos (sub_add_cancel n 1),
      simp only [one_ne_zero, add_right_eq_self, not_false_iff, dif_neg, comp_zero], },
    { apply zero_comp },
  end }

There's a pretty horrible definition. Do you think I can get away with it? Maybe! I guess I'll start filling in the three sorries about imker and stop either if I get stuck or if someone pops up here suggesting a nicer definition. I only used image_subobject and kernel_subobject because I can then use image_to_kernel to define the morphism. Is there a morphism (image f) -> (kernel g) if f >> g = 0?

[Adam Topaz]

WARNING: subobjects are pretty painful to work with in my opiniion!

[Kevin Buzzard]

Do you know how to get the map image f -> kernel g if f >> g = 0?

[Adam Topaz]

docs#image_to_kernel'

[Adam Topaz]

UGH but the definition of image is also terrible. IMO it should have been defined as kernel (cokernel.\pi f).

[Adam Topaz]

Ah we have docs#category_theory.abelian.image

[Adam Topaz]

This is such a mess... :expressionless:

[Adam Topaz]

In any case, the comparison between the two images is docs#category_theory.abelian.image_iso_image

[Adam Topaz]

Unfortunately docs#category_theory.abelian.image_to_kernel doesn't exist.

[Adam Topaz]

@Kevin Buzzard I saw your comment

local attribute [instance] has_zero_object.has_zero -- isn't there a locale which does this??

The answer should be open_locale zero_object.

[Kevin Buzzard]

Thanks! I'll get back to working on this file again tomorrow, hopefully I have many hours to spend on it as I'm travelling through Europe by train all day

[Kevin Buzzard]

I was rather surprised yesterday with how slow progress was. I'm still very much working on this file, I wrote hundreds of lines during many hours on several train journeys across Europe but still didn't finish the boss level of imker. I have reduced the boss to the final stage though. While it's fresh in my mind and before I start on an afternoon's marking, let me tell you the thing which looked easy but turned out to be long.

Let's say we have two maps both called $d$ but I'll call them $f$ and $g$, so $f:A\to B$ and $g:B\to C$, and let's assume f >> g = 0. I can now make two complexes. The first only has two non-zero terms, $J:=Im(f)$ and $K:=ker(g)$, with the map $i:J\to K$ being the canonical inclusion coming from the assumption $gf=0$. The second only has one non-zero term $H:=K/J$, the homology of the original three-term complex. So we're flattening three terms to two to one.

There's a canonical map from the two-nonzero-term complex $J\to K$ to the one-nonzero-term complex $H$ sending $K$ to $H$ via the canonical map, and all other down maps are 0. This induces a map on cohomology from $K/J$ to $H=K/J$ and the claim is that this is an isomorphism. So on paper it looks like there is nothing even to prove, because the map is the identity!

But the cohomology of $0\to H\to 0$ is not $H$, it's a cokernel of an image_to_kernel map from some subobject to some other subobject. If you unravel the question then it becomes the following: Is the obvious map from Im(Im(f)->ker(g)) to ker(ker(g)->ker((ker(g)/Im(f))->0) an isomorphism? Of course the answer to this is going to be "yes" but it took several hours to reduce the question to this (i.e. to cut through all the other definitions and deal with d_prev v d etc), and now I am slowly reducing the question to simpler and simpler ones; I'll get there in the end.

Do you think I'm missing ideas, or just API? The API which I've developed to get me this far is here and I feel like I'm in control -- it's just a case of figuring out what I need for my next move and then proving it if it's not there. I must say that I feel far more at home manipulating abelian categories than I do with general categories, so in contrast to previous adventures I've had in category land (which I've found generally frustrating and challenging) this time I'm having a whole lot of fun. Progress is still slow but I feel like some of the stuff I'm generating might be helpful elsewhere.

[Adam Topaz]

@Kevin Buzzard to construct a map to/from homology, in my opinion, the best approach is to use docs#homology.desc' and docs#homology.lift (as I mentioned before, I find the subobjects approach to be really difficult to work with). We also have a useful isomorphism in for_mathlib/homology_iso which should help get rid of the annoying X_next and X_prev.

[Kevin Buzzard]

Yeah I got rid of them yesterday. Right now I've not had to engage with subobjects in any way other than a superficial one, but they're looming. Right now homology.map is defined in terms of cokernel.desc so that was what I used. Perhaps what you're saying is that it would have been less pain to have worked with a different definition.

[Adam Topaz]

Take a look at the mathlib file category_theory/abelian/homology near the bottom, there are several lemmas that let you rewrite homology.map in terms of desc'or lift.

[Kevin Buzzard]

Right now I'm unsure about whether to go back to this approach or to press on with my own.

[Johan Commelin]

@Kevin Buzzard FYI: I split the file into two pieces. There is now a imker.lean.

[Kevin Buzzard]

I'm now working on the sorries in this file.

[Kevin Buzzard]

for_mathlib/truncation.lean is sorry-free! It needs a refactor.

[Johan Commelin]

Thanks so much for filling in those sorrys!