Theorems · Definition · category theory
CategoryTheory.Cat.freeMap
{V : Type u_1} →
{W : Type u_2} →
[inst : Quiver V] →
[inst_1 : Quiver W] → V ⥤q W → CategoryTheory.Functor (CategoryTheory.Paths V) (CategoryTheory.Paths W)A prefunctor V ⥤q W induces a functor between the path categories defined by F.mapPath.
- Defined in
- Mathlib.CategoryTheory.Category.Quiv
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homproof · cited by 32,603
- CategoryTheory.Functorstatement · cited by 16,252
- Prefunctor.objproof · cited by 1,241
- Quiverstatement and proof · cited by 405
- Prefunctorstatement and proof · cited by 116
- CategoryTheory.Pathsstatement and proof · cited by 82
- Prefunctor.mapPathproof · cited by 15
- Prefunctor.mapPath_compproof · cited by 1
Cited by19
Results whose statement or proof uses this declaration.
- CategoryTheory.Cat.freeproof · cited by 4
- CategoryTheory.Cat.freeMapCompIsostatement and proof · cited by 3
- CategoryTheory.Cat.freeMapIdIsostatement and proof · cited by 3
- CategoryTheory.Quiv.pathsEquivproof · cited by 1
- CategoryTheory.Quiv.pathCompositionNaturalitystatement and proof · cited by 0
- CategoryTheory.Quiv.pathComposition_naturalitystatement · cited by 0
- CategoryTheory.Quiv.pathsOf_freeMap_toPrefunctorstatement · cited by 0
- CategoryTheory.Cat.freeMapCompIso_hom_appstatement · cited by 0
- CategoryTheory.Cat.freeMapCompIso_inv_appstatement · cited by 0
- CategoryTheory.Cat.freeMapIdIso_hom_appstatement · cited by 0
- CategoryTheory.Cat.freeMapIdIso_inv_appstatement · cited by 0
- CategoryTheory.Cat.freeMap_compstatement · cited by 0