Documentation Verification Report

Basic

📁 Source: Mathlib/CategoryTheory/PathCategory/Basic.lean

Statistics

MetricCount
DefinitionscategoryPaths, of, composePath, instInhabitedPaths, instUniquePaths, pathComposition, pathsHomRel, quotientPathsEquiv, quotientPathsTo, toQuotientPaths
10
Theoremsext_functor, induction, induction', induction_fixed_source, induction_fixed_target, lift_cons, lift_nil, lift_spec, lift_toPath, lift_unique, of_map, of_obj, mapPath_comp', composePath_comp, composePath_comp', composePath_cons, composePath_id, composePath_nil, composePath_toPath, pathComposition_map, pathComposition_obj, quotientPathsTo_map, quotientPathsTo_obj, toQuotientPaths_map, toQuotientPaths_obj_as
25
Total35

CategoryTheory

Definitions

NameCategoryTheorems
composePath 📖CompOp
12 mathmath: composePath_comp', composePath_comp, Localization.Construction.lift_map, composePath_nil, Quiv.lift_map, Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_map, composePath_cons, Localization.Construction.liftToPathCategory_map, composePath_id, composePath_toPath, pathComposition_map, quotientPathsTo_map
instInhabitedPaths 📖CompOp—
instUniquePaths 📖CompOp—
pathComposition 📖CompOp
7 mathmath: Quiv.pathsOf_pathComposition_toPrefunctor, pathComposition_obj, Quiv.pathComposition_naturality, Quiv.freeMap_pathsOf_pathComposition, ReflQuiv.adj.counit.comp_app_eq, pathComposition_map, quotientPathsTo_map
pathsHomRel 📖CompOp
4 mathmath: quotientPathsTo_obj, toQuotientPaths_obj_as, toQuotientPaths_map, quotientPathsTo_map
quotientPathsEquiv 📖CompOp—
quotientPathsTo 📖CompOp
2 mathmath: quotientPathsTo_obj, quotientPathsTo_map
toQuotientPaths 📖CompOp
2 mathmath: toQuotientPaths_obj_as, toQuotientPaths_map

Theorems

NameKindAssumesProvesValidatesDepends On
composePath_comp 📖mathematical—composePath
Quiver.Path.comp
CategoryStruct.toQuiver
Category.toCategoryStruct
CategoryStruct.comp		—Category.comp_id
Category.assoc
composePath_comp' 📖mathematical—composePath
CategoryStruct.comp
Paths
Category.toCategoryStruct
Paths.categoryPaths
CategoryStruct.toQuiver		—composePath_comp
composePath_cons 📖mathematical—composePath
Quiver.Path.cons
CategoryStruct.toQuiver
Category.toCategoryStruct
CategoryStruct.comp		——
composePath_id 📖mathematical—composePath
CategoryStruct.id
Paths
Category.toCategoryStruct
Paths.categoryPaths
CategoryStruct.toQuiver		——
composePath_nil 📖mathematical—composePath
Quiver.Path.nil
CategoryStruct.toQuiver
Category.toCategoryStruct
CategoryStruct.id		——
composePath_toPath 📖mathematical—composePath
Quiver.Hom.toPath
CategoryStruct.toQuiver
Category.toCategoryStruct		—Category.id_comp
pathComposition_map 📖mathematical—Functor.map
Paths
Paths.categoryPaths
CategoryStruct.toQuiver
Category.toCategoryStruct
pathComposition
composePath		——
pathComposition_obj 📖mathematical—Functor.obj
Paths
Paths.categoryPaths
CategoryStruct.toQuiver
Category.toCategoryStruct
pathComposition		——
quotientPathsTo_map 📖mathematical—Functor.map
Quotient
Paths
Paths.categoryPaths
CategoryStruct.toQuiver
Category.toCategoryStruct
pathsHomRel
Quotient.category
quotientPathsTo
Quiver.Hom
Quotient.as
HomRel.CompClosure
composePath
pathComposition		——
quotientPathsTo_obj 📖mathematical—Functor.obj
Quotient
Paths
Paths.categoryPaths
CategoryStruct.toQuiver
Category.toCategoryStruct
pathsHomRel
Quotient.category
quotientPathsTo
Quotient.as		——
toQuotientPaths_map 📖mathematical—Functor.map
Quotient
Paths
Paths.categoryPaths
CategoryStruct.toQuiver
Category.toCategoryStruct
pathsHomRel
Quotient.category
toQuotientPaths
Quiver.Hom
Quotient.as
HomRel.CompClosure
Quiver.Hom.toPath		——
toQuotientPaths_obj_as 📖mathematical—Quotient.as
Paths
Paths.categoryPaths
CategoryStruct.toQuiver
Category.toCategoryStruct
pathsHomRel
Functor.obj
Quotient
Quotient.category
toQuotientPaths		——

