projective_obj — Mathlib

English

If F is an equivalence, F preserves projective objects.

Русский

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

LaTeX

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

Lean4

/-- See `Functor.projective_obj_of_projective` for a variant taking `Projective X` as an explicit
argument. -/
instance projective_obj (F : C ⥤ D) [F.PreservesProjectiveObjects] (X : C) [Projective X] : Projective (F.obj X) :=
  Functor.PreservesProjectiveObjects.projective_obj inferInstance

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