Full subcategories of Galois categories

Given a Galois category C, we introduce a typeclass P.IsGaloisSubcategory which allows to show that P.FullSubcategory is also a Galois category.

class CategoryTheory.ObjectProperty.IsGaloisSubcategory {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : Prop

If P is a property of objects in a Galois category, the typeclass IsGaloisSubcategory expresses stability properties which imply that the fullsubcategory given by P is also a Galois category.

• isClosedUnderLimitsOfShape_discrete_pEmpty : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})

  If C has a terminal object,P is sat.

• isClosedUnderLimitsOfShape_walkingCospan : P.IsClosedUnderLimitsOfShape Limits.WalkingCospan

  P is stable under pullbacks.

• isClosedUnderColimitsOfShape_discrete (ι : Type) [Finite ι] : P.IsClosedUnderColimitsOfShape (Discrete ι)

  P is stable under finite coproducs.

• isClosedUnderColimitsOfShape_singleObj (G : Type v) [Group G] [Finite G] : P.IsClosedUnderColimitsOfShape (SingleObj G)

  P is stable under quotients by finite groups.

• isClosedUnderSubobjects : P.IsClosedUnderSubobjects
• preservesEpimorphisms : P.ι.PreservesEpimorphisms

instance CategoryTheory.PreGaloisCategory.instFullSubcategoryOfMonoCoprodOfIsGaloisSubcategory {C : Type u} [Category.{v, u} C] [PreGaloisCategory C] [Limits.MonoCoprod C] (P : ObjectProperty C) [P.IsGaloisSubcategory] : PreGaloisCategory P.FullSubcategory

instance CategoryTheory.PreGaloisCategory.instFiberFunctorFullSubcategoryCompFintypeCatι {C : Type u} [Category.{v, u} C] [PreGaloisCategory C] [Limits.MonoCoprod C] (P : ObjectProperty C) [P.IsGaloisSubcategory] (F : Functor C FintypeCat) [FiberFunctor F] : FiberFunctor (P.ι.comp F)

instance CategoryTheory.GaloisCategory.instFullSubcategoryOfIsGaloisSubcategory {C : Type u} [Category.{v, u} C] [GaloisCategory C] (P : ObjectProperty C) [P.IsGaloisSubcategory] : GaloisCategory P.FullSubcategory