English
The inverse of the kernel iso is the cokernel comparison; i.e., the isomorphism component is given by cokernelComparison.
Русский
Обратная часть изоморфизма ядра равна cokernel-сравнению; то есть составная часть изоморфизма равна cokernelComparison.
LaTeX
$$$(\\mathrm{PreservesKernel.iso}\\;G\\;f).{\\text{inv}} = \\mathrm{cokernelComparison}(f,G)$$$
Lean4
/-- The map of a kernel fork is a limit iff
the kernel fork consisting of the mapped morphisms is a limit.
This essentially lets us commute `KernelFork.ofι` with `Functor.mapCone`.
This is a variant of `isLimitMapConeForkEquiv` for equalizers,
which we can't use directly between `G.map 0 = 0` does not hold definitionally.
-/
def isLimitMapConeForkEquiv' :
IsLimit (G.mapCone (KernelFork.ofι h w)) ≃
IsLimit (KernelFork.ofι (G.map h) (by simp only [← G.map_comp, w, Functor.map_zero]) : Fork (G.map f) 0) :=
KernelFork.isLimitMapConeEquiv _ _
