map_PrimeSpectrum_basicOpen_of_affine

Mathlib.AlgebraicGeometry.AffineScheme

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

← MathLib Explorer

English

For affine X, the basic opens give a basis for Opens via basicOpen.

Русский

Для аффинной X базис открытых задаётся через базовые открытые D(f).

LaTeX

$$$$ X.\text{isBasis_basicOpen} \ (X) $$$$

Lean4

theorem map_PrimeSpectrum_basicOpen_of_affine (X : Scheme) [IsAffine X] (f : Γ(X, ⊤)) :
    X.isoSpec.hom ⁻¹ᵁ PrimeSpectrum.basicOpen f = X.basicOpen f :=
  Scheme.toSpecΓ_preimage_basicOpen _ _

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

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

Разделы

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

Аффилиация

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