English
Exact limits can be pushed forward along initial functors: if F: J -> J' is initial and J' and J have limits in C and J has exact limits in C, then J' has exact limits in C.
Русский
Точные пределы можно проталкивать вдоль начальных функторов: если F: J → J' начальный и в C есть пределы для J' и J, и J имеет точные пределы в C, то J' имеет точные пределы в C.
LaTeX
$$$\\forall C\\, [\\text{HasFiniteColimits } C] \\Rightarrow \\operatorname{HasExactLimitsOfShape} J' C \\text{ from } \\operatorname{HasExactLimitsOfShape} J C \\text{ via initial } F.$$$
Lean4
/-- `HasExactLimitsOfShape` can be "pushed forward" along initial functors -/
theorem hasExactLimitsOfShape_of_initial [HasFiniteColimits C] {J J' : Type*} [Category J] [Category J'] (F : J ⥤ J')
[F.Initial] [HasLimitsOfShape J' C] [HasLimitsOfShape J C] [HasExactLimitsOfShape J C] : HasExactLimitsOfShape J' C
where
preservesFiniteColimits :=
letI : PreservesFiniteColimits ((whiskeringLeft J J' C).obj F) := ⟨fun _ ↦ inferInstance⟩
letI := comp_preservesFiniteColimits ((whiskeringLeft J J' C).obj F) lim
preservesFiniteColimits_of_natIso (Functor.Initial.limIso F)
