range_fromSpecResidueField

Mathlib.AlgebraicGeometry.ResidueField

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

English

The image of the base map from Spec of the residue field κ(x) to X is exactly the singleton {x}.

Русский

Образ базовой карты от Spec остаточного поля κ(x) в X есть единичный множитель {x}.

LaTeX

$$Set.range (X.fromSpecResidueField x).base = { x }$$

Lean4

theorem range_fromSpecResidueField (x : X.carrier) : Set.range (X.fromSpecResidueField x).base = { x } := by simp

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

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

Разделы

Аффилиация

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