map_of_epi_of_preservesCokernel — Mathlib

English

If S is exact, F preserves zero morphisms, (S.map F) has homology, and S.g is epi with F preserving colimits in the parallel pair (S.f, 0), then (S.map F).Exact holds.

Русский

Если S точен, F сохраняет нулевые морфизмы, (S.map F) имеет гомологию и S.g эпиморфен, а F сохраняет колимит параллельной пары (S.f, 0), тогда (S.map F).Exact.

LaTeX

$$$S.Exact \land F.PreservesZeroMorphisms \land (S.map F).HasHomology \land Epi(S.g) \land PreservesColimit(\parallelPair(S.f,0), F) \Rightarrow (S.map F).Exact$$$

Lean4

theorem map_of_epi_of_preservesCokernel (hS : S.Exact) (F : C ⥤ D) [F.PreservesZeroMorphisms] [(S.map F).HasHomology]
    (_ : Epi S.g) (_ : PreservesColimit (parallelPair S.f 0) F) : (S.map F).Exact :=
  exact_of_g_is_cokernel _ (CokernelCofork.mapIsColimit _ hS.gIsCokernel F)

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