Documentation Verification Report

Concrete

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

Statistics

Metric	Count
Definitions `instMulActionCarrierOf`, `ofMulAction`, `quotientToEndHom`, `quotientToQuotientOfLE`, `toEndHom`, `«term_⧸ₐ_»`, `diagonal`, `diagonalOneIsoLeftRegular`, `instMulAction`, `instMulActionCarrierVFintypeCat`, `leftRegular`, `ofMulAction`, `ofMulActionLimitCone`	13
Theorems `ofMulAction_apply`, `quotientToEndHom_mk`, `quotientToQuotientOfLE_hom_mk`, `toEndHom_apply`, `toEndHom_trivial_of_mem`, `ofMulAction_V`, `ofMulAction_apply`, `ofMulAction_ρ`, `ρ_inv_self_apply`, `ρ_self_inv_apply`	10
Total	23

Action

Definitions

Name	Category	Theorems
`diagonal` 📖	CompOp	4 math math: `diagonalSuccIsoTensorDiagonal_inv_hom`, `diagonalSuccIsoTensorTrivial_inv_hom_apply`, `diagonalSuccIsoTensorDiagonal_hom_hom`, `diagonalSuccIsoTensorTrivial_hom_hom_apply`
`diagonalOneIsoLeftRegular` 📖	CompOp	—
`instMulAction` 📖	CompOp	—
`instMulActionCarrierVFintypeCat` 📖	CompOp	2 math math: `CategoryTheory.FintypeCat.Action.pretransitive_of_isConnected`, `CategoryTheory.FintypeCat.Action.isConnected_iff_transitive`
`leftRegular` 📖	CompOp	6 math math: `leftRegularTensorIso_inv_hom`, `diagonalSuccIsoTensorDiagonal_inv_hom`, `diagonalSuccIsoTensorTrivial_inv_hom_apply`, `leftRegularTensorIso_hom_hom`, `diagonalSuccIsoTensorDiagonal_hom_hom`, `diagonalSuccIsoTensorTrivial_hom_hom_apply`
`ofMulAction` 📖	CompOp	5 math math: `ofMulAction_apply`, `classifyingSpaceUniversalCover_map`, `ofMulAction_ρ`, `ofMulAction_V`, `classifyingSpaceUniversalCover_obj`
`ofMulActionLimitCone` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofMulAction_V` 📖	mathematical	—	`V` `CategoryTheory.types` `ofMulAction`	—	—
`ofMulAction_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `CategoryTheory.End` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.types` `V` `ofMulAction` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CategoryTheory.End.monoid` `MonoidHom.instFunLike` `ρ` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	—
`ofMulAction_ρ` 📖	mathematical	—	`ρ` `CategoryTheory.types` `ofMulAction` `MulAction.toEndHom`	—	—
`ρ_inv_self_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `CategoryTheory.End` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.types` `V` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CategoryTheory.End.monoid` `MonoidHom.instFunLike` `ρ` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `inv_mul_cancel` `map_one` `MonoidHomClass.toOneHomClass`
`ρ_self_inv_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `CategoryTheory.End` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.types` `V` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CategoryTheory.End.monoid` `MonoidHom.instFunLike` `ρ` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `mul_inv_cancel` `map_one` `MonoidHomClass.toOneHomClass`

Action.FintypeCat

Definitions

