Theorems · Definition · category theory

Condensed.lanPresheafIso

{S : Profinite} →
  {F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))} →
    CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op) →
      ((Condensed.lanPresheaf F).obj (Opposite.op S) ≅ F.obj (Opposite.op S))

A presheaf, which takes a profinite set written as a cofiltered limit to the corresponding colimit, agrees with the left Kan extension of its restriction.

Defined in

Mathlib.Condensed.Discrete.Colimit

Cited by

1 results in Mathlib

Foundations

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