feat(AlgebraicGeometry/ProjectiveSpectrum/Scheme): finish the Proj construction (#12371)

This PR finishes the `Proj` construction for any ring graded by natural numbers:
If $A$ is an $R$ algebra with 𝒜 as its grading i.e. 𝒜 i is an $R$-submodule of $A$ , then `AlgebraicGeometry.Proj 𝒜` is the scheme whose underlying topological space is the collection of homogeneous relevant prime ideals with the Zariski topology; whose sheaf of rings is the collection of functions that are locally homogeneous fractions. We prove that for each `f : A` with positive degree, `Proj | D(f)` (`Proj` as locally ringed space restricted to the basic open set around `f`) is isomorphic to `Spec A^0_f` (prime spectrum of the homogeneous localization of `A` at `f`).

The isomorphism is constructed as the following:
by the Gamma-Spec adjunction, it is sufficient to construct a ring map `A⁰_f → Γ(Proj, pbo f)` from the ring of homogeneous localization of `A` away from `f` to the local sections of structure sheaf of projective spectrum on the basic open set around `f`.

The map `A⁰_f → Γ(Proj, pbo f)` is defined by sending `s ∈ A⁰_f` to the section `x ↦ s` on `pbo f`.

Then we show that the map `Proj | D(f) -> Spec A⁰_f` induces an isomorphism on stalk level, thus is an isomorphism.

Co-authored-by: Andrew Yang <[email protected]>



Co-authored-by: zjj <[email protected]>
Co-authored-by: Andrew Yang <[email protected]>
Co-authored-by: Andrew Yang <[email protected]>

Author: 3 people

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

@@ -82,6 +82,10 @@ If we further assume `m` is positive
   and `Spec A⁰_f` corresponding to the ring map `A⁰_f → Γ(Proj, pbo f)` under the Gamma-Spec
   adjunction defined by sending `s` to the section `x ↦ s` on `pbo f`.
 
+Finally,
+* `AlgebraicGeometry.Proj`: for any `ℕ`-graded ring `A`, `Proj A` is locally affine, hence is a
+  scheme.
+
 ## Reference
 * [Robin Hartshorne, *Algebraic Geometry*][Har77]: Chapter II.2 Proposition 2.5
 -/
@@ -667,6 +671,11 @@ lemma toSpec_base_apply_eq {f} (x : Proj| pbo f) :
     IsLocalization.AtPrime.isUnit_mk'_iff]
   exact not_not
 
+lemma toSpec_base_isIso {f} {m} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) :
+    IsIso (toSpec 𝒜 f).1.base := by
+  convert (projIsoSpecTopComponent f_deg hm).isIso_hom
+  exact DFunLike.ext _ _ <| toSpec_base_apply_eq 𝒜
+
 lemma mk_mem_toSpec_base_apply {f} (x : Proj| pbo f)
     (z : NumDenSameDeg 𝒜 (.powers f)) :
     HomogeneousLocalization.mk z ∈ ((toSpec 𝒜 f).1.base x).asIdeal ↔
