Structures · Category theory
CategoryTheory.PreGaloisCategory
Definition of a (Pre)Galois category. Lenstra, Def 3.1, (G1)-(G3)
- Defined in
- Mathlib.CategoryTheory.Galois.Basic
- Shape
- One type argument · adds hasTerminal, hasPullbacks, hasFiniteCoproducts, hasQuotientsByFiniteGroups, monoInducesIsoOnDirectSummand
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Every CategoryTheory.PreGaloisCategory is also a
Concrete types that are instances1
- Action
How is a type an instance?
Loading the hierarchy index…
Assumed by41
- CategoryTheory.PreGaloisCategory.evaluation_aut_injective_of_isConnected
- CategoryTheory.PreGaloisCategory.evaluation_injective_of_isConnected
- CategoryTheory.PreGaloisCategory.fiberPullbackEquiv
- CategoryTheory.PreGaloisCategory.surjective_of_nonempty_fiber_of_isConnected
- CategoryTheory.PreGaloisCategory.not_initial_of_inhabited
- CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv
- CategoryTheory.PreGaloisCategory.not_initial_iff_fiber_nonempty
- CategoryTheory.PreGaloisCategory.initial_iff_fiber_empty
- CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv
- CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_snd_apply
- CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_fst_apply
- CategoryTheory.PreGaloisCategory.isIso_of_mono_of_eq_card_fiber
- CategoryTheory.PreGaloisCategory.epi_of_nonempty_of_isConnected
- CategoryTheory.PreGaloisCategory.surjective_on_fiber_of_epi
- CategoryTheory.PreGaloisCategory.FiberFunctor.instReflectsLimitsOfShapeFintypeCatDiscretePEmpty
- CategoryTheory.PreGaloisCategory.instHasColimitsOfShapeSingleObjOfFinite
- CategoryTheory.PreGaloisCategory.instHasFiniteLimits
- CategoryTheory.PreGaloisCategory.monoInducesIsoOnDirectSummand
- CategoryTheory.PreGaloisCategory.hasQuotientsByFiniteGroups
- CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_fst_apply
- CategoryTheory.PreGaloisCategory.nonempty_fiber_pi_of_nonempty_of_finite
- CategoryTheory.PreGaloisCategory.card_aut_le_card_fiber_of_connected
- CategoryTheory.PreGaloisCategory.nonempty_fiber_of_isConnected
- CategoryTheory.PreGaloisCategory.card_hom_le_card_fiber_of_connected
- CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv_symm_ι_apply
- CategoryTheory.PreGaloisCategory.instHasBinaryProducts
- CategoryTheory.PreGaloisCategory.hasPullbacks
- CategoryTheory.PreGaloisCategory.FiberFunctor.instPreservesFiniteLimitsFintypeCat
- CategoryTheory.PreGaloisCategory.non_zero_card_fiber_of_not_initial
- CategoryTheory.PreGaloisCategory.instHasEqualizers
- CategoryTheory.PreGaloisCategory.hasTerminal
- CategoryTheory.PreGaloisCategory.card_fiber_coprod_eq_sum
- CategoryTheory.PreGaloisCategory.FiberFunctor.instReflectsMonomorphismsFintypeCat
- CategoryTheory.PreGaloisCategory.lt_card_fiber_of_mono_of_notIso
- CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_snd_apply
- CategoryTheory.PreGaloisCategory.FiberFunctor.comp_right
- CategoryTheory.PreGaloisCategory.FiberFunctor.instReflectsColimitsOfShapeFintypeCatDiscretePEmpty
- CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv.congr_simp
- CategoryTheory.PreGaloisCategory.FiberFunctor.instPreservesColimitsOfShapeFintypeCatSingleObjOfFinite
- CategoryTheory.PreGaloisCategory.hasFiniteCoproducts
- CategoryTheory.PreGaloisCategory.FiberFunctor.instFaithfulFintypeCat