exact_of_f_is_kernel — Mathlib

English

Kernel-limit implies exactness.

Русский

Предел ядра приводит к точности.

LaTeX

$$$ IsLimit(KernelFork.ofι S.f S.zero) \\Rightarrow S.Exact $$$

Lean4

theorem exact_of_f_is_kernel (hS : IsLimit (KernelFork.ofι S.f S.zero)) [S.HasHomology] : S.Exact :=
  by
  rw [exact_iff_epi_toCycles]
  have : IsSplitEpi S.toCycles :=
    ⟨⟨{   section_ := hS.lift (KernelFork.ofι S.iCycles S.iCycles_g)
          id := by
            rw [← cancel_mono S.iCycles, assoc, toCycles_i, id_comp]
            exact Fork.IsLimit.lift_ι hS }⟩⟩
  infer_instance

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