residue_surjective

Mathlib.AlgebraicGeometry.ResidueField

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

English

The same surjectivity statement for the residue map between stalks and residue fields.

Русский

Та же сюръективность резидуального отображения между стелками и полями остатка.

LaTeX

$$$$ X.\mathrm{residue}(x) \text{ is surjective}. $$$$

Lean4

theorem residue_surjective (X : Scheme.{u}) (x) : Function.Surjective (X.residue x) :=
  Ideal.Quotient.mk_surjective

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

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

Разделы

Аффилиация

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