27.15 Relative Proj via glueing to 27.22 Grassmannians

Section27.15 Relative Proj via glueing #

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

Tag 01NN, a situation

Tag 01NN in the Stacks Project.

Stacks.RelativeProj.Situation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/RelativeProjSectionRings.lean, line 80. The attribute's comment: “the situation datum, on the SheafOfModules.GradedAlgebra substrate”. References: EGA II (8.3.1), “partial”.

Stacks Project, Tag 01NN. A scheme equipped with a graded algebra over its structure sheaf, each of whose homogeneous pieces is quasi-coherent. The algebra is commutative and concentrated in nonnegative degrees.

public structure Situation

Stacks.RelativeProj.Situation.sectionRingStructure_exists, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/RelativeProjSectionRings.lean, line 330. The attribute's comment: “graded rings of local sections”.

The canonical nonnegatively graded rings of local sections of a quasi-coherent graded algebra, with their structure-sheaf maps and restriction maps.

public theorem sectionRingStructure_exists (s : Situation.{u}) :
    Nonempty (s.SectionRingStructure)

Stacks.AlgebraicGeometry.RelativeProjBridge.SheafGradedAlgebra, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjBridge/Algebra.lean, line 85. The attribute's comment: “the situation datum, on the sheaf-level bilinear-multiplication substrate”.

A commutative, nonnegatively graded, quasi-coherent graded 𝒪_S-algebra, given as a family of sheaves of modules with an 𝒪_S-bilinear multiplication and a global unit.

This is the sheaf-level data of Situation 01NN.

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

Stacks.AlgebraicGeometry.RelativeProjBridge.SheafGradedAlgebra.resRingHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjBridge/Basic.lean, line 162. The attribute's comment: “graded rings of local sections”.

Restriction of the graded rings of sections, as a ring homomorphism.

public noncomputable def resRingHom {U V : S.Opens} (h : U ≤ V) :
    A.sectionRing V →+* A.sectionRing U

Stacks.AlgebraicGeometry.RelativeProjBridge.SheafGradedAlgebra.resRingHom_of, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjBridge/Basic.lean, line 175. The attribute's comment: “graded rings of local sections”.

On a homogeneous summand, resRingHom is restriction of homogeneous sections.

public theorem resRingHom_of {U V : S.Opens} (h : U ≤ V) {n : ℕ} (y : A.sectionPieces V n) :
    A.resRingHom h (DirectSum.of (A.sectionPieces V) n y) =
      DirectSum.of (A.sectionPieces U) n (A.resPiece h n y)

Stacks.AlgebraicGeometry.RelativeProjBridge.SheafGradedAlgebra.resRingHom_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjBridge/Basic.lean, line 194. The attribute's comment: “graded rings of local sections”.

Restriction along the identity of an open is the identity.

public theorem resRingHom_id (U : S.Opens) : A.resRingHom (le_refl U) = RingHom.id _

Stacks.AlgebraicGeometry.RelativeProjBridge.SheafGradedAlgebra.resRingHom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjBridge/Basic.lean, line 202. The attribute's comment: “graded rings of local sections”.

Restriction along a composite of inclusions is the composite of the restrictions.

public theorem resRingHom_comp {U V W : S.Opens} (hUV : U ≤ V) (hVW : V ≤ W) :
    A.resRingHom (hUV.trans hVW) = (A.resRingHom hUV).comp (A.resRingHom hVW)

Stacks.AlgebraicGeometry.RelativeProjBridge.SheafGradedAlgebra.resRingHom_strHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjBridge/Basic.lean, line 212. The attribute's comment: “graded rings of local sections”.

Restriction is compatible with the structure maps from the functions on the opens.

public theorem resRingHom_strHom {U V : S.Opens} (h : U ≤ V) (r : Γ(S, V)) :
    A.resRingHom h (A.strHom V r) = A.strHom U (S.presheaf.map (homOfLE h).op r)

Stacks.AlgebraicGeometry.RelativeProjBridge.SheafGradedAlgebra.instGCommRing, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjBridge/SectionRing.lean, line 136. The attribute's comment: “graded rings of local sections”.

Stacks 01NN, the graded rings of local sections. The homogeneous sections of a quasi-coherent graded algebra over an open form a graded commutative ring, whose multiplication and unit are the algebra's own: see the characterizing equations below.

public noncomputable instance instGCommRing : DirectSum.GCommRing (A.sectionPieces U)

Stacks.AlgebraicGeometry.RelativeProjBridge.SheafGradedAlgebra.strHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjBridge/SectionRing.lean, line 244. The attribute's comment: “graded rings of local sections”.

The structure map from the sections of 𝒪_S over an open to the graded ring of sections of A: a function is sent to its multiple of the unit.

public noncomputable def strHom : Γ(S, U) →+* A.sectionRing U

Stacks.AlgebraicGeometry.RelativeProjBridge.SheafGradedAlgebra.strHom_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjBridge/SectionRing.lean, line 256. The attribute's comment: “graded rings of local sections”.

The structure map sends a function to its multiple of the unit, in degree 0.

public theorem strHom_apply (r : Γ(S, U)) :
    A.strHom U r = DirectSum.of (A.sectionPieces U) 0 (r • A.one U)

AlgebraicGeometry.Space.relativeProjChartAlgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GradedAlgebraChartRestriction.lean, line 279. The attribute's comment: “the restriction of a graded algebra on an algebraic space to an étale scheme chart, as graded algebra data on the chart; granted quasi-coherence of the module restrictions of the homogeneous pieces, which is the étale-to-Zariski direction of Descent 03DX and is carried here in the same form as in the neighbouring Tag 060Q”.

The restriction 𝒜|_V of a graded algebra on an algebraic space to an étale scheme chart, as graded algebra data in the sense of Situation 01NN. This is the object the scheme-level theory of the relative Proj consumes, so it is what makes a reduction to the case of schemes on an étale chart possible.

Commutativity and concentration in nonnegative degrees are transported from 𝒜. Quasi-coherence of the restricted pieces is the hypothesis hqc; see the implementation notes for why it is carried and why it is an input rather than a disguised conclusion.

def relativeProjChartAlgebra
    (hcomm : ∀ (i j : ℤ) (W : (SmallEtale B S hS X.1)ᵒᵖ) (a : (A.piece i).val.obj W)
      (b : (A.piece j).val.obj W), HEq ((A.mul i j).app W a b) ((A.mul j i).app W b a))
    (hneg : ∀ (n : ℤ), n < 0 → ∀ (W : (SmallEtale B S hS X.1)ᵒᵖ)
      (y : (A.piece n).val.obj W), y = 0)
    (hqc : ∀ n : ℤ, (restrictToChartScheme B S hS X.1 X.2 (A.piece n) V).IsQuasicoherent) :
    SheafGradedAlgebra (chartScheme V)

AlgebraicGeometry.Space.relativeProjChartSituation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeProjChartSituation.lean, line 206. The attribute's comment: “the relative Proj situation carried on an étale scheme chart by the restriction of a graded algebra on an algebraic space, granted quasi-coherence of the module restrictions of the homogeneous pieces, which is the étale-to-Zariski direction of Descent 03DX”.

The tie: the relative Proj situation of Stacks 01NN carried by the restriction of 𝒜 to an étale scheme chart.

The base is the scheme underlying the chart and the graded algebra is the restriction 𝒜|_V of AlgebraicGeometry.Space.chartSheafAlgebra. Commutativity and concentration in nonnegative degrees are the corresponding fields of the space-level situation, transported; quasi-coherence of the restricted pieces is the hypothesis hqc, for the reason given in the implementation notes.

This is the datum that AlgebraicGeometry.Space.RelativeProjChart lacks: that structure takes an arbitrary situation t on the chart, with no field relating it to the graded algebra on the space.

def relativeProjChartSituation
    (hqc : ∀ n : ℤ, (restrictToChartScheme s.site s.base s.containsBase s.space.1 s.space.2
      (s.algebra.piece n) V).IsQuasicoherent) :
    Stacks.RelativeProj.Situation.{u}

Tag 01NO, a lemma

Tag 01NO in the Stacks Project.

Stacks.Blowup.isOpenImmersion_proj_map_reesRestrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ReesSheafData.lean, line 127. The attribute's comment: “open immersion, for the Rees algebra of a quasi-coherent ideal sheaf”.

For affine opens U ≤ V, the comparison morphism of charts Proj (Γ(S, U)[ℐ(U)t]) ⟶ Proj (Γ(S, V)[ℐ(V)t]) is an open immersion.

theorem isOpenImmersion_proj_map_reesRestrict {U V : S.affineOpens} (h : U ≤ V) :
    IsOpenImmersion (Proj.map (reesRestrict ℐ h) (reesIrrelevant_le ℐ h))

Stacks.Blowup.opensRange_proj_map_reesRestrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ReesSheafData.lean, line 176. The attribute's comment: “image is the preimage, for the Rees algebra of a quasi-coherent ideal sheaf”.

For affine opens U ≤ V, the image of the comparison morphism of charts is the preimage of U in the chart over V.

theorem opensRange_proj_map_reesRestrict {U V : S.affineOpens} (h : U ≤ V) :
    Stacks.RelativeProj.chartToOpen (fun W : S.affineOpens ↦ reesGrading (ℐ.ideal W)) V
        (reesBase ℐ V) ⁻¹ᵁ (S.homOfLE h).opensRange =
      (Proj.map (reesRestrict ℐ h) (reesIrrelevant_le ℐ h)).opensRange

Stacks.AlgebraicGeometry.ProjInclusionTwist.isIso_projInclusionTwistMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjInclusionTwist/Basic.lean, line 201. The attribute's comment: “canonical twist isomorphisms”.

Tag 01NO's transported comparison map on the n-th twist is an isomorphism, for every n : ℤ and for an arbitrary inclusion of affine opens of the base, with no hypothesis beyond that situation.

public theorem isIso_projInclusionTwistMap (U V : S.Opens) (h : U ≤ V) (hU : IsAffineOpen U)
    (hV : IsAffineOpen V) (n : ℤ) :
    IsIso (projInclusionTwistMap A U V h hU hV n)

Stacks.AlgebraicGeometry.RelativeProj.projInclusionDomain_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProj/Assembled.lean, line 154. The attribute's comment: “the everywhere-defined morphism”.

Tag 01NO, the everywhere-defined morphism. For an inclusion U ⊆ V of affine opens of the base, the morphism of projective spectra induced by restriction of homogeneous sections is defined on all of Proj Γ(U, A).

This is Stacks.AlgebraicGeometry.RelativeProjGeneral.mapDomain_res_eq_top_of_le_opens for the graded algebra the bridge produces.

public theorem projInclusionDomain_eq_top (U V : S.Opens) (h : U ≤ V)
    (hU : IsAffineOpen U) (hV : IsAffineOpen V) :
    mapDomain (A.grading V) (A.grading U) (A.res h) = ⊤

Stacks.AlgebraicGeometry.RelativeProj.projInclusion_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProj/Assembled.lean, line 184. The attribute's comment: “the cartesian square”.

Tag 01NO, the cartesian square. For an inclusion U ⊆ V of affine opens of the base, the square formed by the induced morphism of projective spectra, the two structure morphisms to the affine opens and the inclusion U ⊆ V is cartesian.

This is Stacks.AlgebraicGeometry.RelativeProjGeneral.isPullback_transition_of_le_opens for the graded algebra the bridge produces.

public theorem projInclusion_isPullback (U V : S.Opens) (h : U ≤ V)
    (hU : IsAffineOpen U) (hV : IsAffineOpen V) :
    IsPullback (projInclusionMap A U V h hU hV) (projInclusionToOpen A U hU)
      (projInclusionToOpen A V hV) (S.homOfLE h)

Stacks.RelativeProj.Situation.projInclusionDomain_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProj/Charts/Basic.lean, line 237. The attribute's comment: “the everywhere-defined morphism”.

Stacks Project, Tag 01NO. The morphism of projective spectra induced by restriction of homogeneous sections along an inclusion of affine opens is defined on all of Proj (s.sectionRingGrading U).

public theorem projInclusionDomain_eq_top (hU : IsAffineOpen U) (hV : IsAffineOpen V) :
    mapDomain (s.sectionRingGrading V) (s.sectionRingGrading U)
      (gradedSectionRestriction s U V h) = ⊤

Stacks.RelativeProj.Situation.projInclusion_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProj/Charts/Descent.lean, line 299. The attribute's comment: “the cartesian square”.

Stacks Project, Tag 01NO. The square formed by the comparison morphism of charts, the two chart structure morphisms and the inclusion of affine opens of the base is cartesian.

public theorem projInclusion_isPullback {W W' : s.base.Opens} (h : W ≤ W')
    (hW : IsAffineOpen W) (hW' : IsAffineOpen W') :
    IsPullback (projInclusionMap s W W' h hW hW') (projInclusionToOpen s W hW)
      (projInclusionToOpen s W' hW') (s.base.homOfLE h)

Stacks.RelativeProj.Situation.isIso_twistMap_gradedSectionRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProj/Twist/Descent.lean, line 242. The attribute's comment: “the canonical twist isomorphisms θ, for an arbitrary inclusion of affine opens of the base; their compatibility with the multiplication maps is not covered”.

