Documentation Verification Report

ReflQuiver

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

Statistics

Metric	Count
Definitions `toReflPrefunctor`, `ReflPrefunctor`, `comp`, `id`, `instInhabited`, `toPrefunctor`, `«term_⋙rq_»`, `«term_⥤rq_»`, `«term𝟭rq»`, `ReflQuiver`, `discreteReflQuiver`, `id`, `opposite`, `toQuiver`, `catToReflQuiver`, `«term𝟙rq»`	16
Theorems `map_comp`, `toReflPrefunctor_toPrefunctor`, `comp_assoc`, `comp_id`, `comp_map`, `comp_obj`, `congr_hom`, `congr_map`, `congr_obj`, `ext`, `ext'`, `id_comp`, `id_map`, `id_obj`, `map_id`, `mk_map`, `mk_obj`, `homOfEq_id`, `id_eq_id`	19
Total	35

CategoryTheory

Definitions

Name	Category	Theorems
`ReflPrefunctor` 📖	CompData	4 math math: `ReflQuiv.adj.homEquiv_symm_apply`, `ReflQuiv.adj.homEquiv_naturality_left_symm`, `ReflQuiv.adj.homEquiv_apply`, `ReflQuiv.adj.homEquiv_naturality_right`
`ReflQuiver` 📖	CompData	18 math math: `SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_map`, `ReflQuiv.adj_homEquiv`, `Cat.freeRefl_map`, `ReflQuiv.id_map`, `ReflQuiv.comp_map`, `SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj`, `ReflQuiv.comp_eq_comp`, `ReflQuiv.adj.unit.map_app_eq`, `SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_obj`, `ReflQuiv.forgetToQuiv_obj`, `ReflQuiv.comp_obj`, `ReflQuiv.of_val`, `ReflQuiv.forgetToQuiv_map`, `ReflQuiv.id_eq_id`, `ReflQuiv.id_obj`, `Cat.freeRefl_obj`, `SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_map`, `SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map`
`catToReflQuiver` 📖	CompOp	23 math math: `SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_map`, `ReflQuiv.adj.homEquiv_symm_apply`, `SSet.OneTruncation₂.nerveHomEquiv_id`, `Cat.FreeRefl.lift_map`, `Cat.FreeRefl.lift_spec`, `Cat.toFreeRefl_obj`, `SSet.hoFunctor.unitHomEquiv_eq`, `ReflQuiv.forget_obj`, `Functor.toReflPrefunctor_toPrefunctor`, `Cat.toFreeRefl_map`, `ReflQuiv.adj.homEquiv_naturality_left_symm`, `ReflQuiv.adj_counit_app`, `ReflQuiv.adj.homEquiv_apply`, `ReflQuiv.adj.homEquiv_naturality_right`, `ReflQuiv.adj.counit.comp_app_eq`, `SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_map`, `Functor.toReflPrefunctor.map_comp`, `SSet.OneTruncation₂.nerveHomEquiv_apply`, `Cat.FreeRefl.instSubsingletonHomOfUnique`, `SSet.Truncated.HomotopyCategory.BinaryProduct.functor_map`, `SSet.Truncated.HomotopyCategory.subsingleton_hom`, `Cat.FreeRefl.lift_obj`, `ReflQuiver.id_eq_id`
`«term𝟙rq»` 📖	CompOp	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`toReflPrefunctor` 📖	CompOp	6 math math: `CategoryTheory.Cat.FreeRefl.lift_spec`, `CategoryTheory.ReflQuiv.forget_map`, `toReflPrefunctor_toPrefunctor`, `CategoryTheory.ReflQuiv.adj.homEquiv_apply`, `CategoryTheory.ReflQuiv.adj.homEquiv_naturality_right`, `toReflPrefunctor.map_comp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toReflPrefunctor_toPrefunctor` 📖	mathematical	—	`CategoryTheory.ReflPrefunctor.toPrefunctor` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.catToReflQuiver` `CategoryTheory.Cat.str` `toReflPrefunctor` `toPrefunctor`	—	—

CategoryTheory.Functor.toReflPrefunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_comp` 📖	mathematical	—	`CategoryTheory.Functor.toReflPrefunctor` `CategoryTheory.Functor.comp` `CategoryTheory.ReflPrefunctor.comp` `CategoryTheory.catToReflQuiver`	—	—

