Commit 2024-09-18 22:16 f5c515a5

feat(CategoryTheory/Galois): universal property of fundamental group (#16673) We introduce a universal property for the automorphism group of a fiber functor for any topological group. In the further development of the Galois categories API, an arbitrary topological group satisfying this universal property shall be used in the place of Aut F, to prepare for later usages of this API in the case of e.g. G being the absolute Galois group of a field k and F being the fiber functor of the category of finite, étale k-algebras.