Documentation Verification Report

FreeGroupoid

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

Statistics

Metric	Count
Definitions `FreeGroupoid`, `FreeGroupoid`, `instCategory`, `instGroupoid`, `of`, `quotInv`, `redStep`, `toNegPath`, `toPosPath`, `freeGroupoidFunctor`	10
Theorems `congr_comp_reverse`, `congr_reverse`, `congr_reverse_comp`, `instNonempty`, `lift_spec`, `lift_unique`, `of_eq`, `freeGroupoidFunctor_comp`, `freeGroupoidFunctor_id`	9
Total	19

CategoryTheory

Definitions

Name	Category	Theorems
`FreeGroupoid` 📖	CompOp	27 math math: `FreeGroupoid.map_comp_lift`, `Grpd.free_obj`, `FreeGroupoid.lift_comp`, `FreeGroupoid.functorEquiv_apply`, `FreeGroupoid.mapComp_hom_app`, `FreeGroupoid.mapId_hom_app`, `FreeGroupoid.lift_map_homMk`, `FreeGroupoid.liftNatIso_hom_app`, `FreeGroupoid.mapCompLift_inv_app`, `FreeGroupoid.lift_obj_mk`, `FreeGroupoid.map_id`, `FreeGroupoid.map_map_homMk`, `Grpd.freeForgetAdjunction_homEquiv_symm_apply`, `FreeGroupoid.mapComp_inv_app`, `FreeGroupoid.mapId_inv_app`, `FreeGroupoid.liftNatIso_inv_app`, `FreeGroupoid.lift_id_comp_of`, `Grpd.freeForgetAdjunction_homEquiv_apply`, `FreeGroupoid.of_obj_bijective`, `FreeGroupoid.map_obj_mk`, `FreeGroupoid.functorEquiv_symm_apply`, `FreeGroupoid.instIsLocalizationOfTopMorphismProperty`, `FreeGroupoid.of_comp_map`, `FreeGroupoid.lift_spec`, `FreeGroupoid.mapCompLift_hom_app`, `instNonemptyFreeGroupoid`, `FreeGroupoid.map_comp`

Quiver

Definitions

Name	Category	Theorems
`FreeGroupoid` 📖	CompOp	5 math math: `freeGroupoidFunctor_comp`, `FreeGroupoid.lift_spec`, `CategoryTheory.FreeGroupoid.eq_mk`, `FreeGroupoid.instNonempty`, `freeGroupoidFunctor_id`
`freeGroupoidFunctor` 📖	CompOp	2 math math: `freeGroupoidFunctor_comp`, `freeGroupoidFunctor_id`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`freeGroupoidFunctor_comp` 📖	mathematical	—	`freeGroupoidFunctor` `Prefunctor.comp` `CategoryTheory.Functor.comp` `FreeGroupoid` `FreeGroupoid.instCategory`	—	`FreeGroupoid.lift_unique`
`freeGroupoidFunctor_id` 📖	mathematical	—	`freeGroupoidFunctor` `Prefunctor.id` `CategoryTheory.Functor.id` `FreeGroupoid` `FreeGroupoid.instCategory`	—	`FreeGroupoid.lift_unique`

Quiver.FreeGroupoid

Definitions

Name	Category	Theorems
`instCategory` 📖	CompOp	4 math math: `Quiver.freeGroupoidFunctor_comp`, `lift_spec`, `CategoryTheory.FreeGroupoid.eq_mk`, `Quiver.freeGroupoidFunctor_id`
`instGroupoid` 📖	CompOp	—
`of` 📖	CompOp	2 math math: `lift_spec`, `of_eq`
`quotInv` 📖	CompOp	—
`redStep` 📖	CompData	4 math math: `congr_comp_reverse`, `CategoryTheory.FreeGroupoid.eq_mk`, `of_eq`, `congr_reverse_comp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_comp_reverse` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.Paths` `Quiver.Symmetrify` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Paths.categoryPaths` `Quiver.symmetrifyQuiver` `CategoryTheory.HomRel.CompClosure` `redStep` `CategoryTheory.CategoryStruct.comp` `Quiver.Path.reverse` `Quiver.instHasReverseSymmetrify` `CategoryTheory.CategoryStruct.id`	—	`Quot.eqvGen_sound` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.assoc`
`congr_reverse` 📖	mathematical	`CategoryTheory.HomRel.CompClosure` `CategoryTheory.Paths` `Quiver.Symmetrify` `CategoryTheory.Paths.categoryPaths` `Quiver.symmetrifyQuiver` `redStep`	`Quiver.Path.reverse` `Quiver.instHasReverseSymmetrify`	—	`Quiver.Path.nil_comp` `Quiver.Path.reverse_comp` `Quiver.Path.comp_assoc` `Quiver.reverse_reverse`
`congr_reverse_comp` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.Paths` `Quiver.Symmetrify` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Paths.categoryPaths` `Quiver.symmetrifyQuiver` `CategoryTheory.HomRel.CompClosure` `redStep` `CategoryTheory.CategoryStruct.comp` `Quiver.Path.reverse` `Quiver.instHasReverseSymmetrify` `CategoryTheory.CategoryStruct.id`	—	`Quiver.Path.reverse_reverse` `congr_comp_reverse`
`instNonempty` 📖	mathematical	—	`Quiver.FreeGroupoid`	—	—
`lift_spec` 📖	mathematical	—	`Prefunctor.comp` `Quiver.FreeGroupoid` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.Groupoid.toCategory` `of` `CategoryTheory.Functor.toPrefunctor` `lift`	—	`of_eq` `Prefunctor.comp_assoc` `CategoryTheory.Functor.toPrefunctor_comp` `CategoryTheory.Quotient.lift_spec` `CategoryTheory.Paths.lift_spec` `Quiver.Symmetrify.lift_spec`
`lift_unique` 📖	mathematical	`Prefunctor.comp` `Quiver.FreeGroupoid` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.Groupoid.toCategory` `of` `CategoryTheory.Functor.toPrefunctor`	`lift`	—	`CategoryTheory.Quotient.lift_unique` `CategoryTheory.Paths.lift_unique` `Quiver.Symmetrify.lift_unique` `CategoryTheory.Functor.toPrefunctor_comp` `CategoryTheory.IsGroupoid.all_isIso` `CategoryTheory.instIsGroupoid` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Functor.map_inv` `CategoryTheory.IsIso.of_groupoid` `CategoryTheory.Groupoid.inv_eq_inv`
`of_eq` 📖	mathematical	—	`of` `Prefunctor.comp` `CategoryTheory.Paths` `Quiver.Symmetrify` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Paths.categoryPaths` `Quiver.symmetrifyQuiver` `CategoryTheory.Quotient` `redStep` `CategoryTheory.Quotient.category` `Quiver.Symmetrify.of` `CategoryTheory.Paths.of` `CategoryTheory.Functor.toPrefunctor` `CategoryTheory.Quotient.functor`	—	—

Quiver.Hom

Definitions

Name	Category	Theorems
`toNegPath` 📖	CompOp	—
`toPosPath` 📖	CompOp	—

---

← Back to Index