preservesInjectiveObjects_comp — Mathlib

English

If F and G preserve injective objects, then their composition F ⋙ G preserves injective objects.

Русский

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

LaTeX

$$$$\\forall F\\;\\forall G\\;[F\\text{PreservesInjectiveObjects}] [G\\text{PreservesInjectiveObjects}]\\; (F \\circ G)\\text{PreservesInjectiveObjects}. $$$$

Lean4

instance preservesInjectiveObjects_comp (F : C ⥤ D) (G : D ⥤ E) [F.PreservesInjectiveObjects]
    [G.PreservesInjectiveObjects] : (F ⋙ G).PreservesInjectiveObjects where
  injective_obj := G.injective_obj_of_injective ∘ F.injective_obj_of_injective

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