Graded base change of symmetric algebras

The canonical equivalence S ⊗[R] Sym(M) ≃ Sym(S ⊗[R] M) identifies the scalar extension of every homogeneous piece with the corresponding homogeneous piece over S. Both directions are bundled as graded algebra maps, so the equivalence can be used on projective spectra. This supplies the homogeneous-coordinate comparison needed to construct families of projective linear transformations. No freeness, flatness, or finite generation of the module is required.

The underlying equivalence is TauCeti.SymmetricAlgebra.scalarTensorBialgEquiv; the grading on its source is Mathlib's GradedAlgebra.baseChange.

The image computation follows the image-of-powers argument in TauCeti.exteriorAlgebraEquivBaseChange_map_exteriorPower, and the tensor-product comparison follows TauCeti.exteriorPower.equivBaseChange, using Submodule.baseChange_map and Submodule.baseChange_pow over commutative semirings.

Main declarations

• TauCeti.SymmetricAlgebra.homogeneousSubmoduleEquivBaseChange: symmetric powers commute with scalar extension, in tensor-product form.
• TauCeti.SymmetricAlgebra.homogeneousSubmoduleBaseChangeEquiv: the equivalence between homogeneous submodules of the ambient algebras.
• TauCeti.SymmetricAlgebra.scalarTensorGradedAlgHom and TauCeti.SymmetricAlgebra.scalarTensorGradedAlgHomSymm: the mutually inverse graded maps.
• TensorProduct.scalarTensorBialgEquiv_mem_homogeneousSubmodule_iff and SymmetricAlgebra.scalarTensorBialgEquiv_symm_mem_baseChange_iff: preservation and reflection of homogeneous degree in both directions.
• TauCeti.SymmetricAlgebra.scalarTensorGradedAlgHom_gradedZeroRingHom_comp_algebraMap and its inverse counterpart: the degree-zero comparisons preserve scalars.

Naturality is provided by LinearMap.scalarTensorBialgEquiv_comp_map in TauCeti.Algebra.Bialgebra.SymmetricAlgebra.BaseChange.

@[simp]

theorem TauCeti.SymmetricAlgebra.map_scalarTensorBialgEquiv_baseChange_homogeneousSubmodule {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] (n : ℕ) : Submodule.map scalarTensorBialgEquiv.toAlgEquiv.toLinearMap (Submodule.baseChange S (homogeneousSubmodule R M n)) = homogeneousSubmodule S (TensorProduct R S M) n

The image of the scalar-extended degree-n piece is exactly the degree-n piece of the symmetric algebra on the scalar-extended module.

theorem TauCeti.SymmetricAlgebra.scalarTensorBialgEquiv_mem_homogeneousSubmodule {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] {n : ℕ} {x : TensorProduct R S (SymmetricAlgebra R M)} (hx : x ∈ Submodule.baseChange S (homogeneousSubmodule R M n)) : scalarTensorBialgEquiv x ∈ homogeneousSubmodule S (TensorProduct R S M) n

The base-change equivalence preserves every homogeneous degree.

theorem TauCeti.SymmetricAlgebra.scalarTensorBialgEquiv_symm_mem_baseChange {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] {n : ℕ} {x : SymmetricAlgebra S (TensorProduct R S M)} (hx : x ∈ homogeneousSubmodule S (TensorProduct R S M) n) : scalarTensorBialgEquiv.symm x ∈ Submodule.baseChange S (homogeneousSubmodule R M n)

The inverse base-change equivalence also preserves every homogeneous degree.

@[simp]

theorem TensorProduct.scalarTensorBialgEquiv_mem_homogeneousSubmodule_iff {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] {n : ℕ} (x : TensorProduct R S (SymmetricAlgebra R M)) : TauCeti.SymmetricAlgebra.scalarTensorBialgEquiv x ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule S (TensorProduct R S M) n ↔ x ∈ Submodule.baseChange S (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n)

Membership in a homogeneous piece is preserved and reflected by scalar extension.

