English
There is a canonical isomorphism between the basicOpen map and the away map on affine opens.
Русский
Существует канонический изоморфизм между базовым открытием и away-map на афинных открытых подмножеств.
LaTeX
$$$Arrow.mk(f.app(Y.basicOpen r)) \cong Arrow.mk(\mathrm{Away.map}(Y.basicOpen r))$$$
Lean4
theorem app_basicOpen_eq_away_map {X Y : Scheme.{u}} (f : X ⟶ Y) {U : Y.Opens} (hU : IsAffineOpen U)
(h : IsAffineOpen (f ⁻¹ᵁ U)) (r : Γ(Y, U)) :
haveI := hU.isLocalization_basicOpen r
haveI := h.isLocalization_basicOpen (f.app U r)
f.app (Y.basicOpen r) =
(CommRingCat.ofHom (IsLocalization.Away.map Γ(Y, Y.basicOpen r) Γ(X, X.basicOpen (f.app U r)) (f.app U).hom r) ≫
X.presheaf.map (eqToHom (by simp)).op) :=
by
haveI := hU.isLocalization_basicOpen r
haveI := h.isLocalization_basicOpen (f.app U r)
ext : 1
apply IsLocalization.ringHom_ext (.powers r)
rw [IsLocalization.Away.map, CommRingCat.hom_comp, RingHom.comp_assoc, CommRingCat.hom_ofHom, IsLocalization.map_comp,
RingHom.algebraMap_toAlgebra, RingHom.algebraMap_toAlgebra, ← RingHom.comp_assoc, ← CommRingCat.hom_comp, ←
CommRingCat.hom_comp, ← X.presheaf.map_comp]
simp
