English
The assembly of appLE maps along open immersions equals the Away.map construction after localization.
Русский
Сборка отображений appLE вдоль открытых включений равна конструированию Away.map после локализации.
LaTeX
$$$\text{appLE}(f) = \mathrm{Away.map}(... )$$$
Lean4
theorem appLE_eq_away_map {X Y : Scheme.{u}} (f : X ⟶ Y) {U : Y.Opens} (hU : IsAffineOpen U) {V : X.Opens}
(hV : IsAffineOpen V) (e) (r : Γ(Y, U)) :
letI := hU.isLocalization_basicOpen r
letI := hV.isLocalization_basicOpen (f.appLE U V e r)
f.appLE (Y.basicOpen r) (X.basicOpen (f.appLE U V e r)) (by simp [Scheme.Hom.appLE]) =
CommRingCat.ofHom (IsLocalization.Away.map _ _ (f.appLE U V e).hom r) :=
by
letI := hU.isLocalization_basicOpen r
letI := hV.isLocalization_basicOpen (f.appLE U V e r)
ext : 1
apply IsLocalization.ringHom_ext (.powers r)
rw [IsLocalization.Away.map, CommRingCat.hom_ofHom, IsLocalization.map_comp, RingHom.algebraMap_toAlgebra,
RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, ← CommRingCat.hom_comp, Scheme.Hom.appLE_map,
Scheme.Hom.map_appLE]
