Graded functoriality of symmetric algebras

A linear map induces a degree-preserving map of symmetric algebras. The bundled graded map allows linear equivalences to act on the projective spectrum of the symmetric algebra. The construction uses SymmetricAlgebra.map and the grading by powers of the generator range.

theorem SymmetricAlgebra.map_mem_homogeneousSubmodule (R : Type u) [CommSemiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) {n : ℕ} {a : SymmetricAlgebra R M} (ha : a ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n) : (map R f) a ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R N n

A symmetric-algebra map preserves each homogeneous degree.

noncomputable def SymmetricAlgebra.gradedMap (R : Type u) [CommSemiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) : TauCeti.SymmetricAlgebra.homogeneousSubmodule R M →+*ᵍ TauCeti.SymmetricAlgebra.homogeneousSubmodule R N

The degree-preserving ring map of symmetric algebras induced by a linear map.

Equations

• SymmetricAlgebra.gradedMap R f = { toRingHom := (SymmetricAlgebra.map R f).toRingHom, map_mem := ⋯ }

@[simp]

theorem SymmetricAlgebra.gradedMap_toRingHom (R : Type u) [CommSemiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) : ↑(gradedMap R f) = (map R f).toRingHom

The underlying ring homomorphism is the ordinary symmetric-algebra map.

@[simp]

theorem SymmetricAlgebra.gradedMap_apply (R : Type u) [CommSemiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (a : SymmetricAlgebra R M) : (gradedMap R f) a = (map R f) a

The graded map agrees with the symmetric-algebra map on every element.

@[simp]

theorem SymmetricAlgebra.gradedMap_id (R : Type u) [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] : gradedMap R LinearMap.id = GradedRingHom.id (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M)

The identity linear map induces the identity graded map.

@[simp]

theorem SymmetricAlgebra.gradedMap_comp (R : Type u) [CommSemiring R] {M : Type v} {N : Type w} {P : Type x} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) : (gradedMap R g).comp (gradedMap R f) = gradedMap R (g ∘ₗ f)

Composition of linear maps induces composition of graded symmetric-algebra maps.

@[simp]

theorem SymmetricAlgebra.gradedMap_gradedZeroRingHom (R : Type u) [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M) : (gradedMap R f).gradedZeroRingHom = RingHom.id ↥(TauCeti.SymmetricAlgebra.homogeneousSubmodule R M 0)

Every linear endomorphism fixes the degree-zero part of its symmetric algebra.