Theorems · Definition · category theory

Condensed.isColimitLocallyConstantPresheaf

{I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    [CategoryTheory.IsCofiltered I] →
      {F : CategoryTheory.Functor I FintypeCat} →
        (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) →
          (X : Type (u + 1)) →
            CategoryTheory.Limits.IsLimit c →
              [∀ (i : I), CategoryTheory.Epi (c.π.app i)] →
                CategoryTheory.Limits.IsColimit ((Condensed.locallyConstantPresheaf X).mapCocone c.op)

The functor locallyConstantPresheaf takes cofiltered limits of finite sets with surjective projection maps to colimits.

Defined in

Mathlib.Condensed.Discrete.Colimit

Cited by

1 results in Mathlib

Foundations

Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.IsCofilteredCategoryTheory.Epi