isLimitImage — Mathlib

English

Reiteration of the fork-based exactness criterion for short complexes.

Русский

Повторение критерии точности, основанной на форках для кратких комплексов.

LaTeX

$$$S.Exact \\iff cg.ι ≫ cf.π = 0$$$

Lean4

/-- If `(f, g)` is exact, then `Abelian.image.ι S.f` is a kernel of `S.g`. -/
def isLimitImage (h : S.Exact) :
    IsLimit (KernelFork.ofι (Abelian.image.ι S.f) (Abelian.image_ι_comp_eq_zero S.zero) : KernelFork S.g) :=
  by
  rw [exact_iff_kernel_ι_comp_cokernel_π_zero] at h
  exact
    KernelFork.IsLimit.ofι _ _
      (fun u hu ↦ kernel.lift (cokernel.π S.f) u (by rw [← kernel.lift_ι S.g u hu, Category.assoc, h, comp_zero]))
      (by simp) (fun _ _ _ hm => by rw [← cancel_mono (Abelian.image.ι S.f), hm, kernel.lift_ι])

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