Commit 2024-02-08 17:51 fd0d24ab

feat(CategoryTheory/Galois): definition and characterisation of Galois objects (#10215) Defines Galois objects in a Galois category in a fibre functor independent way, also gives an equivalent characterisation in terms of a fibre functor. To allow for a definition that only depends on C, contrary to what was said earlier, we introduce a GaloisCategory typeclass extending PreGaloisCategory that additionally asserts the existence of a fibre functor.