preservesProjectiveObjects_of_isEquivalence

English

If F is an equivalence, then F preserves projective objects.

Русский

Если F эквивалентна, то F сохраняет проективные объекты.

LaTeX

$$$ \\mathrm{IsEquivalence}(F) \\Rightarrow F.PreservesProjectiveObjects. $$$

Lean4

instance (priority := low) preservesProjectiveObjects_of_isEquivalence {F : C ⥤ D} [IsEquivalence F] :
    F.PreservesProjectiveObjects :=
  preservesProjectiveObjects_of_adjunction_of_preservesEpimorphisms F.asEquivalence.toAdjunction

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