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.

Equations

• CategoryTheory.FintypeCat.imageComplement f = FintypeCat.of ↑(Set.range f)ᶜ

def CategoryTheory.FintypeCat.imageComplementIncl {X 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

• CategoryTheory.FintypeCat.imageComplementIncl f = Subtype.val

noncomputable def CategoryTheory.FintypeCat.Action.imageComplement (G : Type u) [Group G] {X 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.

def CategoryTheory.FintypeCat.Action.imageComplementIncl (G : Type u) [Group G] {X 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

• CategoryTheory.FintypeCat.Action.imageComplementIncl G f = { hom := CategoryTheory.FintypeCat.imageComplementIncl f.hom, comm := ⋯ }

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

Equations

• ⋯ = ⋯

instance CategoryTheory.FintypeCat.instHasColimitsOfShapeSingleObjFintypeCatOfFinite (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

• ⋯ = ⋯

noncomputable instance CategoryTheory.FintypeCat.instPreservesFiniteLimitsActionFintypeCatOfForget (G : Type u) [Group G] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget (Action FintypeCat (MonCat.of G)))

Equations

• ⋯ = ⋯

instance CategoryTheory.FintypeCat.instPreGaloisCategoryActionFintypeCatOf (G : Type u) [Group G] : CategoryTheory.PreGaloisCategory (Action FintypeCat (MonCat.of G))

The category of finite G-sets is a PreGaloisCategory.

Equations

• ⋯ = ⋯

noncomputable instance CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatOfForget (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

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

instance CategoryTheory.FintypeCat.instGaloisCategoryActionFintypeCatOf (G : Type u) [Group G] : CategoryTheory.GaloisCategory (Action FintypeCat (MonCat.of G))

The category of finite G-sets is a GaloisCategory.

Equations

• ⋯ = ⋯

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.

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.

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.

noncomputable def CategoryTheory.FintypeCat.isoQuotientStabilizerOfIsConnected {G : Type u} [Group G] (X : Action FintypeCat (MonCat.of G)) [CategoryTheory.PreGaloisCategory.IsConnected X] (x : ↑X.V) [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.

Equations

• One or more equations did not get rendered due to their size.