Theorems · Definition · combinatorics
Prefunctor.star
{U : Type u_1} →
[inst : Quiver U] →
{V : Type u_2} → [inst_1 : Quiver V] → (φ : U ⥤q V) → (u : U) → Quiver.Star u → Quiver.Star (φ.obj u)A prefunctor induces a map of Quiver.Star at every vertex.
- Defined in
- Mathlib.Combinatorics.Quiver.Covering
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Prefunctor.objstatement · cited by 1,241
- Prefunctor.mapproof · cited by 952
- Quiverstatement and proof · cited by 405
- Prefunctorstatement and proof · cited by 116
- Quiver.Starstatement and proof · cited by 22
- Quiver.Star.mkproof · cited by 7
Cited by21
Results whose statement or proof uses this declaration.
- Prefunctor.IsCovering.star_bijectivestatement · cited by 6
- Quiver.SchreierGraph.labellingStarEquivproof · cited by 4
- Prefunctor.bijective_costar_iff_bijective_starstatement and proof · cited by 2
- Prefunctor.pathStar_bijectivestatement and proof · cited by 1
- Prefunctor.pathStar_injectivestatement and proof · cited by 1
- Prefunctor.pathStar_surjectivestatement and proof · cited by 1
- Prefunctor.symmetrifyCostarstatement and proof · cited by 1
- Prefunctor.symmetrifyStarstatement and proof · cited by 1
- Prefunctor.costar_conj_starstatement · cited by 1
- Prefunctor.isCovering_of_bijective_starstatement and proof · cited by 0
- Quiver.SchreierGraph.labellingStarEquiv_applystatement · cited by 0
- Prefunctor.IsCovering.casesOnstatement and proof · cited by 0