Quiv

📁 Source: Mathlib/CategoryTheory/Category/Quiv.lean

Statistics

Metric	Count
Definitions `free`, `freeMap`, `freeMapCompIso`, `freeMapIdIso`, `ofQuivHom`, `toQuivHom`, `Quiv`, `adj`, `category`, `equivOfIso`, `forget`, `freeMapPathsOfCompPathCompositionIso`, `homEquivOfIso`, `instCoeSortType`, `instInhabited`, `isoOfEquiv`, `of`, `pathCompositionNaturality`, `pathsEquiv`, `str'`	20
Theorems `freeMapCompIso_hom_app`, `freeMapCompIso_inv_app`, `freeMapIdIso_hom_app`, `freeMapIdIso_inv_app`, `freeMap_comp`, `freeMap_id`, `freeMap_map`, `freeMap_obj`, `free_map`, `free_obj`, `of_toQuivHom`, `to_ofQuivHom`, `adj_homEquiv`, `comp_eq_comp`, `equivOfIso_apply`, `equivOfIso_symm_apply`, `forget_map`, `forget_obj`, `freeMap_pathsOf_pathComposition`, `homEquivOfIso_apply`, `homEquivOfIso_symm_apply`, `homOfEq_map_homOfEq`, `hom_map_inv_map_of_iso`, `hom_obj_inv_obj_of_iso`, `id_eq_id`, `inv_map_hom_map_of_iso`, `inv_obj_hom_obj_of_iso`, `lift_map`, `lift_obj`, `pathComposition_naturality`, `pathsOf_freeMap_toPrefunctor`, `pathsOf_pathComposition_toPrefunctor`	32
Total	52

CategoryTheory

Definitions

Name	Category	Theorems
`Quiv` 📖	CompOp	20 math math: `Quiv.equivOfIso_symm_apply`, `Quiv.comp_eq_comp`, `Quiv.homEquivOfIso_symm_apply`, `Cat.free_map`, `Quiv.homEquivOfIso_apply`, `Quiv.inv_map_hom_map_of_iso`, `ReflQuiv.adj.unit.map_app_eq`, `Quiv.forget_map`, `Quiv.adj_homEquiv`, `ReflQuiv.forgetToQuiv_obj`, `Quiv.hom_map_inv_map_of_iso`, `ReflQuiv.forget_forgetToQuiv`, `Cat.free_obj`, `ReflQuiv.forgetToQuiv_map`, `Quiv.inv_obj_hom_obj_of_iso`, `Quiv.hom_obj_inv_obj_of_iso`, `Quiv.id_eq_id`, `ReflQuiv.forgetToQuiv.Faithful`, `Quiv.forget_obj`, `Quiv.equivOfIso_apply`

CategoryTheory.Cat

Definitions

