Basic

📁 Source: Mathlib/CategoryTheory/Galois/Basic.lean

Statistics

Metric	Count
Definitions GaloisCategory, PreGaloisCategory, FiberFunctor, getFiberFunctor, PreservesIsConnected, fiberBinaryProductEquiv, fiberEqualizerEquiv, fiberPullbackEquiv, instMulActionAutFunctorFintypeCatCarrierObj	9
Theorems hasFiberFunctor, toPreGaloisCategory, comp_right, instFaithfulFintypeCat, instPreservesColimitsOfShapeFintypeCatSingleObjOfFinite, instPreservesFiniteLimitsFintypeCat, instReflectsColimitsOfShapeFintypeCatDiscretePEmpty, instReflectsLimitsOfShapeFintypeCatDiscretePEmpty, instReflectsMonomorphismsFintypeCat, preservesEpis, preservesFiniteCoproducts, preservesPullbacks, preservesQuotientsByFiniteGroups, preservesTerminalObjects, reflectsIsos, noTrivialComponent, notInitial, preserves, card_aut_le_card_fiber_of_connected, card_fiber_coprod_eq_sum, card_fiber_eq_of_iso, card_hom_le_card_fiber_of_connected, epi_of_nonempty_of_isConnected, evaluation_aut_injective_of_isConnected, evaluation_injective_of_isConnected, fiberBinaryProductEquiv_symm_fst_apply, fiberBinaryProductEquiv_symm_snd_apply, fiberEqualizerEquiv_symm_ι_apply, fiberPullbackEquiv_symm_fst_apply, fiberPullbackEquiv_symm_snd_apply, hasFiniteCoproducts, hasPullbacks, hasQuotientsByFiniteGroups, hasTerminal, has_non_trivial_subobject_of_not_isConnected_of_not_initial, initial_iff_fiber_empty, instFiberFunctorGetFiberFunctor, instFiniteAutOfIsConnected, instFiniteHomOfIsConnected, instHasBinaryProducts, instHasColimitsOfShapeSingleObjOfFinite, instHasEqualizers, instHasFiniteLimits, instMonoCoprod, isIso_of_mono_of_eq_card_fiber, lt_card_fiber_of_mono_of_notIso, monoInducesIsoOnDirectSummand, mulAction_def, mulAction_naturality, non_zero_card_fiber_of_not_initial, nonempty_fiber_of_isConnected, nonempty_fiber_pi_of_nonempty_of_finite, not_initial_iff_fiber_nonempty, not_initial_of_inhabited, surjective_of_nonempty_fiber_of_isConnected, surjective_on_fiber_of_epi	56
Total	65

CategoryTheory

Definitions

Name	Category	Theorems
GaloisCategory 📖	CompData	1 math math: FintypeCat.instGaloisCategoryActionFintypeCat
PreGaloisCategory 📖	CompData	2 math math: GaloisCategory.toPreGaloisCategory, FintypeCat.instPreGaloisCategoryActionFintypeCat

CategoryTheory.GaloisCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasFiberFunctor 📖	mathematical	—	CategoryTheory.PreGaloisCategory.FiberFunctor toPreGaloisCategory	—	—
toPreGaloisCategory 📖	mathematical	—	CategoryTheory.PreGaloisCategory	—	—

CategoryTheory.PreGaloisCategory

Definitions