Name	Category	Theorems
`instMulActionCarrierOf` 📖	CompOp	—
`ofMulAction` 📖	CompOp	8 math math: `toEndHom_apply`, `quotientToEndHom_mk`, `CategoryTheory.PreGaloisCategory.has_decomp_quotients`, `quotientToQuotientOfLE_hom_mk`, `CategoryTheory.PreGaloisCategory.exists_lift_of_quotient_openSubgroup`, `CategoryTheory.FintypeCat.Action.isConnected_of_transitive`, `toEndHom_trivial_of_mem`, `ofMulAction_apply`
`quotientToEndHom` 📖	CompOp	1 math math: `quotientToEndHom_mk`
`quotientToQuotientOfLE` 📖	CompOp	1 math math: `quotientToQuotientOfLE_hom_mk`
`toEndHom` 📖	CompOp	2 math math: `toEndHom_apply`, `toEndHom_trivial_of_mem`
`«term_⧸ₐ_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofMulAction_apply` 📖	mathematical	—	`DFunLike.coe` `Action.V` `FintypeCat` `FintypeCat.instCategory` `ofMulAction` `FintypeCat.carrier` `FintypeCat.instFunLikeHomCarrier` `CategoryTheory.ConcreteCategory.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `FintypeCat.concreteCategoryFintype` `MonoidHom` `CategoryTheory.End` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CategoryTheory.End.monoid` `MonoidHom.instFunLike` `Action.ρ` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	—
`quotientToEndHom_mk` 📖	mathematical	—	`DFunLike.coe` `Action.V` `FintypeCat` `FintypeCat.instCategory` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `ofMulAction` `FintypeCat.of` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `MulAction.quotient` `Monoid.toMulAction` `MulAction.left_quotientAction` `FintypeCat.carrier` `FintypeCat.instFunLikeHomCarrier` `CategoryTheory.ConcreteCategory.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `FintypeCat.concreteCategoryFintype` `Action.Hom.hom` `MonoidHom` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `Subgroup.subgroupOf` `CategoryTheory.End` `Action` `Action.instCategory` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `QuotientGroup.Quotient.group` `Subgroup.normal_subgroupOf` `CategoryTheory.End.monoid` `MonoidHom.instFunLike` `quotientToEndHom` `QuotientGroup.leftRel` `MulOne.toMul` `Subgroup.inv`	—	`MulAction.left_quotientAction` `Subgroup.normal_subgroupOf`
`quotientToQuotientOfLE_hom_mk` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder`	`DFunLike.coe` `Action.V` `FintypeCat` `FintypeCat.instCategory` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `ofMulAction` `FintypeCat.of` `HasQuotient.Quotient` `QuotientGroup.instHasQuotientSubgroup` `MulAction.quotient` `Monoid.toMulAction` `MulAction.left_quotientAction` `FintypeCat.carrier` `FintypeCat.instFunLikeHomCarrier` `CategoryTheory.ConcreteCategory.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `FintypeCat.concreteCategoryFintype` `Action.Hom.hom` `quotientToQuotientOfLE` `QuotientGroup.leftRel`	—	`MulAction.left_quotientAction`
`toEndHom_apply` 📖	mathematical	—	`DFunLike.coe` `Action.V` `FintypeCat` `FintypeCat.instCategory` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `ofMulAction` `FintypeCat.of` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `MulAction.quotient` `Monoid.toMulAction` `MulAction.left_quotientAction` `FintypeCat.carrier` `FintypeCat.instFunLikeHomCarrier` `CategoryTheory.ConcreteCategory.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `FintypeCat.concreteCategoryFintype` `Action.Hom.hom` `MonoidHom` `CategoryTheory.End` `Action` `Action.instCategory` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CategoryTheory.End.monoid` `MonoidHom.instFunLike` `toEndHom` `QuotientGroup.leftRel` `MulOne.toMul` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`MulAction.left_quotientAction`
`toEndHom_trivial_of_mem` 📖	mathematical	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike`	`DFunLike.coe` `MonoidHom` `CategoryTheory.End` `Action` `FintypeCat` `FintypeCat.instCategory` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.Category.toCategoryStruct` `Action.instCategory` `ofMulAction` `FintypeCat.of` `HasQuotient.Quotient` `QuotientGroup.instHasQuotientSubgroup` `MulAction.quotient` `Monoid.toMulAction` `MulAction.left_quotientAction` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CategoryTheory.End.monoid` `MonoidHom.instFunLike` `toEndHom` `CategoryTheory.CategoryStruct.id`	—	`Action.hom_ext` `MulAction.left_quotientAction` `FintypeCat.hom_ext` `QuotientGroup.leftRel_apply` `mul_inv_rev` `inv_inv` `inv_mul_cancel_right`

---

← Back to Index