Symmetric powers of localized modules

Symmetric powers commute with extension of scalars and hence with localization. Here the comparison applies to an arbitrary map exhibiting scalar extension, rather than only to the tensor-product model. Its characteristic equation identifies it with the map induced by the original module map on homogeneous symmetric-algebra elements. Consequently the induced semilinear map on each homogeneous piece is a localization map.

noncomputable def IsBaseChange.symmetricPowerEquiv {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module A N] [IsScalarTower R A N] {f : M →ₗ[R] N} (h : IsBaseChange A f) (n : ℕ) : TensorProduct R A ↥(TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n) ≃ₗ[A] ↥(TauCeti.SymmetricAlgebra.homogeneousSubmodule A N n)

Scalar extension of a symmetric power along any map exhibiting scalar extension. No flatness or finite-generation assumption is required.

@[simp]

theorem IsBaseChange.coe_symmetricPowerEquiv_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module A N] [IsScalarTower R A N] {f : M →ₗ[R] N} (h : IsBaseChange A f) (n : ℕ) (x : TensorProduct R A ↥(TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n)) : ↑((h.symmetricPowerEquiv n) x) = (SymmetricAlgebra.map A ↑h.equiv) (TauCeti.SymmetricAlgebra.scalarTensorBialgEquiv ((LinearMap.baseChange A (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n).subtype) x))

The symmetric-power comparison is the ambient scalar-extension comparison followed by the symmetric-algebra map of the scalar-extension equivalence.

theorem IsBaseChange.coe_symmetricPowerEquiv_tmul {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module A N] [IsScalarTower R A N] {f : M →ₗ[R] N} (h : IsBaseChange A f) (n : ℕ) (f' : M →ₛₗ[algebraMap R A] N) (hf : ∀ (m : M), f' m = f m) (a : A) (x : ↥(TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n)) : ↑((h.symmetricPowerEquiv n) (a ⊗ₜ[R] x)) = a • (SymmetricAlgebra.mapₛₗ f') ↑x

On pure tensors the comparison is the scaled map of symmetric algebras induced by the original module map. The semilinear presentation and its agreement with the linear map are explicit arguments; the equation also applies to degree zero.

theorem IsBaseChange.symmetricPowerEquiv_naturality {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module A N] [IsScalarTower R A N] {f : M →ₗ[R] N} {M' : Type u_5} {N' : Type u_6} [AddCommMonoid M'] [Module R M'] [AddCommMonoid N'] [Module R N'] [Module A N'] [IsScalarTower R A N'] {f' : M' →ₗ[R] N'} (h : IsBaseChange A f) (h' : IsBaseChange A f') (n : ℕ) (g : M →ₗ[R] M') (g' : N →ₗ[A] N') (comm : ↑R g' ∘ₗ f = f' ∘ₗ g) : TauCeti.SymmetricAlgebra.homogeneousSubmoduleMapₛₗ g' n ∘ₗ ↑(h.symmetricPowerEquiv n) = ↑(h'.symmetricPowerEquiv n) ∘ₗ LinearMap.baseChange A (TauCeti.SymmetricAlgebra.homogeneousSubmoduleMapₛₗ g n)

The symmetric-power scalar-extension comparison is natural in commuting maps of the original and extended modules.

theorem LinearMap.isLocalizedModule_symmetricPower {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module A N] [IsScalarTower R A N] (f : M →ₗ[R] N) {S : Submonoid R} [IsLocalization S A] [IsLocalizedModule S f] (n : ℕ) [symR : Module R ↥(TauCeti.SymmetricAlgebra.homogeneousSubmodule A N n)] [symTower : IsScalarTower R A ↥(TauCeti.SymmetricAlgebra.homogeneousSubmodule A N n)] (f' : M →ₛₗ[algebraMap R A] N) (hf : ∀ (m : M), f' m = f m) (g : ↥(TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n) →ₗ[R] ↥(TauCeti.SymmetricAlgebra.homogeneousSubmodule A N n)) (hg : ∀ (x : ↥(TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n)), ↑(g x) = (SymmetricAlgebra.mapₛₗ f') ↑x) : IsLocalizedModule S g

A map on homogeneous symmetric-algebra pieces agreeing with the map induced by a localization of modules is itself a localization. The target scalar action is retained explicitly so that this applies to restriction-of-scalars module presentations.