English
Let F be a diagram valued in D indexed by K, and let E be a cone over the diagram F composed with the diagram functor. For each morphism i arising from a covering W of an object X, there is a canonical morphism E.pt → (lim F).obj (op i.Y) obtained by lifting along the evaluation functor; this serves as a building block in constructing a diagram-limit lift.
Русский
Пусть F — диаграмма в D, индексированная по K, и пусть E — конус над диаграммой F, полученный через диаграммный функтор. Для каждого отображения i из покрытия W над объектом X существует канонический гомоморфизм E.pt → (lim F).obj (op i.Y), получаемый подъемом через оценочный функтор; он служит основой для построения подъема до предела диаграммы.
LaTeX
$$$ liftToDiagramLimitObjAux(F,E,i) : E.pt \\to (\\lim F).obj (op i.Y) $$$
Lean4
/-- Auxiliary definition for `liftToDiagramLimitObj`. -/
def liftToDiagramLimitObjAux {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) :
E.pt ⟶ (limit F).obj (op i.Y) :=
(isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op i.Y)) (limit.isLimit F)).lift
(coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation i E)
