Characterization of injective objects in terms of lifting properties

An object I is injective iff the morphism I ⟶ 0 has the right lifting property with respect to monomorphisms, injective_iff_rlp_monomorphisms_zero.

theorem CategoryTheory.Injective.hasLiftingProperty_of_isZero {C : Type u} [Category.{v, u} C] {A B I Z : C} (i : A ⟶ B) [Mono i] [Injective I] (p : I ⟶ Z) (hZ : Limits.IsZero Z) : HasLiftingProperty i p

instance CategoryTheory.Injective.instHasLiftingPropertyOfMono {C : Type u} [Category.{v, u} C] {A B I : C} (i : A ⟶ B) [Mono i] [Injective I] [Limits.HasZeroObject C] (p : I ⟶ 0) : HasLiftingProperty i p

theorem CategoryTheory.injective_iff_rlp_monomorphisms_of_isZero {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {I Z : C} (p : I ⟶ Z) (hZ : Limits.IsZero Z) : Injective I ↔ (MorphismProperty.monomorphisms C).rlp p

theorem CategoryTheory.injective_iff_rlp_monomorphisms_zero {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] (I : C) : Injective I ↔ (MorphismProperty.monomorphisms C).rlp 0