Commit 2024-10-02 09:44 b91c5b63

View on Github →

feat(CategoryTheory/Galois): fiber functor is essentially surjective (#16552) We show that every finite, discrete Aut F-set is in the essential image of the fiber functor.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Galois/EssSurj.lean

added theorem CategoryTheory.PreGaloisCategory.exists_lift_of_continuous

added theorem CategoryTheory.PreGaloisCategory.exists_lift_of_quotient_openSubgroup

added def CategoryTheory.PreGaloisCategory.fiberIsoQuotientStabilizer

added theorem CategoryTheory.PreGaloisCategory.has_decomp_quotients

Modified Mathlib/CategoryTheory/Galois/Full.lean