English
Taking the span of a set of sections does not change the zero locus.
Русский
Пределение нулевой области не меняется при взятии линейного замыкания набора секций.
LaTeX
$$$X.zeroLocus (\\operatorname{span} s) = X.zeroLocus s$$$
Lean4
theorem zeroLocus_span {U : X.Opens} (s : Set Γ(X, U)) : X.zeroLocus (U := U) (Ideal.span s) = X.zeroLocus s :=
by
ext x
simp only [Scheme.mem_zeroLocus_iff, SetLike.mem_coe]
refine ⟨fun H f hfs ↦ H f (Ideal.subset_span hfs), fun H f ↦ Submodule.span_induction H ?_ ?_ ?_⟩
· simp only [Scheme.basicOpen_zero]; exact not_false
· exact fun a b _ _ ha hb H ↦ (X.basicOpen_add_le a b H).elim ha hb
· simp +contextual