lanSheafProfinite

Mathlib.Condensed.Discrete.Colimit

URI: https://scilib.ai/kg/mathlib#Condensed.lanSheafProfinite

Lean4

/-- `lanPresheaf (locallyConstantPresheaf X)` is a sheaf for the coherent topology on `Profinite`.
-/
def lanSheafProfinite (X : Type (u + 1)) : Sheaf (coherentTopology Profinite.{u}) (Type (u + 1))
    where
  val := lanPresheaf (locallyConstantPresheaf X)
  cond :=
    by
    rw [Presheaf.isSheaf_of_iso_iff (lanPresheafNatIso fun _ ↦ isColimitLocallyConstantPresheafDiagram _ _)]
    exact
      ((CompHausLike.LocallyConstant.functor.{u, u + 1} (hs := fun _ _ _ ↦
              ((Profinite.effectiveEpi_tfae _).out 0 2).mp)).obj
          X).cond

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru