English
The global sections map from R to the structure sheaf over the whole space factors through the usual localization at 1 and the standard basic open at 1 via the structure sheaf map.
Русский
Глобальная карта секций из R в 𝒪_X(⊤) факторируется через локализацию в 1 и стандартное базовое открытие в 1 через отображение структуры sheaf.
LaTeX
$$$toOpen(R, \\top) = \\text{ofHom}(\\text{algebraMap } R (\\mathrm{Away}(1))) \\circ \\text{ofHom}(\\text{toBasicOpen}(R,1)) \\circ (\\text{structureSheaf } R).1.map(\\text{eqToHom } \\mathrm{PrimeSpectrum.basicOpen_one}.symm .\\ ! )$$
Lean4
@[elementwise]
theorem to_global_factors :
toOpen R ⊤ =
CommRingCat.ofHom (algebraMap R (Localization.Away (1 : R))) ≫
CommRingCat.ofHom (toBasicOpen R (1 : R)) ≫
(structureSheaf R).1.map (eqToHom PrimeSpectrum.basicOpen_one.symm).op :=
by
rw [← Category.assoc]
change
toOpen R ⊤ =
(CommRingCat.ofHom <| (toBasicOpen R 1).comp (algebraMap R (Localization.Away 1))) ≫
(structureSheaf R).1.map (eqToHom _).op
rw [localization_toBasicOpen R, CommRingCat.ofHom_hom, toOpen_res]
