Theorems · Definition · category theory
Quiver.Hom.toLoc
{C : Type u} → [inst : CategoryTheory.CategoryStruct.{v, u} C] → {a b : C} → (a ⟶ b) → ({ as := a } ⟶ { as := b })The 1-morphism in LocallyDiscrete C associated to a given morphism f : a ⟶ b in C
- Cited by
- 150 results in Mathlib
- Foundations
- Depth 4 from the axioms, rests on 12 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.CategoryStructstatement and proof · cited by 343
- CategoryTheory.LocallyDiscretestatement · cited by 318
Cited by218
Results whose statement or proof uses this declaration.
- CategoryTheory.Pseudofunctor.DescentData'.pullHom'statement and proof · cited by 29
- CategoryTheory.Pseudofunctor.DescentData.homstatement · cited by 28
- CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHomstatement and proof · cited by 23
- CategoryTheory.Pseudofunctor.DescentData'.homstatement · cited by 22
- CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.homstatement · cited by 22
- CategoryTheory.Pseudofunctor.toDescentDataproof · cited by 21
- CategoryTheory.Pseudofunctor.DescentData.pullFunctorproof · cited by 16
- CategoryTheory.Pseudofunctor.presheafHomproof · cited by 15
- CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalencestatement and proof · cited by 13
- CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.fiberstatement · cited by 11
- CategoryTheory.Pseudofunctor.Grothendieck.Hom.fiberstatement · cited by 9
- CategoryTheory.Pseudofunctor.CoGrothendieck.mapproof · cited by 8
Showing the 200 most cited of 218.