instIsProperToSpecZeroOfFiniteTypeSubtypeMemSubmoduleOfNatNat

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Proj.instIsProperToSpecZeroOfFiniteTypeSubtypeMemSubmoduleOfNatNat

English

For a point x in Proj|pbo f, the corresponding ideal carrier x is a prime ideal of A⁰_f.

Русский

Для точки x в Proj|pbo f соответствующий идеал carrier x является простым идеалом A⁰_f.

LaTeX

$$$\text{carrier}(x)\quad \text{IsPrime over }A⁰_f$$$

Lean4

instance [Algebra.FiniteType (𝒜 0) A] : IsProper (Proj.toSpecZero 𝒜) where

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

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

Разделы

Аффилиация

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