hasLiftingProperty — Mathlib

English

If there is a pushout s f and HasLiftingProperty f g', then the pushout inl has lifting with g'.

Русский

Если существует pushout s f и HasLiftingProperty f g', то pushout.inl имеет подъём для g'.

LaTeX

$$$$ HasLiftingProperty\\big(pushout.inl\\,s\\,f\\big)\\, g' $$$$

Lean4

theorem hasLiftingProperty (h : IsPullback s f g t) {X' Y' : C} (f' : X' ⟶ Y') [HasLiftingProperty f' g] :
    HasLiftingProperty f' f where
  sq_hasLift := fun {u v} sq ↦
    by
    have w : (u ≫ s) ≫ g = f' ≫ v ≫ t := by rw [Category.assoc, h.toCommSq.w, ← Category.assoc, ← Category.assoc, sq.w]
    exact
      ⟨h.lift (CommSq.mk w).lift v (by rw [CommSq.fac_right]),
        h.hom_ext (by rw [Category.assoc, h.lift_fst, CommSq.fac_left]) (by rw [Category.assoc, h.lift_snd, sq.w]),
        h.lift_snd _ _ _⟩

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