English
Under an open immersion f, the image of the zero locus in X of a family of sections s is the zero locus in Y of the transformed sections, intersected with the range of f.base.
Русский
При открытом вложении f образ нулевого множества в X совпадает с нулевым множеством в Y от преобразованных элементов, пересечённым с образами f.base.
LaTeX
$$$f.base '' X.zeroLocus s = Y.zeroLocus\(U := f ''ᵁ U\)\((f.appIso U).inv.hom '' s\) \cap \operatorname{range}(f.base).$$$
Lean4
theorem image_zeroLocus {U : X.Opens} (s : Set Γ(X, U)) :
f.base '' X.zeroLocus s = Y.zeroLocus (U := f ''ᵁ U) ((f.appIso U).inv.hom '' s) ∩ Set.range f.base :=
by
ext x
by_cases hx : x ∈ Set.range f.base
· obtain ⟨x, rfl⟩ := hx
simp only [f.isOpenEmbedding.injective.mem_set_image, Scheme.mem_zeroLocus_iff, ← SetLike.mem_coe,
Set.mem_inter_iff, Set.forall_mem_image, ← Scheme.image_basicOpen, IsOpenMap.coe_functor_obj, Set.mem_range,
exists_apply_eq_apply, and_true]
· simp only [Set.mem_inter_iff, hx, and_false, iff_false]
exact fun H ↦ hx (Set.image_subset_range _ _ H)
