27.2 Relative glueing to 27.14 Invertible sheaves and…

Section27.2 Relative glueing#

Section 27.2 of the Stacks Project, Tag 01LG. 3 tags here are carried by 6 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01LH, a lemma

Tag 01LH in the Stacks Project.

AlgebraicGeometry.Scheme.BasisGluingData.exists_isPullback_res_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/RelativeGluingOverBasis.lean, line 359. The attribute's comment: “existence of the glued scheme, with the charts identifying each piece with the part of it lying over the corresponding member of the basis”.

Let S be a scheme and B a basis for its topology. Given a scheme D.obj U over U for every U ∈ B, together with morphisms D.res : D.obj V ⟶ D.obj U for V ⊆ U in B identifying D.obj V with the part of D.obj U over V and satisfying the cocycle condition, there is a morphism of schemes f : X ⟶ S and charts i U : D.obj U ⟶ X identifying D.obj U with the part of X over U, compatibly with the restriction morphisms.

theorem exists_isPullback_res_comp (hB : Opens.IsBasis B) (D : BasisGluingData S B) :
    ∃ (X : Scheme.{u}) (f : X ⟶ S) (i : ∀ U : B, D.obj U ⟶ X),
      (∀ U : B, IsPullback (D.proj U) (i U) U.1.ι f) ∧
        ∀ {V U : B} (h : V.1 ≤ U.1), D.res h ≫ i U = i V

AlgebraicGeometry.Scheme.BasisGluingData.existsUnique_isoOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/RelativeGluingOverBasis.lean, line 370. The attribute's comment: “the glued scheme is unique up to unique isomorphism over the base”.

The glued scheme of a gluing datum over a basis of the topology of S is unique up to unique isomorphism over S: between any two solutions of the gluing problem there is exactly one isomorphism compatible with the charts, and it is a morphism over S.

