isLimitKernelFork — Mathlib

English

In an injective resolution I of an object Z in a category with zero object and zero morphisms, the kernel of the first differential in the cocomplex I is Z; equivalently the kernel fork is a limit.

Русский

В инъективном разрешении I объекта Z в категории с нулевым объектом и нулевыми морфизмами ядро первого дифференциала кокомplexа I изоморфно Z; эквивалентно, что форк ядра является пределом.

LaTeX

$$$Z \cong \ker\bigl(I.cocomplex.X_0 \longrightarrow I.cocomplex.X_1\bigr)$$$

Lean4

/-- `Z` is the kernel of `I.cocomplex.X 0 ⟶ I.cocomplex.X 1` when `I : InjectiveResolution Z`. -/
def isLimitKernelFork : IsLimit (I.kernelFork) :=
  by
  refine IsLimit.ofIsoLimit (I.cocomplex.cyclesIsKernel 0 1 (by simp)) (Iso.symm ?_)
  refine Fork.ext ((singleObjHomologySelfIso _ _ _).symm ≪≫ isoOfQuasiIsoAt I.ι 0 ≪≫ I.cocomplex.isoHomologyπ₀.symm) ?_
  rw [← cancel_epi (singleObjHomologySelfIso (ComplexShape.up ℕ) _ _).hom, ← cancel_epi (isoHomologyπ₀ _).hom, ←
    cancel_epi (singleObjCyclesSelfIso (ComplexShape.up ℕ) _ _).inv]
  simp

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