English
Exact colimits can be pushed forward along final functors: if F: J -> J' is final and J', J have colimits in C and J has exact colimits in C, then J' has exact colimits in C.
Русский
Точные колимиты можно проталкивать вдоль финальных функторов: если F: J → J' является финальным, существуют колимиты в C для J и J', и J имеет точные колимиты в C, тогда и J' имеет точные колимиты в C.
LaTeX
$$$\\forall C\\, [\\text{HasFiniteLimits } C] \\Rightarrow \\operatorname{HasExactColimitsOfShape} J' C \\text{ given } F: J \\to J' \\text{ final and } [\\text{HasColimitsOfShape } J' C], [\\text{HasColimitsOfShape } J C], [\\text{HasExactColimitsOfShape } J C].$$$
Lean4
/-- `HasExactColimitsOfShape` can be "pushed forward" along final functors -/
theorem hasExactColimitsOfShape_of_final [HasFiniteLimits C] {J J' : Type*} [Category J] [Category J'] (F : J ⥤ J')
[F.Final] [HasColimitsOfShape J' C] [HasColimitsOfShape J C] [HasExactColimitsOfShape J C] :
HasExactColimitsOfShape J' C where
preservesFiniteLimits :=
letI : PreservesFiniteLimits ((whiskeringLeft J J' C).obj F) := ⟨fun _ ↦ inferInstance⟩
letI := comp_preservesFiniteLimits ((whiskeringLeft J J' C).obj F) colim
preservesFiniteLimits_of_natIso (Functor.Final.colimIso F)
