zeroLocus_sup_ideal — Mathlib

English

For any two ideals I and J of A, the vanishing locus of I ∨ J equals the intersection of the vanishing loci of I and J.

Русский

Для любых идеалов I и J кольца A нуль-множество (I ⊔ J) равно пересечению нуль-множества I и J.

LaTeX

$$$ \operatorname{zeroLocus}_{\mathcal{A}}(I \vee J) = \operatorname{zeroLocus}_{\mathcal{A}}(I) \cap \operatorname{zeroLocus}_{\mathcal{A}}(J) $$$

Lean4

theorem zeroLocus_sup_ideal (I J : Ideal A) : zeroLocus 𝒜 ((I ⊔ J : Ideal A) : Set A) = zeroLocus _ I ∩ zeroLocus _ J :=
  (gc_ideal 𝒜).l_sup

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