Documentation Verification Report

Action

📁 Source: Mathlib/CategoryTheory/Action.lean

Statistics

Metric	Count
Definitions `ActionCategory`, `back`, `curry`, `endMulEquivSubgroup`, `homOfPair`, `instCoeTC`, `instGroupoid`, `instInhabited`, `objEquiv`, `stabilizerIsoEnd`, `uncurry`, `π`, `actionAsFunctor`, `instCategoryActionCategory`	14
Theorems `back_coe`, `coe_back`, `comp_val`, `curry_apply_left`, `curry_apply_right`, `val`, `hom_as_subtype`, `id_val`, `instIsConnectedOfIsPretransitiveOfNonempty`, `instNonempty`, `stabilizerIsoEnd_apply`, `stabilizerIsoEnd_symm_apply`, `uncurry_map`, `uncurry_obj`, `π_map`, `π_obj`, `actionAsFunctor_map`, `actionAsFunctor_obj`	18
Total	32

CategoryTheory

Definitions

Name	Category	Theorems
`ActionCategory` 📖	CompOp	12 math math: `ActionCategory.uncurry_map`, `ActionCategory.instNonempty`, `ActionCategory.π_obj`, `ActionCategory.curry_apply_left`, `ActionCategory.comp_val`, `ActionCategory.uncurry_obj`, `ActionCategory.id_val`, `ActionCategory.stabilizerIsoEnd_apply`, `ActionCategory.π_map`, `ActionCategory.instIsConnectedOfIsPretransitiveOfNonempty`, `ActionCategory.hom_as_subtype`, `ActionCategory.stabilizerIsoEnd_symm_apply`
`actionAsFunctor` 📖	CompOp	12 math math: `actionAsFunctor_map`, `ActionCategory.uncurry_map`, `ActionCategory.coe_back`, `ActionCategory.back_coe`, `ActionCategory.curry_apply_left`, `actionAsFunctor_obj`, `ActionCategory.comp_val`, `ActionCategory.id_val`, `ActionCategory.stabilizerIsoEnd_apply`, `ActionCategory.homOfPair.val`, `ActionCategory.π_map`, `ActionCategory.stabilizerIsoEnd_symm_apply`
`instCategoryActionCategory` 📖	CompOp	11 math math: `ActionCategory.uncurry_map`, `ActionCategory.π_obj`, `ActionCategory.curry_apply_left`, `ActionCategory.comp_val`, `ActionCategory.uncurry_obj`, `ActionCategory.id_val`, `ActionCategory.stabilizerIsoEnd_apply`, `ActionCategory.π_map`, `ActionCategory.instIsConnectedOfIsPretransitiveOfNonempty`, `ActionCategory.hom_as_subtype`, `ActionCategory.stabilizerIsoEnd_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`actionAsFunctor_map` 📖	mathematical	—	`Functor.map` `SingleObj` `SingleObj.category` `types` `actionAsFunctor` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	—
`actionAsFunctor_obj` 📖	mathematical	—	`Functor.obj` `SingleObj` `SingleObj.category` `types` `actionAsFunctor`	—	—

CategoryTheory.ActionCategory

Definitions

Name	Category	Theorems
`back` 📖	CompOp	4 math math: `uncurry_map`, `coe_back`, `back_coe`, `hom_as_subtype`
`curry` 📖	CompOp	2 math math: `curry_apply_left`, `curry_apply_right`
`endMulEquivSubgroup` 📖	CompOp	—
`homOfPair` 📖	CompOp	2 math math: `curry_apply_left`, `homOfPair.val`
`instCoeTC` 📖	CompOp	—
`instGroupoid` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`objEquiv` 📖	CompOp	—
`stabilizerIsoEnd` 📖	CompOp	2 math math: `stabilizerIsoEnd_apply`, `stabilizerIsoEnd_symm_apply`
`uncurry` 📖	CompOp	2 math math: `uncurry_map`, `uncurry_obj`
`π` 📖	CompOp	2 math math: `π_obj`, `π_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`back_coe` 📖	mathematical	—	`CategoryTheory.SingleObj` `CategoryTheory.Functor.obj` `CategoryTheory.SingleObj.category` `CategoryTheory.types` `CategoryTheory.actionAsFunctor` `back`	—	—
`coe_back` 📖	mathematical	—	`back` `CategoryTheory.SingleObj` `CategoryTheory.Functor.obj` `CategoryTheory.SingleObj.category` `CategoryTheory.types` `CategoryTheory.actionAsFunctor`	—	—
`comp_val` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.SingleObj` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.SingleObj.category` `CategoryTheory.Functor.obj` `CategoryTheory.types` `CategoryTheory.actionAsFunctor` `CategoryTheory.Functor.map` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.ActionCategory` `CategoryTheory.instCategoryActionCategory` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`curry_apply_left` 📖	mathematical	—	`SemidirectProduct.left` `Pi.group` `mulAutArrow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `DFunLike.coe` `MonoidHom` `SemidirectProduct` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `SemidirectProduct.instGroup` `MonoidHom.instFunLike` `curry` `CategoryTheory.Functor.map` `CategoryTheory.ActionCategory` `CategoryTheory.instCategoryActionCategory` `CategoryTheory.SingleObj` `CategoryTheory.SingleObj.category` `CategoryTheory.Functor.obj` `CategoryTheory.types` `CategoryTheory.actionAsFunctor` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `homOfPair`	—	—
`curry_apply_right` 📖	mathematical	—	`SemidirectProduct.right` `Pi.group` `mulAutArrow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `DFunLike.coe` `MonoidHom` `SemidirectProduct` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `SemidirectProduct.instGroup` `MonoidHom.instFunLike` `curry`	—	—
`hom_as_subtype` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.ActionCategory` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.instCategoryActionCategory` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `back`	—	—
`id_val` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.SingleObj` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.SingleObj.category` `CategoryTheory.Functor.obj` `CategoryTheory.types` `CategoryTheory.actionAsFunctor` `CategoryTheory.Functor.map` `CategoryTheory.CategoryStruct.id` `CategoryTheory.ActionCategory` `CategoryTheory.instCategoryActionCategory` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`instIsConnectedOfIsPretransitiveOfNonempty` 📖	mathematical	—	`CategoryTheory.IsConnected` `CategoryTheory.ActionCategory` `CategoryTheory.instCategoryActionCategory`	—	`CategoryTheory.zigzag_isConnected` `instNonempty` `Relation.ReflTransGen.single` `nonempty_subtype` `MulAction.exists_smul_eq`
`instNonempty` 📖	mathematical	—	`CategoryTheory.ActionCategory`	—	`Nonempty.map`
`stabilizerIsoEnd_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `MulAction.stabilizerSubmonoid` `CategoryTheory.End` `CategoryTheory.ActionCategory` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.instCategoryActionCategory` `CategoryTheory.SingleObj` `CategoryTheory.Functor.obj` `CategoryTheory.SingleObj.category` `CategoryTheory.types` `CategoryTheory.actionAsFunctor` `Submonoid.mul` `CategoryTheory.End.mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `stabilizerIsoEnd`	—	—
`stabilizerIsoEnd_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `CategoryTheory.End` `CategoryTheory.ActionCategory` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.instCategoryActionCategory` `CategoryTheory.SingleObj` `CategoryTheory.Functor.obj` `CategoryTheory.SingleObj.category` `CategoryTheory.types` `CategoryTheory.actionAsFunctor` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `MulAction.stabilizerSubmonoid` `CategoryTheory.End.mul` `Submonoid.mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `stabilizerIsoEnd`	—	—
`uncurry_map` 📖	mathematical	`SemidirectProduct.right` `Pi.group` `mulAutArrow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `DFunLike.coe` `MonoidHom` `SemidirectProduct` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `SemidirectProduct.instGroup` `MonoidHom.instFunLike`	`CategoryTheory.Functor.map` `CategoryTheory.ActionCategory` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.instCategoryActionCategory` `CategoryTheory.SingleObj` `CategoryTheory.SingleObj.category` `uncurry` `SemidirectProduct.left` `Pi.group` `mulAutArrow` `DFunLike.coe` `MonoidHom` `SemidirectProduct` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `SemidirectProduct.instGroup` `MonoidHom.instFunLike` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.types` `CategoryTheory.actionAsFunctor` `back`	—	—
`uncurry_obj` 📖	mathematical	`SemidirectProduct.right` `Pi.group` `mulAutArrow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `DFunLike.coe` `MonoidHom` `SemidirectProduct` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `SemidirectProduct.instGroup` `MonoidHom.instFunLike`	`CategoryTheory.Functor.obj` `CategoryTheory.ActionCategory` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.instCategoryActionCategory` `CategoryTheory.SingleObj` `CategoryTheory.SingleObj.category` `uncurry`	—	—
`π_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.ActionCategory` `CategoryTheory.instCategoryActionCategory` `CategoryTheory.SingleObj` `CategoryTheory.SingleObj.category` `π` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.types` `CategoryTheory.actionAsFunctor`	—	—
`π_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.ActionCategory` `CategoryTheory.instCategoryActionCategory` `CategoryTheory.SingleObj` `CategoryTheory.SingleObj.category` `π` `CategoryTheory.SingleObj.star`	—	—

CategoryTheory.ActionCategory.homOfPair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`val` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.SingleObj` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.SingleObj.category` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.Functor.obj` `CategoryTheory.types` `CategoryTheory.actionAsFunctor` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `CategoryTheory.Functor.map` `CategoryTheory.ActionCategory.homOfPair`	—	—

---

← Back to Index