Translation of polynomial functions on the dual

Let M be a module over a commutative ring R. An element p of the symmetric algebra SymmetricAlgebra R M is a polynomial function on the dual of M, its value at a linear form g being SymmetricAlgebra.lift g p. Translating the argument by a fixed linear form f, g ↦ p (g + f), is again such a function, and it is induced by an algebra automorphism of the symmetric algebra: the one sending each generator m to m + f m. This file constructs it, SymmetricAlgebra.translation f, and proves its evaluation formula p ↦ (g ↦ p (g + f)) (SymmetricAlgebra.lift_translation), its group laws in f, and its interaction with the degree filtration.

The degree filtration is the word filtration TauCeti.Algebra.wordFiltration of the generator map, whose step n is spanned by the products of at most n generators. A translation sends a generator to itself plus a scalar, so it preserves every step; and on an element of degree at most n it changes nothing in degree n, the difference translation f p - p lying in degree strictly less than n (SymmetricAlgebra.translation_sub_self_mem_wordFiltrationPrevious). That is, a translation is unipotent for the filtration, with identity associated graded map.

For a Cartan subalgebra H of a semisimple Lie algebra, S(H) is the algebra of polynomial functions on the weights, and translation by the Weyl vector ρ is what relates the Harish-Chandra projection to its linear normalization and the dot action of the Weyl group to the linear one.

Main definitions

• SymmetricAlgebra.translation f: the algebra automorphism of SymmetricAlgebra R M sending each generator m to m + f m.

Main results

• SymmetricAlgebra.translation_ι: its value on a generator.
• SymmetricAlgebra.lift_translation: evaluation after translating by f is evaluation at the translated linear form.
• SymmetricAlgebra.translation_zero, SymmetricAlgebra.translation_trans and SymmetricAlgebra.translation_symm: translation is a homomorphism from the additive group of linear forms to the automorphisms.
• SymmetricAlgebra.translation_mem_wordFiltration_iff: translation preserves every step of the degree filtration.
• SymmetricAlgebra.translation_sub_self_mem_wordFiltrationPrevious: on an element of degree at most n it agrees with the identity up to degree strictly less than n.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §23.3, where the translation by ρ of polynomial functions on the weights appears in the Harish-Chandra homomorphism.

noncomputable def SymmetricAlgebra.translation {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] R) : SymmetricAlgebra R M ≃ₐ[R] SymmetricAlgebra R M

Translation by a linear form f: the algebra automorphism of the symmetric algebra sending each generator m to m + f m (SymmetricAlgebra.translation_ι). Reading an element p of SymmetricAlgebra R M as a polynomial function on the dual of M, translation f p is the function g ↦ p (g + f) (SymmetricAlgebra.lift_translation). Its inverse is translation by -f (SymmetricAlgebra.translation_symm).

@[simp]

theorem SymmetricAlgebra.translation_ι {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] R) (m : M) : (translation f) ((ι R M) m) = (ι R M) m + (algebraMap R (SymmetricAlgebra R M)) (f m)

Translation on a generator: translation f sends the generator m to m + f m.

@[simp]

theorem SymmetricAlgebra.lift_translation {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] {A : Type w} [CommSemiring A] [Algebra R A] (g : M →ₗ[R] A) (f : M →ₗ[R] R) (p : SymmetricAlgebra R M) : (lift g) ((translation f) p) = (lift (g + Algebra.linearMap R A ∘ₗ f)) p

Evaluation of a translate: evaluating translation f p at a linear form g is evaluating p at g + f. The linear form g may take values in any commutative R-algebra A, the translation f entering through the structure map R → A.

@[simp]

theorem SymmetricAlgebra.translation_translation {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (f g : M →ₗ[R] R) (p : SymmetricAlgebra R M) : (translation f) ((translation g) p) = (translation (g + f)) p

Translations compose additively: translating by g and then by f is translating by g + f.

@[simp]

theorem SymmetricAlgebra.translation_zero {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] : translation 0 = AlgEquiv.refl

Translation by the zero linear form is the identity.

@[simp]

theorem SymmetricAlgebra.translation_trans {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (f g : M →ₗ[R] R) : (translation f).trans (translation g) = translation (f + g)

The bundled form of SymmetricAlgebra.translation_translation: translating by f and then by g is translating by f + g.

@[simp]

theorem SymmetricAlgebra.translation_symm {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] R) : (translation f).symm = translation (-f)

The inverse of a translation is the translation by the negated linear form.

The degree filtration

@[simp]

theorem SymmetricAlgebra.translation_mem_wordFiltration_iff {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] R) {n : ℕ} {p : SymmetricAlgebra R M} : (translation f) p ∈ TauCeti.Algebra.wordFiltration (ι R M) n ↔ p ∈ TauCeti.Algebra.wordFiltration (ι R M) n

Translation preserves the degree filtration: translation f p has degree at most n exactly when p does.

theorem SymmetricAlgebra.translation_sub_self_mem_wordFiltrationPrevious {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] R) {n : ℕ} {p : SymmetricAlgebra R M} (hp : p ∈ TauCeti.Algebra.wordFiltration (ι R M) n) : (translation f) p - p ∈ TauCeti.Algebra.wordFiltrationPrevious (ι R M) n

A translation is unipotent for the degree filtration: on an element p of degree at most n, translation f p - p has degree strictly less than n. In degree zero this says that a translation fixes the scalars.