Formula for the homology if a short complex `S`

Stream: Is there code for X?

[Sophie Morel]

Given a ShortComplex S in an abelian category, I have been looking for the isomorphism between S.homology and Limits.cokernel S.abelianImageToKernel in mathlib and not finding it, which makes me feel very stupid. Is that isomorphism really not there? (It did seem like the perfect use of ShortComplex.abelianImageToKernel.)

Just to be clear:
(1) I am aware of ShortComplex.homology'IsoHomology that says that the homology is S is the cokernel of imageToKernel, but I want to use the actual kernel and image (in its Abelian.image version) with their universal properties and all their API, not their "subobject" versions.
(2) I am also aware of imageToKernel' and of its isomorphism with imageToKernel, however mathlib does not seem to know that imagetoKernel' is a monomorphism, while it does know that abelianImageToKernel is; also, and more importantly because the Mono part would be easy to fix, I find Abelian.image much easier to use than Limits.image...
(3) I am also aware that the isomorphism between Abelian.image and Limits.image is in mathlib, however I did not find the compatibility betweem this isomorphism and the various versions of the imageToKernel morphism. In fact, it cost me some trouble to prove this.
(4) I did write my own code for the isomorphism I want, I just find it horribly ugly. Here it is:

import Mathlib.Algebra.Homology.ShortComplex.Abelian

open CategoryTheory Limits

variable {A : Type*} [Category A] [Abelian A] (S : ShortComplex A)

