English
An auxiliary construction showing how a diagram limit lift interacts with plus-objects; it preserves limits for the forgetful functor D.
Русский
Вспомогательная конструкция, показывающая как подъем предела диаграммы взаимодействует с объектами-плюс; сохраняет пределы для забывающего функторa D.
LaTeX
$$$ liftToPlusObjLimitObj F X S : S.pt \\to (J.plusObj (\\lim F)).obj (op X) $$$
Lean4
/-- An auxiliary definition to be used in the proof that `J.plusFunctor D` commutes
with finite limits. -/
def liftToPlusObjLimitObj {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))) : S.pt ⟶ (J.plusObj (limit F)).obj (op X) :=
let x := (J.Cover X)ᵒᵖ
let F' := F ⋙ J.diagramFunctor D X
let e := colimitLimitIso (F ⋙ J.diagramFunctor D X)
let t : J.diagram (limit F) X ≅ limit (F ⋙ J.diagramFunctor D X) :=
(isLimitOfPreserves (J.diagramFunctor D X) (limit.isLimit F)).conePointUniqueUpToIso (limit.isLimit _)
let p : (J.plusObj (limit F)).obj (op X) ≅ colimit (limit (F ⋙ J.diagramFunctor D X)) := HasColimit.isoOfNatIso t
let s : colimit (F ⋙ J.diagramFunctor D X).flip ≅ F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X) :=
NatIso.ofComponents (fun k => colimitObjIsoColimitCompEvaluation _ k)
(by
intro i j f
rw [← Iso.eq_comp_inv, Category.assoc, ← Iso.inv_comp_eq]
refine colimit.hom_ext (fun w => ?_)
dsimp [plusMap]
erw [colimit.ι_map_assoc, colimitObjIsoColimitCompEvaluation_ι_inv (F ⋙ J.diagramFunctor D X).flip w j,
colimitObjIsoColimitCompEvaluation_ι_inv_assoc (F ⋙ J.diagramFunctor D X).flip w i]
rw [← (colimit.ι (F ⋙ J.diagramFunctor D X).flip w).naturality]
rfl)
limit.lift _ S ≫ (HasLimit.isoOfNatIso s.symm).hom ≫ e.inv ≫ p.inv
