Mathlib Map

Theorems · Definition · category theory

CategoryTheory.GlueData.diagram

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] →
    (D : CategoryTheory.GlueData C) →
      CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod D.J) C

(Implementation) The diagram to take colimit of.

Defined in
Mathlib.CategoryTheory.GlueData
Cited by
68 results in Mathlib
Foundations
Depth 5 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.GlueData.glued · cited by 44GlueData.gluedCategoryTheory.GlueData.ι · cited by 42GlueData.ιAlgebraicGeometry.Scheme.Cover.hom_ext · cited by 18Cover.hom_extAlgebraicGeometry.Scheme.Pullback.p1 · cited by 18Pullback.p1AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms · cited by 12Cover.ι_glueMorphismsAlgebraicGeometry.Scheme.Cover.glueMorphisms · cited by 10Cover.glueMorphismsAlgebraicGeometry.Scheme.Cover.fromGlued · cited by 9Cover.fromGluedCategoryTheory.GlueData.gluedIso · cited by 9GlueData.gluedIsoCategoryTheory.GlueData.diagramIso · cited by 8GlueData.diagramIsoCategoryTheory.GlueData.ι_gluedIso_inv · cited by 8GlueData.ι_gluedIso_invAlgebraicGeometry.Scheme.Pullback.p2 · cited by 7Pullback.p2AlgebraicGeometry.PresheafedSpace.GlueData.ι_isOpenEmbedding · cited by 7GlueData.ι_isOpenEmbeddingTopCat.GlueData.fromOpenSubsetsGlue · cited by 6GlueData.fromOpenSubsetsG…CategoryTheory.GlueData.ι_jointly_surjective · cited by 6GlueData.ι_jointly_surjec…TopCat.GlueData.ι_eq_iff_rel · cited by 4GlueData.ι_eq_iff_relCategoryTheory.Category · cited by 32673CategoryTheory.CategoryQuiver.Hom · cited by 32603Quiver.HomCategoryTheory.CategoryStruct.comp · cited by 17999CategoryStruct.compCategoryTheory.GlueData.J · cited by 141GlueData.JCategoryTheory.Limits.MultispanShape.L · cited by 129MultispanShape.LCategoryTheory.GlueData.U · cited by 121GlueData.UCategoryTheory.Limits.MultispanIndex · cited by 102Limits.MultispanIndexCategoryTheory.Limits.MultispanShape.prod · cited by 93MultispanShape.prodCategoryTheory.GlueData.V · cited by 88GlueData.VCategoryTheory.GlueData.f · cited by 83GlueData.fCategoryTheory.GlueData · cited by 60CategoryTheory.GlueDataCategoryTheory.Limits.MultispanShape.fst · cited by 50MultispanShape.fstCategoryTheory.Limits.MultispanShape.snd · cited by 46MultispanShape.sndCategoryTheory.GlueData.t · cited by 44GlueData.tGlueData.diagramCITED BYCITES

Cites14

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

Cited by94

Results whose statement or proof uses this declaration.