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.lean for the proof that H is (faithfully) full.

source
def CategoryTheory.PreGaloisCategory.functorToAction {C : Type u_1} [Category.{v_1, u_1} 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
    source
    theorem CategoryTheory.PreGaloisCategory.functorToAction_comp_forget₂_eq {C : Type u_1} [Category.{v_1, u_1} C] (F : Functor C FintypeCat) :
    (functorToAction F).comp (forget₂ (Action FintypeCat (Aut F)) FintypeCat) = F
    source
    @[simp]
    theorem CategoryTheory.PreGaloisCategory.functorToAction_map {C : Type u_1} [Category.{v_1, u_1} C] (F : Functor C FintypeCat) {X Y : C} (f : X ⟶ Y) :
    ((functorToAction F).map f).hom = F.map f
    source
    @[instance_reducible]
    instance CategoryTheory.PreGaloisCategory.instMulActionAutObjFiniteVFintypeCatFunctorObjActionFunctorToAction {C : Type u_1} [Category.{v_1, u_1} C] (F : Functor C FintypeCat) (X : C) :
    MulAction (Aut X) ((functorToAction F).obj X).V.obj
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance CategoryTheory.PreGaloisCategory.instIsPretransitiveAutObjFiniteVFintypeCatFunctorObjActionFunctorToActionOfIsGalois {C : Type u_1} [Category.{v_1, u_1} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] (X : C) [IsGalois X] :
    MulAction.IsPretransitive (Aut X) ((functorToAction F).obj X).V.obj
    source
    instance CategoryTheory.PreGaloisCategory.instFaithfulActionFintypeCatAutFunctorFunctorToAction {C : Type u_1} [Category.{v_1, u_1} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] :
    (functorToAction F).Faithful
    source
    instance CategoryTheory.PreGaloisCategory.instPreservesMonomorphismsActionFintypeCatAutFunctorFunctorToAction {C : Type u_1} [Category.{v_1, u_1} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] :
    (functorToAction F).PreservesMonomorphisms
    source
    instance CategoryTheory.PreGaloisCategory.instReflectsMonomorphismsActionFintypeCatAutFunctorFunctorToAction {C : Type u_1} [Category.{v_1, u_1} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] :
    (functorToAction F).ReflectsMonomorphisms
    source
    instance CategoryTheory.PreGaloisCategory.instReflectsIsomorphismsActionFintypeCatAutFunctorFunctorToAction {C : Type u_1} [Category.{v_1, u_1} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] :
    (functorToAction F).ReflectsIsomorphisms
    source
    instance CategoryTheory.PreGaloisCategory.instPreservesFiniteCoproductsActionFintypeCatAutFunctorFunctorToAction {C : Type u_1} [Category.{v_1, u_1} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] :
    Limits.PreservesFiniteCoproducts (functorToAction F)
    source
    instance CategoryTheory.PreGaloisCategory.instPreservesFiniteProductsActionFintypeCatAutFunctorFunctorToAction {C : Type u_1} [Category.{v_1, u_1} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] :
    Limits.PreservesFiniteProducts (functorToAction F)
    source
    instance CategoryTheory.PreGaloisCategory.instPreservesColimitsOfShapeActionFintypeCatAutFunctorSingleObjFunctorToActionOfFinite {C : Type u_1} [Category.{v_1, u_1} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] (G : Type u_2) [Group G] [Finite G] :
    Limits.PreservesColimitsOfShape (SingleObj G) (functorToAction F)
    source
    instance CategoryTheory.PreGaloisCategory.instPreservesIsConnectedActionFintypeCatAutFunctorFunctorToAction {C : Type u_1} [Category.{v_1, u_1} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] :
    PreservesIsConnected (functorToAction F)