injective_obj — Mathlib

English

If F preserves injective objects, then F.obj X is injective whenever X is injectable in the domain category.

Русский

Если F сохраняет инъективные объекты, то F(X) инъективен, когда X инъективен в исходной категории.

LaTeX

$$$$\\forall F\\;[F\\text{PreservesInjectiveObjects}]\\;\\forall X\\; (\\text{Injective}(X) \\Rightarrow \\text{Injective}(F(X))).$$$$

Lean4

/-- See `Functor.injective_obj_of_injective` for a variant taking `Injective X` as an explicit
argument. -/
instance injective_obj (F : C ⥤ D) [F.PreservesInjectiveObjects] (X : C) [Injective X] : Injective (F.obj X) :=
  Functor.PreservesInjectiveObjects.injective_obj inferInstance

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