Isomorphism from image to kernel

Stream: homology

[Yaël Dillies]

What is the @Joël Riou-approved way of getting that the image of the first map of a short exact complex is isomorphic to the kernel of the second one?

[Aaron Liu]

we also want the cokernel of the first map isomorphic to the coimage of the second one

[Joël Riou]

I think everything we need should be in https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Abelian/Exact.html

[Sophie Morel]

I would use https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Abelian/Exact.html#CategoryTheory.ShortComplex.Exact.isLimitImage and https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Abelian/Exact.html#CategoryTheory.ShortComplex.Exact.isColimitCoimage, plus the uniqueness (up to isomorphism) of kernel and cokernel.

[Andrew Yang]

I think the right question is that whether we should use docs#Abelian.image or docs#Abelian.coimage or docs#CategoryTheory.Limits.image or docs#CategoryTheory.Limits.imageSubobject for the "image"

[Sophie Morel]

If you decide to use the more general definition of the image, you have the analogues of the theorems I quoted (they're in the same file, just below).
Which one you decide to use depends on what else you are doing with images/coimages. In my experience with homological algebra, it was always more convenient to use Abelian.image and Abelian.coimage, but ymmv.
As for imageSubobject, I was not able to use it for my purposes when I tried.

[Aaron Liu]

we have an exact sequence A ⟶ B ⟶ C ⟶ D where we want to conclude that coker(A ⟶ B) ≅ ker(C ⟶ D) (since coker(A ⟶ B) ≅ coim(B ⟶ C) ≅ im(B ⟶ C) ≅ ker(C ⟶ D))

[Aaron Liu]

that's docs#CategoryTheory.Limits.cokernel and docs#CategoryTheory.Limits.kernel

[Sophie Morel]

I don't know how you enter your exact sequence exactly, but this seems to work:

import Mathlib.CategoryTheory.Abelian.Exact

open CategoryTheory

universe u

variable {E : Type u} [Category E] [Abelian E]

variable {A B C D : E} (f : A ⟶ B) (g : B ⟶ C) (h : C ⟶ D) (zero1 : f ≫ g = 0) (zero2 : g ≫ h = 0)

variable (ex1 : ShortComplex.Exact (ShortComplex.mk f g zero1))
variable (ex2 : ShortComplex.Exact (ShortComplex.mk g h zero2))

noncomputable example : Limits.cokernel f ≅ Limits.kernel h := by
  set e : Limits.cokernel f ≅ Abelian.coimage g := Limits.IsColimit.coconePointUniqueUpToIso (Limits.colimit.isColimit _)
    (Limits.IsColimit.ofIsoColimit ex1.isColimitCoimage (Limits.Cofork.ext (Iso.refl _)))
  set e'' : Abelian.image g ≅ Limits.kernel h := Limits.IsLimit.conePointUniqueUpToIso
    (Limits.IsLimit.ofIsoLimit ex2.isLimitImage (Limits.Fork.ext (Iso.refl _)) ) (Limits.limit.isLimit _)
  set e' := Abelian.coimageIsoImage g
  exact e ≪≫ e' ≪≫ e''

[Aaron Liu]

We also want this identification to be natural in the exact sequence

[Aaron Liu]

so it's a functor from the category of exact sequences of this length

[Sophie Morel]

The identification will be natural because the isomorphisms commute with any reasonable map, because of theorems like https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Limits/IsLimit.html#CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp
I could help, but only if you show me how your category of exact sequences is actually implemented.

[Yaël Dillies]

Thanks Sophie, but we already got there now: https://github.com/kbuzzard/ClassFieldTheory/pull/31/files#diff-cf53f2f0482db4201a596440e315c51d7c5c267bdc3e9b061e420d97255001d9