Examples

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

Statistics

Metric	Count
Definitions imageComplement, imageComplementIncl, imageComplement, imageComplementIncl, isoQuotientStabilizerOfIsConnected	5
Theorems isConnected_iff_transitive, isConnected_of_transitive, pretransitive_of_isConnected, instFiberFunctorActionFintypeCatForget, instFiberFunctorActionFintypeCatForget₂HomSubtypeHomCarrierV, instGaloisCategoryActionFintypeCat, instHasColimitsOfShapeSingleObjFintypeCatOfFinite, instMonoActionFintypeCatImageComplementIncl, instPreGaloisCategoryActionFintypeCat, instPreservesFiniteLimitsActionFintypeCatForgetHomSubtypeHomCarrierV	10
Total	15

CategoryTheory.FintypeCat

Definitions

Name	Category	Theorems
imageComplement 📖	CompOp	—
imageComplementIncl 📖	CompOp	—
isoQuotientStabilizerOfIsConnected 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFiberFunctorActionFintypeCatForget 📖	mathematical	—	CategoryTheory.PreGaloisCategory.FiberFunctor Action FintypeCat FintypeCat.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory instPreGaloisCategoryActionFintypeCat Action.forget	—	instPreGaloisCategoryActionFintypeCat Action.instPreservesLimitsOfShapeForgetOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits CategoryTheory.Limits.FintypeCat.hasFiniteLimits Finite.of_fintype CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits Action.instPreservesColimitsOfShapeForgetOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Limits.FintypeCat.hasFiniteColimits CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits instHasColimitsOfShapeSingleObjFintypeCatOfFinite Action.isIso_of_hom_isIso
instFiberFunctorActionFintypeCatForget₂HomSubtypeHomCarrierV 📖	mathematical	—	CategoryTheory.PreGaloisCategory.FiberFunctor Action FintypeCat FintypeCat.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory instPreGaloisCategoryActionFintypeCat CategoryTheory.forget₂ Action.HomSubtype Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct FintypeCat.carrier FintypeCat.instFunLikeHomCarrier FintypeCat.concreteCategoryFintype Action.V Action.instFunLikeHomSubtypeV Action.instConcreteCategoryHomSubtypeV Action.hasForgetToV	—	instPreGaloisCategoryActionFintypeCat instFiberFunctorActionFintypeCatForget
instGaloisCategoryActionFintypeCat 📖	mathematical	—	CategoryTheory.GaloisCategory Action FintypeCat FintypeCat.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory	—	instPreGaloisCategoryActionFintypeCat instFiberFunctorActionFintypeCatForget
instHasColimitsOfShapeSingleObjFintypeCatOfFinite 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.SingleObj CategoryTheory.SingleObj.category DivInvMonoid.toMonoid Group.toDivInvMonoid FintypeCat FintypeCat.instCategory	—	Finite.exists_type_univ_nonempty_mulEquiv CategoryTheory.Limits.hasColimitsOfShape_of_equivalence CategoryTheory.Limits.FintypeCat.instHasColimitsOfShapeFintypeCatOfFinCategory
instMonoActionFintypeCatImageComplementIncl 📖	mathematical	—	CategoryTheory.Mono Action FintypeCat FintypeCat.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory Action.imageComplement Action.imageComplementIncl	—	CategoryTheory.Functor.mono_of_mono_map CategoryTheory.Functor.reflectsMonomorphisms_of_faithful CategoryTheory.instFaithfulForget CategoryTheory.ConcreteCategory.mono_of_injective Subtype.val_injective
instPreGaloisCategoryActionFintypeCat 📖	mathematical	—	CategoryTheory.PreGaloisCategory Action FintypeCat FintypeCat.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory	—	CategoryTheory.Limits.hasLimitsOfShape_discrete Action.instHasFiniteProducts CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits CategoryTheory.Limits.FintypeCat.hasFiniteLimits Finite.of_fintype CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits Action.instHasFiniteLimits Action.instHasFiniteCoproducts CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Limits.FintypeCat.hasFiniteColimits Action.hasColimitsOfShape instHasColimitsOfShapeSingleObjFintypeCatOfFinite CategoryTheory.Functor.map_mono CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits instPreservesFiniteLimitsActionFintypeCatForgetHomSubtypeHomCarrierV CategoryTheory.Limits.comp_reflectsColimit Action.instReflectsColimitForget CategoryTheory.CreatesColimit.toReflectsColimit
instPreservesFiniteLimitsActionFintypeCatForgetHomSubtypeHomCarrierV 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits Action FintypeCat FintypeCat.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory CategoryTheory.types CategoryTheory.forget Action.HomSubtype Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct FintypeCat.carrier FintypeCat.instFunLikeHomCarrier FintypeCat.concreteCategoryFintype Action.V Action.instFunLikeHomSubtypeV Action.instConcreteCategoryHomSubtypeV	—	CategoryTheory.Limits.comp_preservesFiniteLimits Action.instPreservesFiniteLimitsForgetOfHasFiniteLimits CategoryTheory.Limits.FintypeCat.hasFiniteLimits CategoryTheory.Limits.FintypeCat.inclusion_preservesFiniteLimits

