functor

Mathlib.Condensed.Discrete.LocallyConstant

URI: https://scilib.ai/kg/mathlib#CompHausLike.LocallyConstant.functor

Lean4

/-- `CompHausLike.LocallyConstant.functorToPresheaves` lands in sheaves. -/
@[simps]
def functor :
    haveI := CompHausLike.preregular hs
    Type (max u w) ⥤ Sheaf (coherentTopology (CompHausLike.{u} P)) (Type (max u w))
    where
  obj
    X :=
    { val := functorToPresheaves.{u, w}.obj X
      cond := by
        rw [Presheaf.isSheaf_of_iso_iff (functorToPresheavesIso P hs X)]
        exact ((TopCat.discrete.obj X).toSheafCompHausLike P hs).cond }
  map f := ⟨functorToPresheaves.{u, w}.map f⟩

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

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

Разделы

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

Аффилиация

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