Zulip Chat Archive

Stream: condensed mathematics

Topic: for_mathlib/truncation.lean


Kevin Buzzard (Jun 02 2022 at 15:29):

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

Kevin Buzzard (Jun 02 2022 at 16:59):

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 (Jun 02 2022 at 17:01):

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

Kevin Buzzard (Jun 02 2022 at 17:04):

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

Adam Topaz (Jun 02 2022 at 17:04):

docs#image_to_kernel'

Adam Topaz (Jun 02 2022 at 17:05):

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

Adam Topaz (Jun 02 2022 at 17:07):

Ah we have docs#category_theory.abelian.image

Adam Topaz (Jun 02 2022 at 17:07):

This is such a mess... :expressionless:

Adam Topaz (Jun 02 2022 at 17:11):

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

Adam Topaz (Jun 02 2022 at 17:14):

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

Adam Topaz (Jun 03 2022 at 12:11):

@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 (Jun 03 2022 at 22:14):

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 (Jun 05 2022 at 10:53):

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 dd but I'll call them ff and gg, so f:ABf:A\to B and g:BCg: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)J:=Im(f) and K:=ker(g)K:=ker(g), with the map i:JKi:J\to K being the canonical inclusion coming from the assumption gf=0gf=0. The second only has one non-zero term H:=K/JH:=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 JKJ\to K to the one-nonzero-term complex HH sending KK to HH via the canonical map, and all other down maps are 0. This induces a map on cohomology from K/JK/J to H=K/JH=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 0H00\to H\to 0 is not HH, 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 (Jun 05 2022 at 11:00):

@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 (Jun 05 2022 at 11:12):

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 (Jun 05 2022 at 11:17):

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 (Jun 05 2022 at 11:38):

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

Johan Commelin (Jun 06 2022 at 06:02):

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

Kevin Buzzard (Jun 08 2022 at 15:11):

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

Kevin Buzzard (Jun 16 2022 at 13:11):

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

Johan Commelin (Jun 18 2022 at 12:37):

Thanks so much for filling in those sorrys!


Last updated: Dec 20 2023 at 11:08 UTC