CategoryTheory.FintypeCat.Action

Definitions

Name	Category	Theorems
imageComplement 📖	CompOp	1 math math: CategoryTheory.FintypeCat.instMonoActionFintypeCatImageComplementIncl
imageComplementIncl 📖	CompOp	1 math math: CategoryTheory.FintypeCat.instMonoActionFintypeCatImageComplementIncl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isConnected_iff_transitive 📖	mathematical	—	CategoryTheory.PreGaloisCategory.IsConnected Action FintypeCat FintypeCat.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory MulAction.IsPretransitive FintypeCat.carrier Action.V SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Action.instMulActionCarrierVFintypeCat	—	pretransitive_of_isConnected isConnected_of_transitive
isConnected_of_transitive 📖	mathematical	—	CategoryTheory.PreGaloisCategory.IsConnected Action FintypeCat FintypeCat.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory Action.FintypeCat.ofMulAction	—	CategoryTheory.PreGaloisCategory.not_initial_of_inhabited CategoryTheory.FintypeCat.instPreGaloisCategoryActionFintypeCat CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget CategoryTheory.PreGaloisCategory.not_initial_iff_fiber_nonempty CategoryTheory.ConcreteCategory.isIso_iff_bijective CategoryTheory.reflectsIsomorphisms_of_full_and_faithful FintypeCat.instFullForgetHomCarrier CategoryTheory.instFaithfulForget CategoryTheory.ConcreteCategory.injective_of_mono_of_preservesPullback CategoryTheory.Functor.map_mono CategoryTheory.ConcreteCategory.forget₂_preservesMonomorphisms CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.FintypeCat.instPreservesFiniteLimitsActionFintypeCatForgetHomSubtypeHomCarrierV CategoryTheory.Limits.FintypeCat.instPreservesFiniteLimitsFintypeCatForgetHomCarrier MulAction.exists_smul_eq Action.Hom.comm FintypeCat.comp_apply CategoryTheory.isIso_of_reflects_iso CategoryTheory.Functor.map_isIso Action.isIso_of_hom_isIso CategoryTheory.PreGaloisCategory.FiberFunctor.reflectsIsos
pretransitive_of_isConnected 📖	mathematical	—	MulAction.IsPretransitive FintypeCat.carrier Action.V FintypeCat FintypeCat.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Action.instMulActionCarrierVFintypeCat	—	Subtype.finite Finite.of_fintype CategoryTheory.ConcreteCategory.mono_of_injective Subtype.val_injective CategoryTheory.PreGaloisCategory.IsConnected.noTrivialComponent CategoryTheory.PreGaloisCategory.not_initial_iff_fiber_nonempty CategoryTheory.FintypeCat.instPreGaloisCategoryActionFintypeCat CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget Set.Nonempty.coe_sort MulAction.nonempty_orbit CategoryTheory.ConcreteCategory.isIso_iff_bijective CategoryTheory.reflectsIsomorphisms_of_full_and_faithful FintypeCat.instFullForgetHomCarrier CategoryTheory.instFaithfulForget CategoryTheory.Functor.map_isIso Function.Bijective.surjective

---

← Back to Index