injective_iff_rlp_monomorphisms_zero

English

Under HasZeroMorphisms and HasZeroObject, Injective I is equivalent to RLP with the zero morphism 0 from I to 0.

Русский

При наличии нулевых морфизмов и нулевого объекта, инъективность I эквивалентна RLP по нулевому морфизму 0: I → 0.

LaTeX

$$$$\\text{Injective}(I) \\iff (\\text{MorphismProperty.monomorphisms}(C)).\\text{rlp}(0:I\\to 0).$$$$

Lean4

theorem injective_iff_rlp_monomorphisms_zero [HasZeroMorphisms C] [HasZeroObject C] (I : C) :
    Injective I ↔ (MorphismProperty.monomorphisms C).rlp (0 : I ⟶ 0) :=
  injective_iff_rlp_monomorphisms_of_isZero _ (isZero_zero C)

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