injective_obj_of_injective — Mathlib

English

Variant: If X is injective, then F.obj X is injective for any F with preserving injectives.

Русский

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

LaTeX

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

Lean4

/-- See `Functor.injective_obj` for a variant taking `Injective X` as a typeclass argument. -/
theorem injective_obj_of_injective (F : C ⥤ D) [F.PreservesInjectiveObjects] {X : C} (h : Injective X) :
    Injective (F.obj X) :=
  Functor.PreservesInjectiveObjects.injective_obj h

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