English
A formal abbreviation describing the lift from a cone to the diagram limit object using a universal property construction with the multiequalizer.
Русский
Формальное сокращение, описывающее подъем конуса к объекту диаграммного предела посредством универсального свойства и мультиравнителя.
LaTeX
$$$ liftToDiagramLimitObj F E : Cone (F \\circ J.diagramFunctor D X) \\to (\\lim F) \\text{ (at) } X $$$
Lean4
instance preservesLimit_diagramFunctor (X : C) (K : Type s) [SmallCategory K] [HasLimitsOfShape K D] (F : K ⥤ Cᵒᵖ ⥤ D) :
PreservesLimit F (J.diagramFunctor D X) :=
preservesLimit_of_evaluation _ _ fun W =>
preservesLimit_of_preserves_limit_cone (limit.isLimit _)
{ lift := fun E => liftToDiagramLimitObj.{_, t, w, v, u} F E
fac := by
intro E k
dsimp [diagramNatTrans]
refine Multiequalizer.hom_ext _ _ _ (fun a => ?_)
simp only [Multiequalizer.lift_ι, Multiequalizer.lift_ι_assoc, Category.assoc, liftToDiagramLimitObjAux_fac]
uniq := by
intro E m hm
refine Multiequalizer.hom_ext _ _ _ (fun a => limit_obj_ext (fun j => ?_))
dsimp [liftToDiagramLimitObj]
rw [Multiequalizer.lift_ι, Category.assoc, liftToDiagramLimitObjAux_fac, ← hm, Category.assoc]
dsimp
rw [limit.lift_π]
dsimp }
