sup_vanishingIdeal_le — Mathlib

English

Membership in the complement of a zero locus corresponds to non-membership of the element in the associated homogeneous ideal.

Русский

Членство в дополнении нуль-множества эквивалентно не принадлежности элемента соответствующему однородному идеалу.

LaTeX

$$$ I \in (\operatorname{zeroLocus}_{\mathcal{A}}(\{f\}) : \ Set (\mathrm{Proj}_{\mathcal{A}}))^{\complement} \iff f \notin I.asHomogeneousIdeal $$$

Lean4

theorem sup_vanishingIdeal_le (t t' : Set (ProjectiveSpectrum 𝒜)) :
    vanishingIdeal t ⊔ vanishingIdeal t' ≤ vanishingIdeal (t ∩ t') :=
  by
  intro r
  rw [← HomogeneousIdeal.mem_iff, HomogeneousIdeal.toIdeal_sup, mem_vanishingIdeal, Submodule.mem_sup]
  rintro ⟨f, hf, g, hg, rfl⟩ x ⟨hxt, hxt'⟩
  rw [HomogeneousIdeal.mem_iff, mem_vanishingIdeal] at hf hg
  apply Submodule.add_mem <;> solve_by_elim

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