Structures · Category theory
CategoryTheory.GaloisCategory
A PreGaloisCategory is a GaloisCategory if it admits a fiber functor.
- Defined in
- Mathlib.CategoryTheory.Galois.Basic
- Shape
- One type argument · adds hasFiberFunctor
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Action
How is a type an instance?
Loading the hierarchy index…
Assumed by132
- CategoryTheory.PreGaloisCategory.PointedGaloisObject.obj
- CategoryTheory.PreGaloisCategory.PointedGaloisObject.pt
- CategoryTheory.PreGaloisCategory.AutGalois
- CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.val
- CategoryTheory.PreGaloisCategory.autMap
- CategoryTheory.PreGaloisCategory.AutGalois.π
- CategoryTheory.PreGaloisCategory.PointedGaloisObject.incl
- CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois
- CategoryTheory.PreGaloisCategory.autGaloisSystem
- CategoryTheory.PreGaloisCategory.autMulEquivAutGalois
- CategoryTheory.PreGaloisCategory.GaloisCategory.getFiberFunctor
- CategoryTheory.PreGaloisCategory.endEquivAutGalois
- CategoryTheory.PreGaloisCategory.autMapHom
- CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_fiber
- CategoryTheory.PreGaloisCategory.has_decomp_connected_components
- CategoryTheory.PreGaloisCategory.endEquivAutGalois_π
- CategoryTheory.PreGaloisCategory.endMulEquivAutGalois
- CategoryTheory.PreGaloisCategory.fiber_in_connected_component
- CategoryTheory.PreGaloisCategory.comp_autMap
- CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_fiber_nonempty
- CategoryTheory.PreGaloisCategory.exists_autMap
- CategoryTheory.PreGaloisCategory.comp_autMap_apply
- CategoryTheory.PreGaloisCategory.toAutMulEquiv
- CategoryTheory.PreGaloisCategory.exists_galois_representative
- CategoryTheory.PreGaloisCategory.autMap_unique
- CategoryTheory.PreGaloisCategory.action_ext_of_isGalois
- CategoryTheory.PreGaloisCategory.has_decomp_connected_components'
- CategoryTheory.PreGaloisCategory.toAut_surjective_isGalois
- CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois_symm_fiber
- CategoryTheory.PreGaloisCategory.PointedGaloisObject.cocone
- CategoryTheory.PreGaloisCategory.exists_set_ker_evaluation_subset_of_isOpen
- CategoryTheory.PreGaloisCategory.endEquivSectionsFibers
- CategoryTheory.PreGaloisCategory.autIsoFibers
- CategoryTheory.PreGaloisCategory.exists_lift_of_mono_of_isConnected
- CategoryTheory.PreGaloisCategory.quotientByAutTerminalEquivUniqueQuotient
- CategoryTheory.PreGaloisCategory.PointedGaloisObject.isColimit
- CategoryTheory.PreGaloisCategory.PointedGaloisObject.comp_val
- CategoryTheory.PreGaloisCategory.nhds_one_has_basis_stabilizers
- CategoryTheory.PreGaloisCategory.natTrans_ext_of_isGalois
- CategoryTheory.PreGaloisCategory.isGalois_iff_pretransitive
- CategoryTheory.PreGaloisCategory.stabilizer_normal_of_isGalois
- CategoryTheory.PreGaloisCategory.toAutHomeo
- CategoryTheory.PreGaloisCategory.AutGalois.π_surjective
- CategoryTheory.PreGaloisCategory.autGaloisSystem_map_surjective
- CategoryTheory.PreGaloisCategory.connected_component_unique
- CategoryTheory.PreGaloisCategory.toAut_bijective
- CategoryTheory.PreGaloisCategory.toAut_surjective_isGalois_finite_family
- CategoryTheory.PreGaloisCategory.isGalois_iff_aux
- CategoryTheory.PreGaloisCategory.toAut_continuous
- CategoryTheory.PreGaloisCategory.autMap_surjective_of_isGalois