CategoryTheory.Paths

Definitions

NameCategoryTheorems
categoryPaths 📖CompOp
54 mathmath: CategoryTheory.Cat.freeMap_map, CategoryTheory.composePath_comp', CategoryTheory.Quiv.pathsOf_pathComposition_toPrefunctor, CategoryTheory.Localization.Construction.lift_obj, CategoryTheory.Cat.freeMap_obj, CategoryTheory.pathComposition_obj, CategoryTheory.Cat.freeMap_comp, CategoryTheory.Cat.freeMapIdIso_hom_app, CategoryTheory.Cat.free_map, CategoryTheory.Cat.FreeRefl.instFullPathsQuotientFunctor, CategoryTheory.Quiv.lift_obj, SSet.OneTruncation₂.HoRel₂.mk, CategoryTheory.ReflQuiv.adj.unit.map_app_eq, of_map, CategoryTheory.quotientPathsTo_obj, CategoryTheory.Localization.Construction.lift_map, CategoryTheory.FreeBicategory.preinclusion_map₂, CategoryTheory.Quiv.adj_homEquiv, CategoryTheory.Cat.freeReflMap_naturality, Quiver.FreeGroupoid.congr_comp_reverse, CategoryTheory.Cat.FreeRefl.quotientFunctor_map_id, CategoryTheory.Cat.freeMap_id, CategoryTheory.Cat.FreeRefl.quotientFunctor_map_nil, lift_spec, CategoryTheory.Quiv.pathComposition_naturality, CategoryTheory.Cat.freeMapCompIso_hom_app, CategoryTheory.Cat.free_obj, CategoryTheory.Quiv.freeMap_pathsOf_pathComposition, CategoryTheory.FreeGroupoid.eq_mk, CategoryTheory.Quiv.lift_map, lift_cons, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_map, CategoryTheory.FreeBicategory.normalize_naturality, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_obj, CategoryTheory.Localization.Construction.liftToPathCategory_map, CategoryTheory.ReflQuiv.adj.counit.comp_app_eq, CategoryTheory.toQuotientPaths_obj_as, CategoryTheory.composePath_id, CategoryTheory.Quiv.pathsOf_freeMap_toPrefunctor, lift_toPath, Quiver.FreeGroupoid.of_eq, CategoryTheory.Localization.Construction.objEquiv_symm_apply, CategoryTheory.Localization.Construction.liftToPathCategory_obj, Quiver.FreeGroupoid.congr_reverse_comp, CategoryTheory.FreeBicategory.preinclusion_obj, lift_nil, CategoryTheory.pathComposition_map, CategoryTheory.toQuotientPaths_map, of_obj, CategoryTheory.quotientPathsTo_map, CategoryTheory.Cat.FreeRefl.quotientFunctor_map_cons, CategoryTheory.Cat.freeMapIdIso_inv_app, CategoryTheory.Cat.freeMapCompIso_inv_app, CategoryTheory.Prefunctor.mapPath_comp'
of 📖CompOp
7 mathmath: CategoryTheory.Quiv.pathsOf_pathComposition_toPrefunctor, of_map, lift_spec, CategoryTheory.Quiv.freeMap_pathsOf_pathComposition, CategoryTheory.Quiv.pathsOf_freeMap_toPrefunctor, Quiver.FreeGroupoid.of_eq, of_obj

