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 (MonCat.of (Aut F)).

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

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

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem CategoryTheory.PreGaloisCategory.functorToAction_comp_forget₂_eq {C : Type u} [Category.{v, u} C] (F : Functor C FintypeCat) :
    (functorToAction F).comp (forget₂ (Action FintypeCat (MonCat.of (Aut F))) FintypeCat) = F
    source
    @[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
    source
    instance CategoryTheory.PreGaloisCategory.instMulActionAutαFintypeVFintypeCatObjActionOfFunctorFunctorToAction {C : Type u} [Category.{v, u} C] (F : Functor C FintypeCat) (X : C) :
    MulAction (Aut X) ↑((functorToAction F).obj X).V
    Equations
    source
    instance CategoryTheory.PreGaloisCategory.instIsPretransitiveAutαFintypeVFintypeCatObjActionOfFunctorFunctorToActionOfIsGalois {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
    source
    instance CategoryTheory.PreGaloisCategory.instFaithfulActionFintypeCatOfAutFunctorFunctorToAction {C : Type u} [Category.{v, u} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] :
    (functorToAction F).Faithful
    source
    instance CategoryTheory.PreGaloisCategory.instPreservesMonomorphismsActionFintypeCatOfAutFunctorFunctorToAction {C : Type u} [Category.{v, u} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] :
    (functorToAction F).PreservesMonomorphisms
    source
    instance CategoryTheory.PreGaloisCategory.instReflectsMonomorphismsActionFintypeCatOfAutFunctorFunctorToAction {C : Type u} [Category.{v, u} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] :
    (functorToAction F).ReflectsMonomorphisms
    source
    instance CategoryTheory.PreGaloisCategory.instReflectsIsomorphismsActionFintypeCatOfAutFunctorFunctorToAction {C : Type u} [Category.{v, u} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] :
    (functorToAction F).ReflectsIsomorphisms
    source
    instance CategoryTheory.PreGaloisCategory.instPreservesFiniteCoproductsActionFintypeCatOfAutFunctorFunctorToAction {C : Type u} [Category.{v, u} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] :
    Limits.PreservesFiniteCoproducts (functorToAction F)
    source
    instance CategoryTheory.PreGaloisCategory.instPreservesFiniteProductsActionFintypeCatOfAutFunctorFunctorToAction {C : Type u} [Category.{v, u} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] :
    Limits.PreservesFiniteProducts (functorToAction F)
    source
    instance CategoryTheory.PreGaloisCategory.instPreservesColimitsOfShapeActionFintypeCatOfAutFunctorSingleObjFunctorToActionOfFinite {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)
    source
    instance CategoryTheory.PreGaloisCategory.instPreservesIsConnectedActionFintypeCatOfAutFunctorFunctorToAction {C : Type u} [Category.{v, u} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] :
    PreservesIsConnected (functorToAction F)