English
The morphism toSpec 𝒜 f is an isomorphism to the Spec of the localized ring, under mild hypotheses; in particular, this furnishes an open immersion that is an isomorphism onto the target.
Русский
Отображение toSpec 𝒜 f является изоморфизмом к Spec локализованной кольцевой структуры; в частности, это открытое внедрение, изоморфное целевой схеме.
LaTeX
$$$$\text{IsIso}(toSpec\ 𝒜 f)$$$$
Lean4
/-- This is the scheme `Proj(A)` for any `ℕ`-graded ring `A`.
-/
def «Proj» : Scheme where
__ := «Proj».toLocallyRingedSpace 𝒜
local_affine
(x :
Proj.T) := by
classical
obtain ⟨f, m, f_deg, hm, hx⟩ : ∃ (f : A) (m : ℕ) (_ : f ∈ 𝒜 m) (_ : 0 < m), f ∉ x.1 :=
by
by_contra!
refine x.not_irrelevant_le fun z hz ↦ ?_
rw [← DirectSum.sum_support_decompose 𝒜 z]
exact x.1.toIdeal.sum_mem fun k hk ↦ this _ k (SetLike.coe_mem _) <| by_contra <| by aesop
exact ⟨⟨pbo f, hx⟩, .of (A⁰_ f), ⟨projIsoSpec 𝒜 f f_deg hm⟩⟩
