hasLiftingProperty_iff — Mathlib

English

In the Arrow category, HasLiftingProperty i p is equivalent to the existence, for every φ between Arrow.mk i and Arrow.mk p, of a LiftStruct.

Русский

В категории стрелок условие подъёма эквивалентно существованию подъёмной структуры для каждого φ между Arrow.mk i и Arrow.mk p.

LaTeX

$$$$ HasLiftingProperty\, i\, p \\iff \\forall \\phi:\\mathrm{Arrow.mk}\\, i \\to \\mathrm{Arrow.mk}\\, p, \\operatorname{Nonempty}(\\mathrm{LiftStruct}(\\phi)) $$$$

Lean4

theorem hasLiftingProperty_iff {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) :
    HasLiftingProperty i p ↔ ∀ (φ : Arrow.mk i ⟶ Arrow.mk p), Nonempty (LiftStruct φ) :=
  by
  constructor
  · intro _ φ
    have sq : CommSq φ.left i p φ.right := CommSq.mk φ.w
    exact ⟨{ l := sq.lift }⟩
  · intro h
    exact ⟨fun {f g} sq ↦ ⟨h (Arrow.homMk f g sq.w)⟩⟩

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