instHasLiftingPropertyMap_1 — Mathlib

English

In the pushoutObjObj construction, the right and left inclusions correspond under flipping the pushout: the flip of ι equals ι.

Русский

В конструировании PushoutObjObj равенство между правой и левой инклюзиями сохраняется при развороте/перекрестном отображении: ι_flip = ι.

LaTeX

$$$\\text{sq.flip.ι} = \\text{sq.ι}.$$$

Lean4

instance {J : Type*} {A B : J → C} [HasCoproduct A] [HasCoproduct B] (f : (j : J) → A j ⟶ B j) {X Y : C} (p : X ⟶ Y)
    [∀ j, HasLiftingProperty (f j) p] : HasLiftingProperty (Limits.Sigma.map f) p where
  sq_hasLift {t b}
    sq := by
    have sq' (j : J) : CommSq (Sigma.ι _ j ≫ t) (f j) p (Sigma.ι _ j ≫ b) := ⟨by simp [sq.w]⟩
    exact ⟨⟨{ l := Sigma.desc (fun j ↦ (sq' j).lift) }⟩⟩

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