Mathlib Map

Theorems · Definition · category theory

CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso

{J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {s t : CategoryTheory.Limits.Cocone F} →
            CategoryTheory.Limits.IsColimit s → CategoryTheory.Limits.IsColimit t → (s.pt ≅ t.pt)

Colimits of F are unique up to isomorphism.

Defined in
Mathlib.CategoryTheory.Limits.IsLimit
Cited by
67 results in Mathlib
Foundations
Depth 31 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CategoryTheory.CategoryCategoryTheory.Category
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom · cited by 45IsColimit.comp_coconePoin…CategoryTheory.Limits.pushoutSymmetry · cited by 30Limits.pushoutSymmetryCategoryTheory.Limits.PreservesCoequalizer.iso · cited by 28PreservesCoequalizer.isoCategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv · cited by 21IsColimit.comp_coconePoin…CategoryTheory.GrothendieckTopology.plusCompIso · cited by 20GrothendieckTopology.plus…CategoryTheory.Limits.colimit.isoColimitCocone · cited by 18colimit.isoColimitCoconeCategoryTheory.preservesColimitIso · cited by 17CategoryTheory.preservesC…CategoryTheory.Limits.PreservesCokernel.iso · cited by 15PreservesCokernel.isoAlgebraicGeometry.Scheme.Hom.normalizationCoprodIso · cited by 15Hom.normalizationCoprodIsoCategoryTheory.Limits.pushoutAssoc · cited by 12Limits.pushoutAssocCategoryTheory.Limits.pushoutLeftPushoutInrIso · cited by 12Limits.pushoutLeftPushout…CategoryTheory.ShortComplex.isoOpcyclesOfIsColimit · cited by 12ShortComplex.isoOpcyclesO…CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv · cited by 12colimit.comp_coconePointU…CategoryTheory.Limits.PreservesPushout.iso · cited by 11PreservesPushout.isoCategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom · cited by 11colimit.comp_coconePointU…CategoryTheory.Category · cited by 32673CategoryTheory.CategoryCategoryTheory.Functor · cited by 16252CategoryTheory.FunctorCategoryTheory.Iso · cited by 3963CategoryTheory.IsoCategoryTheory.Limits.Cocone.pt · cited by 1354Cocone.ptCategoryTheory.Limits.IsColimit · cited by 773Limits.IsColimitCategoryTheory.Limits.Cocone · cited by 746Limits.CoconeCategoryTheory.Functor.mapIso · cited by 224Functor.mapIsoCategoryTheory.Limits.Cocone.forget · cited by 17Cocone.forgetCategoryTheory.Limits.IsColimit.uniqueUpToIso · cited by 13IsColimit.uniqueUpToIsoIsColimit.coconePointUniqueUp…CITED BYCITES

Cites9

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

Cited by124

Results whose statement or proof uses this declaration.