projective_obj_of_projective — Mathlib

English

If F preserves projective objects, then for any X projective in C, F.obj X is projective in D.

Русский

Если F сохраняет проективность объектов, то для любого X проективного в C, F.obj X проективен в D.

LaTeX

$$$ (\\forall X)\ (\\mathrm{Projective}(X) \\Rightarrow \\mathrm{Projective}(F\\!.(X))). $$$

Lean4

/-- See `Functor.projective_obj` for a variant taking `Projective X` as a typeclass argument. -/
theorem projective_obj_of_projective (F : C ⥤ D) [F.PreservesProjectiveObjects] {X : C} (h : Projective X) :
    Projective (F.obj X) :=
  Functor.PreservesProjectiveObjects.projective_obj h

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