English
In an affine setting, the basic open subset defined by f in Spec R coincides with the basic open defined by the corresponding image under ΓSpecIso: Spec R basicOpen inv f = PrimeSpectrum.basicOpen f.
Русский
В аффинном случае базовая открытая подмножество, задаваемое f в Spec R, совпадает с базовой открытой подмножество, заданной образующим элементом: Spec R basicOpen inv f = PrimeSpectrum.basicOpen f.
LaTeX
$$$(\mathrm{Spec} R).basicOpen ((\mathrm{Scheme.ΓSpecIso R}).inv f) = \mathrm{PrimeSpectrum}.basicOpen f$$$
Lean4
theorem basicOpen_eq_of_affine {R : CommRingCat} (f : R) :
(Spec R).basicOpen ((Scheme.ΓSpecIso R).inv f) = PrimeSpectrum.basicOpen f :=
by
ext x
simp only [SetLike.mem_coe, Scheme.mem_basicOpen_top]
suffices IsUnit (StructureSheaf.toStalk R x f) ↔ f ∉ PrimeSpectrum.asIdeal x by exact this
rw [← isUnit_map_iff (StructureSheaf.stalkToFiberRingHom R x).hom, StructureSheaf.stalkToFiberRingHom_toStalk]
exact
(IsLocalization.AtPrime.isUnit_to_map_iff (Localization.AtPrime (PrimeSpectrum.asIdeal x)) (PrimeSpectrum.asIdeal x)
f :
_)
