Documentation Verification Report

SingleObj

📁 Source: Mathlib/Combinatorics/Quiver/SingleObj.lean

Statistics

Metric	Count
Definitions `SingleObj`, `hasInvolutiveReverse`, `hasReverse`, `inst`, `listToPath`, `pathEquivList`, `pathToList`, `toHom`, `toPrefunctor`, `instUniqueSingleObj`	10
Theorems `ext`, `listToPath_pathToList`, `pathEquivList_cons`, `pathEquivList_nil`, `pathEquivList_symm_cons`, `pathEquivList_symm_nil`, `pathToList_listToPath`, `toHom_apply`, `toHom_symm_apply`, `toPrefunctor_apply_map`, `toPrefunctor_apply_obj`, `toPrefunctor_comp`, `toPrefunctor_id`, `toPrefunctor_symm_apply`, `toPrefunctor_symm_comp`, `toPrefunctor_symm_id`	16
Total	26

Quiver

Definitions

Name	Category	Theorems
`SingleObj` 📖	CompOp	14 math math: `SingleObj.pathEquivList_nil`, `SingleObj.toPrefunctor_symm_id`, `SingleObj.toPrefunctor_apply_map`, `SingleObj.toPrefunctor_comp`, `SingleObj.pathEquivList_symm_cons`, `SingleObj.toHom_apply`, `SingleObj.toPrefunctor_id`, `SingleObj.toPrefunctor_apply_obj`, `SingleObj.toHom_symm_apply`, `SingleObj.pathEquivList_symm_nil`, `SingleObj.pathEquivList_cons`, `SingleObj.toPrefunctor_symm_comp`, `SingleObj.toPrefunctor_symm_apply`, `SingleObj.listToPath_pathToList`
`instUniqueSingleObj` 📖	CompOp	—

Quiver.SingleObj

Definitions

Name	Category	Theorems
`hasInvolutiveReverse` 📖	CompOp	—
`hasReverse` 📖	CompOp	—
`inst` 📖	CompOp	16 math math: `pathEquivList_nil`, `toPrefunctor_symm_id`, `toPrefunctor_apply_map`, `CategoryTheory.SingleObj.inv_as_inv`, `CategoryTheory.SingleObj.comp_as_mul`, `toPrefunctor_comp`, `pathEquivList_symm_cons`, `toHom_apply`, `toPrefunctor_id`, `toPrefunctor_apply_obj`, `toHom_symm_apply`, `pathEquivList_symm_nil`, `pathEquivList_cons`, `toPrefunctor_symm_comp`, `toPrefunctor_symm_apply`, `listToPath_pathToList`
`listToPath` 📖	CompOp	2 math math: `pathToList_listToPath`, `listToPath_pathToList`
`pathEquivList` 📖	CompOp	4 math math: `pathEquivList_nil`, `pathEquivList_symm_cons`, `pathEquivList_symm_nil`, `pathEquivList_cons`
`pathToList` 📖	CompOp	3 math math: `pathToList_listToPath`, `pathEquivList_cons`, `listToPath_pathToList`
`toHom` 📖	CompOp	3 math math: `toHom_apply`, `toHom_symm_apply`, `toPrefunctor_symm_apply`
`toPrefunctor` 📖	CompOp	7 math math: `toPrefunctor_symm_id`, `toPrefunctor_apply_map`, `toPrefunctor_comp`, `toPrefunctor_id`, `toPrefunctor_apply_obj`, `toPrefunctor_symm_comp`, `toPrefunctor_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	—	—	—	—
`listToPath_pathToList` 📖	mathematical	—	`listToPath` `pathToList` `Quiver.Path.cast` `Quiver.SingleObj` `inst` `star` `ext`	—	`ext`
`pathEquivList_cons` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Path` `Quiver.SingleObj` `inst` `star` `EquivLike.toFunLike` `Equiv.instEquivLike` `pathEquivList` `Quiver.Path.cons` `Quiver.Hom` `pathToList`	—	—
`pathEquivList_nil` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Path` `Quiver.SingleObj` `inst` `star` `EquivLike.toFunLike` `Equiv.instEquivLike` `pathEquivList` `Quiver.Path.nil`	—	—
`pathEquivList_symm_cons` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Path` `Quiver.SingleObj` `inst` `star` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `pathEquivList` `Quiver.Path.cons`	—	—
`pathEquivList_symm_nil` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Path` `Quiver.SingleObj` `inst` `star` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `pathEquivList` `Quiver.Path.nil`	—	—
`pathToList_listToPath` 📖	mathematical	—	`pathToList` `star` `listToPath`	—	—
`toHom_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `Quiver.SingleObj` `inst` `star` `EquivLike.toFunLike` `Equiv.instEquivLike` `toHom`	—	—
`toHom_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `Quiver.SingleObj` `inst` `star` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toHom`	—	—
`toPrefunctor_apply_map` 📖	mathematical	—	`Prefunctor.map` `Quiver.SingleObj` `inst` `DFunLike.coe` `Equiv` `Prefunctor` `EquivLike.toFunLike` `Equiv.instEquivLike` `toPrefunctor`	—	—
`toPrefunctor_apply_obj` 📖	mathematical	—	`Prefunctor.obj` `Quiver.SingleObj` `inst` `DFunLike.coe` `Equiv` `Prefunctor` `EquivLike.toFunLike` `Equiv.instEquivLike` `toPrefunctor`	—	—
`toPrefunctor_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Prefunctor` `Quiver.SingleObj` `inst` `EquivLike.toFunLike` `Equiv.instEquivLike` `toPrefunctor` `Prefunctor.comp`	—	—
`toPrefunctor_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Prefunctor` `Quiver.SingleObj` `inst` `EquivLike.toFunLike` `Equiv.instEquivLike` `toPrefunctor` `Prefunctor.id`	—	—
`toPrefunctor_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Prefunctor` `Quiver.SingleObj` `inst` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toPrefunctor` `Prefunctor.map` `star` `Quiver.Hom` `toHom`	—	—
`toPrefunctor_symm_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Prefunctor` `Quiver.SingleObj` `inst` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toPrefunctor` `Prefunctor.comp`	—	`Equiv.apply_symm_apply`
`toPrefunctor_symm_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Prefunctor` `Quiver.SingleObj` `inst` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toPrefunctor` `Prefunctor.id`	—	—

---

← Back to Index