CategoryTheory.ReflPrefunctor

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	11 math math: `comp_assoc`, `CategoryTheory.Cat.FreeRefl.lift_spec`, `CategoryTheory.ReflQuiv.comp_eq_comp`, `CategoryTheory.ReflQuiv.adj.homEquiv_naturality_left_symm`, `comp_map`, `CategoryTheory.ReflQuiv.adj.homEquiv_apply`, `CategoryTheory.ReflQuiv.adj.homEquiv_naturality_right`, `comp_obj`, `CategoryTheory.Functor.toReflPrefunctor.map_comp`, `comp_id`, `id_comp`
`id` 📖	CompOp	6 math math: `id_map`, `id_obj`, `CategoryTheory.ReflQuiv.adj_counit_app`, `CategoryTheory.ReflQuiv.id_eq_id`, `comp_id`, `id_comp`
`instInhabited` 📖	CompOp	—
`toPrefunctor` 📖	CompOp	29 math math: `SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_map`, `id_map`, `id_obj`, `CategoryTheory.Cat.freeReflMap_obj`, `congr_obj`, `CategoryTheory.ReflQuiv.id_map`, `CategoryTheory.Cat.FreeRefl.lift_map`, `CategoryTheory.ReflQuiv.comp_map`, `SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj`, `CategoryTheory.Cat.toFreeRefl_obj`, `CategoryTheory.ReflQuiv.adj.unit.map_app_eq`, `congr_hom`, `SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_obj`, `CategoryTheory.Functor.toReflPrefunctor_toPrefunctor`, `CategoryTheory.Cat.freeReflMap_naturality`, `congr_map`, `CategoryTheory.ReflQuiv.comp_obj`, `CategoryTheory.Cat.toFreeRefl_map`, `map_id`, `comp_map`, `CategoryTheory.ReflQuiv.forgetToQuiv_map`, `CategoryTheory.ReflQuiv.id_obj`, `comp_obj`, `SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_map`, `SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map`, `CategoryTheory.Cat.freeReflMap_map`, `SSet.OneTruncation₂.map_map`, `SSet.OneTruncation₂.map_obj`, `CategoryTheory.Cat.FreeRefl.lift_obj`
`«term_⋙rq_»` 📖	CompOp	—
`«term_⥤rq_»` 📖	CompOp	—
`«term𝟭rq»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	—
`comp_map` 📖	mathematical	—	`Prefunctor.map` `CategoryTheory.ReflQuiver.toQuiver` `toPrefunctor` `comp` `Prefunctor.obj`	—	—
`comp_obj` 📖	mathematical	—	`Prefunctor.obj` `CategoryTheory.ReflQuiver.toQuiver` `toPrefunctor` `comp`	—	—
`congr_hom` 📖	mathematical	—	`Quiver.homOfEq` `CategoryTheory.ReflQuiver.toQuiver` `Prefunctor.obj` `toPrefunctor` `Prefunctor.map` `congr_obj`	—	`congr_obj`
`congr_map` 📖	mathematical	—	`Prefunctor.map` `CategoryTheory.ReflQuiver.toQuiver` `toPrefunctor`	—	—
`congr_obj` 📖	mathematical	—	`Prefunctor.obj` `CategoryTheory.ReflQuiver.toQuiver` `toPrefunctor`	—	—
`ext` 📖	—	`Prefunctor.obj` `CategoryTheory.ReflQuiver.toQuiver` `toPrefunctor` `Prefunctor.map` `Quiver.Hom`	—	—	`Set.eqOn_univ`
`ext'` 📖	—	`Prefunctor.obj` `CategoryTheory.ReflQuiver.toQuiver` `toPrefunctor` `Prefunctor.map` `Quiver.homOfEq`	—	—	`Prefunctor.ext'`
`id_comp` 📖	mathematical	—	`comp` `id`	—	—
`id_map` 📖	mathematical	—	`Prefunctor.map` `CategoryTheory.ReflQuiver.toQuiver` `toPrefunctor` `id`	—	—
`id_obj` 📖	mathematical	—	`Prefunctor.obj` `CategoryTheory.ReflQuiver.toQuiver` `toPrefunctor` `id`	—	—
`map_id` 📖	mathematical	—	`Prefunctor.map` `CategoryTheory.ReflQuiver.toQuiver` `toPrefunctor` `CategoryTheory.ReflQuiver.id` `Prefunctor.obj`	—	—
`mk_map` 📖	mathematical	—	`Prefunctor.map` `CategoryTheory.ReflQuiver.toQuiver`	—	—
`mk_obj` 📖	mathematical	—	`Prefunctor.obj` `CategoryTheory.ReflQuiver.toQuiver`	—	—

CategoryTheory.ReflQuiver

Definitions

Name	Category	Theorems
`discreteReflQuiver` 📖	CompOp	—
`id` 📖	CompOp	8 math math: `SSet.OneTruncation₂.nerveHomEquiv_id`, `homOfEq_id`, `CategoryTheory.Cat.FreeRefl.homMk_id`, `SSet.OneTruncation₂.reflQuiver_id`, `CategoryTheory.Cat.FreeRefl.quotientFunctor_map_id`, `CategoryTheory.ReflPrefunctor.map_id`, `SSet.OneTruncation₂.id_edge`, `id_eq_id`
`opposite` 📖	CompOp	—
`toQuiver` 📖	CompOp	44 math math: `SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_map`, `CategoryTheory.ReflPrefunctor.id_map`, `CategoryTheory.ReflPrefunctor.id_obj`, `SSet.OneTruncation₂.nerveHomEquiv_id`, `SSet.OneTruncation₂.homOfEq_edge`, `homOfEq_id`, `CategoryTheory.Cat.freeReflMap_obj`, `CategoryTheory.ReflPrefunctor.congr_obj`, `CategoryTheory.ReflQuiv.id_map`, `CategoryTheory.Cat.FreeRefl.lift_map`, `CategoryTheory.ReflQuiv.comp_map`, `SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj`, `CategoryTheory.Cat.toFreeRefl_obj`, `CategoryTheory.Cat.FreeRefl.instFullPathsQuotientFunctor`, `SSet.hoFunctor.unitHomEquiv_eq`, `SSet.OneTruncation₂.HoRel₂.mk`, `CategoryTheory.ReflQuiv.adj.unit.map_app_eq`, `CategoryTheory.ReflPrefunctor.congr_hom`, `SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_obj`, `CategoryTheory.Cat.freeReflMap_naturality`, `CategoryTheory.ReflPrefunctor.congr_map`, `CategoryTheory.ReflQuiv.forgetToQuiv_obj`, `CategoryTheory.ReflQuiv.comp_obj`, `CategoryTheory.Cat.FreeRefl.quotientFunctor_map_id`, `CategoryTheory.Cat.FreeRefl.quotientFunctor_map_nil`, `CategoryTheory.Cat.toFreeRefl_map`, `CategoryTheory.ReflPrefunctor.map_id`, `CategoryTheory.ReflPrefunctor.comp_map`, `CategoryTheory.ReflQuiv.id_obj`, `CategoryTheory.ReflPrefunctor.comp_obj`, `CategoryTheory.ReflQuiv.adj.counit.comp_app_eq`, `SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_map`, `SSet.OneTruncation₂.reflQuiver_Hom`, `SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map`, `SSet.OneTruncation₂.nerveHomEquiv_apply`, `CategoryTheory.Cat.freeReflMap_map`, `SSet.OneTruncation₂.map_map`, `SSet.OneTruncation₂.map_obj`, `SSet.Truncated.HomotopyCategory.BinaryProduct.functor_map`, `SSet.Truncated.HomotopyCategory.subsingleton_hom`, `CategoryTheory.ReflPrefunctor.mk_map`, `CategoryTheory.Cat.FreeRefl.lift_obj`, `CategoryTheory.Cat.FreeRefl.quotientFunctor_map_cons`, `CategoryTheory.ReflPrefunctor.mk_obj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homOfEq_id` 📖	mathematical	—	`Quiver.homOfEq` `toQuiver` `id`	—	—
`id_eq_id` 📖	mathematical	—	`id` `CategoryTheory.catToReflQuiver` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—

---

← Back to Index