English
For a homogeneous element f of positive degree, the basic open subset D_+(f) inside Proj 𝒜 is canonically isomorphic to the spectrum of the degree-zero part of the away localization at f, i.e. D_+(f) ≅ Spec Away 𝒜 f.
Русский
Для однородного элемента f положительной степени базовый открытый множитель D_+(f) внутри Proj 𝒜 естественным образом изоморфен спектру степени ноль локализации Away 𝒜 f: D_+(f) ≅ Spec Away 𝒜 f.
LaTeX
$$$(\text{basicOpen } 𝒜 f).\text{toScheme} \cong \operatorname{Spec}(\operatorname{Away} 𝒜 f)$$$
Lean4
/-- The canonical isomorphism `Proj A |_ D₊(f) ≅ Spec (A_f)₀`
when `f` is homogeneous of positive degree. -/
@[simps! -isSimp hom]
noncomputable def basicOpenIsoSpec : (basicOpen 𝒜 f).toScheme ≅ Spec (.of <| Away 𝒜 f) :=
have : IsIso (basicOpenToSpec 𝒜 f) :=
by
apply (isIso_iff_of_reflects_iso _ Scheme.forgetToLocallyRingedSpace).mp ?_
convert ProjectiveSpectrum.Proj.isIso_toSpec 𝒜 f f_deg hm using 1
refine Eq.trans ?_ (ΓSpec.locallyRingedSpaceAdjunction.homEquiv_apply _ _ _).symm
dsimp [basicOpenToSpec, Scheme.Opens.toSpecΓ]
simp only [eqToHom_op, Category.assoc, ← Spec.map_comp]
rfl
asIso (basicOpenToSpec 𝒜 f)
