preservesProjectiveObjects_comp — Mathlib

English

If F and G preserve projective objects, then FG preserves projective objects.

Русский

Если F и G сохраняют проективность объектов, то композиция FG сохраняет проективность.

LaTeX

$$$ (F.PreservesProjectiveObjects) \\land (G.PreservesProjectiveObjects) \\Rightarrow ((F \\circ G).PreservesProjectiveObjects). $$$

Lean4

instance preservesProjectiveObjects_comp (F : C ⥤ D) (G : D ⥤ E) [F.PreservesProjectiveObjects]
    [G.PreservesProjectiveObjects] : (F ⋙ G).PreservesProjectiveObjects where
  projective_obj := G.projective_obj_of_projective ∘ F.projective_obj_of_projective

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