Theorems · Definition · group theory
IsFreeGroupoid.Generators
(G : Type u_1) → [CategoryTheory.Groupoid G] → Type u_1
IsFreeGroupoid.Generators G is a type synonym for G. We think of this as
the vertices of the generating quiver of G when G is free. We can't use G directly,
since G already has a quiver instance from being a groupoid.
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- CategoryTheory.Groupoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Groupoidstatement and proof · cited by 182
Cited by21
Results whose statement or proof uses this declaration.
- IsFreeGroupoid.ofstatement · cited by 7
- IsFreeGroupoid.SpanningTree.homOfPathstatement and proof · cited by 4
- IsFreeGroupoid.SpanningTree.treeHomstatement and proof · cited by 4
- IsFreeGroupoid.SpanningTree.functorOfMonoidHomstatement and proof · cited by 3
- IsFreeGroupoid.SpanningTree.loopOfHomstatement and proof · cited by 3
- IsFreeGroupoid.ext_functorstatement and proof · cited by 2
- IsFreeGroupoid.unique_liftstatement · cited by 2
- IsFreeGroupoid.SpanningTree.treeHom_eqstatement and proof · cited by 2
- IsFreeGroupoid.SpanningTree.loopOfHom_eq_idstatement and proof · cited by 1
- IsFreeGroupoid.SpanningTree.treeHom_rootstatement and proof · cited by 1
- IsFreeGroupoid.casesOnstatement and proof · cited by 0
- IsFreeGroupoid.ext_functor_iffstatement and proof · cited by 0