toTopGlueData

Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.PresheafedSpace.GlueData.toTopGlueData

← MathLib Explorer

English

Same as previous, alternative presentation.

Русский

То же, альтернативная формулировка.

LaTeX

$$$IsIso(f)$ given epi f.base$$

Lean4

/-- The glue data of topological spaces associated to a family of glue data of PresheafedSpaces. -/
abbrev toTopGlueData : TopCat.GlueData :=
  { f_open := fun i j => (D.f_open i j).base_open
    toGlueData := 𝖣.mapGlueData (forget C) }

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

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

Разделы

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

Аффилиация

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