cover

Mathlib.AlgebraicGeometry.Cover.MorphismProperty

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.AffineCover.cover

Lean4

/-- The cover associated to an affine cover. -/
@[simps]
def cover {X : Scheme.{u}} (𝒰 : X.AffineCover P) : X.Cover (precoverage P)
    where
  I₀ := 𝒰.I₀
  X j := Spec (𝒰.X j)
  f := 𝒰.f
  mem₀ := by
    rw [presieve₀_mem_precoverage_iff]
    refine ⟨fun x ↦ ?_, 𝒰.map_prop⟩
    obtain ⟨y, hy⟩ := 𝒰.covers x
    use 𝒰.idx x, y

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

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

Разделы

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

Аффилиация

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