English
The object πObj I κ f has the right lifting property with respect to I: that is, for any commutative square with left map in I, a diagonal filler exists for πObj.
Русский
Объект πObj I κ f обладает правым свойством подстановки по отношению к I: существует диагональный заполнитель для любой коммутативной квадратуры.
LaTeX
$$$I\!\!\!rlp\ (\piObj I κ f)$$$
Lean4
theorem hasRightLiftingProperty_πObj {A B : C} (i : A ⟶ B) (hi : I i) (f : X ⟶ Y) : HasLiftingProperty i (πObj I κ f) :=
⟨by
haveI := hasColimitsOfShape_discrete I κ
haveI := hasPushouts I κ
haveI := preservesColimit I κ i hi _ (relativeCellComplexιObj I κ f)
intro g b sq
obtain ⟨j, t, ht⟩ :=
Types.jointly_surjective _
(isColimitOfPreserves (coyoneda.obj (Opposite.op A)) (relativeCellComplexιObj I κ f).isColimit) g
dsimp at g b sq t ht
obtain ⟨l, hl₁, hl₂⟩ :=
ιFunctorObj_extension' I.homFamily ((relativeCellComplexιObj I κ f).incl.app j ≫ πObj I κ f)
((relativeCellComplexιObj I κ f).F.map (homOfLE (Order.le_succ j)))
((relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫ πObj I κ f) (by simp) (Iso.refl _)
(iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).symm (relativeCellComplexιObjFObjSuccIso I κ f j)
(by dsimp; rw [ιFunctorObj_eq, id_comp]) (by dsimp; rw [πFunctorObj_eq, assoc, Iso.hom_inv_id_assoc]) (i :=
⟨i, hi⟩) t b (by rw [reassoc_of% ht, sq.w]; dsimp)
dsimp at hl₁
exact ⟨⟨{
l := l ≫ (relativeCellComplexιObj I κ f).incl.app (Order.succ j)
fac_left := by simp [reassoc_of% hl₁, ← ht]
fac_right := by rw [assoc, hl₂] }⟩⟩⟩
