fromAffineRefinement

Mathlib.AlgebraicGeometry.Cover.Open

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

Lean4

/-- Given any open cover `𝓤`, this is an affine open cover which refines it. -/
def fromAffineRefinement {X : Scheme.{u}} (𝓤 : X.OpenCover) : 𝓤.affineRefinement.openCover ⟶ 𝓤
    where
  idx j := j.fst
  app j := (𝓤.X j.fst).affineCover.f _

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

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

Разделы

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

Аффилиация

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