Mathlib Map

Theorems · Definition · category theory

CategoryTheory.Limits.MulticospanIndex.fst

{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.fst b) ⟶ self.right b

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

Defined in
Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Cited by
39 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.fstPiMapOfIsLimit · cited by 29MulticospanIndex.fstPiMap…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.Limits.Multifork.IsLimit.hom_ext · cited by 6IsLimit.hom_extCategoryTheory.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.MulticospanIndex.fstPiMapOfIsLimit_proj · cited by 4MulticospanIndex.fstPiMap…CategoryTheory.Limits.MulticospanIndex.sectionsEquiv · cited by 4MulticospanIndex.sections…CategoryTheory.Limits.Multifork.IsLimit.lift · cited by 4IsLimit.liftCategoryTheory.Limits.Concrete.multiequalizer_ext · cited by 3Concrete.multiequalizer_e…CategoryTheory.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.fst · cited by 54MulticospanShape.fstMulticospanIndex.fstCITED BYCITES

Cites8

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

Cited by54

Results whose statement or proof uses this declaration.