Name	Category	Theorems
FiberFunctor 📖	CompData	5 math math: CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget, instFiberFunctorGetFiberFunctor, FiberFunctor.comp_right, CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeHomCarrierV, CategoryTheory.GaloisCategory.hasFiberFunctor
PreservesIsConnected 📖	CompData	1 math math: instPreservesIsConnectedActionFintypeCatAutFunctorFunctorToAction
fiberBinaryProductEquiv 📖	CompOp	2 math math: fiberBinaryProductEquiv_symm_fst_apply, fiberBinaryProductEquiv_symm_snd_apply
fiberEqualizerEquiv 📖	CompOp	1 math math: fiberEqualizerEquiv_symm_ι_apply
fiberPullbackEquiv 📖	CompOp	2 math math: fiberPullbackEquiv_symm_fst_apply, fiberPullbackEquiv_symm_snd_apply
instMulActionAutFunctorFintypeCatCarrierObj 📖	CompOp	8 math math: mulAction_def, instIsFundamentalGroupAutFunctorFintypeCat, continuousSMul_aut_fiber, FiberFunctor.isPretransitive_of_isConnected, nhds_one_has_basis_stabilizers, stabilizer_normal_of_isGalois, mulAction_naturality, FiberFunctor.isPretransitive_of_isGalois

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_aut_le_card_fiber_of_connected 📖	mathematical	—	Nat.card CategoryTheory.Aut FintypeCat.carrier CategoryTheory.Functor.obj FintypeCat FintypeCat.instCategory	—	nonempty_fiber_of_isConnected Nat.card_le_card_of_injective Finite.of_fintype evaluation_aut_injective_of_isConnected
card_fiber_coprod_eq_sum 📖	mathematical	—	Nat.card FintypeCat.carrier CategoryTheory.Functor.obj FintypeCat FintypeCat.instCategory CategoryTheory.Limits.coprod CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts Finite.of_fintype CategoryTheory.Limits.Types.hasColimit CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.comp_preservesColimit CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts FiberFunctor.preservesFiniteCoproducts CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit Nat.card_sum Nat.card_eq_of_bijective Equiv.bijective
card_fiber_eq_of_iso 📖	mathematical	—	Nat.card FintypeCat.carrier CategoryTheory.Functor.obj FintypeCat FintypeCat.instCategory	—	Nat.card_eq_of_bijective Equiv.bijective
card_hom_le_card_fiber_of_connected 📖	mathematical	—	Nat.card Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct FintypeCat.carrier CategoryTheory.Functor.obj FintypeCat FintypeCat.instCategory	—	Nat.card_le_card_of_injective Finite.of_fintype nonempty_fiber_of_isConnected evaluation_injective_of_isConnected
epi_of_nonempty_of_isConnected 📖	mathematical	—	CategoryTheory.Epi	—	evaluation_injective_of_isConnected CategoryTheory.Functor.map_comp DFunLike.congr_fun CategoryTheory.Functor.congr_map
evaluation_aut_injective_of_isConnected 📖	mathematical	—	CategoryTheory.Aut FintypeCat.carrier CategoryTheory.Functor.obj FintypeCat FintypeCat.instCategory DFunLike.coe FintypeCat.instFunLikeHomCarrier CategoryTheory.ConcreteCategory.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct FintypeCat.concreteCategoryFintype CategoryTheory.Functor.map CategoryTheory.Iso.hom	—	evaluation_injective_of_isConnected CategoryTheory.Aut.ext
evaluation_injective_of_isConnected 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct FintypeCat.carrier CategoryTheory.Functor.obj FintypeCat FintypeCat.instCategory DFunLike.coe FintypeCat.instFunLikeHomCarrier CategoryTheory.ConcreteCategory.hom FintypeCat.concreteCategoryFintype CategoryTheory.Functor.map	—	CategoryTheory.Limits.eq_of_epi_equalizer CategoryTheory.Limits.hasLimitOfHasLimitsOfShape instHasEqualizers CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso IsConnected.noTrivialComponent CategoryTheory.Limits.equalizer.ι_mono not_initial_of_inhabited
fiberBinaryProductEquiv_symm_fst_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj FintypeCat FintypeCat.instCategory CategoryTheory.Limits.prod CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory instHasBinaryProducts CategoryTheory.Limits.pair FintypeCat.carrier FintypeCat.instFunLikeHomCarrier CategoryTheory.ConcreteCategory.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct FintypeCat.concreteCategoryFintype CategoryTheory.Functor.map CategoryTheory.Limits.prod.fst Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm fiberBinaryProductEquiv	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape instHasBinaryProducts CategoryTheory.Limits.Types.hasLimit CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.PreservesLimitPair.iso_inv_fst CategoryTheory.Limits.Types.binaryProductIso_inv_comp_fst
fiberBinaryProductEquiv_symm_snd_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj FintypeCat FintypeCat.instCategory CategoryTheory.Limits.prod CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory instHasBinaryProducts CategoryTheory.Limits.pair FintypeCat.carrier FintypeCat.instFunLikeHomCarrier CategoryTheory.ConcreteCategory.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct FintypeCat.concreteCategoryFintype CategoryTheory.Functor.map CategoryTheory.Limits.prod.snd Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm fiberBinaryProductEquiv	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape instHasBinaryProducts CategoryTheory.Limits.Types.hasLimit CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.PreservesLimitPair.iso_inv_snd CategoryTheory.Limits.Types.binaryProductIso_inv_comp_snd
fiberEqualizerEquiv_symm_ι_apply 📖	mathematical	DFunLike.coe CategoryTheory.Functor.obj FintypeCat FintypeCat.instCategory FintypeCat.carrier FintypeCat.instFunLikeHomCarrier CategoryTheory.ConcreteCategory.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct FintypeCat.concreteCategoryFintype CategoryTheory.Functor.map	CategoryTheory.Limits.equalizer CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory instHasEqualizers CategoryTheory.Limits.parallelPair CategoryTheory.Limits.equalizer.ι Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm fiberEqualizerEquiv	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape instHasEqualizers CategoryTheory.Limits.Types.hasLimit UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.PreservesEqualizer.iso_inv_ι CategoryTheory.Limits.Types.equalizerIso_inv_comp_ι
fiberPullbackEquiv_symm_fst_apply 📖	mathematical	DFunLike.coe CategoryTheory.Functor.obj FintypeCat FintypeCat.instCategory FintypeCat.carrier FintypeCat.instFunLikeHomCarrier CategoryTheory.ConcreteCategory.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct FintypeCat.concreteCategoryFintype CategoryTheory.Functor.map	CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair hasPullbacks CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.fst Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm fiberPullbackEquiv	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape hasPullbacks CategoryTheory.Limits.Types.hasLimit UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.PreservesPullback.iso_inv_fst CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst
fiberPullbackEquiv_symm_snd_apply 📖	mathematical	DFunLike.coe CategoryTheory.Functor.obj FintypeCat FintypeCat.instCategory FintypeCat.carrier FintypeCat.instFunLikeHomCarrier CategoryTheory.ConcreteCategory.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct FintypeCat.concreteCategoryFintype CategoryTheory.Functor.map	CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair hasPullbacks CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm fiberPullbackEquiv	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape hasPullbacks CategoryTheory.Limits.Types.hasLimit UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.PreservesPullback.iso_inv_snd CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd
hasFiniteCoproducts 📖	mathematical	—	CategoryTheory.Limits.HasFiniteCoproducts	—	—
hasPullbacks 📖	mathematical	—	CategoryTheory.Limits.HasPullbacks	—	—
hasQuotientsByFiniteGroups 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.SingleObj CategoryTheory.SingleObj.category DivInvMonoid.toMonoid Group.toDivInvMonoid	—	—
hasTerminal 📖	mathematical	—	CategoryTheory.Limits.HasTerminal	—	—
has_non_trivial_subobject_of_not_isConnected_of_not_initial 📖	mathematical	IsConnected	CategoryTheory.Mono CategoryTheory.IsIso	—	Mathlib.Tactic.Contrapose.contrapose₂ Mathlib.Tactic.Push.not_and_eq
initial_iff_fiber_empty 📖	mathematical	—	CategoryTheory.Limits.IsInitial IsEmpty FintypeCat.carrier CategoryTheory.Functor.obj FintypeCat FintypeCat.instCategory	—	Equiv.nonempty_congr CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts Finite.of_fintype FiberFunctor.preservesFiniteCoproducts CategoryTheory.Limits.reflectsColimit_of_reflectsColimitsOfShape FiberFunctor.instReflectsColimitsOfShapeFintypeCatDiscretePEmpty CategoryTheory.Limits.Concrete.initial_iff_empty_of_preserves_of_reflects CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit CategoryTheory.Limits.Types.hasColimit CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.CreatesColimit.toReflectsColimit
instFiberFunctorGetFiberFunctor 📖	mathematical	—	FiberFunctor CategoryTheory.GaloisCategory.toPreGaloisCategory GaloisCategory.getFiberFunctor	—	CategoryTheory.GaloisCategory.toPreGaloisCategory CategoryTheory.GaloisCategory.hasFiberFunctor
instFiniteAutOfIsConnected 📖	mathematical	—	Finite CategoryTheory.Aut	—	nonempty_fiber_of_isConnected CategoryTheory.GaloisCategory.toPreGaloisCategory instFiberFunctorGetFiberFunctor Finite.of_injective Finite.of_fintype evaluation_aut_injective_of_isConnected
instFiniteHomOfIsConnected 📖	mathematical	—	Finite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	nonempty_fiber_of_isConnected CategoryTheory.GaloisCategory.toPreGaloisCategory instFiberFunctorGetFiberFunctor Finite.of_injective Finite.of_fintype evaluation_injective_of_isConnected
instHasBinaryProducts 📖	mathematical	—	CategoryTheory.Limits.HasBinaryProducts	—	hasBinaryProducts_of_hasTerminal_and_pullbacks hasTerminal hasPullbacks
instHasColimitsOfShapeSingleObjOfFinite 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.SingleObj CategoryTheory.SingleObj.category DivInvMonoid.toMonoid Group.toDivInvMonoid	—	Finite.exists_type_univ_nonempty_mulEquiv CategoryTheory.Limits.hasColimitsOfShape_of_equivalence hasQuotientsByFiniteGroups Finite.of_fintype
instHasEqualizers 📖	mathematical	—	CategoryTheory.Limits.HasEqualizers	—	CategoryTheory.Limits.hasEqualizers_of_hasPullbacks_and_binary_products instHasBinaryProducts hasPullbacks
instHasFiniteLimits 📖	mathematical	—	CategoryTheory.Limits.HasFiniteLimits	—	CategoryTheory.Limits.hasFiniteLimits_of_hasTerminal_and_pullbacks hasTerminal hasPullbacks
instMonoCoprod 📖	mathematical	—	CategoryTheory.Limits.MonoCoprod	—	CategoryTheory.Limits.MonoCoprod.monoCoprod_of_preservesCoprod_of_reflectsMono CategoryTheory.Limits.MonoCoprod.instOfPreservesColimitsOfShapeDiscreteWalkingPairOfReflectsMonomorphismsForget CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits CategoryTheory.Limits.FintypeCat.instPreservesFiniteColimitsFintypeCatForgetHomCarrier CategoryTheory.reflectsMonomorphisms_of_reflectsLimitsOfShape CategoryTheory.Limits.ReflectsFiniteLimits.reflects CategoryTheory.Limits.reflectsFiniteLimits_of_reflectsIsomorphisms CategoryTheory.reflectsIsomorphisms_of_full_and_faithful FintypeCat.instFullForgetHomCarrier CategoryTheory.instFaithfulForget CategoryTheory.Limits.FintypeCat.hasFiniteLimits CategoryTheory.Limits.FintypeCat.instPreservesFiniteLimitsFintypeCatForgetHomCarrier CategoryTheory.Limits.instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts Finite.of_fintype FiberFunctor.preservesFiniteCoproducts CategoryTheory.GaloisCategory.toPreGaloisCategory instFiberFunctorGetFiberFunctor FiberFunctor.instReflectsMonomorphismsFintypeCat
isIso_of_mono_of_eq_card_fiber 📖	mathematical	Nat.card FintypeCat.carrier CategoryTheory.Functor.obj FintypeCat FintypeCat.instCategory	CategoryTheory.IsIso	—	CategoryTheory.ConcreteCategory.isIso_iff_bijective CategoryTheory.reflectsIsomorphisms_of_full_and_faithful FintypeCat.instFullForgetHomCarrier CategoryTheory.instFaithfulForget Fintype.bijective_iff_injective_and_card CategoryTheory.ConcreteCategory.injective_of_mono_of_preservesPullback CategoryTheory.Functor.map_mono CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape FiberFunctor.preservesPullbacks CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.FintypeCat.instPreservesFiniteLimitsFintypeCatForgetHomCarrier CategoryTheory.isIso_of_reflects_iso FiberFunctor.reflectsIsos
lt_card_fiber_of_mono_of_notIso 📖	mathematical	CategoryTheory.IsIso	Nat.card FintypeCat.carrier CategoryTheory.Functor.obj FintypeCat FintypeCat.instCategory	—	isIso_of_mono_of_eq_card_fiber Nat.card_le_card_of_injective Finite.of_fintype CategoryTheory.ConcreteCategory.injective_of_mono_of_preservesPullback CategoryTheory.Functor.map_mono CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape FiberFunctor.preservesPullbacks CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.FintypeCat.instPreservesFiniteLimitsFintypeCatForgetHomCarrier
monoInducesIsoOnDirectSummand 📖	mathematical	—	CategoryTheory.Limits.IsColimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair	—	—
mulAction_def 📖	mathematical	—	CategoryTheory.Aut CategoryTheory.Functor FintypeCat FintypeCat.instCategory CategoryTheory.Functor.category FintypeCat.carrier CategoryTheory.Functor.obj SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup MulAction.toSemigroupAction instMulActionAutFunctorFintypeCatCarrierObj DFunLike.coe FintypeCat.instFunLikeHomCarrier CategoryTheory.ConcreteCategory.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct FintypeCat.concreteCategoryFintype CategoryTheory.NatTrans.app CategoryTheory.Iso.hom	—	—
mulAction_naturality 📖	mathematical	—	CategoryTheory.Aut CategoryTheory.Functor FintypeCat FintypeCat.instCategory CategoryTheory.Functor.category FintypeCat.carrier CategoryTheory.Functor.obj SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup MulAction.toSemigroupAction instMulActionAutFunctorFintypeCatCarrierObj DFunLike.coe FintypeCat.instFunLikeHomCarrier CategoryTheory.ConcreteCategory.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct FintypeCat.concreteCategoryFintype CategoryTheory.Functor.map	—	FunctorToFintypeCat.naturality
non_zero_card_fiber_of_not_initial 📖	—	—	—	—	initial_iff_fiber_empty Finite.card_eq_zero_iff Finite.of_fintype
nonempty_fiber_of_isConnected 📖	mathematical	—	FintypeCat.carrier CategoryTheory.Functor.obj FintypeCat FintypeCat.instCategory	—	initial_iff_fiber_empty not_nonempty_iff IsConnected.notInitial
nonempty_fiber_pi_of_nonempty_of_finite 📖	mathematical	FintypeCat.carrier CategoryTheory.Functor.obj FintypeCat FintypeCat.instCategory	CategoryTheory.Limits.piObj CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits instHasFiniteLimits CategoryTheory.Discrete.functor	—	nonempty_fintype CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits instHasFiniteLimits CategoryTheory.Limits.FintypeCat.hasFiniteLimits CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts CategoryTheory.Limits.instPreservesFiniteProductsOfPreservesFiniteLimits FiberFunctor.instPreservesFiniteLimitsFintypeCat CategoryTheory.Limits.FintypeCat.nonempty_pi_of_nonempty
not_initial_iff_fiber_nonempty 📖	mathematical	—	FintypeCat.carrier CategoryTheory.Functor.obj FintypeCat FintypeCat.instCategory	—	not_isEmpty_iff initial_iff_fiber_empty
not_initial_of_inhabited 📖	—	—	—	—	IsEmpty.false initial_iff_fiber_empty
surjective_of_nonempty_fiber_of_isConnected 📖	mathematical	—	FintypeCat.carrier CategoryTheory.Functor.obj FintypeCat FintypeCat.instCategory DFunLike.coe FintypeCat.instFunLikeHomCarrier CategoryTheory.ConcreteCategory.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct FintypeCat.concreteCategoryFintype CategoryTheory.Functor.map	—	epi_of_nonempty_of_isConnected surjective_on_fiber_of_epi
surjective_on_fiber_of_epi 📖	mathematical	—	FintypeCat.carrier CategoryTheory.Functor.obj FintypeCat FintypeCat.instCategory DFunLike.coe FintypeCat.instFunLikeHomCarrier CategoryTheory.ConcreteCategory.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct FintypeCat.concreteCategoryFintype CategoryTheory.Functor.map	—	CategoryTheory.surjective_of_epi CategoryTheory.Functor.map_epi CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits CategoryTheory.Limits.FintypeCat.inclusion_preservesFiniteColimits FiberFunctor.preservesEpis

