Documentation

Mathlib.CategoryTheory.Galois.Examples

Examples of Galois categories and fiber functors #

We show that for a group G the category of finite G-sets is a PreGaloisCategory and that the forgetful functor to FintypeCat is a FiberFunctor.

The connected finite G-sets are precisely the ones with transitive G-action.

source
noncomputable def CategoryTheory.FintypeCat.imageComplement {X : FintypeCat} {Y : FintypeCat} (f : X ⟶ Y) :
FintypeCat

Complement of the image of a morphism f : X ⟶ Y in FintypeCat.

Equations
Instances For
    source
    def CategoryTheory.FintypeCat.imageComplementIncl {X : FintypeCat} {Y : FintypeCat} (f : X ⟶ Y) :
    CategoryTheory.FintypeCat.imageComplement f ⟶ Y

    The inclusion from the complement of the image of f : X ⟶ Y into Y.

    Equations
    Instances For
      source
      noncomputable def CategoryTheory.FintypeCat.Action.imageComplement (G : Type u) [Group G] {X : Action FintypeCat (MonCat.of G)} {Y : Action FintypeCat (MonCat.of G)} (f : X ⟶ Y) :
      Action FintypeCat (MonCat.of G)

      Given f : X ⟶ Y for X Y : Action FintypeCat (MonCat.of G), the complement of the image of f has a natural G-action.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def CategoryTheory.FintypeCat.Action.imageComplementIncl (G : Type u) [Group G] {X : Action FintypeCat (MonCat.of G)} {Y : Action FintypeCat (MonCat.of G)} (f : X ⟶ Y) :
        CategoryTheory.FintypeCat.Action.imageComplement G f ⟶ Y

        The inclusion from the complement of the image of f : X ⟶ Y into Y.

        Equations
        Instances For
          source
          instance CategoryTheory.FintypeCat.instMonoActionFintypeCatInstCategoryFintypeCatOfToMonoidToDivInvMonoidInstCategoryActionImageComplementImageComplementIncl (G : Type u) [Group G] {X : Action FintypeCat (MonCat.of G)} {Y : Action FintypeCat (MonCat.of G)} (f : X ⟶ Y) :
          CategoryTheory.Mono (CategoryTheory.FintypeCat.Action.imageComplementIncl G f)
          Equations
          source
          instance CategoryTheory.FintypeCat.instHasColimitsOfShapeSingleObjCategoryToMonoidToDivInvMonoidFintypeCatInstCategoryFintypeCat (G : Type u) [Group G] [Finite G] :
          CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.SingleObj G) FintypeCat

          The category of finite sets has quotients by finite groups in arbitrary universes.

          Equations
          source
          noncomputable instance CategoryTheory.FintypeCat.instPreservesFiniteLimitsActionFintypeCatInstCategoryFintypeCatOfToMonoidToDivInvMonoidInstCategoryActionTypeTypesForgetInstConcreteCategoryActionInstCategoryActionConcreteCategoryFintype (G : Type u) [Group G] :
          CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget (Action FintypeCat (MonCat.of G)))
          Equations
          • One or more equations did not get rendered due to their size.
          source
          instance CategoryTheory.FintypeCat.instPreGaloisCategoryActionFintypeCatInstCategoryFintypeCatOfToMonoidToDivInvMonoidInstCategoryAction (G : Type u) [Group G] :
          CategoryTheory.PreGaloisCategory (Action FintypeCat (MonCat.of G))

          The category of finite G-sets is a PreGaloisCategory.

          Equations
          source
          noncomputable instance CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatInstCategoryFintypeCatOfToMonoidToDivInvMonoidInstCategoryActionInstPreGaloisCategoryActionFintypeCatInstCategoryFintypeCatOfToMonoidToDivInvMonoidInstCategoryActionForget (G : Type u) [Group G] :
          CategoryTheory.PreGaloisCategory.FiberFunctor (Action.forget FintypeCat (MonCat.of G))

          The forgetful functor from finite G-sets to sets is a FiberFunctor.

          Equations
          • One or more equations did not get rendered due to their size.
          source
          instance CategoryTheory.FintypeCat.instGaloisCategoryActionFintypeCatInstCategoryFintypeCatOfToMonoidToDivInvMonoidInstCategoryAction (G : Type u) [Group G] :
          CategoryTheory.GaloisCategory (Action FintypeCat (MonCat.of G))

          The category of finite G-sets is a GaloisCategory.

          Equations
          source
          theorem CategoryTheory.FintypeCat.Action.pretransitive_of_isConnected (G : Type u) [Group G] (X : Action FintypeCat (MonCat.of G)) [CategoryTheory.PreGaloisCategory.IsConnected X] :
          MulAction.IsPretransitive G ↑X.V

          The G-action on a connected finite G-set is transitive.

          source
          theorem CategoryTheory.FintypeCat.Action.isConnected_of_transitive (G : Type u) [Group G] (X : FintypeCat) [MulAction G ↑X] [MulAction.IsPretransitive G ↑X] [h : Nonempty ↑X] :
          CategoryTheory.PreGaloisCategory.IsConnected (Action.FintypeCat.ofMulAction G X)

          A nonempty G-set with transitive G-action is connected.

          source
          theorem CategoryTheory.FintypeCat.Action.isConnected_iff_transitive (G : Type u) [Group G] (X : Action FintypeCat (MonCat.of G)) [Nonempty ↑X.V] :
          CategoryTheory.PreGaloisCategory.IsConnected X ↔ MulAction.IsPretransitive G ↑X.V

          A nonempty finite G-set is connected if and only if the G-action is transitive.