π_iso_hom — Mathlib

English

The hom component of the kernel/cokernel iso matches the kernel/cokernel comparison morphism.

Русский

Гомоморфизм изоморфизма ядра/кокон совпадает с морфизмом сравнения ядра/кокон.

LaTeX

$$$(\\mathrm{PreservesCokernel.iso}\\; G f).hom = kernelComparison f G$$$

Lean4

@[reassoc (attr := simp)]
theorem π_iso_hom : G.map (cokernel.π f) ≫ (iso G f).hom = cokernel.π (G.map f) :=
  IsColimit.comp_coconePointUniqueUpToIso_hom (isColimitOfHasCokernelOfPreservesColimit G f) (colimit.isColimit _)
    (WalkingParallelPair.one)

Похожие утверждения