cokernel_lift_iso_kernel_desc

Stream: Is there code for X?

[Andrew Yang]

Do we have this canonical iso somewhere? Or that this is simply not true?
I don't have a good way to construct the inverse map though.

noncomputable
def cokernel_lift_iso_kernel_desc {V : Type*} [category V] [abelian V]
  {A B C : V} (f : A ⟶ B) (g : B ⟶ C) (w : f ≫ g = 0) :
  cokernel (kernel.lift g f w) ≅ kernel (cokernel.desc f g w) := sorry

[Riccardo Brasca]

This looks very similar to what I've been doing for derived functors. Let me check if it is actually identical.

[Riccardo Brasca]

What are you working on?

[Andrew Yang]

I'm constructing projective replacements of bounded cochain complexes.

[Riccardo Brasca]

I didn't prove this one, but you can have a look here.

[Riccardo Brasca]

I think you can do it using pseudoelements

[Riccardo Brasca]

You have the morphism in one direction, right?

[Riccardo Brasca]

(My file is a mess, I know. I will clean it once it's sorry free)

[Andrew Yang]

The morphism is just
cokernel.desc _ (kernel.lift _ (kernel.ι _ ≫ cokernel.π _) (by simp)) (by { ext, simp }).
Yeah, I'm also fiddling with pseudoelements. Not sure if there is a cleaner proof though.

[Markus Himmel]

The morphism is also equal to kernel.lift _ (cokernel.desc _ (kernel.ι g ≫ cokernel.π _) (by simp)) (by { ext, simp }), and I think using one way you can show that it is mono, and with the other way that it is epi.

[Markus Himmel]

(deleted)

[Markus Himmel]

Here's a full proof without pseudoelements:

import category_theory.abelian.basic

noncomputable theory

open category_theory
open category_theory.limits

variables {V : Type*} [category V] [abelian V]
variables {A B C : V} (f : A ⟶ B) (g : B ⟶ C) (w : f ≫ g = 0)

def cokernel_lift_to_kernel_desc₁ : cokernel (kernel.lift g f w) ⟶ kernel (cokernel.desc f g w) :=
kernel.lift _ (cokernel.desc _ (kernel.ι g ≫ cokernel.π _) (by simp)) (by { ext, simp })

def cokernel_lift_to_kernel_desc₂ : cokernel (kernel.lift g f w) ⟶ kernel (cokernel.desc f g w) :=
cokernel.desc _ (kernel.lift _ (kernel.ι g ≫ cokernel.π _) (by simp)) (by { ext, simp })

lemma cokernel_lift_to_kernel_desc_eq :
  cokernel_lift_to_kernel_desc₁ f g w = cokernel_lift_to_kernel_desc₂ f g w :=
by { ext, simp [cokernel_lift_to_kernel_desc₁, cokernel_lift_to_kernel_desc₂] }

instance : mono (cokernel.desc (kernel.lift g f w) (kernel.ι g ≫ cokernel.π f) (by simp)) :=
begin
  let x := kernel.lift g f w,
  let t := (cokernel.desc (kernel.lift g f w) (kernel.ι g ≫ cokernel.π f) (by simp)),
  suffices : is_colimit (pushout_cocone.mk t (cokernel.π f) _ : pushout_cocone (cokernel.π x) (kernel.ι g)),
  { exact abelian.mono_inl_of_is_colimit _ _ this,
    simp },
  refine pushout_cocone.is_colimit_aux' _ (λ s, _),
  refine ⟨cokernel.desc f s.inr _, ⟨_, _, λ m w w', _⟩⟩,
  { rw [← kernel.lift_ι g f w, category.assoc, ← s.condition, ← category.assoc, cokernel.condition,
      zero_comp] },
  { apply (cancel_epi (cokernel.π x)).1,
    simp only [s.condition, cokernel.π_desc, category.assoc, pushout_cocone.mk_inl,
      cokernel.π_desc_assoc] },
  { simp only [cokernel.π_desc, pushout_cocone.mk_inr] },
  { apply (cancel_epi (cokernel.π f)).1,
    simpa only [cokernel.π_desc] using w' }
end

instance : epi (kernel.lift (cokernel.desc f g w) (kernel.ι g ≫ cokernel.π f) (by simp)) :=
begin
  let x := cokernel.desc f g w,
  let t := (kernel.lift (cokernel.desc f g w) (kernel.ι g ≫ cokernel.π f)
    (by simp only [category.assoc, cokernel.π_desc, kernel.condition])),
  suffices : is_limit (pullback_cone.mk t (kernel.ι g) _ : pullback_cone (kernel.ι x) (cokernel.π f)),
  { exact abelian.epi_fst_of_is_limit _ _ this,
    simp only [kernel.lift_ι] },
  refine pullback_cone.is_limit_aux' _ (λ s, _),
  refine ⟨kernel.lift g s.snd _, ⟨_, _, λ m w w', _⟩⟩,
  { rw [← cokernel.π_desc f g w, ← category.assoc, ← s.condition, category.assoc, kernel.condition,
      comp_zero] },
  { apply (cancel_mono (kernel.ι x)).1,
    simp only [s.condition, kernel.lift_ι, category.assoc, pullback_cone.mk_fst,
      kernel.lift_ι_assoc] },
  { simp only [kernel.lift_ι, pullback_cone.mk_snd] },
  { apply (cancel_mono (kernel.ι g)).1,
    simpa only [kernel.lift_ι] using w' }
end

instance mono_cokernel_lift_to_kernel_desc₁ : mono (cokernel_lift_to_kernel_desc₁ f g w) :=
kernel.lift_mono _ _ _

instance epi_cokernel_lift_to_kernel_desc₁ : epi (cokernel_lift_to_kernel_desc₁ f g w) :=
begin
  rw cokernel_lift_to_kernel_desc_eq,
  exact cokernel.desc_epi _ _ _
end

instance : is_iso (cokernel_lift_to_kernel_desc₁ f g w) :=
is_iso_of_mono_of_epi _

noncomputable
def cokernel_lift_iso_kernel_desc {V : Type*} [category V] [abelian V]
  {A B C : V} (f : A ⟶ B) (g : B ⟶ C) (w : f ≫ g = 0) :
  cokernel (kernel.lift g f w) ≅ kernel (cokernel.desc f g w) :=
as_iso (cokernel_lift_to_kernel_desc₁ f g w)

[Adam Topaz]

@Andrew Yang https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/LES.20for.20Ext/near/272419447

[Adam Topaz]

So is everyone ready to change the definition of homology now?

[Riccardo Brasca]

I am in favor of changing it, but we already use quite a lot in the LTE. I don't know how much work a refactor would be

[Adam Topaz]

We should at least add the API obtained by identifying it with a cokernel or kernel, similarly to the lemmas in the code under the link I posted

[Adam Topaz]

That would make it much more pleasant to work with IMO

[Adam Topaz]

This should help: #12171

[Riccardo Brasca]

I am adding the file to the LTE (shamelessly of course, but you're listed as the author).

[Riccardo Brasca]

I am already lost trying to use your constructions :D Do you see an easy way of providing the following?

def left_derived.zero_to_self_obj_hom [enough_projectives C] {X : C}
  (P : ProjectiveResolution X) : (F.left_derived 0).obj X ⟶ F.obj X

[Adam Topaz]

Perhaps using homology.desc'? I'm away from my computer, so I can't check

[Riccardo Brasca]

I mean, I already have it with the current API, it's just to play with what you did

[Adam Topaz]

If you want to map out of homology, you can use homology.desc' and if you want to map into it, use homology.lift

[Riccardo Brasca]

Something like

def left_derived.zero_to_self_obj_hom [enough_projectives C] {X : C}
  (P : ProjectiveResolution X) : (F.left_derived 0).obj X ⟶ F.obj X :=
(left_derived_obj_iso F 0 P).hom ≫ homology.desc' _ _ _ (kernel.ι _ ≫ (F.map (P.π.f 0)))
begin
  { have : (complex_shape.down ℕ).rel 1 0 := rfl,
    rw [kernel.lift_ι_assoc, homological_complex.d_to_eq _ this, map_homological_complex_obj_d,
      category.assoc, ← functor.map_comp],
    simp },
end
≫ F.map (𝟙 _)

works (I don't know if using P is a good idea or not). In any case naturality of this morphism seems a pain. I will have a closer look tomorrow.

[Adam Topaz]

@Riccardo Brasca I added the lemmas you asked for in #12171 .
homology.map is pretty clunky to work with. Maybe we should think about (eventually) redefining homology.map to be, e.g.
homology.desc' _ _ _ (homology.lift _ _ _ (kernel.ι _ ≫ β.left ≫ cokernel.π _) _) _.

[Adam Topaz]

Note that the proofs that switch between homology.desc' ... (homology.lift ...) and homology.lift ... (homology.desc' ...) are now just a simple ext, simp game.

[Adam Topaz]

This should make the naturality of your map pretty simple to prove I think.

[Riccardo Brasca]

Thanks!!

[Adam Topaz]

Adam Topaz said:

This should make the naturality of your map pretty simple to prove I think.

Assuming you define it using homology.desc', of course!

[Riccardo Brasca]

I will do it later, but I agree it should be easy now.

[Riccardo Brasca]

I confirm it's now easy