Action

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

Statistics

Metric	Count
Definitions functorToAction, instMulActionAutObjFiniteVFintypeCatFunctorObjActionFunctorToAction	2
Theorems functorToAction_comp_forget₂_eq, functorToAction_map, instFaithfulActionFintypeCatAutFunctorFunctorToAction, instIsPretransitiveAutObjFiniteVFintypeCatFunctorObjActionFunctorToActionOfIsGalois, instPreservesColimitsOfShapeActionFintypeCatAutFunctorSingleObjFunctorToActionOfFinite, instPreservesFiniteCoproductsActionFintypeCatAutFunctorFunctorToAction, instPreservesFiniteProductsActionFintypeCatAutFunctorFunctorToAction, instPreservesIsConnectedActionFintypeCatAutFunctorFunctorToAction, instPreservesMonomorphismsActionFintypeCatAutFunctorFunctorToAction, instReflectsIsomorphismsActionFintypeCatAutFunctorFunctorToAction, instReflectsMonomorphismsActionFintypeCatAutFunctorFunctorToAction	11
Total	13

CategoryTheory.PreGaloisCategory

Definitions

Name	Category	Theorems
functorToAction 📖	CompOp	18 math math: instFaithfulActionFintypeCatAutFunctorFunctorToAction, functorToContAction_map, instPreservesIsConnectedActionFintypeCatAutFunctorFunctorToAction, exists_lift_of_continuous, instIsPretransitiveAutObjFiniteVFintypeCatFunctorObjActionFunctorToActionOfIsGalois, exists_lift_of_mono_of_isConnected, instPreservesColimitsOfShapeActionFintypeCatAutFunctorSingleObjFunctorToActionOfFinite, functorToAction_map, instPreservesFiniteCoproductsActionFintypeCatAutFunctorFunctorToAction, instPreservesMonomorphismsActionFintypeCatAutFunctorFunctorToAction, instReflectsIsomorphismsActionFintypeCatAutFunctorFunctorToAction, exists_lift_of_mono, functorToContAction_obj_obj, exists_lift_of_quotient_openSubgroup, instReflectsMonomorphismsActionFintypeCatAutFunctorFunctorToAction, functorToAction_full, instPreservesFiniteProductsActionFintypeCatAutFunctorFunctorToAction, functorToAction_comp_forget₂_eq
instMulActionAutObjFiniteVFintypeCatFunctorObjActionFunctorToAction 📖	CompOp	1 math math: instIsPretransitiveAutObjFiniteVFintypeCatFunctorObjActionFunctorToActionOfIsGalois

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functorToAction_comp_forget₂_eq 📖	mathematical	—	CategoryTheory.Functor.comp Action FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup Action.instCategory functorToAction CategoryTheory.forget₂ Action.HomSubtype Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Types.instFunLike FintypeCat.concreteCategoryFintype Action.V Action.instFunLikeHomSubtypeV Action.instConcreteCategoryHomSubtypeV Action.hasForgetToV	—	—
functorToAction_map 📖	mathematical	—	Action.Hom.hom FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup CategoryTheory.Functor.obj Action Action.instCategory functorToAction CategoryTheory.Functor.map	—	—
instFaithfulActionFintypeCatAutFunctorFunctorToAction 📖	mathematical	—	CategoryTheory.Functor.Faithful Action FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup Action.instCategory functorToAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory CategoryTheory.Functor.Faithful.of_comp
instIsPretransitiveAutObjFiniteVFintypeCatFunctorObjActionFunctorToActionOfIsGalois 📖	mathematical	—	MulAction.IsPretransitive CategoryTheory.Aut CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.types Finite Action.V FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup CategoryTheory.Functor.obj Action Action.instCategory functorToAction SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction instMulActionAutObjFiniteVFintypeCatFunctorObjActionFunctorToAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory isPretransitive_of_isGalois
instPreservesColimitsOfShapeActionFintypeCatAutFunctorSingleObjFunctorToActionOfFinite 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape Action FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup Action.instCategory CategoryTheory.SingleObj CategoryTheory.SingleObj.category functorToAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory Action.preservesColimitsOfShape_of_preserves
instPreservesFiniteCoproductsActionFintypeCatAutFunctorFunctorToAction 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteCoproducts Action FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup Action.instCategory functorToAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory Action.preservesColimitsOfShape_of_preserves
instPreservesFiniteProductsActionFintypeCatAutFunctorFunctorToAction 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteProducts Action FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup Action.instCategory functorToAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory Action.preservesLimitsOfShape_of_preserves
instPreservesIsConnectedActionFintypeCatAutFunctorFunctorToAction 📖	mathematical	—	PreservesIsConnected Action FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup Action.instCategory functorToAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory CategoryTheory.FintypeCat.Action.isConnected_of_transitive FiberFunctor.isPretransitive_of_isConnected nonempty_fiber_of_isConnected
instPreservesMonomorphismsActionFintypeCatAutFunctorFunctorToAction 📖	mathematical	—	CategoryTheory.Functor.PreservesMonomorphisms Action FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup Action.instCategory functorToAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory CategoryTheory.Functor.preservesMonomorphisms_of_preserves_of_reflects FiberFunctor.instReflectsMonomorphismsFintypeCat CategoryTheory.FintypeCat.instPreGaloisCategoryActionFintypeCat CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeHomObjFiniteV
instReflectsIsomorphismsActionFintypeCatAutFunctorFunctorToAction 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms Action FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup Action.instCategory functorToAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory CategoryTheory.Functor.map_isIso CategoryTheory.isIso_of_reflects_iso FiberFunctor.reflectsIsos
instReflectsMonomorphismsActionFintypeCatAutFunctorFunctorToAction 📖	mathematical	—	CategoryTheory.Functor.ReflectsMonomorphisms Action FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup Action.instCategory functorToAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory CategoryTheory.Functor.reflectsMonomorphisms_of_faithful instFaithfulActionFintypeCatAutFunctorFunctorToAction

---

← Back to Index