coconeOfLocallyDirected

Mathlib.AlgebraicGeometry.Cover.Directed

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.Cover.coconeOfLocallyDirected

Lean4

/-- The canonical cocone with point `X` on the functor induced by the locally directed cover `𝒰`.
If `𝒰` is an open cover, this is colimiting (see `OpenCover.isColimitCoconeOfLocallyDirected`).
-/
@[simps]
def coconeOfLocallyDirected : Cocone 𝒰.functorOfLocallyDirected
    where
  pt := X
  ι.app := 𝒰.f

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

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

Разделы

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

Аффилиация

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