English
For any F, E, i, and k, the auxiliary lift commutes with the k-th limit projection: lifting then projecting equals projecting then lifting through the multiequalizer.
Русский
Для любых F, E, i и k выполнено, что вспомогательный подъем коммутирует с k-ой проекцией предела: подъем затем проекция равны проекции затем подъем через мультиравнитель.
LaTeX
$$$ liftToDiagramLimitObjAux(F,E,i) \\;\\gg\\; (limit.\\pi F k).app (op i.Y) = E.\\pi.app k \\;\\gg\\; Multiequalizer.ι ((unop W).index (F.obj k)) i $$$
Lean4
@[reassoc (attr := simp)]
theorem liftToDiagramLimitObjAux_fac {X : C} {K : Type s} [SmallCategory K] [HasLimitsOfShape K D] {W : (J.Cover X)ᵒᵖ}
(F : K ⥤ Cᵒᵖ ⥤ D) (E : Cone (F ⋙ J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W)) (i : (unop W).Arrow)
(k : K) :
liftToDiagramLimitObjAux F E i ≫ (limit.π F k).app (op i.Y) =
E.π.app k ≫ Multiequalizer.ι ((unop W).index (F.obj k)) i :=
IsLimit.fac _ _ _
