Projective spectra of scalar-extended symmetric algebras

The graded equivalence between S ⊗[R] Sym(M) and Sym(S ⊗[R] M) induces an isomorphism of their projective spectra, contravariantly. This compares the two graded presentations and is an input to constructing algebraic families of projective linear transformations.

The convention is Proj(Sym M): M is the module of linear homogeneous coordinates. For the projective space of lines in a finite locally free module V, take M = V∨. No finite generation or freeness is needed for the comparison of projective spectra.

One side is Proj of the scalar-extended graded ring. Identification with the scheme fiber product over Spec R is a separate assertion, not part of this isomorphism. The construction combines Proj.mapIso with the graded symmetric-algebra base-change maps. The comparison commutes with Proj.toSpecZero, and the degree-zero comparison preserves the scalar copy of S in both presentations.

References

• J. S. Milne, Algebraic Groups (2017), §§7.d–7.f, projective actions and homogeneous spaces.

noncomputable def AlgebraicGeometry.Proj.symmetricAlgebraScalarTensorIso (R S M : Type u) [CommRing R] [CommRing S] [Algebra R S] [AddCommMonoid M] [Module R M] : Proj (TauCeti.SymmetricAlgebra.homogeneousSubmodule S (TensorProduct R S M)) ≅ Proj fun (n : ℕ) => Submodule.baseChange S (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n)

The canonical graded symmetric-algebra base-change equivalence induces an isomorphism of projective spectra. The tensor-product grading places S in degree zero.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Proj.symmetricAlgebraScalarTensorIso_hom (R S M : Type u) [CommRing R] [CommRing S] [Algebra R S] [AddCommMonoid M] [Module R M] : (symmetricAlgebraScalarTensorIso R S M).hom = map TauCeti.SymmetricAlgebra.scalarTensorGradedAlgHom.toGradedRingHom ⋯

The forward projective morphism pulls back coordinates by the scalar-extension equivalence.

@[simp]

theorem AlgebraicGeometry.Proj.symmetricAlgebraScalarTensorIso_inv (R S M : Type u) [CommRing R] [CommRing S] [Algebra R S] [AddCommMonoid M] [Module R M] : (symmetricAlgebraScalarTensorIso R S M).inv = map TauCeti.SymmetricAlgebra.scalarTensorGradedAlgHomSymm.toGradedRingHom ⋯

The inverse projective morphism pulls back coordinates by the inverse scalar-extension equivalence.

@[simp]

theorem AlgebraicGeometry.Proj.symmetricAlgebraScalarTensorIso_hom_toSpecZero (R S M : Type u) [CommRing R] [CommRing S] [Algebra R S] [AddCommMonoid M] [Module R M] : CategoryTheory.CategoryStruct.comp (symmetricAlgebraScalarTensorIso R S M).hom (toSpecZero fun (n : ℕ) => Submodule.baseChange S (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n)) = CategoryTheory.CategoryStruct.comp (toSpecZero (TauCeti.SymmetricAlgebra.homogeneousSubmodule S (TensorProduct R S M))) (Spec.map (CommRingCat.ofHom TauCeti.SymmetricAlgebra.scalarTensorGradedAlgHom.toGradedRingHom.gradedZeroRingHom))

The projective comparison lies over the induced comparison of degree-zero rings.

@[simp]

theorem AlgebraicGeometry.Proj.symmetricAlgebraScalarTensorIso_hom_toSpecZero_assoc (R S M : Type u) [CommRing R] [CommRing S] [Algebra R S] [AddCommMonoid M] [Module R M] {Z : Scheme} (h : Spec ↧↥(Submodule.baseChange S (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M 0)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (symmetricAlgebraScalarTensorIso R S M).hom (CategoryTheory.CategoryStruct.comp (toSpecZero fun (n : ℕ) => Submodule.baseChange S (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n)) h) = CategoryTheory.CategoryStruct.comp (toSpecZero (TauCeti.SymmetricAlgebra.homogeneousSubmodule S (TensorProduct R S M))) (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom TauCeti.SymmetricAlgebra.scalarTensorGradedAlgHom.toGradedRingHom.gradedZeroRingHom)) h)

The projective comparison lies over the induced comparison of degree-zero rings.