hasLiftingProperty_of_isZero — Mathlib

English

If i: A → B is mono, I is injective, p: I → Z, and Z is zero object, then there is a lift from i to p.

Русский

Если i: A → B моно, I инъективен, p: I → Z и Z нулевой объект, то существует подъем (lifting) из i к p.

LaTeX

$$$$\\forall i:A\\to B\\;[\\text{Mono}(i)]\\;\\forall p:I\\to Z\\;[\\text{Injective}(I)]\\;[\\text{IsZero}(Z)]\\;\\Rightarrow \\; \\text{HasLiftingProperty}(i,p).$$$$

Lean4

theorem hasLiftingProperty_of_isZero {A B I Z : C} (i : A ⟶ B) [Mono i] [Injective I] (p : I ⟶ Z) (hZ : IsZero Z) :
    HasLiftingProperty i p where
  sq_hasLift {f g}
    sq :=
    ⟨⟨{   l := Injective.factorThru f i
          fac_right := hZ.eq_of_tgt _ _ }⟩⟩

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