Commit 2025-05-05 21:48 24bb9b2c

View on Github →

feat(CategoryTheory/Galois): equivalence to ContAction (#24563)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Galois/Basic.lean

deleted theorem CategoryTheory.PreGaloisCategory.FiberFunctor.comp_right

Created Mathlib/CategoryTheory/Galois/Equivalence.lean

added def CategoryTheory.PreGaloisCategory.functorToContAction

Modified Mathlib/CategoryTheory/Galois/Topology.lean

added theorem CategoryTheory.PreGaloisCategory.continuous_mapAut_whiskeringRight

Modified Mathlib/Topology/Category/FinTopCat.lean