Theorems

NameKindAssumesProvesValidatesDepends On
ext_functor 📖—CategoryTheory.Functor.obj
CategoryTheory.Paths
categoryPaths
CategoryTheory.Functor.map
Quiver.Hom.toPath
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.eqToHom		——CategoryTheory.Functor.ext
CategoryTheory.Functor.map_id
CategoryTheory.Category.id_comp
CategoryTheory.eqToHom_trans
CategoryTheory.eqToHom_refl
CategoryTheory.Functor.map_comp
CategoryTheory.Category.assoc
CategoryTheory.eqToHom_trans_assoc
induction 📖—Prefunctor.obj
CategoryTheory.Paths
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
categoryPaths
of
CategoryTheory.CategoryStruct.id
CategoryTheory.CategoryStruct.comp
Prefunctor.map		——induction_fixed_source
induction' 📖—Prefunctor.obj
CategoryTheory.Paths
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
categoryPaths
of
CategoryTheory.CategoryStruct.id
CategoryTheory.CategoryStruct.comp
Prefunctor.map		——induction_fixed_target
induction_fixed_source 📖—CategoryTheory.CategoryStruct.id
CategoryTheory.Paths
CategoryTheory.Category.toCategoryStruct
categoryPaths
Prefunctor.obj
CategoryTheory.CategoryStruct.toQuiver
of
CategoryTheory.CategoryStruct.comp
Prefunctor.map		———
induction_fixed_target 📖—CategoryTheory.CategoryStruct.id
CategoryTheory.Paths
CategoryTheory.Category.toCategoryStruct
categoryPaths
Prefunctor.obj
CategoryTheory.CategoryStruct.toQuiver
of
CategoryTheory.CategoryStruct.comp
Prefunctor.map		——Quiver.Path.eq_toPath_comp_of_length_eq_succ
lift_cons 📖mathematical—CategoryTheory.Functor.map
CategoryTheory.Paths
categoryPaths
lift
Quiver.Path.cons
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
Prefunctor.obj
CategoryTheory.CategoryStruct.toQuiver
Prefunctor.map		——
lift_nil 📖mathematical—CategoryTheory.Functor.map
CategoryTheory.Paths
categoryPaths
lift
Quiver.Path.nil
CategoryTheory.CategoryStruct.id
CategoryTheory.Category.toCategoryStruct
Prefunctor.obj
CategoryTheory.CategoryStruct.toQuiver		——
lift_spec 📖mathematical—Prefunctor.comp
CategoryTheory.Paths
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
categoryPaths
of
CategoryTheory.Functor.toPrefunctor
lift		—Prefunctor.ext
CategoryTheory.Category.id_comp
lift_toPath 📖mathematical—CategoryTheory.Functor.map
CategoryTheory.Paths
categoryPaths
lift
Quiver.Hom.toPath
Prefunctor.map
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct		—CategoryTheory.Category.id_comp
lift_unique 📖mathematicalPrefunctor.comp
CategoryTheory.Paths
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
categoryPaths
of
CategoryTheory.Functor.toPrefunctor		lift—CategoryTheory.Functor.ext
CategoryTheory.Category.comp_id
CategoryTheory.Functor.map_id
CategoryTheory.Category.id_comp
CategoryTheory.Functor.map_comp
of_map 📖mathematical—Prefunctor.map
CategoryTheory.Paths
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
categoryPaths
of
Quiver.Hom.toPath		——
of_obj 📖mathematical—Prefunctor.obj
CategoryTheory.Paths
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
categoryPaths
of		——

CategoryTheory.Prefunctor

Theorems

NameKindAssumesProvesValidatesDepends On
mapPath_comp' 📖mathematical—Prefunctor.mapPath
CategoryTheory.CategoryStruct.comp
CategoryTheory.Paths
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Paths.categoryPaths
Quiver.Path.comp
Prefunctor.obj		—Prefunctor.mapPath_comp

---

← Back to Index