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} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C FintypeCat) :
CategoryTheory.Functor C (Action FintypeCat (MonCat.of (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C FintypeCat) :
    (CategoryTheory.PreGaloisCategory.functorToAction F).comp (CategoryTheory.forget₂ (Action FintypeCat (MonCat.of (CategoryTheory.Aut F))) FintypeCat) = F
    source
    @[simp]
    theorem CategoryTheory.PreGaloisCategory.functorToAction_map {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C FintypeCat) {X Y : C} (f : X ⟶ Y) :
    ((CategoryTheory.PreGaloisCategory.functorToAction F).map f).hom = F.map f
    source
    instance CategoryTheory.PreGaloisCategory.instMulActionAutαFintypeVFintypeCatObjActionOfFunctorFunctorToAction {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C FintypeCat) (X : C) :
    MulAction (CategoryTheory.Aut X) ↑((CategoryTheory.PreGaloisCategory.functorToAction F).obj X).V
    Equations
    source
    instance CategoryTheory.PreGaloisCategory.instIsPretransitiveAutαFintypeVFintypeCatObjActionOfFunctorFunctorToActionOfIsGalois {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) [CategoryTheory.PreGaloisCategory.IsGalois X] :
    MulAction.IsPretransitive (CategoryTheory.Aut X) ↑((CategoryTheory.PreGaloisCategory.functorToAction F).obj X).V
    Equations
    • ⋯ = ⋯
    source
    instance CategoryTheory.PreGaloisCategory.instFaithfulActionFintypeCatOfAutFunctorFunctorToAction {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] :
    (CategoryTheory.PreGaloisCategory.functorToAction F).Faithful
    Equations
    • ⋯ = ⋯
    source
    instance CategoryTheory.PreGaloisCategory.instPreservesMonomorphismsActionFintypeCatOfAutFunctorFunctorToAction {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] :
    (CategoryTheory.PreGaloisCategory.functorToAction F).PreservesMonomorphisms
    Equations
    • ⋯ = ⋯
    source
    instance CategoryTheory.PreGaloisCategory.instReflectsMonomorphismsActionFintypeCatOfAutFunctorFunctorToAction {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] :
    (CategoryTheory.PreGaloisCategory.functorToAction F).ReflectsMonomorphisms
    Equations
    • ⋯ = ⋯
    source
    instance CategoryTheory.PreGaloisCategory.instReflectsIsomorphismsActionFintypeCatOfAutFunctorFunctorToAction {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] :
    (CategoryTheory.PreGaloisCategory.functorToAction F).ReflectsIsomorphisms
    Equations
    • ⋯ = ⋯
    source
    noncomputable instance CategoryTheory.PreGaloisCategory.instPreservesFiniteCoproductsActionFintypeCatOfAutFunctorFunctorToAction {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] :
    CategoryTheory.Limits.PreservesFiniteCoproducts (CategoryTheory.PreGaloisCategory.functorToAction F)
    Equations
    • ⋯ = ⋯
    source
    noncomputable instance CategoryTheory.PreGaloisCategory.instPreservesFiniteProductsActionFintypeCatOfAutFunctorFunctorToAction {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] :
    CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.PreGaloisCategory.functorToAction F)
    Equations
    • ⋯ = ⋯
    source
    noncomputable instance CategoryTheory.PreGaloisCategory.instPreservesColimitsOfShapeActionFintypeCatOfAutFunctorSingleObjFunctorToActionOfFinite {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (G : Type u_1) [Group G] [Finite G] :
    CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.SingleObj G) (CategoryTheory.PreGaloisCategory.functorToAction F)
    Equations
    • ⋯ = ⋯
    source
    instance CategoryTheory.PreGaloisCategory.instPreservesIsConnectedActionFintypeCatOfAutFunctorFunctorToAction {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] :
    CategoryTheory.PreGaloisCategory.PreservesIsConnected (CategoryTheory.PreGaloisCategory.functorToAction F)
    Equations
    • ⋯ = ⋯