Name	Category	Theorems
`free` 📖	CompOp	4 math math: `free_map`, `CategoryTheory.ReflQuiv.adj.unit.map_app_eq`, `CategoryTheory.Quiv.adj_homEquiv`, `free_obj`
`freeMap` 📖	CompOp	13 math math: `freeMap_map`, `freeMap_obj`, `freeMap_comp`, `freeMapIdIso_hom_app`, `free_map`, `freeReflMap_naturality`, `freeMap_id`, `CategoryTheory.Quiv.pathComposition_naturality`, `freeMapCompIso_hom_app`, `CategoryTheory.Quiv.freeMap_pathsOf_pathComposition`, `CategoryTheory.Quiv.pathsOf_freeMap_toPrefunctor`, `freeMapIdIso_inv_app`, `freeMapCompIso_inv_app`
`freeMapCompIso` 📖	CompOp	2 math math: `freeMapCompIso_hom_app`, `freeMapCompIso_inv_app`
`freeMapIdIso` 📖	CompOp	2 math math: `freeMapIdIso_hom_app`, `freeMapIdIso_inv_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`freeMapCompIso_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Paths` `CategoryTheory.Paths.categoryPaths` `freeMap` `Prefunctor.comp` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `freeMapCompIso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `Prefunctor.obj`	—	—
`freeMapCompIso_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Paths` `CategoryTheory.Paths.categoryPaths` `CategoryTheory.Functor.comp` `freeMap` `Prefunctor.comp` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `freeMapCompIso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `Prefunctor.obj`	—	—
`freeMapIdIso_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Paths` `CategoryTheory.Paths.categoryPaths` `freeMap` `Prefunctor.id` `CategoryTheory.Functor.id` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `freeMapIdIso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`freeMapIdIso_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Paths` `CategoryTheory.Paths.categoryPaths` `CategoryTheory.Functor.id` `freeMap` `Prefunctor.id` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `freeMapIdIso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`freeMap_comp` 📖	mathematical	—	`freeMap` `Prefunctor.comp` `CategoryTheory.Functor.comp` `CategoryTheory.Paths` `CategoryTheory.Paths.categoryPaths`	—	`CategoryTheory.Functor.ext_of_iso`
`freeMap_id` 📖	mathematical	—	`freeMap` `Prefunctor.id` `CategoryTheory.Functor.id` `CategoryTheory.Paths` `CategoryTheory.Paths.categoryPaths`	—	`CategoryTheory.Functor.ext_of_iso`
`freeMap_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Paths` `CategoryTheory.Paths.categoryPaths` `freeMap` `Prefunctor.mapPath`	—	—
`freeMap_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Paths` `CategoryTheory.Paths.categoryPaths` `freeMap` `Prefunctor.obj`	—	—
`free_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Quiv` `CategoryTheory.Quiv.category` `CategoryTheory.Cat` `category` `free` `CategoryTheory.Functor.toCatHom` `CategoryTheory.Paths` `CategoryTheory.Bundled.α` `Quiver` `CategoryTheory.Paths.categoryPaths` `CategoryTheory.Quiv.str'` `freeMap` `CategoryTheory.Prefunctor.ofQuivHom`	—	—
`free_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Quiv` `CategoryTheory.Quiv.category` `CategoryTheory.Cat` `category` `free` `of` `CategoryTheory.Paths` `CategoryTheory.Bundled.α` `Quiver` `CategoryTheory.Paths.categoryPaths` `CategoryTheory.Quiv.str'`	—	—

CategoryTheory.Prefunctor

Definitions

Name	Category	Theorems
`ofQuivHom` 📖	CompOp	3 math math: `CategoryTheory.Cat.free_map`, `of_toQuivHom`, `to_ofQuivHom`
`toQuivHom` 📖	CompOp	2 math math: `of_toQuivHom`, `to_ofQuivHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_toQuivHom` 📖	mathematical	—	`ofQuivHom` `CategoryTheory.Quiv.of` `toQuivHom`	—	—
`to_ofQuivHom` 📖	mathematical	—	`toQuivHom` `CategoryTheory.Bundled.α` `Quiver` `CategoryTheory.Quiv.str'` `ofQuivHom`	—	—

CategoryTheory.Quiv

Definitions