Stacks Project, Tag 01NO. The canonical comparison θ : r^* 𝒪_{Proj 𝒜(W')}(n) ⟶ 𝒪_{Proj 𝒜(W)}(n) attached to an inclusion W ≤ W' of affine opens of the base is an isomorphism, for every n : ℤ.

theorem isIso_twistMap_gradedSectionRestriction {W W' : s.base.Opens} (h : W ≤ W')
    (hW : IsAffineOpen W) (hW' : IsAffineOpen W') (n : ℤ) :
    IsIso (twistMap (gradedSectionRestriction s W W' h)
      (irrelevant_le_map_gradedSectionRestriction s W W' h hW hW') n)

Stacks.ProjTwistComparison.isIso_twistMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProj/Twist/Iso.lean, line 151. The attribute's comment: “the twist comparison is an isomorphism, for a degreewise localization away from a degree-zero element; the descent to a general affine open and the compatibility with the multiplication maps are not covered”.

The canonical twist comparison of a degreewise localization is an isomorphism. If φ is, in each degree, the localization of 𝒜 away from a degree-zero element g, then for every n the comparison θ : r^* 𝒪_{Proj 𝒜}(n) ⟶ 𝒪_{Proj ℬ}(n) is an isomorphism.

theorem isIso_twistMap {g : A} (h : Stacks.GradedLocalization.IsAwayDegreewise φ g)
    (hg : g ∈ 𝒜 0) : IsIso (twistMap φ hφ n)

Stacks.ProjTwistComparison.sectionsMap_twistSectionsMul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProj/Twist/Multiplication.lean, line 158. The attribute's comment: “the compatibility of the twist comparison with the multiplication of twisted sections, i.e. with the pointwise product of fraction families; the compatibility with the sheaf-level multiplication maps 𝒪(p) ⊗ 𝒪(q) ⟶ 𝒪(p + q) is not covered”.

The twist comparison is compatible with the multiplication of twisted sections. The comparison of a product of a degree-p and a degree-q section is the product of the comparisons; this is the multiplicativity of the comparison of local rings, applied at each point.

theorem sectionsMap_twistSectionsMul (p q : ℤ) (U : Opens (ProjectiveSpectrum.top 𝒜))
    (a : moduleSections 𝒜 (twistGrading (S := A) 𝒜 p) U)
    (b : moduleSections 𝒜 (twistGrading (S := A) 𝒜 q) U) :
    sectionsMap φ hφ (p + q) U (twistSectionsMul 𝒜 p q U a b) =
      twistSectionsMul ℬ p q (U.comap (ProjectiveSpectrum.comap φ hφ))
        (sectionsMap φ hφ p U a) (sectionsMap φ hφ q U b)

Stacks.AlgebraicGeometry.TwistMultCompat.projInclusionTwistIso_preserves_products, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TwistMultCompat/Basic.lean, line 179. The attribute's comment: “multiplication compatibility of twist isomorphisms”.

Tag 01NO, multiplication compatibility of twist isomorphisms. For an inclusion U ⊆ V of affine opens of the base of a quasi-coherent graded algebra and any two twist indices n, m : ℤ, the canonical isomorphisms on the twists of the induced morphism of projective spectra are compatible with the multiplication maps of Tag 01MU: the pulled-back multiplication followed by the comparison on the (n + m)-th twist is the tensor product of the comparisons on the n-th and the m-th twists followed by the multiplication map downstairs.

The hypotheses are exactly those of the tagged statement: a quasi-coherent graded algebra on a scheme, two affine opens, an inclusion between them, and two unrestricted twist indices.

public theorem projInclusionTwistIso_preserves_products :
    pullbackTwistMultiplication (A.grading V) (projInclusionMap A U V h hU hV) n m ≫
        (projInclusionTwistIso A U V h hU hV (n + m)).hom =
      ((Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor.{u, u, u, u, u}
          ⟨(((AlgebraicGeometry.Proj (A.grading U)).toRingedSpace)).presheaf,
            (((AlgebraicGeometry.Proj (A.grading U)).toRingedSpace)).IsSheaf⟩)).map
          (X := ((Scheme.Modules.pullback (projInclusionMap A U V h hU hV)).obj
            (twistingSheaf (A.grading V) n),
            (Scheme.Modules.pullback (projInclusionMap A U V h hU hV)).obj
              (twistingSheaf (A.grading V) m)))
          (Y := (twistingSheaf (A.grading U) n, twistingSheaf (A.grading U) m))
          (((projInclusionTwistIso A U V h hU hV n).hom,
            (projInclusionTwistIso A U V h hU hV m).hom) : (_, _) ⟶ (_, _))) ≫
        twistMultiplicationMap (A.grading U) n m

Tag 01NP, a lemma

Tag 01NP in the Stacks Project.

Stacks.RelativeProj.Situation.projInclusionMap_and_twistMap_trans, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjSituation/Transitive.lean, line 157. The attribute's comment: “both assertions of the tag as one statement, in the shape of Situation 01NN: the composition law for the tag-01NO morphisms r, and the similar law for the comparison isomorphisms θ”.

Stacks Project, Tag 01NP, both of its assertions as one statement. In Situation 01NN, let U ⊆ U' ⊆ U'' be affine opens of the base and put A = 𝒜(U), A' = 𝒜(U'), A'' = 𝒜(U'') for the graded rings of local sections. Then:

the composition of the tag-01NO morphisms r : Proj A ⟶ Proj A' and r' : Proj A' ⟶ Proj A'' is the tag-01NO morphism r'' : Proj A ⟶ Proj A'' of the inclusion U ⊆ U'';

the similar statement holds for the tag-01NO comparison isomorphisms θ: for every degree n, every open V of Proj A'', every section a of 𝒪_{Proj A''}(n) over V and every point of Proj A lying over V, the composite of θ and θ' and the comparison θ'' of the outer inclusion read the same degree-n fraction.

The two conjuncts are Stacks.RelativeProj.Situation.projInclusionMap_trans and Stacks.RelativeProj.Situation.twistMap_gradedSectionRestriction_trans.

public theorem projInclusionMap_and_twistMap_trans (U U' U'' : s.base.Opens) (hUU' : U ≤ U')
    (hU'U'' : U' ≤ U'') (hU : IsAffineOpen U) (hU' : IsAffineOpen U')
    (hU'' : IsAffineOpen U'') :
    (projInclusionMap s U U' hUU' hU hU' ≫ projInclusionMap s U' U'' hU'U'' hU' hU'' =
        projInclusionMap s U U'' (hUU'.trans hU'U'') hU hU'') ∧
      ∀ (n : ℤ) (V : Opens (ProjectiveSpectrum.top (s.sectionRingGrading U'')))
          (a : moduleSections (s.sectionRingGrading U'')
            (twistGrading (S := s.sectionRing U'') (s.sectionRingGrading U'') n) V)
          (y : V.comap (ProjectiveSpectrum.comap
            (gradedSectionRestriction s U U'' (hUU'.trans hU'U''))
            (irrelevant_le_map_gradedSectionRestriction s U U'' (hUU'.trans hU'U'') hU hU''))),
        (sectionsMap (gradedSectionRestriction s U U'' (hUU'.trans hU'U''))
            (irrelevant_le_map_gradedSectionRestriction s U U'' (hUU'.trans hU'U'') hU hU'')
            n V a).1 y
          = (sectionsMap (gradedSectionRestriction s U U' hUU')
              (irrelevant_le_map_gradedSectionRestriction s U U' hUU' hU hU') n
              (V.comap (ProjectiveSpectrum.comap (gradedSectionRestriction s U' U'' hU'U'')
                (irrelevant_le_map_gradedSectionRestriction s U' U'' hU'U'' hU' hU'')))
              (sectionsMap (gradedSectionRestriction s U' U'' hU'U'')
                (irrelevant_le_map_gradedSectionRestriction s U' U'' hU'U'' hU' hU'') n V a)).1
              ⟨y.1, mem_comap_comap_of_eq_comp (gradedSectionRestriction s U' U'' hU'U'')
                (irrelevant_le_map_gradedSectionRestriction s U' U'' hU'U'' hU' hU'')
                (gradedSectionRestriction s U U' hUU')
                (irrelevant_le_map_gradedSectionRestriction s U U' hUU' hU hU')
                (irrelevant_le_map_gradedSectionRestriction s U U'' (hUU'.trans hU'U'') hU hU'')
                (gradedSectionRestriction_comp s U U' U'' hUU' hU'U'') y.2⟩

Tag 01NQ, a lemma

Tag 01NQ in the Stacks Project.

Stacks.AlgebraicGeometry.RelativeProj.relativeProj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProj/Assembled.lean, line 224. References: EGA II (3.1.2), “existence”; EGA II (8.3.1).

Tag 01NQ. The relative homogeneous spectrum of a quasi-coherent graded algebra on a scheme, together with its structure morphism to the base and its canonical affine charts.

The scheme is the colimit of the chart functor on the small affine Zariski site of the base; the chart over an affine open is the colimit inclusion, and it is cartesian over that affine open because the relative glueing datum's squares are. Compatibility of the charts with the transitions holds for the arrows of the site by the defining equation of the colimit, and for an arbitrary inclusion of affine opens by Stacks.AlgebraicGeometry.RelativeProjGeneral.transition_comp_chart_of_le_opens.

public def relativeProj : RelativeProjData A

Stacks.RelativeProj.Situation.relativeProj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProj/Charts/Descent.lean, line 319. References: EGA II (3.1.2); EGA II (8.3.1), “more general”.

Stacks Project, Tag 01NQ. The relative projective spectrum of a quasi-coherent nonnegatively graded algebra on a scheme: the scheme glued from the projective spectra of the graded rings of local sections over the affine opens of the base.

public noncomputable def relativeProj : Scheme.{u}

Stacks.RelativeProj.Situation.relativeProjToBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProj/Charts/Descent.lean, line 323.

The structure morphism of the relative projective spectrum to its base.

public noncomputable def relativeProjToBase : relativeProj s ⟶ s.base

Stacks.RelativeProj.Situation.relativeProjChart, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProj/Charts/Descent.lean, line 328.

The chart over an affine open of the base, as a morphism into the relative projective spectrum.

public noncomputable def relativeProjChart (W : s.base.affineOpens) :
    Proj (s.sectionRingGrading W.1) ⟶ relativeProj s

Stacks.RelativeProj.Situation.relativeProjChart_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProj/Charts/Descent.lean, line 334.

The chart over W is the part of the relative projective spectrum lying over W. This is the defining property of a relative projective spectrum.

public theorem relativeProjChart_isPullback (W : s.base.affineOpens) :
    IsPullback (relativeProjChart s W) (projInclusionToOpen s W.1 W.2)
      (relativeProjToBase s) W.1.ι

Stacks.RelativeProj.Situation.relativeProjChart_transition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProj/Charts/Descent.lean, line 341.

The charts are compatible with the comparison morphisms of charts.

public theorem relativeProjChart_transition {W W' : s.base.affineOpens} (h : W ≤ W') :
    projInclusionMap s W.1 W'.1 h W.2 W'.2 ≫ relativeProjChart s W' = relativeProjChart s W

Tag 01NR, a lemma

Tag 01NR in the Stacks Project.

Stacks.AlgebraicGeometry.GluedTwistAlgebra.twistDataOfGradedAlgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GluedTwistAlgebra/Assemble.lean, line 507. The attribute's comment: “the existence assertion: the graded twists and the homogeneous-section map, for a quasi-coherent graded algebra on any scheme, with no hypothesis beyond the algebra itself. The two uniqueness assertions are carried by Stacks.AlgebraicGeometry.TwistExistence.isUniqueTwistData and Stacks.AlgebraicGeometry.TwistRigidity.determinesChartIso, which were vacuous until this term existed”.

The twists on the relative projective spectrum of a quasi-coherent graded algebra exist, on no hypothesis beyond the graded algebra itself: the nested cocycle of Tag 01MZ that the glued twists are indexed by is discharged in every integer degree by Stacks.AlgebraicGeometry.ProjTwistCocycle.isNestedCocycle.

public def twistDataOfGradedAlgebra : TwistData A

Stacks.AlgebraicGeometry.TwistExistence.isUniqueTwistData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TwistExistence/Glue.lean, line 230. The attribute's comment: “uniqueness of the complete structure”.

Tag 01NR's first uniqueness assertion. Any two sets of twist data on a relative Proj are carried into each other by a unique isomorphism of graded algebras commuting with the homogeneous-section maps. The existence half is the glued comparison of this file; the uniqueness half is Stacks.AlgebraicGeometry.TwistUnique.isUniqueTwistData_of_exists.

public theorem isUniqueTwistData (A : SheafGradedAlgebra S) : IsUniqueTwistData A

Stacks.AlgebraicGeometry.TwistRigidity.determinesChartIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TwistRigidity/Determines.lean, line 135. The attribute's comment: “uniqueness of the affine-chart identifications”.

An isomorphism of the glued graded algebras of two twist data which commutes with the homogeneous-section maps determines every chart identification, in every integer degree.

public theorem determinesChartIso (A : SheafGradedAlgebra S) : DeterminesChartIso A

Declarations registered for the tag:

Stacks.AlgebraicGeometry.RelativeProjTwists.TwistData.chartIso_mul, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/RelativeProjTwistQcoh/Tags.lean, line 50 (StacksFrontier): “multiplication on affine charts”.
Stacks.AlgebraicGeometry.RelativeProjTwists.TwistData.chartIso_one, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/RelativeProjTwistQcoh/Tags.lean, line 53 (StacksFrontier): “the unit on affine charts”.

Sources

LeanStacks.RelativeProj.Situation · Stacks.RelativeProj.Situation.sectionRingStructure_exists · Stacks.AlgebraicGeometry.RelativeProjBridge.SheafGradedAlgebra · Stacks.AlgebraicGeometry.RelativeProjBridge.SheafGradedAlgebra.resRingHom · Stacks.AlgebraicGeometry.RelativeProjBridge.SheafGradedAlgebra.resRingHom_of · Stacks.AlgebraicGeometry.RelativeProjBridge.SheafGradedAlgebra.resRingHom_id · Stacks.AlgebraicGeometry.RelativeProjBridge.SheafGradedAlgebra.resRingHom_comp · Stacks.AlgebraicGeometry.RelativeProjBridge.SheafGradedAlgebra.resRingHom_strHom

Section27.16 Relative Proj as a functor #

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

Tag 01NS, the section

Tag 01NS in the Stacks Project.

Stacks.AlgebraicGeometry.RelativeProjQcohSheaf.Fd.toBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjQcohSheaf/OverBase.lean, line 97. The attribute's comment: “the projection of F_d to the functor of points of the base, as a natural transformation F_d ⟹ h_S: a class in F_d(T) records a morphism T ⟶ S and the identification is natural in the test scheme. This is the structure that makes representable by a scheme over S (Tag 01NV) and the fibre product h_{S'} ×_{h_S} F_d (Tag 01NT) statable; neither of those is proved here”.

Stacks Project, Section 01NS: the projection F_d ⟹ h_S. A point of F_d(T) is the strict equivalence class of a quadruple (d, f : T → S, L, ψ), and this is the natural transformation sending it to the morphism f it records.

Naturality is the computation Fd.pullback_fst of the morphism to the base of a pulled-back class: it is the composite of the morphism of test schemes with the old one, which is exactly the action of h_S on a morphism.

def Fd.toBase : Fd.functor A d ⟶ yoneda.obj S ⋙ uliftFunctor.{u + 1, u}

Stacks.AlgebraicGeometry.RelativeProjQcohSheaf.Fd.overFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjQcohSheaf/OverBase.lean, line 142. The attribute's comment: “the functor F_d on the category of schemes OVER S, for an arbitrary base scheme: on an object f : T ⟶ S the set of strict equivalence classes of quadruples (d, f, L, psi) with that structure morphism, on a morphism of Sch/S the pullback of a quadruple. The two functor laws are Fd.pullback_id and Fd.pullback_comp. Representability of F_d is Tag 01NV and is not proved here”.

Stacks Project, Section 01NS: the functor F_d : (Sch/S)^{opp} ⟶ Sets. On an object f : T ⟶ S of the category of schemes over S its value is the fibre of F_d(T) over f, that is, the set of strict equivalence classes of quadruples (d, f, L, ψ) with that structure morphism; on a morphism of Sch/S it is the pullback of a quadruple, which lands in the fibre over the new structure morphism because the morphism to the base of a pulled-back class is the composite.

This is the form of F_d the source's phrase "a functor on schemes over S" refers to; the form fibred over Hom(-, S) on all of Sch is ...RelativeProjQcohSheaf.Fd.functor together with the projection Fd.toBase.

def Fd.overFunctor : (Over S)ᵒᵖ ⥤ Type (u + 1)

Stacks.AlgebraicGeometry.RelativeProjQcohSheaf.Quadruple, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjQcohSheaf/Quadruple.lean, line 127. The attribute's comment: “quadruples over a test scheme”.

Stacks Project, Section 01NS. A quadruple (d, f : T → S, L, ψ) over the test scheme T: an invertible 𝒪_T-module L, a homomorphism ψ of graded 𝒪_T-algebras from the pullback of the d-th Veronese regrading of 𝒜 to the Laurent algebra of L, and the requirement that the degree-one component f^*𝒜_d ⟶ L of ψ be surjective.

The integer d and the morphism f are parameters; the pair (L, ψ) is the data.

structure Quadruple (f : T ⟶ S)
    (A : SheafOfModules.GradedAlgebra.{u, u} (structureRingSheaf S.toRingedSpace)) (d : ℤ)

Stacks.AlgebraicGeometry.RelativeProjQcohSheaf.Quadruple.StrictlyEquivalent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjQcohSheaf/Quadruple.lean, line 189. The attribute's comment: “strict equivalence of quadruples”.

Stacks Project, Section 01NS. Two quadruples over the same morphism f are strictly equivalent when there is an isomorphism β : L ≅ L' of their invertible modules with β ∘ ψ = ψ'.

The composite β ∘ ψ is spelled through the isomorphism γ of Laurent algebras induced by β: the condition is that γ be an isomorphism of sheaves of graded algebras whose degree-one component is β and which carries ψ to ψ' in every degree.

def StrictlyEquivalent (P Q : Quadruple f A d) : Prop

Stacks.AlgebraicGeometry.RelativeProjQcohSheaf.Quadruple.strictlyEquivalent_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjQcohSheaf/Quadruple.lean, line 214. The attribute's comment: “strict equivalence of quadruples”.

Strict equivalence of quadruples is an equivalence relation.

theorem strictlyEquivalent_equivalence :
    Equivalence (StrictlyEquivalent (f := f) (A := A) (d := d))

Stacks.AlgebraicGeometry.RelativeProjQcohSheaf.Fd, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjQcohSheaf/Quadruple.lean, line 267. The attribute's comment: “the set of strict equivalence classes of quadruples over a test scheme”.

Stacks Project, Section 01NS. The set F_d(T) of strict equivalence classes of quadruples (d, f : T → S, L, ψ) over the test scheme T.

Strict equivalence relates only quadruples over the same morphism f : T ⟶ S, so the set of classes is fibred over the morphisms T ⟶ S, which is the morphism recorded by a quadruple.

def Fd (A : SheafOfModules.GradedAlgebra.{u, u} (structureRingSheaf S.toRingedSpace)) (d : ℤ)
    (T : Scheme.{u}) : Type (u + 1)

Stacks.AlgebraicGeometry.RelativeProjQcohSheaf.Quadruple.strictlyEquivalent_pullback_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjQcohSheaf/UnionFunctor.lean, line 334. The attribute's comment: “the pullback of a quadruple along the identity morphism of the test scheme is strictly equivalent to the quadruple”.

The pullback of a quadruple along an identity is strictly equivalent to the quadruple.

theorem strictlyEquivalent_pullback_id (P : Quadruple f A d) :
    StrictlyEquivalent (P.pullback (𝟙 T)) P

Stacks.AlgebraicGeometry.RelativeProjQcohSheaf.Quadruple.strictlyEquivalent_pullback_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjQcohSheaf/UnionFunctor.lean, line 343. The attribute's comment: “the pullback of a quadruple along a composite of morphisms of test schemes is strictly equivalent to the twice-pulled-back quadruple”.

The pullback of a quadruple along a composite of morphisms of test schemes is strictly equivalent to the twice-pulled-back quadruple.

theorem strictlyEquivalent_pullback_comp (P : Quadruple f A d) (g : T' ⟶ T) (g' : T'' ⟶ T') :
    StrictlyEquivalent ((P.pullback g).pullback g') (P.pullback (g' ≫ g))

Stacks.AlgebraicGeometry.RelativeProjQcohSheaf.Fd.functor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjQcohSheaf/UnionFunctor.lean, line 375. The attribute's comment: “the functor F_d : Sch^opp -> Sets at a fixed degree d, with both functor laws proved (Fd.pullback_id and Fd.pullback_comp): on objects the set F_d(T) of strict equivalence classes of quadruples of degree d, on morphisms the pullback of a quadruple. Representability of F_d by a scheme is Tag 01NV and is not proved here”.

The functor F_d : Sch^{opp} ⟶ Sets at a fixed degree d. It sends a test scheme T to the set F_d(T) of strict equivalence classes of quadruples (d, f : T → S, L, ψ) of degree d, and a morphism g : T' ⟶ T of test schemes to the map sending the class of a quadruple to the class of its pullback along g.

def Fd.functor (A : SheafOfModules.GradedAlgebra.{u, u} (structureRingSheaf S.toRingedSpace))
    (d : ℤ) : Scheme.{u}ᵒᵖ ⥤ Type (u + 1)

Stacks.AlgebraicGeometry.RelativeProjQcohSheaf.Quadruple.StrictlyEquivalent.pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjQcohSheaf/UnionPullback.lean, line 528. The attribute's comment: “the pullback of a quadruple along a morphism of test schemes respects strict equivalence”.

Stacks Project, Section 01NS: the pullback of a quadruple respects strict equivalence. Strict equivalence is witnessed by an isomorphism of the Laurent algebras carrying ψ to ψ'; laurentPullbackIso carries that witness to one for the pullbacks, and Twisting.pullbackApp_comp_laurentTransport_of_app is the compatibility with ψ.

theorem StrictlyEquivalent.pullback {P Q : Quadruple f A d} (h : StrictlyEquivalent P Q)
    (g : T' ⟶ T) : StrictlyEquivalent (P.pullback g) (Q.pullback g)

Stacks.AlgebraicGeometry.RelativeProjQcohSheaf.Quadruple.Equivalent.pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjQcohSheaf/UnionPullback.lean, line 559. The attribute's comment: “the pullback of a quadruple along a morphism of test schemes respects equivalence of quadruples of possibly different degrees”.

Stacks Project, Section 01NS: the pullback of a quadruple respects equivalence of quadruples of possibly different degrees. Equivalence is the comparison at the common multiple d d' of the two degrees, and the pullback leaves both degrees unchanged.

theorem Equivalent.pullback {P : Quadruple f A d} {Q : Quadruple f A d'} (h : Equivalent P Q)
    (g : T' ⟶ T) : Equivalent (P.pullback g) (Q.pullback g)

Stacks.AlgebraicGeometry.RelativeProjQcohSheaf.Fd.pullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjQcohSheaf/UnionPullback.lean, line 575. The attribute's comment: “the map F_d(T) → F_d(T') of a morphism of test schemes at a fixed degree d, the pullback of a quadruple descended to the strict equivalence classes”.

Stacks Project, Section 01NS: the map F_d(T) → F_d(T') of a morphism g : T' ⟶ T of test schemes, at a fixed degree d. A point of F_d(T) over f : T ⟶ S is a quadruple of degree d over f taken modulo strict equivalence; its image is the pullback of that quadruple, again of degree d, over g ≫ f. This is well defined because the pullback respects strict equivalence (Quadruple.StrictlyEquivalent.pullback), and no identification across degrees is involved.

def Fd.pullback {A : SheafOfModules.GradedAlgebra.{u, u} (structureRingSheaf S.toRingedSpace)}
    {d : ℤ} (g : T' ⟶ T) (ξ : Fd A d T) : Fd A d T'

Tag 01NT, a lemma

Tag 01NT in the Stacks Project.

Stacks.AlgebraicGeometry.RelativeProjQcohSheaf.Fd.baseChangePullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjQcohSheaf/BaseChangeFunctor.lean, line 936. The attribute's comment: “the canonical isomorphism F'_d = h_{S'} x_{h_S} F_d of functors on Sch^opp read off at the categorical fibre product, with its compatibility with both projections (baseChangePullbackIso_hom_fst and _hom_snd), so that it is the canonical isomorphism and not merely some isomorphism. Stated for every integer d”.

Stacks Project, Tag 01NT: the canonical isomorphism F'_d ≅ h_{S'} ×_{h_S} F_d, with the right-hand side the categorical fibre product of the cospan h_{S'} ⟶ h_S ⟵ F_d in the functor category. It is canonical: Fd.baseChangePullbackIso_hom_fst and ..._hom_snd identify its composites with the two projections as the projection of F'_d to the functor of points of S' and the canonical map F'_d ⟹ F_d.

def Fd.baseChangePullbackIso :
    Fd.functor (baseAlgebra g A) d ≅
      Limits.pullback (yonedaBaseMap g) (Fd.toBase A d)

Tag 01NU, a lemma

Tag 01NU in the Stacks Project.

Stacks.AlgebraicGeometry.RelativeProjQcohSheaf.Fd.representableByDegreeOpen, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjQcohSheaf/AffineFdRepresentable.lean, line 355. The attribute's comment: “THE TAG, for an AFFINE base: for S affine, A with quasi-coherent homogeneous pieces (Situation 01NN) and d >= 1, the functor F_d of strict equivalence classes of quadruples of Section 01NS is REPRESENTABLE by the open U_d of Equation 27.12.0.1 inside Proj Gamma(S, A) a CategoryTheory.Functor.RepresentableBy for Fd.functor, i.e. the bijections Quadruple.fdEquiv together with their naturality in the test scheme (Quadruple.classifyingHomOfClass_pullback, which rests on the unconditional veroneseSections_pullback).”.

Stacks Project, Tag 01NU: the functor F_d of Section 01NS is represented by the open U_d ⊆ Proj Γ(S, 𝒜) of Equation 27.12.0.1. Let S be affine, 𝒜 a graded 𝒪_S-algebra with quasi-coherent homogeneous pieces (Situation 01NN) and d ≥ 1. The bijections ...RelativeProjQcohSheaf.Quadruple.fdEquiv of StacksFrontier/AlgebraicGeometry/RelativeProjQcohSheaf/AffineQuadrupleBijection.lean, one for each test scheme, form a natural isomorphism Mor(−, U_d) ≅ F_d: the naturality clause is Quadruple.classifyingHomOfClass_pullback, transported across the bijection.

The hypotheses are exactly IsAffine S, the quasi-coherence of the homogeneous pieces, and 0 < d; the naturality statements the proof rests on are unconditional.

public def Fd.representableByDegreeOpen [IsAffine S] (hk : 0 < k)
    (hqc : ∀ n : ℤ, ((situationAlgebra B).piece n).IsQuasicoherent) :
    (Fd.functor (situationAlgebra B) (k : ℤ)).RepresentableBy
      (degreeOpen (B.grading (⊤ : S.Opens)) k).toScheme

Tag 01NV, a lemma

Tag 01NV in the Stacks Project.

Stacks.AlgebraicGeometry.RelativeProjQcohSheaf.Fd.exists_representableBy_functor_of_pos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjQcohSheaf/AffineOpenCharts.lean, line 515. The attribute's comment: “THE TAG, UNCONDITIONALLY: for S a scheme, A a quasi-coherent graded O_S-algebra (Situation 01NN) and d = k with 0 < k, the functor F_d of Section 01NS is representable by a scheme over S. The conclusion is about Fd.functor, the genuine functor whose restriction maps are the pullback of a quadruple, and it records that the representing morphism composed with p : Y -> S is the class's own morphism to S.”.

Stacks Project, Tag 01NV. Let S be a scheme, 𝒜 a quasi-coherent graded 𝒪_S-algebra (Situation 01NN) and d ≥ 1. The functor F_d of Section 01NS is representable by a scheme over S: there are a scheme Y, a morphism p : Y ⟶ S and a representation of F_d by Y under which the morphism T ⟶ Y representing a class ξ ∈ F_d(T), composed with p, is the morphism T ⟶ S recorded by ξ.

theorem Fd.exists_representableBy_functor_of_pos :
    ∃ (Y : Scheme.{u}) (p : Y ⟶ S)
      (e : (Fd.functor (situationAlgebra A) (k : ℤ)).RepresentableBy Y),
      ∀ (T : Scheme.{u}) (ξ : Fd (situationAlgebra A) (k : ℤ) T),
        e.homEquiv.symm ξ ≫ p = ξ.1

Tag 01NW, a lemma

Tag 01NW in the Stacks Project.

Stacks.AlgebraicGeometry.RelativeProjQcohSheaf.Quadruple.tfae_compatibleAt_lcm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjQcohSheaf/EquivalenceDescent.lean, line 954. The attribute's comment: “for two quadruples over the same morphism with positive degrees d and d', and the least common multiple m of d and d' written as m = a d = a' d', these three conditions are equivalent: compatibility at the cofactors (a, a') of the least common multiple; equivalence of the two quadruples, i.e. compatibility at (d', d); and compatibility at the cofactors of some positive common multiple of the two degrees”.

[Stacks, Tag 01NW]. In Situation 01NN, let T be a scheme and let (d, f, L, ψ) and (d', f, L', ψ') be two quadruples over T with d and d' positive, and write the least common multiple m of d and d' as m = a₀ d = a₀' d'. Then the following three conditions are equivalent:

the two quadruples are compatible at (a₀, a₀'), that is, there is an isomorphism β : L^{⊗ a₀} ⟶ (L')^{⊗ a₀'} for which β ∘ ψ|_{f^*𝒜^{(m)}} and ψ'|_{f^*𝒜^{(m)}} agree as graded ring maps;

the two quadruples are equivalent, that is, compatible at (d', d);

the two quadruples are compatible at (a, a') for some positive common multiple m = a d = a' d' of their degrees.

The source's remaining clause f = f' is not a separate condition here: both quadruples are taken over the same morphism f : T ⟶ S, which is a parameter of the type Quadruple f 𝒜 d, so the two morphisms are equal by construction in all three conditions.

The five implications of the cycle are the five declarations above and in StacksFrontier.AlgebraicGeometry.RelativeProjQcohSheaf.Equivalence: equivalent_of_lcm_compatible, exists_compatible_of_equivalent, lcm_compatible_of_exists_compatible, lcm_compatible_of_equivalent and equivalent_of_exists_compatible.

theorem tfae_compatibleAt_lcm (hd : 0 < d) (hd' : 0 < d') {a₀ a₀' : ℤ}
    (ha₀ : (Int.lcm d d' : ℤ) = a₀ * d) (ha₀' : (Int.lcm d d' : ℤ) = a₀' * d') :
    List.TFAE
      [CompatibleAt P Q a₀ a₀',
        Equivalent P Q,
        ∃ m a a' : ℤ, 0 < m ∧ m = a * d ∧ m = a' * d' ∧ CompatibleAt P Q a a']

Tag 01NX, an equation

Tag 01NX in the Stacks Project.

Stacks.AlgebraicGeometry.RelativeProjQcohSheaf.F.limFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjQcohSheaf/UnionRepresentable.lean, line 148. The attribute's comment: “the functor F of the display for EVERY test scheme, which closes the second qualification recorded on F.functor: the source defines F(T) as the union over d >= 1 of the F_d(T) only for a quasi- compact T and as the inverse limit of those over the quasi-compact opens of T in general, and that inverse limit, previously NOT CONSTRUCTED, is this functor. Both functor laws come from AlgebraicGeometry.Scheme.QcExtension.pullback_id and pullback_comp; F.limEquiv is the identification with the union on a quasi-compact test scheme, and AlgebraicGeometry.Scheme.QcExtension.equivQcOpen the identification of the index used here (all morphisms out of quasi-compact schemes, which makes the functoriality in T a reindexing) with the quasi-compact opens of T that the source indexes by. The FIRST qualification recorded on F.functor is DISCHARGED and is NOT inherited: the value of this functor on a quasi-compact test scheme is the source's F(T) itself, not a quotient of it. UnionRel IS an equivalence relation, being cofinal equality ...UnionEquivalenceRelation.unionRel_iff_cofinallyEqual and ...UnionEquivalenceRelation.unionRel_equivalence so two quadruples of positive degree have the same point of F(T) EXACTLY when they are equivalent (...UnionEquivalenceRelation.F.mk_eq_mk_iff_equivalent, and ...UnionEquivalenceRelation.F.mk_eq_mk_iff_strictlyEquivalent when the two degrees agree). The brick that had been missing was NOT the implication (3) => (1) of Tag 01NW, which was already proved as ...EquivalenceDescent.Quadruple.lcm_compatible_of_exists_compatible, but the converse of ...PowerTransitionColimit.Quadruple.strictlyEquivalent_scale_of_compatibleAt, namely ...UnionEquivalenceRelation.Quadruple.compatibleAt_of_strictlyEquivalent_scale; neither Tag 01NB nor Tag 01NU is used for it.”.

Stacks Project, display 01NX, on all of Sch. The functor sending a test scheme T to the union F(T) = ⋃_{d ≥ 1} F_d(T) when T is quasi-compact, and to the inverse limit of those unions over the quasi-compact opens of T in general.

It is the quasi-compact extension AlgebraicGeometry.Scheme.QcExtension.functor of F.functor, the union taken at every test scheme; F.limEquiv says the two agree on a quasi-compact test scheme, and AlgebraicGeometry.Scheme.QcExtension.equivQcOpen that the extension is the limit over the quasi-compact opens the source writes.

def F.limFunctor (A : SheafOfModules.GradedAlgebra.{u, u} (structureRingSheaf S.toRingedSpace)) :
    Scheme.{u}ᵒᵖ ⥤ Type (u + 1)

Tag 01NY, a lemma

Tag 01NY in the Stacks Project.

Stacks.AlgebraicGeometry.RelativeProjQcohSheaf.F.isRepresentable_limFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjQcohSheaf/RelativeProjRepresents.lean, line 103. The attribute's comment: “the tag's sentence in one statement, with no datum beyond the scheme and the graded algebra: the functor F of the display 01NX is representable by a scheme, the representing scheme being the constructed relative homogeneous spectrum Proj_S(A)”.

[Stacks, Tag 01NY]. In Situation 01NN — a scheme S and a quasi-coherent graded 𝒪_S-algebra 𝒜 — the functor F of the display 01NX is representable by a scheme.

This is the tag's sentence itself, with no datum quantified over beyond S and 𝒜: the representing scheme is Proj_S(𝒜) of [Stacks, Tag 01NQ], and the representation is F.representableByRelativeProjOfCharts at that scheme. The functor is F.limFunctor, the display on every test scheme — the union over d ≥ 1 of the F_d on a quasi-compact one and the inverse limit of those over the quasi-compact opens in general — so the statement is about the source's F and not about one F_d.

The sibling F.representableByRelativeProjOfCharts is the sharper form, naming the representing scheme and allowing it to be an arbitrary relative homogeneous spectrum of 𝒜; this is the bare existential the tag states. Nothing is assumed beyond Situation 01NN, which 𝒜 carries.

theorem F.isRepresentable_limFunctor :
    (F.limFunctor (situationAlgebra A)).IsRepresentable

Tag 01NZ, a lemma

Tag 01NZ in the Stacks Project.

Stacks.AlgebraicGeometry.RelativeProjQcohSheaf.representableBy_and_existsUnique_isoOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjQcohSheaf/RelativeProjRepresents.lean, line 173. The attribute's comment: “for a scheme S and a quasi-coherent graded O_S-algebra A (Situation 01NN) and any scheme over S carrying projective-spectrum charts on the affine opens of S, the constructed relative homogeneous spectrum Proj_S(A) represents the functor F.limFunctor of the display 01NX, and there is exactly one isomorphism from Proj_S(A) to that scheme compatible with the charts, which is an isomorphism over S”.

[Stacks, Tag 01NZ]. In Situation 01NN, let P be any scheme over S carrying projective-spectrum charts on the affine opens of S — for instance the scheme representing the functor F, which is such a datum by the source's "over each affine open of S we can identify X with the homogeneous spectrum of the sections of 𝒜 over that open". Then

the relative homogeneous spectrum π : Proj_S(𝒜) → S of [Stacks, Tag 01NQ] represents F, and

there is exactly one isomorphism Proj_S(𝒜) ≅ P compatible with the charts, and it is an isomorphism over S.

Together these say that Proj_S(𝒜) and the scheme representing F are canonically isomorphic as schemes over S, which is the source's statement: the first assertion identifies Proj_S(𝒜) as a representing object and the second produces the canonical comparison with any other chart-carrying scheme over S, uniquely.

The first assertion is a representation, hence data rather than a proposition, so the two are packaged by PProd rather than And. The chart datum P is the only binder beyond Situation 01NN, and it is data the statement needs in order to speak of the second scheme at all; it is not a hypothesis of the source, since relativeProj A is itself a RelativeProjData A and so is every projective bundle of ...SheafSymmetricAlgebra.

The two assertions are relativeProjRepresentableByFunctorUnconditional of this file and ...RelativeProjQcohSheaf.existsUnique_isoOver of StacksFrontier.AlgebraicGeometry.RelativeProjQcohSheaf.GluedRepresents.

def representableBy_and_existsUnique_isoOver (P : RelativeProjData A) :
    PProd ((F.limFunctor (situationAlgebra A)).RepresentableBy (relativeProj A).scheme)
      (∃! e : (relativeProj A).scheme ≅ P.scheme,
        (∀ U : S.affineOpens, (relativeProj A).chart U.1 U.2 ≫ e.hom = P.chart U.1 U.2) ∧
          e.hom ≫ P.toBase = (relativeProj A).toBase)

Tag 01O0, a definition

Tag 01O0 in the Stacks Project.

Stacks.AlgebraicGeometry.RelativeProj.relativeHomogeneousSpectrum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProj/Spectrum.lean, line 87. The attribute's comment: “the scheme Proj_S(A) itself. The tag NAMES the scheme constructed in Lemma 01NQ, which in this repository is the field scheme of Stacks.AlgebraicGeometry.RelativeProj.relativeProj, a construction (a colimit over the small affine Zariski site of S) and not a choice; the structure morphism pi the tag's last sentence names is relativeHomogeneousSpectrumToBase, which carries this tag too. NOT re-asserted here: the tag's reference to the functor F of the display 01NX and to Lemma 01NZ, namely that this scheme REPRESENTS F. The functor F is not constructed in this repository; that representability is carried, with the source's inputs to it, in ...RelativeProjQcohSheaf.RepresentingProjData and proved there as ...RepresentingProjData.relativeProjRepresentableBy”. References: EGA II (3.1.3); EGA II (8.3.1).

The relative homogeneous spectrum Proj_S(A), or relative Proj, of a quasi-coherent sheaf of graded 𝒪_S-algebras A over a scheme S: the scheme glued from the projective spectra of the graded rings of sections of A over the affine opens of S.

public def relativeHomogeneousSpectrum : Scheme.{u}

Stacks.AlgebraicGeometry.RelativeProj.relativeHomogeneousSpectrumToBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProj/Spectrum.lean, line 93. The attribute's comment: “ONLY the structure morphism pi : Proj_S(A) → S of the tag's last sentence; the scheme itself is relativeHomogeneousSpectrum, whose clause string describes the covering set and what the tag's reference to 01NX/01NZ is and where it lives”.

The structure morphism π : Proj_S(A) → S of the relative homogeneous spectrum.

public def relativeHomogeneousSpectrumToBase :
    relativeHomogeneousSpectrum A ⟶ S

Tag 01O1, a lemma

Tag 01O1 in the Stacks Project.

Stacks.AlgebraicGeometry.RelativeProjTwistChartBridge.tag01O1, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjTwistChartBridge/ThetaIsomorphism.lean, line 150. The attribute's comment: “for a quadruple (f : T -> S, d, L, psi) with associated morphism r : T -> Proj_S(A), the morphism the representation of F by Proj_S(A) attaches to the class of the quadruple: r lies over S, and there is an isomorphism theta of Z-graded O_T-algebras from r^*((+)_n O(nd)) to (+)_n L^(x)n, preserving the unit, with psi = theta o psi_univ in every degree, and every homomorphism of graded algebras with psi = Theta o psi_univ is theta”.

Stacks Project, Tag 01O1. In Situation 01NN — S a scheme and 𝒜 a quasi-coherent graded 𝒪_S-algebra — let (f : T → S, d, ℒ, ψ) be a quadruple of Section 01NS, so d ≥ 1, and let r = r_{d, ℒ, ψ} : T → Proj_S(𝒜) be the associated morphism (...RelativeProjTwistChartBridge.thetaMorphism: the morphism into U_d that the class of the quadruple defines, followed by U_d ⊆ Proj_S(𝒜)). Write 𝒪(n) for the twists of Proj_S(𝒜) with their homogeneous-section map ψ_univ (...GluedTwistAlgebra.twistDataOfGradedAlgebra). Then

r is the morphism the representability of F attaches to the quadruple: the image of its class in F(T) under the representation ...RelativeProjQcohSheaf.relativeProjRepresentableByFunctorUnconditional of the functor F of the display 01NX by Proj_S(𝒜), which is the representation of [Stacks, Tag 01NZ];

r is a morphism over S;

there is an isomorphism of sheaves of ℤ-graded 𝒪_T-algebras θ : r^*(⨁_{n ∈ ℤ} 𝒪(nd)) ≅ ⨁_{n ∈ ℤ} ℒ^{⊗ n}, which preserves the unit;

the triangle commutes: ψ = θ ∘ ψ_univ in every degree, the maps out of 𝒜^{(d)} being read through the adjunction f^* ⊣ f_*, so that ψ_univ becomes ...RelativeProjTwists.TwistData.psiLegVeronese; and

the triangle determines θ: any homomorphism of graded algebras r^*(⨁_n 𝒪(nd)) ⟶ ⨁_n ℒ^{⊗ n} making it commute is θ.

theorem tag01O1 (hd : 0 < d) (P : Quadruple f (situationAlgebra A) (d : ℤ)) :
    thetaMorphism hd P =
        (relativeProjRepresentableByFunctorUnconditional A).homEquiv.symm
          (RelativeProjInvertibleMorphism.F.toLim A (F.mk f (by exact_mod_cast hd) P)) ∧
    thetaMorphism hd P ≫ (relativeProj A).toBase = f ∧
      ∃ θ : pullbackTwistVeronese (GluedTwistAlgebra.twistDataOfGradedAlgebra A) (d : ℤ)
          (thetaMorphism hd P) ≅ laurent P.L,
        SheafOfModules.GradedAlgebra.oneHom
              (pullbackTwistVeronese (GluedTwistAlgebra.twistDataOfGradedAlgebra A) (d : ℤ)
                (thetaMorphism hd P)) ≫ θ.hom.app 0 =
            SheafOfModules.GradedAlgebra.oneHom (laurent P.L) ∧
          (∀ n : ℤ, (GluedTwistAlgebra.twistDataOfGradedAlgebra A).psiLegVeronese
              (thetaMorphism hd P) (thetaMorphism_comp_toBase hd P) (d : ℤ) n ≫ θ.hom.app n =
                P.twisting.app n) ∧
          ∀ Θ : pullbackTwistVeronese (GluedTwistAlgebra.twistDataOfGradedAlgebra A) (d : ℤ)
              (thetaMorphism hd P) ⟶ laurent P.L,
            (∀ n : ℤ, (GluedTwistAlgebra.twistDataOfGradedAlgebra A).psiLegVeronese
              (thetaMorphism hd P) (thetaMorphism_comp_toBase hd P) (d : ℤ) n ≫ Θ.app n =
                P.twisting.app n) → Θ = θ.hom

Tag 01O2, a lemma

Tag 01O2 in the Stacks Project.

Stacks.RelativeProj.Data.isSeparated_toBase, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/TerminalRelativeProj.lean, line 125. The attribute's comment: “the gluing-datum form”. References: EGA II (2.4.2); EGA II (3.1.3), “separated over Y”; EGA II (8.14.1), “more general”.

Stacks Project, Tag 01O2. The structure morphism of a relative Proj is separated.

Separatedness is local on the target, so it suffices to check it over the affine opens of the base; over an affine open U the preimage is the chart Proj (𝒜 U), a separated scheme, and a morphism out of a separated scheme is separated.

instance isSeparated_toBase (d : Data 𝒜) : IsSeparated d.toBase

Stacks.RelativeProj.Situation.isSeparated_relativeProjToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BlowUpSeparatedInput/Basic.lean, line 97. References: EGA II (3.1.3), “separated over Y”; EGA II (8.14.1).

Stacks Project, Tag 01O2. The structure morphism of the relative Proj of a quasi-coherent, commutative, nonnegatively graded algebra on a scheme is separated.

Separatedness is local at the target, and over an affine open W of the base the restriction of relativeProjToBase is the chart structure morphism Proj Γ(W, 𝒜) ⟶ W, because both are pullbacks of relativeProjToBase along W.ι.

public theorem _root_.Stacks.RelativeProj.Situation.isSeparated_relativeProjToBase
    (s : Stacks.RelativeProj.Situation.{u}) :
    IsSeparated (Stacks.RelativeProj.Situation.relativeProjToBase s)

Tag 01O3, a lemma

Tag 01O3 in the Stacks Project.

Stacks.AlgebraicGeometry.RelativeProjBaseChangeTwist.relativeProj_baseChange_twist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjBaseChangeTwist/Theta.lean, line 74. The attribute's comment: “the canonical isomorphism r : Proj_S'(g^A) -> S' x_S Proj_S(A) over S', and the isomorphism theta : r^ pr_2^ ((+)_d O(d)) -> (+)_d O_{Proj_S'(g^A)}(d) of Z-graded algebras, preserving the unit”.

Stacks Project, Tag 01O3. Let S be a scheme, A a quasi-coherent sheaf of graded 𝒪_S-algebras and g : S' → S a morphism of schemes. The canonical isomorphism r : Proj_{S'}(g^*A) ≅ S' ×_S Proj_S(A) (baseChangeIso) lies over S' and has second component the base change Proj_{S'}(g^*A) → Proj_S(A), and θ (baseChangeTheta) is an isomorphism of ℤ-graded algebras r^* pr₂^* (⨁_d 𝒪_{Proj_S(A)}(d)) ≅ ⨁_d 𝒪_{Proj_{S'}(g^*A)}(d), which preserves the unit.

theorem relativeProj_baseChange_twist :
    (baseChangeIso A g).hom ≫
          pullback.fst g (Stacks.AlgebraicGeometry.RelativeProj.relativeProj A).toBase =
        (Stacks.AlgebraicGeometry.RelativeProj.relativeProj (A.pullback g)).toBase ∧
      (baseChangeIso A g).hom ≫
          pullback.snd g (Stacks.AlgebraicGeometry.RelativeProj.relativeProj A).toBase =
        baseChangeHom A g ∧
      ∀ U, ((baseChangeTheta A g).hom.app 0).val.app U
          ((pbAlgS (baseChangeIso A g).hom
            (Stacks.RingedSpace.pullbackGradedAlgebra
              (pullback.snd g
                (Stacks.AlgebraicGeometry.RelativeProj.relativeProj A).toBase).toLRSHom.toShHom
              (twistAlgebra A))).one.eval U) =
        (twistAlgebra (A.pullback g)).one.eval U

Stacks.RelativeProj.Situation.twistSheafPullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/ModuleGlueing/RelativeProjTwistBaseChangeGlued.lean, line 455. The attribute's comment: “the graded isomorphism θ on the twisting sheaves, in each degree separately, as clause (3) of Tag 01N2 is carried with the same reading”. References: EGA II (2.8.10), “partial”; EGA II (2.8.11), “more general”; EGA II (4.1.3), “more general”.

The twist assertion of [Stacks, Tag 01O3]. For a morphism g : S' ⟶ S, relative Proj situations s over S and s' over S', and an identification Φ of the graded algebra of s' with the pullback along g of that of s, degreewise invertible, the base-change morphism r : Proj_{S'}(g^*𝒜) ⟶ Proj_S(𝒜) carries the n-th twisting sheaf to the n-th twisting sheaf:

θ n : r^* 𝒪_{Proj_S(𝒜)}(n) ≅ 𝒪_{Proj_{S'}(g^*𝒜)}(n),

for every n : ℤ and with no hypothesis beyond the two situations and the datum Φ.

The scheme half of the tag — the isomorphism r itself, and the cartesian square — is Stacks.RelativeProj.Situation.relativeProjBaseChangeIso and isPullback_relativeProjBaseChange.

Multiplicativity of θ is not proved: this is the degreewise isomorphism, exactly as clause (3) of Tag 01N2 is carried by Stacks.ProjBaseChange.isIso_twistMap_includeRight with the same restriction.

public def twistSheafPullbackIso :
    (Scheme.Modules.pullback (relativeProjBaseChange g Φ hΦ)).obj (twistSheaf s n)
      ≅ twistSheaf s' n

Tag 01O4, a lemma

Tag 01O4 in the Stacks Project.

Stacks.AlgebraicGeometry.TwistMapsInvertible.f1Bundle_and_twists, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TwistMapsInvertible/RepresentsAndTwists.lean, line 95. The attribute's comment: “for a scheme S and a quasi-coherent sheaf of graded O_S-modules A generated as an A_0-algebra by A_1, three things hold of X = Proj_S(A): X represents the functor F_1 sending f : T -> S to the strict isomorphism classes of pairs (L, psi) with L an invertible O_T-module and psi : f^A -> ⨁_{n >= 0} L^{⊗ n} a graded algebra homomorphism whose degree-one component f^A_1 -> L is surjective, by bijections normalised at the identity of X and natural in the test scheme; every homogeneous piece O_X(n) of the canonical twist datum on X is an invertible O_X-module; and the multiplication maps O_X(n) (x) O_X(m) -> O_X(n+m) are isomorphisms in all integer degrees”.

[Stacks, Tag 01O4]. Let S be a scheme and 𝒜 a quasi-coherent sheaf of graded 𝒪_S-modules generated as an 𝒜_0-algebra by 𝒜_1. Then, for X = Proj_S(𝒜):

X represents the functor F_1 of pairs (L, ψ) with L invertible and f^*𝒜_1 ⟶ L surjective, up to strict equivalence — the bijections between the morphisms T ⟶ X over S and the strict isomorphism classes of such pairs, normalised at the identity of X and natural in the test scheme;

every homogeneous piece 𝒪_X(n) of the canonical twist datum on X is an invertible 𝒪_X-module; and

the multiplication maps 𝒪_X(n) ⊗ 𝒪_X(m) ⟶ 𝒪_X(n + m) are isomorphisms in all integer degrees.

The first assertion is a family of bijections, hence data rather than a proposition, so it is joined to the other two by PProd rather than And.

The hypothesis hgen is the source's own degree-one generation. The binder TA is the choice of tensor algebras, which is data the library needs in order to state the first assertion at all, and the comparison of its pullbacks is the canonical tensorAlgebraPullbackIsos. The twists are the canonical twist datum twistDataOfGradedAlgebra, constructed from 𝒜 alone.

The three assertions are ...ProjRepresentsF1.f1Bundle, twistDataOfGradedAlgebra_isInvertible and isIso_mulSheaf_twistDataOfGradedAlgebra.

def f1Bundle_and_twists {S : Scheme.{u}} (A : SheafGradedAlgebra.{u} S) (TA : TensorAlgebras.{u})
    (hgen : IsGeneratedInDegreeOne A) :
    PProd (F1Bundle A TA (tensorAlgebraPullbackIsos TA))
      ((∀ n : ℤ, AlgebraicGeometry.SheafOfModules.IsInvertible (relativeProj A).scheme.presheaf
            (relativeProj A).scheme.ringCatSheaf.2
            ((twistDataOfGradedAlgebra A).algebra.piece n)) ∧
        ∀ n m : ℤ, IsIso (_root_.SheafOfModules.GradedAlgebra.mulSheaf
          (twistDataOfGradedAlgebra A).algebra n m))

Sources

Section27.17 Quasi-coherent sheaves on relative Proj #

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

Tag 01O6, an equation

Tag 01O6 in the Stacks Project.

Stacks.AlgebraicGeometry.RelativeProjQcohSheaf.Twisting.associatedSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjQcohSheaf/Basic.lean, line 304.

Stacks Project, Tag 01O6, equation (27.17.0.1). The 𝒪_T-module

ℳ̃_T = (f^*ℳ^{(d)} ⊗_{f^*𝒜^{(d)}} (⨁_{n ∈ ℤ} L^{⊗ n}))₀

attached to a graded 𝒜-module ℳ and a quadruple (d, f : T → S, L, ψ): the degree-zero part of the tensor product, over the pullback of the d-th Veronese regrading of 𝒜, of the pullback of the d-th Veronese regrading of ℳ with the Laurent algebra of L. It is the quotient of ⨁_{n ∈ ℤ} f^*ℳ_{nd} ⊗ L^{⊗ (-n)} by the balancing relations (x · a) ⊗ l = x ⊗ (ψ(a) · l).

def associatedSheaf : SheafOfModules.{u} (structureRingSheaf T.toRingedSpace)

Tag 01O7, a lemma

Tag 01O7 in the Stacks Project.

Stacks.RelativeProj.Situation.tensorModuleSheafMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjLeftGradedTensorGlueHom.lean, line 449. The attribute's comment: “property (6): the canonical map from the tensor product of the sheaves attached to two left graded modules with quasi-coherent homogeneous pieces to the sheaf attached to the tensor product of those modules, on a relative projective spectrum”.

The canonical map ℳ̃ ⊗_𝒪 𝒩̃ ⟶ (ℳ ⊗_𝒜 𝒩)~ of property (6) of Tag 01O7, for two left graded modules with quasi-coherent homogeneous pieces over the graded algebra of a relative Proj situation. It is glued from the chart members Stacks.RelativeProj.Situation.moduleSheafTensorChartMap, to each of which it restricts, and it is the only morphism that does so.

public noncomputable def tensorModuleSheafMap :
    (((Stacks.SheafOfModules.Tensor.sheafTensor
        ⟨(((relativeProj s).toRingedSpace)).presheaf,
          (((relativeProj s).toRingedSpace)).IsSheaf⟩).obj ((moduleSheaf ℳ))).obj
        ((moduleSheaf 𝒩))) ⟶ s.tensorModuleSheaf ℳ 𝒩

Stacks.AlgebraicGeometry.RelativeProjQuadrupleTilde.tag01O7_property1, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjQuadrupleTilde/TildeComparison.lean, line 62. The attribute's comment: “property (1): the canonical isomorphism M~_T ≅ h^*M~”.

For a quadruple P = (f : T → S, d, L, ψ) and the morphism h : T ⟶ Proj_S(𝒜) it classifies, the isomorphism Quadruple.tildeComparison ℳ hd P : ℳ̃_T ≅ h^*ℳ̃ satisfies:

chart data of (f, ψ, h) exist around every point of T;

along every morphism a : Z ⟶ T carrying a chart datum D, its pullback is the local comparison localHom ℳ hd a D, which is a^*ℳ̃_T ≅ ℳ̃_Z, then the chart comparison of D, then (a ≫ h)^*ℳ̃ ≅ a^*h^*ℳ̃ (localHom_eq);

the chart comparison of a datum sends the pure tensor x ⊗ l in degree n to (w^n · l) · g^*(x / c^n), w = ψ(c);

it is the only isomorphism ℳ̃_T ≅ h^*ℳ̃ with the second property along the opens of T.

theorem tag01O7_property1 :
    letI := P.isInvertible
    (∀ t : T, ∃ V : T.Opens, t ∈ V ∧ Nonempty (ChartDatum (V.ι ≫ f) (P.twisting.pullback V.ι)
      (V.ι ≫ classifyingHom s (by exact_mod_cast hd) P))) ∧
    (∀ {Z : Scheme.{u}} (a : Z ⟶ T) (D : ChartDatum (a ≫ f) (P.twisting.pullback a)
        (a ≫ classifyingHom s (by exact_mod_cast hd) P)),
      (Scheme.Modules.pullback a).map (Quadruple.tildeComparison ℳ hd P).hom =
        localHom ℳ hd a D) ∧
    (∀ {Z : Scheme.{u}} (a : Z ⟶ T) (D : ChartDatum (a ≫ f) (P.twisting.pullback a)
        (a ≫ classifyingHom s (by exact_mod_cast hd) P)) (n : ℤ),
      Twisting.pureTensor (ℳ.toGradedModule s.mul_comm) (P.twisting.pullback a) n ≫
          (D.iso ℳ hd).hom =
        bmap ℳ D.U D.c (a ≫ f) D.hf D.g D.hg D.hgf D.w n ≫
          (moduleSheafPullbackChartIso ℳ D.U D.g D.fac).inv) ∧
    (∀ Φ : Twisting.associatedSheaf (ℳ.toGradedModule s.mul_comm) P.twisting ≅
        (Scheme.Modules.pullback (classifyingHom s (by exact_mod_cast hd) P)).obj (moduleSheaf ℳ),
      (∀ (V : T.Opens) (D : ChartDatum (V.ι ≫ f) (P.twisting.pullback V.ι)
          (V.ι ≫ classifyingHom s (by exact_mod_cast hd) P)),
        (Scheme.Modules.pullback V.ι).map Φ.hom = localHom ℳ hd V.ι D) →
        Φ = Quadruple.tildeComparison ℳ hd P)

Stacks.AlgebraicGeometry.RelativeProjQuadrupleTilde.Quadruple.tildeComparison_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjQuadrupleTilde/TildePullback.lean, line 308. The attribute's comment: “property (2): the isomorphisms of property (1) are compatible with pullback along every morphism of test schemes”.

Property (2) of [Stacks, Tag 01O7]: the isomorphisms of property (1) are compatible with pullbacks. For a quadruple P = (f : T → S, d, L, ψ) classifying h : T ⟶ Proj_S(𝒜) and a morphism g : T' ⟶ T, the pulled-back quadruple P.pullback g classifies g ≫ h, and its isomorphism ℳ̃_{T'} ≅ (g ≫ h)^*ℳ̃ of property (1) is the pullback along g of the isomorphism ℳ̃_T ≅ h^*ℳ̃ of P, read through the canonical comparisons ℳ̃_{T'} ≅ g^*ℳ̃_T and g^*h^*ℳ̃ ≅ (g ≫ h)^*ℳ̃.

theorem Quadruple.tildeComparison_pullback {T : Scheme.{u}} {f : T ⟶ s.base}
    (P : Quadruple f s.algebra (d : ℤ)) {T' : Scheme.{u}} (g : T' ⟶ T) :
    letI := P.isInvertible
    (Quadruple.tildeComparison ℳ hd (P.pullback g)).hom =
      (Quadruple.associatedSheafPullbackIso (M := ℳ.toGradedModule s.mul_comm) (P := P)
          (g := g)).inv ≫
        (Scheme.Modules.pullback g).map (Quadruple.tildeComparison ℳ hd P).hom ≫
          (Scheme.Modules.pullbackComp g (classifyingHom s (by exact_mod_cast hd) P)).hom.app
            (moduleSheaf ℳ) ≫
            (Scheme.Modules.pullbackCongr
              (classifyingHom_pullback s (by exact_mod_cast hd) P g).symm).hom.app
                (moduleSheaf ℳ)

Stacks.RelativeProj.Situation.moduleSheafPullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/ModuleGlueing/RelativeProjModuleBaseChangeIso.lean, line 169. The attribute's comment: “property (8): the canonical isomorphism r^ ℳ̃ ≅ (g^ ℳ)~ on the relative projective spectrum of g^* 𝒜, for any morphism of schemes g : S' ⟶ S”.

Stacks Project, Tag 01O7, property (8). The formation of ℳ̃ commutes with base change. For a morphism of schemes g : S' ⟶ S, put 𝒜' = g^* 𝒜 and ℳ' = g^* ℳ, and let r : Proj_{S'}(𝒜') ⟶ Proj_S(𝒜) be the induced morphism of relative projective spectra. Then the canonical comparison r^* ℳ̃ ⟶ ℳ̃' is an isomorphism.

The comparison is Stacks.RelativeProj.Situation.moduleSheafBaseChangeHom, the unique morphism restricting on the chart of Proj_{S'}(𝒜') over each pair W' ⊆ g⁻¹W of affine opens to the comparison of the sheaves of Tag 01M6 across the base change of the graded section rings (Stacks.RelativeProj.Situation.restrictFunctor_map_moduleSheafBaseChangeHom); it is invertible by Stacks.RelativeProj.Situation.isIso_moduleSheafBaseChangeHom.

public noncomputable def moduleSheafPullbackIso :
    (Scheme.Modules.pullback (pullbackRelativeProjMap s g)).obj (moduleSheaf ℳ) ≅
      moduleSheaf (s := s.pullback g) (Stacks.Conormal.leftGradedPullback g ℳ)

Stacks.RelativeProj.Situation.moduleSheafFibreProductIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/ModuleGlueing/RelativeProjModuleBaseChangeIso.lean, line 216. The attribute's comment: “property (8) on the fibre product: the canonical isomorphism between the pullback of ℳ̃ along S' ×_S Proj_S(𝒜) ⟶ Proj_S(𝒜) and (g^* ℳ)~ carried to S' ×_S Proj_S(𝒜)”.

Stacks Project, Tag 01O7, property (8), on the fibre product. For a morphism of schemes g : S' ⟶ S, the pullback of ℳ̃ along the projection S' ×_S Proj_S(𝒜) ⟶ Proj_S(𝒜) is canonically isomorphic to the sheaf (g^* ℳ)~, transported to the fibre product along the canonical identification e : Proj_{S'}(g^* 𝒜) ≅ S' ×_S Proj_S(𝒜) of Stacks.RelativeProj.Situation.relativeProjBaseChangeIso.

It is Stacks.RelativeProj.Situation.moduleSheafPullbackIso read through e: the projection is e⁻¹ followed by the base-change morphism r, so its inverse image is e⁻¹'s of r^* ℳ̃.

public noncomputable def moduleSheafFibreProductIso :
    (Scheme.Modules.pullback (Limits.pullback.fst (relativeProjToBase s) g)).obj (moduleSheaf ℳ) ≅
      (Scheme.Modules.pullback (pullbackRelativeProjIso s g).inv).obj
        (moduleSheaf (s := s.pullback g) (Stacks.Conormal.leftGradedPullback g ℳ))

Stacks.RelativeProj.Situation.degreeZeroSheafMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/ModuleGlueing/RelativeProjModuleSheafDegreeZeroMap.lean, line 450. The attribute's comment: “property (3): the canonical map from the pullback of the degree-zero part of a graded module to its associated sheaf on the relative projective spectrum”. References: EGA II (3.3.2), “Map (3.3.2.4) for n = 0”.

Stacks Project, Tag 01O7, property (3). The canonical map

π^*ℳ_0 ⟶ ℳ̃

on the relative projective spectrum π : Proj_S(𝒜) ⟶ S, for a graded 𝒜-module ℳ with quasi-coherent homogeneous pieces. It is the transpose, across the adjunction π^* ⊣ π_*, of Stacks.RelativeProj.Situation.degreeZeroPushforwardHom, the morphism ℳ_0 ⟶ π_* ℳ̃ which on the sections over an affine open W of the base carries m to the section m / 1 of ℳ̃ over π⁻¹(W): under the identification of ℳ̃ over π⁻¹(W) with the sheaf of the graded module of sections of ℳ over W on Proj 𝒜(W), this is the global section m / 1 of Tag 01M7.

public def degreeZeroSheafMap :
    (Scheme.Modules.pullback (relativeProjToBase s)).obj (ℳ.piece 0) ⟶ moduleSheaf ℳ

Stacks.RelativeProj.Situation.moduleSheafFunctor_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/ModuleGlueing/RelativeProjModuleSheafExactAbelian.lean, line 216. The attribute's comment: “property (5): the construction ℳ ↦ ℳ̃ is an exact functor from the abelian category of quasi-coherent graded modules over 𝒜 to modules on the relative projective spectrum”. References: EGA II (8.14.1), “partial”.

The functor Stacks.RelativeProj.Situation.moduleSheafFunctor, from the abelian category of quasi-coherent graded modules over the graded algebra 𝒜 of the situation to the modules on the relative projective spectrum Proj_S(𝒜), is additive, preserves finite limits and preserves finite colimits; equivalently, it carries short exact sequences of quasi-coherent graded modules to short exact sequences of modules on Proj_S(𝒜).

public theorem moduleSheafFunctor_exact :
    (moduleSheafFunctor s).Additive ∧ PreservesFiniteLimits (moduleSheafFunctor s) ∧
      PreservesFiniteColimits (moduleSheafFunctor s) ∧
      ∀ S : ShortComplex (QcohGradedModule s), S.ShortExact →
        (S.map (moduleSheafFunctor s)).ShortExact

Stacks.RelativeProj.Situation.moduleSheafFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/ModuleGlueing/RelativeProjModuleSheafFunctorial.lean, line 229. The attribute's comment: “property (4): the construction ℳ ↦ ℳ̃ is a functor from quasi-coherent graded modules over 𝒜 to modules on the relative projective spectrum”.

The construction ℳ ↦ ℳ̃ is functorial in ℳ: it is a functor from the quasi-coherent graded modules over the graded algebra 𝒜 to the modules over the relative projective spectrum Proj_S(𝒜), sending ℳ to the sheaf Stacks.RelativeProj.Situation.moduleSheaf ℳ and a homomorphism to the glued morphism Stacks.RelativeProj.Situation.moduleSheafMap of the chart morphisms.

public noncomputable def moduleSheafFunctor : QcohGradedModule s ⥤ (relativeProj s).Modules

Stacks.RelativeProj.Situation.shiftedSumSheafMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/ModuleGlueing/RelativeProjModuleSheafShiftedSum.lean, line 115. The attribute's comment: “property (7): the canonical map from the pullback of a graded module to the direct sum of the sheaves associated to its shifts on the relative projective spectrum”.

Stacks Project, Tag 01O7, property (7). The canonical map

π^*ℳ ⟶ ⨁_{n ∈ ℤ} (ℳ(n))~

on the relative projective spectrum π : Proj_S(𝒜) ⟶ S, out of the pullback of the 𝒪_S-module ℳ = ⨁_{n ∈ ℤ} ℳ_n underlying a graded 𝒜-module with quasi-coherent homogeneous pieces. On the summand π^*ℳ_n it is the degree-n component Stacks.RelativeProj.Situation.shiftedDegreeSheafMap, the canonical map of property (3) for the shift ℳ(n), followed by the inclusion of the n-th summand; on the sections over an affine open of the base it is the map of Tag 01MR, m ↦ m / 1 in degree n.

public def shiftedSumSheafMap :
    (Scheme.Modules.pullback (relativeProjToBase s)).obj (∐ fun n : ℤ => ℳ.piece n) ⟶
      ∐ fun n : ℤ => moduleSheaf (ℳ.shift n)

Sources

LeanStacks.AlgebraicGeometry.RelativeProjQcohSheaf.Twisting.associatedSheaf · Stacks.RelativeProj.Situation.tensorModuleSheafMap · Stacks.AlgebraicGeometry.RelativeProjQuadrupleTilde.tag01O7_property1 · Stacks.AlgebraicGeometry.RelativeProjQuadrupleTilde.Quadruple.tildeComparison_pullback · Stacks.RelativeProj.Situation.moduleSheafPullbackIso · Stacks.RelativeProj.Situation.moduleSheafFibreProductIso · Stacks.RelativeProj.Situation.degreeZeroSheafMap · Stacks.RelativeProj.Situation.moduleSheafFunctor_exact

Section27.18 Functoriality of relative Proj #

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

Tag 07ZG, a lemma

Tag 07ZG in the Stacks Project.

Stacks.AlgebraicGeometry.Tag07ZGTwist.relativeProjMapTriple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphism/TwistAlgebra.lean, line 239. The attribute's comment: “the tag in one statement: the open U(ψ) of Proj_S(B), the morphism r_ψ : U(ψ) ⟶ Proj_S(A) over S, and θ as a map of ℤ-graded 𝒪_{U(ψ)}-algebras, together with the characterisation of all three over every affine open of the base by the triple Lemma 01MY attaches to the induced homomorphism of graded rings of sections, and the uniqueness of each”. References: EGA II (3.5.1), “partial”; EGA II (8.12.4), “special case”.

Let S be a scheme, let A and B be quasi-coherent graded 𝒪_S-algebras, set p : X = Proj_S(A) ⟶ S and q : Y = Proj_S(B) ⟶ S, and let ψ : A ⟶ B be a homomorphism of graded 𝒪_S-algebras. There is a canonical open U(ψ) ⊆ Y, a canonical morphism of schemes r_ψ : U(ψ) ⟶ X over S, and a map of ℤ-graded 𝒪_{U(ψ)}-algebras

θ = θ_ψ : r_ψ^*(⨁_{d ∈ ℤ} 𝒪_X(d)) ⟶ ⨁_{d ∈ ℤ} 𝒪_{U(ψ)}(d),

and the triple (U(ψ), r_ψ, θ) is characterised by the property that for every affine open W ⊆ S the triple (U(ψ) ∩ q⁻¹W, r_ψ|_{U(ψ) ∩ q⁻¹W}, θ|_{U(ψ) ∩ q⁻¹W}) is the triple attached to ψ : A(W) ⟶ B(W), via the identifications p⁻¹W = Proj(A(W)) and q⁻¹W = Proj(B(W)).

The triple is ψ.relativeMapDomain, relativeMapHom ψ and relativeTwistAlgebraHom ψ, and the seven conjuncts are, in order:

r_ψ is a morphism over S.

The inverse image of U(ψ) under the chart over an affine open W of the base is the open mapDomain of ψ_W in Proj(B(W)).

Under the canonical identification of U(ψ) ∩ q⁻¹W with U(ψ_W), the restriction of r_ψ is the morphism mapHom of ψ_W followed by the chart of X over W.

In every degree n, the restriction of the n-th component of θ to the piece over W is relativeTwistChart ψ n W, the comparison map for ψ_W conjugated by the chart identifications. 5., 6., 7. Each of the three is determined by its affine-local description.

public theorem relativeProjMapTriple :
    (relativeMapHom ψ ≫ (relativeProj A).toBase =
        ψ.relativeMapDomain.ι ≫ (relativeProj B).toBase) ∧
      (∀ (V : S.Opens) (hV : IsAffineOpen V),
        (relativeProj B).chart V hV ⁻¹ᵁ ψ.relativeMapDomain =
          mapDomain (A.grading V) (B.grading V) (ψ.sectionHom V)) ∧
      (∀ U : AffineOpen S,
        (chartPieceIso ψ U).hom ≫
            (relativeProj B).scheme.homOfLE
                (inf_le_left : ψ.relativeMapDomain ⊓ ((relativeProj B).toBase ⁻¹ᵁ U.1) ≤ _) ≫
              relativeMapHom ψ =
          mapHom (A.grading U.1) (B.grading U.1) (ψ.sectionHom U.1) ≫
            (relativeProj A).chart U.1 U.2) ∧
      (∀ (n : ℤ) (U : S.affineOpens),
        (Scheme.Modules.pullback (pieceIncl ψ U)).map ((relativeTwistAlgebraHom ψ).app n) =
          relativeTwistChart ψ n U) ∧
      (∀ W : (relativeProj B).scheme.Opens,
        (∀ (V : S.Opens) (hV : IsAffineOpen V),
            (relativeProj B).chart V hV ⁻¹ᵁ W =
              mapDomain (A.grading V) (B.grading V) (ψ.sectionHom V)) →
          W = ψ.relativeMapDomain) ∧
      (∀ r : ψ.relativeMapDomain.toScheme ⟶ (relativeProj A).scheme,
        (∀ U : AffineOpen S,
            (((relativeProj B).chart U.1 U.2).isoImage
                  (mapDomain (A.grading U.1) (B.grading U.1) (ψ.sectionHom U.1))).hom ≫
                (relativeProj B).scheme.homOfLE (chartImage_le ψ U) ≫ r =
              mapHom (A.grading U.1) (B.grading U.1) (ψ.sectionHom U.1) ≫
                (relativeProj A).chart U.1 U.2) →
          r = relativeMapHom ψ) ∧
      (∀ (n : ℤ)
          (θ : (Scheme.Modules.pullback (relativeMapHom ψ)).obj (relativeTwist A n) ⟶
            (Scheme.Modules.pullback ψ.relativeMapDomain.ι).obj (relativeTwist B n)),
        (∀ U : S.affineOpens,
            (Scheme.Modules.pullback (pieceIncl ψ U)).map θ = relativeTwistChart ψ n U) →
          θ = (relativeTwistAlgebraHom ψ).app n)

Tag 07ZH, a lemma

Tag 07ZH in the Stacks Project.

Stacks.AlgebraicGeometry.Tag07ZGTwistStatement.relativeMapDomain_mapHom_twistMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphism/TwistCompStatement.lean, line 107. The attribute's comment: “the tag's three assertions in one statement: the domain of the composite is the inverse image of the inner factor's domain along r_ψ, the morphism of the composite is the restriction of r_ψ followed by r_φ, and the maps on twists compose. The first conjunct is the intended reading U(psi.comp phi) = r_psi^{-1}(U(phi)) of a source statement printed as U(psi.comp phi) = r_phi^{-1}(U(psi)), which is TYPE-INCORRECT -- r_phi is defined on U(phi) in Proj_S(B) and so accepts opens of Proj_S(A), whereas U(psi) is an open of Proj_S(C), the two names having been interchanged; the deviation is documented in the module docstring”.

[Stacks, Tag 07ZH]. Let S be a scheme, let A, B and C be quasi-coherent graded 𝒪_S-algebras and let φ : A ⟶ B and ψ : B ⟶ C be homomorphisms between them. Then the open, the morphism and the maps on twists that Tag 07ZG attaches to the composite ψ ∘ φ are determined by those of φ and of ψ.

The three conjuncts are, in order:

U(ψ ∘ φ) = r_ψ^{-1}(U(φ)): the open attached to the composite is the inverse image under r_ψ of the open attached to the inner factor, read inside Proj_S(C) as the image of that inverse image under the inclusion of U(ψ). (This is the intended reading of a source statement that is type-incorrect as printed; see the implementation notes above.)

r_{ψ ∘ φ} = r_φ ∘ r_ψ|_{U(ψ ∘ φ)}: the morphism attached to the composite is the restriction Stacks.AlgebraicGeometry.Tag07ZGTwist.relativeMapHomRestrict of r_ψ to U(ψ ∘ φ), followed by the morphism attached to the inner factor.

θ_ψ ∘ r_ψ^*θ_φ = θ_{ψ ∘ φ}: for every n the n-th map on twists of the composite is the inverse image along that same restriction of the n-th map on twists of φ, followed by the inverse image along the inclusion of U(ψ ∘ φ) into U(ψ) of the n-th map on twists of ψ. The isomorphisms of inverse-image functors that identify the source and the target of the two sides are the ones named by conjuncts 1 and 2 and by Stacks.AlgebraicGeometry.Tag07ZGTwist.relativeMapHomRestrict_comp_ι.

Each conjunct is the corresponding component declaration: Stacks.AlgebraicGeometry.RelativeProjMapComp.relativeMapDomain_comp, Stacks.AlgebraicGeometry.Tag07ZGTwist.relativeMapHomRestrict_comp_relativeMapHom and Stacks.AlgebraicGeometry.Tag07ZGTwist.relativeTwistMap_comp. The source states the tag for arbitrary A, B, C, φ and ψ, and those are the only binders here.

theorem relativeMapDomain_mapHom_twistMap_comp :
    (ψ.comp φ).relativeMapDomain =
        ψ.relativeMapDomain.ι ''ᵁ (relativeMapHom ψ ⁻¹ᵁ φ.relativeMapDomain) ∧
      relativeMapHomRestrict φ ψ ≫ relativeMapHom φ = relativeMapHom (ψ.comp φ) ∧
      ∀ n : ℤ,
        (Scheme.Modules.pullbackCongr
              (relativeMapHomRestrict_comp_relativeMapHom φ ψ)).inv.app
            (relativeTwist A n) ≫
            (Scheme.Modules.pullbackComp (relativeMapHomRestrict φ ψ)
              (relativeMapHom φ)).inv.app (relativeTwist A n) ≫
            (Scheme.Modules.pullback (relativeMapHomRestrict φ ψ)).map
              (relativeTwistMap φ n) ≫
            (Scheme.Modules.pullbackComp (relativeMapHomRestrict φ ψ)
              φ.relativeMapDomain.ι).hom.app (relativeTwist B n) ≫
            (Scheme.Modules.pullbackCongr
              (relativeMapHomRestrict_comp_ι φ ψ)).hom.app (relativeTwist B n) ≫
            (Scheme.Modules.pullbackComp
              ((relativeProj C).scheme.homOfLE (relativeMapDomain_comp_le φ ψ))
              (relativeMapHom ψ)).inv.app (relativeTwist B n) ≫
            (Scheme.Modules.pullback ((relativeProj C).scheme.homOfLE
              (relativeMapDomain_comp_le φ ψ))).map (relativeTwistMap ψ n) ≫
            (Scheme.Modules.pullbackComp
              ((relativeProj C).scheme.homOfLE (relativeMapDomain_comp_le φ ψ))
              ψ.relativeMapDomain.ι).hom.app (relativeTwist C n) ≫
            (Scheme.Modules.pullbackCongr (Scheme.homOfLE_ι (relativeProj C).scheme
              (relativeMapDomain_comp_le φ ψ))).hom.app (relativeTwist C n) =
          relativeTwistMap (ψ.comp φ) n

Tag 07ZI, a lemma

Tag 07ZI in the Stacks Project.

Stacks.AlgebraicGeometry.Tag07ZGTwistStatement.domain_closedImmersion_twistEpi_of_eventually_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphism/TwistEventualStatement.lean, line 87. The attribute's comment: “the tag's three assertions in one statement: under degreewise surjectivity in all large degrees the domain of definition is all of Proj_S(B), the induced morphism r_ψ is a closed immersion, and every comparison map θ_n on twists is an epimorphism”. References: EGA II (2.9.2), “more general”.

[Stacks, Tag 07ZI]. Let S be a scheme, let A and B be quasi-coherent graded 𝒪_S-algebras and let ψ : A ⟶ B be a homomorphism between them. If A_d → B_d is surjective for all sufficiently large d, then U(ψ) = Y, the morphism r_ψ : U(ψ) ⟶ X of Tag 07ZG is a closed immersion, and every map θ_n : r_ψ^* 𝒪_X(n) ⟶ 𝒪_Y(n)|_{U(ψ)} is an epimorphism.

The three conjuncts are, in order:

The open of Y = Proj_S(B) on which ψ induces a morphism is all of Y.

That morphism is a closed immersion.

For every n : ℤ the comparison map on the n-th twist is an epimorphism.

Each is the corresponding component declaration: Stacks.AlgebraicGeometry.RelativeProjMapDomain.relativeMapDomain_eq_top_of_eventually_epi, Stacks.AlgebraicGeometry.RelativeProjMapDomain.isClosedImmersion_relativeMapHom_of_eventually_epi and Stacks.AlgebraicGeometry.Tag07ZGTwist.epi_relativeTwistMap_of_eventually_epi. The only hypothesis is the source's, degreewise surjectivity in all large degrees.

theorem domain_closedImmersion_twistEpi_of_eventually_epi
    (hsurj : ∀ᶠ d : ℕ in atTop, Epi (ψ.app (d : ℤ))) :
    ψ.relativeMapDomain = ⊤ ∧
      IsClosedImmersion (relativeMapHom ψ) ∧
      ∀ n : ℤ, Epi (relativeTwistMap ψ n)

Tag 07ZJ, a lemma

Tag 07ZJ in the Stacks Project.

Stacks.AlgebraicGeometry.Tag07ZGTwistStatement.domain_isIso_twistIsIso_of_eventually_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphism/TwistEventualStatement.lean, line 117. The attribute's comment: “the tag's three assertions in one statement: under degreewise invertibility in all large degrees the domain of definition is all of Proj_S(B), the induced morphism r_ψ is an isomorphism, and every comparison map θ_n on twists is an isomorphism”. References: EGA II (3.6.1), “TN-bijective clause”.

[Stacks, Tag 07ZJ]. Let S be a scheme, let A and B be quasi-coherent graded 𝒪_S-algebras and let ψ : A ⟶ B be a homomorphism between them. If A_d → B_d is an isomorphism for all sufficiently large d, then U(ψ) = Y, the morphism r_ψ : U(ψ) ⟶ X of Tag 07ZG is an isomorphism, and every map θ_n : r_ψ^* 𝒪_X(n) ⟶ 𝒪_Y(n)|_{U(ψ)} is an isomorphism.

The three conjuncts are, in order:

The open of Y = Proj_S(B) on which ψ induces a morphism is all of Y.

That morphism is an isomorphism.

For every n : ℤ the comparison map on the n-th twist is an isomorphism.

Each is the corresponding component declaration: Stacks.AlgebraicGeometry.RelativeProjMapDomain.relativeMapDomain_eq_top_of_eventually_isIso, Stacks.AlgebraicGeometry.RelativeProjMapDomain.isIso_relativeMapHom_of_eventually_isIso and Stacks.AlgebraicGeometry.Tag07ZGTwist.isIso_relativeTwistMap_of_eventually_isIso. The only hypothesis is the source's, degreewise invertibility in all large degrees.

theorem domain_isIso_twistIsIso_of_eventually_isIso
    (hbij : ∀ᶠ d : ℕ in atTop, IsIso (ψ.app (d : ℤ))) :
    ψ.relativeMapDomain = ⊤ ∧
      IsIso (relativeMapHom ψ) ∧
      ∀ n : ℤ, IsIso (relativeTwistMap ψ n)

Tag 07ZK, a lemma

Tag 07ZK in the Stacks Project.

Stacks.AlgebraicGeometry.Tag07ZGTwistStatement.domain_closedImmersion_twistIsIso_of_generatedInDegreeOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphism/TwistEventualStatement.lean, line 149. The attribute's comment: “the tag's three assertions in one statement: under degreewise surjectivity in all large degrees and generation in degree one the domain of definition is all of Proj_S(B), the induced morphism r_ψ is a closed immersion, and every comparison map θ_n on twists is an isomorphism”. References: EGA II (3.5.1), “special case”.

[Stacks, Tag 07ZK]. Let S be a scheme, let A and B be quasi-coherent graded 𝒪_S-algebras and let ψ : A ⟶ B be a homomorphism between them. If A_d → B_d is surjective for all sufficiently large d and A is generated by A_1 over A_0, then U(ψ) = Y, the morphism r_ψ : U(ψ) ⟶ X of Tag 07ZG is a closed immersion, and every map θ_n : r_ψ^* 𝒪_X(n) ⟶ 𝒪_Y(n)|_{U(ψ)} is an isomorphism.

The three conjuncts are, in order:

The open of Y = Proj_S(B) on which ψ induces a morphism is all of Y.

That morphism is a closed immersion.

For every n : ℤ the comparison map on the n-th twist is an isomorphism.

The first two are the two component declarations of Tag 07ZI, Stacks.AlgebraicGeometry.RelativeProjMapDomain.relativeMapDomain_eq_top_of_eventually_epi and Stacks.AlgebraicGeometry.RelativeProjMapDomain.isClosedImmersion_relativeMapHom_of_eventually_epi, which need only the surjectivity hypothesis; the third is Stacks.AlgebraicGeometry.Tag07ZGTwist.isIso_relativeTwistMap_of_generatedInDegreeOne, which uses both. Generation in degree one is read over the affine opens of the base, which is where the graded algebras have graded rings of sections.

theorem domain_closedImmersion_twistIsIso_of_generatedInDegreeOne
    (hsurj : ∀ᶠ d : ℕ in atTop, Epi (ψ.app (d : ℤ)))
    (hgen : ∀ U : S.Opens, IsAffineOpen U → A.IsGeneratedInDegreeOneAt U) :
    ψ.relativeMapDomain = ⊤ ∧
      IsClosedImmersion (relativeMapHom ψ) ∧
      ∀ n : ℤ, IsIso (relativeTwistMap ψ n)

Sources

LeanStacks.AlgebraicGeometry.Tag07ZGTwist.relativeProjMapTriple · Stacks.AlgebraicGeometry.Tag07ZGTwistStatement.relativeMapDomain_mapHom_twistMap_comp · Stacks.AlgebraicGeometry.Tag07ZGTwistStatement.domain_closedImmersion_twistEpi_of_eventually_epi · Stacks.AlgebraicGeometry.Tag07ZGTwistStatement.domain_isIso_twistIsIso_of_eventually_isIso · Stacks.AlgebraicGeometry.Tag07ZGTwistStatement.domain_closedImmersion_twistIsIso_of_generatedInDegreeOne

Section27.19 Invertible sheaves and morphisms into relative Proj #

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

Tag 01O8, the section

Tag 01O8 in the Stacks Project.

Stacks.AlgebraicGeometry.RelativeProjInvertibleMorphism.GradedPowerMap.value_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjInvertibleMorphism/Locus.lean, line 120. The attribute's comment: “item (6): the components of psi are multiplicative across degrees, the value at a product of homogeneous sections over an open of the base being the product of the values in the tensor powers of L over the preimage of that open”.

ψ is multiplicative across degrees on values: ψ(a · b) = ψ(a) · ψ(b) in Γ(f^{-1}(V), ℒ^{⊗ (n + m)}).

public theorem value_mul (n m : ℕ) (V : S.Opens) (a : Γ(A.piece (n : ℤ), V))
    (b : Γ(A.piece (m : ℤ), V)) :
    P.value (n + m) V ((A.mul (n : ℤ) (m : ℤ)).app V a b)
      = Stacks.AlgebraicGeometry.NatTensorPowLocalMul.localMulSections P.L
          (P.value n V a) (P.value m V b)

Stacks.AlgebraicGeometry.RelativeProjInvertibleMorphism.GradedPowerMap.coveringOpen, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjInvertibleMorphism/Locus.lean, line 175. The attribute's comment: “the open U(psi) = union over triples (U, V, a) -- V affine open of the base, U = f^{-1}(V), a a homogeneous section of positive degree of A over V -- of the open U_{psi(a)} on which the section psi(a) of L^{tensor deg(a)} over U does not vanish”.

The open U(ψ) = ⋃_{(U, V, a)} U_{ψ(a)}: the union of the opens on which the values of ψ at the homogeneous sections of positive degree over the affine opens of the base do not vanish.

public def coveringOpen : T.Opens

Tag 01O9, a lemma

Tag 01O9 in the Stacks Project.

Stacks.AlgebraicGeometry.RelativeProjInvertibleMorphism.tag01O9, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjInvertibleMorphism/Statement.lean, line 87. The attribute's comment: “the open U(psi), the morphism r_{L,psi} : U(psi) -> Proj_S(A) over S and the unital map of graded algebras theta : r^*(sum_d O(d)) -> sum_d L^d|_{U(psi)}; properties (1), (2) and (3) for them; and every triple (U', r', theta') with properties (1), (2) and (3) is (U(psi), r_{L,psi}, theta)”.

[Stacks, Tag 01O9]. For ψ : f^*𝒜 ⟶ ⨁_{d} ℒ^{⊗ d} with ℒ invertible, put P = toGradedPowerMap ψ, U(ψ) = P.coveringOpen, r = P.globalMorphism (relativeProj A) and θ = P.theta. Then:

r is a morphism over S: r ≫ π = (U(ψ) ⊆ X) ≫ f;

θ preserves the unit, and its components in degrees d, e ≥ 0 are multiplicative, so that they form a map of graded algebras r^*(⨁_{d ≥ 0} 𝒪(d)) ⟶ ⨁_{d ≥ 0} ℒ^{⊗ d}|_{U(ψ)};

property (1): for every open V ⊆ S, d ≥ 0 and a ∈ 𝒜_d(V), θ carries the pullback along r of the section ψ(a) of 𝒪(d) over π^{-1}(V) to ψ(a) restricted to f^{-1}(V) ∩ U(ψ) = r^{-1}(π^{-1}(V));

property (2): for every d ≥ 1 and every open W ⊆ X on which ψ_d : f^*𝒜_d|_W ⟶ ℒ^{⊗ d}|_W is surjective, W ⊆ U(ψ) and r|_W is the morphism W ⟶ Proj_S(𝒜) which the representation of the functor of quadruples by Proj_S(𝒜) attaches to (d, f|_W, ℒ^{⊗ d}|_W, ψ|_W);

property (3), for the open and the morphism: for every affine open V ⊆ S, with ψ' : 𝒜(V) ⟶ Γ_*(f^{-1}(V), ℒ) the induced map, U(ψ') = U(ψ) ∩ f^{-1}(V) and r restricted along U(ψ') ⟶ U(ψ) is i_V ∘ r_{ℒ, ψ'}; and any morphism U(ψ) ⟶ Proj_S(𝒜) with that restriction property over every affine V is r;

the triple (U(ψ), r, θ) (with θ in degrees d ≥ 0) is Triple.canonical P, and it has properties (1), (2) and (3), property (3) including that θ restricted along U(ψ') ⟶ U(ψ) is the θ' of the induced map, read through i_V;

the characterization: every triple (U', r', θ') with properties (1), (2) and (3) is (U(ψ), r, θ).

theorem tag01O9 :
    (toGradedPowerMap ψ).globalMorphism (relativeProj A) ≫ (relativeProj A).toBase
        = (toGradedPowerMap ψ).coveringOpen.ι ≫ f
      ∧ SheafOfModules.sectionsMap (((toGradedPowerMap ψ).theta).app 0)
          (Stacks.Conormal.gradedPullback ((toGradedPowerMap ψ).globalMorphism (relativeProj A))
            (GluedTwistAlgebra.twistDataOfGradedAlgebra A).algebra).one
        = (Stacks.AlgebraicGeometry.ProjChartGradedTriple.laurentOn L
            (toGradedPowerMap ψ).coveringOpen).one
      ∧ (∀ (d e : ℕ) (U : (toGradedPowerMap ψ).coveringOpen.toScheme.Opens)
          (x : ((Stacks.Conormal.gradedPullback
            ((toGradedPowerMap ψ).globalMorphism (relativeProj A))
            (GluedTwistAlgebra.twistDataOfGradedAlgebra A).algebra).piece (d : ℤ)).val.obj (op U))
          (y : ((Stacks.Conormal.gradedPullback
            ((toGradedPowerMap ψ).globalMorphism (relativeProj A))
            (GluedTwistAlgebra.twistDataOfGradedAlgebra A).algebra).piece (e : ℤ)).val.obj (op U)),
          (((toGradedPowerMap ψ).theta.app ((d : ℤ) + (e : ℤ))).val.app (op U)
              (((Stacks.Conormal.gradedPullback
                ((toGradedPowerMap ψ).globalMorphism (relativeProj A))
                (GluedTwistAlgebra.twistDataOfGradedAlgebra A).algebra).mul d e).app (op U) x y))
            = ((Stacks.AlgebraicGeometry.ProjChartGradedTriple.laurentOn L
                (toGradedPowerMap ψ).coveringOpen).mul d e).app (op U)
                (((toGradedPowerMap ψ).theta.app d).val.app (op U) x)
                (((toGradedPowerMap ψ).theta.app e).val.app (op U) y))
      ∧ (∀ (V : S.Opens) (d : ℕ) (a : Γ(A.piece (d : ℤ), V)),
          ((tensorPowerModule X L (d : ℤ)).restrict
            (toGradedPowerMap ψ).coveringOpen.ι).presheaf.map
              (eqToHom ((toGradedPowerMap ψ).toBase_preimage_eq V)).op
              (((toGradedPowerMap ψ).theta.app d).val.app
                (op ((toGradedPowerMap ψ).globalMorphism (relativeProj A) ⁻¹ᵁ
                  ((relativeProj A).toBase ⁻¹ᵁ V)))
                (Stacks.RingedSpace.pullbackUnit
                  ((toGradedPowerMap ψ).globalMorphism (relativeProj A)).toLRSHom.toShHom
                  ((GluedTwistAlgebra.twistDataOfGradedAlgebra A).algebra.piece (d : ℤ))
                  (op ((relativeProj A).toBase ⁻¹ᵁ V))
                  (((GluedTwistAlgebra.twistDataOfGradedAlgebra A).ψ d).app V a)))
            = (tensorPowerModule X L (d : ℤ)).presheaf.map
                (homOfLE ((toGradedPowerMap ψ).coveringOpen.ι.image_preimage_le (f ⁻¹ᵁ V))).op
                ((Stacks.AlgebraicGeometry.CoherentMulSections.powCompare L d).hom.app (f ⁻¹ᵁ V)
                  (valueSec ψ d V a)))
      ∧ (∀ {k : ℕ} (hk : 0 < k) (W : X.Opens) [Epi ((ψ.pullback W.ι).app (k : ℤ))],
          ∃ h : W ≤ (toGradedPowerMap ψ).coveringOpen,
            X.homOfLE h ≫ (toGradedPowerMap ψ).globalMorphism (relativeProj A)
              = F.classifyingMorphism A (F.mk (W.ι ≫ f) (by exact_mod_cast hk)
                  (restrictQuadruple ψ W k)))
      ∧ (∀ V : S.affineOpens,
          (f ⁻¹ᵁ V.1).ι ''ᵁ ((toGradedPowerMap ψ).affineDatum V.1).coveringOpen
              = (toGradedPowerMap ψ).coveringOpen ⊓ f ⁻¹ᵁ V.1
            ∧ ∀ j : (((toGradedPowerMap ψ).affineDatum V.1).coveringOpen).toScheme ⟶
                (toGradedPowerMap ψ).coveringOpen.toScheme,
              j ≫ (toGradedPowerMap ψ).coveringOpen.ι
                  = (((toGradedPowerMap ψ).affineDatum V.1).coveringOpen).ι ≫ (f ⁻¹ᵁ V.1).ι →
                j ≫ (toGradedPowerMap ψ).globalMorphism (relativeProj A)
                  = ((toGradedPowerMap ψ).affineDatum V.1).glued ≫ (relativeProj A).chart V.1 V.2)
      ∧ (∀ R : (toGradedPowerMap ψ).coveringOpen.toScheme ⟶ (relativeProj A).scheme,
          (∀ V : S.affineOpens,
            ∀ j : (((toGradedPowerMap ψ).affineDatum V.1).coveringOpen).toScheme ⟶
                (toGradedPowerMap ψ).coveringOpen.toScheme,
              j ≫ (toGradedPowerMap ψ).coveringOpen.ι
                  = (((toGradedPowerMap ψ).affineDatum V.1).coveringOpen).ι ≫ (f ⁻¹ᵁ V.1).ι →
                j ≫ R = ((toGradedPowerMap ψ).affineDatum V.1).glued
                  ≫ (relativeProj A).chart V.1 V.2) →
          R = (toGradedPowerMap ψ).globalMorphism (relativeProj A))
      ∧ Triple.canonical (toGradedPowerMap ψ)
          = ⟨(toGradedPowerMap ψ).coveringOpen,
              (toGradedPowerMap ψ).globalMorphism (relativeProj A),
              GradedNonnegHom.ofHom (toGradedPowerMap ψ).theta⟩
      ∧ Triple.IsTriple ψ (Triple.canonical (toGradedPowerMap ψ))
      ∧ (∀ t : Triple A L, Triple.IsTriple ψ t → t = Triple.canonical (toGradedPowerMap ψ))

Sources

LeanStacks.AlgebraicGeometry.RelativeProjInvertibleMorphism.GradedPowerMap.value_mul · Stacks.AlgebraicGeometry.RelativeProjInvertibleMorphism.GradedPowerMap.coveringOpen · Stacks.AlgebraicGeometry.RelativeProjInvertibleMorphism.tag01O9

Section27.20 Twisting by invertible sheaves and relative Proj #

Section 27.20 of the Stacks Project, Tag 02NB. 2 tags here are carried by 1 declaration of the repository (in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02NB, the section

Tag 02NB in the Stacks Project.

Declarations registered for the tag:

twist registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/GradedAlgebraTwist/Basic.lean, line 1285 (StacksFrontier): “the twisted graded algebra B_d = A_d ⊗ L^{⊗ d} of the section's setting”.

Tag 02NC, a lemma

Tag 02NC in the Stacks Project.

Stacks.AlgebraicGeometry.RelativeInvertibleTwist.relativeTwist_tag, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjInvertibleTwistRelativeTag.lean, line 77. The attribute's comment: “the canonical isomorphism g from Proj_S(A) to Proj_S(B) over S, with (1) the isomorphisms theta_n from g^O_P'(n) to O_P(n) tensor pi^L^n fitting together into an isomorphism of Z-graded algebras theta, and (2) the commuting diagrams on sections over every open V of S, theta being the unique such map”.

Let S be a scheme, 𝒜 a quasi-coherent graded 𝒪_S-algebra, ℒ an invertible 𝒪_S-module and ℬ = ⨁_d 𝒜_d ⊗_{𝒪_S} ℒ^{⊗ d}, with π : P = Proj_S(𝒜) ⟶ S and π' : P' = Proj_S(ℬ) ⟶ S. The canonical morphism g = relativeTwistHom L 𝒜 : P ⟶ P':

is an isomorphism, and a morphism over S: π' ∘ g = π;

is canonical, with nothing chosen: g⁻¹ restricts, over every affine open V of S and every section x of ℒ over V whose powers trivialize the powers of ℒ there, to the morphism of homogeneous spectra induced by the comparison a ↦ a ⊗ x^d, and it is the only isomorphism P' ≅ P over S doing so;

(1) carries isomorphisms θ_n = twistThetaIso L 𝒜 n : g^*𝒪_{P'}(n) ≅ 𝒪_P(n) ⊗ π^*ℒ^{⊗ n} for every n : ℤ, which fit together into the isomorphism of sheaves of ℤ-graded algebras θ = twistTheta L 𝒜 : g^*(⨁_n 𝒪_{P'}(n)) ≅ ⨁_n 𝒪_P(n) ⊗ π^*ℒ^{⊗ n}, its component in degree n being θ_n; θ preserves the unit;

(2) for every open V ⊆ S and every n, the square of the source commutes: the image under θ_n of the section of 𝒪_{P'}(n) over π'^{-1}V given by a ⊗ l ∈ ℬ_n(V) (a ∈ 𝒜_n(V), l ∈ ℒ^{⊗ n}(V)) is ψ(a) ⊗ π^*l over π^{-1}V;

θ is canonical, with nothing chosen: it is the only homomorphism of sheaves of graded algebras g^*(⨁_n 𝒪_{P'}(n)) ⟶ ⨁_n 𝒪_P(n) ⊗ π^*ℒ^{⊗ n} making the squares of (2) commute.

theorem relativeTwist_tag :
    IsIso (relativeTwistHom L 𝒜 : (relativeProj 𝒜).scheme ⟶ (relativeProj (twist 𝒜 L)).scheme) ∧
      relativeTwistHom L 𝒜 ≫ (relativeProj (twist 𝒜 L)).toBase = (relativeProj 𝒜).toBase ∧
      (relativeTwistIso L 𝒜).inv = relativeTwistHom L 𝒜 ∧
      (∀ (V : S.Opens) (hV : IsAffineOpen V) (x : (tp L 1).val.obj (op V))
          (hx : ∀ d : ℕ, 0 < d → TrivializesPower L V x d),
          (relativeProj (twist 𝒜 L)).chart V hV ≫ (relativeTwistIso L 𝒜).hom =
            projMap_psiSectionAt L 𝒜 hx ≫ (relativeProj 𝒜).chart V hV) ∧
      (∀ e : (relativeProj (twist 𝒜 L)).scheme ≅ (relativeProj 𝒜).scheme,
          (∀ (V : S.Opens) (hV : IsAffineOpen V) (x : (tp L 1).val.obj (op V))
              (hx : ∀ d : ℕ, 0 < d → TrivializesPower L V x d),
              (relativeProj (twist 𝒜 L)).chart V hV ≫ e.hom =
                projMap_psiSectionAt L 𝒜 hx ≫ (relativeProj 𝒜).chart V hV) →
            e.hom ≫ (relativeProj 𝒜).toBase = (relativeProj (twist 𝒜 L)).toBase →
            e = relativeTwistIso L 𝒜) ∧
      (∀ n : ℤ, (targetAlgebra L 𝒜).piece n =
        tensorMod (Tag07ZGTwist.relativeTwist 𝒜 n)
          ((Scheme.Modules.pullback (relativeProj 𝒜).toBase).obj (tpMod L n))) ∧
      (∀ n : ℤ, (twistTheta L 𝒜 :
          Stacks.RingedSpace.pullbackGradedAlgebra (relativeTwistHom L 𝒜).toLRSHom.toShHom
              (Tag07ZGTwist.twistAlgebra (twist 𝒜 L)) ≅ targetAlgebra L 𝒜).hom.app n =
        (twistThetaIso L 𝒜 n :
          (Scheme.Modules.pullback (relativeTwistHom L 𝒜)).obj
              (Tag07ZGTwist.relativeTwist (twist 𝒜 L) n) ≅
            tensorMod (Tag07ZGTwist.relativeTwist 𝒜 n)
              ((Scheme.Modules.pullback (relativeProj 𝒜).toBase).obj (tpMod L n))).hom) ∧
      (∀ W : (relativeProj 𝒜).scheme.Opensᵒᵖ,
        ((twistTheta L 𝒜).hom.app 0).val.app W
            ((Stacks.RingedSpace.pullbackGradedAlgebra (relativeTwistHom L 𝒜).toLRSHom.toShHom
              (Tag07ZGTwist.twistAlgebra (twist 𝒜 L))).one.eval W) =
          (targetAlgebra L 𝒜).one.eval W) ∧
      (∀ (n : ℕ) (V : S.Opens),
        (∀ (a : Γ(𝒜.piece (n : ℤ), V)) (l : Γ(tpMod L (n : ℤ), V)),
          thetaSections (relativeProj 𝒜).toBase (relativeProj (twist 𝒜 L)).toBase
              (relativeTwistHom L 𝒜) (relativeTwistHom_comp_toBase L 𝒜)
              (twistThetaIso L 𝒜 n).hom V
              (((GluedTwistAlgebra.twistDataOfGradedAlgebra (twist 𝒜 L)).ψ n).val.app (op V)
                (gammaTmul (𝒜.piece (n : ℤ)) (tpMod L (n : ℤ)) V a l)) =
            gammaTmul (Tag07ZGTwist.relativeTwist 𝒜 n)
              ((Scheme.Modules.pullback (relativeProj 𝒜).toBase).obj (tpMod L n))
              ((relativeProj 𝒜).toBase ⁻¹ᵁ V)
              (((GluedTwistAlgebra.twistDataOfGradedAlgebra 𝒜).ψ n).val.app (op V) a)
              (((Scheme.Modules.pullbackPushforwardAdjunction (relativeProj 𝒜).toBase).unit.app
                (tpMod L n)).val.app (op V) l)) ∧
        ∀ z : Γ(𝒜.piece (n : ℤ), V) ⊗[Γ(S, V)] Γ(tpMod L (n : ℤ), V),
          thetaSections (relativeProj 𝒜).toBase (relativeProj (twist 𝒜 L)).toBase
              (relativeTwistHom L 𝒜) (relativeTwistHom_comp_toBase L 𝒜)
              (twistThetaIso L 𝒜 n).hom V
              (((GluedTwistAlgebra.twistDataOfGradedAlgebra (twist 𝒜 L)).ψ n).val.app (op V)
                (gammaTensorMap (𝒜.piece (n : ℤ)) (tpMod L (n : ℤ)) V z)) =
            lowerRoute (relativeProj 𝒜).toBase ((GluedTwistAlgebra.twistDataOfGradedAlgebra 𝒜).ψ n)
              V z) ∧
      (∀ α : Stacks.RingedSpace.pullbackGradedAlgebra (relativeTwistHom L 𝒜).toLRSHom.toShHom
            (Tag07ZGTwist.twistAlgebra (twist 𝒜 L)) ⟶ targetAlgebra L 𝒜,
          (∀ (n : ℕ) (V : S.Opens) (a : Γ(𝒜.piece (n : ℤ), V)) (l : Γ(tpMod L (n : ℤ), V)),
            thetaSections (relativeProj 𝒜).toBase (relativeProj (twist 𝒜 L)).toBase
                (relativeTwistHom L 𝒜) (relativeTwistHom_comp_toBase L 𝒜) (α.app (n : ℤ)) V
                (((GluedTwistAlgebra.twistDataOfGradedAlgebra (twist 𝒜 L)).ψ n).val.app (op V)
                  (gammaTmul (𝒜.piece (n : ℤ)) (tpMod L (n : ℤ)) V a l)) =
              gammaTmul (Tag07ZGTwist.relativeTwist 𝒜 n)
                ((Scheme.Modules.pullback (relativeProj 𝒜).toBase).obj (tpMod L n))
                ((relativeProj 𝒜).toBase ⁻¹ᵁ V)
                (((GluedTwistAlgebra.twistDataOfGradedAlgebra 𝒜).ψ n).val.app (op V) a)
                (((Scheme.Modules.pullbackPushforwardAdjunction (relativeProj 𝒜).toBase).unit.app
                  (tpMod L n)).val.app (op V) l)) →
          α = (twistTheta L 𝒜).hom)

Sources

Leantwist · Stacks.AlgebraicGeometry.RelativeInvertibleTwist.relativeTwist_tag

Section27.21 Projective bundles #

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

Tag 01OB, a definition

Tag 01OB in the Stacks Project.

Stacks.RelativeProj.projectiveBundle, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjBundle/Basic.lean, line 83. The attribute's comment: “the projective bundle and its projection”. References: EGA II (4.1.1), “P(E) itself”.

The projective bundle 𝐏(F) = Proj_X(Sym(F)) of a quasi-coherent sheaf of modules, the relative projective spectrum of its symmetric algebra.

abbrev projectiveBundle (X : Scheme.{u}) (F : X.Modules) [F.IsQuasicoherent] : Scheme.{u}

Stacks.RelativeProj.projectiveBundleToBase, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjBundle/Basic.lean, line 89. The attribute's comment: “the projective bundle and its projection”. References: EGA II (4.1.1), “projection to Y”.

The projection π : 𝐏(F) ⟶ X of a projective bundle, the structure morphism of the relative projective spectrum of Sym(F) over its base.

abbrev projectiveBundleToBase (X : Scheme.{u}) (F : X.Modules) [F.IsQuasicoherent] :
    projectiveBundle X F ⟶ X

Tag 0FCY, an example

Tag 0FCY in the Stacks Project.

Stacks.AlgebraicGeometry.ProjectiveSpaceOfModuleStatement.coordinates_bundle_points_sections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjectiveSpaceOfModuleStatement.lean, line 90. The attribute's comment: “the five assertions of the tag in one statement”.

[Stacks, Tag 0FCY]. Let k be a field and V a k-vector space, and let 𝐏(V) = Proj(Sym_k V) be the projective space of V, with its structure morphism to Spec k. Then:

if dim V = n + 1 then 𝐏(V) is isomorphic to ℙⁿ_k as a scheme over Spec k;

𝐏(V) is the projective space bundle over Spec k of V read as a quasi-coherent module on Spec k, by an isomorphism carrying the bundle projection to the structure morphism;

the k-valued points of 𝐏(V), that is the sections of its structure morphism, correspond to the one-dimensional quotients of V, a point going to the space of vectors whose degree-one forms vanish at it;

for every scheme X over k, every invertible 𝒪_X-module ℒ and every k-linear map ψ : V → Γ(X, ℒ) whose image generates ℒ, the morphism φ_{ℒ,ψ} : X ⟶ 𝐏(V) is a morphism over Spec k, and there is an isomorphism θ : φ_{ℒ,ψ}^*𝒪_{𝐏(V)}(1) ≅ ℒ through which each v : V is sent to ψ v by the universal degree-one section of v;

for every basis v₀, …, vₙ of V, the composite of φ_{ℒ,ψ} with the coordinate isomorphism 𝐏(V) ≅ ℙⁿ_k of that basis is the morphism X ⟶ ℙⁿ_k of [Stacks, Tag 01ND] for the sections ψ(v₀), …, ψ(vₙ).

theorem coordinates_bundle_points_sections :
    (∀ n : ℕ, Module.finrank k V = n + 1 →
        Nonempty ((projectiveSpaceOfModule k V).asOver (Spec (.of k)) ≅
          (projectiveSpaceOverRing n (.of k)).asOver (Spec (.of k)))) ∧
      (∃ e : projectiveSpaceOfModule k V ≅
          Stacks.RelativeProj.projectiveBundle (Spec (.of k)) (tildeOfModule k V),
        e.hom ≫ Stacks.RelativeProj.projectiveBundleToBase (Spec (.of k)) (tildeOfModule k V) =
          projectiveSpaceOfModuleToSpec k V) ∧
      (∃ E : {p : Spec (.of k) ⟶ projectiveSpaceOfModule k V //
            p ≫ projectiveSpaceOfModuleToSpec k V = 𝟙 (Spec (.of k))} ≃
          {K : Submodule k V // Module.finrank k (V ⧸ K) = 1},
        ∀ p v, v ∈ (E p).val ↔
          SymmetricAlgebra.ι k V v ∈ (p.val.base default).asHomogeneousIdeal) ∧
      ∀ {X : Scheme.{u}} [X.Over (Spec (.of k))] (L : X.Modules)
          [Stacks.Ample.IsInvertibleModule X L] (ψ : V →ₗ[k] Γ(L, ⊤))
          (hψ : ⨆ v : V, nonvanishingOpen X L (ψ v) = ⊤),
        morphismOfGeneratingSections k V L ψ hψ ≫ projectiveSpaceOfModuleToSpec k V =
            X ↘ Spec (.of k) ∧
          (∃ θ : pullbackTwistOne (grading k V) (morphismOfGeneratingSections k V L ψ hψ) ≅ L,
            ∀ v : V, θ.hom.app ⊤ (pullbackSectionOne (grading k V)
              (morphismOfGeneratingSections k V L ψ hψ) (degreeOneElement k V v)) = ψ v) ∧
          ∀ {n : ℕ} (b : Module.Basis (Fin (n + 1)) k V),
            morphismOfGeneratingSections k V L ψ hψ ≫
                (basisProjectiveSpaceOfModuleIso b).hom.left =
              Stacks.ProjectiveFromSections.toProjectiveSpaceOver (basisSections b ψ)
                (generatesStalks_basisSections b ψ hψ) (X ↘ Spec (.of k))

Tag 01OC, an example

Tag 01OC in the Stacks Project.

Stacks.ProjectiveBundle.Noninjective.isSymmetricAlgebra_toQuotientAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundle/Noninjective.lean, line 180. The attribute's comment: “the presentation of the symmetric algebra of the module”.

Sym(M) = A[x, y] / (ū x + v̄ y). This is the displayed identity of Stacks 01OC that makes the example concrete: M is A x ⊕ A y modulo the single relation ū x + v̄ y, so its symmetric algebra is the polynomial ring A[x, y] modulo the ideal generated by that same linear form, which symmetricAlgebra_relationForm_eq identifies.

public theorem isSymmetricAlgebra_toQuotientAlgebra :
    IsSymmetricAlgebra
      (SymmetricAlgebra.toQuotientAlgebra (coefficientRing R) (relationVector R))

Stacks.ProjectiveBundle.Noninjective.counterexampleSection_mapsTo_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundle/Noninjective.lean, line 193. The attribute's comment: “the section maps to zero in the first twist”.

m maps to zero in Γ(P, 𝒪_P(1)).

public theorem counterexampleSection_mapsTo_zero :
    SymmetricAlgebra.toTwistSections (coefficientRing R) (presentedModule R)
      (counterexampleSection R) = 0

Stacks.ProjectiveBundle.Noninjective.iSup_basicOpen_symGen_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundle/Noninjective.lean, line 202. The attribute's comment: “the two-chart affine open covering of the projective bundle”.

P = D₊(x) ∪ D₊(y): the two standard opens of the degree-one generators cover the projective bundle. This is the affine open covering Stacks 01OC records.

public theorem iSup_basicOpen_symGen_eq_top :
    ⨆ i : Fin 2, Proj.basicOpen
      (SymmetricAlgebra.grading (coefficientRing R) (presentedModule R)) (symGen R i) = ⊤

Stacks.ProjectiveBundle.Noninjective.basicOpen_symGen_sup_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundle/Noninjective.lean, line 221. The attribute's comment: “the two-chart affine open covering of the projective bundle”.

P = D₊(x) ∪ D₊(y), written as a binary union.

public theorem basicOpen_symGen_sup_eq_top :
    Proj.basicOpen (SymmetricAlgebra.grading (coefficientRing R) (presentedModule R))
        (symGen R 0) ⊔
      Proj.basicOpen (SymmetricAlgebra.grading (coefficientRing R) (presentedModule R))
        (symGen R 1) = ⊤

Stacks.ProjectiveBundle.Noninjective.not_injective_toTwistSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundle/Noninjective.lean, line 245. The attribute's comment: “the map from the first symmetric power is not injective”.

The map M = Sym¹(ℰ) → Γ(P, 𝒪_P(1)) is not injective. This is the conclusion of Stacks 01OC: m is a nonzero global section of ℰ whose image in Γ(P, 𝒪_P(1)) is zero, so the canonical map Sym¹(ℰ) → π_* 𝒪_{𝐏(ℰ)}(1) of Stacks 01OB is not injective, and in particular not an isomorphism.

public theorem not_injective_toTwistSections :
    ¬ Function.Injective
      (SymmetricAlgebra.toTwistSections (coefficientRing R) (presentedModule R))

Stacks.ProjectiveBundle.Noninjective.counterexampleSection_ne_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundle/NoninjectiveAlgebra.lean, line 259. The attribute's comment: “the section is nonzero”.

For a nontrivial ring R, the element m = ū s̄₁ x + v̄ t̄₂ y of M is nonzero.

public theorem counterexampleSection_ne_zero : counterexampleSection R ≠ 0

Stacks.ProjectiveBundle.Noninjective.X_zero_mul_counterexampleForm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundle/NoninjectiveAlgebra.lean, line 318. The attribute's comment: “the first displayed congruence”.

In A[x, y], x (ū s̄₁ x + v̄ t̄₂ y) = (s̄₁ x + s̄₂ y)(ū x + v̄ y).

public theorem X_zero_mul_counterexampleForm :
    X 0 * counterexampleForm R =
      (C (coefficient R 2) * X 0 + C (coefficient R 3) * X 1) * relationForm R

Stacks.ProjectiveBundle.Noninjective.X_one_mul_counterexampleForm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundle/NoninjectiveAlgebra.lean, line 327. The attribute's comment: “the second displayed congruence”.

In A[x, y], y (ū s̄₁ x + v̄ t̄₂ y) = (t̄₁ x + t̄₂ y)(ū x + v̄ y).

public theorem X_one_mul_counterexampleForm :
    X 1 * counterexampleForm R =
      (C (coefficient R 4) * X 0 + C (coefficient R 5) * X 1) * relationForm R

Tag 01OD, a lemma

Tag 01OD in the Stacks Project.

Stacks.SymGraded.isSeparated_projectiveBundleToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundle/SectionClosedImmersion.lean, line 81.

The structure morphism of the projective bundle of a quasi-coherent module on an arbitrary scheme is separated.

This is Stacks.SymGraded.isSeparated_schemeProjectiveBundleToBase with its quasi-coherence hypothesis discharged, and it is the single assertion of Tag 01OD.

public theorem isSeparated_projectiveBundleToBase :
    IsSeparated
      (schemeProjectiveBundle E (isQuasicoherentPieces_of_isQuasicoherent E)).toBase

Tag 01OE, a lemma

Tag 01OE in the Stacks Project.

Stacks.SymGraded.projectiveBundleIsoProjectiveSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SheafSymmetricAlgebra/ProjectiveSpaceMorphism.lean, line 658.

ℙⁿ_X is a projective bundle over X: the projective bundle of the free module sheaf 𝒪_X^{n+1} — that is Proj_X(Sym(𝒪_X^{n+1})) — is projective n-space over X.

This is the isomorphism; Stacks.SymGraded.projectiveBundleIsoProjectiveSpace_hom_comp_fst is the other half of the statement, that it is an isomorphism over X.

def projectiveBundleIsoProjectiveSpace :
    (freeProjectiveBundle (X := X) n).scheme ≅
      AlgebraicGeometry.projectiveSpaceOver.{u} n X

Stacks.SymGraded.projectiveBundleIsoProjectiveSpace_hom_comp_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SheafSymmetricAlgebra/ProjectiveSpaceMorphism.lean, line 669.

The isomorphism of Tag 01OE is an isomorphism over X: it carries the structure morphism of ℙⁿ_X to the projection of the bundle. Together with Stacks.SymGraded.projectiveBundleIsoProjectiveSpace this is the whole assertion of the tag, which is that ℙⁿ_X is a projective bundle over X and not merely abstractly isomorphic to one.

theorem projectiveBundleIsoProjectiveSpace_hom_comp_fst :
    (projectiveBundleIsoProjectiveSpace (X := X) n).hom ≫
        pullback.fst (terminal.from X)
          (terminal.from (AlgebraicGeometry.projectiveSpaceAtUniverse.{u} n)) =
      (freeProjectiveBundle (X := X) n).toBase

Sources

LeanStacks.RelativeProj.projectiveBundle · Stacks.RelativeProj.projectiveBundleToBase · Stacks.AlgebraicGeometry.ProjectiveSpaceOfModuleStatement.coordinates_bundle_points_sections · Stacks.ProjectiveBundle.Noninjective.isSymmetricAlgebra_toQuotientAlgebra · Stacks.ProjectiveBundle.Noninjective.counterexampleSection_mapsTo_zero · Stacks.ProjectiveBundle.Noninjective.iSup_basicOpen_symGen_eq_top · Stacks.ProjectiveBundle.Noninjective.basicOpen_symGen_sup_eq_top · Stacks.ProjectiveBundle.Noninjective.not_injective_toTwistSections

Section27.22 Grassmannians #

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

Tag 089S, an equation

Tag 089S in the Stacks Project.

AlgebraicGeometry.Grassmannian.functor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Recovery27/Functor.lean, line 121.

The Grassmannian functor G(k, n) from schemes to sets, contravariant on morphisms by pullback.

public noncomputable def functor (k n : ℕ) :
    Scheme.{u}ᵒᵖ ⥤ Type u

Tag 089T, a lemma

Tag 089T in the Stacks Project.

AlgebraicGeometry.Grassmannian.functor_isRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Recovery27/Representable/Gluing.lean, line 537. References: SGA 6 VI (4.1), “Grassmannian, free case”.

The Grassmannian functor G(k, n) is representable by a scheme when 0 < k < n.

public theorem functor_isRepresentable (k n : ℕ) (hk : 0 < k) (hkn : k < n) :
    (functor.{u} k n).IsRepresentable

Tag 089U, a definition

Tag 089U in the Stacks Project.

AlgebraicGeometry.Grassmannian.scheme, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Recovery27/GrassmannianScheme.lean, line 58. The attribute's comment: “the Grassmannian over ℤ”. References: SGA 6 VI (4.9), “special case”.

The Grassmannian G(k, n) over the integers: the scheme representing the functor of finite locally free rank-n - k quotients of the free module of rank n.

public def scheme (k n : ℕ) : Scheme.{u}

AlgebraicGeometry.Grassmannian.schemeOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Recovery27/GrassmannianScheme.lean, line 72. The attribute's comment: “the Grassmannian over a scheme”. References: SGA 6 VI (4.9); SGA 7 XIX (1.4), “partial”.

The Grassmannian G(k, n)_S over a scheme S: the base change of the integral Grassmannian along the unique morphism S ⟶ Spec ℤ.

public abbrev schemeOver (k n : ℕ) (S : Scheme.{u}) : Scheme.{u}

AlgebraicGeometry.Grassmannian.schemeOverRing, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Recovery27/GrassmannianScheme.lean, line 97. The attribute's comment: “the Grassmannian over a ring”. References: SGA 6 VI (4.9), “G_S^(n, special case”; SGA 7 XIX (1.4), “partial”.

The Grassmannian G(k, n)_R over a commutative ring R: the base change of the integral Grassmannian to Spec R.

public abbrev schemeOverRing (k n : ℕ) (R : CommRingCat.{u}) : Scheme.{u}

Tag 089V, a lemma

Tag 089V in the Stacks Project.

Stacks.ProjectiveSpaceModuli.grassmannianSuccIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpaceModuli/Grassmannian.lean, line 357.

The Grassmannian G(n, n + 1) over the integers is isomorphic to projective n-space, by the comparison of their representations of the functor of finite locally free rank-one quotients of the free module of rank n + 1.

def grassmannianSuccIso (n : ℕ) :
    Grassmannian.scheme.{u} n (n + 1) ≅ projectiveSpaceAtUniverse.{u} n

Stacks.ProjectiveSpaceModuli.homEquiv_comp_grassmannianSuccIso_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpaceModuli/Grassmannian.lean, line 378. The attribute's comment: “the isomorphism matches the two moduli descriptions”.

The isomorphism G(n, n + 1) ≅ ℙⁿ_ℤ matches the two representations: the rank-one quotient classified by a morphism f to the Grassmannian is classified, after composing with the isomorphism, by the same point of the Grassmannian functor read through projective space.

theorem homEquiv_comp_grassmannianSuccIso_hom (n : ℕ) {Z : Scheme.{u}}
    (f : Z ⟶ Grassmannian.scheme.{u} n (n + 1)) :
    (projectiveSpaceRepresentableBy.{u} n).homEquiv (f ≫ (grassmannianSuccIso.{u} n).hom) =
      (Grassmannian.schemeRepresentableBy.{u} n (n + 1)).homEquiv f

Sources

LeanAlgebraicGeometry.Grassmannian.functor · AlgebraicGeometry.Grassmannian.functor_isRepresentable · AlgebraicGeometry.Grassmannian.scheme · AlgebraicGeometry.Grassmannian.schemeOver · AlgebraicGeometry.Grassmannian.schemeOverRing · Stacks.ProjectiveSpaceModuli.grassmannianSuccIso · Stacks.ProjectiveSpaceModuli.homEquiv_comp_grassmannianSuccIso_hom

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

27.15 Relative Proj via glueing to 27.22 Grassmannians

Section27.15 Relative Proj via glueing#

Tag 01NN, a situation

Tag 01NO, a lemma

Tag 01NP, a lemma

Tag 01NQ, a lemma

Tag 01NR, a lemma

Sources

Section27.16 Relative Proj as a functor#

Tag 01NS, the section

Tag 01NT, a lemma

Tag 01NU, a lemma

Tag 01NV, a lemma

Tag 01NW, a lemma

Tag 01NX, an equation

Tag 01NY, a lemma

Tag 01NZ, a lemma

Tag 01O0, a definition

Tag 01O1, a lemma

Tag 01O2, a lemma

Tag 01O3, a lemma

Tag 01O4, a lemma

Sources

Section27.17 Quasi-coherent sheaves on relative Proj#

Tag 01O6, an equation

Tag 01O7, a lemma

Sources

Section27.18 Functoriality of relative Proj#

Tag 07ZG, a lemma

Tag 07ZH, a lemma

Tag 07ZI, a lemma

Tag 07ZJ, a lemma

Tag 07ZK, a lemma

Sources

Section27.19 Invertible sheaves and morphisms into relative Proj#

Tag 01O8, the section

Tag 01O9, a lemma

Sources

Section27.20 Twisting by invertible sheaves and relative Proj#

Tag 02NB, the section

Tag 02NC, a lemma

Sources

Section27.21 Projective bundles#

Tag 01OB, a definition

Tag 0FCY, an example

Tag 01OC, an example

Tag 01OD, a lemma

Tag 01OE, a lemma

Sources

Section27.22 Grassmannians#

Tag 089S, an equation

Tag 089T, a lemma

Tag 089U, a definition

Tag 089V, a lemma

Sources

Section27.15 Relative Proj via glueing #

Section27.16 Relative Proj as a functor #

Section27.17 Quasi-coherent sheaves on relative Proj #

Section27.18 Functoriality of relative Proj #

Section27.19 Invertible sheaves and morphisms into relative Proj #

Section27.20 Twisting by invertible sheaves and relative Proj #

Section27.21 Projective bundles #

Section27.22 Grassmannians #