Theorem CategoryTheory.PreGaloisCategory.exists_lift_of_continuous

Modification history

2025-02-25 19:33

Mathlib/CategoryTheory/Galois/EssSurj.lean

refactor(CategoryTheory/Action/*): make `Action.rho` a `MonoidHom` instead of a morphism in `MonCat` (#21652)

Modified CategoryTheory.PreGaloisCategory.exists_lift_of_continuous View on Github →

2024-10-02 09:44

Mathlib/CategoryTheory/Galois/EssSurj.lean

feat(CategoryTheory/Galois): fiber functor is essentially surjective (#16552) …

Added CategoryTheory.PreGaloisCategory.exists_lift_of_continuous View on Github →