Commit 2024-01-24 14:31 9a8dc7a2

View on Github →

feat(CategoryTheory/Galois): finite G-sets are a PreGaloisCategory (#9879) We show that the category of finite G-sets is a PreGaloisCategory and the forgetful functor to finite sets is a FibreFunctor.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Galois/Examples.lean

added def CategoryTheory.FintypeCat.Action.imageComplementIncl

added def CategoryTheory.FintypeCat.imageComplementIncl

Modified Mathlib/CategoryTheory/SingleObj.lean

Modified Mathlib/Logic/Equiv/TransferInstance.lean

added theorem Finite.exists_type_zero_nonempty_mulEquiv