Structures · Category theory
CategoryTheory.PreGaloisCategory.FiberFunctor
Definition of a fiber functor from a Galois category. Lenstra, Def 3.1, (G4)-(G6)
- Defined in
- Mathlib.CategoryTheory.Galois.Basic
- Shape
- One type argument · adds preservesTerminalObjects, preservesPullbacks, preservesFiniteCoproducts, preservesEpis, preservesQuotientsByFiniteGroups, reflectsIsos
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Action
How is a type an instance?
Loading the hierarchy index…
Assumed by116
- CategoryTheory.PreGaloisCategory.evaluation_aut_injective_of_isConnected
- CategoryTheory.PreGaloisCategory.evaluation_injective_of_isConnected
- CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois
- CategoryTheory.PreGaloisCategory.autMulEquivAutGalois
- CategoryTheory.PreGaloisCategory.endEquivAutGalois
- CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_fiber
- CategoryTheory.PreGaloisCategory.fiberPullbackEquiv
- CategoryTheory.PreGaloisCategory.surjective_of_nonempty_fiber_of_isConnected
- CategoryTheory.PreGaloisCategory.endEquivAutGalois_π
- CategoryTheory.PreGaloisCategory.not_initial_of_inhabited
- CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv
- CategoryTheory.PreGaloisCategory.endMulEquivAutGalois
- CategoryTheory.PreGaloisCategory.fiber_in_connected_component
- CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_fiber_nonempty
- CategoryTheory.PreGaloisCategory.toAutMulEquiv
- CategoryTheory.PreGaloisCategory.exists_galois_representative
- CategoryTheory.PreGaloisCategory.not_initial_iff_fiber_nonempty
- CategoryTheory.PreGaloisCategory.initial_iff_fiber_empty
- CategoryTheory.PreGaloisCategory.action_ext_of_isGalois
- CategoryTheory.PreGaloisCategory.toAut_surjective_isGalois
- CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois_symm_fiber
- CategoryTheory.PreGaloisCategory.exists_set_ker_evaluation_subset_of_isOpen
- CategoryTheory.PreGaloisCategory.endEquivSectionsFibers
- CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv
- CategoryTheory.PreGaloisCategory.autIsoFibers
- CategoryTheory.PreGaloisCategory.exists_lift_of_mono_of_isConnected
- CategoryTheory.PreGaloisCategory.quotientByAutTerminalEquivUniqueQuotient
- CategoryTheory.PreGaloisCategory.PointedGaloisObject.isColimit
- CategoryTheory.PreGaloisCategory.nhds_one_has_basis_stabilizers
- CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_snd_apply
- CategoryTheory.PreGaloisCategory.natTrans_ext_of_isGalois
- CategoryTheory.PreGaloisCategory.isGalois_iff_pretransitive
- CategoryTheory.PreGaloisCategory.stabilizer_normal_of_isGalois
- CategoryTheory.PreGaloisCategory.toAutHomeo
- CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_fst_apply
- CategoryTheory.PreGaloisCategory.isIso_of_mono_of_eq_card_fiber
- CategoryTheory.PreGaloisCategory.epi_of_nonempty_of_isConnected
- CategoryTheory.PreGaloisCategory.AutGalois.π_surjective
- CategoryTheory.PreGaloisCategory.connected_component_unique
- CategoryTheory.PreGaloisCategory.toAut_bijective
- CategoryTheory.PreGaloisCategory.toAut_surjective_isGalois_finite_family
- CategoryTheory.PreGaloisCategory.toAut_continuous
- CategoryTheory.PreGaloisCategory.exists_lift_of_quotient_openSubgroup
- CategoryTheory.PreGaloisCategory.endEquivSectionsFibers_π
- CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_π
- CategoryTheory.PreGaloisCategory.fiberIsoQuotientStabilizer
- CategoryTheory.PreGaloisCategory.toAut_surjective_of_isPretransitive
- CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_symm_app
- CategoryTheory.PreGaloisCategory.surjective_on_fiber_of_epi
- CategoryTheory.PreGaloisCategory.evaluation_aut_surjective_of_isGalois
Ancestors0
No ancestors.