Theorems · Definition · category theory

CategoryTheory.Limits.MultispanIndex.fstSigmaMapOfIsColimit

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      (I : CategoryTheory.Limits.MultispanIndex J C) →
        {c : CategoryTheory.Limits.Cofan I.left} →
          (d : CategoryTheory.Limits.Cofan I.right) → CategoryTheory.Limits.IsColimit c → (c.pt ⟶ d.pt)

The induced map ∐ I.left ⟶ ∐ I.right via I.fst for colimiting cofans.

Defined in: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Cited by: 29 results in Mathlib
Foundations: Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites18

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.Homstatement · cited by 32,603
CategoryTheory.CategoryStruct.compproof · cited by 17,999
CategoryTheory.Discretestatement · cited by 2,447
CategoryTheory.Limits.Cocone.ptstatement · cited by 1,354
CategoryTheory.Limits.IsColimitstatement and proof · cited by 773
CategoryTheory.Discrete.functorstatement · cited by 633
CategoryTheory.Limits.Cofan.injproof · cited by 170
CategoryTheory.Limits.MultispanShape.Rstatement · cited by 133
CategoryTheory.Limits.MultispanShape.Lstatement and proof · cited by 129
CategoryTheory.Limits.Cofanstatement and proof · cited by 124
CategoryTheory.Limits.MultispanIndex.rightstatement and proof · cited by 117

Cited by36

Results whose statement or proof uses this declaration.

CategoryTheory.Limits.MultispanIndex.fstSigmaMapproof · cited by 16
CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctorstatement and proof · cited by 9
CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctorstatement · cited by 9
CategoryTheory.Limits.Multicofork.ofSigmaCoforkstatement and proof · cited by 6
CategoryTheory.Limits.Multicofork.toSigmaCoforkstatement · cited by 5
TopCat.GlueData.ι_eq_iff_relproof · cited by 4
CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimitstatement and proof · cited by 4
CategoryTheory.Limits.MultispanIndex.inj_fstSigmaMapOfIsColimitstatement · cited by 2
CategoryTheory.Limits.MultispanIndex.inj_fstSigmaMapOfIsColimit_assocstatement and proof · cited by 2
CategoryTheory.Limits.MultispanIndex.parallelPairDiagramOfIsColimitproof · cited by 2
CategoryTheory.Limits.Multicofork.sigma_conditionstatement and proof · cited by 2
CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_ι_appstatement and proof · cited by 1