zeroLocus_span — Mathlib

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

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