Documentation Verification Report

NielsenSchreier

📁 Source: Mathlib/GroupTheory/FreeGroup/NielsenSchreier.lean

Statistics

Metric	Count
Definitions `IsFreeGroupoid`, `functorOfMonoidHom`, `homOfPath`, `loopOfHom`, `treeHom`, `actionGroupoidIsFree`, `of`, `quiverGenerators`	8
Theorems `endIsFree`, `functorOfMonoidHom_map`, `functorOfMonoidHom_obj`, `loopOfHom_eq_id`, `treeHom_eq`, `treeHom_root`, `endIsFreeOfConnectedFree`, `ext_functor`, `ext_functor_iff`, `generators_connected`, `path_nonempty_of_hom`, `unique_lift`, `subgroupIsFreeOfIsFree`	13
Total	21

IsFreeGroupoid

Definitions

Name	Category	Theorems
`actionGroupoidIsFree` 📖	CompOp	—
`of` 📖	CompOp	2 math math: `SpanningTree.loopOfHom_eq_id`, `ext_functor_iff`
`quiverGenerators` 📖	CompOp	2 math math: `path_nonempty_of_hom`, `generators_connected`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`endIsFreeOfConnectedFree` 📖	mathematical	—	`IsFreeGroup` `CategoryTheory.End` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Groupoid.toCategory` `CategoryTheory.End.group`	—	`SpanningTree.endIsFree` `generators_connected`
`ext_functor` 📖	—	`CategoryTheory.Functor.map` `CategoryTheory.Groupoid.toCategory` `CategoryTheory.SingleObj` `CategoryTheory.SingleObj.category` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `of`	—	—	`unique_lift` `trans` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `eq_isEquiv`
`ext_functor_iff` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Groupoid.toCategory` `CategoryTheory.SingleObj` `CategoryTheory.SingleObj.category` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `of`	—	`ext_functor`
`generators_connected` 📖	mathematical	—	`Quiver.RootedConnected` `Quiver.Symmetrify` `Generators` `Quiver.symmetrifyQuiver` `quiverGenerators`	—	`path_nonempty_of_hom` `CategoryTheory.nonempty_hom_of_preconnected_groupoid` `CategoryTheory.IsConnected.toIsPreconnected`
`path_nonempty_of_hom` 📖	mathematical	—	`Quiver.Path` `Quiver.Symmetrify` `Generators` `Quiver.symmetrifyQuiver` `quiverGenerators`	—	`Quiver.WeaklyConnectedComponent.eq` `FreeGroup.of_injective` `mul_inv_eq_one` `ext_functor` `CategoryTheory.Functor.const_obj_map` `CategoryTheory.SingleObj.id_as_one` `CategoryTheory.SingleObj.differenceFunctor_map`
`unique_lift` 📖	mathematical	—	`ExistsUnique` `CategoryTheory.Functor` `CategoryTheory.Groupoid.toCategory` `CategoryTheory.SingleObj` `CategoryTheory.SingleObj.category` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—

IsFreeGroupoid.SpanningTree

Definitions

Name	Category	Theorems
`functorOfMonoidHom` 📖	CompOp	2 math math: `functorOfMonoidHom_map`, `functorOfMonoidHom_obj`
`homOfPath` 📖	CompOp	1 math math: `treeHom_eq`
`loopOfHom` 📖	CompOp	2 math math: `functorOfMonoidHom_map`, `loopOfHom_eq_id`
`treeHom` 📖	CompOp	2 math math: `treeHom_eq`, `treeHom_root`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`endIsFree` 📖	mathematical	—	`IsFreeGroup` `CategoryTheory.End` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Groupoid.toCategory` `CategoryTheory.End.group`	—	`IsFreeGroup.ofUniqueLift` `IsFreeGroupoid.unique_lift` `homOfPath.eq_1` `CategoryTheory.Functor.map_id` `CategoryTheory.SingleObj.id_as_one` `homOfPath.eq_2` `CategoryTheory.Functor.map_comp` `CategoryTheory.SingleObj.comp_as_mul` `mul_one` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Functor.map_inv` `CategoryTheory.IsGroupoid.all_isIso` `CategoryTheory.instIsGroupoid` `CategoryTheory.SingleObj.inv_as_inv` `inv_eq_one` `CategoryTheory.inv.congr_simp` `inv_one` `one_mul` `CategoryTheory.Functor.mapEnd_apply` `MonoidHom.ext` `loopOfHom_eq_id` `CategoryTheory.End.one_def` `MonoidHom.map_one` `treeHom_root` `CategoryTheory.IsIso.inv_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`functorOfMonoidHom_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Groupoid.toCategory` `CategoryTheory.SingleObj` `CategoryTheory.SingleObj.category` `functorOfMonoidHom` `DFunLike.coe` `MonoidHom` `CategoryTheory.End` `CategoryTheory.Category.toCategoryStruct` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CategoryTheory.End.monoid` `MonoidHom.instFunLike` `loopOfHom`	—	—
`functorOfMonoidHom_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Groupoid.toCategory` `CategoryTheory.SingleObj` `CategoryTheory.SingleObj.category` `functorOfMonoidHom`	—	—
`loopOfHom_eq_id` 📖	mathematical	`Quiver.Hom` `IsFreeGroupoid.Generators` `IsFreeGroupoid.quiverGenerators` `Set` `Set.instMembership` `Quiver.wideSubquiverSymmetrify`	`loopOfHom` `IsFreeGroupoid.of` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Groupoid.toCategory`	—	`loopOfHom.eq_1` `CategoryTheory.Category.assoc` `CategoryTheory.IsIso.comp_inv_eq` `CategoryTheory.Category.id_comp` `treeHom_eq` `homOfPath.eq_2` `CategoryTheory.IsIso.inv_hom_id` `CategoryTheory.Category.comp_id`
`treeHom_eq` 📖	mathematical	—	`treeHom` `homOfPath`	—	`treeHom.eq_1` `Unique.default_eq`
`treeHom_root` 📖	mathematical	—	`treeHom` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Groupoid.toCategory`	—	`trans` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `eq_isEquiv` `treeHom_eq`

(root)

Definitions

Name	Category	Theorems
`IsFreeGroupoid` 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subgroupIsFreeOfIsFree` 📖	mathematical	—	`IsFreeGroup` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup`	—	`IsFreeGroup.ofMulEquiv` `MulAction.left_quotientAction` `IsFreeGroupoid.endIsFreeOfConnectedFree` `CategoryTheory.ActionCategory.instIsConnectedOfIsPretransitiveOfNonempty` `MulAction.isPretransitive_quotient`

---

← Back to Index