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.
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
@[simp]
theorem
CategoryTheory.PreGaloisCategory.functorToContAction_obj_obj
{C : Type u₁}
[Category.{u₂, u₁} C]
(F : Functor C FintypeCat)
(X : C)
:
@[simp]
theorem
CategoryTheory.PreGaloisCategory.functorToContAction_map
{C : Type u₁}
[Category.{u₂, u₁} C]
(F : Functor C FintypeCat)
{X✝ Y✝ : C}
(f : X✝ ⟶ Y✝)
:
instance
CategoryTheory.PreGaloisCategory.instFaithfulContActionFintypeCatAutFunctorFunctorToContAction
{C : Type u₁}
[Category.{u₂, u₁} C]
{F : Functor C FintypeCat}
[GaloisCategory C]
[FiberFunctor F]
:
instance
CategoryTheory.PreGaloisCategory.instFullContActionFintypeCatAutFunctorFunctorToContAction
{C : Type u₁}
[Category.{u₂, u₁} C]
{F : Functor C FintypeCat}
[GaloisCategory C]
[FiberFunctor F]
:
instance
CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatAutFunctorFunctorToContActionOfFiberFunctor
{C : Type u₁}
[Category.{u₂, u₁} C]
[GaloisCategory C]
{F : Functor C FintypeCat}
[FiberFunctor F]
:
instance
CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatAutFunctorFunctorToContAction
{C : Type u₁}
[Category.{u₂, u₁} C]
{F : Functor C FintypeCat}
[GaloisCategory C]
[FiberFunctor F]
:
instance
CategoryTheory.PreGaloisCategory.instIsEquivalenceContActionFintypeCatAutFunctorFunctorToContAction
{C : Type u₁}
[Category.{u₂, u₁} C]
{F : Functor C FintypeCat}
[GaloisCategory C]
[FiberFunctor F]
:
Any fiber functor F
induces an equivalence of categories with the category of finite and
discrete Aut F
-sets.