Commit 2024-06-08 16:29 dc44d90b

feat(CategoryTheory/Galois): fundamental group is limit of automorphism groups (#12843) We show that the automorphism group of a fiber functor is isomorphic to the limit of the automorphism groups of all Galois objects. From this we deduce that the automorphism group of a fiber functor acts transitively on the fibers of connected objects. This is the last essential step towards showing that a fiber functor induces a fully faithful embedding into the category of finite Aut F-types.