noncomputable def TauCeti.SymmetricAlgebra.homogeneousSubmoduleBaseChangeEquiv {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] (n : ℕ) : ↥(Submodule.baseChange S (homogeneousSubmodule R M n)) ≃ₗ[S] ↥(homogeneousSubmodule S (TensorProduct R S M) n)

Scalar extension identifies the degree-n homogeneous pieces as S-modules.

Equations

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

@[simp]

theorem TauCeti.SymmetricAlgebra.coe_homogeneousSubmoduleBaseChangeEquiv_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] (n : ℕ) (x : ↥(Submodule.baseChange S (homogeneousSubmodule R M n))) : ↑((homogeneousSubmoduleBaseChangeEquiv n) x) = scalarTensorBialgEquiv ↑x

The degreewise equivalence is the restriction of the scalar-extension equivalence.

@[simp]

theorem TauCeti.SymmetricAlgebra.coe_homogeneousSubmoduleBaseChangeEquiv_symm_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] (n : ℕ) (x : ↥(homogeneousSubmodule S (TensorProduct R S M) n)) : ↑((homogeneousSubmoduleBaseChangeEquiv n).symm x) = scalarTensorBialgEquiv.symm ↑x

The inverse degreewise equivalence is the restriction of the inverse scalar-extension equivalence.

theorem TauCeti.SymmetricAlgebra.homogeneousSubmodule_baseChange_subtype_injective {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] (n : ℕ) : Function.Injective ⇑(LinearMap.baseChange S (homogeneousSubmodule R M n).subtype)

Scalar extension of the inclusion of a homogeneous piece remains injective.

noncomputable def TauCeti.SymmetricAlgebra.homogeneousSubmoduleEquivBaseChange {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] (n : ℕ) : ↥(homogeneousSubmodule S (TensorProduct R S M) n) ≃ₗ[S] TensorProduct R S ↥(homogeneousSubmodule R M n)

Symmetric powers commute with scalar extension, without a flatness assumption.

Equations

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

@[simp]

theorem TauCeti.SymmetricAlgebra.subtype_baseChange_homogeneousSubmoduleEquivBaseChange {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] (n : ℕ) (x : ↥(homogeneousSubmodule S (TensorProduct R S M) n)) : (LinearMap.baseChange S (homogeneousSubmodule R M n).subtype) ((homogeneousSubmoduleEquivBaseChange n) x) = scalarTensorBialgEquiv.symm ↑x

The tensor-product comparison agrees with the inverse ambient comparison after inclusion.

@[simp]

theorem TauCeti.SymmetricAlgebra.coe_homogeneousSubmoduleEquivBaseChange_symm_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] (n : ℕ) (x : TensorProduct R S ↥(homogeneousSubmodule R M n)) : ↑((homogeneousSubmoduleEquivBaseChange n).symm x) = scalarTensorBialgEquiv ((LinearMap.baseChange S (homogeneousSubmodule R M n).subtype) x)

The inverse tensor-product comparison agrees with the forward ambient comparison.

noncomputable def TauCeti.SymmetricAlgebra.scalarTensorGradedAlgHom {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] : (fun (n : ℕ) => Submodule.baseChange S (homogeneousSubmodule R M n)) →ₐᵍ[S] homogeneousSubmodule S (TensorProduct R S M)

The canonical scalar-extension equivalence, bundled as a graded algebra map.

Equations

• TauCeti.SymmetricAlgebra.scalarTensorGradedAlgHom = { toAlgHom := ↑TauCeti.SymmetricAlgebra.scalarTensorBialgEquiv.toAlgEquiv, map_mem := ⋯ }

noncomputable def TauCeti.SymmetricAlgebra.scalarTensorGradedAlgHomSymm {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] : homogeneousSubmodule S (TensorProduct R S M) →ₐᵍ[S] fun (n : ℕ) => Submodule.baseChange S (homogeneousSubmodule R M n)

The inverse scalar-extension equivalence, bundled as a graded algebra map.

Equations

