Symmetric powers and restriction of scalars

Let f : S →+* R be a morphism of commutative rings and M an R-module. Restriction of scalars has a natural symmetric-power comparison Symⁿ_S M ⟶ Symⁿ_R M, sending a product m₁ ⋯ mₙ of elements of M over S to the same product over R. It is the restriction to degree-n parts of the ring homomorphism of symmetric algebras SymmetricAlgebra.mapₛₗ induced by the identity of M, viewed as an f-semilinear map. It is an isomorphism when f is bijective, although this need not hold for a general ring map. This supplies the sectionwise maps for symmetric powers of pushforwards of module presheaves, in the same way as TauCeti.ModuleCat.restrictScalarsExteriorPowerComparison does for exterior powers.

noncomputable def TauCeti.ModuleCat.restrictScalarsSymmetricPowerComparison {S : Type u} {R : Type v} [CommRing S] [CommRing R] (f : S →+* R) (n : ℕ) : (ModuleCat.restrictScalars f).comp (ModuleCat.symmetricPower.functor S n) ⟶ (ModuleCat.symmetricPower.functor R n).comp (ModuleCat.restrictScalars f)

Restriction of scalars carries the natural symmetric-power comparison, changing the coefficient ring of a product of elements without changing its factors.

@[simp]

theorem TauCeti.ModuleCat.coe_restrictScalarsSymmetricPowerComparison_app_apply {S : Type u} {R : Type v} [CommRing S] [CommRing R] (f : S →+* R) (n : ℕ) (M : ModuleCat R) (x : ↑(((ModuleCat.restrictScalars f).obj M).symmetricPower n)) : ↑((CategoryTheory.ConcreteCategory.hom ((restrictScalarsSymmetricPowerComparison f n).app M)) x) = (SymmetricAlgebra.mapₛₗ ((ModuleCat.semilinearMapAddEquiv f ((ModuleCat.restrictScalars f).obj M) M).symm (CategoryTheory.CategoryStruct.id ((ModuleCat.restrictScalars f).obj M)))) ↑x

The restriction-of-scalars comparison is computed in the symmetric algebra by the ring homomorphism induced by the identity of M, viewed as an f-semilinear map; it sends the generator of m over S to the generator of m over R (SymmetricAlgebra.mapₛₗ_ι).

theorem TauCeti.ModuleCat.isIso_restrictScalarsSymmetricPowerComparison_app_of_bijective {S : Type u} {R : Type v} [CommRing S] [CommRing R] (f : S →+* R) (hf : Function.Bijective ⇑f) (n : ℕ) (M : ModuleCat R) : CategoryTheory.IsIso ((restrictScalarsSymmetricPowerComparison f n).app M)

Restriction along an isomorphism of coefficient rings preserves symmetric powers.