English
The basicOpen of an affine open yields a localization away with respect to the basicOpen f.
Русский
Базовая область афинного открытого множества даёт локализацию away по базовому открытому f.
LaTeX
$$$IsLocalization.Away \; f \; Γ(X, X.basicOpen f)$$$
Lean4
theorem isLocalization_basicOpen : IsLocalization.Away f Γ(X, X.basicOpen f) :=
by
apply
(IsLocalization.isLocalization_iff_of_ringEquiv (Submonoid.powers f)
(asIso <| basicOpenSectionsToAffine hU f).commRingCatIsoToRingEquiv).mpr
convert StructureSheaf.IsLocalization.to_basicOpen _ f using 1
-- Porting note: more hand holding is required here, the next 3 lines were not necessary
congr 1
dsimp [CommRingCat.ofHom, RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, basicOpenSectionsToAffine]
rw [hU.fromSpec.naturality_assoc, hU.fromSpec_app_self]
simp only [Category.assoc, ← Functor.map_comp, ← op_comp]
exact CommRingCat.hom_ext_iff.mp (StructureSheaf.toOpen_res _ _ _ _)
