zeroLocus_radical — Mathlib

English

The zero locus depends only on the radical of an ideal: X.zeroLocus I.radical = X.zeroLocus I.

Русский

Область нулей зависит только от радикала идеала: zeroLocus(I.radical) = zeroLocus(I).

LaTeX

$$$X.zeroLocus I.radical = X.zeroLocus I$$$

Lean4

theorem zeroLocus_radical {U : X.Opens} (I : Ideal Γ(X, U)) : X.zeroLocus (U := U) I.radical = X.zeroLocus (U := U) I :=
  by
  refine (X.zeroLocus_mono I.le_radical).antisymm ?_
  simp only [Set.subset_def, mem_zeroLocus_iff, SetLike.mem_coe]
  rintro x H f ⟨n, hn⟩ hx
  rcases n.eq_zero_or_pos with rfl | hn'
  · exact H f (by simpa using I.mul_mem_left f hn) hx
  · exact H _ hn (X.basicOpen_pow f hn' ▸ hx)

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