epi_f — Mathlib

English

Under a colimit cocone with IsColimit, the induced map f on X yields epimorphisms when J is filtered; i.e., epi_f holds.

Русский

При гомоморфизме f, полученном из колимита, если J фильтровано, то f является эпиморфизмом.

LaTeX

$$$[IsFiltered J] \Rightarrow Epi\; f(y)$$

Lean4

theorem epi_f [IsFiltered J] : Epi (f y) := by
  exact
    (colim.exact_mapShortComplex
          ((ShortComplex.mk _ _ (kernel.condition (g y))).exact_of_f_is_kernel (kernelIsKernel (g y)))
          (colimit.isColimit _) (isColimitConstCocone _ _)
          ((Functor.Final.isColimitWhiskerEquiv (Under.forget j₀) c).symm hc) (f y) 0 (fun j ↦ by simpa using hf y j)
          (fun _ ↦ by simpa using hy.symm)).epi_f
      rfl

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