English
If monomorphisms in C are stable under transfinite composition of shape K and C has pullbacks along with a suitable iteration shape K, then monomorphisms in the functor category J ⥤ C are stable under transfinite composition of shape K.
Русский
Если монофоморфизмы в C устойчивы к трансфинитной композиции формы K и в C есть растяжение по диагонали (pullbacks) и подходящая итерационная структура K, то монофоморфизмы в категориe функторов J ⥤ C устойчивы к трансфинитной композиции формы K.
LaTeX
$$$ [\text{HasPullbacks } C] \; \land \ (\mathrm{monomorphisms}\ C).\mathrm{IsStableUnderTransfiniteCompositionOfShape} K \;\Rightarrow \ (\mathrm{monomorphisms}\ (J \;⥤\; C)).\mathrm{IsStableUnderTransfiniteCompositionOfShape} K $$$
Lean4
instance (K : Type u') [LinearOrder K] [SuccOrder K] [OrderBot K] [WellFoundedLT K]
[(monomorphisms C).IsStableUnderTransfiniteCompositionOfShape K] [HasPullbacks C] (J : Type u'') [Category.{v''} J]
[HasIterationOfShape K C] : (monomorphisms (J ⥤ C)).IsStableUnderTransfiniteCompositionOfShape K :=
by
rw [← functorCategory_monomorphisms]
infer_instance
