Mathlib Map

Theorems · Definition · category theory

CompHausLike.finiteCoproduct.isColimit

{P : TopCat → Prop} →
  {α : Type w} →
    [inst : Finite α] →
      (X : α → CompHausLike P) →
        [inst_1 : CompHausLike.HasExplicitFiniteCoproduct X] →
          CategoryTheory.Limits.IsColimit (CompHausLike.finiteCoproduct.cofan X)

The explicit finite coproduct cocone is a colimit cocone.

Defined in
Mathlib.Topology.Category.CompHausLike.Limits
Cited by
3 results in Mathlib
Foundations
Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FiniteCompHausLike.HasExplicitFiniteCoproduct
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CompHaus.effectiveEpiFamily_tfae · cited by 3CompHaus.effectiveEpiFami…CompHausLike.Sigma.isOpenEmbedding_ι · cited by 1Sigma.isOpenEmbedding_ιCompHausLike.sigmaComparison_eq_comp_isos · cited by 0CompHausLike.sigmaCompari…Finite · cited by 3029FiniteCategoryTheory.Discrete · cited by 2447CategoryTheory.DiscreteTopCat · cited by 1889TopCatCategoryTheory.Limits.IsColimit · cited by 773Limits.IsColimitCategoryTheory.Discrete.functor · cited by 633Discrete.functorCategoryTheory.Limits.Cofan.inj · cited by 170Cofan.injCompHausLike · cited by 145CompHausLikeCategoryTheory.Limits.Cofan · cited by 124Limits.CofanCompHausLike.HasExplicitFiniteCoproduct · cited by 8CompHausLike.HasExplicitF…CompHausLike.finiteCoproduct.desc · cited by 4finiteCoproduct.descCategoryTheory.Limits.Cofan.IsColimit.mk · cited by 3IsColimit.mkCompHausLike.finiteCoproduct.cofan · cited by 2finiteCoproduct.cofanfiniteCoproduct.isColimitCITED BYCITES

Cites12

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

Cited by3

Results whose statement or proof uses this declaration.