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.

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

Stacks Tag 0BN4