zeroLocus_map — Mathlib

English

Let U ⊆ V be opens in X and s a set of sections over V. Then the zero locus of the pullback of s along the map to V equals the zero locus of s plus the complement of U.

Русский

Пусть U ⊆ V — открытые подмножества в X и s — семейство секций над V. Тогда нулевая область образа s вдоль отображения в V равна нулевой области s плюс комплемент U.

LaTeX

$$$ X.zeroLocus((X.presheaf.map (homOfLE i).op).hom '' s) = X.zeroLocus s \\cup U^c $$$

Lean4

theorem zeroLocus_map {U V : X.Opens} (i : U ≤ V) (s : Set Γ(X, V)) :
    X.zeroLocus ((X.presheaf.map (homOfLE i).op).hom '' s) = X.zeroLocus s ∪ Uᶜ :=
  by
  ext x
  suffices (∀ f ∈ s, x ∈ U → x ∉ X.basicOpen f) ↔ x ∈ U → (∀ f ∈ s, x ∉ X.basicOpen f) by simpa [or_iff_not_imp_right]
  grind

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