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.
Instances For
@[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
@[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)
instance
CategoryTheory.PreGaloisCategory.instFaithfulContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction
{C : Type uā}
[Category.{uā, uā} C]
{F : Functor C FintypeCat}
[GaloisCategory C]
[FiberFunctor F]
:
instance
CategoryTheory.PreGaloisCategory.instFullContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction
{C : Type uā}
[Category.{uā, uā} C]
{F : Functor C FintypeCat}
[GaloisCategory C]
[FiberFunctor F]
:
instance
CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction
{C : Type uā}
[Category.{uā, uā} C]
{F : Functor C FintypeCat}
[GaloisCategory C]
[FiberFunctor F]
:
instance
CategoryTheory.PreGaloisCategory.instIsEquivalenceContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction
{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.