English
The natural isomorphism between global sections on X and the global sections of Spec Γ(X,U) commutes with the relevant structure maps from the affine open U.
Русский
Естественный изоморфизм между глобальными секциями на X и глобальными секциями Spec Γ(X,U) коммутирует с соответствующими структурными отображениями от афинного открытого множества U.
LaTeX
$$$(\mathrm{Scheme.\,ΓSpecIso}(X,U))^{\mathrm{hom}} \circ h_U^{\mathrm{fromSpec}}(U) = (\mathrm{Spec}(X.presheaf.obj{unop:=U})).presheaf.map(eqToHom(h_U.fromSpec_preimage_self).op$$$
Lean4
theorem ΓSpecIso_hom_fromSpec_app :
(Scheme.ΓSpecIso Γ(X, U)).hom ≫ hU.fromSpec.app U =
(Spec Γ(X, U)).presheaf.map (eqToHom hU.fromSpec_preimage_self).op :=
by
simp only [fromSpec, Scheme.comp_coeBase, Opens.map_comp_obj, Scheme.comp_app, Scheme.Opens.ι_app_self, eqToHom_op,
Scheme.app_eq _ U.ι_preimage_self, Scheme.Opens.toScheme_presheaf_map, eqToHom_unop, eqToHom_map U.ι.opensFunctor,
Opens.map_top, isoSpec_inv_appTop, Scheme.Opens.topIso_hom, Category.assoc, ← Functor.map_comp_assoc, eqToHom_trans,
eqToHom_refl, X.presheaf.map_id, Category.id_comp, Iso.hom_inv_id_assoc]