@@ -755,6 +764,78 @@ lemma isLocalization_atPrime (f) (x : pbo f) {m} (f_deg : f ∈ 𝒜 m) (hm : 0
     rw [mul_left_comm, mul_left_comm y.den.1, ← tsub_add_cancel_of_le (show 1 ≤ m from hm),
       pow_succ, mul_assoc, mul_assoc, e]
 
+/--
+For an element `f ∈ A` with positive degree and a homogeneous ideal in `D(f)`, we have that the
+stalk of `Spec A⁰_ f` at `y` is isomorphic to `A⁰ₓ` where `y` is the point in `Proj` corresponding
+to `x`.
+-/
+def specStalkEquiv (f) (x : pbo f) {m} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) :
+    (Spec.structureSheaf (A⁰_ f)).presheaf.stalk ((toSpec 𝒜 f).1.base x) ≅
+      CommRingCat.of (AtPrime 𝒜 x.1.asHomogeneousIdeal.toIdeal) :=
+  letI : Algebra (Away 𝒜 f) (AtPrime 𝒜 x.1.asHomogeneousIdeal.toIdeal) :=
+    (mapId 𝒜 (Submonoid.powers_le.mpr x.2)).toAlgebra
+  haveI := isLocalization_atPrime 𝒜 f x f_deg hm
+  (IsLocalization.algEquiv
+    (R := A⁰_ f)
+    (M := ((toSpec 𝒜 f).1.base x).asIdeal.primeCompl)
+    (S := (Spec.structureSheaf (A⁰_ f)).presheaf.stalk ((toSpec 𝒜 f).1.base x))
+    (Q := AtPrime 𝒜 x.1.asHomogeneousIdeal.toIdeal)).toRingEquiv.toCommRingCatIso
+
+lemma toStalk_specStalkEquiv (f) (x : pbo f) {m} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) :
+    StructureSheaf.toStalk (A⁰_ f) ((toSpec 𝒜 f).1.base x) ≫ (specStalkEquiv 𝒜 f x f_deg hm).hom =
+      (mapId _ <| Submonoid.powers_le.mpr x.2 : (A⁰_ f) →+* AtPrime 𝒜 x.1.1.toIdeal) :=
+  letI : Algebra (Away 𝒜 f) (AtPrime 𝒜 x.1.asHomogeneousIdeal.toIdeal) :=
+    (mapId 𝒜 (Submonoid.powers_le.mpr x.2)).toAlgebra
+  letI := isLocalization_atPrime 𝒜 f x f_deg hm
+  (IsLocalization.algEquiv
+    (R := A⁰_ f)
+    (M := ((toSpec 𝒜 f).1.base x).asIdeal.primeCompl)
+    (S := (Spec.structureSheaf (A⁰_ f)).presheaf.stalk ((toSpec 𝒜 f).1.base x))
+    (Q := AtPrime 𝒜 x.1.asHomogeneousIdeal.toIdeal)).toAlgHom.comp_algebraMap
+
+lemma stalkMap_toSpec (f) (x : pbo f) {m} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) :
+    LocallyRingedSpace.stalkMap (toSpec 𝒜 f) x =
+      (specStalkEquiv 𝒜 f x f_deg hm).hom ≫ (Proj.stalkIso' 𝒜 x.1).toCommRingCatIso.inv ≫
+      ((Proj.toLocallyRingedSpace 𝒜).restrictStalkIso (Opens.openEmbedding _) x).inv :=
+  IsLocalization.ringHom_ext (R := A⁰_ f) ((toSpec 𝒜 f).1.base x).asIdeal.primeCompl
+    (S := (Spec.structureSheaf (A⁰_ f)).presheaf.stalk ((toSpec 𝒜 f).1.base x)) <|
+    (toStalk_stalkMap_toSpec _ _ _).trans <| by
+    rw [awayToΓ_ΓToStalk, ← toStalk_specStalkEquiv, Category.assoc]; rfl
+
+lemma isIso_toSpec (f) {m} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) :
+    IsIso (toSpec 𝒜 f) := by
+  haveI : IsIso (toSpec 𝒜 f).1.base := toSpec_base_isIso 𝒜 f_deg hm
+  haveI (x) : IsIso (LocallyRingedSpace.stalkMap (toSpec 𝒜 f) x) := by
+    rw [stalkMap_toSpec 𝒜 f x f_deg hm]; infer_instance
+  haveI : LocallyRingedSpace.IsOpenImmersion (toSpec 𝒜 f) :=
+    LocallyRingedSpace.IsOpenImmersion.of_stalk_iso (toSpec 𝒜 f)
+      (TopCat.homeoOfIso (asIso <| (toSpec 𝒜 f).1.base)).openEmbedding
+  exact LocallyRingedSpace.IsOpenImmersion.to_iso _
+
 end ProjectiveSpectrum.Proj
 
+open ProjectiveSpectrum.Proj in
+/--
+If `f ∈ A` is a homogeneous element of positive degree, then the projective spectrum restricted to
+`D(f)` as a locally ringed space is isomorphic to `Spec A⁰_f`.
+-/
+def projIsoSpec (f) {m} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) :
+    (Proj| pbo f) ≅ (Spec (A⁰_ f)) :=
+  @asIso (f := toSpec 𝒜 f) (isIso_toSpec 𝒜 f f_deg hm)
+
+/--
+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⟩⟩
+
+
 end AlgebraicGeometry