Theorems · Definition · category theory
Quiver.FreeGroupoid.of
(V : Type u_1) → [inst : Quiver V] → V ⥤q Quiver.FreeGroupoid V
The inclusion of the quiver on V to the underlying quiver on FreeGroupoid V
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, Quot.sound
- Assumes
- Quiver
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
- Quiverstatement and proof · cited by 405
- Prefunctorstatement · cited by 116
- CategoryTheory.Quotient.asproof · cited by 47
- CategoryTheory.HomRel.CompClosureproof · cited by 19
- Quiver.FreeGroupoidstatement · cited by 8
- Quiver.FreeGroupoid.redStepproof · cited by 7
- Quiver.Hom.toPosPathproof · cited by 0
Cited by11
Results whose statement or proof uses this declaration.
- CategoryTheory.FreeGroupoid.ofproof · cited by 21
- CategoryTheory.FreeGroupoid.lift_specproof · cited by 4
- Quiver.FreeGroupoid.lift_uniquestatement and proof · cited by 3
- Quiver.freeGroupoidFunctorproof · cited by 2
- Quiver.FreeGroupoid.lift_specstatement · cited by 1
- Quiver.FreeGroupoid.of_eqstatement · cited by 1
- CategoryTheory.FreeGroupoid.homRel.recOnstatement and proof · cited by 0
- CategoryTheory.FreeGroupoid.of_obj_bijectiveproof · cited by 0
- Quiver.freeGroupoidFunctor_compproof · cited by 0
- Quiver.freeGroupoidFunctor_idproof · cited by 0
- CategoryTheory.FreeGroupoid.homRel.casesOnstatement and proof · cited by 0