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.

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

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

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

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

noncomputable def CategoryTheory.FintypeCat.Action.imageComplement (G : Type u) [Group G] {X Y : Action FintypeCat G} (f : X ⟶ Y) : Action FintypeCat G

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

noncomputable def CategoryTheory.FintypeCat.Action.imageComplementIncl (G : Type u) [Group G] {X Y : Action FintypeCat G} (f : X ⟶ Y) : imageComplement G f ⟶ Y

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

instance CategoryTheory.FintypeCat.instMonoActionFintypeCatImageComplementIncl (G : Type u) [Group G] {X Y : Action FintypeCat G} (f : X ⟶ Y) : Mono (Action.imageComplementIncl G f)

instance CategoryTheory.FintypeCat.instHasColimitsOfShapeSingleObjFintypeCatOfFinite (G : Type u) [Group G] [Finite G] : Limits.HasColimitsOfShape (SingleObj G) FintypeCat

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

instance CategoryTheory.FintypeCat.instPreservesFiniteLimitsActionFintypeCatForget (G : Type u) [Group G] : Limits.PreservesFiniteLimits (forget (Action FintypeCat G))

instance CategoryTheory.FintypeCat.instPreGaloisCategoryActionFintypeCat (G : Type u) [Group G] : PreGaloisCategory (Action FintypeCat G)

The category of finite G-sets is a PreGaloisCategory.

instance CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget (G : Type u) [Group G] : PreGaloisCategory.FiberFunctor (Action.forget FintypeCat G)

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

instance CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂ (G : Type u) [Group G] : PreGaloisCategory.FiberFunctor (forget₂ (Action FintypeCat G) FintypeCat)

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

instance CategoryTheory.FintypeCat.instGaloisCategoryActionFintypeCat (G : Type u) [Group G] : GaloisCategory (Action FintypeCat G)

The category of finite G-sets is a GaloisCategory.

theorem CategoryTheory.FintypeCat.Action.pretransitive_of_isConnected (G : Type u) [Group G] (X : Action FintypeCat G) [PreGaloisCategory.IsConnected X] : MulAction.IsPretransitive G X.V.carrier

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

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

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

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

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

noncomputable def CategoryTheory.FintypeCat.isoQuotientStabilizerOfIsConnected {G : Type u} [Group G] (X : Action FintypeCat G) [PreGaloisCategory.IsConnected X] (x : X.V.carrier) [Fintype (G ⧸ MulAction.stabilizer G x)] : X ≅ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ MulAction.stabilizer G x))

If X is a connected G-set and x is an element of X, X is isomorphic to the quotient of G by the stabilizer of x as G-sets.