zeroLocus_map_of_eq — Mathlib

English

If i is an equality of opens U = V, then pulling back along i does not change the zero locus: zeroLocus((X.presheaf.map (eqToHom i).op).hom '' s) = zeroLocus s.

Русский

Если i реализует равенство открытых подмножеств U = V, то нулевая область не изменяется под тягиванием по i: zeroLocus((X.presheaf.map (eqToHom i).op).hom '' s) = zeroLocus s.

LaTeX

$$$X.zeroLocus\big((X.presheaf.map (eqToHom i).op).hom'' s\big) = X.zeroLocus s$$$

Lean4

theorem zeroLocus_map_of_eq {U V : X.Opens} (i : U = V) (s : Set Γ(X, V)) :
    X.zeroLocus ((X.presheaf.map (eqToHom i).op).hom '' s) = X.zeroLocus s := by ext; simp

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