English
The functor J.plusFunctor D preserves limits of shape K whenever forgetful functor preserves limits and K is finite/Cat-sized with small shape conditions.
Русский
Функтор J.plusFunctor D сохраняет пределы формы K при условии, что забывающий функтор сохраняет пределы и форма K удовлетворяет ограничениям малости.
LaTeX
$$$ \\text{PreservesLimitsOfShape K (J.plusFunctor D)} $$$
Lean4
instance preservesLimitsOfShape_plusFunctor (K : Type t) [SmallCategory K] [FinCategory K] [HasLimitsOfShape K D]
[PreservesLimitsOfShape K (forget D)] [ReflectsLimitsOfShape K (forget D)] :
PreservesLimitsOfShape K (J.plusFunctor D) := by
constructor; intro F; apply preservesLimit_of_evaluation; intro X
apply preservesLimit_of_preserves_limit_cone (limit.isLimit F)
refine ⟨fun S => liftToPlusObjLimitObj F X.unop S, ?_, ?_⟩
· intro S k
apply liftToPlusObjLimitObj_fac
· intro S m hm
dsimp [liftToPlusObjLimitObj]
simp_rw [← Category.assoc, Iso.eq_comp_inv, ← Iso.comp_inv_eq]
refine limit.hom_ext (fun k => ?_)
simp only [limit.lift_π, Category.assoc, ← hm]
congr 1
refine colimit.hom_ext (fun k => ?_)
dsimp [plusMap, plusObj]
erw [colimit.ι_map, colimit.ι_desc_assoc, limit.lift_π]
conv_lhs => dsimp
simp only [Category.assoc]
rw [ι_colimitLimitIso_limit_π_assoc]
simp only [colimitObjIsoColimitCompEvaluation_ι_app_hom]
conv_lhs => dsimp [IsLimit.conePointUniqueUpToIso]
rw [← Category.assoc, ← NatTrans.comp_app, limit.lift_π]
rfl
