zeroLocus_anti_mono_homogeneousIdeal

English

If s ≤ t for homogeneous ideals, then the zero locus is anti-monotone with respect to t and s.

Русский

Если s ≤ t для однородных идеалов, нулевая локация anti-монотно относится к t и s.

LaTeX

$$$s \\le t \\Rightarrow \\zeroLocus 𝒜 (t) \\subseteq \\zeroLocus 𝒜 (s)$$$

Lean4

theorem zeroLocus_anti_mono_homogeneousIdeal {s t : HomogeneousIdeal 𝒜} (h : s ≤ t) :
    zeroLocus 𝒜 (t : Set A) ⊆ zeroLocus 𝒜 (s : Set A) :=
  (gc_homogeneousIdeal _).monotone_l h

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