subset_zeroLocus_iff_le_vanishingIdeal

English

For a set t and s, t ⊆ zeroLocus 𝒜 s iff s ⊆ vanishingIdeal t.

Русский

Для множеств t и s выполняется: t ⊆ zeroLocus 𝒜 s эквивалентно s ⊆ vanishingIdeal t.

LaTeX

$$$$ t \\subseteq \\mathrm{zeroLocus}(\\mathcal{A}, s) \\iff s \\subseteq \\operatorname{vanishingIdeal}(t) $$$$

Lean4

theorem subset_zeroLocus_iff_le_vanishingIdeal (t : Set (ProjectiveSpectrum 𝒜)) (I : Ideal A) :
    t ⊆ zeroLocus 𝒜 I ↔ I ≤ (vanishingIdeal t).toIdeal :=
  ⟨fun h _ k => (mem_vanishingIdeal _ _).mpr fun _ j => (mem_zeroLocus _ _ _).mpr (h j) k, fun h => fun x j =>
    (mem_zeroLocus _ _ _).mpr (le_trans h fun _ h => ((mem_vanishingIdeal _ _).mp h) x j)⟩

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