English
If W is stable under cobase change, then the functor category inherits stability under cobase change.
Русский
Если W устойчиво к кобазовым изменениям, то категория-функтор наследует устойчивость к кобазовым изменениям.
LaTeX
$$$W.IsStableUnderCobaseChange ⇒ (W.functorCategory J).IsStableUnderCobaseChange$$$
Lean4
instance (K : Type u') [LinearOrder K] [SuccOrder K] [OrderBot K] [WellFoundedLT K]
[W.IsStableUnderTransfiniteCompositionOfShape K] (J : Type u'') [Category.{v''} J] [HasIterationOfShape K C] :
(W.functorCategory J).IsStableUnderTransfiniteCompositionOfShape K where
le := by
rintro X Y f ⟨hf⟩ j
have : W.functorCategory J ≤ W.inverseImage ((evaluation _ _).obj j) := fun _ _ _ h ↦ h _
exact W.transfiniteCompositionsOfShape_le K _ ⟨(hf.ofLE this).map⟩
