English
The plus-object lift is compatible with limits and preserves certain shapes; it yields a limit for the opposite forgetful category.
Русский
Подъем объекта-плюса совместим с пределами и сохраняет определенные формы; даёт предел в противоположном забывающем категории контексте.
LaTeX
$$$ liftToPlusObjLimitObj (F) (X) : \\text{HasLimit } (F \\circ (J.diagramFunctor D X)) $$$
Lean4
theorem liftToPlusObjLimitObj_fac {K : Type s} [SmallCategory K] [FinCategory K] [HasLimitsOfShape K D]
[PreservesLimitsOfShape K (forget D)] [ReflectsLimitsOfShape K (forget D)] (F : K ⥤ Cᵒᵖ ⥤ D) (X : C)
(S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))) (k) :
liftToPlusObjLimitObj F X S ≫ (J.plusMap (limit.π F k)).app (op X) = S.π.app k :=
by
dsimp only [liftToPlusObjLimitObj]
rw [← (limit.isLimit (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))).fac S k, Category.assoc]
congr 1
dsimp
rw [Category.assoc, Category.assoc, ← Iso.eq_inv_comp, Iso.inv_comp_eq, Iso.inv_comp_eq]
refine colimit.hom_ext (fun j => ?_)
dsimp [plusMap]
simp only [HasColimit.isoOfNatIso_ι_hom_assoc, ι_colimMap]
dsimp [IsLimit.conePointUniqueUpToIso, HasLimit.isoOfNatIso, IsLimit.map]
rw [limit.lift_π]
dsimp
rw [ι_colimitLimitIso_limit_π_assoc]
simp_rw [← Category.assoc, ← NatTrans.comp_app]
rw [limit.lift_π, Category.assoc]
congr 1
rw [← Iso.comp_inv_eq]
erw [colimit.ι_desc]
rfl
