Theorems · Definition · category theory

CategoryTheory.Limits.MulticospanIndex.multicospan

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      CategoryTheory.Limits.MulticospanIndex J C → CategoryTheory.Functor (CategoryTheory.Limits.WalkingMulticospan J) C

The multicospan associated to I : MulticospanIndex.

Defined in: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Cited by: 167 results in Mathlib
Foundations: Depth 16 from the axioms, rests on 92 definitions · uses propext
Assumes: CategoryTheory.Category

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites13

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

CategoryTheory.Categorystatement and proof · cited by 32,673
Quiver.Homproof · cited by 32,603
CategoryTheory.Functorstatement · cited by 16,252
CategoryTheory.CategoryStruct.idproof · cited by 6,235
CategoryTheory.Limits.WalkingMulticospanstatement and proof · cited by 199
CategoryTheory.Limits.MulticospanShapestatement and proof · cited by 160
CategoryTheory.Limits.MulticospanShape.Lproof · cited by 135
CategoryTheory.Limits.MulticospanShape.Rproof · cited by 124
CategoryTheory.Limits.MulticospanIndex.leftproof · cited by 119
CategoryTheory.Limits.MulticospanIndexstatement and proof · cited by 101
CategoryTheory.Limits.MulticospanIndex.rightproof · cited by 77
CategoryTheory.Limits.MulticospanIndex.fstproof · cited by 39

Cited by257

Results whose statement or proof uses this declaration.

CategoryTheory.Limits.HasMultiequalizerproof · cited by 88
CategoryTheory.Limits.Multiforkproof · cited by 69
CategoryTheory.Limits.Multifork.ιstatement · cited by 55
CategoryTheory.Limits.Multiequalizer.ιproof · cited by 37
CategoryTheory.Limits.multiequalizerproof · cited by 33
CategoryTheory.Limits.Multifork.ofιproof · cited by 21
CategoryTheory.GrothendieckTopology.plusCompIsostatement and proof · cited by 20
CategoryTheory.Limits.Multiequalizer.liftproof · cited by 18
CategoryTheory.Limits.Multiequalizer.hom_extproof · cited by 12
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkstatement · cited by 11
CategoryTheory.GrothendieckTopology.sheafifyCompIsostatement and proof · cited by 11
CategoryTheory.Limits.Multifork.conditionstatement and proof · cited by 10

Showing the 200 most cited of 257.