lemma image_compat : (Abelian.imageIsoImage S.f).hom ≫ (imageToKernel' S.f S.g S.zero) =
    S.abelianImageToKernel := by
  refine Mono.right_cancellation (f := kernel.ι S.g) _ _ ?_
  refine Epi.left_cancellation (f := (Abelian.imageIsoImage S.f).inv) _ _ ?_
  conv_lhs => rw [← Category.assoc, ← Category.assoc,  Iso.inv_hom_id, Category.id_comp]
  simp only [imageToKernel']
  simp only [kernel.lift_ι, IsImage.isoExt_inv, image.isImage_lift,
    ShortComplex.abelianImageToKernel_comp_kernel_ι, equalizer_as_kernel]
  refine Epi.left_cancellation (f := factorThruImage S.f) _ _ ?_
  simp only [image.fac, image.fac_lift_assoc, Abelian.imageStrongEpiMonoFactorisation_I,
    Abelian.imageStrongEpiMonoFactorisation_e, kernel.lift_ι]

noncomputable def ShortComplex.homologyIsoCokernelAbelianImageToKernel (S : ShortComplex A) :
    S.homology ≅ Limits.cokernel S.abelianImageToKernel := by
  refine (S.homology'IsoHomology.symm.trans (homology'IsoCokernelImageToKernel' S.f S.g
    S.zero)).trans ?_
  refine cokernel.mapIso (imageToKernel' S.f S.g S.zero) S.abelianImageToKernel
    (Abelian.imageIsoImage S.f).symm (Iso.refl _) ?_
  refine Epi.left_cancellation (f := (Abelian.imageIsoImage S.f).hom) _ _ ?_
  rw [Iso.refl, Category.comp_id, ← Category.assoc, Iso.symm_hom, Iso.hom_inv_id,
    Category.id_comp, image_compat]

[Sophie Morel]

In fact I found more formulas for the homology of a short complex there, but I couldn't figure out an easy way to get the one I wanted. I'm hoping that this is just because I missed something.

[Andrew Yang]

import Mathlib.Algebra.Homology.ShortComplex.Abelian

open CategoryTheory Limits

variable {A : Type*} [Category A] [Abelian A] (S : ShortComplex A)

noncomputable def ShortComplex.homologyIsoCokernelAbelianImageToKernel (S : ShortComplex A) :
    S.homology ≅ Limits.cokernel S.abelianImageToKernel :=
  S.homology'IsoHomology.symm ≪≫ homology'IsoCokernelImageToKernel' S.f S.g S.zero ≪≫
    cokernel.mapIso _ _ (Abelian.imageIsoImage S.f).symm (Iso.refl _)
      (by ext; simp [imageToKernel'])

Looks better, but maybe there's a way to use docs#CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian. @Joël Riou might know more.

[Andrew Yang]

Usually any purely category theoretical compatibility arguments could be proved with ext; simp. If not, we are probably missing simp lemmas.
Also why do you find Limits.image hard to work with? Can you list some pain points so that we can try to improve the API?

[Joël Riou]

The purpose of the file ShortComplex.Abelian was to show the existence of a HomologyData, such that the "left" homology and "right" homology are respectively given by the coimage/image of a certain map, which are isomorphic because of one of the characterizations of abelian categories.

[Joël Riou]

I have not formalized this specific isomorphism, but it should be easy following the general principle of the API that in order to compute the homology, we may provide a structure LeftHomologyData (or RightHomologyData):

import Mathlib.Algebra.Homology.ShortComplex.Abelian

namespace CategoryTheory

open Category Limits

namespace ShortComplex

variable {C : Type*} [Category C] [Abelian C] (S : ShortComplex C)

noncomputable def LeftHomologyData.ofIsColimitCokernelCoforkAbelianImageToKernel
    (cc : CokernelCofork S.abelianImageToKernel) (hcc : IsColimit cc) :
    S.LeftHomologyData where
  K := kernel S.g
  H := cc.pt
  i := kernel.ι S.g
  π := cc.π
  wi := by simp
  hi := kernelIsKernel S.g
  wπ := by
    have h := Abelian.factorThruImage S.f ≫= cc.condition
    rw [comp_zero, ← assoc] at h
    convert h
    simp [← cancel_mono (kernel.ι _)]
  hπ := CokernelCofork.IsColimit.ofπ _ _
      (fun a ha ↦ hcc.desc (CokernelCofork.ofπ (π := a) (by
        rw [← cancel_epi (Abelian.factorThruImage S.f), comp_zero, ← assoc]
        convert ha
        simp [← cancel_mono (kernel.ι _)])))
      (fun a ha ↦ hcc.fac _ _)
      (fun a ha b hb ↦ Cofork.IsColimit.hom_ext hcc (by simpa using hb))

noncomputable def homologyIsoCokernelAbelianImageToKernel :
    S.homology ≅ cokernel S.abelianImageToKernel :=
  (LeftHomologyData.ofIsColimitCokernelCoforkAbelianImageToKernel S _
    (cokernelIsCokernel _)).homologyIso

end ShortComplex

end CategoryTheory

[Joël Riou]

The definitions with names like homology' or homology'IsoHomology are remains of the old homology API, and shall be removed at some point...

[Sophie Morel]

Andrew Yang said:

Usually any purely category theoretical compatibility arguments could be proved with ext; simp. If not, we are probably missing simp lemmas.
Also why do you find Limits.image hard to work with? Can you list some pain points so that we can try to improve the API?

Thank you for the nicer code!

Concerning Limits.image, I've mostly worked with abelian categories so far, so for me the image is the kernel of the cokernel and I use that a lot. But Limits.image does not behave like that. For example I tried this:

import Mathlib.Algebra.Homology.ShortComplex.Abelian

open CategoryTheory Limits

variable {A : Type*} [Category A] [Abelian A]
variable {X Y : A} (f : X ⟶ Y)

noncomputable def test : KernelFork (cokernel.π f) := by
  refine KernelFork.ofι (image.ι f) ?_

And then I asked simp to close the goal. It couldn't. Then I asked exact?, and it also couldn't. Then I asked apply?, used its first suggestion and after that simp closed the goal:

noncomputable def test : KernelFork (cokernel.π f) := by
  refine KernelFork.ofι (image.ι f) ?_
  refine Eq.symm (image.ext f ?w)
  simp only [comp_zero, image.fac_assoc, cokernel.condition]

Okay, then I tried to see if lean knew that IsLimit (test f), but I couldn't find it.

I'm actually quite happy to use Abelian.image instead, until I run into stuff like what I mentioned in my original message, where some things exist for Limits.image for not Abelian.image. (I was trying to prove that a short complex S is exact if and only if the canonical morphism from the image of S.f to the kernel of S.g is an isomorphism and went back and forth on which version of the image I was supposed to use, since mathlib knew that S.homology is isomorphic to the cokernel of imageToKernel' S.f S.g S.zero but not that that morphism is a monomorphism, while it knew that S.abelianImageToKernel is a monomorphism but not that S.homology is isomorphic to its cokernel!)

[Sophie Morel]

Joël Riou said:

I have not formalized this specific isomorphism, but it should be easy following the general principle of the API that in order to compute the homology, we may provide a structure LeftHomologyData (or RightHomologyData):

import Mathlib.Algebra.Homology.ShortComplex.Abelian

namespace CategoryTheory

open Category Limits

namespace ShortComplex

variable {C : Type*} [Category C] [Abelian C] (S : ShortComplex C)

noncomputable def LeftHomologyData.ofIsColimitCokernelCoforkAbelianImageToKernel
    (cc : CokernelCofork S.abelianImageToKernel) (hcc : IsColimit cc) :
    S.LeftHomologyData where
  K := kernel S.g
  H := cc.pt
  i := kernel.ι S.g
  π := cc.π
  wi := by simp
  hi := kernelIsKernel S.g
  wπ := by
    have h := Abelian.factorThruImage S.f ≫= cc.condition
    rw [comp_zero, ← assoc] at h
    convert h
    simp [← cancel_mono (kernel.ι _)]
  hπ := CokernelCofork.IsColimit.ofπ _ _
      (fun a ha ↦ hcc.desc (CokernelCofork.ofπ (π := a) (by
        rw [← cancel_epi (Abelian.factorThruImage S.f), comp_zero, ← assoc]
        convert ha
        simp [← cancel_mono (kernel.ι _)])))
      (fun a ha ↦ hcc.fac _ _)
      (fun a ha b hb ↦ Cofork.IsColimit.hom_ext hcc (by simpa using hb))

noncomputable def homologyIsoCokernelAbelianImageToKernel :
    S.homology ≅ cokernel S.abelianImageToKernel :=
  (LeftHomologyData.ofIsColimitCokernelCoforkAbelianImageToKernel S _
    (cokernelIsCokernel _)).homologyIso

end ShortComplex

end CategoryTheory

Thanks for the code!

I understand that homology in mathlib is in the middle of an overhaul so it may be too early, but I think that this particular isomorphism should be there when homology is stabilized, because it's the definition that is most familiar to people in math.

[Sophie Morel]

(And the dual isomorphism as well, of course! Though I cannot argue that "kernel of the morphism from the cokernel to S.f to the coimage of S.g" is the definition that is commonly taught for the cohomology, I found myself just now using it without meaning to. :sweat_smile: )

[Joël Riou]

The homology API provides S.cycles (which is isomorphic to kernel of S.g, though it is not definitionally equal to it), and S.homology identifies to the cokernel of the morphism S.toCycles : S.X₁ ⟶ S.cycles. Then, any factorization of S.toCycles as an epi followed by another map (typically a mono) would give an alternative expression of the homology as a cokernel (even though, we may have missing definitions in order to show this: the API for cokernel coforks could be improved so that the hπ field above would become a one-liner). (More precisely if p ≫ g = f with p an epi, then there is an equivalence between cokernel coforks of f and g, and colimit coforks correspond via this bijection.)

[Joël Riou]

I would like to encourage people to use more S.cycles and all this homology API. This is the reason why I am not completely sure we absolutely need this particular isomorphism. The API already allows to construct and prove results in several different manners, and every time we introduce new isomorphisms, it is yet another way to phrase definitions and lemmas, even though the differences are only superficial, and introducing new isomorphisms also means that we need more simp lemmas to express the compatibilities they satisfy. If it is very important for certain applications, we will add it, but I would rather wait and see...

[Joël Riou]

The dual definition S.opcycles (and S.homology as a kernel instead of a cokernel) is actually very important for the applications. When I formalized Verdier's approach to spectral sequences from Des catégories dérivées des catégories abéliennes, even though there is no explicit mention of it in the book, certain objects which appear in the computations can be interpreted as S.opcycles for some S, and it turned out that for every lemma about cycles, I had to prove a dual one for opcycles in order to formalise spectral sequences in general abelian categories.

[Sophie Morel]

Okay, I'll see if I can things with cycles instead of kernel then.

I will probably be trying to use spectral sequences soon, and then things should get really fun. I am trying to formalize some constructions/lemmas of Beilinson (plus some additional stuff I had to do) about filtered triangulated categories, realization functors etc.

[Joël Riou]

It will take a lot of time before the following (undocumented) code on spectral objects in triangulated categories and abelian categories, and spectral sequences enters mathlib:
https://github.com/leanprover-community/mathlib4/tree/jriou_localization/Mathlib/Algebra/Homology/SpectralObject
https://github.com/leanprover-community/mathlib4/tree/jriou_localization/Mathlib/Algebra/Homology/SpectralSequence

[Sophie Morel]

No problem, I have been using a terrible Frankensteined merge of mathlib and your "localization" branch for a while now, because I was doing stuff with t-structures and I didn't want to write the definition of the cohomology functor myself. So in that way I already have spectral sequences in my branch.