VertexGroup

📁 Source: Mathlib/CategoryTheory/Groupoid/VertexGroup.lean

Statistics

Metric	Count
Definitions mapVertexGroup, vertexGroup, vertexGroupIsomOfMap, vertexGroupIsomOfPath	4
Theorems mapVertexGroup_apply, inv_eq_inv, vertexGroupIsomOfMap_apply, vertexGroupIsomOfMap_symm_apply, vertexGroup_inv, vertexGroup_mul, vertexGroup_one	7
Total	11

CategoryTheory.Groupoid

Definitions

Name	Category	Theorems
vertexGroup 📖	CompOp	8 math math: vertexGroup.inv_eq_inv, vertexGroup_inv, vertexGroup_one, CategoryTheory.Functor.mapVertexGroup_apply, vertexGroupIsomOfMap_apply, vertexGroupIsomOfMap_symm_apply, CategoryTheory.Subgroupoid.IsNormal.vertexSubgroup, vertexGroup_mul
vertexGroupIsomOfMap 📖	CompOp	2 math math: vertexGroupIsomOfMap_apply, vertexGroupIsomOfMap_symm_apply
vertexGroupIsomOfPath 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
vertexGroupIsomOfMap_apply 📖	mathematical	—	DFunLike.coe MulEquiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct toCategory MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid vertexGroup EquivLike.toFunLike MulEquiv.instEquivLike vertexGroupIsomOfMap CategoryTheory.CategoryStruct.comp inv	—	—
vertexGroupIsomOfMap_symm_apply 📖	mathematical	—	DFunLike.coe MulEquiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct toCategory MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid vertexGroup EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm vertexGroupIsomOfMap CategoryTheory.CategoryStruct.comp inv	—	—
vertexGroup_inv 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct toCategory DivInvMonoid.toInv Group.toDivInvMonoid vertexGroup inv	—	—
vertexGroup_mul 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct toCategory MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid vertexGroup CategoryTheory.CategoryStruct.comp	—	—
vertexGroup_one 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct toCategory MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid vertexGroup CategoryTheory.CategoryStruct.id	—	—

CategoryTheory.Groupoid.CategoryTheory.Functor

Definitions

Name	Category	Theorems
mapVertexGroup 📖	CompOp	1 math math: mapVertexGroup_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapVertexGroup_apply 📖	mathematical	—	DFunLike.coe MonoidHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory CategoryTheory.Functor.obj MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Groupoid.vertexGroup MonoidHom.instFunLike mapVertexGroup CategoryTheory.Functor.map	—	—

CategoryTheory.Groupoid.vertexGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inv_eq_inv 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid CategoryTheory.Groupoid.vertexGroup CategoryTheory.inv CategoryTheory.IsGroupoid.all_isIso CategoryTheory.instIsGroupoid	—	CategoryTheory.Groupoid.inv_eq_inv

---

← Back to Index