Commit 2024-03-06 12:56 e6d6f9dd

feat(CategoryTheory/Galois): Fibers are represented by Galois objects (#10426) We show that if X is an object in a Galois category, then there exists an object A and a point a in the fiber of A such that A is Galois and that the evaluation map at a from A ⟶ X to the fiber of X is bijective. This is the main input in the pro-representability of fiber functors.