English
If two subopens V, W of U correspond under the inclusion U.ι, then the induced presheaf maps agree after applying the appropriate eqToHom.
Русский
Если два подпуста V и W открыты в U и соответствуют включению U.ι, то порождающие отображения расшитого пространства согласуются после применения соответствующего eqToHom.
LaTeX
$$$ X.presheaf.map (eqToHom e).op = U.toScheme.presheaf.map (eqToHom \\<| U.isOpenEmbedding.functor_obj_injective e).op $$$
Lean4
theorem eq_presheaf_map_eqToHom {V W : Opens U} (e : U.ι ''ᵁ V = U.ι ''ᵁ W) :
X.presheaf.map (eqToHom e).op = U.toScheme.presheaf.map (eqToHom <| U.isOpenEmbedding.functor_obj_injective e).op :=
rfl