Documentation

Mathlib.CategoryTheory.Galois.Action

Induced functor to finite `Aut F`-sets #

Any (fiber) functor F : C ⥤ FintypeCat factors via the forgetful functor from finite Aut F-sets to finite sets. In this file we collect basic properties of the induced functor H : C ⥤ Action FintypeCat (Aut F).

See Mathlib.CategoryTheory.Galois.Full for the proof that H is (faithfully) full.

def CategoryTheory.PreGaloisCategory.functorToAction {C : Type u} [Category.{v, u} C] (F : Functor C FintypeCat) :

Functor C (Action FintypeCat (Aut F))

Any (fiber) functor F : C ⥤ FintypeCat naturally factors via the forgetful functor from Action FintypeCat (Aut F) to FintypeCat.

Equations

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

Instances For

theorem CategoryTheory.PreGaloisCategory.functorToAction_comp_forget₂_eq {C : Type u} [Category.{v, u} C] (F : Functor C FintypeCat) :

(functorToAction F).comp (forget₂ (Action FintypeCat (Aut F)) FintypeCat) = F

@[simp]

theorem CategoryTheory.PreGaloisCategory.functorToAction_map {C : Type u} [Category.{v, u} C] (F : Functor C FintypeCat) {X Y : C} (f : X ⟶ Y) :

((functorToAction F).map f).hom = F.map f

instance CategoryTheory.PreGaloisCategory.instMulActionAutCarrierVFintypeCatFunctorObjActionFunctorToAction {C : Type u} [Category.{v, u} C] (F : Functor C FintypeCat) (X : C) :

MulAction (Aut X) ((functorToAction F).obj X).V.carrier

Equations

CategoryTheory.PreGaloisCategory.instMulActionAutCarrierVFintypeCatFunctorObjActionFunctorToAction F X = inferInstanceAs (MulAction (CategoryTheory.Aut X) (F.obj X).carrier)

instance CategoryTheory.PreGaloisCategory.instIsPretransitiveAutCarrierVFintypeCatFunctorObjActionFunctorToActionOfIsGalois {C : Type u} [Category.{v, u} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] (X : C) [IsGalois X] :

MulAction.IsPretransitive (Aut X) ((functorToAction F).obj X).V.carrier

instance CategoryTheory.PreGaloisCategory.instFaithfulActionFintypeCatAutFunctorFunctorToAction {C : Type u} [Category.{v, u} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] :

(functorToAction F).Faithful

instance CategoryTheory.PreGaloisCategory.instPreservesMonomorphismsActionFintypeCatAutFunctorFunctorToAction {C : Type u} [Category.{v, u} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] :

(functorToAction F).PreservesMonomorphisms

instance CategoryTheory.PreGaloisCategory.instReflectsMonomorphismsActionFintypeCatAutFunctorFunctorToAction {C : Type u} [Category.{v, u} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] :

(functorToAction F).ReflectsMonomorphisms

instance CategoryTheory.PreGaloisCategory.instReflectsIsomorphismsActionFintypeCatAutFunctorFunctorToAction {C : Type u} [Category.{v, u} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] :

(functorToAction F).ReflectsIsomorphisms

instance CategoryTheory.PreGaloisCategory.instPreservesFiniteCoproductsActionFintypeCatAutFunctorFunctorToAction {C : Type u} [Category.{v, u} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] :

Limits.PreservesFiniteCoproducts (functorToAction F)

instance CategoryTheory.PreGaloisCategory.instPreservesFiniteProductsActionFintypeCatAutFunctorFunctorToAction {C : Type u} [Category.{v, u} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] :

Limits.PreservesFiniteProducts (functorToAction F)

instance CategoryTheory.PreGaloisCategory.instPreservesColimitsOfShapeActionFintypeCatAutFunctorSingleObjFunctorToActionOfFinite {C : Type u} [Category.{v, u} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] (G : Type u_1) [Group G] [Finite G] :

Limits.PreservesColimitsOfShape (SingleObj G) (functorToAction F)

instance CategoryTheory.PreGaloisCategory.instPreservesIsConnectedActionFintypeCatAutFunctorFunctorToAction {C : Type u} [Category.{v, u} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] :

PreservesIsConnected (functorToAction F)