instIsPrimeToIdealNatSubmoduleAsHomogeneousIdeal

English

Let 𝒜 be a graded algebra as above. For every point x in the projective spectrum ProjectiveSpectrum 𝒜, the associated ideal x.asHomogeneousIdeal.toIdeal is a prime ideal of A.

Русский

Пусть 𝒜 — градуированная алгебра. Для каждой точки x в проективном спектре ProjectiveSpectrum 𝒜 соответствующий ей идеал x.asHomogeneousIdeal.toIdeal является простым идеалом в A.

LaTeX

$$$$ \\forall x \\in \\mathrm{ProjectiveSpectrum}(\\mathcal{A}), \\ \\mathrm{IsPrime}\\bigl( x.asHomogeneousIdeal.toIdeal \\bigr). $$$$

Lean4

instance (x : ProjectiveSpectrum 𝒜) : Ideal.IsPrime x.asHomogeneousIdeal.toIdeal :=
  x.isPrime

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