Commit 2024-09-19 18:05 db697686

View on Github →

feat(CategoryTheory/Galois): prerequisites for essential surjectivity (#16948) This PR collects prerequisites for the essential surjectivity of fiber functors in a Galois category.

Estimated changes

Modified Mathlib/CategoryTheory/Galois/Basic.lean

added theorem CategoryTheory.PreGaloisCategory.mulAction_naturality

Modified Mathlib/CategoryTheory/Galois/Examples.lean

Modified Mathlib/CategoryTheory/Galois/GaloisObjects.lean

added theorem CategoryTheory.PreGaloisCategory.stabilizer_normal_of_isGalois

Modified Mathlib/RepresentationTheory/Action/Basic.lean

added theorem Action.hom_inv_hom

added theorem Action.inv_hom_hom

Modified Mathlib/RepresentationTheory/Action/Concrete.lean

added def Action.FintypeCat.quotientToEndHom

added theorem Action.FintypeCat.quotientToEndHom_mk

added def Action.FintypeCat.quotientToQuotientOfLE

added theorem Action.FintypeCat.quotientToQuotientOfLE_hom_mk

added def Action.FintypeCat.toEndHom

added theorem Action.FintypeCat.toEndHom_apply

added theorem Action.FintypeCat.toEndHom_trivial_of_mem