general theory of Galois categories

[chrisflav]

This issue is meant as a way to track PRs on the development of the general theory of Galois categories. The rough outline is:

• Prove that any fiber functor F induces an equivalence with the category of finite, discrete Aut F-sets. Here C should not be required to be (essentially) small.
• Develop the notion of IsFundamentalGroup F G for a fiber functor F and a topological group G.
• Show that an exact functor between Galois categories induces a continuous homomorphism between fundamental groups.
• API for when this induced homomorphism is injective, surjective, etc.

The main chunk of the first point is already in mathlib. Already closed or still open PRs on this topic:

• [Merged by Bors] - feat(CategoryTheory/Galois): topology of fundamental group #16441
• [Merged by Bors] - feat(CategoryTheory/Galois): any fiber functor of a Galois category is full #16478
• [Merged by Bors] - chore(CategoryTheory/Galois): split out definition from Full file #16661
• [Merged by Bors] - feat(Algebra/OpenSubgroup): quotient of compact group by open subgroup is finite #16671
• [Merged by Bors] - feat(CategoryTheory/Galois): generalize transitivity to arbitrary universes #16664
• [Merged by Bors] - feat(CategorTheory/Galois): stabilizers form a neighborhood basis of the identity #16668
• [Merged by Bors] - feat(CategoryTheory/Galois): prerequisites for essential surjectivity #16948
• [Merged by Bors] - feat(CategoryTheory/Galois): fiber functor is essentially surjective #16552
• [Merged by Bors] - feat(CategoryTheory/Galois): universal property of fundamental group #16673