hasLiftingProperty — Mathlib

English

If s ⟶ f is a pushout and there exists g' with HasLiftingProperty f g', then there is a lifting for g with g'.

Русский

Если s⟶f образует pushout и существует g' с HasLiftingProperty f g', то существует подъём для g по отношению к g'.

LaTeX

$$$$ h:\\mathrm{IsPushout}(s,f,g,t) \\Rightarrow \\forall g'\\;[HasLiftingProperty f\\, g'] \\Rightarrow HasLiftingProperty g\\, g' $$$$

Lean4

theorem hasLiftingProperty (h : IsPushout s f g t) {Z' W' : C} (g' : Z' ⟶ W') [HasLiftingProperty f g'] :
    HasLiftingProperty g g' where
  sq_hasLift := fun {u v} sq ↦
    by
    have w : (s ≫ u) ≫ g' = f ≫ (t ≫ v) := by rw [← Category.assoc, ← h.w, Category.assoc, Category.assoc, sq.w]
    exact
      ⟨h.desc u (CommSq.mk w).lift (by rw [CommSq.fac_left]), h.inl_desc ..,
        h.hom_ext (by rw [h.inl_desc_assoc, sq.w]) (by rw [h.inr_desc_assoc, CommSq.fac_right])⟩

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