Theorems · Definition · category theory

Condensed.isoLocallyConstantOfIsColimit

(F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) →
  [CategoryTheory.Limits.PreservesFiniteProducts F] →
    ((S : Profinite) → CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)) →
      (F ≅
        Condensed.locallyConstantPresheaf
          (F.obj (FintypeCat.toProfinite.op.obj (Opposite.op (FintypeCat.of PUnit.{u + 1})))))

A presheaf F, which takes a profinite set written as a cofiltered limit to the corresponding colimit, is isomorphic to the presheaf LocallyConstant - F(*).

Defined in

Mathlib.Condensed.Discrete.Colimit

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Limits.PreservesFiniteProducts