English
An auxiliary definition to facilitate the proof that the diagram functor preserves limits: lift a cone over the diagram into a cone over the diagram of the limit, using a canonical isomorphism between diagrammatic forms.
Русский
Вспомогательное определение для упрощения доказательства того, что диаграммный функтор сохраняет пределы: поднимаем конус над диаграммой в конус над диаграммой предела, пользуясь канонической изоморфией форм диаграмм.
LaTeX
$$$ liftToDiagramLimitObj F E i := \\text{Multiequalizer.lift} ((unop W).index (limit F)) E.pt (liftToDiagramLimitObjAux F E) (by ... ) $$$
Lean4
/-- An auxiliary definition to be used in the proof of the fact that
`J.diagramFunctor D X` preserves limits. -/
abbrev liftToDiagramLimitObj {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)) :
E.pt ⟶ (J.diagram (limit F) X).obj W :=
Multiequalizer.lift ((unop W).index (limit F)) E.pt (liftToDiagramLimitObjAux F E)
(by
intro i
dsimp
ext k
dsimp
simp only [Category.assoc, NatTrans.naturality, liftToDiagramLimitObjAux_fac_assoc]
erw [Multiequalizer.condition]
rfl)
