Extension of scalars and symmetric powers

Symmetric powers commute with extension of scalars along arbitrary homomorphisms of commutative rings. The natural comparison constructed here is induced by the unit of the extension--restriction adjunction on homogeneous symmetric-algebra elements. It is the module calculation used for pullback of symmetric powers of quasicoherent sheaves on affine schemes.

The comparison uses TauCeti.SymmetricAlgebra.homogeneousSubmoduleEquivBaseChange; its categorical packaging follows TauCeti.extendScalarsExteriorPowerNatIso. The identity law uses Mathlib's canonical ModuleCat.extendScalarsId. No flatness or finiteness assumption is needed.

References

• R. Hartshorne, Algebraic Geometry, Chapter II, Exercise 5.16.

noncomputable def RingHom.extendScalarsSymmetricPowerIso {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) (n : ℕ) (M : ModuleCat R) : (ModuleCat.extendScalars f).obj (M.symmetricPower n) ≅ ((ModuleCat.extendScalars f).obj M).symmetricPower n

Symmetric powers commute with extension of scalars along any ring homomorphism.

theorem RingHom.coe_extendScalarsSymmetricPowerIso_hom_apply {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) (n : ℕ) (M : ModuleCat R) (x : ↑((ModuleCat.extendScalars f).obj (M.symmetricPower n))) : ↑((ModuleCat.Hom.hom (f.extendScalarsSymmetricPowerIso n M).hom) x) = TauCeti.SymmetricAlgebra.scalarTensorBialgEquiv ((LinearMap.baseChange S (TauCeti.SymmetricAlgebra.homogeneousSubmodule R (↑M) n).subtype) x)

After inclusion in the symmetric algebra, the comparison is the ambient scalar-extension equivalence on the extended homogeneous piece.

@[simp]

theorem RingHom.coe_extendScalarsSymmetricPowerIso_hom_tmul {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) (n : ℕ) (M : ModuleCat R) (s : S) (x : ↑(M.symmetricPower n)) : ↑((ModuleCat.Hom.hom (f.extendScalarsSymmetricPowerIso n M).hom) (s ⊗ₜ[R] x)) = TauCeti.SymmetricAlgebra.scalarTensorBialgEquiv (s ⊗ₜ[R] ↑x)

On pure tensors the comparison is the ambient symmetric-algebra comparison.

theorem RingHom.coe_extendScalarsSymmetricPowerIso_hom_one_tmul_prod {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) (M : ModuleCat R) (l : List ↑M) (hl : (List.map (⇑(SymmetricAlgebra.ι R ↑M)) l).prod ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R (↑M) l.length) : ↑((ModuleCat.Hom.hom (f.extendScalarsSymmetricPowerIso l.length M).hom) (1 ⊗ₜ[R] ⟨(List.map (⇑(SymmetricAlgebra.ι R ↑M)) l).prod, hl⟩)) = (List.map (fun (m : ↑M) => (SymmetricAlgebra.ι S ↑((ModuleCat.extendScalars f).obj M)) (1 ⊗ₜ[R] m)) l).prod

The comparison sends 1 ⊗ (m₁ ⋯ mₙ) to the product of the generators 1 ⊗ mᵢ.

theorem RingHom.subtype_baseChange_extendScalarsSymmetricPowerIso_inv_apply {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) (n : ℕ) (M : ModuleCat R) (x : ↑(((ModuleCat.extendScalars f).obj M).symmetricPower n)) : (LinearMap.baseChange S (TauCeti.SymmetricAlgebra.homogeneousSubmodule R (↑M) n).subtype) ((ModuleCat.Hom.hom (f.extendScalarsSymmetricPowerIso n M).inv) x) = TauCeti.SymmetricAlgebra.scalarTensorBialgEquiv.symm ↑x

The inverse comparison is the inverse ambient scalar-extension equivalence, after inclusion of the extended homogeneous piece.

theorem RingHom.extendScalarsSymmetricPowerIso_hom_naturality {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) (n : ℕ) {M N : ModuleCat R} (g : M ⟶ N) : CategoryTheory.CategoryStruct.comp ((ModuleCat.extendScalars f).map (ModuleCat.symmetricPower.map g n)) (f.extendScalarsSymmetricPowerIso n N).hom = CategoryTheory.CategoryStruct.comp (f.extendScalarsSymmetricPowerIso n M).hom (ModuleCat.symmetricPower.map ((ModuleCat.extendScalars f).map g) n)

The comparison is natural in the original module.

theorem RingHom.extendScalarsSymmetricPowerIso_hom_naturality_assoc {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) (n : ℕ) {M N : ModuleCat R} (g : M ⟶ N) {Z : ModuleCat S} (h : ((ModuleCat.extendScalars f).obj N).symmetricPower n ⟶ Z) : CategoryTheory.CategoryStruct.comp ((ModuleCat.extendScalars f).map (ModuleCat.symmetricPower.map g n)) (CategoryTheory.CategoryStruct.comp (f.extendScalarsSymmetricPowerIso n N).hom h) = CategoryTheory.CategoryStruct.comp (f.extendScalarsSymmetricPowerIso n M).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.symmetricPower.map ((ModuleCat.extendScalars f).map g) n) h)

The comparison is natural in the original module.

noncomputable def RingHom.extendScalarsSymmetricPowerNatIso {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) (n : ℕ) : (ModuleCat.symmetricPower.functor R n).comp (ModuleCat.extendScalars f) ≅ (ModuleCat.extendScalars f).comp (ModuleCat.symmetricPower.functor S n)

The natural scalar-extension comparison for symmetric powers of arbitrary modules.

@[simp]

theorem RingHom.extendScalarsSymmetricPowerNatIso_hom_app {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) (n : ℕ) (M : ModuleCat R) : (f.extendScalarsSymmetricPowerNatIso n).hom.app M = (f.extendScalarsSymmetricPowerIso n M).hom

The forward components of the natural comparison.

@[simp]

theorem RingHom.extendScalarsSymmetricPowerNatIso_inv_app {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) (n : ℕ) (M : ModuleCat R) : (f.extendScalarsSymmetricPowerNatIso n).inv.app M = (f.extendScalarsSymmetricPowerIso n M).inv

The inverse components of the natural comparison.

theorem RingHom.extendScalarsSymmetricPowerNatIso_id {R : Type u} [CommRing R] (n : ℕ) : CategoryTheory.CategoryStruct.comp ((id R).extendScalarsSymmetricPowerNatIso n).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (ModuleCat.extendScalarsId R).hom (ModuleCat.symmetricPower.functor R n)) (ModuleCat.symmetricPower.functor R n).leftUnitor.hom) = CategoryTheory.CategoryStruct.comp ((ModuleCat.symmetricPower.functor R n).whiskerLeft (ModuleCat.extendScalarsId R).hom) (ModuleCat.symmetricPower.functor R n).rightUnitor.hom

The symmetric-power comparison respects Mathlib's identity comparison for extension of scalars.