theorem existsUnique_isoOver (hB : Opens.IsBasis B) (D : BasisGluingData S B)
    {X X' : Scheme.{u}} {f : X ⟶ S} {f' : X' ⟶ S}
    {i : ∀ U : B, D.obj U ⟶ X} {i' : ∀ U : B, D.obj U ⟶ X'}
    (hi : ∀ U : B, IsPullback (D.proj U) (i U) U.1.ι f)
    (hi' : ∀ U : B, IsPullback (D.proj U) (i' U) U.1.ι f')
    (hres : ∀ {V U : B} (h : V.1 ≤ U.1), D.res h ≫ i U = i V)
    (hres' : ∀ {V U : B} (h : V.1 ≤ U.1), D.res h ≫ i' U = i' V) :
    ∃! e : X ≅ X', (∀ U : B, i U ≫ e.hom = i' U) ∧ e.hom ≫ f' = f
Tag 01LI, a lemma

Tag 01LI in the Stacks Project.

Stacks.AlgebraicGeometry.RelativeSheafGluing.RelativeSheafGluingData.exists_glued_and_existsUnique_pairIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/RelativeGluingPairUniqueness.lean, line 471. The attribute's comment: “both assertions of the tag as one statement: existence of the glued package — the morphism f, the charts i_U, the quasi-coherent module F, the identifications θ_U and their two compatibilities — and uniqueness of the pair (X, F) up to unique isomorphism over S”.

Stacks Project, Tag 01LI, both of its assertions as one statement. Let 𝒰 be a locally directed open cover of a scheme S, let d be a relative gluing datum over it, and let D be a compatible family of quasi-coherent modules on the schemes of d. Then:

  • existence of the whole package. There is a morphism of schemes f : X ⟶ S, morphisms i a : X a ⟶ X exhibiting each X a as the part of X lying over the a-th member of the cover and compatible with the transition morphisms of d, and a quasi-coherent module F on X together with isomorphisms θ a : F a ≅ (i a)^* F under which the prescribed transition isomorphisms of the F a are the ones induced by F.
  • uniqueness. The pair (X, F) is unique up to unique isomorphism over S: any two glued pairs are related by exactly one isomorphism of pairs.

The two conjuncts are Stacks.AlgebraicGeometry.RelativeSheafGluing.RelativeSheafGluingData.exists_isPullback_localIso and Stacks.AlgebraicGeometry.RelativeSheafGluing.RelativeSheafGluingData.existsUnique_pairIso.

theorem exists_glued_and_existsUnique_pairIso :
    (∃ (X : Scheme.{u}) (f : X ⟶ S) (i : ∀ a, d.functor.obj a ⟶ X)
      (_ : ∀ a, IsPullback (d.natTrans.app a) (i a) (𝒰.f a) f)
      (hi : ∀ {a b : 𝒰.I₀} (hab : a ⟶ b), d.functor.map hab ≫ i b = i a)
      (F : X.Modules), F.IsQuasicoherent ∧
        ∃ θ : ∀ a, D.obj a ≅ (Scheme.Modules.pullback (i a)).obj F,
          ∀ {a b : 𝒰.I₀} (hab : a ⟶ b),
            (D.transitionIso hab).hom ≫ (θ a).hom =
              (Scheme.Modules.pullback (d.functor.map hab)).map (θ b).hom ≫
                (Scheme.Modules.pullbackComp (d.functor.map hab) (i b)).hom.app F ≫
                  (Scheme.Modules.pullbackCongr (hi hab)).hom.app F) ∧
      ∀ (H H' : Gluing d) (R : D.RealizationOn H) (R' : D.RealizationOn H'),
        ∃ p : D.PairIso R R', ∀ q : D.PairIso R R', q = p
Tag 01LK, a remark

Tag 01LK in the Stacks Project.

AlgebraicGeometry.CompatibleRelativeGluingData.colimMap_localHom_toBase, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/RelativeGluingMorphism.lean, line 114. The attribute's comment: “scheme_morphism”.

The morphism induced on the glued schemes is a morphism over the common base.

public lemma colimMap_localHom_toBase :
    colimMap D.localHom ≫ D.target.toBase = D.source.toBase

AlgebraicGeometry.Scheme.BasisGluingData.existsUnique_hom_of_compatible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/RelativeGluingMorphism.lean, line 141. The attribute's comment: “scheme_morphism, for the gluing data over a basis of Tag 01LH”.

Stacks Project, Tag 01LK: functoriality for the data of Lemma 01LH. Let S be a scheme and B a basis for its topology, and let D and D' be gluing data over B as in Tag 01LH, with local schemes D.obj U ⟶ U and D'.obj U ⟶ U and restriction morphisms D.res and D'.res. Let f : X ⟶ S be a scheme glued from D, with charts i U, and g : Y ⟶ S one glued from D', with charts j U. A family of morphisms h U : D.obj U ⟶ D'.obj U over U compatible with the restriction morphisms gives rise to a morphism k : X ⟶ Y over S which restricts back to the h U, and k is the only such morphism.

public theorem existsUnique_hom_of_compatible (hB : Opens.IsBasis B) (D D' : BasisGluingData S B)
    {X Y : Scheme.{u}} {f : X ⟶ S} {g : Y ⟶ S}
    {i : ∀ U : B, D.obj U ⟶ X} {j : ∀ U : B, D'.obj U ⟶ Y}
    (hi : ∀ U : B, IsPullback (D.proj U) (i U) U.1.ι f)
    (hj : ∀ U : B, IsPullback (D'.proj U) (j U) U.1.ι g)
    (hires : ∀ {V U : B} (h : V.1 ≤ U.1), D.res h ≫ i U = i V)
    (hjres : ∀ {V U : B} (h : V.1 ≤ U.1), D'.res h ≫ j U = j V)
    (h : ∀ U : B, D.obj U ⟶ D'.obj U)
    (hover : ∀ U : B, h U ≫ D'.proj U = D.proj U)
    (hcompat : ∀ {V U : B} (hVU : V.1 ≤ U.1), D.res hVU ≫ h U = h V ≫ D'.res hVU) :
    ∃! k : X ⟶ Y, (∀ U : B, i U ≫ k = h U ≫ j U) ∧ k ≫ g = f

Stacks.AlgebraicGeometry.RelativeSheafGluing.exists_pullbackHom_of_transitionCompatible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/RelativeSheafGluingMorphism.lean, line 347. The attribute's comment: “sheaf_morphism”.

Stacks Project, Tag 01LK. Functoriality of relative gluing for quasi-coherent sheaves. Let 𝒰 be a locally directed open cover of a scheme S and let dX, dY be relative gluing data over it, carrying compatible families of quasi-coherent modules realized by ℱ on the glued scheme X and 𝒢 on the glued scheme Y. Given a family of morphisms hᵢ : Xᵢ ⟶ Yᵢ commuting with the restriction maps — hence the morphism h = colimMap of glued schemes — and morphisms τᵢ : hᵢ⁎𝒢ᵢ ⟶ ℱᵢ compatible with the transition isomorphisms of the two families, there is a morphism h⁎𝒢 ⟶ ℱ whose inverse image on the i-th chart is τᵢ, read through the canonical identifications.

The companion half of the remark — that h is a morphism over S restricting to the given hᵢ — is CategoryTheory.Limits.ι_colimMap together with AlgebraicGeometry.CompatibleRelativeGluingData.colimMap_localHom_toBase.

theorem exists_pullbackHom_of_transitionCompatible (hom : dX.functor ⟶ dY.functor)
    (A : DX.Realization) (B : DY.Realization)
    (τ : ∀ i, (Scheme.Modules.pullback (hom.app i)).obj (DY.obj i) ⟶ DX.obj i)
    (hτ : IsTransitionCompatible hom DX DY τ) :
    ∃ ψ : (Scheme.Modules.pullback (colimMap hom)).obj B.sheaf ⟶ A.sheaf, ∀ i,
      (Scheme.Modules.pullback (colimit.ι dX.functor i)).map ψ =
        pullbackChartHom hom A B τ i

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.Scheme.BasisGluingData.exists_isPullback_res_comp · AlgebraicGeometry.Scheme.BasisGluingData.existsUnique_isoOver · Stacks.AlgebraicGeometry.RelativeSheafGluing.RelativeSheafGluingData.exists_glued_and_existsUnique_pairIso · AlgebraicGeometry.CompatibleRelativeGluingData.colimMap_localHom_toBase · AlgebraicGeometry.Scheme.BasisGluingData.existsUnique_hom_of_compatible · Stacks.AlgebraicGeometry.RelativeSheafGluing.exists_pullbackHom_of_transitionCompatible · CategoryTheory.Limits.colimMap · CategoryTheory.Limits.ι_colimMap

Section27.3 Relative spectrum via glueing#

Section 27.3 of the Stacks Project, Tag 01LL. 4 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01LM, a situation

Tag 01LM in the Stacks Project.

Stacks.RelativeSpec.RelativeSpecSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/QuasicoherentSquare.lean, line 207.

A scheme equipped with a quasi-coherent sheaf of commutative algebras over its structure sheaf.

structure RelativeSpecSituation
Tag 01LN, a lemma

Tag 01LN in the Stacks Project.

Stacks.RelativeSpec.isPullback_specMap_restriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/QuasicoherentSquare.lean, line 221.

For nested affine opens U ⊆ U' of the base of a relative spectrum situation, the square formed by the spectra of the sections of the quasi-coherent algebra, the two open subschemes, and their canonical restriction morphisms is cartesian.

theorem isPullback_specMap_restriction (s : RelativeSpecSituation.{u})
    (U U' : s.base.Opens) (hU : IsAffineOpen U) (hU' : IsAffineOpen U') (h : U ≤ U') :
    IsPullback
      (Spec.map (s.algebra.right.obj.map (homOfLE h).op))
      (Spec.map (s.algebra.hom.hom.app (.op U)) ≫ hU.isoSpec.inv)
      (Spec.map (s.algebra.hom.hom.app (.op U')) ≫ hU'.isoSpec.inv)
      (s.base.homOfLE h)
Tag 01LO, a lemma

Tag 01LO in the Stacks Project.

Stacks.RelativeSpec.specMap_restriction_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/QuasicoherentSquare.lean, line 237. The attribute's comment: “the composite of the restriction morphisms of spectra of sections is the restriction morphism”.

For opens U ⊆ U' ⊆ U'' of the base of a relative spectrum situation, the composition of the morphisms Spec A(U) ⟶ Spec A(U') and Spec A(U') ⟶ Spec A(U'') of Stacks.RelativeSpec.isPullback_specMap_restriction is the morphism Spec A(U) ⟶ Spec A(U'') of the same lemma.

theorem specMap_restriction_comp (s : RelativeSpecSituation.{u}) {U U' U'' : s.base.Opens}
    (h : U ≤ U') (h' : U' ≤ U'') :
    Spec.map (s.algebra.right.obj.map (homOfLE h).op) ≫
        Spec.map (s.algebra.right.obj.map (homOfLE h').op) =
      Spec.map (s.algebra.right.obj.map (homOfLE (h.trans h')).op)
Tag 01LP, a lemma

Tag 01LP in the Stacks Project.

Stacks.RelativeSpec.relativeSpectrum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/Construction.lean, line 123. References: EGA II (1.3.1), “existence”; EGA IV (21.12.1), “more general”; SGA 3 I (4.2).

Stacks Project, Tag 01LP, existence. The affine spectra of the sections of a quasi-coherent algebra glue to a scheme over the base, with the prescribed inverse images and the prescribed transition morphisms.

The glued scheme and its structure morphism are Stacks.AffineAlgebraEquivalence.relativeSpec and Stacks.AffineAlgebraEquivalence.relativeSpecToBase; the content added here is that its charts satisfy properties (1) and (2) of the tag.

def relativeSpectrum : RelativeSpectrum s

Stacks.RelativeSpec.existsUnique_relativeSpectrumIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/Construction.lean, line 280.

Stacks Project, Tag 01LP, uniqueness. Any two relative spectra of the same quasi-coherent algebra admit a unique isomorphism over the base compatible with all the charts.

theorem existsUnique_relativeSpectrumIso (X Y : RelativeSpectrum s) :
    ∃! e : X.scheme ≅ Y.scheme,
      (e.hom ≫ Y.toBase = X.toBase) ∧ ∀ U, X.chart U ≫ e.hom = Y.chart U

Stacks.RelativeSpec.gluedSpectrum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/Glueing.lean, line 95. The attribute's comment: “existence and local properties”. References: EGA II (1.3.1), “existence”; SGA 3 I (4.2).

Stacks Project, Tag 01LP, parts (1) and (2). The affine spectra of the sections of a quasi-coherent algebra glue to a scheme over the base, with the prescribed inverse images and transition open immersions.

noncomputable def gluedSpectrum (s : RelativeSpecSituation.{u}) : GluedSpectrum s

Stacks.RelativeSpec.existsUnique_gluedSpectrumIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/Glueing.lean, line 248. The attribute's comment: “uniqueness”.

Stacks Project, Tag 01LP, uniqueness. Any two schemes over the base carrying the affine charts of the relative spectrum admit a unique isomorphism over the base that respects all the charts.

theorem _root_.Stacks.RelativeSpec.existsUnique_gluedSpectrumIso
    (s : RelativeSpecSituation.{u}) (X Y : GluedSpectrum s) :
    ∃! e : X.scheme ≅ Y.scheme,
      (e.hom ≫ Y.toBase = X.toBase) ∧ (∀ U, X.chart U ≫ e.hom = Y.chart U)
Sources
LeanStacks.RelativeSpec.RelativeSpecSituation · Stacks.RelativeSpec.isPullback_specMap_restriction · Stacks.RelativeSpec.specMap_restriction_comp · Stacks.RelativeSpec.relativeSpectrum · Stacks.RelativeSpec.existsUnique_relativeSpectrumIso · Stacks.RelativeSpec.gluedSpectrum · Stacks.RelativeSpec.existsUnique_gluedSpectrumIso

Section27.4 Relative spectrum as a functor#

Section 27.4 of the Stacks Project, Tag 01LQ. 8 tags here are carried by 26 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01LR, an equation

Tag 01LR in the Stacks Project.

Stacks.RelativeSpec.relativeSpecFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpecRepresentability/Basic.lean, line 283.

The contravariant functor sending a test scheme T to the pairs (f : T ⟶ X, φ : A ⟶ f_* 𝒪_T) and a morphism of test schemes to pullback of such pairs.

noncomputable def relativeSpecFunctor (s : RelativeSpecSituation.{u}) :
    Scheme.{u}ᵒᵖ ⥤ Type u

Declarations registered for the tag:

Tag 01LS, a lemma

Tag 01LS in the Stacks Project.

Stacks.RelativeSpec.algebraPullback_nonempty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/BaseChange.lean, line 129. The attribute's comment: “existence of the pulled-back algebra”.

Stacks Project, Tag 01LS. Extension of scalars of a quasi-coherent algebra sheaf along any morphism of schemes exists and is quasi-coherent.

theorem algebraPullback_nonempty : Nonempty (AlgebraPullback s g)

Stacks.RelativeSpec.relativeSpecFunctorPullbackToOriginal_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/BaseChange.lean, line 233. The attribute's comment: “base component of the canonical map to the original functor”.

Stacks Project, Tag 01LS. On a test scheme, the canonical map composes the structural morphism with the base-change morphism.

theorem relativeSpecFunctorPullbackToOriginal_base {T : Scheme.{u}}
    (p : RelativeSpecPair (pullbackAlgebra s g).situation T) :
    ((relativeSpecFunctorPullbackToOriginal s g).app (.op T) p).1 = p.1 ≫ g

Stacks.RelativeSpec.relativeSpecFunctorPullbackToOriginal_algebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/BaseChange.lean, line 240. The attribute's comment: “algebra component of the canonical map to the original functor”.

Stacks Project, Tag 01LS. The algebra component of the canonical map is obtained from the transpose of g⁻¹A ⟶ g⁺A, then pushed forward along the test-scheme map.

theorem relativeSpecFunctorPullbackToOriginal_algebra {T : Scheme.{u}}
    (p : RelativeSpecPair (pullbackAlgebra s g).situation T) :
    HEq ((relativeSpecFunctorPullbackToOriginal s g).app (.op T) p).2.right
      (((TopCat.Sheaf.pullbackPushforwardAdjunction CommRingCat g.base).homEquiv
          s.algebra.right (pullbackAlgebra s g).algebra.right
          (pullbackAlgebra s g).map).hom ≫
        (TopCat.Presheaf.pushforward CommRingCat g.base).map p.2.right)

Stacks.RelativeSpec.relativeSpecFunctor_pullback_iso_pullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/BaseChange.lean, line 330. The attribute's comment: “canonical base-change isomorphism”.

Stacks Project, Tag 01LS. Formation of the relative spectrum functor commutes with arbitrary base change.

noncomputable def relativeSpecFunctor_pullback_iso_pullback :
    relativeSpecFunctor (pullbackAlgebra s g).situation ≅
      pullback (yoneda.map g) (relativeSpecFunctorToBase s)

Stacks.RelativeSpec.relativeSpecFunctor_pullback_iso_pullback_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/BaseChange.lean, line 338. The attribute's comment: “first component of the canonical isomorphism”.

Stacks Project, Tag 01LS. The first component of the canonical base-change isomorphism remembers the map from a test scheme to the new base.

theorem relativeSpecFunctor_pullback_iso_pullback_fst :
    (relativeSpecFunctor_pullback_iso_pullback s g).hom ≫
        pullback.fst (yoneda.map g) (relativeSpecFunctorToBase s) =
      relativeSpecFunctorToBase (pullbackAlgebra s g).situation

Stacks.RelativeSpec.relativeSpecFunctor_pullback_iso_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/BaseChange.lean, line 347. The attribute's comment: “second component of the canonical isomorphism”.

Stacks Project, Tag 01LS. The second component of the isomorphism is the canonical transformation induced by the algebra pullback map.

theorem relativeSpecFunctor_pullback_iso_pullback_snd :
    (relativeSpecFunctor_pullback_iso_pullback s g).hom ≫
        pullback.snd (yoneda.map g) (relativeSpecFunctorToBase s) =
      relativeSpecFunctorPullbackToOriginal s g

Stacks.RelativeSpec.RelativeSpecSituation.baseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/FunctorBaseChange.lean, line 153. The attribute's comment: “the base-changed situation (S', g^*A)”.

Stacks Project, Tag 01LS. The relative-spectrum situation obtained from (S, A) by base change along g : S' ⟶ S: the base is S' and the algebra is A' = g^*A, the pullback g⁻¹A ⊗_{g⁻¹𝒪_S} 𝒪_{S'} of A as an algebra sheaf, which is again quasi-coherent.

def RelativeSpecSituation.baseChange (s : RelativeSpecSituation.{u}) {S' : Scheme.{u}}
    (g : S' ⟶ s.base) : RelativeSpecSituation.{u}

Stacks.RelativeSpec.baseChangeToOriginal_app_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/FunctorBaseChange.lean, line 207. The attribute's comment: “base component of the canonical map to the original functor”.

Stacks Project, Tag 01LS. The morphism to S underlying the image of a pair under the canonical transformation F' ⟶ F is the morphism to S' of the pair, composed with g.

theorem baseChangeToOriginal_app_fst {T : Scheme.{u}}
    (p : RelativeSpecPair (s.baseChange g) T) :
    ((baseChangeToOriginal s g).app (.op T) p).1 = p.1 ≫ g

Stacks.RelativeSpec.baseChangeToOriginal_app_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/FunctorBaseChange.lean, line 216. The attribute's comment: “algebra component of the canonical map to the original functor”.

Stacks Project, Tag 01LS. The algebra map of the image of a pair under the canonical transformation F' ⟶ F is the direct image along g of the pair's algebra map, precomposed with the adjunct of the canonical map g⁻¹A ⟶ g^*A.

theorem baseChangeToOriginal_app_right {T : Scheme.{u}}
    (p : RelativeSpecPair (s.baseChange g) T) :
    ((baseChangeToOriginal s g).app (.op T) p).2.right =
      ((TopCat.Sheaf.pullbackPushforwardAdjunction CommRingCat g.base).homEquiv
          s.algebra.right ((algebraPullback g).obj s.algebra).right
          ((algebraPullbackMap g).app s.algebra)).hom ≫
        (TopCat.Presheaf.pushforward CommRingCat g.base).map p.2.right

Stacks.RelativeSpec.relativeSpecFunctorBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/FunctorBaseChange.lean, line 321. The attribute's comment: “canonical base-change isomorphism”.

Stacks Project, Tag 01LS. Formation of the relative-spectrum functor commutes with arbitrary base change: the functor attached to (S', g^*A) is canonically the fibre product h_{S'} ×_{h_S} F of the functor of points of S' and the functor attached to (S, A) over the functor of points of S.

def relativeSpecFunctorBaseChangeIso :
    relativeSpecFunctor (s.baseChange g) ≅
      pullback (yoneda.map g) (relativeSpecFunctorToBase s)

Stacks.RelativeSpec.relativeSpecFunctorBaseChangeIso_hom_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/FunctorBaseChange.lean, line 329. The attribute's comment: “first component of the canonical isomorphism”.

Stacks Project, Tag 01LS. The first component of the base-change isomorphism is the structural map of F' to the functor of points of the new base.

theorem relativeSpecFunctorBaseChangeIso_hom_fst :
    (relativeSpecFunctorBaseChangeIso s g).hom ≫
        pullback.fst (yoneda.map g) (relativeSpecFunctorToBase s) =
      relativeSpecFunctorToBase (s.baseChange g)

Stacks.RelativeSpec.relativeSpecFunctorBaseChangeIso_hom_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/FunctorBaseChange.lean, line 338. The attribute's comment: “second component of the canonical isomorphism”.

Stacks Project, Tag 01LS. The second component of the base-change isomorphism is the canonical transformation F' ⟶ F induced by the base-change map of algebras.

theorem relativeSpecFunctorBaseChangeIso_hom_snd :
    (relativeSpecFunctorBaseChangeIso s g).hom ≫
        pullback.snd (yoneda.map g) (relativeSpecFunctorToBase s) =
      baseChangeToOriginal s g
Tag 01LT, a lemma

Tag 01LT in the Stacks Project.

Stacks.AffineAlgebraEquivalence.relativeSpecIsoSpecSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpecOpenRestriction/RelativeSpecAffineBase.lean, line 99. The attribute's comment: “the scheme-level form: over an affine base the relative spectrum is the spectrum of the ring of global sections of the algebra”.

[Stacks, Tag 01LT] at the level of schemes. Over an affine base the relative spectrum of a quasi-coherent sheaf of algebras is the spectrum of the ring of global sections of the algebra:

Spec_S(A) ≅ Spec Γ(S, A).

Stacks.RelativeSpec.relativeSpecFunctor_representableBy is the same tag in its functor-of-points form; this is the identification with the glued relative spectrum Stacks.AffineAlgebraEquivalence.relativeSpec.

It is an isomorphism of schemes; no compatibility with the structure morphism to S is claimed.

public noncomputable def relativeSpecIsoSpecSections [IsAffine S] :
    relativeSpec A ≅ Spec (A.right.obj.obj (op (⊤ : S.Opens)))

Stacks.RelativeSpec.relativeSpecFunctor_representableBy, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpecRepresentability/Basic.lean, line 496.

If the base is affine, the functor of relative-spectrum pairs associated to a quasi-coherent algebra is represented by the spectrum of the algebra's ring of global sections.

theorem relativeSpecFunctor_representableBy (s : RelativeSpecSituation.{u}) [IsAffine s.base] :
    Nonempty ((relativeSpecFunctor s).RepresentableBy
      (Spec (s.algebra.right.obj.obj (.op (⊤ : s.base.Opens)))))
Tag 01LU, a lemma

Tag 01LU in the Stacks Project.

Stacks.RelativeSpec.relativeSpecFunctor_isRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/Representability.lean, line 409.

The functor associated to a quasi-coherent algebra on a scheme is representable by a scheme.

theorem relativeSpecFunctor_isRepresentable : (relativeSpecFunctor s).IsRepresentable
Tag 01LV, a lemma

Tag 01LV in the Stacks Project.

Stacks.RelativeSpec.relativeSpecRepresentableBy, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/Representability.lean, line 374.

The glued relative spectrum represents the relative spectrum functor, with universal element the structure morphism together with the universal algebra map.

noncomputable def relativeSpecRepresentableBy :
    (relativeSpecFunctor s).RepresentableBy (gluedSpectrum s).scheme

Stacks.RelativeSpec.gluedSpectrumIso_hom_toBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/Representability.lean, line 432. The attribute's comment: “canonical comparison over the base”.

The canonical comparison between the glued relative spectrum and a scheme representing the relative spectrum functor is a morphism over the base, where the representing scheme carries the structure morphism of its universal element.

theorem gluedSpectrumIso_hom_toBase {X : Scheme.{u}}
    (h : (relativeSpecFunctor s).RepresentableBy X) :
    (gluedSpectrumIso s h).hom ≫ (h.homEquiv (𝟙 X)).1 = (gluedSpectrum s).toBase
Tag 01LW, a definition

Tag 01LW in the Stacks Project.

Stacks.RelativeSpec.relativeSpecRepresentableBy, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/Representability.lean, line 374. The attribute's comment: “the relative spectrum with its universal algebra map”.

The glued relative spectrum represents the relative spectrum functor, with universal element the structure morphism together with the universal algebra map.

noncomputable def relativeSpecRepresentableBy :
    (relativeSpecFunctor s).RepresentableBy (gluedSpectrum s).scheme
Tag 01LX, a lemma

Tag 01LX in the Stacks Project.

Stacks.AffineAlgebraEquivalence.isAffineOpen_preimage_relativeSpecToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineAlgebraEquivalence2/RelativeSpec.lean, line 137. The attribute's comment: “affine_inverse_image”. References: SGA 3 I (4.2), “Spec(A) affine over S”.

Stacks Project, Tag 01LX(1). The preimage of an affine open of the base in the relative spectrum is affine.

public theorem isAffineOpen_preimage_relativeSpecToBase (U : S.affineOpens) :
    IsAffineOpen (relativeSpecToBase A ⁻¹ᵁ (U : S.Opens))

Stacks.AffineAlgebraEquivalence.pushforwardAlgebraIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpecEssSurj/Basic.lean, line 296. The attribute's comment: “universal_map_iso”. References: SGA 3 I (4.2), “A ≅ π_*O_Spec(A)”.

Stacks Project, Tag 01LX(3). The isomorphism of sheaves of 𝒪_S-algebras (relativeSpecToBase A)_* 𝒪 ≅ A. Its inverse is the universal map A ⟶ (relativeSpecToBase A)_* 𝒪 of the relative spectrum, so this says that the universal map is an isomorphism; it is also the essential surjectivity of the pushforward functor.

public noncomputable def pushforwardAlgebraIso : pushforwardAlgebra (relativeSpecToBase A) ≅ A

Stacks.AffineAlgebraEquivalence.relativeSpecBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpecOpenRestriction/RelativeSpecBaseChange.lean, line 113. The attribute's comment: “part (2): Spec_S(A) ×_S T = Spec_T(g^*A) for an arbitrary morphism g : T → S”. References: EGA II (1.5.6); SGA 3 III (0.1.7); SGA 3 VIA (2.1.2), “more general”.

Stacks Project, Tag 01LX part (2). For a quasi-coherent sheaf of 𝒪_S-algebras A and an arbitrary morphism of schemes g : T ⟶ S, the fibre product \underline{Spec}_S(A) ×_S T is the relative spectrum over T of the base change g^*A: 

T ×_S \underline{Spec}_S(A) = \underline{Spec}_T(g^*A).
The base change g^*A is quasi-coherent by Stacks.AffineAlgebraEquivalence.isQuasicoherent_algebraPullback_obj, which is what makes the right-hand side meaningful.

public noncomputable def relativeSpecBaseChangeIso :
    (Over.pullback g).obj (Over.mk (relativeSpecToBase A)) ≅
      Over.mk (relativeSpecToBase ((algebraPullback g).obj A))
Tag 01LY, a lemma

Tag 01LY in the Stacks Project.

Stacks.RelativeSpec.AlgebraSheaf.isQuasicoherent_pushforwardAlgebra, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/CanonicalMorphism.lean, line 106. The attribute's comment: “quasi-coherence of the pushed-forward algebra”. References: EGA I (4.1.1), “more general”; EGA I (9.2.2), “special case”; EGA IV (11.10.3); EGA IV (21.12.1); EGA IV (3.1.10.2), “special case”; SGA 3 III (0.13), “special case”; SGA 3 VIB (11.0), “special case”.

For a quasi-compact and quasi-separated morphism of schemes f : X ⟶ S, the sheaf of 𝒪_S-algebras f_* 𝒪_X is quasi-coherent.

This is Tag 01LC for the structure sheaf of X: the 𝒪_S-module underlying f_* 𝒪_X is the direct image of the unit module over 𝒪_X.

instance AlgebraSheaf.isQuasicoherent_pushforwardAlgebra [QuasiCompact f] [QuasiSeparated f] :
    AlgebraSheaf.IsQuasicoherent (pushforwardAlgebra f)

Stacks.RelativeSpec.toRelativeSpec, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/CanonicalMorphism.lean, line 156. The attribute's comment: “canonical morphism”. References: EGA III (4.3.1).

The canonical morphism can : X ⟶ Spec_S(f_* 𝒪_X) from the source of a quasi-compact, quasi-separated morphism to the relative spectrum of the direct image of its structure sheaf. It is the morphism classified by the identity map of f_* 𝒪_X under the representing bijection of Tag 01LV.

noncomputable def toRelativeSpec : X ⟶ (gluedSpectrum (pushforwardSituation f)).scheme

Stacks.RelativeSpec.toRelativeSpec_toBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/CanonicalMorphism.lean, line 171. The attribute's comment: “morphism over the base”.

The canonical morphism to the relative spectrum of f_* 𝒪_X is a morphism of schemes over S.

theorem toRelativeSpec_toBase :
    toRelativeSpec f ≫ (gluedSpectrum (pushforwardSituation f)).toBase = f

Stacks.RelativeSpec.ι_toRelativeSpec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/CanonicalMorphism.lean, line 192. The attribute's comment: “identification on affine opens”.

Over an affine open U of the base, the canonical morphism to the relative spectrum of f_* 𝒪_X restricts on f⁻¹(U) to the canonical morphism f⁻¹(U) ⟶ Spec Γ(f⁻¹(U), 𝒪_X), followed by the chart of U.

theorem ι_toRelativeSpec (U : S.affineOpens) :
    (f ⁻¹ᵁ U.1).ι ≫ toRelativeSpec f =
      (f ⁻¹ᵁ U.1).toSpecΓ ≫ (gluedSpectrum (pushforwardSituation f)).chart U
Sources
LeanStacks.RelativeSpec.relativeSpecFunctor · relativeSpecFunctor · Stacks.RelativeSpec.algebraPullback_nonempty · Stacks.RelativeSpec.relativeSpecFunctorPullbackToOriginal_base · Stacks.RelativeSpec.relativeSpecFunctorPullbackToOriginal_algebra · Stacks.RelativeSpec.relativeSpecFunctor_pullback_iso_pullback · Stacks.RelativeSpec.relativeSpecFunctor_pullback_iso_pullback_fst · Stacks.RelativeSpec.relativeSpecFunctor_pullback_iso_pullback_snd

Section27.5 Affine n-space#

Section 27.5 of the Stacks Project, Tag 01LZ. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01M0, a definition

Tag 01M0 in the Stacks Project.

Stacks.AffineSpace.affineNSpace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/AffineSpace.lean, line 287. The attribute's comment: “affine n-space over S, the relative spectrum of the polynomial algebra O_S[T_1, ..., T_n], as a scheme over S”. References: EGA IV (5.5.5).

Affine n-space over a scheme. For a scheme S and an integer n ≥ 0, affine n-space 𝐀ⁿ_S = Spec_S(𝒪_S[T_1, …, T_n]) over S is the relative spectrum of the quasi-coherent sheaf of 𝒪_S-algebras 𝒪_S[T_1, …, T_n], as a scheme over S. For S = Spec R this is affine n-space 𝐀ⁿ_R over R.

Here 𝒪_S[T_1, …, T_n] is the sheaf associated to the presheaf U ↦ 𝒪_S(U)[T_1, …, T_n], whose sections over an affine open U are 𝒪_S(U)[T_1, …, T_n] (Stacks.AffineSpace.bijective_toSheafify_app), and the result is Mathlib's 𝔸(n; S) over S by Stacks.AffineSpace.affineSpaceIso.

abbrev affineNSpace (n : ℕ) : Over S
Sources
LeanStacks.AffineSpace.affineNSpace

Section27.6 Vector bundles#

Section 27.6 of the Stacks Project, Tag 01M1. 3 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01M2, a definition

Tag 01M2 in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.vectorBundle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/VectorBundleOfModule.lean, line 72. The attribute's comment: “the vector bundle V(E) = Spec_S(Sym(E)) associated to a quasi-coherent module”. References: EGA II (1.7.8); EGA IV (16.4.7); EGA IV (16.5.12), “more general”; EGA IV (18.5.2); SGA 3 I (4.6.3.1), “partial”; SGA 3 VIB (11.5); SGA 4½ Sommes trig (4.6), “partial”; SGA 6 VIII (5.2).

The vector bundle 𝐕(ℰ) = Spec_S(Sym(ℰ)) associated to a quasi-coherent 𝒪_S-module ℰ: the relative spectrum of the symmetric algebra of ℰ.

Following EGA II, Definition 1.7.8, ℰ is not assumed finite locally free.

def vectorBundle [E.IsQuasicoherent] : Scheme.{u}
Tag 062M, a definition

Tag 062M in the Stacks Project.

AlgebraicGeometry.VectorBundle, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/VectorBundle.lean, line 223. The attribute's comment: “vector bundles”.

A vector bundle over S: a cone whose direct-image algebra is generated in degree one in the strongest sense, namely that every canonical map Sym^n(ℰ_1) ⟶ ℰ_n is an isomorphism.

structure VectorBundle (S : Scheme.{u}) extends AbstractCone S

AlgebraicGeometry.VectorBundle.category, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/VectorBundle.lean, line 236. The attribute's comment: “morphisms of vector bundles”.

Vector bundles over a fixed base form a category, with the morphisms of the underlying cones as its morphisms.

instance category : Category (VectorBundle S)
Tag 062N, a lemma

Tag 062N in the Stacks Project.

AlgebraicGeometry.VectorBundle.degreeOneEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/VectorBundleEssSurj.lean, line 422. The attribute's comment: “the anti-equivalence between vector bundles over S and quasi-coherent O_S-modules”.

The category of vector bundles over a scheme S is anti-equivalent to the category of quasi-coherent 𝒪_S-modules.

The anti-equivalence is recorded in the contravariant form (VectorBundle S)ᵒᵖ ≌ QCoh(𝒪_S), the functor being V ↦ (π_* 𝒪_V)_1 and its quasi-inverse ℰ ↦ 𝐕(ℰ) = Spec_S(Sym(ℰ)). Of the two standard forms of an anti-equivalence this is the one with the opposite taken on the geometric side, which is the side the source's two functors are contravariant on, and it is the form of Tag 01SA's (AffineOver S)ᵒᵖ ≌ QuasicoherentAlgebra S that this one restricts.

def degreeOneEquivalence (S : Scheme.{u}) :
    (VectorBundle S)ᵒᵖ ≌ Scheme.QuasicoherentModules S
Sources
LeanAlgebraicGeometry.Scheme.Modules.vectorBundle · AlgebraicGeometry.VectorBundle · AlgebraicGeometry.VectorBundle.category · AlgebraicGeometry.VectorBundle.degreeOneEquivalence

Section27.7 Cones#

Section 27.7 of the Stacks Project, Tag 062P. 2 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 062Q, a definition

Tag 062Q in the Stacks Project.

AlgebraicGeometry.GradedConeAlgebra.cone, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ConeOfGradedAlgebra.lean, line 153. References: EGA II (8.3.1), “affine cone C=Spec(S)”; EGA II (8.6.1), “partial”; SGA 7 XV (2.1.1), “more general”.

The cone, or affine cone, associated to a quasi-coherent graded 𝒪_S-algebra 𝒜 whose degree-zero part is 𝒪_S: the relative spectrum C(𝒜) = Spec_S(𝒜).

public noncomputable def cone : Scheme.{u}
Tag 062R, a definition

Tag 062R in the Stacks Project.

AlgebraicGeometry.AbstractCone, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/Cone.lean, line 65. The attribute's comment: “cones”.

A cone over S: an affine morphism whose direct-image algebra is nonnegatively graded and has degree-zero part 𝒪_S.

public structure AbstractCone (S : Scheme.{u})

AlgebraicGeometry.AbstractCone.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/Cone.lean, line 117. The attribute's comment: “morphisms of cones”.

A morphism of cones. The map on direct images is the pullback on functions induced by the displayed morphism of total spaces.

public structure Hom {S : Scheme.{u}} (X Y : AbstractCone S)
Sources
LeanAlgebraicGeometry.GradedConeAlgebra.cone · AlgebraicGeometry.AbstractCone · AlgebraicGeometry.AbstractCone.Hom

Section27.8 Proj of a graded ring#

Section 27.8 of the Stacks Project, Tag 01M3. 13 tags here are carried by 27 declarations of the repository (all in StacksFrontier) and 5 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01M4, a lemma

Tag 01M4 in the Stacks Project.

Stacks.ProjStandardOpenStatement.tag01M4, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjStandardOpenStatement.lean, line 89. The attribute's comment: “the ten assertions of the tag in one statement: part (1)(a)-(h) for a standard open D+(g) contained in D+(f), part (2) the finite refinement of an open covering of D+(f) by standard opens, part (3) the unit-ideal criterion”.

[Stacks, Tag 01M4]. For a graded ring A and f ∈ 𝒜 d homogeneous of positive degree:

  • part (1), for homogeneous g of positive degree with D₊(g) ⊆ D₊(f), the eight assertions (a)–(h) of the source, the module assertions (g) and (h) quantified over the graded module inside their own conjuncts;
  • part (2), the finite refinement of an open covering of D₊(f) by standard opens;
  • part (3), the unit-ideal criterion for D₊(f) ⊆ ⋃ D₊(gᵢ).
theorem tag01M4 (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {d : ℕ}
    (hfd : f ∈ 𝒜 d) (hd : 0 < d) :
    -- part (1)
    (∀ (g : A) (e : ℕ) (hge : g ∈ 𝒜 e) (he : 0 < e)
        (hfg : ProjectiveSpectrum.basicOpen 𝒜 g ≤ ProjectiveSpectrum.basicOpen 𝒜 f),
        -- (a) `f` is invertible in `A[1/g]`, and `f ^ deg g / g ^ deg f` is invertible in `A₍g₎`
        (IsUnit (algebraMap A (Localization.Away g) f) ∧
          IsUnit (Away.isLocalizationElem hge hfd)) ∧
        -- (b) a positive power of `g` is a homogeneous multiple of `f`
        (∃ k : ℕ, 1 ≤ k ∧ ∃ a : A, SetLike.IsHomogeneousElem 𝒜 a ∧ g ^ k = a * f) ∧
        -- (c) the canonical, and only, `A`-algebra map `A[1/f] → A[1/g]`
        ((∀ x : A,
            ProjectiveSpectrum.localizedRingMap 𝒜 f g ⟨d, hd, hfd⟩ ⟨e, he, hge⟩ hfg
                (algebraMap A (Localization.Away f) x) = algebraMap A (Localization.Away g) x) ∧
          Subsingleton (Localization.Away f →ₐ[A] Localization.Away g)) ∧
        -- (d) the canonical `𝒜 0`-algebra map `A₍f₎ → A₍g₎`, compatible with the map of (c),
        -- and the only `𝒜 0`-algebra map compatible with it
        ((∀ x : Away 𝒜 f,
            (ProjectiveSpectrum.degreeZeroRingMap 𝒜 f g ⟨d, hd, hfd⟩ ⟨e, he, hge⟩ hfg x).val =
              ProjectiveSpectrum.localizedRingMap 𝒜 f g ⟨d, hd, hfd⟩ ⟨e, he, hge⟩ hfg x.val) ∧
          ∀ ψ : Away 𝒜 f →ₐ[𝒜 0] Away 𝒜 g,
            (∀ x : Away 𝒜 f, (ψ x).val =
              ProjectiveSpectrum.localizedRingMap 𝒜 f g ⟨d, hd, hfd⟩ ⟨e, he, hge⟩ hfg x.val) →
            ψ = ProjectiveSpectrum.degreeZeroRingMap 𝒜 f g ⟨d, hd, hfd⟩ ⟨e, he, hge⟩ hfg) ∧
        -- (e) that map exhibits `A₍g₎` as `A₍f₎` localized at `g ^ deg f / f ^ deg g`
        (letI : Algebra (Away 𝒜 f) (Away 𝒜 g) :=
          (ProjectiveSpectrum.degreeZeroRingMap 𝒜 f g
            ⟨d, hd, hfd⟩ ⟨e, he, hge⟩ hfg).toRingHom.toAlgebra
         IsLocalization.Away
           (Away.mk 𝒜 hfd e (g ^ d) (by simpa [mul_comm] using SetLike.pow_mem_graded d hge))
           (Away 𝒜 g)) ∧
        -- (f) the commutative diagram of topological spaces, with horizontal arrows
        -- homeomorphisms and vertical arrows open immersions
        (letI := gradedRingTwistAway 𝒜 hfd
         letI := gradedRingTwistAway 𝒜 hge
         IsHomeomorph (gradedPrimeToBasicOpen 𝒜 hge he) ∧
           IsHomeomorph (gradedPrimesAwayToSpec 𝒜 hge) ∧
           IsHomeomorph (gradedPrimeToBasicOpen 𝒜 hfd hd) ∧
           IsHomeomorph (gradedPrimesAwayToSpec 𝒜 hfd) ∧
           Topology.IsOpenEmbedding (basicOpenInclusion 𝒜 hfg) ∧
           Topology.IsOpenEmbedding
             (gradedPrimesVertical 𝒜 hfd hge ⟨d, hd, hfd⟩ ⟨e, he, hge⟩ hfg) ∧
           Topology.IsOpenEmbedding (specDegreeZeroVertical 𝒜 f g d e hd he hfd hge hfg) ∧
           (∀ q : gradedPrimes (twistAway 𝒜 g e),
             basicOpenInclusion 𝒜 hfg (gradedPrimeToBasicOpen 𝒜 hge he q) =
               gradedPrimeToBasicOpen 𝒜 hfd hd
                 (gradedPrimesVertical 𝒜 hfd hge ⟨d, hd, hfd⟩ ⟨e, he, hge⟩ hfg q)) ∧
           (∀ q : gradedPrimes (twistAway 𝒜 g e),
             specDegreeZeroVertical 𝒜 f g d e hd he hfd hge hfg
                 (gradedPrimesAwayToSpec 𝒜 hge q) =
               gradedPrimesAwayToSpec 𝒜 hfd
                 (gradedPrimesVertical 𝒜 hfd hge ⟨d, hd, hfd⟩ ⟨e, he, hge⟩ hfg q))) ∧
        -- (g) and (h), for an arbitrary graded `A`-module `M`
        (∀ {M : Type w} {τ : Type t} [AddCommGroup M] [Module A M] [SetLike τ M]
            [AddSubgroupClass τ M] (𝒨 : ℤ → τ) [DirectSum.Decomposition 𝒨]
            [SetLike.GradedSMul 𝒜 𝒨],
          -- (g) compatible maps `M_f → M_g` and `M₍f₎ → M₍g₎`, induced by the identity of `M`,
          -- each the only such map
          ((∀ m : M,
              (ProjectiveSpectrum.moduleRestrictionMaps 𝒜 𝒨 f g
                    ⟨d, hd, hfd⟩ ⟨e, he, hge⟩ hfg).localizedMap
                  (LocalizedModule.mkLinearMap (Submonoid.powers f) M m) =
                LocalizedModule.mkLinearMap (Submonoid.powers g) M m) ∧
            (∀ x : GradedModuleDegreeZeroLocalization 𝒜 𝒨 f,
              (((ProjectiveSpectrum.moduleRestrictionMaps 𝒜 𝒨 f g
                      ⟨d, hd, hfd⟩ ⟨e, he, hge⟩ hfg).degreeZeroMap x :
                    GradedModuleDegreeZeroLocalization 𝒜 𝒨 g) :
                  LocalizedModule.Away (R := A) g M) =
                (ProjectiveSpectrum.moduleRestrictionMaps 𝒜 𝒨 f g
                  ⟨d, hd, hfd⟩ ⟨e, he, hge⟩ hfg).localizedMap x) ∧
            (∀ L :
                letI := Module.compHom (R := Localization.Away g) (S := Localization.Away f)
                  (LocalizedModule.Away (R := A) g M)
                  (ProjectiveSpectrum.localizedRingMap 𝒜 f g
                    ⟨d, hd, hfd⟩ ⟨e, he, hge⟩ hfg).toRingHom
                LocalizedModule.Away (R := A) f M →ₗ[Localization.Away f]
                  LocalizedModule.Away (R := A) g M,
              (∀ m : M, L (LocalizedModule.mkLinearMap (Submonoid.powers f) M m) =
                LocalizedModule.mkLinearMap (Submonoid.powers g) M m) →
              L = (ProjectiveSpectrum.moduleRestrictionMaps 𝒜 𝒨 f g
                ⟨d, hd, hfd⟩ ⟨e, he, hge⟩ hfg).localizedMap) ∧
            (∀ N :
                letI := Module.compHom (R := Localization.Away f)
                  (LocalizedModule.Away (R := A) f M)
                  (algebraMap (Away 𝒜 f) (Localization.Away f))
                letI := Module.compHom (R := Localization.Away g)
                  (LocalizedModule.Away (R := A) g M)
                  (algebraMap (Away 𝒜 g) (Localization.Away g))
                letI := Module.compHom (R := Away 𝒜 g)
                  (GradedModuleDegreeZeroLocalization 𝒜 𝒨 g)
                  (ProjectiveSpectrum.degreeZeroRingMap 𝒜 f g
                    ⟨d, hd, hfd⟩ ⟨e, he, hge⟩ hfg).toRingHom
                GradedModuleDegreeZeroLocalization 𝒜 𝒨 f →ₗ[Away 𝒜 f]
                  GradedModuleDegreeZeroLocalization 𝒜 𝒨 g,
              (∀ x : GradedModuleDegreeZeroLocalization 𝒜 𝒨 f,
                (N x : LocalizedModule.Away (R := A) g M) =
                  (ProjectiveSpectrum.moduleRestrictionMaps 𝒜 𝒨 f g
                    ⟨d, hd, hfd⟩ ⟨e, he, hge⟩ hfg).localizedMap x) →
              N = (ProjectiveSpectrum.moduleRestrictionMaps 𝒜 𝒨 f g
                ⟨d, hd, hfd⟩ ⟨e, he, hge⟩ hfg).degreeZeroMap)) ∧
          -- (h) `M₍g₎` is `M₍f₎` localized at `g ^ deg f / f ^ deg g`
          (letI : Algebra (Away 𝒜 f) (Away 𝒜 g) :=
             (ProjectiveSpectrum.degreeZeroRingMap 𝒜 f g
               ⟨d, hd, hfd⟩ ⟨e, he, hge⟩ hfg).toRingHom.toAlgebra
           letI := Module.compHom (R := Away 𝒜 g)
             (GradedModuleDegreeZeroLocalization 𝒜 𝒨 g)
             (ProjectiveSpectrum.degreeZeroRingMap 𝒜 f g
               ⟨d, hd, hfd⟩ ⟨e, he, hge⟩ hfg).toRingHom
           IsLocalizedModule
             (Submonoid.powers
               (Away.mk 𝒜 hfd e (g ^ d) (by simpa [mul_comm] using SetLike.pow_mem_graded d hge)))
             (ProjectiveSpectrum.moduleRestrictionMaps 𝒜 𝒨 f g
               ⟨d, hd, hfd⟩ ⟨e, he, hge⟩ hfg).degreeZeroMap))) ∧
    -- part (2)
    (∀ {ι : Type s} (U : ι → TopologicalSpace.Opens (ProjectiveSpectrum 𝒜)),
        ProjectiveSpectrum.basicOpen 𝒜 f ≤ ⨆ i, U i →
        ∃ (n : ℕ) (g : Fin n → A) (e : Fin n → ℕ),
          (∀ i, 0 < e i ∧ g i ∈ 𝒜 (e i)) ∧
          ProjectiveSpectrum.basicOpen 𝒜 f = ⨆ i, ProjectiveSpectrum.basicOpen 𝒜 (g i) ∧
          ∀ i, ∃ j, ProjectiveSpectrum.basicOpen 𝒜 (g i) ≤ U j) ∧
    -- part (3)
    (∀ {ι : Type s'} (g : ι → A) (e : ι → ℕ) (hg : ∀ i, g i ∈ 𝒜 (e i)) (_he : ∀ i, 0 < e i),
        AlgebraicGeometry.Proj.basicOpen 𝒜 f ≤ ⨆ i, AlgebraicGeometry.Proj.basicOpen 𝒜 (g i) ↔
          Ideal.span (Set.range fun i => Away.isLocalizationElem hfd (hg i)) = ⊤)
Tag 01M5, a definition

Tag 01M5 in the Stacks Project.

ProjectiveSpectrum.IsStandardOpenCover, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjStandardOpenCover.lean, line 61.

A finite family of positive-degree homogeneous elements gᵢ gives a standard open covering of the projective standard open D₊(f) when their standard opens have union exactly D₊(f).

public abbrev IsStandardOpenCover {A : Type u} {σ : Type v}
    [CommRing A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜]
    (f : A) {n : ℕ} (g : Fin n → A) : Prop
Tag 01M6, a definition

Tag 01M6 in the Stacks Project.

AlgebraicGeometry.ProjectiveSpectrum.Proj.associatedModuleSheafStandardOpenEquiv_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistLocalRestriction.lean, line 67. The attribute's comment: “part (3), the standard-open identification intertwines the restriction map of the associated sheaf with the degree-zero restriction map of Tag 01M4”.

The standard-open identification Γ(D₊(f), M̃) = M₍f₎ intertwines the restriction map of M̃ with the canonical degree-zero restriction map M₍f₎ → M₍g₎, for any two positive-degree homogeneous elements with D₊(g) ⊆ D₊(f).

theorem associatedModuleSheafStandardOpenEquiv_restrict (f g : S) {d e : ℕ}
    (hf : f ∈ 𝒜 d) (hd : 0 < d) (hg : g ∈ 𝒜 e) (he : 0 < e)
    (hfg : ProjectiveSpectrum.basicOpen 𝒜 g ≤ ProjectiveSpectrum.basicOpen 𝒜 f)
    (s : (associatedModuleSheaf 𝒜 𝒨).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
    associatedModuleSheafStandardOpenEquiv 𝒜 𝒨 hg he
        ((associatedModuleSheaf 𝒜 𝒨).val.map (homOfLE hfg).op s) =
      (ProjectiveSpectrum.moduleRestrictionMaps 𝒜 𝒨 f g
          ⟨d, hd, hf⟩ ⟨e, he, hg⟩ hfg).degreeZeroMap
        (associatedModuleSheafStandardOpenEquiv 𝒜 𝒨 hf hd s)

AlgebraicGeometry.ProjectiveSpectrum.Proj.coe_associatedModuleSheafStandardOpenEquiv_smul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjStandardOpenScalars.lean, line 82. The attribute's comment: “part (3), the scalar action in the standard-open identification, written out on the underlying elements of the localization”.

The standard-open identification Γ(D₊(f), M̃) = M₍f₎ is linear for the action of Γ(P, D₊(f)) read through AlgebraicGeometry.Proj.awayToSection, the action on the target being multiplication by the fraction inside M_f.

theorem coe_associatedModuleSheafStandardOpenEquiv_smul {f : S} {d : ℕ} (hf : f ∈ 𝒜 d)
    (hd : 0 < d) (r : HomogeneousLocalization.Away 𝒜 f)
    (s : (associatedModuleSheaf 𝒜 𝒨).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
    ((associatedModuleSheafStandardOpenEquiv 𝒜 𝒨 hf hd
          ((ProjectiveSpectrum.Proj.awayToSection 𝒜 f).hom r • s) :
        LocalizedModule.Away f M)) =
      HomogeneousLocalization.val r •
        ((associatedModuleSheafStandardOpenEquiv 𝒜 𝒨 hf hd s : LocalizedModule.Away f M))

AlgebraicGeometry.ProjectiveSpectrum.Proj.associatedModuleSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjStructureSheaf.lean, line 221. The attribute's comment: “part (3), the sheaf associated to a graded module”. References: SGA 6 VI (2.3.2), “affine base”.

The actual sheaf associated to a graded module. Its sections are locally homogeneous fractions of degree zero, and its restrictions are restrictions of dependent functions.

public noncomputable def associatedModuleSheaf :
    SheafOfModules.{max u v}
      ((sheafCompose (Opens.grothendieckTopology (ProjectiveSpectrum.top 𝒜))
        (forget₂ CommRingCat.{u} RingCat.{u})).obj
        (ProjectiveSpectrum.Proj.structureSheaf 𝒜))

AlgebraicGeometry.ProjectiveSpectrum.Proj.degreeZeroToSection_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjStructureSheaf.lean, line 710. The attribute's comment: “part (3), injectivity of the standard-open comparison”.

Distinct degree-zero fractions give distinct sections on a positive-degree standard open.

public theorem degreeZeroToSection_injective {f : S} {d : ℕ}
    (hf : f ∈ 𝒜 d) (hd : 0 < d) :
    Function.Injective (degreeZeroToSection 𝒜 𝒨 f)

AlgebraicGeometry.ProjectiveSpectrum.Proj.degreeZeroToSection_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjStructureSheaf.lean, line 729. The attribute's comment: “part (3), surjectivity of the standard-open comparison”.

Every section on a positive-degree standard open comes from a degree-zero fraction.

public theorem degreeZeroToSection_surjective {f : S} {d : ℕ}
    (hf : f ∈ 𝒜 d) (hd : 0 < d) :
    Function.Surjective (degreeZeroToSection 𝒜 𝒨 f)

AlgebraicGeometry.ProjectiveSpectrum.Proj.associatedModuleSheafStandardOpenEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjStructureSheaf.lean, line 937. The attribute's comment: “part (3), canonical linear identification on standard opens”.

The canonical linear identification of sections on D₊(f) with M_(f). Its inverse is evaluation of a degree-zero fraction in every homogeneous-prime fiber.

public noncomputable def associatedModuleSheafStandardOpenEquiv {f : S} {d : ℕ}
    (hf : f ∈ 𝒜 d) (hd : 0 < d) :
    (associatedModuleSheaf 𝒜 𝒨).val.obj (.op (ProjectiveSpectrum.basicOpen 𝒜 f))
      ≃ₗ[HomogeneousLocalization.Away 𝒜 f]
        GradedModuleDegreeZeroLocalization 𝒜 𝒨 f

Declarations registered for the tag:

Tag 01M7, a lemma

Tag 01M7 in the Stacks Project.

Stacks.AlgebraicGeometry.ProjSheafFunctoriality.shortExact_map_associatedModuleSheafFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjSheafFunctoriality/Exact.lean, line 167. The attribute's comment: “the functor M ↦ M~ is exact, in its categorical form: a short exact sequence of graded S-modules goes to a short exact sequence of sheaves of modules on Proj S”.

Stacks 01M7: the functor M ↦ M̃ is exact, in the form that it carries a short exact sequence of graded S-modules to a short exact sequence of sheaves of 𝒪_{Proj 𝒮}-modules.

Short exactness of sheaves of modules is short exactness on every stalk, the stalk of M̃ at a homogeneous prime 𝔭 is the degree-zero part of the localization of M at 𝔭, and that operation is exact.

public theorem shortExact_map_associatedModuleSheafFunctor
    (T : ShortComplex (GradedModuleCat.{u, u, w} 𝒮)) (hT : T.ShortExact) :
    (T.map (associatedModuleSheafFunctor 𝒮)).ShortExact

Stacks.AlgebraicGeometry.ProjSheafFunctoriality.sections_restriction_stalks_functorial_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjSheafFunctoriality/Statement.lean, line 115. The attribute's comment: “the tag's assertions in one statement: the sections of the structure sheaf and of the associated sheaf over a positive-degree standard open are the degree-zero localizations S₍f₎ and M₍f₎, the restriction maps between two standard opens are the canonical maps S₍f₎ → S₍g₎ and M₍f₎ → M₍g₎ of degree-zero localizations, the stalks at a homogeneous prime are S₍𝔭₎ and M₍𝔭₎, there are canonical maps S₀ → Γ(Proj S, 𝒪) and M₀ → Γ(Proj S, M̃) fitting both descriptions, every one of these identifications is natural in the graded module, and M ↦ M̃ is an exact functor”. References: EGA II (2.5.5), “special case”.

[Stacks, Tag 01M7]. Let S be a graded ring, let M be a graded S-module and let M̃ be the sheaf of 𝒪_{Proj(S)}-modules associated to M. Then all of the following hold.

The conjuncts are, in order:

  1. For f homogeneous of positive degree, Γ(D₊(f), 𝒪_{Proj(S)}) is S₍f₎.
  2. For f homogeneous of positive degree, Γ(D₊(f), M̃) is M₍f₎ as an S₍f₎-module.
  3. For D₊(g) ⊆ D₊(f) with f, g homogeneous of positive degree, the restriction map of 𝒪_{Proj(S)} is the map S₍f₎ → S₍g₎ of Tag 01M4, and the restriction map of M̃ is the map M₍f₎ → M₍g₎ of Tag 01M4.
  4. At a point x of Proj(S), with homogeneous prime 𝔭, the stalk 𝒪_{Proj(S), x} is S₍𝔭₎.
  5. At the same point, the stalk (M̃)_x is M₍𝔭₎ as an S₍𝔭₎-module.
  6. There is a canonical ring map S₀ → Γ(Proj(S), 𝒪_{Proj(S)}) and a canonical S₀-module map M₀ → Γ(Proj(S), M̃), each compatible with the description of the sections over a positive-degree standard open and with the description of the stalks: the four equations say that the restriction of the global section attached to a, resp. to m, is a / 1, resp. m / f ^ 0, and that its germ at x is a / 1, resp. m / 1.
  7. The identifications are functorial in the graded module. The identity map of M induces the identity morphism of M̃; and for every graded S-module N and degree-preserving φ : M →ₗ[S] N, with M̃ ⟶ Ñ the induced morphism: composition with a degree-preserving map out of N is respected, and the identifications of (2), (5) and (6) are natural — over a positive-degree standard open the induced morphism is the degree-zero part of the localized map M_f → N_f, on the stalk at x it is the localization of φ at 𝔭, and it takes the global section attached to m to the global section attached to φ m.
  8. In particular M ↦ M̃ is an exact functor: a short exact sequence of graded S-modules with degree-preserving maps goes to a short exact sequence of sheaves of 𝒪_{Proj(S)}-modules.

Every conjunct is the separate statement that proves it; the separate registrations of the tag are on those.

theorem sections_restriction_stalks_functorial_exact :
    (∀ (f : S) (d : ℕ), f ∈ 𝒮 d → 0 < d →
        Nonempty (CommRingCat.of (HomogeneousLocalization.Away 𝒮 f) ≅
          (AlgebraicGeometry.Proj 𝒮).presheaf.obj (op (Proj.basicOpen 𝒮 f)))) ∧
      (∀ (f : S) (d : ℕ), f ∈ 𝒮 d → 0 < d →
        Nonempty ((ProjectiveSpectrum.Proj.associatedModuleSheaf 𝒮 𝒨).val.obj
            (op (ProjectiveSpectrum.basicOpen 𝒮 f)) ≃ₗ[HomogeneousLocalization.Away 𝒮 f]
          GradedModuleDegreeZeroLocalization 𝒮 𝒨 f)) ∧
      (∀ (f g : S) (d e : ℕ) (hf : f ∈ 𝒮 d) (hd : 0 < d) (hg : g ∈ 𝒮 e) (he : 0 < e)
          (hfg : ProjectiveSpectrum.basicOpen 𝒮 g ≤ ProjectiveSpectrum.basicOpen 𝒮 f),
        CommRingCat.ofHom (ProjectiveSpectrum.degreeZeroRingMap 𝒮 f g
              ⟨d, hd, hf⟩ ⟨e, he, hg⟩ hfg).toRingHom ≫
            (Proj.basicOpenIsoAway 𝒮 g hg he).hom =
          (Proj.basicOpenIsoAway 𝒮 f hf hd).hom ≫
            (AlgebraicGeometry.Proj 𝒮).presheaf.map (homOfLE hfg).op) ∧
      (∀ (f g : S) (hf : ∃ d : ℕ, 0 < d ∧ f ∈ 𝒮 d) (hg : ∃ d : ℕ, 0 < d ∧ g ∈ 𝒮 d)
          (hfg : ProjectiveSpectrum.basicOpen 𝒮 g ≤ ProjectiveSpectrum.basicOpen 𝒮 f)
          (a : GradedModuleDegreeZeroLocalization 𝒮 𝒨 f),
        (ProjectiveSpectrum.Proj.associatedModuleSheaf 𝒮 𝒨).val.map (homOfLE hfg).op
            (ProjectiveSpectrum.Proj.degreeZeroToSection 𝒮 𝒨 f a) =
          ProjectiveSpectrum.Proj.degreeZeroToSection 𝒮 𝒨 g
            ((ProjectiveSpectrum.moduleRestrictionMaps 𝒮 𝒨 f g hf hg hfg).degreeZeroMap a)) ∧
      (∀ x : ProjectiveSpectrum.top 𝒮,
        Nonempty ((ProjectiveSpectrum.Proj.structureSheaf 𝒮).presheaf.stalk x ≃+*
          HomogeneousLocalization.AtPrime 𝒮 x.asHomogeneousIdeal.toIdeal)) ∧
      (∀ x : ProjectiveSpectrum.top 𝒮,
        Nonempty
          (letI : Module ((ProjectiveSpectrum.Proj.structureSheaf 𝒮).presheaf.stalk x)
              (ProjStalkGlobalSections.degreeZeroModuleAt 𝒮 𝒨 x) :=
            Module.compHom _ (Proj.stalkIso' 𝒮 x).toRingHom
          ProjStalkGlobalSections.associatedModuleSheafStalk 𝒮 𝒨 x ≃ₗ[
              (ProjectiveSpectrum.Proj.structureSheaf 𝒮).presheaf.stalk x]
            ProjStalkGlobalSections.degreeZeroModuleAt 𝒮 𝒨 x)) ∧
      Nonempty (𝒮 0 →+* (ProjectiveSpectrum.Proj.structureSheaf 𝒮).1.obj (op ⊤)) ∧
      (∀ (f : S) (a : 𝒮 0),
        (ProjectiveSpectrum.Proj.structureSheaf 𝒮).1.map (homOfLE le_top).op
            (ProjStalkGlobalSections.degreeZeroRingToGlobalSections 𝒮 a) =
          (ProjectiveSpectrum.Proj.awayToSection 𝒮 f).hom
            (HomogeneousLocalization.fromZeroRingHom 𝒮 (Submonoid.powers f) a)) ∧
      (∀ (x : ProjectiveSpectrum.top 𝒮) (a : 𝒮 0),
        Proj.stalkIso' 𝒮 x ((ProjectiveSpectrum.Proj.structureSheaf 𝒮).presheaf.germ ⊤ x trivial
            (ProjStalkGlobalSections.degreeZeroRingToGlobalSections 𝒮 a)) =
          HomogeneousLocalization.fromZeroRingHom 𝒮 x.asHomogeneousIdeal.toIdeal.primeCompl a) ∧
      Nonempty
        (letI : Module (𝒮 0)
            ((ProjectiveSpectrum.Proj.associatedModuleSheaf 𝒮 𝒨).val.obj (op ⊤)) :=
          Module.compHom _ (ProjStalkGlobalSections.degreeZeroRingToGlobalSections 𝒮)
        𝒨 0 →ₗ[𝒮 0] (ProjectiveSpectrum.Proj.associatedModuleSheaf 𝒮 𝒨).val.obj (op ⊤)) ∧
      (∀ (f : S) (d : ℕ) (hf : f ∈ 𝒮 d) (hd : 0 < d) (m : 𝒨 0),
        ProjectiveSpectrum.Proj.associatedModuleSheafStandardOpenEquiv 𝒮 𝒨 hf hd
            ((ProjectiveSpectrum.Proj.associatedModuleSheaf 𝒮 𝒨).val.map (homOfLE le_top).op
              (ProjStalkGlobalSections.degreeZeroToGlobalSections 𝒮 𝒨 m)) =
          ProjectiveSpectrum.Proj.degreeZeroFraction 𝒮 𝒨 hf 0 m.1 (mem_zero_nsmul 𝒨 d m)) ∧
      (∀ (x : ProjectiveSpectrum.top 𝒮) (m : 𝒨 0),
        ((ProjStalkGlobalSections.associatedModuleSheafStalkEquiv 𝒮 𝒨 x
              (ProjStalkGlobalSections.associatedModuleSheafGerm 𝒮 𝒨 x ⊤ trivial
                (ProjStalkGlobalSections.degreeZeroToGlobalSections 𝒮 𝒨 m)) :
            ProjStalkGlobalSections.degreeZeroModuleAt 𝒮 𝒨 x) :
              ProjectiveSpectrum.Proj.ModuleFiber (M := M) 𝒮 x) =
          LocalizedModule.mk m.1 (1 : x.asHomogeneousIdeal.toIdeal.primeCompl)) ∧
      (associatedModuleSheafMap 𝒮 𝒨 𝒨 (LinearMap.id : M →ₗ[S] M) (fun _ _ hm => hm) = 𝟙 _) ∧
      (∀ (N : Type u) [AddCommGroup N] [Module S N] {υ : Type t'} [SetLike υ N]
          [AddSubgroupClass υ N] (𝒩 : ℤ → υ) [Decomposition 𝒩] [SetLike.GradedSMul 𝒮 𝒩]
          (φ : M →ₗ[S] N) (hφ : ∀ i (m : M), m ∈ 𝒨 i → φ m ∈ 𝒩 i),
        (∀ (P : Type u) [AddCommGroup P] [Module S P] {ρ : Type t''} [SetLike ρ P]
              [AddSubgroupClass ρ P] (𝒬 : ℤ → ρ) [Decomposition 𝒬] [SetLike.GradedSMul 𝒮 𝒬]
              (ψ : N →ₗ[S] P) (hψ : ∀ i (n : N), n ∈ 𝒩 i → ψ n ∈ 𝒬 i),
            associatedModuleSheafMap 𝒮 𝒨 𝒬 (ψ.comp φ) (fun i m hm => hψ i (φ m) (hφ i m hm)) =
              associatedModuleSheafMap 𝒮 𝒨 𝒩 φ hφ ≫ associatedModuleSheafMap 𝒮 𝒩 𝒬 ψ hψ) ∧
          (∀ (f : S) (d : ℕ) (hf : f ∈ 𝒮 d) (hd : 0 < d)
              (s : (ProjectiveSpectrum.Proj.associatedModuleSheaf 𝒮 𝒨).val.obj
                (op (ProjectiveSpectrum.basicOpen 𝒮 f))),
            ((ProjectiveSpectrum.Proj.associatedModuleSheafStandardOpenEquiv 𝒮 𝒩 hf hd
                  ((associatedModuleSheafMap 𝒮 𝒨 𝒩 φ hφ).val.app _ s) :
                GradedModuleDegreeZeroLocalization 𝒮 𝒩 f) :
                  LocalizedModule.Away (R := S) f N) =
              LocalizedModule.map (Submonoid.powers f) φ
                (ProjectiveSpectrum.Proj.associatedModuleSheafStandardOpenEquiv 𝒮 𝒨 hf hd s :
                  GradedModuleDegreeZeroLocalization 𝒮 𝒨 f)) ∧
          (∀ (x : ProjectiveSpectrum.top 𝒮)
              (s : ProjStalkGlobalSections.associatedModuleSheafStalk 𝒮 𝒨 x),
            ((ProjStalkGlobalSections.associatedModuleSheafStalkEquiv 𝒮 𝒩 x
                  (colim.map (Functor.whiskerLeft (OpenNhds.inclusion x).op
                    ((PresheafOfModules.toPresheaf _).map
                      (associatedModuleSheafMap 𝒮 𝒨 𝒩 φ hφ).val)) s) :
                ProjStalkGlobalSections.degreeZeroModuleAt 𝒮 𝒩 x) :
                  ProjectiveSpectrum.Proj.ModuleFiber (M := N) 𝒮 x) =
              LocalizedModule.map x.asHomogeneousIdeal.toIdeal.primeCompl φ
                (ProjStalkGlobalSections.associatedModuleSheafStalkEquiv 𝒮 𝒨 x s :
                  ProjStalkGlobalSections.degreeZeroModuleAt 𝒮 𝒨 x)) ∧
          (∀ m : 𝒨 0,
            (associatedModuleSheafMap 𝒮 𝒨 𝒩 φ hφ).val.app (op ⊤)
                (ProjStalkGlobalSections.degreeZeroToGlobalSections 𝒮 𝒨 m) =
              ProjStalkGlobalSections.degreeZeroToGlobalSections 𝒮 𝒩
                ⟨φ m.1, hφ 0 m.1 m.2⟩)) ∧
      (∀ {X Y Z : GradedModuleCat.{u, u, w} 𝒮} (α : X ⟶ Y) (β : Y ⟶ Z),
        Function.Injective α.toLinearMap → Function.Surjective β.toLinearMap →
        ∀ hexact : Function.Exact α.toLinearMap β.toLinearMap,
          (ShortComplex.mk ((associatedModuleSheafFunctor 𝒮).map α)
            ((associatedModuleSheafFunctor 𝒮).map β)
            (associatedModuleSheafFunctor_map_comp_eq_zero α β
              fun m => (hexact (α.toLinearMap m)).mpr ⟨m, rfl⟩)).ShortExact)
Tag 01MA, a lemma

Tag 01MA in the Stacks Project.

AlgebraicGeometry.Proj.exists_homogeneous_awayι_preimage_basicOpen_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjBasicOpen.lean, line 360.

Stacks Project, Tag 01MA. Let f be a homogeneous element of positive degree m in a graded ring A, and let g be an element of the degree-zero localization A₍f₎, so that D(g) is a standard open of Spec A₍f₎. Then there is a homogeneous element h of positive degree n • m such that g = h / f ^ n, such that D₊(h) ⊆ D₊(f), and such that D(g) and D₊(h) correspond under the open immersion Spec A₍f₎ ⟶ Proj A identifying Spec A₍f₎ with D₊(f): D(g) is the preimage of D₊(h), and D₊(h) is the image of D(g).

public theorem exists_homogeneous_awayι_preimage_basicOpen_eq {f : A} {m : ℕ} (hf : f ∈ 𝒜 m)
    (hm : 0 < m) (g : Away 𝒜 f) :
    ∃ (n : ℕ) (h : A) (hh : h ∈ 𝒜 (n • m)), 0 < n • m ∧
      Away.mk 𝒜 hf n h hh = g ∧
      AlgebraicGeometry.Proj.basicOpen 𝒜 h ≤ AlgebraicGeometry.Proj.basicOpen 𝒜 f ∧
      AlgebraicGeometry.Proj.awayι 𝒜 f hf hm ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜 h =
        PrimeSpectrum.basicOpen g ∧
      AlgebraicGeometry.Proj.awayι 𝒜 f hf hm ''ᵁ PrimeSpectrum.basicOpen g =
        AlgebraicGeometry.Proj.basicOpen 𝒜 h
Tag 01MB, a lemma

Tag 01MB in the Stacks Project.

AlgebraicGeometry.associatedModuleSheaf_isQuasicoherent, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjGradedRing/Basic.lean, line 454. The attribute's comment: “associated graded-module sheaves are quasi-coherent”. References: EGA II (3.2.1), “affine base”; EGA II (3.2.2), “affine base Y”.

The sheaf of degree-zero local homogeneous fractions of a graded module on its projective spectrum is quasi-coherent.

instance associatedModuleSheaf_isQuasicoherent [Decomposition 𝒨] :
    SheafOfModules.IsQuasicoherent.{u, u, u}
      (ProjectiveSpectrum.Proj.associatedModuleSheaf 𝒮 𝒨)

AlgebraicGeometry.ProjectiveSpectrum.Proj.associatedModuleSheaf_isQuasicoherent, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjGradedModuleQcoh/Quasicoherent.lean, line 247. The attribute's comment: “associated graded-module sheaves are quasi-coherent”. References: EGA II (3.2.1), “affine base”; EGA II (3.2.2), “affine base Y”.

The sheaf of degree-zero local homogeneous fractions of a graded module on its projective spectrum is quasi-coherent.

public instance associatedModuleSheaf_isQuasicoherent :
    SheafOfModules.IsQuasicoherent.{u, u, u} (associatedModuleSheaf 𝒜 𝒨)

Declarations registered for the tag:

Tag 01MD, a lemma

Tag 01MD in the Stacks Project.

AlgebraicGeometry.Proj.compactSpace_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjQuasiCompact.lean, line 89. The attribute's comment: “quasi-compactness criterion”.

The projective spectrum is quasi-compact exactly when finitely many positive-degree homogeneous elements generate an ideal whose radical contains the irrelevant ideal.

public theorem compactSpace_iff :
    CompactSpace (AlgebraicGeometry.Proj 𝒮) ↔
      ∃ s : Finset S,
        (∀ f ∈ s, ∃ d : ℕ, 0 < d ∧ f ∈ 𝒮 d) ∧
          (HomogeneousIdeal.irrelevant 𝒮).toIdeal ≤ (Ideal.span (s : Set S)).radical

AlgebraicGeometry.Proj.iSup_basicOpen_eq_top_of_irrelevant_le_radical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjQuasiCompact.lean, line 124. The attribute's comment: “standard-open cover”. References: EGA II (2.3.14), “special case”.

Elements whose span contains the irrelevant ideal up to radical have standard opens covering the projective spectrum.

public theorem iSup_basicOpen_eq_top_of_irrelevant_le_radical (s : Finset S)
    (h : (HomogeneousIdeal.irrelevant 𝒮).toIdeal ≤ (Ideal.span (s : Set S)).radical) :
    ⨆ f ∈ s, Proj.basicOpen 𝒮 f = ⊤
Tag 01ME, a lemma

Tag 01ME in the Stacks Project.

Stacks.AlgebraicGeometry.ProjToSpecZero.toSpecZero_base_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjToSpecZero.lean, line 85. The attribute's comment: “the canonical morphism Proj S → Spec S₀, equal on points to 𝔭 ↦ 𝔭 ∩ S₀”.

The canonical morphism Proj 𝒜 ⟶ Spec 𝒜₀ is Proj.toSpecZero 𝒜, glued from the ring maps 𝒜₀ → S_(f) on the standard opens. On underlying topological spaces it is the map of the homogeneous spectrum: the inclusion Proj 𝒜 ⊆ Spec S followed by Spec S → Spec 𝒜₀ induced by 𝒜₀ ⊆ S, i.e. 𝔭 ↦ 𝔭 ∩ 𝒜₀.

theorem toSpecZero_base_eq :
    ⇑(Proj.toSpecZero 𝒜) =
      PrimeSpectrum.comap (algebraMap (𝒜 0) A) ∘ _root_.Proj.toSpec 𝒜
Tag 01MF, a lemma

Tag 01MF in the Stacks Project.

Stacks.AlgebraicGeometry.ProjToSpecZero.valuativeCriterion_toSpecZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjToSpecZero.lean, line 95. The attribute's comment: “existence and uniqueness parts of the valuative criterion for Proj S → Spec S₀”.

The valuative criterion for Proj 𝒜 ⟶ Spec 𝒜₀. If S is finitely generated as an 𝒜₀-algebra, then for every valuation ring O with fraction field K and every commutative square Spec K ⟶ Proj 𝒜, Spec O ⟶ Spec 𝒜₀, there exists a lift Spec O ⟶ Proj 𝒜 (existence) and it is unique (uniqueness, from separatedness).

theorem valuativeCriterion_toSpecZero [Algebra.FiniteType (𝒜 0) A] :
    ValuativeCriterion (Proj.toSpecZero 𝒜)
Tag 01MG, an example

Tag 01MG in the Stacks Project.

AlgebraicGeometry.FractionalExponentExample.exists_nonextendable_valuative_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjNonextendableValuativeMap.lean, line 572.

The specified valuative example: the canonical generic-fibre morphism induced by polynomialMap cannot be extended to the spectrum of the local valuation ring.

theorem exists_nonextendable_valuative_map :
    ∃ hm : positiveIdeal.IsPrime,
      letI : positiveIdeal.IsPrime := hm
      letI : GradedRing (MvPolynomial.homogeneousSubmodule ℕ ℂ) :=
        MvPolynomial.gradedAlgebra
      let A := Localization positiveIdeal.primeCompl
      let K := FractionRing A
      let φ : polynomialAlgebra →+* K :=
        (algebraMap fractionalExponentAlgebra K).comp polynomialMap.toRingHom
      let F : polynomialAlgebra →+* Γ(Spec (CommRingCat.of K), ⊤) :=
        (Scheme.ΓSpecIso (CommRingCat.of K)).inv.hom.comp φ
      (IsValuationRing A) ∧
        ∃ hf : (HomogeneousIdeal.irrelevant
            (MvPolynomial.homogeneousSubmodule ℕ ℂ)).toIdeal.map F = ⊤,
          ¬ ∃ g : Spec (CommRingCat.of A) ⟶
              Proj (MvPolynomial.homogeneousSubmodule ℕ ℂ),
            Spec.map (CommRingCat.ofHom (algebraMap A K)) ≫ g =
              Proj.fromOfGlobalSections
                (MvPolynomial.homogeneousSubmodule ℕ ℂ) F hf
Tag 01MH, an example

Tag 01MH in the Stacks Project.

Stacks.IteratedSquareRootAlgebra.projCanonicalProperties, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjIteratedSquareRootImage.lean, line 367. The attribute's comment: “the example's six assertions in one statement”.

Stacks Project, Tag 01MH. The worked example in a single statement, for the grading the source specifies on S = ℂ[t][X₁, X₂, …]/(Xᵢ² - t Xᵢ₊₁), deg Xᵢ = 2ⁱ⁻¹. In order: the image of t lies in no point of Proj S; consecutive generators define the same standard open, D₊(Xᵢ) = D₊(Xᵢ₊₁); Proj S is quasi-compact; it is affine, being the single standard open D₊(X₁); the image of Proj S → Spec ℂ[t] is the distinguished open D(t); and that morphism is therefore not closed.

public theorem projCanonicalProperties :
    (∀ p : ProjectiveSpectrum canonicalGrading.grading,
        algebraMap baseRing ring t ∉ p.asHomogeneousIdeal) ∧
      (∀ i : ℕ, ProjectiveSpectrum.basicOpen canonicalGrading.grading (x i) =
        ProjectiveSpectrum.basicOpen canonicalGrading.grading (x (i + 1))) ∧
      CompactSpace (AlgebraicGeometry.Proj canonicalGrading.grading) ∧
      Proj.basicOpen canonicalGrading.grading (x 0) = ⊤ ∧
      IsAffine (AlgebraicGeometry.Proj canonicalGrading.grading) ∧
      Set.range
          (Proj.toSpecZero canonicalGrading.grading ≫
            Spec.map (CommRingCat.ofHom
              ((GradedRing.projZeroRingHom' canonicalGrading.grading).comp
                (algebraMap baseRing ring)))).base =
        ((Spec (.of baseRing)).basicOpen
          ((Scheme.ΓSpecIso (.of baseRing)).inv t) : Set (Spec (.of baseRing))) ∧
      ¬ IsClosed (Set.range
        (Proj.toSpecZero canonicalGrading.grading ≫
          Spec.map (CommRingCat.ofHom
            ((GradedRing.projZeroRingHom' canonicalGrading.grading).comp
              (algebraMap baseRing ring)))).base)
Tag 01MI, an example

Tag 01MI in the Stacks Project.

AlgebraicGeometry.ProjectiveSpace.isIso_toSpecZero_oneVariable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjOfPolynomialOneVariable.lean, line 119.

Proj of a polynomial ring in one variable is the spectrum of the coefficient ring. The canonical morphism Proj A[T] ⟶ Spec A[T]₀ of a graded ring to the spectrum of its degree-zero part is an isomorphism when A[T] is the polynomial ring in one variable of degree one.

public theorem isIso_toSpecZero_oneVariable :
    IsIso (Proj.toSpecZero (homogeneousSubmodule (Fin 1) A))
Tag 0G5W, an example

Tag 0G5W in the Stacks Project.

AlgebraicGeometry.openProjAlgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjOfOpenInAffine.lean, line 88. The attribute's comment: “the graded subring”.

The subalgebra of A[T] generated by A and all f Tⁿ with D(f) ⊆ U.

public noncomputable def openProjAlgebra (U : (Spec (.of A)).Opens) :
    Subalgebra A (MvPolynomial (Fin 1) A)

AlgebraicGeometry.openProjGrading, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjOfOpenInAffine.lean, line 95. The attribute's comment: “the homogeneous components”.

The degree-n piece of the indicated subalgebra, inherited from polynomial degree.

public noncomputable def openProjGrading (U : (Spec (.of A)).Opens) (n : ℕ) :
    Submodule A (openProjAlgebra U)

AlgebraicGeometry.openProjGradedRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjOfOpenInAffine.lean, line 238. The attribute's comment: “the grading”.

The polynomial-degree decomposition restricts to the algebra of the open.

public noncomputable def openProjGradedRing (U : (Spec (.of A)).Opens) :
    GradedRing (openProjGrading U)

AlgebraicGeometry.openProjDegreeZeroEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjOfOpenInAffine.lean, line 265. The attribute's comment: “the degree-zero ring”.

The canonical identification of the degree-zero part with the coefficient ring.

public noncomputable def openProjDegreeZeroEquiv (U : (Spec (.of A)).Opens) :
    letI := openProjGradedRing U
    A ≃+* openProjGrading U 0

AlgebraicGeometry.openProjDegreeZeroEquiv_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjOfOpenInAffine.lean, line 306. The attribute's comment: “the canonical degree-zero identification”.

The degree-zero identification sends a coefficient to its image in the subalgebra.

public theorem openProjDegreeZeroEquiv_apply (U : (Spec (.of A)).Opens) (a : A) :
    letI := openProjGradedRing U
    ((openProjDegreeZeroEquiv U a : openProjGrading U 0) : openProjAlgebra U) =
      algebraMap A (openProjAlgebra U) a

AlgebraicGeometry.projOpenIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjOfOpenInAffine.lean, line 1033. The attribute's comment: “the isomorphism with the open subscheme”.

The projective spectrum of the indicated algebra is the chosen open subscheme.

public noncomputable def projOpenIso (U : (Spec (.of A)).Opens) :
    letI := openProjGradedRing U
    AlgebraicGeometry.Proj (openProjGrading U) ≅ U.toScheme

AlgebraicGeometry.projOpenIso_hom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjOfOpenInAffine.lean, line 1043. The attribute's comment: “compatibility with the structure morphism”.

Under the isomorphism, the canonical morphism to Spec A is inclusion.

public theorem projOpenIso_hom_comp (U : (Spec (.of A)).Opens) :
    letI := openProjGradedRing U
    Proj.toSpecZero (openProjGrading U) ≫
      Spec.map (CommRingCat.ofHom (openProjDegreeZeroEquiv U).toRingHom) =
        (projOpenIso U).hom ≫ U.ι
Sources
LeanStacks.ProjStandardOpenStatement.tag01M4 · ProjectiveSpectrum.IsStandardOpenCover · AlgebraicGeometry.ProjectiveSpectrum.Proj.associatedModuleSheafStandardOpenEquiv_restrict · AlgebraicGeometry.ProjectiveSpectrum.Proj.coe_associatedModuleSheafStandardOpenEquiv_smul · AlgebraicGeometry.ProjectiveSpectrum.Proj.associatedModuleSheaf · AlgebraicGeometry.ProjectiveSpectrum.Proj.degreeZeroToSection_injective · AlgebraicGeometry.ProjectiveSpectrum.Proj.degreeZeroToSection_surjective · AlgebraicGeometry.ProjectiveSpectrum.Proj.associatedModuleSheafStandardOpenEquiv

Section27.9 Quasi-coherent sheaves on Proj#

Section 27.9 of the Stacks Project, Tag 01MJ. 4 tags here are carried by 7 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0AG1, an equation

Tag 0AG1 in the Stacks Project.

Declarations registered for the tag:

Tag 0AG2, an equation

Tag 0AG2 in the Stacks Project.

Stacks.AlgebraicGeometry.ProjShiftedSections.degreeNToGlobalSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjShiftedSectionModule.lean, line 309. The attribute's comment: “map_degree_n_global_sections”. References: EGA II (3.3.2), “partial, special case”.

The canonical map from the degree-n homogeneous elements of M to the global sections of M(n)~, as an additive homomorphism: it is the degree-zero global-sections map of the shift. This is the map Mₙ → Γ(Proj(S), M(n)~) of Tag 0AG2, obtained from the degree-zero map of Tag 0AG1 for the grading of M(n) and the identification M(n)₀ = Mₙ of Stacks.GradedModule.shiftedGrading_zero.

public noncomputable def degreeNToGlobalSections (n : ℤ) :
    𝒨 n →+ shiftedSectionsComponent 𝒮 𝒨 n

Stacks.GradedModule.shiftedGrading_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjTwistGlobalSections.lean, line 78. The attribute's comment: “twist_degree_zero”.

The degree-zero piece of the twist M(n) is the degree-n piece of M: M(n)₀ = Mₙ. The two indices are 0 + n and n, which are equal by zero_add and not by reduction.

public theorem shiftedGrading_zero {M : Type v} {τ : Type t} [SetLike τ M] (𝒩 : ℤ → τ) (n : ℤ) :
    shiftedGrading 𝒩 n 0 = 𝒩 n
Tag 01MK, a lemma

Tag 01MK in the Stacks Project.

Stacks.AlgebraicGeometry.ProjSheafFunctoriality.associatedModuleSheafTensorMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjSheafFunctoriality/Tensor.lean, line 661. The attribute's comment: “canonical sheaf morphism”. References: EGA II (2.5.11), “(2.5.11.2)”; EGA II (3.2.6), “λ (3.2.6.1)”.

The canonical morphism from the tensor product of the associated sheaves of M and N to the associated sheaf of the graded tensor product M ⊗[S] N.

def associatedModuleSheafTensorMap :
    letI := tensorGrading_decomposition (S := S) 𝒮 𝒨 𝒩
    letI := tensorGrading_gradedSMul (S := S) 𝒮 𝒨 𝒩
    (((Stacks.SheafOfModules.Tensor.sheafTensor ((_root_.AlgebraicGeometry.Proj
      𝒮).toRingedSpace).sheaf).obj ((ProjectiveSpectrum.Proj.associatedModuleSheaf 𝒮 𝒨))).obj
      ((ProjectiveSpectrum.Proj.associatedModuleSheaf 𝒮 𝒩))) ⟶
      ProjectiveSpectrum.Proj.associatedModuleSheaf 𝒮 (tensorGrading (S := S) 𝒨 𝒩)

Stacks.AlgebraicGeometry.ProjSheafFunctoriality.associatedModuleSheafTensorMap_standardOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjSheafFunctoriality/Tensor.lean, line 731. The attribute's comment: “formula on standard opens”. References: EGA II (2.5.11), “λ_f on D_+(f)”.

On a positive-degree standard open, the canonical morphism sends the tensor of two homogeneous fractions to the fraction of their tensor over the product of the denominators.

theorem associatedModuleSheafTensorMap_standardOpen
    {f : S} {d : ℕ} (hf : f ∈ 𝒮 d) (hd : 0 < d)
    (p q : ℕ) (m : M) (hm : m ∈ 𝒨 (p • (d : ℤ)))
    (n : N) (hn : n ∈ 𝒩 (q • (d : ℤ))) :
    letI := tensorGrading_decomposition (S := S) 𝒮 𝒨 𝒩
    letI := tensorGrading_gradedSMul (S := S) 𝒮 𝒨 𝒩
    let U := ProjectiveSpectrum.basicOpen 𝒮 f
    let F := ProjectiveSpectrum.Proj.associatedModuleSheaf 𝒮 𝒨
    let G := ProjectiveSpectrum.Proj.associatedModuleSheaf 𝒮 𝒩
    ((associatedModuleSheafTensorMap 𝒮 𝒨 𝒩).val.app (op U))
      (Stacks.SheafOfModules.TensorStalkRingedSpace.toTensorSheafSection
        (_root_.AlgebraicGeometry.Proj 𝒮).toRingedSpace F G (op U)
        (((ProjectiveSpectrum.Proj.associatedModuleSheafStandardOpenEquiv 𝒮 𝒨 hf hd).symm
          (ProjectiveSpectrum.Proj.degreeZeroFraction 𝒮 𝒨 hf p m hm)) ⊗ₜ[_]
         ((ProjectiveSpectrum.Proj.associatedModuleSheafStandardOpenEquiv 𝒮 𝒩 hf hd).symm
          (ProjectiveSpectrum.Proj.degreeZeroFraction 𝒮 𝒩 hf q n hn)))) =
      (ProjectiveSpectrum.Proj.associatedModuleSheafStandardOpenEquiv 𝒮
        (tensorGrading (S := S) 𝒨 𝒩) hf hd).symm
        (ProjectiveSpectrum.Proj.degreeZeroFraction 𝒮 (tensorGrading (S := S) 𝒨 𝒩)
          hf (p + q) (m ⊗ₜ[S] n)
          (by
            apply AddSubgroup.subset_closure
            refine ⟨p • (d : ℤ), q • (d : ℤ), ?_, m, hm, n, hn, rfl⟩
            simp [add_mul]))

Stacks.AlgebraicGeometry.ProjSheafFunctoriality.associatedModuleSheafTensorMap_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjSheafFunctoriality/Tensor.lean, line 794. The attribute's comment: “formula on stalks”.

On the stalk at a homogeneous prime of a positive-degree standard open, the canonical morphism carries the tensor of the germs of two homogeneous fractions to the germ of the fraction of their tensor.

theorem associatedModuleSheafTensorMap_stalk
    {f : S} {d : ℕ} (hf : f ∈ 𝒮 d) (hd : 0 < d)
    (x : ProjectiveSpectrum.top 𝒮)
    (hx : x ∈ ProjectiveSpectrum.basicOpen 𝒮 f)
    (p q : ℕ) (m : M) (hm : m ∈ 𝒨 (p • (d : ℤ)))
    (n : N) (hn : n ∈ 𝒩 (q • (d : ℤ))) :
    letI := tensorGrading_decomposition (S := S) 𝒮 𝒨 𝒩
    letI := tensorGrading_gradedSMul (S := S) 𝒮 𝒨 𝒩
    let X := (_root_.AlgebraicGeometry.Proj 𝒮).toRingedSpace
    let U := ProjectiveSpectrum.basicOpen 𝒮 f
    let F := ProjectiveSpectrum.Proj.associatedModuleSheaf 𝒮 𝒨
    let G := ProjectiveSpectrum.Proj.associatedModuleSheaf 𝒮 𝒩
    let T := ProjectiveSpectrum.Proj.associatedModuleSheaf 𝒮 (tensorGrading (S := S) 𝒨 𝒩)
    letI := Stacks.SheafOfModules.TensorStalkRingedSpace.stalkModule X F.val x
    letI := Stacks.SheafOfModules.TensorStalkRingedSpace.stalkModule X G.val x
    letI := Stacks.SheafOfModules.TensorStalkRingedSpace.stalkModule X
      ((((Stacks.SheafOfModules.Tensor.sheafTensor (X).sheaf).obj (F)).obj (G))).val x
    letI := Stacks.SheafOfModules.TensorStalkRingedSpace.stalkModule X T.val x
    Stacks.SheafOfModules.TensorStalkRingedSpace.stalkMapL X
      ((((Stacks.SheafOfModules.Tensor.sheafTensor (X).sheaf).obj (F)).obj (G))).val T.val
      (associatedModuleSheafTensorMap 𝒮 𝒨 𝒩).val x
      ((Stacks.SheafOfModules.TensorStalkRingedSpace.tensorStalkIso X x F G).symm
        ((Stacks.SheafOfModules.TensorStalkRingedSpace.grpGerm X F.val x U hx
            ((ProjectiveSpectrum.Proj.associatedModuleSheafStandardOpenEquiv 𝒮 𝒨 hf hd).symm
              (ProjectiveSpectrum.Proj.degreeZeroFraction 𝒮 𝒨 hf p m hm)))
          ⊗ₜ[Stacks.SheafOfModules.TensorStalkRingedSpace.ringStalk X x]
         (Stacks.SheafOfModules.TensorStalkRingedSpace.grpGerm X G.val x U hx
            ((ProjectiveSpectrum.Proj.associatedModuleSheafStandardOpenEquiv 𝒮 𝒩 hf hd).symm
              (ProjectiveSpectrum.Proj.degreeZeroFraction 𝒮 𝒩 hf q n hn))))) =
      Stacks.SheafOfModules.TensorStalkRingedSpace.grpGerm X T.val x U hx
        ((ProjectiveSpectrum.Proj.associatedModuleSheafStandardOpenEquiv 𝒮
          (tensorGrading (S := S) 𝒨 𝒩) hf hd).symm
          (ProjectiveSpectrum.Proj.degreeZeroFraction 𝒮 (tensorGrading (S := S) 𝒨 𝒩)
            hf (p + q) (m ⊗ₜ[S] n)
            (by
              apply AddSubgroup.subset_closure
              refine ⟨p • (d : ℤ), q • (d : ℤ), ?_, m, hm, n, hn, rfl⟩
              simp [add_mul])))

Stacks.AlgebraicGeometry.ProjStalkGlobalSections.associatedModuleSheafTensorMap_globalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjStalkGlobalSections/Tensor.lean, line 67. The attribute's comment: “global-sections compatibility”.

The canonical morphism commutes with the maps from degree-zero elements into global sections, evaluated on a pure tensor.

theorem associatedModuleSheafTensorMap_globalSections (m : 𝒨 0) (n : 𝒩 0) :
    letI := ProjSheafFunctoriality.tensorGrading_decomposition (S := S) 𝒮 𝒨 𝒩
    letI := ProjSheafFunctoriality.tensorGrading_gradedSMul (S := S) 𝒮 𝒨 𝒩
    let F := ProjectiveSpectrum.Proj.associatedModuleSheaf 𝒮 𝒨
    let G := ProjectiveSpectrum.Proj.associatedModuleSheaf 𝒮 𝒩
    ((ProjSheafFunctoriality.associatedModuleSheafTensorMap 𝒮 𝒨 𝒩).val.app (op ⊤))
      (Stacks.SheafOfModules.TensorStalkRingedSpace.toTensorSheafSection
        (_root_.AlgebraicGeometry.Proj 𝒮).toRingedSpace F G (op ⊤)
        ((degreeZeroToGlobalSections 𝒮 𝒨 m) ⊗ₜ[_]
         (degreeZeroToGlobalSections 𝒮 𝒩 n))) =
      degreeZeroToGlobalSections 𝒮 (tensorGrading (S := S) 𝒨 𝒩)
        ⟨m.1 ⊗ₜ[S] n.1,
          (by
            apply AddSubgroup.subset_closure
            exact ⟨0, 0, by simp, m.1, m.2, n.1, n.2, rfl⟩)⟩
Tag 01ML, a remark

Tag 01ML in the Stacks Project.

Stacks.ProjTensorComparison.tensorComparison_not_isomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjTensorComparisonStatement.lean, line 146. The attribute's comment: “Remark 27.10.3 as one theorem: the canonical comparison morphism M-tilde ⊗ N-tilde ⟶ (M ⊗_S N)-tilde of sheaves of modules on Proj(S) is not an isomorphism, and for k[x, y, z] with weights 1, 2, 3, M = S(1) and N = S(2) the remark's computation — S_z is S with 1/z adjoined, M ⊗_S N = S(3) degreewise, S₍z₎ ≅ k[u, v, w]/(uw - v³) by the map sending the variables to u, v, w, M₍z₎ = S₍z₎x + S₍z₎y²/z, N₍z₎ = S₍z₎y + S₍z₎x², S(3)₍z₎ = S₍z₎z, the ideal (u, v, w) is maximal with residue field k, the fibres of M₍z₎ and N₍z₎ there have dimension 2 and that of S(3)₍z₎ dimension 1, and the multiplication map M₍z₎ ⊗ N₍z₎ → S(3)₍z₎ is not bijective. The first conjunct is witnessed by k[X] with deg X = 2 and M = N = S(1)”.

Stacks Project, Tag 01ML. The canonical comparison morphism M̃ ⊗_𝒪 Ñ ⟶ (M ⊗_S N)~ of sheaves of modules on Proj(S) is not an isomorphism, and the remark's example computes why. For a field k and S = k[x, y, z] with weights 1, 2, 3, M = S(1), N = S(2):

  1. the comparison morphism of sheaves of modules is not an isomorphism;
  2. S_z is S with 1/z adjoined;
  3. M ⊗_S N = S(3), degreewise;
  4. S₍z₎ ≅ k[u, v, w]/(uw - v³), by the map carrying the three variables to u, v, w;
  5. M₍z₎ = S₍z₎ · x + S₍z₎ · y²/z;
  6. N₍z₎ = S₍z₎ · y + S₍z₎ · x²;
  7. S(3)₍z₎ = S₍z₎ · z;
  8. 𝔪 = (u, v, w) is a maximal ideal of S₍z₎;
  9. its residue field is k;
  10. the fibres of M₍z₎ and of N₍z₎ at 𝔪 have dimension 2, and that of S(3)₍z₎ dimension 1;
  11. the multiplication map M₍z₎ ⊗_{S₍z₎} N₍z₎ → S(3)₍z₎ is not bijective.

Conjunct (1) is the failure of generality asserted by Stacks Tag 01ML of the morphism constructed in Stacks Tag 01MK, and it is witnessed by k[X] with deg X = 2 and M = N = S(1) rather than by the remark's own weights; see the module docstring for what a derivation from the remark's own witness would still need. Conjunct (4) is stated as the existence of an algebra isomorphism together with its values on the three variables, which pins it down to the map the remark writes.

theorem tensorComparison_not_isomorphism :
    letI : (situation k).vertexIdeal.IsMaximal :=
      WeightedPolynomialSituation.vertexIdeal_isMaximal (situation k)
    (¬ IsIso (Stacks.AlgebraicGeometry.ProjSheafFunctoriality.associatedModuleSheafTensorMap
        (Stacks.EvenWeightProj.grading k) (Stacks.EvenWeightProj.oddTwist k)
        (Stacks.EvenWeightProj.oddTwist k))) ∧
      Algebra.adjoin (situation k).S
          ({(IsLocalization.Away.invSelf (situation k).z :
              (situation k).ordinaryLocalization)} :
            Set (situation k).ordinaryLocalization) = ⊤ ∧
      (∀ n : ℤ,
        Submodule.map
            ((TensorProduct.lid (situation k).S (situation k).S).toLinearMap.restrictScalars
              (situation k).k)
            (Submodule.span (situation k).k
              {t : TensorProduct (situation k).S (situation k).S (situation k).S |
                ∃ i j : ℤ, i + j = n ∧
                  ∃ a b : (situation k).S, a ∈ (situation k).grading (i + 1) ∧
                    b ∈ (situation k).grading (j + 2) ∧
                      t = TensorProduct.tmul (situation k).S a b}) =
          (situation k).grading (n + 3)) ∧
      (∃ e :
          (MvPolynomial (Fin 3) (situation k).k ⧸ cubicRelationIdeal (situation k).k)
            ≃ₐ[(situation k).k] (situation k).R,
        ∀ i : Fin 3,
          e (Ideal.Quotient.mk (cubicRelationIdeal (situation k).k) (MvPolynomial.X i)) =
            ![(situation k).u, (situation k).v, (situation k).w] i) ∧
      (situation k).firstTwistLocalization =
        Submodule.span (situation k).R
          {Localization.mk (situation k).x (1 : Submonoid.powers (situation k).z),
            Localization.mk ((situation k).y ^ 2)
              ⟨(situation k).z, Submonoid.mem_powers (situation k).z⟩} ∧
      (situation k).secondTwistLocalization =
        Submodule.span (situation k).R
          ({algebraMap (situation k).S (situation k).ordinaryLocalization (situation k).y,
            algebraMap (situation k).S (situation k).ordinaryLocalization
              ((situation k).x ^ 2)} : Set (situation k).ordinaryLocalization) ∧
      (situation k).localizedTwist 3 =
        Submodule.span (situation k).R
          {algebraMap (situation k).S (Localization.Away (situation k).z) (situation k).z} ∧
      (situation k).vertexIdeal.IsMaximal ∧
      Function.Bijective (algebraMap (situation k).k (situation k).vertexIdeal.ResidueField) ∧
      Module.finrank (situation k).vertexIdeal.ResidueField
        ((situation k).vertexIdeal.ResidueField ⊗[(situation k).R]
          (situation k).firstTwistLocalization) = 2 ∧
      Module.finrank ((situation k).R ⧸ (situation k).vertexIdeal)
        ((situation k).secondTwistLocalization ⧸
          (situation k).vertexIdeal •
            (⊤ : Submodule (situation k).R (situation k).secondTwistLocalization)) = 2 ∧
      Module.finrank ((situation k).R ⧸ (situation k).vertexIdeal)
        ((situation k).localizedTwist 3 ⧸
          (situation k).vertexIdeal •
            (⊤ : Submodule (situation k).R ((situation k).localizedTwist 3))) = 1 ∧
      ¬ Function.Bijective
          (WeightedPolynomialSituation.localizedTwistTensorMap (situation k))
Sources
LeanStacks.AlgebraicGeometry.ProjStalkGlobalSections.degreeZeroToGlobalSections · Stacks.AlgebraicGeometry.ProjShiftedSections.degreeNToGlobalSections · Stacks.GradedModule.shiftedGrading_zero · Stacks.AlgebraicGeometry.ProjSheafFunctoriality.associatedModuleSheafTensorMap · Stacks.AlgebraicGeometry.ProjSheafFunctoriality.associatedModuleSheafTensorMap_standardOpen · Stacks.AlgebraicGeometry.ProjSheafFunctoriality.associatedModuleSheafTensorMap_stalk · Stacks.AlgebraicGeometry.ProjStalkGlobalSections.associatedModuleSheafTensorMap_globalSections · Stacks.ProjTensorComparison.tensorComparison_not_isomorphism

Section27.10 Invertible sheaves on Proj#

Section 27.10 of the Stacks Project, Tag 01MM. 14 tags here are carried by 25 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01MN, a definition

Tag 01MN in the Stacks Project.

Stacks.ProjectiveCohomology.coe_sectionsTwistEquivAwayGrading_smul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjStandardOpenScalars.lean, line 134. The attribute's comment: “part (1), the scalar action in the standard-open description of the sections of a twist, written out on the underlying elements of the localization”.

The identification of Γ(D₊(f), 𝒪_P(m)) with the degree-m part of A_f is linear for the action of Γ(P, D₊(f)) read through AlgebraicGeometry.Proj.awayToSection: a section scaled by the fraction r has for underlying element the product of r.val with the underlying element of the section.

theorem coe_sectionsTwistEquivAwayGrading_smul (hf : f ∈ 𝒜 k) (hk : 0 < k) (m : ℤ)
    (r : HomogeneousLocalization.Away 𝒜 f)
    (s : (twistingSheaf 𝒜 m).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
    ((sectionsTwistEquivAwayGrading 𝒜 hf hk m
        ((ProjectiveSpectrum.Proj.awayToSection 𝒜 f).hom r • s) :
      LocalizedModule.Away f A)) =
      HomogeneousLocalization.val r •
        ((sectionsTwistEquivAwayGrading 𝒜 hf hk m s : LocalizedModule.Away f A))

AlgebraicGeometry.ProjectiveSpectrum.Proj.twistingSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjTwist.lean, line 168. The attribute's comment: “part (1), twist of the structure sheaf”.

The n-th twist of the structure sheaf on Proj(S).

public noncomputable abbrev twistingSheaf
    (𝒜 : ℕ → σ) [GradedRing 𝒜] (n : ℤ) :
    SheafOfModules.{u}
      ((sheafCompose (Opens.grothendieckTopology (ProjectiveSpectrum.top 𝒜))
        (forget₂ CommRingCat.{u} RingCat.{u})).obj
        (ProjectiveSpectrum.Proj.structureSheaf 𝒜))

AlgebraicGeometry.ProjectiveSpectrum.Proj.twistSheafOfModules, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjTwist.lean, line 178. The attribute's comment: “part (2), twist of a module sheaf”.

Tensoring an 𝒪_Proj(S)-module with the n-th twisting sheaf.

public noncomputable def twistSheafOfModules
    (𝒜 : ℕ → σ) [GradedRing 𝒜]
    (F : SheafOfModules.{u}
      ((sheafCompose (Opens.grothendieckTopology (ProjectiveSpectrum.top 𝒜))
        (forget₂ CommRingCat.{u} RingCat.{u})).obj
        (ProjectiveSpectrum.Proj.structureSheaf 𝒜))) (n : ℤ) :
    SheafOfModules.{u}
      ((sheafCompose (Opens.grothendieckTopology (ProjectiveSpectrum.top 𝒜))
        (forget₂ CommRingCat.{u} RingCat.{u})).obj
        (ProjectiveSpectrum.Proj.structureSheaf 𝒜))

Stacks.AlgebraicGeometry.ProjTwistAwayPiece.coe_sectionsTwistEquivGradedPiece_smul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjTwistAwayPieceScalars.lean, line 58. The attribute's comment: “part (1), the scalar action in the description of the sections of a twist over a standard open as a homogeneous piece of the graded localization, written out on the underlying elements of the localization”.

The identification Γ(D₊(f), 𝒪_X(n)) ≅ (A_f)_n is semilinear for the action of Γ(D₊(f), 𝒪_X) read through AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection: a section scaled by the fraction r has for underlying element the product of r.val with the underlying element of the section.

theorem coe_sectionsTwistEquivGradedPiece_smul (hf : f ∈ 𝒜 k) (hk : 0 < k) (n : ℤ)
    (r : HomogeneousLocalization.Away 𝒜 f)
    (s : (twistingSheaf 𝒜 n).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
    ((sectionsTwistEquivGradedPiece 𝒜 hf hk n
        ((ProjectiveSpectrum.Proj.awayToSection 𝒜 f).hom r • s) :
      LocalizedModule.Away f A)) =
      HomogeneousLocalization.val r •
        ((sectionsTwistEquivGradedPiece 𝒜 hf hk n s : LocalizedModule.Away f A))
Tag 01MO, an equation

Tag 01MO in the Stacks Project.

Declarations registered for the tag:

Tag 03GJ, an equation

Tag 03GJ in the Stacks Project.

AlgebraicGeometry.ProjectiveSpectrum.Proj.twistSheafMultiplicationMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjTwistModuleMultiplication.lean, line 51.

The canonical multiplication map 𝒪_X(n) ⊗ ℱ(m) ⟶ ℱ(n + m) on X = Proj S, for a sheaf of 𝒪_X-modules ℱ: reassociate, braid 𝒪(n) past ℱ, reassociate again, and multiply the two twists of the structure sheaf together.

public noncomputable def twistSheafMultiplicationMap
    (F : SheafOfModules.{u}
      ((sheafCompose (Opens.grothendieckTopology (ProjectiveSpectrum.top 𝒮))
        (forget₂ CommRingCat.{u} RingCat.{u})).obj
        (ProjectiveSpectrum.Proj.structureSheaf 𝒮))) (n m : ℤ) :
    (((Stacks.SheafOfModules.Tensor.sheafTensor.{u, u, u, u, u}
        (ProjectiveSpectrum.Proj.structureSheaf 𝒮)).obj ((twistingSheaf 𝒮 n))).obj
        ((twistSheafOfModules 𝒮 F m))) ⟶
      twistSheafOfModules 𝒮 F (n + m)
Tag 01MP, an equation

Tag 01MP in the Stacks Project.

AlgebraicGeometry.ProjectiveSpectrum.Proj.globalSectionsRingMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjTwistSectionRing.lean, line 379.

The canonical homomorphism of graded rings S → ⨁_{n ≥ 0} Γ(Proj 𝒮, 𝒪(n)). Its multiplication on sections is the pointwise product of local fractions, and in each degree it is the canonical map from the homogeneous elements; those two formulas determine it.

public noncomputable def globalSectionsRingMap : GlobalSectionsRingMap 𝒮

Stacks.AlgebraicGeometry.ProjTwistSectionRing.globalSectionsRingMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjTwistSectionRing/Statement.lean, line 210.

The canonical graded ring map S → ⨁ n ≥ 0, Γ(Proj(S), 𝒪(n)).

public def globalSectionsRingMap : GlobalSectionsRingMap 𝒮
Tag 03GK, an equation

Tag 03GK in the Stacks Project.

AlgebraicGeometry.ProjectiveSpectrum.Proj.globalSectionsPairing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjTwistSectionModule.lean, line 278.

The pairing (⨁_{n ≥ 0} Γ(X, 𝒪_X(n))) × (⨁_{m ∈ ℤ} Γ(X, ℱ(m))) ⟶ ⨁_{m ∈ ℤ} Γ(X, ℱ(m)) on X = Proj 𝒮: the biadditive extension of the canonical multiplication of a global section of 𝒪_X(n) with a global section of ℱ(m).

public noncomputable def globalSectionsPairing :
    (⨁ n : ℕ, twistGlobalSections 𝒮 n) →+
      (twistedGlobalSections 𝒮 F →+ twistedGlobalSections 𝒮 F)

AlgebraicGeometry.ProjectiveSpectrum.Proj.globalSectionsPairing_of_of, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjTwistSectionModule.lean, line 286.

The pairing of a global section of 𝒪(n) with a global section of ℱ(m) is their canonical product, a global section of ℱ(n + m).

public theorem globalSectionsPairing_of_of (n : ℕ) (m : ℤ) (s : twistGlobalSections 𝒮 n)
    (t : (twistSheafOfModules 𝒮 F m).val.obj (op ⊤)) :
    globalSectionsPairing 𝒮 F (DirectSum.of _ n s) (DirectSum.of _ m t) =
      DirectSum.of _ ((n : ℤ) + m) (multiplyHomogeneousSections 𝒮 F n m s t)

AlgebraicGeometry.ProjectiveSpectrum.Proj.twistedGlobalSectionsModule, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjTwistSectionModule.lean, line 904. The attribute's comment: “the module structure on the twisted global sections”.

The module ⨁_{m ∈ ℤ} Γ(X, ℱ(m)) over the graded ring ⨁_{n ≥ 0} Γ(X, 𝒪_X(n)) on X = Proj 𝒮, for the pairing that multiplies a global section of 𝒪_X(n) with a global section of ℱ(m) through the canonical morphism 𝒪_X(n) ⊗ ℱ(m) ⟶ ℱ(n + m).

public noncomputable instance twistedGlobalSectionsModule :
    Module (⨁ n : ℕ, twistGlobalSections 𝒮 n) (twistedGlobalSections 𝒮 F)
Tag 01MQ, an equation

Tag 01MQ in the Stacks Project.

Declarations registered for the tag:

Tag 01MR, an equation

Tag 01MR in the Stacks Project.

Stacks.AlgebraicGeometry.ProjShiftedSections.globalSectionsModuleMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjShiftedSectionModule.lean, line 473.

The canonical map of graded S-modules M → ⨁_{n ∈ ℤ} Γ(Proj 𝒮, M(n)~). In degree n it is the canonical map from the homogeneous elements of degree n, and a homogeneous scalar acts pointwise on local fractions; those two formulas determine the whole datum.

public noncomputable def globalSectionsModuleMap : GlobalSectionsModuleMap 𝒮 𝒨
Tag 01MS, a lemma

Tag 01MS in the Stacks Project.

Stacks.AlgebraicGeometry.ModuleTwistIso.twistsOnBasicOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ModuleTwistIso/StandardOpen.lean, line 66. The attribute's comment: “the lemma's five assertions in one statement”.

Let f ∈ S be homogeneous of degree d. Restricted to the standard open D₊(f), the twisting sheaf 𝒪_X(nd) is invertible and in fact trivial for every integer n, and the three families of canonical maps built from it are isomorphisms: 𝒪_X(nd) ⊗ 𝒪_X(m) ⟶ 𝒪_X(nd+m), 𝒪_X(nd) ⊗ ℱ(m) ⟶ ℱ(nd+m) for every sheaf of 𝒪_X-modules ℱ, and M̃ ⊗ 𝒪_X(nd) ⟶ M(nd)~ for every graded S-module M. The second index is arbitrary throughout, and d is not assumed positive.

theorem twistsOnBasicOpen {f : S} {d : ℕ} (hf : f ∈ 𝒮 d) :
    (∀ n : ℤ, _root_.AlgebraicGeometry.SheafOfModules.IsInvertible
        ((Over.forget (ProjectiveSpectrum.basicOpen 𝒮 f)).op ⋙
          (ProjectiveSpectrum.Proj.structureSheaf 𝒮).obj)
        ((projRingSheaf 𝒮).over (ProjectiveSpectrum.basicOpen 𝒮 f)).property
        ((twistingSheaf 𝒮 (n * d)).over (ProjectiveSpectrum.basicOpen 𝒮 f))) ∧
      (∀ n : ℤ, _root_.AlgebraicGeometry.SheafOfModules.IsTrivial
        ((Over.forget (ProjectiveSpectrum.basicOpen 𝒮 f)).op ⋙
          (ProjectiveSpectrum.Proj.structureSheaf 𝒮).obj)
        ((projRingSheaf 𝒮).over (ProjectiveSpectrum.basicOpen 𝒮 f)).property
        ((twistingSheaf 𝒮 (n * d)).over (ProjectiveSpectrum.basicOpen 𝒮 f))) ∧
      (∀ n m : ℤ, IsIso
        ((Scheme.Modules.restrictFunctor (AlgebraicGeometry.Proj.basicOpen 𝒮 f).ι).map
          (twistMultiplicationMap 𝒮 ((d : ℤ) * n) m))) ∧
      (∀ (F : SheafOfModules.{u}
          ((sheafCompose (Opens.grothendieckTopology (ProjectiveSpectrum.top 𝒮))
            (forget₂ CommRingCat.{u} RingCat.{u})).obj
            (ProjectiveSpectrum.Proj.structureSheaf 𝒮))) (n m : ℤ), IsIso
        ((Scheme.Modules.restrictFunctor (AlgebraicGeometry.Proj.basicOpen 𝒮 f).ι).map
          (twistSheafMultiplicationMap 𝒮 F ((d : ℤ) * n) m))) ∧
      (∀ (M : Type u) [AddCommGroup M] [Module S M] (τ : Type t) [SetLike τ M]
          [AddSubgroupClass τ M] (𝒨 : ℤ → τ) [DirectSum.Decomposition 𝒨]
          [SetLike.GradedSMul 𝒮 𝒨] (n : ℤ), IsIso
        ((Scheme.Modules.restrictFunctor (AlgebraicGeometry.Proj.basicOpen 𝒮 f).ι).map
          (moduleTwistMap 𝒮 𝒨 ((d : ℤ) * n))))
Tag 01MT, a lemma

Tag 01MT in the Stacks Project.

Stacks.AlgebraicGeometry.ProjTwistDegreeOneCover.isInvertible_twistingSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjTwistDegreeOneCover/Basic.lean, line 141. The attribute's comment: “the sheaves 𝒪_X(n) are invertible”. References: EGA II (3.2.5), “Second assertion”.

Stacks 01MT: the sheaves 𝒪_X(n) are invertible.

The trivializing sections are the ratios (f/1)^n on the standard opens D₊(f) with f ∈ S₁, assembled by Stacks.AlgebraicGeometry.ProjInvertibleLocus.isInvertible_twistingSheaf_of_ratioLocus_eq_top at d = 1.

public theorem isInvertible_twistingSheaf (hcover : DegreeOneCover 𝒮) (n : ℤ) :
    _root_.AlgebraicGeometry.SheafOfModules.IsInvertible (AlgebraicGeometry.Proj 𝒮).presheaf
      (AlgebraicGeometry.Proj 𝒮).ringCatSheaf.2 (twistingSheaf 𝒮 n)

Stacks.AlgebraicGeometry.ProjTwistDegreeOneCover.isIso_twistMultiplicationMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjTwistDegreeOneCover/Basic.lean, line 157. The attribute's comment: “equation 01MO is an isomorphism”.

Stacks 01MT: Equation 01MO 𝒪_X(n) ⊗ 𝒪_X(m) ⟶ 𝒪_X(n + m) is an isomorphism, for all integers n and m.

This is Stacks.AlgebraicGeometry.TwistTensor.isIso_twistMultiplicationMap_of_ratioLocus_eq_top at k = 1; the only work is the substitution of 1 * n for n, which has to be done after revert because the index occurs in the type of the morphism.

public theorem isIso_twistMultiplicationMap (hcover : DegreeOneCover 𝒮) (n m : ℤ) :
    IsIso (twistMultiplicationMap 𝒮 n m)

Stacks.AlgebraicGeometry.ProjTwistDegreeOneCover.isIso_twistSheafMultiplicationMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjTwistDegreeOneCover/Basic.lean, line 187. The attribute's comment: “equation 03GJ is an isomorphism”.

Stacks 01MT: Equation 03GJ 𝒪_X(n) ⊗ ℱ(m) ⟶ ℱ(n + m) is an isomorphism, for every sheaf of 𝒪_X-modules ℱ and all integers n and m.

The source deduces this clause from the Equation 01MO clause, and so does the proof: by construction AlgebraicGeometry.ProjectiveSpectrum.Proj.twistSheafMultiplicationMap is the composite of the inverse associator, the braiding on 𝒪(n) ⊗ ℱ tensored with 𝒪(m), the associator, and 𝟙 ℱ ⊗ (Equation 01MO). The first three factors are isomorphisms unconditionally, and the fourth is one because the native tensor bifunctor maps the product of two isomorphisms to an isomorphism.

public theorem isIso_twistSheafMultiplicationMap (hcover : DegreeOneCover 𝒮)
    (F : SheafOfModules.{u}
      ((sheafCompose (Opens.grothendieckTopology (ProjectiveSpectrum.top 𝒮))
        (forget₂ CommRingCat.{u} RingCat.{u})).obj
        (ProjectiveSpectrum.Proj.structureSheaf 𝒮))) (n m : ℤ) :
    IsIso (twistSheafMultiplicationMap 𝒮 F n m)

Stacks.AlgebraicGeometry.ProjTwistDegreeOneCover.nonempty_tensorPowModule_iso_twistingSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjTwistDegreeOneCover/Basic.lean, line 258. The attribute's comment: “the induced identification 𝒪_X(1)^{⊗ n} ≅ 𝒪_X(n)”. References: EGA II (2.5.14), “(2.5.14.2)”.

Stacks 01MT: the induced identification 𝒪_X(1)^{⊗ n} ≅ 𝒪_X(n), for every integer n, at the canonical integral tensor power Stacks.Ample.tensorPowModule of Tag 01CU.

Both families are carried one degree by the autoequivalence twistRight — the tensor powers by the addition law of Tag 01CU, the twists by Equation 01MO at (n, 1) — and they agree in degree one, so Stacks.AlgebraicGeometry.ProjTwistPowers.nonempty_iso_of_shift identifies them in every degree, negative ones included, with no separate argument.

The library already had this under the stronger hypothesis Algebra.adjoin (𝒮 0) (𝒮 1) = ⊤, as Stacks.AlgebraicGeometry.ProjTwistPowers.nonempty_tensorPowModule_iso_twistingSheaf; this is the same statement at the source's own printed hypothesis.

public theorem nonempty_tensorPowModule_iso_twistingSheaf (hcover : DegreeOneCover 𝒮) (n : ℤ) :
    letI := isInvertibleModule_twistingSheaf 𝒮 hcover 1
    Nonempty (Stacks.Ample.tensorPowModule (AlgebraicGeometry.Proj 𝒮) (twistingSheaf 𝒮 1) n ≅
      twistingSheaf 𝒮 n)

Stacks.AlgebraicGeometry.ProjTwistDegreeOneCover.isIso_moduleTwistMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjTwistDegreeOneCover/Basic.lean, line 314. The attribute's comment: “equation 01MQ is an isomorphism”. References: EGA II (2.5.15); EGA II (3.2.8).

Stacks 01MT: Equation 01MQ M̃ ⊗ 𝒪_X(n) ⟶ M(n)̃ is an isomorphism, for every graded S-module M and every integer n.

isIso_moduleTwistMap_of_ratioLocus_eq_top at d = 1.

public theorem isIso_moduleTwistMap (hcover : DegreeOneCover 𝒮) (n : ℤ) :
    IsIso (ProjShifted.moduleTwistMap 𝒮 𝒨 n)

Stacks.AlgebraicGeometry.ProjTwistDegreeOneCover.moduleTwistIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjTwistDegreeOneCover/Basic.lean, line 324. The attribute's comment: “the induced isomorphism M̃ ⊗ 𝒪_X(n) ≅ M(n)~”.

Stacks 01MT: the induced isomorphism M̃ ⊗_{𝒪_X} 𝒪_X(n) = M̃(n) ≅ M(n)̃.

public def moduleTwistIso (hcover : DegreeOneCover 𝒮) (n : ℤ) :
    (((Stacks.SheafOfModules.Tensor.sheafTensor
        ⟨(((AlgebraicGeometry.Proj 𝒮).toRingedSpace)).presheaf,
          (((AlgebraicGeometry.Proj 𝒮).toRingedSpace)).IsSheaf⟩).obj
        ((associatedModuleSheaf 𝒮 𝒨))).obj ((twistingSheaf 𝒮 n))) ≅
      associatedModuleSheaf 𝒮 (shiftedGrading 𝒨 n)
Tag 0AG3, an equation

Tag 0AG3 in the Stacks Project.

Stacks.AlgebraicGeometry.ProjTwistDegreeOneCover.degreeNToTwistedGlobalSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjTwistDegreeOneCover/GlobalSections.lean, line 87.

Equation 0AG3: the canonical map M_n ⟶ Γ(X, M̃(n)). A homogeneous element of degree n gives a global section of M(n)~, which the isomorphism M(n)~ ≅ M̃(n) of Tag 01MT turns into a global section of the twist M̃(n).

public def degreeNToTwistedGlobalSections (hcover : DegreeOneCover 𝒮) (n : ℤ) :
    𝒨 n →+ twistedModuleGlobalSections 𝒮 𝒨 n
Tag 01MU, a lemma

Tag 01MU in the Stacks Project.

Stacks.AlgebraicGeometry.GoodOpenClose.isGoodOpen_iff_le_whereInvertible_of_pos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GoodOpenClose/Basic.lean, line 156. The attribute's comment: “maximality and goodness of the invertible locus”.

For 0 < d, an open is good exactly when it lies in the largest good open whereInvertible 𝒮 d.

theorem isGoodOpen_iff_le_whereInvertible_of_pos (d : ℕ) (_hd : 0 < d)
    (U : (AlgebraicGeometry.Proj 𝒮).Opens) :
    IsGoodOpen 𝒮 d U ↔ U ≤ whereInvertible 𝒮 d

Stacks.AlgebraicGeometry.GoodOpenClose.whereInvertible_eq_iSup_basicOpen_mul_of_pos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GoodOpenClose/Basic.lean, line 186. The attribute's comment: “equality of the two open subsets”.

For 0 < d, the largest good open whereInvertible 𝒮 d is the union of the standard opens D₊(fg) with deg f = deg g + d.

theorem whereInvertible_eq_iSup_basicOpen_mul_of_pos (d : ℕ) (_hd : 0 < d) :
    whereInvertible 𝒮 d =
      ⨆ (e : ℕ) (f : 𝒮 (e + d)) (g : 𝒮 e),
        AlgebraicGeometry.Proj.basicOpen 𝒮 ((f : S) * (g : S))

Stacks.AlgebraicGeometry.ModuleTwistIso.moduleTwistMap_isIso_on_whereInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ModuleTwistIso/Basic.lean, line 391. The attribute's comment: “comparison for associated modules”.

On the largest open on which the d-divisible twists are invertible and their multiplication maps are isomorphisms, the canonical comparison from the tensor product of an associated sheaf with such a twist to the associated sheaf of the shifted module is an isomorphism, for every graded module and every integral multiple of d. The hypothesis 0 < d is not used.

theorem moduleTwistMap_isIso_on_whereInvertible (d : ℕ) (_hd : 0 < d) (n : ℤ) :
    IsIso ((Scheme.Modules.restrictFunctor (whereInvertible 𝒮 d).ι).map
      (moduleTwistMap 𝒮 𝒨 ((d : ℤ) * n)))
Tag 01MV, a lemma

Tag 01MV in the Stacks Project.

Stacks.AlgebraicGeometry.ProjInvertibleLocus.nonvanishingLocus_degreeSection_inter, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjInvertibleLocus/NonvanishingLocus.lean, line 534.

Stacks Tag 01MV. Let S be a graded ring, X = Proj(S), d ≥ 1, n ≥ 1 and f ∈ S_{nd}. Let s be the global section of 𝒪(nd) attached to f. Then, on the open W_d where the d-divisible twists are invertible, the nonvanishing locus of s is the standard open D₊(f):

X_s ∩ W_d = D₊(f) ∩ W_d.

This is stated on Proj(S) rather than on the open subscheme W_d, which is strictly stronger than the form of the source: the statement there is the image of this one under Stacks.SheafOfModules.preimage_nonvanishingLocus. No positivity of d or n is needed.

theorem nonvanishingLocus_degreeSection_inter (d n : ℕ) (f : 𝒮 (n * d)) :
    Stacks.SheafOfModules.nonvanishingLocus
          (X := (AlgebraicGeometry.Proj 𝒮).toRingedSpace)
          (twistingSheaf 𝒮 ((n * d : ℕ) : ℤ))
          (sectionsOfTop _ (degreeSection 𝒮 (n * d) f)) ∩
        (whereInvertible 𝒮 d : Set ↥(AlgebraicGeometry.Proj 𝒮)) =
      (AlgebraicGeometry.Proj.basicOpen 𝒮 (f : S) : Set ↥(AlgebraicGeometry.Proj 𝒮)) ∩
        (whereInvertible 𝒮 d : Set ↥(AlgebraicGeometry.Proj 𝒮))
Tag 01MW, a lemma

Tag 01MW in the Stacks Project.

Stacks.AlgebraicGeometry.CommonDegreeTwist.exists_degree_forall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CommonDegreeTwist/AffineSectionBasis.lean, line 285. The attribute's comment: “degree_exists”.

Stacks Tag 01MW. Let S be a graded ring, X = Proj(S) and Y ⊆ X a quasi-compact open subscheme; write 𝒪_Y(n) for the restriction of 𝒪_X(n) to Y. Then there is an integer d ≥ 1 such that

  1. Y is contained in the open W_d of Tag 01MU;
  2. 𝒪_Y(dn) is invertible for every n : ℤ;
  3. every multiplication map 𝒪_Y(nd) ⊗_{𝒪_Y} 𝒪_Y(m) ⟶ 𝒪_Y(nd + m) of Equation 01MO is an isomorphism;
  4. every comparison map M̃|_Y ⊗_{𝒪_Y} 𝒪_Y(nd) ⟶ M(nd)~|_Y of Equation 01MQ is an isomorphism, for every graded S-module M;
  5. for f ∈ S_{nd} with image s ∈ Γ(Y, 𝒪_Y(nd)) the nonvanishing locus Y_s is D₊(f) ∩ Y;
  6. the opens Y_s, for s ∈ Γ(Y, 𝒪_Y(nd)) with n ≥ 1, form a basis for the topology of Y;
  7. so do those among them which are affine.

The degree is the common degree of a finite standard-open cover of Y, which quasi-compactness produces: AlgebraicGeometry.Proj.commonDegreeCover. Each clause is then the corresponding result about such a cover, so all seven hold for that one degree.

theorem exists_degree_forall (Y : (AlgebraicGeometry.Proj 𝒮).Opens)
    (hY : IsCompact (Y : Set (AlgebraicGeometry.Proj 𝒮))) :
    ∃ d : ℕ, 1 ≤ d ∧
      Y ≤ whereInvertible 𝒮 d ∧
      (∀ n : ℤ, SheafOfModules.IsInvertible Y.toScheme.presheaf Y.toScheme.ringCatSheaf.2
        ((Scheme.Modules.pullback Y.ι).obj (twistingSheaf 𝒮 ((d : ℤ) * n)))) ∧
      (∀ n m : ℤ, IsIso ((Scheme.Modules.restrictFunctor Y.ι).map
        (twistMultiplicationMap 𝒮 ((d : ℤ) * n) m))) ∧
      (∀ (M : Type u) [AddCommGroup M] [Module S M] (τ : Type t) [SetLike τ M]
        [AddSubgroupClass τ M] (𝒨 : ℤ → τ) [DirectSum.Decomposition 𝒨]
        [SetLike.GradedSMul 𝒮 𝒨] (n : ℤ),
          IsIso ((Scheme.Modules.restrictFunctor Y.ι).map
            (Stacks.AlgebraicGeometry.ProjShifted.moduleTwistMap 𝒮 𝒨 ((d : ℤ) * n)))) ∧
      (∀ (n : ℕ) (f : 𝒮 (n * d)),
        Stacks.Ample.nonvanishingLocus (restrictedTwist 𝒮 Y ((n * d : ℕ) : ℤ))
            (restrictedDegreeSection 𝒮 Y (n * d) f) =
          ((Y.ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒮 (f : S) : Y.toScheme.Opens) :
            Set Y.toScheme)) ∧
      Opens.IsBasis {V : Y.toScheme.Opens | ∃ n : ℕ, 1 ≤ n ∧
        ∃ s : Γ(restrictedTwist 𝒮 Y ((n * d : ℕ) : ℤ), ⊤),
          (V : Set Y.toScheme) =
            Stacks.Ample.nonvanishingLocus (restrictedTwist 𝒮 Y ((n * d : ℕ) : ℤ)) s} ∧
      Opens.IsBasis {V : Y.toScheme.Opens | ∃ n : ℕ, 1 ≤ n ∧
        ∃ s : Γ(restrictedTwist 𝒮 Y ((n * d : ℕ) : ℤ), ⊤),
          IsAffineOpen V ∧ (V : Set Y.toScheme) =
            Stacks.Ample.nonvanishingLocus (restrictedTwist 𝒮 Y ((n * d : ℕ) : ℤ)) s}
Tag 0B5I, a lemma

Tag 0B5I in the Stacks Project.

Stacks.AlgebraicGeometry.ProjTwistIntegerComparisonStatement.comparison_existsUnique_functorial_degreeZeroId, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TensorSectionNonvanishing/ProjTwistIntegerComparisonStatement.lean, line 82. The attribute's comment: “the tag's three assertions in one statement, for the canonical graded-module structure on M = ⨁_{n ∈ ℤ} Γ(X, ℱ(n)): the comparison morphism M̃ ⟶ ℱ exists and is the unique morphism restricting on each positive-degree standard open to m / f ^ k ↦ m|_{D₊(f)} ⊗ f ^ (-k), it commutes with every morphism of sheaves of modules out of ℱ, and it returns each global section of ℱ to itself through the identification ℱ(0) ≅ ℱ”. References: EGA II (2.6.4), “more general”.

Let S be a graded ring, X = Proj S, let ℱ be a sheaf of 𝒪_X-modules and let M = ⨁_{n ∈ ℤ} Γ(X, ℱ(n)) be the graded S-module of twisted global sections, taken with its canonical graded-module structure Stacks.AlgebraicGeometry.ProjTwistedSections.twistedGlobalSectionsModule. Then there is a canonical 𝒪_X-module map M̃ ⟶ ℱ, functorial in ℱ, whose induced map M₀ → Γ(X, ℱ) is the identity.

The three conjuncts are, in order:

  1. Existence and canonicity. There is exactly one morphism M̃ ⟶ ℱ whose restriction to the standard open D₊(f) of each positive-degree homogeneous element is the chart comparison m / f ^ k ↦ m|_{D₊(f)} ⊗ f ^ (-k). The morphism it names is Stacks.AlgebraicGeometry.ProjTwistIntegerComparison.integerComparison.
  2. Functoriality in ℱ. For every sheaf 𝒢 and every morphism ψ : ℱ ⟶ 𝒢, the comparison morphisms of ℱ and of 𝒢 form a commuting square with ψ and with the morphism of associated sheaves that ψ induces on the graded modules of twisted global sections.
  3. The degree-zero map is the identity. A global section t of ℱ is a degree-zero element of M through the identification ℱ(0) ≅ ℱ of Stacks.AlgebraicGeometry.ProjTwistDegreeZeroNormalization.twistZeroCancelIso; the global section of M̃ attached to it is sent by the comparison morphism back to t.
theorem comparison_existsUnique_functorial_degreeZeroId
    (F : SheafOfModules.{u} (projRingSheaf 𝒮)) :
    (∃! φ : twistedGlobalSectionsAssociatedSheaf 𝒮 F (twistedGlobalSectionsModule 𝒮 F) ⟶ F,
        ∀ p : PositiveElem 𝒮,
          φ.val.app (op (positiveBasicOpen 𝒮 p)) =
            localComparison 𝒮 F (twistedGlobalSectionsModule 𝒮 F) p) ∧
      (∀ (G : SheafOfModules.{u} (projRingSheaf 𝒮)) (ψ : F ⟶ G),
          twistedGlobalSectionsAssociatedSheafMap 𝒮 (twistedGlobalSectionsModule 𝒮 F)
                (twistedGlobalSectionsModule 𝒮 G) ψ ≫
              integerComparison 𝒮 G (twistedGlobalSectionsModule 𝒮 G) =
            integerComparison 𝒮 F (twistedGlobalSectionsModule 𝒮 F) ≫ ψ) ∧
      (letI := (twistedGlobalSectionsModule 𝒮 F).moduleInst
       letI := (twistedGlobalSectionsModule 𝒮 F).gradedSMul
       ∀ t : F.val.obj (op (⊤ : Opens (ProjectiveSpectrum.top 𝒮))),
        (integerComparison 𝒮 F (twistedGlobalSectionsModule 𝒮 F)).val.app
            (op (⊤ : Opens (ProjectiveSpectrum.top 𝒮)))
            (degreeZeroToGlobalSections 𝒮 (twistedGlobalSectionsGrading 𝒮 F)
              ⟨DirectSum.of (fun k : ℤ => twistedSectionsComponent 𝒮 F k) 0
                  ((twistZeroCancelIso 𝒮 F (rfl : (0 : ℤ) = 0)).inv.val.app
                    (op (⊤ : Opens (ProjectiveSpectrum.top 𝒮))) t),
                (DirectSum.mem_rangeGrading ℤ (fun k : ℤ => twistedSectionsComponent 𝒮 F k) 0
                  _).mpr ⟨_, rfl⟩⟩) = t)
Sources
LeanStacks.ProjectiveCohomology.coe_sectionsTwistEquivAwayGrading_smul · AlgebraicGeometry.ProjectiveSpectrum.Proj.twistingSheaf · AlgebraicGeometry.ProjectiveSpectrum.Proj.twistSheafOfModules · Stacks.AlgebraicGeometry.ProjTwistAwayPiece.coe_sectionsTwistEquivGradedPiece_smul · twistMultiplicationMap · AlgebraicGeometry.ProjectiveSpectrum.Proj.twistSheafMultiplicationMap · AlgebraicGeometry.ProjectiveSpectrum.Proj.globalSectionsRingMap · Stacks.AlgebraicGeometry.ProjTwistSectionRing.globalSectionsRingMap

Section27.11 Functoriality of Proj#

Section 27.11 of the Stacks Project, Tag 01MX. 8 tags here are carried by 28 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01MY, a lemma

Tag 01MY in the Stacks Project.

Stacks.AlgebraicGeometry.ProjMapCard.projMapData_preserves_products, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjMapCard/Multiplication.lean, line 345. The attribute's comment: “graded-algebra multiplication”.

Tag 01MY, graded-algebra multiplication, on the canonical bundle. The tagged statement's spelling of twistMap_comp_pullbackTwistMultiplication: the morphism and the twist maps are the fields of Stacks.AlgebraicGeometry.ProjTwistCompare.projMapData.

public theorem projMapData_preserves_products (ψ : 𝒜 →+*ᵍ ℬ)
    (n m : ℤ) :
    pullbackTwistMultiplication 𝒜 (projMapData 𝒜 ℬ ψ).hom n m ≫
      (projMapData 𝒜 ℬ ψ).twistMap (n + m) =
    ((Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor.{u, u, u, u, u}
      ⟨(((mapDomain 𝒜 ℬ ψ).toScheme.toRingedSpace)).presheaf,
      (((mapDomain 𝒜 ℬ ψ).toScheme.toRingedSpace)).IsSheaf⟩)).map
      ((((projMapData 𝒜 ℬ ψ).twistMap n), ((projMapData 𝒜 ℬ ψ).twistMap m)) : (_, _) ⟶ (_, _))) ≫
      pullbackTwistMultiplication ℬ (mapDomain 𝒜 ℬ ψ).ι n m

Stacks.AlgebraicGeometry.ProjMapCardUnit.projMapData_preserves_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjMapCardUnit/Basic.lean, line 332. The attribute's comment: “graded-algebra unit”.

Tag 01MY, the graded-algebra unit, on the canonical bundle. The Stacks statement's spelling of twistMap_comp_pullbackTwistUnit: the morphism and the twist maps are the fields of Stacks.AlgebraicGeometry.ProjTwistCompare.projMapData.

theorem projMapData_preserves_unit (ψ : 𝒜 →+*ᵍ ℬ) :
    pullbackTwistUnit 𝒜 (projMapData 𝒜 ℬ ψ).hom ≫ (projMapData 𝒜 ℬ ψ).twistMap 0 =
      pullbackTwistUnit ℬ (mapDomain 𝒜 ℬ ψ).ι

Stacks.AlgebraicGeometry.ProjTwistChain.awayToSection_comp_appLE_mapHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjMapData/Basic.lean, line 165. The attribute's comment: “part (2), localization map on standard opens”.

Stacks 01MY (2): on the standard open D₊(ψ f) of the domain of definition, the morphism induced by ψ is the one induced by the map 𝒜_{(f)} → ℬ_{(ψ f)} of degree-zero homogeneous localizations.

With no hypothesis on ψ; compare AlgebraicGeometry.Proj.awayToSection_comp_appLE, which states this for AlgebraicGeometry.Proj.map and so assumes ℬ₊ ≤ 𝒜₊.map ψ.

public theorem awayToSection_comp_appLE_mapHom (ψ : 𝒜 →+*ᵍ ℬ) (f : A) (d : ℕ) (hf : f ∈ 𝒜 d)
    (hd : 0 < d) :
    Proj.awayToSection 𝒜 f ≫
      Scheme.Hom.appLE (mapHom 𝒜 ℬ ψ) (Proj.basicOpen 𝒜 f)
        ((mapDomain 𝒜 ℬ ψ).ι ⁻¹ᵁ Proj.basicOpen ℬ (ψ f))
        (by rw [mapHom_preimage_basicOpen 𝒜 ℬ ψ f d hf hd]) =
    CommRingCat.ofHom (Away.map ψ f) ≫
      Proj.awayToSection ℬ (ψ f) ≫
        Scheme.Hom.appLE (mapDomain 𝒜 ℬ ψ).ι (Proj.basicOpen ℬ (ψ f))
          ((mapDomain 𝒜 ℬ ψ).ι ⁻¹ᵁ Proj.basicOpen ℬ (ψ f)) le_rfl

Stacks.AlgebraicGeometry.ProjTwistChain.eq_mapHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjMapData/Basic.lean, line 182. The attribute's comment: “uniqueness of the scheme morphism”.

Stacks 01MY (2), uniqueness: a morphism out of the domain of definition that has the inverse images of standard opens of Tag 01MY (2), and that on each of them is induced by the corresponding map of degree-zero homogeneous localizations, is mapHom.

public theorem eq_mapHom (ψ : 𝒜 →+*ᵍ ℬ)
    (p : (mapDomain 𝒜 ℬ ψ).toScheme ⟶ AlgebraicGeometry.Proj 𝒜)
    (hopen : ∀ (f : A) (d : ℕ), f ∈ 𝒜 d → 0 < d →
      p ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜 f =
        (mapDomain 𝒜 ℬ ψ).ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen ℬ (ψ f))
    (hlocal : ∀ (f : A) (d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d),
      Proj.awayToSection 𝒜 f ≫
        Scheme.Hom.appLE p (Proj.basicOpen 𝒜 f)
          ((mapDomain 𝒜 ℬ ψ).ι ⁻¹ᵁ Proj.basicOpen ℬ (ψ f))
          (by rw [hopen f d hf hd]) =
      CommRingCat.ofHom (Away.map ψ f) ≫
        Proj.awayToSection ℬ (ψ f) ≫
          Scheme.Hom.appLE (mapDomain 𝒜 ℬ ψ).ι (Proj.basicOpen ℬ (ψ f))
            ((mapDomain 𝒜 ℬ ψ).ι ⁻¹ᵁ Proj.basicOpen ℬ (ψ f)) le_rfl) :
    p = mapHom 𝒜 ℬ ψ

Stacks.AlgebraicGeometry.ProjMapUniqueTwist.projMapData_twistMap_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjMapUniqueTwist/Basic.lean, line 282. The attribute's comment: “uniqueness of the graded-algebra map”.

Tag 01MY, uniqueness of the graded-algebra map. A bundle of the canonical morphism with maps on all twists which satisfies condition (1) at ⊤, the multiplication law in all integer degrees and the unit law is the canonical bundle.

Together with Stacks.AlgebraicGeometry.ProjMapData.eq_mapHom, this is uniqueness of the canonical triple of Tag 01MY.

public theorem projMapData_twistMap_unique (𝒜 : ℕ → σ) (ℬ : ℕ → τ) [GradedRing 𝒜] [GradedRing ℬ]
    (ψ : 𝒜 →+*ᵍ ℬ) (D : ProjMapData 𝒜 ℬ ψ)
    (hh : D.hom = (projMapData 𝒜 ℬ ψ).hom)
    (hdegree : ∀ (n : ℕ) (a : 𝒜 n),
      (D.twistMap (n : ℤ)).val.app (.op ⊤)
        (((Scheme.Modules.pullbackPushforwardAdjunction D.hom).unit.app
          (twistingSheaf 𝒜 (n : ℤ))).val.app (.op ⊤)
            (degreeSection 𝒜 n a)) =
      ((Scheme.Modules.pullbackPushforwardAdjunction (mapDomain 𝒜 ℬ ψ).ι).unit.app
        (twistingSheaf ℬ (n : ℤ))).val.app (.op ⊤)
          (degreeSection ℬ n ⟨ψ a, ψ.map_mem a.2⟩))
    (hmul : ∀ n m : ℤ,
      pullbackTwistMultiplication 𝒜 D.hom n m ≫ D.twistMap (n + m) =
      ((Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor ⟨(((mapDomain 𝒜 ℬ
        ψ).toScheme.toRingedSpace)).presheaf, (((mapDomain 𝒜 ℬ
        ψ).toScheme.toRingedSpace)).IsSheaf⟩)).map
          (((D.twistMap n), (D.twistMap m)) : (_, _) ⟶ (_, _))) ≫
        pullbackTwistMultiplication ℬ (mapDomain 𝒜 ℬ ψ).ι n m)
    (hunit : pullbackTwistUnit 𝒜 D.hom ≫ D.twistMap 0 =
      pullbackTwistUnit ℬ (mapDomain 𝒜 ℬ ψ).ι) :
    D = projMapData 𝒜 ℬ ψ

Stacks.AlgebraicGeometry.ProjShared.mapDomain, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjShared/MapDomain.lean, line 89. The attribute's comment: “the open domain”. References: EGA II (2.8.1); EGA II (3.5.6), “partial”.

The union of the standard opens D₊(ψ f) of Proj ℬ for f homogeneous of positive degree: the largest open on which a graded ring homomorphism ψ induces a morphism to Proj 𝒜.

public def mapDomain (ψ : 𝒜 →+*ᵍ ℬ) : (Proj ℬ).Opens

Stacks.AlgebraicGeometry.ProjTwistChain.mapHom_preimage_basicOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjTwistChain/MY.lean, line 248. The attribute's comment: “part (2), inverse images of standard opens”. References: EGA II (2.8.1).

Stacks 01MY (2): the inverse image of a standard open of Proj 𝒜 under the induced morphism is the standard open of the image element.

public theorem mapHom_preimage_basicOpen (ψ : 𝒜 →+*ᵍ ℬ) (f : A) (d : ℕ) (hf : f ∈ 𝒜 d)
    (hd : 0 < d) :
    mapHom 𝒜 ℬ ψ ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜 f =
      (mapDomain 𝒜 ℬ ψ).ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen ℬ (ψ f)

Stacks.AlgebraicGeometry.ProjTwistCompare.projMapData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjTwistCompare/Twist.lean, line 356. The attribute's comment: “the morphism and the maps on all twists”.

The canonical bundle of Tag 01MY: the glued morphism mapHom together with the comparison maps θ on all twists.

public def projMapData (ψ : 𝒜 →+*ᵍ ℬ) : ProjMapData 𝒜 ℬ ψ

Stacks.AlgebraicGeometry.ProjTwistGradedAlgebra.thetaGraded, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjTwistGradedAlgebra/Basic.lean, line 198. The attribute's comment: “theta as a single morphism of sheaves of Z-graded algebras: the comparison maps on all integer twists, assembled into one morphism from the pullback along r_psi of the graded algebra of integer twists of Proj A to the pullback along the inclusion of U(psi) of that of Proj B”.

The comparison maps on all integer twists, as one homomorphism of sheaves of ℤ-graded algebras θ : r_ψ^*(⨁_{n ∈ ℤ} 𝒪_{Proj 𝒜}(n)) ⟶ ⨁_{n ∈ ℤ} 𝒪_{Proj ℬ}(n)|_{U(ψ)}. Its degree-n component is Stacks.AlgebraicGeometry.ProjTwistCompare.twistMap.

def thetaGraded (ψ : 𝒜 →+*ᵍ ℬ) :
    pullbackTwistAlgebra 𝒜 (mapHom 𝒜 ℬ ψ) ⟶
      pullbackTwistAlgebra ℬ (mapDomain 𝒜 ℬ ψ).ι

Stacks.AlgebraicGeometry.ProjTwistTheta.twistMap_degreeSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjTwistTheta/DegreeSection.lean, line 225. The attribute's comment: “part (1), homogeneous global sections”.

Tag 01MY, part (1), homogeneous global sections. The comparison map on the n-th twist carries the global section of O(n) attached to a homogeneous element a of degree n to the global section attached to psi a, both read through the unit of the pullback--pushforward adjunction.

public theorem twistMap_degreeSection (ψ : 𝒜 →+*ᵍ ℬ) (n : ℕ) (a : 𝒜 n) :
    ((projMapData 𝒜 ℬ ψ).twistMap (n : ℤ)).val.app (.op ⊤)
      (((Scheme.Modules.pullbackPushforwardAdjunction (projMapData 𝒜 ℬ ψ).hom).unit.app
        (twistingSheaf 𝒜 (n : ℤ))).val.app (.op ⊤)
          (degreeSection 𝒜 n a)) =
    ((Scheme.Modules.pullbackPushforwardAdjunction (mapDomain 𝒜 ℬ ψ).ι).unit.app
      (twistingSheaf ℬ (n : ℤ))).val.app (.op ⊤)
        (degreeSection ℬ n ⟨ψ a, ψ.map_mem a.2⟩)
Tag 01MZ, a lemma

Tag 01MZ in the Stacks Project.

Stacks.AlgebraicGeometry.ProjTwistCompTwistMap.mapDomain_mapHom_twistMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjTwistCompTwistMap/Statement.lean, line 100. The attribute's comment: “the tag's three assertions in one statement, for an arbitrary composable pair of homomorphisms of nonnegatively graded rings: the domain of definition of the composite is the inverse image under r_ψ of the domain of definition of φ, the morphism of the composite is r_φ ∘ r_ψ restricted to that open, and the comparison maps on every twist compose”. References: EGA II (2.8.4).

[Stacks, Tag 01MZ]. Let 𝒜, ℬ, 𝒞 be nonnegatively graded rings, write X = Proj 𝒜, Y = Proj ℬ, Z = Proj 𝒞, and let φ : 𝒜 →+*ᵍ ℬ and ψ : ℬ →+*ᵍ 𝒞 be homomorphisms of graded rings. Then U(ψ ∘ φ) = r_ψ⁻¹(U(φ)), the morphism r_{ψ ∘ φ} : U(ψ ∘ φ) ⟶ X is r_φ ∘ r_ψ|_{U(ψ ∘ φ)}, and θ_ψ ∘ r_ψ^* θ_φ = θ_{ψ ∘ φ} on every twist.

The three conjuncts are, in order:

  1. The domain of definition of the composite. U(ψ ∘ φ), an open of Z, is the image under the inclusion of U(ψ) of the open r_ψ⁻¹(U(φ)) of U(ψ). This is mapDomain_comp.
  2. The morphism of the composite. Read through the canonical isomorphism mapDomainCompIso : r_ψ⁻¹(U(φ)) ≅ U(ψ ∘ φ) that the first conjunct supplies, r_{ψ ∘ φ} is the restriction r_ψ|_{r_ψ⁻¹(U(φ))} : r_ψ⁻¹(U(φ)) ⟶ U(φ) followed by r_φ. This is mapDomainCompIso_hom_mapHom.
  3. The comparison maps on the twists. For every n : ℤ, Tag 01MY's comparison θ_{ψ ∘ φ} on the n-th twist, pulled back along the canonical isomorphism, is θ_φ pulled back along r_ψ|_{r_ψ⁻¹(U(φ))} followed by θ_ψ pulled back along the inclusion of r_ψ⁻¹(U(φ)), the pseudofunctoriality isomorphisms of the inverse image and the three identifications of composites of the first two conjuncts mediating between the two sides. This is twistMap_comp.

The source's data are the three graded rings and the two homomorphisms, and those are the only binders here: every domain of definition is an arbitrary open, and θ is Tag 01MY's comparison for an arbitrary homomorphism of nonnegatively graded rings.

public theorem mapDomain_mapHom_twistMap_comp (φ : 𝒜 →+*ᵍ ℬ) (ψ : ℬ →+*ᵍ 𝒞) :
    mapDomain 𝒜 𝒞 (ψ.comp φ) =
        (mapDomain ℬ 𝒞 ψ).ι ''ᵁ (mapHom ℬ 𝒞 ψ ⁻¹ᵁ mapDomain 𝒜 ℬ φ) ∧
      (mapDomainCompIso 𝒜 ℬ 𝒞 φ ψ).hom ≫ mapHom 𝒜 𝒞 (ψ.comp φ) =
        (mapHom ℬ 𝒞 ψ ∣_ mapDomain 𝒜 ℬ φ) ≫ mapHom 𝒜 ℬ φ ∧
      ∀ n : ℤ,
        (Scheme.Modules.pullbackComp (mapDomainCompIso 𝒜 ℬ 𝒞 φ ψ).hom
              (mapHom 𝒜 𝒞 (ψ.comp φ))).inv.app (twistingSheaf 𝒜 n) ≫
            (Scheme.Modules.pullback (mapDomainCompIso 𝒜 ℬ 𝒞 φ ψ).hom).map
              (twistMap 𝒜 𝒞 (ψ.comp φ) n) ≫
            (Scheme.Modules.pullbackComp (mapDomainCompIso 𝒜 ℬ 𝒞 φ ψ).hom
              (mapDomain 𝒜 𝒞 (ψ.comp φ)).ι).hom.app (twistingSheaf 𝒞 n) =
          (Scheme.Modules.pullbackCongr
              (mapDomainCompIso_hom_mapHom 𝒜 ℬ 𝒞 φ ψ)).hom.app (twistingSheaf 𝒜 n) ≫
            (Scheme.Modules.pullbackComp (mapHom ℬ 𝒞 ψ ∣_ mapDomain 𝒜 ℬ φ)
              (mapHom 𝒜 ℬ φ)).inv.app (twistingSheaf 𝒜 n) ≫
            (Scheme.Modules.pullback (mapHom ℬ 𝒞 ψ ∣_ mapDomain 𝒜 ℬ φ)).map
              (twistMap 𝒜 ℬ φ n) ≫
            (Scheme.Modules.pullbackComp (mapHom ℬ 𝒞 ψ ∣_ mapDomain 𝒜 ℬ φ)
              (mapDomain 𝒜 ℬ φ).ι).hom.app (twistingSheaf ℬ n) ≫
            (Scheme.Modules.pullbackCongr
              (morphismRestrict_ι (mapHom ℬ 𝒞 ψ) (mapDomain 𝒜 ℬ φ))).hom.app
                (twistingSheaf ℬ n) ≫
            (Scheme.Modules.pullbackComp (mapHom ℬ 𝒞 ψ ⁻¹ᵁ mapDomain 𝒜 ℬ φ).ι
              (mapHom ℬ 𝒞 ψ)).inv.app (twistingSheaf ℬ n) ≫
            (Scheme.Modules.pullback (mapHom ℬ 𝒞 ψ ⁻¹ᵁ mapDomain 𝒜 ℬ φ).ι).map
              (twistMap ℬ 𝒞 ψ n) ≫
            (Scheme.Modules.pullbackComp (mapHom ℬ 𝒞 ψ ⁻¹ᵁ mapDomain 𝒜 ℬ φ).ι
              (mapDomain ℬ 𝒞 ψ).ι).hom.app (twistingSheaf 𝒞 n) ≫
            (Scheme.Modules.pullbackCongr
              (mapDomainCompIso_hom_ι 𝒜 ℬ 𝒞 φ ψ)).inv.app (twistingSheaf 𝒞 n)
Tag 01N0, a lemma

Tag 01N0 in the Stacks Project.

AlgebraicGeometry.ProjectiveSpectrum.Proj.pullbackGlobalSections_degreeSection_eq_zero_iff_degreeSection_map_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjSaturation/QuotientComparison.lean, line 250. The attribute's comment: “part (3), the comparison θ : r_ψ^* 𝒪_X(n) ⟶ 𝒪_Y(n) on the canonical twisted sections: for ψ surjective out of a Noetherian graded ring generated in degree one, θ is injective on them, so the pulled-back section of a ∈ 𝒮 n vanishes iff the section of ψ a does. Surjectivity of θ is twist_surjective; sheaf-level isomorphy of θ, and the source's counterexample to it, are not proved.”.

Tag 01N0 part (3) on canonical twisted sections, for a surjective homomorphism of graded rings out of a Noetherian ring generated in degree one. Write X = Proj 𝒮, Y = Proj ℬ and r = r_ψ : Y ⟶ X for the closed immersion of part (2). For a ∈ 𝒮 n, the pullback along r of the canonical section of 𝒪_X(n) attached to a vanishes exactly when the canonical section of 𝒪_Y(n) attached to ψ a vanishes.

The source's part (3) says the comparison maps θ : r^* 𝒪_X(n) ⟶ 𝒪_Y(n) of Tag 01MY are surjective but in general not injective, even for a surjective ψ; its counterexample is 𝒮 = k[x, y] with deg x = 1, deg y = 2 and Ker ψ = (x). The statement here is that θ is injective on the canonical sections once 𝒮 is generated in degree one — the hypothesis the counterexample violates. Surjectivity of θ is Stacks.AlgebraicGeometry.ProjTwistEpi.epi_projMapData_twistMap_of_eventually_surjective.

Both sides are the saturation of Ker ψ: the left by mem_idealOfClosedSubscheme_map_iff and the right by AlgebraicGeometry.ProjectiveSpectrum.Proj.degreeSection_eq_zero_iff on ℬ, which inherits Noetherianness and degree-one generation from 𝒮 along ψ.

theorem pullbackGlobalSections_degreeSection_eq_zero_iff_degreeSection_map_eq_zero
    [IsNoetherianRing S] (hψ : Function.Surjective ψ)
    (hgen : Algebra.adjoin (𝒮 0) (𝒮 1 : Set S) = ⊤) {n : ℕ} (b : 𝒮 n) :
    pullbackGlobalSections (Proj.map ψ hq) (twistingSheaf 𝒮 (n : ℤ))
          (degreeSection 𝒮 n b) = 0 ↔
      degreeSection ℬ n ⟨ψ (b : S), ψ.map_mem b.2⟩ = 0

Stacks.AlgebraicGeometry.ProjTwistEpi.epi_projMapData_twistMap_of_eventually_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjTwistEpi/Basic.lean, line 201. The attribute's comment: “twist_surjective”.

If ψ is surjective on homogeneous components of all sufficiently large degree, then the twist maps of the bundle projMapData 𝒜 ℬ ψ are epimorphisms of sheaves of modules.

public theorem epi_projMapData_twistMap_of_eventually_surjective (ψ : 𝒜 →+*ᵍ ℬ)
    (hψ : ∀ᶠ d : ℕ in atTop, Function.Surjective (GradedRingHom.gradedAddHom ψ d))
    (n : ℤ) : Epi ((projMapData 𝒜 ℬ ψ).twistMap n)

Stacks.AlgebraicGeometry.RelativeProjChain.mapDomain_eq_top_of_eventually_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjChain/EventualSurjective.lean, line 155. The attribute's comment: “domain”.

Stacks 01N1 (1): a graded ring homomorphism surjective in all sufficiently large degrees is defined on the whole of Proj ℬ.

A point of Proj ℬ omits some homogeneous g of positive degree m; a large power g ^ k is homogeneous of degree k * m, is still omitted because the point is prime, and is in the image of ψ.

public theorem mapDomain_eq_top_of_eventually_surjective (ψ : 𝒜 →+*ᵍ ℬ)
    (hψ : ∀ᶠ d : ℕ in atTop, Function.Surjective (GradedRingHom.gradedAddHom ψ d)) :
    mapDomain 𝒜 ℬ ψ = ⊤

Stacks.AlgebraicGeometry.RelativeProjChain.isClosedImmersion_projMapData_hom_of_eventually_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjChain/EventualSurjective.lean, line 223. The attribute's comment: “closed_immersion”.

Stacks 01N1 (2) on Tag 01MY's bundle: the underlying morphism of Stacks.AlgebraicGeometry.ProjTwistCompare.projMapData is a closed immersion. This is the form the statements of the chain quantify over, and it is the previous result unchanged, since the bundle's morphism is mapHom by definition.

public theorem isClosedImmersion_projMapData_hom_of_eventually_surjective (ψ : 𝒜 →+*ᵍ ℬ)
    (hψ : ∀ᶠ d : ℕ in atTop, Function.Surjective (GradedRingHom.gradedAddHom ψ d)) :
    IsClosedImmersion (ProjTwistCompare.projMapData 𝒜 ℬ ψ).hom

Stacks.AlgebraicGeometry.RelativeProjChain.isClosedImmersion_projToProjectiveSpaceGradeZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjChain/PolynomialSurjection.lean, line 233. The attribute's comment: “part (2) at a polynomial ring: closed immersion into ℙⁿ”. References: EGA II (2.9.5), “special case”.

Stacks Tag 01N0 at a polynomial ring: a graded ring generated in degree one by n + 1 elements is a closed subscheme of ℙⁿ. Let S be a graded ring and let x_0, …, x_n ∈ S_1 generate S as an S_0-algebra. Then the induced morphism Proj S ⟶ ℙⁿ_{S_0} = Proj S_0[T_0, …, T_n] is a closed immersion.

This is the source's hypothesis "S is generated by S_1 over S_0" together with a choice of n + 1 generators, and it is isClosedImmersion_projToProjectiveSpace with R = S_0 and the inclusion of the degree-zero part as the structure map.

theorem isClosedImmersion_projToProjectiveSpaceGradeZero (x : Fin (n + 1) → S)
    (hx : ∀ i, x i ∈ 𝒮 1) (hgen : Algebra.adjoin (𝒮 0) (Set.range x) = ⊤) :
    IsClosedImmersion
      (projToProjectiveSpace 𝒮 (R := (𝒮 0)) (fun r => r.2) x hx hgen)
Tag 07ZE, a lemma

Tag 07ZE in the Stacks Project.

Stacks.AlgebraicGeometry.RelativeProjChain.mapDomain_eq_top_of_eventually_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjChain/EventualBijective.lean, line 166. The attribute's comment: “part (1), the domain is all of Proj B”.

Stacks 07ZE (1): a graded homomorphism bijective in all large degrees is defined on all of Proj ℬ. Only surjectivity is used, so this is Stacks 01N1's first assertion.

public theorem mapDomain_eq_top_of_eventually_bijective (ψ : 𝒜 →+*ᵍ ℬ)
    (hψ : ∀ᶠ d : ℕ in atTop, Function.Bijective (GradedRingHom.gradedAddHom ψ d)) :
    mapDomain 𝒜 ℬ ψ = ⊤

Stacks.AlgebraicGeometry.RelativeProjChain.isIso_projMapData_hom_of_eventually_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjChain/EventualBijective.lean, line 197. The attribute's comment: “part (2), the projective-spectrum morphism is an isomorphism”.

Stacks 07ZE (2) on Tag 01MY's bundle: the underlying morphism of Stacks.AlgebraicGeometry.ProjTwistCompare.projMapData is an isomorphism. This is the form the statements of the chain quantify over, and it is the previous result unchanged, since the bundle's morphism is mapHom by definition.

public theorem isIso_projMapData_hom_of_eventually_bijective (ψ : 𝒜 →+*ᵍ ℬ)
    (hψ : ∀ᶠ d : ℕ in atTop, Function.Bijective (GradedRingHom.gradedAddHom ψ d)) :
    IsIso (ProjTwistCompare.projMapData 𝒜 ℬ ψ).hom

Stacks.AlgebraicGeometry.RelativeProjChain.isIso_projMapData_twistMap_of_eventually_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjChain/EventualBijective.lean, line 383. The attribute's comment: “part (3), the maps on twists are isomorphisms”.

Stacks 07ZE (3): a graded homomorphism bijective in all large degrees makes Tag 01MY's comparison map on the n-th twist an isomorphism, for every n : ℤ.

The map is an epimorphism by Stacks 01N0, and a monomorphism because its adjoint form is injective on sections and the unit of the adjunction is an isomorphism by assertion (2).

public theorem isIso_projMapData_twistMap_of_eventually_bijective (ψ : 𝒜 →+*ᵍ ℬ)
    (hψ : ∀ᶠ d : ℕ in atTop, Function.Bijective (GradedRingHom.gradedAddHom ψ d))
    (n : ℤ) :
    IsIso ((ProjTwistCompare.projMapData 𝒜 ℬ ψ).twistMap n)
Tag 01N1, a lemma

Tag 01N1 in the Stacks Project.

Stacks.AlgebraicGeometry.ProjTwistMono.isIso_projMapData_twistMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjTwistMono/Assembly.lean, line 125. The attribute's comment: “part (3): isomorphisms on all twists”.

Tag 01N1's third assertion. For a homomorphism of graded rings surjective on homogeneous components of all large degree, with the source generated in degree one over its degree-zero part, Tag 01MY's comparison map on the n-th twist is an isomorphism for every n.

theorem isIso_projMapData_twistMap (ψ : 𝒜 →+*ᵍ ℬ)
    (hψ : ∀ᶠ d : ℕ in atTop, Function.Surjective (GradedRingHom.gradedAddHom ψ d))
    (hgen : Algebra.adjoin (𝒜 0) (𝒜 1 : Set A) = ⊤) (n : ℤ) :
    IsIso ((ProjTwistCompare.projMapData 𝒜 ℬ ψ).twistMap n)

Stacks.AlgebraicGeometry.RelativeProjChain.mapDomain_eq_top_of_eventually_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjChain/EventualSurjective.lean, line 155. The attribute's comment: “part (1): the domain is all of Proj”.

Stacks 01N1 (1): a graded ring homomorphism surjective in all sufficiently large degrees is defined on the whole of Proj ℬ.

A point of Proj ℬ omits some homogeneous g of positive degree m; a large power g ^ k is homogeneous of degree k * m, is still omitted because the point is prime, and is in the image of ψ.

public theorem mapDomain_eq_top_of_eventually_surjective (ψ : 𝒜 →+*ᵍ ℬ)
    (hψ : ∀ᶠ d : ℕ in atTop, Function.Surjective (GradedRingHom.gradedAddHom ψ d)) :
    mapDomain 𝒜 ℬ ψ = ⊤

Stacks.AlgebraicGeometry.RelativeProjChain.isClosedImmersion_projMapData_hom_of_eventually_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjChain/EventualSurjective.lean, line 223. The attribute's comment: “part (2): the closed immersion”.

Stacks 01N1 (2) on Tag 01MY's bundle: the underlying morphism of Stacks.AlgebraicGeometry.ProjTwistCompare.projMapData is a closed immersion. This is the form the statements of the chain quantify over, and it is the previous result unchanged, since the bundle's morphism is mapHom by definition.

public theorem isClosedImmersion_projMapData_hom_of_eventually_surjective (ψ : 𝒜 →+*ᵍ ℬ)
    (hψ : ∀ᶠ d : ℕ in atTop, Function.Surjective (GradedRingHom.gradedAddHom ψ d)) :
    IsClosedImmersion (ProjTwistCompare.projMapData 𝒜 ℬ ψ).hom
Tag 01N2, a lemma

Tag 01N2 in the Stacks Project.

Stacks.ProjBaseChange.mapDomain_isPullback_isIso_twistMap_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ProjBaseChangeStatement.lean, line 98. The attribute's comment: “the tag's three assertions in one statement, for the base change of a graded R-algebra A along an R-algebra S: the domain of definition of the base-change homomorphism is the whole of Proj (S ⊗[R] A), the square it forms with the structure morphisms to Spec S and Spec R is a fibre product, and the comparison map on every twist is an isomorphism”.

[Stacks, Tag 01N2]. Let A be a graded R-algebra with grading 𝒜, let S be an R-algebra, write X = Proj 𝒜 and Y = Proj (S ⊗[R] 𝒜), and let ψ : a ↦ 1 ⊗ₜ a be the base-change homomorphism of graded rings. Then U(ψ) = Y, the square

Y = Proj (S ⊗[R] 𝒜) ⟶ Proj 𝒜 = X
         |                 |
         v                 v
      Spec S      ⟶     Spec R

is a fibre product, and every comparison map θ : r_ψ^* 𝒪_X(n) ⟶ 𝒪_Y(n) is an isomorphism.

The three conjuncts are, in order:

  1. The domain of definition is everything. The base-changed irrelevant ideal is generated by the images of the homogeneous elements of positive degree, so already the standard opens D₊(1 ⊗ₜ f) cover Y. This is Stacks.AlgebraicGeometry.ProjShared.mapDomain_baseChange.
  2. The square is a fibre product. The structure morphism of each projective spectrum is written as its morphism to the spectrum of the degree-zero part of its grading followed by the spectrum of the structure map of that degree-zero part. This is Stacks.ProjBaseChange.isPullback_map_Spec.
  3. The comparison maps are isomorphisms. For every n : ℤ, the canonical comparison on the n-th twist along r_ψ = AlgebraicGeometry.Proj.map ψ is an isomorphism. This is Stacks.ProjBaseChange.isIso_twistMap_includeRight.

The source's data are the graded R-algebra and the R-algebra S, and those are the only binders here; the identification of the target graded ring with the base change holds by construction, since the target is the base change.

theorem mapDomain_isPullback_isIso_twistMap_baseChange :
    mapDomain 𝒜 (grading 𝒜 S) (includeRight 𝒜 S) = ⊤ ∧
      IsPullback (map 𝒜 S)
          (Proj.toSpecZero (grading 𝒜 S) ≫ Spec.map (ofHom (algebraMap S ↥(grading 𝒜 S 0))))
          (Proj.toSpecZero 𝒜 ≫ Spec.map (ofHom (algebraMap R ↥(𝒜 0))))
          (Spec.map (ofHom (algebraMap R S))) ∧
      ∀ n : ℤ, IsIso (Stacks.ProjTwistComparison.twistMap (includeRight 𝒜 S)
        (irrelevant_le_map 𝒜 S) n)
Tag 01N3, a lemma

Tag 01N3 in the Stacks Project.

Stacks.AlgebraicGeometry.ProjShared.mapDomain_eq_top_of_isLocalizationAway, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjShared/MapDomain.lean, line 181. The attribute's comment: “the open domain”.

A graded homomorphism that presents its target as a localization of its source at a degree-zero element is everywhere defined.

A homogeneous element b of B of positive degree becomes, after multiplication by a power of the image of g, the image of some a ∈ A; that image is homogeneous of the same degree, so b lies in the ideal generated by the images of the positive-degree homogeneous elements of A. Hence the irrelevant ideal of ℬ is contained in that ideal and the standard opens D₊(ψ f) cover Proj ℬ.

The algebra structure is an arbitrary one whose structure map is ψ, which covers the structure map ψ.toRingHom.toAlgebra in particular.

This is the first assertion of Tag 01N3, U(ψ) = Y.

public theorem mapDomain_eq_top_of_isLocalizationAway (ψ : 𝒜 →+*ᵍ ℬ) (g : 𝒜 0)
    [Algebra A B] (halg : algebraMap A B = (ψ : A →+* B))
    [IsLocalization.Away (g : A) B] :
    mapDomain 𝒜 ℬ ψ = ⊤

Stacks.AlgebraicGeometry.TwistBaseChange.isOpenImmersion_mapHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TwistBaseChange/Fibre.lean, line 204. The attribute's comment: “the open immersion”.

The induced morphism of a graded localization away from a degree-zero element is an open immersion.

public theorem isOpenImmersion_mapHom (ψ : 𝒜 →+*ᵍ ℬ) {g : A} (hg : g ∈ 𝒜 0) [Algebra A B]
    (halg : (algebraMap A B : A →+* B) = ψ.toRingHom) [IsLocalization.Away g B] :
    IsOpenImmersion (mapHom 𝒜 ℬ ψ)

Stacks.AlgebraicGeometry.TwistBaseChange.opensRange_mapHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TwistBaseChange/Fibre.lean, line 269. The attribute's comment: “the inverse image of D(g)”.

For a graded ring homomorphism exhibiting B as a localization of A away from an element g of degree 0, the open immersion Proj ℬ ⟶ Proj 𝒜 identifies Proj ℬ with the inverse image of the standard open D(g) ⊆ Spec (𝒜 0) under the structure morphism AlgebraicGeometry.Proj.toSpecZero.

public theorem opensRange_mapHom (ψ : 𝒜 →+*ᵍ ℬ) {g : A} (hg : g ∈ 𝒜 0) [Algebra A B]
    (halg : (algebraMap A B : A →+* B) = ψ.toRingHom) [IsLocalization.Away g B]
    [IsOpenImmersion (mapHom 𝒜 ℬ ψ)] :
    (mapHom 𝒜 ℬ ψ).opensRange =
      Proj.toSpecZero 𝒜 ⁻¹ᵁ PrimeSpectrum.basicOpen (⟨g, hg⟩ : 𝒜 0)

Stacks.AlgebraicGeometry.TwistBaseChange.isIso_projMapData_twistMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TwistBaseChange/Iso.lean, line 290. The attribute's comment: “the maps on twists”.

If ψ presents B as the localization A_g of A at a degree-zero element g, then the comparison map θ : r_ψ^* 𝒪_X(n) → 𝒪_Y(n) of Stacks.AlgebraicGeometry.ProjTwistCompare.projMapData is an isomorphism for every n : ℤ.

public theorem isIso_projMapData_twistMap (ψ : 𝒜 →+*ᵍ ℬ) {g : A} (hg : g ∈ 𝒜 0) [Algebra A B]
    (halg : (algebraMap A B : A →+* B) = ψ.toRingHom) [IsLocalization.Away g B] (n : ℤ) :
    IsIso ((projMapData 𝒜 ℬ ψ).twistMap n)
Tag 0B5J, a lemma

Tag 0B5J in the Stacks Project.

Stacks.Veronese.tag0B5J, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjVeroneseStatement.lean, line 157. The attribute's comment: “the canonical isomorphism i : Proj S to Proj S^(d) induced by the inclusion S^(d) in S, described on homogeneous primes and on the standard opens D+(f) = Spec S_(f); assertion (1), the canonical isomorphism from the sheaf of a graded S-module M, in any universe, to the pullback of the sheaf of M^(d), described on the standard opens; assertion (2), the isomorphisms O_X(nd) to i^* O_X'(n) obtained from (1) at M = S(nd); and the compatibility of these isomorphisms with the multiplication maps of associated sheaves (through the comparison map from M^(d) tensor N^(d) to (M tensor N)^(d)), with the multiplication of twists, with the maps O(n) tensor F(m) to F(n+m) and M~ tensor O(n) to M(n)~, with the maps from S and from M to twisted global sections, and with the products of twisted global sections”. References: EGA II (8.14.13), “partial”.

[Stacks, Tag 0B5J]. Let S be a graded ring and d ≥ 1. Set S' = S⁽ᵈ⁾, X = Proj S and X' = Proj S'. There is a canonical isomorphism i : X ⟶ X' of schemes such that (1) for any graded S-module M, setting M' = M⁽ᵈ⁾, there is a canonical isomorphism M̃ ≅ i^*(M'~), and (2) there are canonical isomorphisms 𝒪_X(nd) ≅ i^*𝒪_{X'}(n); and these isomorphisms are compatible with the multiplication maps of Tag 01MK and hence with the maps of Tags 01MO, 03GJ, 01MP, 03GK, 01MQ and 01MR.

The isomorphism i is Stacks.Veronese.veroneseProjIso 𝒮 d hd, glued from the chart isomorphisms; the first conjunct says its underlying morphism veroneseProjHom is an isomorphism of schemes, that on homogeneous primes it is contraction along S' ⊆ S, and that on each standard open D₊(f) = Spec S₍f₎ it is Spec of the identification S'₍f ᵈ₎ ≅ S₍f₎ followed by the inclusion of D₊(f ᵈ) — the source's "S₍f₎ ≅ S'₍f ᵈ₎, compatible with the restriction maps". These charts cover Proj S, so they determine i as a morphism of schemes, not only on points. The next conjunct is the consequence i⁻¹ D₊(f ᵈ) = D₊(f), which the chart descriptions of assertion (1) are written over. The third conjunct is assertion (1) for a module in any universe v: the isomorphism Stacks.Veronese.veroneseAssociatedSheafIso 𝒮 𝒨 d hd : M̃ ≅ i^*(M'~), with the chart description that makes it canonical — on D₊(f) its inverse is the degree-zero Veronese localization comparison M'₍f ᵈ₎ ≅ M₍f₎. The fourth conjunct is assertion (2), each isomorphism exhibited as the source derives it: (1) at M = S(nd) followed by (S(nd))⁽ᵈ⁾ ≅ S'(n). The remaining conjuncts are the trailing clause: the commuting square with the multiplication maps of Tag 01MK, and the six squares with the maps of Tags 01MO, 03GJ, 01MP, 03GK, 01MQ and 01MR which the source derives from it and whose precise statements it omits. See the module documentation for each square, for why the source's proof of the first is corrected here (the comparison along its lower edge is not injective at S = k[x, y], d = 2, M = N = S(1): Stacks.Veronese.not_injective_veroneseTensorMap), and for the universes.

theorem tag0B5J (d : ℕ) (hd : 1 ≤ d) :
    letI := veroneseGradingGradedRing 𝒮 d hd
    -- `i` is an isomorphism of schemes, and on homogeneous primes it is contraction along
    -- `S⁽ᵈ⁾ ⊆ S`
    IsIso (veroneseProjHom 𝒮 d hd) ∧
      (∀ (x : ProjectiveSpectrum 𝒮) (g : veroneseSubring 𝒮 d),
        g ∈ ((veroneseProjIso 𝒮 d hd).hom.base x).asHomogeneousIdeal ↔
          (g : S) ∈ x.asHomogeneousIdeal) ∧
      -- on each chart `D₊(f) = Spec S₍f₎`, `i` is `Spec` of `S'₍f ᵈ₎ ≅ S₍f₎` followed by the
      -- inclusion of `D₊(f ᵈ)`: these determine `i` as a morphism of schemes
      (∀ (f : S) (e : ℕ) (he : 0 < e) (hf : f ∈ 𝒮 e),
        Proj.awayι 𝒮 f hf he ≫ (veroneseProjIso 𝒮 d hd).hom =
          Spec.map (veroneseAwayEquiv 𝒮 d f hf hd).toCommRingCatIso.hom ≫
            Proj.awayι (veroneseGrading 𝒮 d) (veronesePower 𝒮 d f hf)
              (veronesePower_mem 𝒮 d f hf) he) ∧
      -- the chart identification `i⁻¹ D₊(f ᵈ) = D₊(f)`
      (∀ (f : S) (e : ℕ), 0 < e → ∀ hf : f ∈ 𝒮 e,
        (veroneseProjIso 𝒮 d hd).hom ⁻¹ᵁ
            Proj.basicOpen (veroneseGrading 𝒮 d) (veronesePower 𝒮 d f hf) =
          Proj.basicOpen 𝒮 f) ∧
      -- assertion (1): `veroneseAssociatedSheafIso 𝒮 𝒨 d hd : M̃ ≅ i^*(M'~)`, for a module in
      -- any universe, with the chart description that makes it the canonical isomorphism
      (∀ (M : Type v) [AddCommGroup M] [Module S M] (𝒨 : ℤ → AddSubgroup M)
          [Decomposition 𝒨] [SetLike.GradedSMul 𝒮 𝒨],
        letI := veroneseModuleGradingDecomposition 𝒮 𝒨 d hd
        ∀ (f : S) (e : ℕ) (he : 0 < e) (hf : f ∈ 𝒮 e)
          (hvf : veronesePower 𝒮 d f hf ∈ veroneseGrading 𝒮 d e)
          (z : GradedModuleDegreeZeroLocalization (veroneseGrading 𝒮 d)
            (veroneseModuleGrading 𝒮 𝒨 d) (veronesePower 𝒮 d f hf)),
          ProjectiveSpectrum.Proj.associatedModuleSheafStandardOpenEquiv 𝒮 𝒨 hf he
              ((veroneseAssociatedSheafIso 𝒮 𝒨 d hd).inv.val.app (op (Proj.basicOpen 𝒮 f))
                (veroneseProjIso_basicOpen 𝒮 d hd f he hf ▸
                  ((SheafOfModules.pullbackPushforwardAdjunction.{max u v}
                        (veroneseProjIso 𝒮 d hd).hom.toRingCatSheafHom).unit.app
                      (ProjectiveSpectrum.Proj.associatedModuleSheaf (veroneseGrading 𝒮 d)
                        (veroneseModuleGrading 𝒮 𝒨 d))).val.app
                    (op (Proj.basicOpen (veroneseGrading 𝒮 d) (veronesePower 𝒮 d f hf)))
                    ((ProjectiveSpectrum.Proj.associatedModuleSheafStandardOpenEquiv
                        (veroneseGrading 𝒮 d) (veroneseModuleGrading 𝒮 𝒨 d)
                        hvf he).symm z))) =
            veroneseModuleAwayEquiv 𝒮 d 𝒨 f hf hd z) ∧
      -- assertion (2), as the source derives it from (1) at `M = S(nd)`
      (∀ n : ℤ, ∃ E : ProjectiveSpectrum.Proj.twistingSheaf 𝒮 (n * d) ≅
          (Scheme.Modules.pullback (veroneseProjIso 𝒮 d hd).hom).obj
            (ProjectiveSpectrum.Proj.twistingSheaf (veroneseGrading 𝒮 d) n),
        E.hom =
          (associatedModuleSheafVeroneseIso 𝒮 (twistGradingAddSubgroup 𝒮 (n * d)) d hd).hom ≫
            (Scheme.Modules.pullback (veroneseProjIso 𝒮 d hd).hom).map
              (veroneseShiftSheafIso 𝒮 d hd n).hom) ∧
      -- the trailing clause: compatibility of (1) with the multiplication maps
      (∀ (M N : Type u) [AddCommGroup M] [Module S M] [AddCommGroup N] [Module S N]
          (𝒨 : ℤ → AddSubgroup M) [Decomposition 𝒨] [SetLike.GradedSMul 𝒮 𝒨]
          (𝒩 : ℤ → AddSubgroup N) [Decomposition 𝒩] [SetLike.GradedSMul 𝒮 𝒩],
        veroneseTensorSquareLeft 𝒮 𝒨 𝒩 d hd = veroneseTensorSquareRight 𝒮 𝒨 𝒩 d hd) ∧
      -- "and hence with (01MO)": `𝒪(nd) ⊗ 𝒪(md) ⟶ 𝒪((n+m)d)` against `𝒪'(n) ⊗ 𝒪'(m) ⟶ 𝒪'(n+m)`
      (∀ n m : ℤ, veroneseTwistMulLeft 𝒮 d hd n m = veroneseTwistMulRight 𝒮 d hd n m) ∧
      -- "and hence with (03GJ)": `𝒪(nd) ⊗ ℱ(md) ⟶ ℱ((n+m)d)` against
      -- `𝒪'(n) ⊗ ℱ'(m) ⟶ ℱ'(n+m)`, for `ℱ = i^*ℱ'`
      (∀ (F' : SheafOfModules.{u}
            ((sheafCompose (Opens.grothendieckTopology
              (ProjectiveSpectrum.top (veroneseGrading 𝒮 d)))
              (forget₂ CommRingCat.{u} RingCat.{u})).obj
              (ProjectiveSpectrum.Proj.structureSheaf (veroneseGrading 𝒮 d)))) (n m : ℤ),
        veroneseTwistSheafMulLeft 𝒮 d hd F' n m = veroneseTwistSheafMulRight 𝒮 d hd F' n m) ∧
      -- "and hence with (03GK)": products of global sections of `𝒪(nd)` and `ℱ(md)`
      (∀ (F' : SheafOfModules.{u}
            ((sheafCompose (Opens.grothendieckTopology
              (ProjectiveSpectrum.top (veroneseGrading 𝒮 d)))
              (forget₂ CommRingCat.{u} RingCat.{u})).obj
              (ProjectiveSpectrum.Proj.structureSheaf (veroneseGrading 𝒮 d)))) (n m : ℤ)
          (s : (ProjectiveSpectrum.Proj.twistingSheaf 𝒮 (n * d)).val.obj (op ⊤))
          (t : (ProjectiveSpectrum.Proj.twistSheafOfModules 𝒮 (pullbackProjModule 𝒮
            (veroneseGrading 𝒮 d) (veroneseProjIso 𝒮 d hd).hom F') (m * d)).val.obj (op ⊤))
          (s' : (ProjectiveSpectrum.Proj.twistingSheaf (veroneseGrading 𝒮 d) n).val.obj (op ⊤))
          (t' : (ProjectiveSpectrum.Proj.twistSheafOfModules (veroneseGrading 𝒮 d) F' m).val.obj
            (op ⊤)),
        ((veroneseTwistingSheafIso 𝒮 d hd n).hom.val.app (op ⊤)).hom s =
            Stacks.Tag01VSPullbackTensor.modulesPullbackUnit (veroneseProjIso 𝒮 d hd).hom
              (ProjectiveSpectrum.Proj.twistingSheaf (veroneseGrading 𝒮 d) n) ⊤ s' →
        ((veroneseTwistedModuleIso 𝒮 d hd F' m).hom.val.app (op ⊤)).hom t =
            Stacks.Tag01VSPullbackTensor.modulesPullbackUnit (veroneseProjIso 𝒮 d hd).hom
              (ProjectiveSpectrum.Proj.twistSheafOfModules (veroneseGrading 𝒮 d) F' m) ⊤ t' →
        ((veroneseTwistedModuleIso 𝒮 d hd F' (n + m)).hom.val.app (op ⊤)).hom
            (((eqToHom (congrArg (ProjectiveSpectrum.Proj.twistSheafOfModules 𝒮
                (pullbackProjModule 𝒮 (veroneseGrading 𝒮 d) (veroneseProjIso 𝒮 d hd).hom F'))
                (add_mul n m (d : ℤ)).symm)).val.app (op ⊤)).hom
              (ProjectiveSpectrum.Proj.multiplyHomogeneousSections' 𝒮
                (pullbackProjModule 𝒮 (veroneseGrading 𝒮 d) (veroneseProjIso 𝒮 d hd).hom F')
                (n * d) (m * d) s t)) =
          Stacks.Tag01VSPullbackTensor.modulesPullbackUnit (veroneseProjIso 𝒮 d hd).hom
            (ProjectiveSpectrum.Proj.twistSheafOfModules (veroneseGrading 𝒮 d) F' (n + m)) ⊤
            (ProjectiveSpectrum.Proj.multiplyHomogeneousSections' (veroneseGrading 𝒮 d) F' n m
              s' t')) ∧
      -- "and hence with (01MP)": `S → ⨁ₙ Γ(X, 𝒪_X(n))` against `S' → ⨁ₙ Γ(X', 𝒪_{X'}(n))`
      (letI := (ProjectiveSpectrum.Proj.globalSectionsRingMap 𝒮).gradedRing
       letI := (ProjectiveSpectrum.Proj.globalSectionsRingMap (veroneseGrading 𝒮 d)).gradedRing
       ∀ (n : ℕ) (a : veroneseSubring 𝒮 d),
        (veroneseTwistingSheafIso 𝒮 d hd n).hom.val.app (op ⊤)
            ((eqToHom (congrArg (ProjectiveSpectrum.Proj.twistingSheaf 𝒮)
              (Nat.cast_mul n d))).val.app (op ⊤)
              (DirectSum.component ℤ ℕ (ProjectiveSpectrum.Proj.twistGlobalSections 𝒮) (n * d)
                ((ProjectiveSpectrum.Proj.globalSectionsRingMap 𝒮).hom (a : S)))) =
          Stacks.Tag01VSPullbackTensor.modulesPullbackUnit (veroneseProjIso 𝒮 d hd).hom
            (ProjectiveSpectrum.Proj.twistingSheaf (veroneseGrading 𝒮 d) n) ⊤
            (DirectSum.component ℤ ℕ
              (ProjectiveSpectrum.Proj.twistGlobalSections (veroneseGrading 𝒮 d)) n
              ((ProjectiveSpectrum.Proj.globalSectionsRingMap (veroneseGrading 𝒮 d)).hom a))) ∧
      -- "and hence with (01MQ)": `M̃ ⊗ 𝒪_X(nd) ⟶ M(nd)~` against `M'~ ⊗ 𝒪_{X'}(n) ⟶ M'(n)~`
      (∀ (M : Type u) [AddCommGroup M] [Module S M] (𝒨 : ℤ → AddSubgroup M)
          [Decomposition 𝒨] [SetLike.GradedSMul 𝒮 𝒨] (n : ℤ),
        veroneseModuleTwistLeft 𝒮 𝒨 d hd n = veroneseModuleTwistRight 𝒮 𝒨 d hd n) ∧
      -- "and hence with (01MR)": `M → ⨁ₙ Γ(X, M(n)~)` against `M' → ⨁ₙ Γ(X', M'(n)~)`
      (∀ (M : Type v) [AddCommGroup M] [Module S M] (𝒨 : ℤ → AddSubgroup M)
          [Decomposition 𝒨] [SetLike.GradedSMul 𝒮 𝒨],
        letI := veroneseModuleGradingDecomposition 𝒮 𝒨 d hd
        ∀ (n : ℤ) (m : veroneseSubmodule 𝒮 𝒨 d),
        (veroneseShiftedSheafIsoAny 𝒮 𝒨 d hd n).hom.val.app (op ⊤)
            (DirectSum.component ℤ ℤ _ (n * d)
              ((Stacks.AlgebraicGeometry.ProjShiftedSections.globalSectionsModuleMap 𝒮 𝒨).hom
                (m : M))) =
          pullbackUnitAny (veroneseProjIso 𝒮 d hd).hom
            (ProjectiveSpectrum.Proj.associatedModuleSheaf (veroneseGrading 𝒮 d)
              (shiftedGrading (veroneseModuleGrading 𝒮 𝒨 d) n)) ⊤
            (DirectSum.component ℤ ℤ _ n
              ((Stacks.AlgebraicGeometry.ProjShiftedSections.globalSectionsModuleMap
                (veroneseGrading 𝒮 d) (veroneseModuleGrading 𝒮 𝒨 d)).hom m)))
Sources
LeanStacks.AlgebraicGeometry.ProjMapCard.projMapData_preserves_products · Stacks.AlgebraicGeometry.ProjMapCardUnit.projMapData_preserves_unit · Stacks.AlgebraicGeometry.ProjTwistChain.awayToSection_comp_appLE_mapHom · Stacks.AlgebraicGeometry.ProjTwistChain.eq_mapHom · Stacks.AlgebraicGeometry.ProjMapUniqueTwist.projMapData_twistMap_unique · Stacks.AlgebraicGeometry.ProjShared.mapDomain · Stacks.AlgebraicGeometry.ProjTwistChain.mapHom_preimage_basicOpen · Stacks.AlgebraicGeometry.ProjTwistCompare.projMapData

Section27.12 Morphisms into Proj#

Section 27.12 of the Stacks Project, Tag 01N4. 9 tags here are carried by 23 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01N4, the section

Tag 01N4 in the Stacks Project.

Stacks.AlgebraicGeometry.ProjTriple.Triple, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjTriple.lean, line 199. The attribute's comment: “triple”.

A triple (d, L, ψ) of Stacks Tag 01N4, with the integer d and the invertible 𝒪_Y-module L as parameters: a graded ring map ψ : S^{(d)} ⟶ Γ_*(Y, L) such that L is generated by the global sections ψ(f) for f homogeneous of degree d.

Generation is the statement that the nonvanishing loci of those sections cover Y, which for an invertible module is exactly generation: at a point of the nonvanishing locus of a section the section generates the stalk (Stacks.SectionProduct.mem_nonvanishingLocus_iff_generates).

structure Triple

Stacks.AlgebraicGeometry.ProjTriple.BundledTriple, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjTriple.lean, line 217. The attribute's comment: “triple, bundled”.

A triple of Stacks Tag 01N4 in the literal shape of the source: an integer d ≥ 1, an invertible 𝒪_Y-module L, and a graded ring map ψ : S^{(d)} ⟶ Γ_*(Y, L) for which L is generated by the sections ψ(f), f ∈ S_d.

structure BundledTriple

Stacks.AlgebraicGeometry.ProjTriple.StrictEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjTriple.lean, line 246. The attribute's comment: “strict equivalence”.

Strict equivalence of two triples with the same d, Stacks Tag 01N4: there is an isomorphism β : L ⟶ L' of invertible 𝒪_Y-modules with β ∘ ψ = ψ'.

The condition β ∘ ψ = ψ' is written out degreewise: in degree n the induced isomorphism L^{⊗ n} ≅ (L')^{⊗ n} carries the degree n component of ψ to that of ψ'. A graded map is its family of components, so this is the source's condition and not a weakening of it.

def StrictEquiv (t : Triple 𝒮 Y L d) (t' : Triple 𝒮 Y L' d) : Prop

Stacks.AlgebraicGeometry.ProjTripleDegreeFunctor.Fd.functor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjTripleDegreeFunctor.lean, line 195. The attribute's comment: “the functor F_d : Sch^opp ⟶ Sets of this section at a fixed weight d, with both functor laws proved (Fd.pullback_id and Fd.pullback_comp): on objects the set F_d(Y) of strict equivalence classes of weight-d triples (d, L, ψ) over Y, on morphisms the pullback of a triple. The weight is a parameter rather than a field, so that SectionsEquiv applies with no transport. The target is Type (u+1), not Type u, because a triple carries an 𝒪_Y-module. Representability of F_d by U_d is Tag 01N9 and of the colimit F by Proj(A) is Tag 01NC; neither is proved in this file (Tag 01NC's is the carrier ProjTripleDegreeFunctor.F.representableBy, which is built on top of this functor)”.

The functor F_d : Sch^{opp} ⟶ Sets at a fixed weight d. It sends a scheme Y to the set F_d(Y) of strict equivalence classes of weight-d triples (d, L, ψ) over Y, and a morphism of schemes h : Y' ⟶ Y to the map sending the class of a triple to the class of its pullback along h.

def Fd.functor (d : ℕ) : Scheme.{u}ᵒᵖ ⥤ Type (u + 1)

Stacks.AlgebraicGeometry.ProjTripleFunctorLaws.sectionsEquiv_pullbackTriple_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjTripleFunctorLaws.lean, line 163. The attribute's comment: “the identity functor law for the pullback of a triple of this section: the pullback along the identity is STRICTLY EQUIVALENT to the triple, in the SectionsEquiv sense of the section; the composition law is sectionsEquiv_pullbackTriple_comp below”.

The identity functor law for the pullback of a triple: the pullback (d, (𝟙 Y)^*L, (𝟙 Y)^* ∘ ψ) of a triple (d, L, ψ) along 𝟙 Y is strictly equivalent to it.

theorem sectionsEquiv_pullbackTriple_id (t : ProjTripleClassifying.Triple 𝒜 Y) :
    ProjTripleClassifying.SectionsEquiv 𝒜 (ProjTriplePullback.pullbackTriple 𝒜 t (𝟙 Y)).psi
      t.psi

Stacks.AlgebraicGeometry.ProjTripleFunctorLaws.sectionsEquiv_pullbackTriple_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjTripleFunctorLaws.lean, line 368. The attribute's comment: “the composition functor law for the pullback of a triple of this section: the pullback along f of the pullback along g is STRICTLY EQUIVALENT to the pullback along f ≫ g, in the SectionsEquiv sense of the section”.

The composition functor law for the pullback of a triple: the pullback along f of the pullback along g of a triple is strictly equivalent to its pullback along f ≫ g.

theorem sectionsEquiv_pullbackTriple_comp (t : ProjTripleClassifying.Triple 𝒜 W'') :
    ProjTripleClassifying.SectionsEquiv 𝒜
      (ProjTriplePullback.pullbackTriple 𝒜 (ProjTriplePullback.pullbackTriple 𝒜 t g) f).psi
      (ProjTriplePullback.pullbackTriple 𝒜 t (f ≫ g)).psi

Stacks.AlgebraicGeometry.ProjTriplePullback.pullbackTriple, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjTriplePullback.lean, line 170. The attribute's comment: “the pullback of a triple along a morphism of schemes h : Y' ⟶ Y: the triple (d, h^L, h^ ∘ ψ), in the VeroneseSections spelling of the graded map that Tag 01N8 and Tag 01N9 are stated in. The two functor laws — that the pullback along an identity and the pullback along a composite are STRICTLY EQUIVALENT to the triple and to the twice-pulled-back triple — are ProjTripleFunctorLaws.sectionsEquiv_pullbackTriple_id and sectionsEquiv_pullbackTriple_comp. The functor F_d itself, i.e. the quotient of the triples by strict equivalence with this pullback on morphisms, is ProjTripleDegreeFunctor.Fd.functor; it is built at a fixed weight, on a carrier that takes the weight as a parameter rather than as a field, because strict equivalence compares two graded maps of the same weight and a triple-level version would need a transport”.

For h : Y' ⟶ Y, the pullback of the triple (d, L, ψ) over Y is the triple (d, h^*L, h^* ∘ ψ) over Y': the same integer d, the pullback of the invertible module, and the degreewise pullback pullbackSections of the graded map.

def pullbackTriple (t : ProjTripleClassifying.Triple 𝒜 Y) (h : Y' ⟶ Y) :
    ProjTripleClassifying.Triple 𝒜 Y'
Tag 01N5, an equation

Tag 01N5 in the Stacks Project.

AlgebraicGeometry.Proj.degreeOpen, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjDegreeOpen.lean, line 49.

The degree d open of Proj 𝒜, the union U_d = ⋃_{f ∈ 𝒜 d} D₊(f) of the projective standard opens of the homogeneous elements of degree exactly d.

public def degreeOpen (d : ℕ) : (Proj 𝒜).Opens

AlgebraicGeometry.Proj.degreeOpen_le_of_dvd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjDegreeOpen.lean, line 61. The attribute's comment: “divisibility”.

The degree opens grow along divisibility: if d ∣ d' and d' is positive then U_d ⊆ U_{d'}. A homogeneous f of degree d has f ^ k of degree d' = d * k, and D₊(f ^ k) = D₊(f).

public theorem degreeOpen_le_of_dvd {d d' : ℕ} (hdvd : d ∣ d') (hd' : 0 < d') :
    degreeOpen 𝒜 d ≤ degreeOpen 𝒜 d'

AlgebraicGeometry.Proj.iSup_degreeOpen_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjDegreeOpen.lean, line 74. The attribute's comment: “covering”.

The degree opens cover Proj 𝒜: every point lies in U_d for some positive d, because a homogeneous prime of Proj 𝒜 does not contain the irrelevant ideal, which is generated by the homogeneous elements of positive degree.

public theorem iSup_degreeOpen_eq_top :
    (⨆ d : ℕ, ⨆ _ : 0 < d, degreeOpen 𝒜 d) = ⊤
Tag 01N6, an equation

Tag 01N6 in the Stacks Project.

Stacks.AlgebraicGeometry.ProjDegreeOpenSections.psi, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjDegreeOpenSections.lean, line 484.

The graded ring homomorphism ψ^d : S^(d) ⟶ Γ_*(Y, 𝒪_Y(d)), sending a homogeneous element of degree nd to the restriction to Y of the global section of 𝒪(nd) it determines. Taken at Y = U_d this is ψ^d : S^(d) ⟶ Γ_*(U_d, 𝒪_{U_d}(d)).

public def psi (hd : 0 < d) :
    letI := veroneseGradingGradedRing 𝒮 d hd
    letI := veroneseGradedRing 𝒮 Y d
    veroneseGrading 𝒮 d →+*ᵍ veroneseSectionRingGrading 𝒮 Y d

Stacks.AlgebraicGeometry.ProjDegreeOpenSections.nonvanishingLocus_veroneseSection_inter, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjDegreeOpenSections.lean, line 519. The attribute's comment: “global generation in degree one”.

Global generation of 𝒪_{U_d}(d) by the image of ψ^d in degree one. The nonvanishing locus on U_d of the section attached to a homogeneous f of degree d is D₊(f) ∩ U_d; since the D₊(f) for f ∈ 𝒮 d cover U_d by definition, the sections in the image of ψ^d in degree one generate.

public theorem nonvanishingLocus_veroneseSection_inter (f : 𝒮 (1 * d)) :
    Stacks.SheafOfModules.nonvanishingLocus
          (X := (AlgebraicGeometry.Proj 𝒮).toRingedSpace)
          (twistingSheaf 𝒮 ((1 * d : ℕ) : ℤ))
          (Stacks.SheafOfModules.sectionsOfTop _ (degreeSection 𝒮 (1 * d) f)) ∩
        (Proj.degreeOpen 𝒮 d : Set (AlgebraicGeometry.Proj 𝒮)) =
      (Proj.basicOpen 𝒮 (f : S) : Set (AlgebraicGeometry.Proj 𝒮)) ∩
        (Proj.degreeOpen 𝒮 d : Set (AlgebraicGeometry.Proj 𝒮))
Tag 01N7, an equation

Tag 01N7 in the Stacks Project.

Stacks.AlgebraicGeometry.MorphismsIntoProj.psiPullback_gradedRingHom_and_generatesStalks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MorphismsIntoProjGradedRing.lean, line 290. The attribute's comment: “the graded ring homomorphism ψ^d_φ : S^(d) ⟶ Γ_*(Y, φ⁎𝒪_X(d)) attached to a morphism φ : Y ⟶ U_d, whose degree n component sends a homogeneous element of degree nd to the pullback along φ of the global section of 𝒪_X(nd) it determines, together with the global generation of φ⁎𝒪_X(d) by the sections in the image of its degree-one component S_d”.

Let S be a graded ring, X = Proj(S), let d ≥ 1, let U_d ⊂ X be the degree d open and let φ : Y ⟶ U_d be a morphism of schemes. Then the degreewise maps assemble into a graded ring homomorphism

ψ^d_φ : S^{(d)} ⟶ Γ_*(Y, φ⁎𝒪_X(d)),

sending a homogeneous element of degree nd to the pullback along φ of the global section of 𝒪_X(nd) it determines, and the invertible sheaf φ⁎𝒪_X(d) is generated by the global sections in the image of the degree-one component (S^{(d)})_1 = S_d ⟶ Γ(Y, φ⁎𝒪_X(d)).

The target is the twist model of Γ_*: its degree n piece is Γ(Y, φ⁎𝒪_X(nd)) rather than Γ(Y, (φ⁎𝒪_X(d))^{⊗ n}), and the grading index type lives in the same universe as the ring. The graded ring homomorphism itself is available as psiPullback, and the two conjuncts separately as psiPullback_apply_homogeneous and generatesStalks_psiPullbackVeroneseHom_one.

theorem psiPullback_gradedRingHom_and_generatesStalks (hd : 0 < d)
    (φ : Y ⟶ (degreeOpen 𝒜 d).toScheme) :
    (letI := veroneseGradingGradedRing 𝒜 d hd
     letI := veroneseSectionGradedRing 𝒜 (toProjRS 𝒜 φ) d (op ⊤)
     ∃ ψ : veroneseGrading 𝒜 d →+*ᵍ veroneseSectionRingGrading 𝒜 (toProjRS 𝒜 φ) d (op ⊤),
       ∀ (n : ℕ) (a : veroneseGrading 𝒜 d n),
         ψ (a : veroneseSubring 𝒜 d) =
           DirectSum.of (veroneseSections 𝒜 (toProjRS 𝒜 φ) d (op ⊤)) n
             (psiPullbackVeroneseHom 𝒜 φ n a)) ∧
      Stacks.ProjectiveFromSections.GeneratesStalks
        (L := pullbackTwist 𝒜 φ ((1 * d : ℕ) : ℤ))
        (fun x : ↥(veroneseGrading 𝒜 d 1) => psiPullbackVeroneseHom 𝒜 φ 1 x)
Tag 01N8, a lemma

Tag 01N8 in the Stacks Project.

Stacks.AlgebraicGeometry.MorphismToProjSquare.existsUnique_square, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/MorphismToProjSquare.lean, line 114. The attribute's comment: “the unique pair (φ, α) of φ : Y ⟶ U_d and α : φ^O_{U_d}(d) ≅ L making the square α^{⊗n}(φ^(ψ^d(x))) = ψ(x) commute in every degree n”.

Let A be a graded ring, X = Proj(A), let d ≥ 1 and let U_d ⊆ X be the open of Equation 27.12.0.1. Let Y be a scheme, L an invertible 𝒪_Y-module and ψ : A^{(d)} → Γ_*(Y, L) a graded map such that L is generated by the sections ψ(f), f ∈ A_d — in the geometric form of Section 27.12, that their nonvanishing opens cover Y. Then there is a unique pair (φ, α) of a morphism φ : Y ⟶ U_d (so the morphism Y ⟶ X it defines has image in U_d) and an isomorphism α : φ⁎𝒪_{U_d}(d) ≅ L such that ψ^d_φ agrees with ψ via α: the square

α ∘ φ^* ∘ ψ^d = ψ

commutes in every degree n, i.e. α^{⊗ n}(φ^*(ψ^d(x))) = ψ(x) in Γ(Y, L^{⊗ n}) for every x ∈ A_{nd}. Here ψ^d : A^{(d)} ⟶ Γ_*(U_d, 𝒪_{U_d}(d)) is Stacks.AlgebraicGeometry.ProjDegreeOpenUniversalTriple.universalVeroneseSections, φ^* on sections of tensor powers is Stacks.AlgebraicGeometry.ProjChartRatioPullback.pullSection, and α^{⊗ n} is Stacks.AmplePullbackPart1.natTensorPowCongr α n.

theorem existsUnique_square (hd : 0 < d) (ψ : VeroneseSections 𝒜 d L)
    (hgen : ⨆ f : 𝒜 d, nonvanishingOpen Y L (psiSection 𝒜 ψ f) = ⊤) :
    ∃! p : (φ : Y ⟶ (degreeOpen 𝒜 d).toScheme) ×
        ((Scheme.Modules.pullback φ).obj (universalTwist 𝒜 d) ≅ L),
      ∀ (n : ℕ) (x : 𝒜 (n * d)),
        (natTensorPowCongr p.2 n).hom.app ⊤
            (pullSection p.1 (universalTwist 𝒜 d) n
              ((universalVeroneseSections 𝒜 d).toFun n x))
          = ψ.toFun n x
Tag 01N9, a lemma

Tag 01N9 in the Stacks Project.

Stacks.AlgebraicGeometry.ProjChartAlphaInstance.isInvertibleModule_pullbackTwist, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjChartAlphaInstance.lean, line 211. The attribute's comment: “the universal family (d, 𝒪_{U_d}(d), ψ^d): 𝒪_{U_d}(d) is an invertible 𝒪_{U_d}-module”.

φ⁎𝒪_{U_d}(d) is an invertible 𝒪_Y-module. The twist 𝒪_X(d) is invertible only after restriction to U_d ([Stacks, Tag 01MU]), the pullback along φ of an invertible module is invertible ([Stacks, Tag 0B8L]), and AlgebraicGeometry.Scheme.Modules.pullbackComp identifies the iterated pullback with the pullback along φ ≫ U_d.ι. At φ = 𝟙 this is the invertibility of 𝒪_{U_d}(d), the module of the universal family of [Stacks, Tag 01N9].

instance isInvertibleModule_pullbackTwist (φ : Y ⟶ (degreeOpen 𝒜 d).toScheme) :
    Stacks.Ample.IsInvertibleModule Y (pullbackTwist 𝒜 φ (d : ℤ))

Stacks.AlgebraicGeometry.ProjDegreeOpenRepresents.iSup_nonvanishingOpen_universalSection_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjDegreeOpenRepresents.lean, line 163. The attribute's comment: “the universal family (d, 𝒪_{U_d}(d), ψ^d): the degree-one values ψ^d(f), f ∈ A_d, generate 𝒪_{U_d}(d), their nonvanishing opens covering U_d”.

The universal family of [Stacks, Tag 01N9] is generated in degree one. The nonvanishing open of ψ^d(f) on U_d is the preimage of D₊(f) under the open immersion U_d ⟶ X (Stacks.AlgebraicGeometry.MorphismToProjUniversal.preimage_basicOpen_eq_nonvanishingOpen, which is [Stacks, Tag 01MV] together with [Stacks, Tag 0H78]), and those preimages cover U_d because the D₊(f), f ∈ 𝒜 d, are what U_d is the union of. So 𝒪_{U_d}(d) is generated by the global sections ψ^d(f), in the geometric form Section 27.12 uses that condition.

theorem iSup_nonvanishingOpen_universalSection_eq_top :
    (⨆ f : 𝒜 d, nonvanishingOpen (degreeOpen 𝒜 d).toScheme (universalTwist 𝒜 d)
      (universalSection 𝒜 d f)) = ⊤

Stacks.AlgebraicGeometry.ProjDegreeOpenRepresents.existsUnique_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjDegreeOpenRepresents.lean, line 209. The attribute's comment: “U_d represents F_d, with (d, 𝒪_{U_d}(d), ψ^d) the universal family: a unique morphism Y ⟶ U_d for every triple over Y. The strict equivalence between the pullback of the universal family and the given triple is IsCompatible, whose degree-n clause for n ≥ 2 is the source's local identity ψ(a)|_V = φ♯(a/f^n)·ψ(f)^n|_V rather than the tensor-power square α^{⊗n}(ψ^d_φ(x)) = ψ(x); the square implies it, so the uniqueness assertion is at least as strong as the source's, and the caveat is inherited verbatim from Tag 01N8. Degree 1 is the square itself. The source quantifies over strict equivalence classes; this statement quantifies over representatives, which is stronger.”.

Stacks Tag 01N9, Lemma 27.12.2. Let A be a graded ring, X = Proj(A), let d > 0 and let U_d ⊆ X be the open of Equation 27.12.0.1. The open subscheme U_d represents the functor F_d, the triple (d, 𝒪_{U_d}(d), ψ^d) being the universal family: for a scheme Y and a triple (d, L, ψ) over Y — an invertible 𝒪_Y-module L and a graded map ψ : A^{(d)} ⟶ Γ_*(Y, L) whose degree-d part generates L, in the geometric form that the nonvanishing opens of the sections ψ(f), f ∈ A_d, cover Y — there is one and only one morphism φ : Y ⟶ U_d for which the pullback φ⁎(d, 𝒪_{U_d}(d), ψ^d) of the universal family is strictly equivalent to (d, L, ψ), i.e. for which some isomorphism α : φ⁎𝒪_{U_d}(d) ≅ L identifies ψ^d_φ with ψ.

That is the bijection Mor(Y, U_d) ≅ F_d(Y): the existence of φ is its surjectivity and the uniqueness of φ its injectivity, the map being φ ↦ [φ⁎(d, 𝒪_{U_d}(d), ψ^d)].

The source's proof is "this is a reformulation of Lemma 27.12.1", and so is this one: [Stacks, Tag 01N8] (Stacks.AlgebraicGeometry.MorphismToProjUniversal.existsUnique_pair) gives a unique pair (φ, α), and a pair is its first component together with the compatibility, so the morphism is unique among those admitting a compatible α.

theorem existsUnique_hom (hd : 0 < d) (ψ : VeroneseSections 𝒜 d L)
    (hgen : ⨆ f : 𝒜 d, nonvanishingOpen Y L (psiSection 𝒜 ψ f) = ⊤) :
    ∃! φ : Y ⟶ (degreeOpen 𝒜 d).toScheme,
      ∃ α : pullbackTwist 𝒜 φ (d : ℤ) ≅ L, IsCompatible 𝒜 ψ ⟨φ, α⟩
Tag 01NA, a lemma

Tag 01NA in the Stacks Project.

Stacks.AlgebraicGeometry.ProjDegreeOneRepresents.degreeOpen_one_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjDegreeOneRepresents.lean, line 145. The attribute's comment: “X = U₁”.

X = U_1. When A is generated as an 𝒜 0-algebra by its degree-one part, the open U_1 = ⋃_{f ∈ 𝒜 1} D₊(f) of Equation 27.12.0.1 is all of Proj A. This is the one input the source's proof of [Stacks, Tag 01NA] names, and it is Stacks.AlgebraicGeometry.ProjDegreeOne.iSup_basicOpen_degreeOne_eq_top read through the definition of U_1.

theorem degreeOpen_one_eq_top (hgen : Algebra.adjoin (𝒜 0) ((𝒜 1 : Set A)) = ⊤) :
    degreeOpen 𝒜 1 = ⊤

Stacks.AlgebraicGeometry.ProjDegreeOneRepresents.isInvertibleModule_twistingSheafOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjDegreeOneRepresents.lean, line 219. The attribute's comment: “the universal family on X: 𝒪_X(1) is invertible”. References: EGA II (2.6.1); EGA II (3.2.5), “special case”.

𝒪_X(1) is an invertible 𝒪_X-module on all of Proj A when A is generated in degree one over 𝒜 0. Without that hypothesis the twist is invertible only on U_1; this is Stacks.AlgebraicGeometry.ProjDegreeOne.isInvertible_twistingSheaf, read in the Stacks.Ample.IsInvertibleModule spelling that triples and their trivializations are stated in.

theorem isInvertibleModule_twistingSheafOne
    (hgen : Algebra.adjoin (𝒜 0) ((𝒜 1 : Set A)) = ⊤) :
    Stacks.Ample.IsInvertibleModule (AlgebraicGeometry.Proj 𝒜)
      (twistingSheaf 𝒜 ((1 : ℕ) : ℤ))

Stacks.AlgebraicGeometry.ProjDegreeOneRepresents.exists_mem_nonvanishingLocus_degreeSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjDegreeOneRepresents.lean, line 234. The attribute's comment: “the universal family on X: global generation in degree one”.

The universal family of [Stacks, Tag 01NA] generates 𝒪_X(1) on all of X. The global section of 𝒪_X(1) attached to a degree-one element f is nonvanishing exactly on D₊(f) ([Stacks, Tag 01MV], available because U_1 ⊆ W_1), and those opens cover Proj A by degreeOpen_one_eq_top. So the degree-one part of ψ^1 generates 𝒪_X(1), which is the second assertion of [Stacks, Tag 01N9] transported to X by X = U_1.

theorem exists_mem_nonvanishingLocus_degreeSection
    (hgen : Algebra.adjoin (𝒜 0) ((𝒜 1 : Set A)) = ⊤) (x : ProjectiveSpectrum.top 𝒜) :
    ∃ f : 𝒜 1, x ∈ Stacks.Ample.nonvanishingLocus (X := AlgebraicGeometry.Proj 𝒜)
      (twistingSheaf 𝒜 ((1 : ℕ) : ℤ)) (degreeSection 𝒜 1 f)

Stacks.AlgebraicGeometry.ProjDegreeOneRepresents.existsUnique_classifies, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjDegreeOneRepresents.lean, line 353. The attribute's comment: “the universal property of Proj”.

The universal property of Proj A of [Stacks, Tag 01NA]. Let A be a graded ring generated as an 𝒜 0-algebra by its degree-one part, let Y be a scheme, L an invertible 𝒪_Y-module and ψ : A ⟶ Γ_*(Y, L) a graded map whose degree-one part generates L. Then there is one and only one pair (φ, α) consisting of a morphism φ : Y ⟶ Proj A and an isomorphism α : φ⁎𝒪_X(1) ≅ L ^⊗ 1 classifying (L, ψ).

This is [Stacks, Tag 01N8] at d = 1 with the target raised from U_1 to the whole of Proj A, which is the content of [Stacks, Tag 01NA]: X = U_1 by degreeOpen_one_eq_top, so every morphism into X is a morphism into U_1 and the uniqueness assertion holds among all morphisms into X.

theorem existsUnique_classifies (hgen : Algebra.adjoin (𝒜 0) ((𝒜 1 : Set A)) = ⊤)
    (ψ : VeroneseSections 𝒜 1 L) (hcover : ⨆ f : 𝒜 1, nvOpen 𝒜 ψ f = ⊤) :
    ∃! p : Pair 𝒜 L, Classifies 𝒜 ψ p
Tag 01NB, a lemma

Tag 01NB in the Stacks Project.

Stacks.AlgebraicGeometry.ProjEquivalenceCycle.tfae_triple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjEquivalenceCycle.lean, line 134. The attribute's comment: “all four clauses of the tag are equivalent, for two triples over a scheme, as a single statement; the list entries are clauses (1), (2), (3), (4) in that order”.

For two triples t, t' over a scheme the following are equivalent: the agreement condition at the weights (lcm(d, d') / d, lcm(d, d') / d'); the agreement condition at the weights (d', d); the agreement condition at some positive weights (a, a') with a * d = a' * d'; the two triples classify the same morphism. Here d = t.deg and d' = t'.deg.

theorem tfae_triple (t t' : Triple 𝒜 Y) :
    List.TFAE
      [AgreeAt t t' (Nat.lcm t.deg t'.deg / t.deg) (Nat.lcm t.deg t'.deg / t'.deg),
        AgreeAt t t' t'.deg t.deg,
        ∃ a a' : ℕ, 0 < a ∧ 0 < a' ∧ a * t.deg = a' * t'.deg ∧ AgreeAt t t' a a',
        SameMorphism 𝒜 t t']
Tag 01NC, a lemma

Tag 01NC in the Stacks Project.

Stacks.AlgebraicGeometry.ProjTripleDegreeFunctor.F.representableBy, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjFunctorRepresentable.lean, line 337. The attribute's comment: “the FULL statement of this tag: Proj(A) represents the functor F of Section 01N4. F.functor is F as a functor Sch^opp ⟶ Type (u+1) on ALL schemes (the colimit Fcolim of the F_d along divisibility on a quasi-compact T, by F.fcolimEquiv, and the limit over the quasi-compact test objects in general, which is the limit over the quasi-compact opens the source writes — see the module docstring for why the index is the morphisms out of quasi-compact schemes), F.classifyingEquiv is the bijection F(T) ≃ Mor(T, Proj(A)) for every scheme T, and this is the RepresentableBy datum. The two halves of the bijection remain available separately as Fd.veronese_eq_weightCongr_veronese_of_classifyingMorphism_eq (injectivity) and Fd.exists_pos_classifyingMorphism_eq (surjectivity for a quasi-compact Y). The grading is taken with its index type in the same universe as the graded ring, which is the generality of Tag 01N9's universal family here; the functor F itself and F.fcolimEquiv are unrestricted.”.

Proj(A) represents the functor F of Section 01N4. Let A be a graded ring and X = Proj(A). The functor F : Sch^{opp} ⟶ Sets which sends a quasi-compact scheme T to ⋃_{d ≥ 1} F_d(T), the colimit of the sets of strict equivalence classes of triples of positive weight along the weight transitions, and a general scheme to the limit of those over its quasi-compact opens, is represented by X: there is a bijection Mor(T, X) ≃ F(T) natural in T.

The bijection is F.classifyingEquiv, whose two halves are the injectivity of [Stacks, Tag 01NB] and the surjectivity coming from [Stacks, Tag 01N9]'s universal family; its naturality is F.ofHom_comp.

def F.representableBy : (F.functor 𝒮).RepresentableBy (AlgebraicGeometry.Proj 𝒮)
Sources
LeanStacks.AlgebraicGeometry.ProjTriple.Triple · Stacks.AlgebraicGeometry.ProjTriple.BundledTriple · Stacks.AlgebraicGeometry.ProjTriple.StrictEquiv · Stacks.AlgebraicGeometry.ProjTripleDegreeFunctor.Fd.functor · Stacks.AlgebraicGeometry.ProjTripleFunctorLaws.sectionsEquiv_pullbackTriple_id · Stacks.AlgebraicGeometry.ProjTripleFunctorLaws.sectionsEquiv_pullbackTriple_comp · Stacks.AlgebraicGeometry.ProjTriplePullback.pullbackTriple · AlgebraicGeometry.Proj.degreeOpen

Section27.13 Projective space#

Section 27.13 of the Stacks Project, Tag 01ND. 9 tags here are carried by 21 declarations of the repository (all in StacksFrontier) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01ND, the section

Tag 01ND in the Stacks Project.

Stacks.ProjectiveFromSections.toProjectiveSpaceOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveFromSections/Morphism.lean, line 118. The attribute's comment: “the notation phi_(L, (s_0, ..., s_n)) of the section, as data: the morphism to P^n_S attached to an invertible module with n + 1 generating global sections, pinned on each standard chart. The scheme P^n_S itself is Tag 01NF (AlgebraicGeometry.projectiveSpaceOver). The section's characterisation of the morphism by L = phi^ O(1) and s_i = phi^ T_i is NOT proved: the comparison of L with the pullback of the hyperplane sheaf is the twist identification recorded as missing in StacksFrontier/AlgebraicGeometry/AmpleProjectiveImmersion/Basic.lean. The representability statement Tag 01NE is likewise not proved, only this direction of it”.

The morphism φ_{(L, (s₀, …, sₙ))} : X ⟶ ℙⁿ_S of Section 27.13, attached to a structure morphism f : X ⟶ S, an invertible 𝒪_X-module L and a generating family of n + 1 global sections of L. It is the morphism to the integral model paired with f; no compatibility has to be checked, ℙⁿ_S being a fibre product over the terminal scheme.

def toProjectiveSpaceOver {S : Scheme.{u}} (f : X ⟶ S) : X ⟶ projectiveSpaceOver n S
Tag 01NE, a lemma

Tag 01NE in the Stacks Project.

Stacks.ProjectiveSpaceModuli.bijective_pointsOfHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpaceModuli/Basic.lean, line 501. The attribute's comment: “the bijection on points”.

Projective n-space over the integers represents the functor sending a scheme X to the set of pairs (L, (s₀, …, sₙ)) with L an invertible 𝒪_X-module and the sᵢ generating global sections, up to an isomorphism matching the sections: the classifying map is a bijection.

theorem bijective_pointsOfHom :
    Function.Bijective (pointsOfHom (X := X) (n := n))

Stacks.ProjectiveSpaceModuli.pointsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpaceModuli/Basic.lean, line 508. The attribute's comment: “the representing bijection”.

The bijection between morphisms X ⟶ ℙⁿ_ℤ and invertible modules with n + 1 generating global sections up to isomorphism.

def pointsEquiv (X : Scheme.{u}) (n : ℕ) :
    (X ⟶ projectiveSpaceAtUniverse.{u} n) ≃ Points X n

Stacks.ProjectiveSpaceModuli.pointsOfHom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpaceModuli/Basic.lean, line 570. The attribute's comment: “naturality of the bijection in the test scheme”.

The classifying map is natural in the test scheme: the pair attached to h ≫ g is the pullback along h of the pair attached to g.

theorem pointsOfHom_comp (h : Y ⟶ X) (g : X ⟶ projectiveSpaceAtUniverse.{u} n) :
    pointsOfHom (h ≫ g) = pullbackPoints h (pointsOfHom g)
Tag 01NF, a definition

Tag 01NF in the Stacks Project.

AlgebraicGeometry.projectiveSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjectiveSpace.lean, line 61. The attribute's comment: “projective space over the integers”.

Projective n-space over the integers.

public noncomputable def projectiveSpace (n : ℕ) : Scheme.{0}

AlgebraicGeometry.projectiveSpaceIntegralIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjectiveSpace.lean, line 78. The attribute's comment: “canonical comparison of integral models”.

The canonical comparison between the literal integral model and its universe-zero copy.

public noncomputable def projectiveSpaceIntegralIso (n : ℕ) :
    projectiveSpace n ≅ projectiveSpaceAtUniverse.{0} n

AlgebraicGeometry.projectiveSpaceOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjectiveSpace.lean, line 138. The attribute's comment: “projective space over a scheme”.

Projective n-space over S, by base change from the integers.

public noncomputable abbrev projectiveSpaceOver (n : ℕ) (S : Scheme.{u}) : Scheme.{u}

AlgebraicGeometry.projectiveSpaceOverRing, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjectiveSpace.lean, line 181. The attribute's comment: “projective space over a ring”.

Projective n-space over a commutative ring R.

public noncomputable abbrev projectiveSpaceOverRing (n : ℕ) (R : CommRingCat.{u}) : Scheme.{u}
Tag 01NG, a lemma

Tag 01NG in the Stacks Project.

AlgebraicGeometry.ProjectiveSpace.basicOpenXIsoAffineSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjectiveSpaceCharts.lean, line 121. The attribute's comment: “affine-space charts”.

The standard open at a homogeneous coordinate of projective n-space over the integers is affine n-space over the integers.

The identification sends the affine coordinate indexed by j ≠ i to the ratio T_j / T_i.

public noncomputable def basicOpenXIsoAffineSpace (i : Fin (n + 1)) :
    (Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) ℤ)
      (MvPolynomial.X i)).toScheme ≅ AffineSpace (Fin n) (Spec (.of ℤ))

Stacks.ProjectiveChart.iSup_basicOpen_X_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveChart/Basic.lean, line 350. The attribute's comment: “standard-open covering”.

The homogeneous coordinate standard opens cover projective space.

theorem iSup_basicOpen_X_eq_top (n : ℕ) :
    (⨆ i : Fin (n + 1),
      Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R)
        (MvPolynomial.X i)) = ⊤

Stacks.ProjectiveChart.basicOpen_X_iso_affineSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveChart/Basic.lean, line 374. The attribute's comment: “affine-space charts”.

The standard open at a homogeneous coordinate is affine n-space.

noncomputable def basicOpen_X_iso_affineSpace (A : Type) [CommRing A] (n : ℕ)
    (i : Fin (n + 1)) :
    (Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)
      (MvPolynomial.X i)).toScheme ≅ AffineSpace (Fin n) (Spec (.of A))

Stacks.ProjectiveSpace.iSup_basicOpen_X_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/Dimension/Basic.lean, line 95. The attribute's comment: “standard-open covering”.

The standard opens D₊(Xᵢ) cover Proj of the polynomial algebra graded by total degree. For R = ℤ and σ = Fin (n + 1) this is the standard covering of projective n-space over the integers.

theorem iSup_basicOpen_X_eq_top (R : Type u) [CommRing R] (σ : Type v) :
    (⨆ i : σ, Proj.basicOpen (homogeneousSubmodule σ R) (X i)) = ⊤
Tag 01NH, a lemma

Tag 01NH in the Stacks Project.

AlgebraicGeometry.projectiveSpaceOver.isProper, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjectiveSpaceProper.lean, line 89. The attribute's comment: “universally closed”.

Projective n-space over a scheme S is proper over S. In particular the structure morphism ℙⁿ_S ⟶ S is universally closed, assertion (4) of Stacks 01NH.

instance isProper (n : ℕ) (S : Scheme.{u}) : IsProper ((projectiveSpaceOver n S) ↘ S)

AlgebraicGeometry.projectiveSpaceOver.valuativeCriterion_existence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjectiveSpaceStructureMorphism.lean, line 61. The attribute's comment: “existence part of the valuative criterion”.

Stacks 01NH (3), existence. The structure morphism of projective n-space over a scheme S satisfies the existence part of the valuative criterion.

theorem valuativeCriterion_existence (n : ℕ) (S : Scheme.{u}) :
    ValuativeCriterion.Existence (projectiveSpaceOver n S ↘ S)

AlgebraicGeometry.projectiveSpaceOver.valuativeCriterion_uniqueness, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjectiveSpaceStructureMorphism.lean, line 70. The attribute's comment: “uniqueness part of the valuative criterion”.

Stacks 01NH (3), uniqueness. The structure morphism of projective n-space over a scheme S satisfies the uniqueness part of the valuative criterion.

theorem valuativeCriterion_uniqueness (n : ℕ) (S : Scheme.{u}) :
    ValuativeCriterion.Uniqueness (projectiveSpaceOver n S ↘ S)

Declarations registered for the tag:

Tag 01WD, a lemma

Tag 01WD in the Stacks Project.

AlgebraicGeometry.Segre.isClosedImmersion_segreMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Segre/ChartSurjective.lean, line 379. The attribute's comment: “the integral models”. References: EGA II (4.3.3), “over Spec ℤ”.

The Segre morphism of the integral models is a closed immersion.

theorem isClosedImmersion_segreMorphism (n m : ℕ) :
    IsClosedImmersion (segreMorphism.{u} n m)

AlgebraicGeometry.Segre.hasSegreEmbeddingSharp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Segre/ChartSurjective.lean, line 398. The attribute's comment: “over an arbitrary base”. References: EGA II (4.3.3).

[Stacks, Tag 01WD] over an arbitrary base. For every scheme S and all n m, there is a closed immersion ℙⁿ_S ×_S ℙᵐ_S ⟶ ℙ^{nm + n + m}_S over S.

theorem hasSegreEmbeddingSharp (S : Scheme.{u}) : HasSegreEmbeddingSharp S

Stacks.AlgebraicGeometry.SegreProdIso.exists_segreEmbedding, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SegreProdIso/Main.lean, line 362. References: EGA II (4.3.3).

Stacks Tag 01WD. Over an arbitrary base scheme S the product ℙⁿ_S ×_S ℙᵐ_S admits a closed immersion into ℙ^{nm+n+m}_S over S.

public theorem exists_segreEmbedding (S : Scheme.{u}) :
    ∃ f : pullback ((projectiveSpaceOver n S) ↘ S) ((projectiveSpaceOver m S) ↘ S) ⟶
        projectiveSpaceOver (n * m + n + m) S,
      IsClosedImmersion f ∧
        f ≫ ((projectiveSpaceOver (n * m + n + m) S) ↘ S) =
          pullback.fst ((projectiveSpaceOver n S) ↘ S) ((projectiveSpaceOver m S) ↘ S) ≫
            ((projectiveSpaceOver n S) ↘ S)
Tag 03GL, a lemma

Tag 03GL in the Stacks Project.

Stacks.ClosedSubschemeProjectiveSpace.closedSubscheme_iso_projQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedSubschemeProjectiveSpace/Basic.lean, line 109. The attribute's comment: “the closed subscheme is the Proj of the quotient”. References: EGA II (2.9.2), “(ii), special case”.

Stacks Tag 03GL, third assertion: Z = Proj(R[T₀, …, Tₙ]/I). Let R be an arbitrary commutative ring and let i : Z ⟶ ℙⁿ_R be a closed subscheme of projective n-space over R. Let I ⊆ R[T₀, …, Tₙ] be the homogeneous ideal generated by the homogeneous polynomials whose twisted global section pulls back to zero on Z — the ideal whose degree-d part is Ker(R[T₀, …, Tₙ]_d ⟶ Γ(Z, 𝒪(d)|_Z)), by the two assertions of the tag registered on Stacks.AlgebraicGeometry.IdealOfClosedSubscheme.mem_idealOfClosedSubscheme_iff and Stacks.AlgebraicGeometry.IdealOfClosedSubscheme.idealOfClosedSubscheme_isHomogeneous.

Then Z is isomorphic to Proj(R[T₀, …, Tₙ]/I), compatibly with the two morphisms into ℙⁿ_R: the closed immersion i itself, and the canonical morphism Stacks.ClosedSubschemeProjQuotient.ambientHom read through the comparison. So the two are equal as closed subschemes of projective space.

No hypothesis is placed on R; in particular it need not be Noetherian.

theorem closedSubscheme_iso_projQuotient {Z : Scheme.{u}}
    (i : Z ⟶ AlgebraicGeometry.projectiveSpaceOverRing n (CommRingCat.of R))
    [IsClosedImmersion i] :
    ∃ e : Z ≅ projQuotient (polyGrading R n) (i ≫ (comparisonIso R n).hom),
      e.hom ≫ ambientHom (polyGrading R n) (i ≫ (comparisonIso R n).hom) ≫
        (comparisonIso R n).inv = i

Declarations registered for the tag:

Tag 03GM, a lemma

Tag 03GM in the Stacks Project.

Stacks.AlgebraicGeometry.ProjTwistComparisonIso.gradedModule_and_isIso_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TensorSectionNonvanishing/ProjTwistComparisonIsoStatement.lean, line 125. The attribute's comment: “both assertions of the tag in one statement, for a quasi-coherent ℱ on ℙᵐ_R: the twisted global sections M = ⨁_{d ≥ 0} Γ(ℙᵐ_R, ℱ(d)) form a graded R[T₀, …, Tₘ]-module -- internally graded, with the grading of the ring acting on the grading of M, the action being the multiplication map of the twists of Equation 03GK -- and the canonical comparison M̃ ⟶ ℱ, the unique morphism restricting on each positive-degree standard open D₊(f) to x / f ^ n ↦ x|_{D₊(f)} ⊗ f ^ (-n), is an isomorphism”.

[Stacks, Tag 03GM]. Let R be a ring and let ℱ be a quasi-coherent sheaf on ℙᵐ_R. For d ≥ 0 put M_d = Γ(ℙᵐ_R, ℱ(d)). Then M = ⨁_{d ≥ 0} M_d is a graded R[T₀, …, Tₘ]-module and there is a canonical isomorphism ℱ = M̃.

The first conjunct is the graded-module assertion, in three parts: the integer grading decomposes M internally, the grading of R[T₀, …, Tₘ] acts on that grading, and the action of a homogeneous element is the multiplication map of the twists of Equation 03GK. The second and third are the canonical isomorphism: the comparison M̃ ⟶ ℱ is the unique morphism restricting on each positive-degree standard open D₊(f) to x / f ^ n ↦ x|_{D₊(f)} ⊗ f ^ (-n), and it is invertible.

The source's omitted injectivity and surjectivity arguments are Stacks.AlgebraicGeometry.ProjTwistChartBijective.exists_pow_smul_eq_zero_of_numerSection_eq_zero and Stacks.AlgebraicGeometry.ProjTwistChartBijective.exists_numerSection_eq.

theorem gradedModule_and_isIso_comparison
    (F : SheafOfModules.{u} (projRingSheaf (projectiveGrading m R)))
    (hqc : SheafOfModules.IsQuasicoherent
      (R := (AlgebraicGeometry.Proj (projectiveGrading m R)).ringCatSheaf) F) :
    (DirectSum.IsInternal (moduleGrading (projectiveGrading m R) F) ∧
        SetLike.GradedSMul (projectiveGrading m R)
          (moduleGrading (projectiveGrading m R) F) ∧
        ∀ (e k : ℕ) (a : projectiveGrading m R e)
          (s : twistSections (projectiveGrading m R) F k),
          (a : MvPolynomial (Fin (m + 1)) R) •
              DirectSum.of (twistSections (projectiveGrading m R) F) k s =
            DirectSum.of (twistSections (projectiveGrading m R) F) (e + k)
              (gsmul (projectiveGrading m R) F a.2 k (e + k) rfl s)) ∧
      (∃! φ : associatedTwistSectionSheaf (projectiveGrading m R) F ⟶ F,
          ∀ p : PositiveElem (projectiveGrading m R),
            φ.val.app (op (positiveBasicOpen (projectiveGrading m R) p)) =
              positiveChartHom (projectiveGrading m R) F p) ∧
      IsIso (comparison (projectiveGrading m R) F)
Tag 0B3B, a lemma

Tag 0B3B in the Stacks Project.

Stacks.SheafOfModules.kernelTensorGeneratingSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/Generators/KernelTensorInvertible.lean, line 668.

Stacks 0B3B. Let L be an invertible sheaf of modules on a locally ringed space, let s : I → Γ(X, L) be global sections generating L, and let F be the kernel of the induced map O_X^{⊕I} ⟶ L. Then F ⊗ L is generated by global sections, by the Koszul sections e_i ⊗ s_j − e_j ⊗ s_i.

noncomputable def kernelTensorGeneratingSections (g : L.GeneratingSections) :
    ((((Stacks.SheafOfModules.Tensor.sheafTensor.{u, u, u, u, u}
        (⟨X.presheaf, X.IsSheaf⟩ : Sheaf (JX X) CommRingCat.{u})).obj ((kernel g.π))).obj
        (L))).GeneratingSections
Sources
LeanStacks.ProjectiveFromSections.toProjectiveSpaceOver · Stacks.ProjectiveSpaceModuli.bijective_pointsOfHom · Stacks.ProjectiveSpaceModuli.pointsEquiv · Stacks.ProjectiveSpaceModuli.pointsOfHom_comp · AlgebraicGeometry.projectiveSpace · AlgebraicGeometry.projectiveSpaceIntegralIso · AlgebraicGeometry.projectiveSpaceOver · AlgebraicGeometry.projectiveSpaceOverRing

Section27.14 Invertible sheaves and morphisms into Proj#

Section 27.14 of the Stacks Project, Tag 01NJ. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01NK, a lemma

Tag 01NK in the Stacks Project.

Stacks.AlgebraicGeometry.ProjChartGradedTripleTag.tag01NK, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjChartGradedTripleTag.lean, line 95. The attribute's comment: “the open U(psi), the morphism r_{L,psi} : U(psi) -> Proj A and the unital map of Z-graded algebras theta : r^*(sum_d O_X(d)) -> sum_d L^{tensor d}|_{U(psi)}; properties (1) and (2); every triple (U', r', theta') with (1) and (2) equals (U(psi), r, theta); and for d >= 1 and an open V on which psi(A_d) generates L^{tensor d}, the pair (phi, alpha) attached to the Veronese restriction of psi to V exists uniquely, r|_V = phi, and theta|_V in degree d equals alpha”.

Let A be a graded ring, X = Proj A, T a scheme, L an invertible 𝒪_T-module and ψ : A → Γ_*(T, L) a homomorphism of graded rings. Put U(ψ) = ⋃_{f ∈ A_+ homogeneous} T_{ψ(f)}. Then ψ induces the canonical morphism r_{L, ψ} = ψ.glued : U(ψ) ⟶ X and the map of ℤ-graded algebras θ = theta 𝒜 ψ : r_{L, ψ}^*(⨁_{d ∈ ℤ} 𝒪_X(d)) ⟶ ⨁_{d ∈ ℤ} L^{⊗ d}|_{U(ψ)}, and:

  1. U(ψ) is the union of the T_{ψ(f)} (by definition);
  2. θ preserves the unit;
  3. property (1): r_{L, ψ}^{-1}(D₊(f)) = T_{ψ(f)} for f ∈ A_+ homogeneous;
  4. property (2): for every d ≥ 0 and a ∈ A_d, θ carries the pullback of the global section of 𝒪_X(d) attached to a (the map of [Stacks, Tag 01MP]) to ψ(a)|_{U(ψ)} — the commutativity of the square of the tag;
  5. the characterization: every triple (U', r', θ') — an open of T, a morphism U' ⟶ X and a map of graded algebras r'^*(⨁ 𝒪_X(d)) ⟶ ⨁ L^{⊗ d}|_{U'} — with properties (1) and (2) is (U(ψ), r_{L, ψ}, θ);
  6. the final assertion: for d ≥ 1 and an open V ⊆ T on which the sections ψ(A_d) generate L^{⊗ d}|_V, the pair (φ, α) of [Stacks, Tag 01N8] for ψ|_{A^{(d)}} : A^{(d)} → Γ_*(V, L^{⊗ d}) exists and is unique, and for it r_{L, ψ}|_V = φ and the restriction of the degree-d part of θ to V, read through the canonical identifications (r_{L, ψ}|_V)^*𝒪_X(d) = φ^*𝒪_X(d) and L^{⊗ d}|_{U(ψ)}|_V = L|_V^{⊗ d}, is α.

The value ψ(a) is read in the tensor powers of [Stacks, Tag 01CU] that the Laurent algebra is made of, through the canonical comparison Stacks.AlgebraicGeometry.ProjChartGradedDivision.intValue. The sections ψ(A_d) generate L^{⊗ d}|_V exactly when their nonvanishing opens cover V.

theorem tag01NK :
    ψ.coveringOpen
        = ⨆ p : (e : ℕ) × 𝒜 (e + 1),
            nonvanishingOpen T (natTensorPow L (p.1 + 1)) (ψ.toFun (p.1 + 1) p.2)
      ∧ SheafOfModules.sectionsMap ((theta 𝒜 ψ).app 0)
          (Stacks.Conormal.gradedPullback ψ.glued
            (Stacks.AlgebraicGeometry.ProjConeTwist.integerTwistAlgebra 𝒜)).one
        = (laurentRestrict 𝒜 ψ).one
      ∧ (∀ {e : ℕ} {f : A} (hf : f ∈ 𝒜 e), 0 < e →
          ψ.coveringOpen.ι ''ᵁ (ψ.glued ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜 f)
            = nonvanishingOpen T (natTensorPow L e) (ψ.toFun e ⟨f, hf⟩))
      ∧ (∀ (d : ℕ) {a : A} (ha : a ∈ 𝒜 d),
          ((theta 𝒜 ψ).app (d : ℤ)).val.app (op ⊤)
              (Scheme.Modules.pullbackSection ψ.glued (twistM 𝒜 (d : ℤ)) ⊤ ⊤
                (fun _ _ => trivial) (degreeSection 𝒜 d ⟨a, ha⟩))
            = resTop (tensorPowerModule T L (d : ℤ)) (intValue ψ d ⟨a, ha⟩)
                (ψ.coveringOpen.ι ''ᵁ ⊤))
      ∧ (∀ t : Triple 𝒜 L, IsTriple ψ t → t = canonicalTriple ψ)
      ∧ (∀ {d : ℕ} (hd : 0 < d) {V : T.Opens}
          (hVgen : V ≤ ⨆ g : 𝒜 d, nonvanishingOpen T (natTensorPow L d) (ψ.toFun d g)),
          (∃! p : Pair 𝒜 (natTensorPow ((Scheme.Modules.pullback V.ι).obj L) d) d,
              IsCompatible 𝒜 (veroneseAt 𝒜 (GradedSections.pullback V.ι ψ) d) p) ∧
          ∀ p : Pair 𝒜 (natTensorPow ((Scheme.Modules.pullback V.ι).obj L) d) d,
            IsCompatible 𝒜 (veroneseAt 𝒜 (GradedSections.pullback V.ι ψ) d) p →
            ∃ h : T.homOfLE (hVgen.trans (iSup_nonvanishingOpen_le_coveringOpen 𝒜 ψ hd))
                ≫ ψ.glued = toProj 𝒜 p.1,
              (Scheme.Modules.pullbackCongr h.symm).hom.app (twistM 𝒜 (d : ℤ))
                ≫ (Scheme.Modules.pullbackComp
                    (T.homOfLE (hVgen.trans (iSup_nonvanishingOpen_le_coveringOpen 𝒜 ψ hd)))
                    ψ.glued).inv.app (twistM 𝒜 (d : ℤ))
                ≫ (Scheme.Modules.pullback
                    (T.homOfLE (hVgen.trans (iSup_nonvanishingOpen_le_coveringOpen 𝒜 ψ hd)))).map
                    ((theta 𝒜 ψ).app (d : ℤ))
                ≫ (Scheme.Modules.pullback
                    (T.homOfLE (hVgen.trans (iSup_nonvanishingOpen_le_coveringOpen 𝒜 ψ hd)))).map
                    ((Scheme.Modules.restrictFunctorIsoPullback ψ.coveringOpen.ι).hom.app
                      (tensorPowerModule T L (d : ℤ)))
                ≫ (Scheme.Modules.pullbackComp
                    (T.homOfLE (hVgen.trans (iSup_nonvanishingOpen_le_coveringOpen 𝒜 ψ hd)))
                    ψ.coveringOpen.ι).hom.app (tensorPowerModule T L (d : ℤ))
                ≫ (Scheme.Modules.pullbackCongr (T.homOfLE_ι _)).hom.app
                    (tensorPowerModule T L (d : ℤ))
                ≫ (Scheme.Modules.pullback V.ι).map (powCompare L d).inv
                ≫ (pullbackNatTensorPowIso V.ι L d).inv
                = p.2.hom)
Tag 01NL, a remark

Tag 01NL in the Stacks Project.

Stacks.AlgebraicGeometry.ProjInvertibleLocusEscape.not_range_subset_whereInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjInvertibleLocusEscape.lean, line 414.

Let k be a field, let S = k[A, B, C] be graded by deg A = 1, deg B = 2, deg C = 3 and set X = Proj S. Let T = 𝐏²_k = Proj k[X₀, X₁, X₂] with 𝓛 = 𝒪_T(1), so 𝒪_T(n) = 𝓛^{⊗ n}, and let ψ : S → Γ_*(T, 𝓛) be the composite of the degree-preserving homomorphism A ↦ X₀, B ↦ X₁², C ↦ X₂³ with the canonical graded ring map of Tag 01MP. The image of the induced morphism r_{𝓛, ψ} : T → X is not contained in the invertible locus W₁ of 𝒪_X(1) — the largest open of X on which all the twists 𝒪_X(n) are invertible and all their multiplication maps are isomorphisms, Tag 01MU. Indeed the point of X given by the homogeneous prime (A, B) is in the image, and a homogeneous element of S outside (A, B) has degree divisible by 3, so no two of them have degrees differing by 1.

public theorem not_range_subset_whereInvertible :
    ¬ Set.range (mapHom E.naturalGrading (projectiveGrading E) (coverHom E)).base ⊆
      ↑(whereInvertible E.naturalGrading 1)
Sources
LeanStacks.AlgebraicGeometry.ProjChartGradedTripleTag.tag01NK · Stacks.AlgebraicGeometry.ProjInvertibleLocusEscape.not_range_subset_whereInvertible

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.