Action

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

Statistics

Metric	Count
Definitions functorToAction, instMulActionAutCarrierVFintypeCatFunctorObjActionFunctorToAction	2
Theorems functorToAction_comp_forget₂_eq, functorToAction_map, instFaithfulActionFintypeCatAutFunctorFunctorToAction, instIsPretransitiveAutCarrierVFintypeCatFunctorObjActionFunctorToActionOfIsGalois, 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, 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, instIsPretransitiveAutCarrierVFintypeCatFunctorObjActionFunctorToActionOfIsGalois, functorToAction_full, instPreservesFiniteProductsActionFintypeCatAutFunctorFunctorToAction, functorToAction_comp_forget₂_eq
instMulActionAutCarrierVFintypeCatFunctorObjActionFunctorToAction 📖	CompOp	1 math math: instIsPretransitiveAutCarrierVFintypeCatFunctorObjActionFunctorToActionOfIsGalois

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functorToAction_comp_forget₂_eq 📖	mathematical	—	CategoryTheory.Functor.comp Action FintypeCat FintypeCat.instCategory 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 FintypeCat.carrier FintypeCat.instFunLikeHomCarrier FintypeCat.concreteCategoryFintype Action.V Action.instFunLikeHomSubtypeV Action.instConcreteCategoryHomSubtypeV Action.hasForgetToV	—	—
functorToAction_map 📖	mathematical	—	Action.Hom.hom FintypeCat FintypeCat.instCategory 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 FintypeCat.instCategory CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup Action.instCategory functorToAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory FiberFunctor.instFaithfulFintypeCat CategoryTheory.Functor.Faithful.of_comp
instIsPretransitiveAutCarrierVFintypeCatFunctorObjActionFunctorToActionOfIsGalois 📖	mathematical	—	MulAction.IsPretransitive CategoryTheory.Aut FintypeCat.carrier Action.V FintypeCat FintypeCat.instCategory 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 instMulActionAutCarrierVFintypeCatFunctorObjActionFunctorToAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory isPretransitive_of_isGalois
instPreservesColimitsOfShapeActionFintypeCatAutFunctorSingleObjFunctorToActionOfFinite 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape Action FintypeCat FintypeCat.instCategory 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 FiberFunctor.instPreservesColimitsOfShapeFintypeCatSingleObjOfFinite
instPreservesFiniteCoproductsActionFintypeCatAutFunctorFunctorToAction 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteCoproducts Action FintypeCat FintypeCat.instCategory CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup Action.instCategory functorToAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory Action.preservesColimitsOfShape_of_preserves CategoryTheory.Limits.instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts Finite.of_fintype FiberFunctor.preservesFiniteCoproducts
instPreservesFiniteProductsActionFintypeCatAutFunctorFunctorToAction 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteProducts Action FintypeCat FintypeCat.instCategory CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup Action.instCategory functorToAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory Action.preservesLimitsOfShape_of_preserves CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits FiberFunctor.instPreservesFiniteLimitsFintypeCat
instPreservesIsConnectedActionFintypeCatAutFunctorFunctorToAction 📖	mathematical	—	PreservesIsConnected Action FintypeCat FintypeCat.instCategory 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 FintypeCat.instCategory CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup Action.instCategory functorToAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape FiberFunctor.preservesPullbacks CategoryTheory.Functor.preservesMonomorphisms_of_preserves_of_reflects FiberFunctor.instReflectsMonomorphismsFintypeCat CategoryTheory.FintypeCat.instPreGaloisCategoryActionFintypeCat CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeHomCarrierV
instReflectsIsomorphismsActionFintypeCatAutFunctorFunctorToAction 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms Action FintypeCat FintypeCat.instCategory 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 FintypeCat.instCategory 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