V

Mathlib.AlgebraicGeometry.Gluing

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.IsLocallyDirected.V

Lean4

/-- (Implementation detail)
The intersection `V` in the glue data associated to a locally directed diagram. -/
noncomputable def V (i j : J) : (F.obj i).Opens :=
  ⨆ (k : Σ k, (k ⟶ i) × (k ⟶ j)), (F.map k.2.1).opensRange

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

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

Разделы

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

Аффилиация

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