Stability properties of morphism properties on functor categories

Given W : MorphismProperty C and a category J, we study the stability properties of W.functorCategory J : MorphismProperty (J ⥤ C).

Under suitable assumptions, we also show that if monomorphisms in C are stable under transfinite compositions, then the same holds in the category J ⥤ C.

instance CategoryTheory.MorphismProperty.instIsStableUnderRetractsFunctorFunctorCategory {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) [W.IsStableUnderRetracts] (J : Type u'') [Category.{v'', u''} J] : (W.functorCategory J).IsStableUnderRetracts

theorem CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape.functorCategory {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {K : Type u'} [Category.{v', u'} K] (hW : W.IsStableUnderLimitsOfShape K) (J : Type u'') [Category.{v'', u''} J] [Limits.HasLimitsOfShape K C] : (W.functorCategory J).IsStableUnderLimitsOfShape K

theorem CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape.functorCategory {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {K : Type u'} [Category.{v', u'} K] (hW : W.IsStableUnderColimitsOfShape K) (J : Type u'') [Category.{v'', u''} J] [Limits.HasColimitsOfShape K C] : (W.functorCategory J).IsStableUnderColimitsOfShape K

instance CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeFunctorFunctorCategoryOfHasPullbacks {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} [W.IsStableUnderBaseChange] (J : Type u'') [Category.{v'', u''} J] [Limits.HasPullbacks C] : (W.functorCategory J).IsStableUnderBaseChange

instance CategoryTheory.MorphismProperty.instIsStableUnderCobaseChangeFunctorFunctorCategoryOfHasPushouts {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} [W.IsStableUnderCobaseChange] (J : Type u'') [Category.{v'', u''} J] [Limits.HasPushouts C] : (W.functorCategory J).IsStableUnderCobaseChange

instance CategoryTheory.MorphismProperty.instIsStableUnderTransfiniteCompositionOfShapeFunctorFunctorCategoryOfHasIterationOfShape {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} (K : Type u') [LinearOrder K] [SuccOrder K] [OrderBot K] [WellFoundedLT K] [W.IsStableUnderTransfiniteCompositionOfShape K] (J : Type u'') [Category.{v'', u''} J] [Limits.HasIterationOfShape K C] : (W.functorCategory J).IsStableUnderTransfiniteCompositionOfShape K

theorem CategoryTheory.MorphismProperty.functorCategory_isomorphisms {C : Type u} [Category.{v, u} C] (J : Type u'') [Category.{v'', u''} J] : (isomorphisms C).functorCategory J = isomorphisms (Functor J C)

theorem CategoryTheory.MorphismProperty.functorCategory_monomorphisms {C : Type u} [Category.{v, u} C] (J : Type u'') [Category.{v'', u''} J] [Limits.HasPullbacks C] : (monomorphisms C).functorCategory J = monomorphisms (Functor J C)

theorem CategoryTheory.MorphismProperty.functorCategory_epimorphisms {C : Type u} [Category.{v, u} C] (J : Type u'') [Category.{v'', u''} J] [Limits.HasPushouts C] : (epimorphisms C).functorCategory J = epimorphisms (Functor J C)

instance CategoryTheory.MorphismProperty.instIsStableUnderTransfiniteCompositionOfShapeFunctorMonomorphismsOfHasPullbacksOfHasIterationOfShape {C : Type u} [Category.{v, u} C] (K : Type u') [LinearOrder K] [SuccOrder K] [OrderBot K] [WellFoundedLT K] [(monomorphisms C).IsStableUnderTransfiniteCompositionOfShape K] [Limits.HasPullbacks C] (J : Type u'') [Category.{v'', u''} J] [Limits.HasIterationOfShape K C] : (monomorphisms (Functor J C)).IsStableUnderTransfiniteCompositionOfShape K