• TauCeti.SymmetricAlgebra.scalarTensorGradedAlgHomSymm = { toAlgHom := ↑TauCeti.SymmetricAlgebra.scalarTensorBialgEquiv.symm.toAlgEquiv, map_mem := ⋯ }

@[simp]

theorem TensorProduct.scalarTensorGradedAlgHom_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] (x : TensorProduct R S (SymmetricAlgebra R M)) : TauCeti.SymmetricAlgebra.scalarTensorGradedAlgHom x = TauCeti.SymmetricAlgebra.scalarTensorBialgEquiv x

The forward graded map is the existing scalar-extension equivalence.

@[simp]

theorem SymmetricAlgebra.scalarTensorGradedAlgHomSymm_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] (x : SymmetricAlgebra S (TensorProduct R S M)) : TauCeti.SymmetricAlgebra.scalarTensorGradedAlgHomSymm x = TauCeti.SymmetricAlgebra.scalarTensorBialgEquiv.symm x

The inverse graded map is the inverse scalar-extension equivalence.

theorem TauCeti.SymmetricAlgebra.scalarTensorGradedAlgHom_rightInverse {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] : Function.RightInverse ⇑scalarTensorGradedAlgHomSymm ⇑scalarTensorGradedAlgHom

The inverse graded map is a right inverse of the forward graded map.

theorem TauCeti.SymmetricAlgebra.scalarTensorGradedAlgHom_leftInverse {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] : Function.LeftInverse ⇑scalarTensorGradedAlgHomSymm ⇑scalarTensorGradedAlgHom

The inverse graded map is a left inverse of the forward graded map.

@[simp]

theorem TauCeti.SymmetricAlgebra.scalarTensorGradedAlgHom_gradedZeroRingHom_algebraMap {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] (s : S) : scalarTensorGradedAlgHom.toGradedRingHom.gradedZeroRingHom ((algebraMap S ↥(Submodule.baseChange S (homogeneousSubmodule R M 0))) s) = (algebraMap S ↥(homogeneousSubmodule S (TensorProduct R S M) 0)) s

On degree zero, the forward comparison preserves each scalar from S.

@[simp]

theorem TauCeti.SymmetricAlgebra.scalarTensorGradedAlgHomSymm_gradedZeroRingHom_algebraMap {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] (s : S) : scalarTensorGradedAlgHomSymm.toGradedRingHom.gradedZeroRingHom ((algebraMap S ↥(homogeneousSubmodule S (TensorProduct R S M) 0)) s) = (algebraMap S ↥(Submodule.baseChange S (homogeneousSubmodule R M 0))) s

On degree zero, the inverse comparison preserves each scalar from S.

theorem TauCeti.SymmetricAlgebra.scalarTensorGradedAlgHom_gradedZeroRingHom_comp_algebraMap {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] : scalarTensorGradedAlgHom.toGradedRingHom.gradedZeroRingHom.comp (algebraMap S ↥(Submodule.baseChange S (homogeneousSubmodule R M 0))) = algebraMap S ↥(homogeneousSubmodule S (TensorProduct R S M) 0)

On degree zero, the forward comparison preserves the scalar map from S.

theorem TauCeti.SymmetricAlgebra.scalarTensorGradedAlgHomSymm_gradedZeroRingHom_comp_algebraMap {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] : scalarTensorGradedAlgHomSymm.toGradedRingHom.gradedZeroRingHom.comp (algebraMap S ↥(homogeneousSubmodule S (TensorProduct R S M) 0)) = algebraMap S ↥(Submodule.baseChange S (homogeneousSubmodule R M 0))

On degree zero, the inverse comparison preserves the scalar map from S.

@[simp]

theorem SymmetricAlgebra.scalarTensorBialgEquiv_symm_mem_baseChange_iff {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] {n : ℕ} (x : SymmetricAlgebra S (TensorProduct R S M)) : TauCeti.SymmetricAlgebra.scalarTensorBialgEquiv.symm x ∈ Submodule.baseChange S (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n) ↔ x ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule S (TensorProduct R S M) n

The inverse comparison preserves and reflects homogeneous degree as well.