Challenge with homology

Stream: maths

[Adam Topaz]

Here's a bit of a challenge, in case anyone is bored. Fill in the sorry!

import category_theory.abelian.opposite
import category_theory.abelian.exact

noncomputable theory

open category_theory

variables {C : Type*} [category C] [abelian C]
  {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)

lemma w_op (w : f ≫ g = 0) : (g.op ≫ f.op = 0) := by { simp [← op_comp, w] }

def ugh (w : f ≫ g = 0) : (homology g.op f.op (w_op f g w)).unop ≅ homology f g w := sorry

[Johan Commelin]

cc @Markus Himmel @Scott Morrison :crazy:

[Adam Topaz]

And @Bhavik Mehta

[Markus Himmel]

I guess this is similar in spirit to https://github.com/TwoFX/lean-homological-algebra/blob/lean-3.8.0/src/dual_cohomology_construction.lean, except of course that my code has bitrotted and uses thre wrong definitions

[Adam Topaz]

Yes, that's exactly the point. When you undualize the homology of the dual, you get the second construction from that file using coker_to_coim

[Adam Topaz]

on a somewhat related note, maybe we should introduce a Prop valued class for f ≫ g = 0 and ask that exact f g extend that, while also replacing the explicit assumption for homology with such an instance?

[Kevin Buzzard]

Can you explain the mathematical issue for those of us too lazy to try and prove this on a Friday night?

[Adam Topaz]

@Kevin Buzzard Here's a summary of the issue. Suppose $f : A \to B$ and $g : B \to C$$ are morphisms in an abelian caategory whose composition is $0$, and let w denote a proof of this fact. This means that we have a canonically induced morphism $\gamma : image(f) \to kernel(g)$, and homology f g w is defined to be the cokernel of this morphism $\gamma$, as usual.

Now, the opposite category is again abelian, and we have w' := w_op w asserting that the composition of g.op and f.op is 0. So we can compute homology g.op f.op w', and go back to the original category using opposite.unop. The goal is to prove that (homology g.op f.op w').unop is isomorphic to homology f g w.

But kernels in the opposite category correspond to cokernels in the original category (and vice versa), so (homology g.op f.op w').unop is really the kernel of something (this is where the map coker_to_coim comes in), while homology f g w is the cokernel of something. The challenge is in relating these two objects, which a priori satisfy different universal properties (in the sense that one is a kernel and one is a cokernel).

[Adam Topaz]

Thinking more about this is making me wonder why we didn't define homology of $f : A \to B$ and $g : B \to C$ as the cokernel of kernel.lift ... : A \to (kernel g). I feel like this whole suubobject approach is just making things more difficult in this case.

[Scott Morrison]

Hopefully an iso to the cokernel of the lift to the kernel is available already?

[Adam Topaz]

Scott Morrison said:

Hopefully an iso to the cokernel of the lift to the kernel is available already?

Is it? I didn't see such an iso, but it's very possible I missed it

[Adam Topaz]

import category_theory.abelian.opposite
import category_theory.abelian.exact

noncomputable theory

open category_theory
open category_theory.limits

variables {C : Type*} [category C] [abelian C]
  {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)

def homology_iso_cokernel_lift (w : f ≫ g = 0) :
  homology _ _ w ≅ cokernel (kernel.lift _ _ w) :=
{ hom := cokernel.desc _ ((kernel_subobject_iso _).hom  ≫ cokernel.π _) sorry,
  inv := cokernel.desc _ ((kernel_subobject_iso _).inv ≫ homology.π _ _ _) sorry,
  hom_inv_id' := sorry,
  inv_hom_id' := sorry }

At least the data is easy to define, but 30 seconds of playing around got me nowhere in the proofs, which is a bit annoying...

[Scott Morrison]

I agree this is a problem. The following solves it, but needs some cleaning up and mathlib-ifying:

import category_theory.abelian.opposite
import category_theory.abelian.exact

noncomputable theory

open category_theory
open category_theory.limits

variables {C : Type*} [category C] [abelian C]
  {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)

def image_to_kernel' (w : f ≫ g = 0) : image f ⟶ kernel g :=
kernel.lift g (image.ι f) (by { ext, simpa using w, })

def foo (w : f ≫ g = 0) : homology f g w ≅ cokernel (image_to_kernel' f g w) :=
{ hom := cokernel.map _ _ (image_subobject_iso f).hom (kernel_subobject_iso g).hom
    (by { ext, simp [image_to_kernel'], }),
  inv := cokernel.map _ _ (image_subobject_iso f).inv (kernel_subobject_iso g).inv
    (by { ext, simp [image_to_kernel'], }),
  hom_inv_id' := begin apply coequalizer.hom_ext, simp, exact (category.comp_id _).symm, end, -- yuck?
  inv_hom_id' := begin apply coequalizer.hom_ext, simp, end, }

def bar (w : f ≫ g = 0) : cokernel (image_to_kernel' f g w) ≅ cokernel (kernel.lift g f w) :=
begin
  have p : factor_thru_image f ≫ image_to_kernel' f g w = kernel.lift g f w,
  { ext, simp [image_to_kernel'], },
  exact (cokernel_epi_comp _ _).symm ≪≫ cokernel_iso_of_eq p,
end

[Scott Morrison]

#8355