Mathlib Map

Theorems · Definition · category theory

CategoryTheory.Limits.MulticospanIndex.snd

{J : CategoryTheory.Limits.MulticospanShape} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (self : CategoryTheory.Limits.MulticospanIndex J C) → (b : J.R) → self.left (J.snd b) ⟶ self.right b

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

Defined in
Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Cited by
35 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.MulticospanIndex.multicospan · cited by 167MulticospanIndex.multicos…CategoryTheory.Limits.MulticospanIndex.sndPiMapOfIsLimit · cited by 29MulticospanIndex.sndPiMap…CategoryTheory.Limits.Multifork.ofι · cited by 21Multifork.ofιCategoryTheory.Limits.Multiequalizer.lift · cited by 18Multiequalizer.liftCategoryTheory.Limits.Multifork.condition · cited by 10Multifork.conditionCategoryTheory.Limits.MulticospanIndex.map · cited by 8MulticospanIndex.mapCategoryTheory.Limits.Multiequalizer.lift_ι · cited by 8Multiequalizer.lift_ιCategoryTheory.GrothendieckTopology.plusMap_toPlus · cited by 5GrothendieckTopology.plus…CategoryTheory.Limits.Multifork.IsLimit.fac · cited by 5IsLimit.facCategoryTheory.Limits.Multifork.ofι_π_app · cited by 5Multifork.ofι_π_appCategoryTheory.Limits.Multifork.IsLimit.lift · cited by 4IsLimit.liftCategoryTheory.Limits.MulticospanIndex.sndPiMapOfIsLimit_proj · cited by 3MulticospanIndex.sndPiMap…CategoryTheory.Limits.Multiequalizer.condition · cited by 3Multiequalizer.conditionCategoryTheory.Limits.Multifork.app_right_eq_ι_comp_snd · cited by 2Multifork.app_right_eq_ι_…CategoryTheory.Limits.Multiequalizer.lift.congr_simp · cited by 2lift.congr_simpCategoryTheory.Category · cited by 32673CategoryTheory.CategoryQuiver.Hom · cited by 32603Quiver.HomCategoryTheory.Limits.MulticospanShape · cited by 160Limits.MulticospanShapeCategoryTheory.Limits.MulticospanShape.R · cited by 124MulticospanShape.RCategoryTheory.Limits.MulticospanIndex.left · cited by 119MulticospanIndex.leftCategoryTheory.Limits.MulticospanIndex · cited by 101Limits.MulticospanIndexCategoryTheory.Limits.MulticospanIndex.right · cited by 77MulticospanIndex.rightCategoryTheory.Limits.MulticospanShape.snd · cited by 48MulticospanShape.sndMulticospanIndex.sndCITED BYCITES

Cites8

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

Cited by49

Results whose statement or proof uses this declaration.