Mathlib Map

Theorems · Definition · category theory

Prefunctor.obj

{V : Type u₁} → [inst : Quiver V] → {W : Type u₂} → [inst_1 : Quiver W] → V ⥤q W → V → W

The action of a (pre)functor on vertices/objects.

Defined in
Mathlib.Combinatorics.Quiver.Prefunctor
Cited by
1,241 results in Mathlib
Foundations
Depth 2 from the axioms, rests on 3 definitions · uses no axioms
Assumes
QuiverQuiver
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Prefunctor.map · cited by 952Prefunctor.mapCategoryTheory.PrelaxFunctorStruct.map₂ · cited by 303PrelaxFunctorStruct.map₂CategoryTheory.Pseudofunctor.mapComp · cited by 177Pseudofunctor.mapCompCategoryTheory.Pseudofunctor.mapId · cited by 175Pseudofunctor.mapIdCategoryTheory.Pseudofunctor.StrongTrans.app · cited by 106StrongTrans.appCategoryTheory.MorphismProperty.Q · cited by 98MorphismProperty.QCategoryTheory.Pseudofunctor.mapComp' · cited by 87Pseudofunctor.mapComp'CategoryTheory.Pseudofunctor.StrongTrans.naturality · cited by 81StrongTrans.naturalityCategoryTheory.LaxFunctor.mapComp · cited by 77LaxFunctor.mapCompCategoryTheory.Oplax.OplaxTrans.app · cited by 76OplaxTrans.appCategoryTheory.OplaxFunctor.mapComp · cited by 73OplaxFunctor.mapCompCategoryTheory.Lax.LaxTrans.app · cited by 61LaxTrans.appCategoryTheory.LaxFunctor.mapId · cited by 61LaxFunctor.mapIdCategoryTheory.Oplax.StrongTrans.app · cited by 60StrongTrans.appCategoryTheory.OplaxFunctor.mapId · cited by 52OplaxFunctor.mapIdQuiver · cited by 405QuiverPrefunctor · cited by 116PrefunctorPrefunctor.objCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Quiverstatement and proof · cited by 405
  • Prefunctorstatement and proof · cited by 116

Cited by1,575

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 1,575.