injective_iff_preservesEpimorphisms_yoneda_obj

English

If L ⊣ R with L preserving monos and J injective, then R maps J to an injective in the codomain; i.e., the right adjoint preserves injectives under suitable hypotheses.

Русский

Если L ⊣ R и L сохраняет моно-морфизмы, и J инъективен, тогда R(J) инъективен в целевой категории; т.к. правая смежная функтор сохраняет инъективность при подходящих условиях.

LaTeX

$$$$\text{Injective}(J) \Rightarrow \text{Injective}(\mathrm{R.obj}(J))\quad\text{for an adjunction } L \dashv R.$$$

Lean4

theorem injective_iff_preservesEpimorphisms_yoneda_obj (J : C) : Injective J ↔ (yoneda.obj J).PreservesEpimorphisms :=
  by
  rw [injective_iff_projective_op, Projective.projective_iff_preservesEpimorphisms_coyoneda_obj]
  exact Functor.preservesEpimorphisms.iso_iff (Coyoneda.objOpOp _)

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