map_of_mono_of_preservesKernel — Mathlib

English

Let S be exact, F a functor preserving zero morphisms, (S.map F) has right homology, S.f is mono, and F preserves the limit of the parallel pair (S.g, 0). Then (S.map F).Exact holds.

Русский

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

LaTeX

$$$S.Exact \land F.PreservesZeroMorphisms \land (S.map F).HasHomology \land Mono(S.f) \land PreservesLimit(\mathrm{parallelPair}(S.g,0), F) \Rightarrow (S.map F).Exact$$$

Lean4

theorem map_of_mono_of_preservesKernel (hS : S.Exact) (F : C ⥤ D) [F.PreservesZeroMorphisms] [(S.map F).HasHomology]
    (_ : Mono S.f) (_ : PreservesLimit (parallelPair S.g 0) F) : (S.map F).Exact :=
  exact_of_f_is_kernel _ (KernelFork.mapIsLimit _ hS.fIsKernel F)

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