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 = (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.instFaithfulContActionFintypeCatAutFunctorFunctorToContAction {C : Type u₁} [Category.{u₂, u₁} C] {F : Functor C FintypeCat} [GaloisCategory C] [FiberFunctor F] :
      (functorToContAction F).Faithful
      source
      instance CategoryTheory.PreGaloisCategory.instFullContActionFintypeCatAutFunctorFunctorToContAction {C : Type u₁} [Category.{u₂, u₁} C] {F : Functor C FintypeCat} [GaloisCategory C] [FiberFunctor F] :
      (functorToContAction F).Full
      source
      instance CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatAutFunctorFunctorToContActionOfFiberFunctor {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] {F : Functor C FintypeCat} [FiberFunctor F] :
      (functorToContAction F).EssSurj
      source
      instance CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatAutFunctorFunctorToContAction {C : Type u₁} [Category.{u₂, u₁} C] {F : Functor C FintypeCat} [GaloisCategory C] [FiberFunctor F] :
      (functorToContAction F).EssSurj
      source
      instance CategoryTheory.PreGaloisCategory.instIsEquivalenceContActionFintypeCatAutFunctorFunctorToContAction {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.

      Stacks Tag 0BN4