Theorem CategoryTheory.PreGaloisCategory.exists_lift_of_mono_of_isConnected

Modification history

2025-02-25 19:33

Mathlib/CategoryTheory/Galois/Full.lean

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

Modified CategoryTheory.PreGaloisCategory.exists_lift_of_mono_of_isConnected View on Github →

2024-09-10 09:38

Mathlib/CategoryTheory/Galois/Full.lean

feat(CategoryTheory/Galois): any fiber functor of a Galois category is full (#16478) …

Added CategoryTheory.PreGaloisCategory.exists_lift_of_mono_of_isConnected View on Github →