Mathlib Map

Theorems · Definition · category theory

CategoryTheory.Limits.MultispanIndex.snd

{J : CategoryTheory.Limits.MultispanShape} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (self : CategoryTheory.Limits.MultispanIndex J C) → (a : J.L) → self.left a ⟶ self.right (J.snd a)

A family of maps from left a to right (J.snd a)

Defined in
Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Cited by
40 results in Mathlib
Foundations
Depth 3 from the axioms · uses no axioms
Assumes
CategoryTheory.Category
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CategoryTheory.Limits.MultispanIndex.multispan · cited by 139MultispanIndex.multispanCategoryTheory.Limits.MultispanIndex.sndSigmaMapOfIsColimit · cited by 29MultispanIndex.sndSigmaMa…CategoryTheory.Limits.MultispanIndex.map · cited by 22MultispanIndex.mapCategoryTheory.Limits.MultispanIndex.toLinearOrder · cited by 20MultispanIndex.toLinearOr…CategoryTheory.Limits.Multicofork.ofπ · cited by 15Multicofork.ofπCategoryTheory.Limits.Multicoequalizer.desc · cited by 10Multicoequalizer.descCategoryTheory.Limits.Multicofork.condition · cited by 9Multicofork.conditionTopCat.GlueData.ι_eq_iff_rel · cited by 4GlueData.ι_eq_iff_relCategoryTheory.Limits.Multicoequalizer.condition · cited by 3Multicoequalizer.conditionCategoryTheory.Limits.Multicoequalizer.π_desc · cited by 3Multicoequalizer.π_descCategoryTheory.Limits.Multicoequalizer.π_desc_assoc · cited by 3Multicoequalizer.π_desc_a…CategoryTheory.Limits.Multicofork.IsColimit.isPushout.multicofork · cited by 3isPushout.multicoforkCategoryTheory.Limits.Multicofork.IsColimit.desc · cited by 3IsColimit.descCategoryTheory.Limits.Multicofork.IsColimit.hom_ext · cited by 3IsColimit.hom_extCategoryTheory.Limits.MultispanIndex.inj_sndSigmaMapOfIsColimit · cited by 2MultispanIndex.inj_sndSig…CategoryTheory.Category · cited by 32673CategoryTheory.CategoryQuiver.Hom · cited by 32603Quiver.HomCategoryTheory.Limits.MultispanShape.L · cited by 129MultispanShape.LCategoryTheory.Limits.MultispanIndex.right · cited by 117MultispanIndex.rightCategoryTheory.Limits.MultispanIndex · cited by 102Limits.MultispanIndexCategoryTheory.Limits.MultispanShape · cited by 102Limits.MultispanShapeCategoryTheory.Limits.MultispanIndex.left · cited by 85MultispanIndex.leftCategoryTheory.Limits.MultispanShape.snd · cited by 46MultispanShape.sndMultispanIndex.sndCITED BYCITES

Cites8

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

Cited by53

Results whose statement or proof uses this declaration.