CategoryTheory.PreGaloisCategory.FiberFunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_right 📖	mathematical	—	CategoryTheory.PreGaloisCategory.FiberFunctor CategoryTheory.Functor.comp FintypeCat FintypeCat.instCategory	—	CategoryTheory.Limits.comp_preservesLimitsOfShape preservesTerminalObjects CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence preservesPullbacks CategoryTheory.Limits.comp_preservesFiniteCoproducts preservesFiniteCoproducts CategoryTheory.Limits.instPreservesFiniteCoproductsOfPreservesFiniteColimits CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Functor.preservesEpimorphisms_comp preservesEpis CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Limits.comp_preservesColimitsOfShape instPreservesColimitsOfShapeFintypeCatSingleObjOfFinite CategoryTheory.reflectsIsomorphisms_comp reflectsIsos CategoryTheory.reflectsIsomorphisms_of_full_and_faithful CategoryTheory.Functor.IsEquivalence.full CategoryTheory.Functor.IsEquivalence.faithful
instFaithfulFintypeCat 📖	mathematical	—	CategoryTheory.Functor.Faithful FintypeCat FintypeCat.instCategory	—	CategoryTheory.Limits.eq_of_epi_equalizer CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.PreGaloisCategory.instHasEqualizers CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.isIso_of_reflects_iso CategoryTheory.Limits.FintypeCat.instHasLimitsOfShapeFintypeCatOfFinCategory CategoryTheory.Limits.equalizerComparison_comp_π CategoryTheory.IsIso.comp_isIso CategoryTheory.Limits.instIsIsoEqualizerComparison CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits instPreservesFiniteLimitsFintypeCat CategoryTheory.Limits.equalizer.ι_of_eq reflectsIsos
instPreservesColimitsOfShapeFintypeCatSingleObjOfFinite 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape FintypeCat FintypeCat.instCategory CategoryTheory.SingleObj CategoryTheory.SingleObj.category DivInvMonoid.toMonoid Group.toDivInvMonoid	—	CategoryTheory.Limits.preservesColimitsOfShape_of_equiv preservesQuotientsByFiniteGroups Finite.of_fintype Finite.exists_type_univ_nonempty_mulEquiv
instPreservesFiniteLimitsFintypeCat 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits FintypeCat FintypeCat.instCategory	—	CategoryTheory.Limits.preservesFiniteLimits_of_preservesTerminal_and_pullbacks CategoryTheory.PreGaloisCategory.hasTerminal CategoryTheory.PreGaloisCategory.hasPullbacks preservesTerminalObjects preservesPullbacks
instReflectsColimitsOfShapeFintypeCatDiscretePEmpty 📖	mathematical	—	CategoryTheory.Limits.ReflectsColimitsOfShape FintypeCat FintypeCat.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory	—	CategoryTheory.Limits.reflectsColimitsOfShape_of_reflectsIsomorphisms reflectsIsos CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.PreGaloisCategory.hasFiniteCoproducts Finite.of_fintype CategoryTheory.Limits.instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts preservesFiniteCoproducts
instReflectsLimitsOfShapeFintypeCatDiscretePEmpty 📖	mathematical	—	CategoryTheory.Limits.ReflectsLimitsOfShape FintypeCat FintypeCat.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory	—	CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsIsomorphisms reflectsIsos CategoryTheory.PreGaloisCategory.hasTerminal preservesTerminalObjects
instReflectsMonomorphismsFintypeCat 📖	mathematical	—	CategoryTheory.Functor.ReflectsMonomorphisms FintypeCat FintypeCat.instCategory	—	CategoryTheory.IsKernelPair.mono_of_isIso_fst CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.PreGaloisCategory.hasPullbacks CategoryTheory.Limits.pullback.diagonal_isKernelPair CategoryTheory.isIso_of_reflects_iso CategoryTheory.Limits.has_kernel_pair_of_mono CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit preservesPullbacks CategoryTheory.Limits.PreservesPullback.iso_hom_fst CategoryTheory.IsIso.comp_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.isIso_fst_of_mono reflectsIsos
preservesEpis 📖	mathematical	—	CategoryTheory.Functor.PreservesEpimorphisms FintypeCat FintypeCat.instCategory	—	—
preservesFiniteCoproducts 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteCoproducts FintypeCat FintypeCat.instCategory	—	—
preservesPullbacks 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape FintypeCat FintypeCat.instCategory CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair	—	—
preservesQuotientsByFiniteGroups 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape FintypeCat FintypeCat.instCategory CategoryTheory.SingleObj CategoryTheory.SingleObj.category DivInvMonoid.toMonoid Group.toDivInvMonoid	—	—
preservesTerminalObjects 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape FintypeCat FintypeCat.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory	—	—
reflectsIsos 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms FintypeCat FintypeCat.instCategory	—	—

CategoryTheory.PreGaloisCategory.GaloisCategory

Definitions

Name	Category	Theorems
getFiberFunctor 📖	CompOp	1 math math: CategoryTheory.PreGaloisCategory.instFiberFunctorGetFiberFunctor

CategoryTheory.PreGaloisCategory.IsConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
noTrivialComponent 📖	mathematical	—	CategoryTheory.IsIso	—	—
notInitial 📖	—	—	—	—	—

CategoryTheory.PreGaloisCategory.PreservesIsConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preserves 📖	mathematical	—	CategoryTheory.PreGaloisCategory.IsConnected CategoryTheory.Functor.obj	—	—

---

← Back to Index