hasLiftingProperty_iff — Mathlib

English

Let adj be an adjunction G ⊣ F. For arrows i: A → B and p: X → Y, the lifting property transfers along the adjunction: HasLiftingProperty (G.map i) p iff HasLiftingProperty i (F.map p).

Русский

Пусть adj — сопряжение G ⊣ F. Для стрел i: A → B и p: X → Y свойство подъёма переносится через сопряжение: HasLiftingProperty (G.map i) p эквивалентно HasLiftingProperty i (F.map p).

LaTeX

$$$$ HasLiftingProperty (G.map i) p \\iff HasLiftingProperty i (F.map p) $$$$

Lean4

theorem hasLiftingProperty_iff (adj : G ⊣ F) {A B : C} {X Y : D} (i : A ⟶ B) (p : X ⟶ Y) :
    HasLiftingProperty (G.map i) p ↔ HasLiftingProperty i (F.map p) :=
  by
  constructor <;> intro <;> constructor <;> intro f g sq
  · rw [← sq.left_adjoint_hasLift_iff adj]
    infer_instance
  · rw [← sq.right_adjoint_hasLift_iff adj]
    infer_instance

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