map — Mathlib

English

Exactness is preserved under the image of a functor F that preserves zero morphisms and appropriate homology data.

Русский

Точность сохраняется под образом функторов F, которые сохраняют нулевые морфизмы и соответствующие данные гомологий.

LaTeX

$$$ShortExact(S) \Rightarrow ShortExact(S.map(F))$$$

Lean4

theorem map (h : S.ShortExact) (F : C ⥤ D) [F.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S]
    [F.PreservesRightHomologyOf S] [Mono (F.map S.f)] [Epi (F.map S.g)] : (S.map F).ShortExact
    where
  exact := h.exact.map F
  mono_f := (inferInstance : Mono (F.map S.f))
  epi_g := (inferInstance : Epi (F.map S.g))

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