injective_iff_rlp_monomorphisms_of_isZero

English

For HasZeroMorphisms and HasZeroObject, Injective I is equivalent to I having the right lifting property with the unique map to a zero object.

Русский

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

LaTeX

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

Lean4

theorem injective_iff_rlp_monomorphisms_of_isZero [HasZeroMorphisms C] {I Z : C} (p : I ⟶ Z) (hZ : IsZero Z) :
    Injective I ↔ (MorphismProperty.monomorphisms C).rlp p :=
  by
  obtain rfl := hZ.eq_of_tgt p 0
  constructor
  · intro _ A B i (_ : Mono i)
    exact Injective.hasLiftingProperty_of_isZero i 0 hZ
  · intro h
    constructor
    intro A B f i hi
    have := h _ hi
    have sq : CommSq f i (0 : I ⟶ Z) 0 := ⟨by simp⟩
    exact ⟨sq.lift, by simp⟩

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