Documentation

Mathlib.CategoryTheory.Galois.Equivalence

Fiber functors induce an equivalence of categories #

Let C be a Galois category with fiber functor F.

In this file we conclude that the induced functor from C to the category of finite, discrete Aut F-sets is an equivalence of categories.

source
def CategoryTheory.PreGaloisCategory.functorToContAction {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) :
Functor C (ContAction FintypeCat (Aut F))

The induced functor from C to the category of finite, discrete Aut F-sets.

Equations
Instances For
    source
    @[simp]
    theorem CategoryTheory.PreGaloisCategory.functorToContAction_map {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
    (functorToContAction F).map f = ObjectProperty.homMk ((functorToAction F).map f)
    source
    @[simp]
    theorem CategoryTheory.PreGaloisCategory.functorToContAction_obj_obj {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) (X : C) :
    ((functorToContAction F).obj X).obj = (functorToAction F).obj X
    source
    instance CategoryTheory.PreGaloisCategory.instFaithfulContActionFintypeCatFunObjFiniteAutFunctorFunctorToContAction {C : Type u₁} [Category.{u₂, u₁} C] {F : Functor C FintypeCat} [GaloisCategory C] [FiberFunctor F] :
    (functorToContAction F).Faithful
    source
    instance CategoryTheory.PreGaloisCategory.instFullContActionFintypeCatFunObjFiniteAutFunctorFunctorToContAction {C : Type u₁} [Category.{u₂, u₁} C] {F : Functor C FintypeCat} [GaloisCategory C] [FiberFunctor F] :
    (functorToContAction F).Full
    source
    instance CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatFunObjFiniteAutFunctorFunctorToContActionOfFiberFunctor {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] {F : Functor C FintypeCat} [FiberFunctor F] :
    (functorToContAction F).EssSurj
    source
    instance CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatFunObjFiniteAutFunctorFunctorToContAction {C : Type u₁} [Category.{u₂, u₁} C] {F : Functor C FintypeCat} [GaloisCategory C] [FiberFunctor F] :
    (functorToContAction F).EssSurj
    source
    instance CategoryTheory.PreGaloisCategory.instIsEquivalenceContActionFintypeCatFunObjFiniteAutFunctorFunctorToContAction {C : Type u₁} [Category.{u₂, u₁} C] {F : Functor C FintypeCat} [GaloisCategory C] [FiberFunctor F] :
    (functorToContAction F).IsEquivalence

    Any fiber functor F induces an equivalence of categories with the category of finite and discrete Aut F-sets.