Name	Category	Theorems
`adj` 📖	CompOp	2 math math: `CategoryTheory.ReflQuiv.adj.unit.map_app_eq`, `adj_homEquiv`
`category` 📖	CompOp	20 math math: `equivOfIso_symm_apply`, `comp_eq_comp`, `homEquivOfIso_symm_apply`, `CategoryTheory.Cat.free_map`, `homEquivOfIso_apply`, `inv_map_hom_map_of_iso`, `CategoryTheory.ReflQuiv.adj.unit.map_app_eq`, `forget_map`, `adj_homEquiv`, `CategoryTheory.ReflQuiv.forgetToQuiv_obj`, `hom_map_inv_map_of_iso`, `CategoryTheory.ReflQuiv.forget_forgetToQuiv`, `CategoryTheory.Cat.free_obj`, `CategoryTheory.ReflQuiv.forgetToQuiv_map`, `inv_obj_hom_obj_of_iso`, `hom_obj_inv_obj_of_iso`, `id_eq_id`, `CategoryTheory.ReflQuiv.forgetToQuiv.Faithful`, `forget_obj`, `equivOfIso_apply`
`equivOfIso` 📖	CompOp	2 math math: `equivOfIso_symm_apply`, `equivOfIso_apply`
`forget` 📖	CompOp	5 math math: `CategoryTheory.ReflQuiv.adj.unit.map_app_eq`, `forget_map`, `adj_homEquiv`, `CategoryTheory.ReflQuiv.forget_forgetToQuiv`, `forget_obj`
`freeMapPathsOfCompPathCompositionIso` 📖	CompOp	—
`homEquivOfIso` 📖	CompOp	2 math math: `homEquivOfIso_symm_apply`, `homEquivOfIso_apply`
`instCoeSortType` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`isoOfEquiv` 📖	CompOp	—
`of` 📖	CompOp	5 math math: `CategoryTheory.Prefunctor.of_toQuivHom`, `CategoryTheory.ReflQuiv.adj.unit.map_app_eq`, `adj_homEquiv`, `CategoryTheory.ReflQuiv.forgetToQuiv_obj`, `forget_obj`
`pathCompositionNaturality` 📖	CompOp	—
`pathsEquiv` 📖	CompOp	1 math math: `adj_homEquiv`
`str'` 📖	CompOp	14 math math: `equivOfIso_symm_apply`, `comp_eq_comp`, `homEquivOfIso_symm_apply`, `CategoryTheory.Cat.free_map`, `homEquivOfIso_apply`, `inv_map_hom_map_of_iso`, `CategoryTheory.ReflQuiv.adj.unit.map_app_eq`, `CategoryTheory.Prefunctor.to_ofQuivHom`, `hom_map_inv_map_of_iso`, `CategoryTheory.Cat.free_obj`, `inv_obj_hom_obj_of_iso`, `hom_obj_inv_obj_of_iso`, `id_eq_id`, `equivOfIso_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adj_homEquiv` 📖	mathematical	—	`CategoryTheory.Adjunction.homEquiv` `CategoryTheory.Quiv` `category` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.Cat.free` `forget` `adj` `of` `CategoryTheory.Cat.of` `Equiv.trans` `Quiver.Hom` `CategoryTheory.Cat.instQuiver` `CategoryTheory.Paths` `CategoryTheory.Paths.categoryPaths` `CategoryTheory.Functor` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Cat.str` `Prefunctor` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Cat.Hom.equivFunctor` `pathsEquiv`	—	—
`comp_eq_comp` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Quiv` `CategoryTheory.Category.toCategoryStruct` `category` `Prefunctor.comp` `CategoryTheory.Bundled.α` `Quiver` `str'`	—	—
`equivOfIso_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.Bundled.α` `Quiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivOfIso` `Prefunctor.obj` `str'` `CategoryTheory.Iso.hom` `CategoryTheory.Quiv` `category`	—	—
`equivOfIso_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.Bundled.α` `Quiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivOfIso` `Prefunctor.obj` `str'` `CategoryTheory.Iso.inv` `CategoryTheory.Quiv` `category`	—	—
`forget_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.Quiv` `category` `forget` `CategoryTheory.Functor.toPrefunctor` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Cat.str` `CategoryTheory.Cat.Hom.toFunctor`	—	—
`forget_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.Quiv` `category` `forget` `of` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Cat.str`	—	—
`freeMap_pathsOf_pathComposition` 📖	mathematical	—	`CategoryTheory.Functor.comp` `CategoryTheory.Paths` `CategoryTheory.Paths.categoryPaths` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Cat.freeMap` `CategoryTheory.Paths.of` `CategoryTheory.pathComposition` `CategoryTheory.Functor.id`	—	`CategoryTheory.Paths.ext_functor` `CategoryTheory.composePath_toPath` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`homEquivOfIso_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Bundled.α` `Quiver` `str'` `Prefunctor.obj` `CategoryTheory.Iso.hom` `CategoryTheory.Quiv` `category` `EquivLike.toFunLike` `Equiv.instEquivLike` `homEquivOfIso` `Prefunctor.map`	—	—
`homEquivOfIso_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Bundled.α` `Quiver` `str'` `Prefunctor.obj` `CategoryTheory.Iso.hom` `CategoryTheory.Quiv` `category` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `homEquivOfIso` `Quiver.homOfEq` `CategoryTheory.Iso.inv` `Prefunctor.map`	—	—
`homOfEq_map_homOfEq` 📖	mathematical	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Quiver.homOfEq` `Quiver.Hom`	—	—
`hom_map_inv_map_of_iso` 📖	mathematical	—	`Prefunctor.map` `CategoryTheory.Bundled.α` `Quiver` `str'` `CategoryTheory.Iso.hom` `CategoryTheory.Quiv` `category` `Prefunctor.obj` `CategoryTheory.Iso.inv` `Quiver.homOfEq`	—	`Prefunctor.comp_map` `Prefunctor.congr_obj` `CategoryTheory.Iso.inv_hom_id` `Prefunctor.congr_hom`
`hom_obj_inv_obj_of_iso` 📖	mathematical	—	`Prefunctor.obj` `CategoryTheory.Bundled.α` `Quiver` `str'` `CategoryTheory.Iso.hom` `CategoryTheory.Quiv` `category` `CategoryTheory.Iso.inv`	—	`Equiv.right_inv`
`id_eq_id` 📖	mathematical	—	`CategoryTheory.CategoryStruct.id` `CategoryTheory.Quiv` `CategoryTheory.Category.toCategoryStruct` `category` `Prefunctor.id` `CategoryTheory.Bundled.α` `Quiver` `str'`	—	—
`inv_map_hom_map_of_iso` 📖	mathematical	—	`Prefunctor.map` `CategoryTheory.Bundled.α` `Quiver` `str'` `CategoryTheory.Iso.inv` `CategoryTheory.Quiv` `category` `Prefunctor.obj` `CategoryTheory.Iso.hom` `Quiver.homOfEq`	—	`hom_map_inv_map_of_iso`
`inv_obj_hom_obj_of_iso` 📖	mathematical	—	`Prefunctor.obj` `CategoryTheory.Bundled.α` `Quiver` `str'` `CategoryTheory.Iso.inv` `CategoryTheory.Quiv` `category` `CategoryTheory.Iso.hom`	—	`Equiv.left_inv`
`lift_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Paths` `CategoryTheory.Paths.categoryPaths` `lift` `CategoryTheory.composePath` `Prefunctor.obj` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Prefunctor.mapPath`	—	—
`lift_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Paths` `CategoryTheory.Paths.categoryPaths` `lift` `Prefunctor.obj` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	—	—
`pathComposition_naturality` 📖	mathematical	—	`CategoryTheory.Functor.comp` `CategoryTheory.Paths` `CategoryTheory.Paths.categoryPaths` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Cat.freeMap` `CategoryTheory.Functor.toPrefunctor` `CategoryTheory.pathComposition`	—	`CategoryTheory.Paths.ext_functor` `CategoryTheory.composePath_toPath` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`pathsOf_freeMap_toPrefunctor` 📖	mathematical	—	`Prefunctor.comp` `CategoryTheory.Paths` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Paths.categoryPaths` `CategoryTheory.Paths.of` `CategoryTheory.Functor.toPrefunctor` `CategoryTheory.Cat.freeMap`	—	—
`pathsOf_pathComposition_toPrefunctor` 📖	mathematical	—	`Prefunctor.comp` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Paths` `CategoryTheory.Paths.categoryPaths` `CategoryTheory.Paths.of` `CategoryTheory.Functor.toPrefunctor` `CategoryTheory.pathComposition` `Prefunctor.id`	—	`CategoryTheory.Category.id_comp`

---

← Back to Index