isColimitCoconeOfLocallyDirected

Mathlib.AlgebraicGeometry.Cover.Directed

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.OpenCover.isColimitCoconeOfLocallyDirected

Lean4

/-- If `𝒰` is an open cover of `X` that is locally directed, `X` is
the colimit of the components of `𝒰`. -/
def isColimitCoconeOfLocallyDirected : IsColimit 𝒰.coconeOfLocallyDirected
    where
  desc s := 𝒰.glueMorphismsOfLocallyDirected s.ι.app fun _ ↦ s.ι.naturality _
  uniq s m hm := 𝒰.hom_ext _ _ fun j ↦ by simpa using hm j

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

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

Разделы

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

Аффилиация

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