isPreservedBy_of_preserves — Mathlib

English

Let S be a short complex in a category C with right homology data h2. If F is a functor from C to D that preserves zero morphisms and preserves the right homology of S, then h2 is preserved by F; i.e., h2.IsPreservedBy F.

Русский

Пусть S — короткий комплекс в категории C с правыми данными гомологии h2. Тогда если F: C → D — функтор, сохраняющий нулевые морфизмы и сохраняющий правую гомологию S, то h2 сохраняется относительно F; т.е. h2.IsPreservedBy F.

LaTeX

$$$h_2\text{ is preserved by }F\quad\text{whenever }F\text{ preserves the right homology of }S.$$$

Lean4

instance isPreservedBy_of_preserves [F.PreservesRightHomologyOf S] : h₂.IsPreservedBy F :=
  Functor.PreservesRightHomologyOf.isPreservedBy _

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