Divided-difference operators on a symmetric algebra

Let σ be a linear endomorphism of a module M over a commutative ring R, and let ℓ ∈ M be such that m - σ m is a multiple of ℓ for every m ∈ M. Then for every p in the symmetric algebra Sym M, the difference p - σ p is divisible by ℓ, where σ acts on Sym M by the induced algebra endomorphism SymmetricAlgebra.map R σ. When ℓ is a nonzerodivisor of Sym M the quotient is unique, which defines the divided-difference operator δ p = (p - σ p) / ℓ.

The typical example is a pseudoreflection s of a vector space V acting on the polynomial functions Sym(V*), with ℓ a linear form cutting out the hyperplane fixed by s. The operator δ is the basic tool of the proof that the invariants of a finite group generated by pseudoreflections form a polynomial algebra.

The operator δ is R-linear and satisfies ℓ * δ p = p - σ p, so that 1 - σ = m_ℓ ∘ δ as operators on Sym M. It lowers degrees by one, it vanishes exactly on the elements fixed by σ, it satisfies the twisted Leibniz rule δ (p * q) = δ p * q + σ p * δ q, and consequently it is linear over the σ-fixed elements.

Main definitions

• SymmetricAlgebra.dividedDifference: the divided-difference operator p ↦ (p - σ p) / ℓ.

Main results

• SymmetricAlgebra.ι_dvd_sub_map: ℓ divides p - σ p for every p ∈ Sym M.
• SymmetricAlgebra.ι_mul_dividedDifference and SymmetricAlgebra.mulLeft_comp_dividedDifference: the operator identity 1 - σ = m_ℓ ∘ δ.
• SymmetricAlgebra.dividedDifference_eq_zero_iff: δ p = 0 exactly when σ p = p.
• SymmetricAlgebra.dividedDifference_mul: the twisted Leibniz rule.
• SymmetricAlgebra.dividedDifference_mul_of_map_eq: δ is linear over σ-fixed elements.
• SymmetricAlgebra.dividedDifference_mem_homogeneousSubmodule: δ lowers degrees by one.

References

• R. Kane, Reflection Groups and Invariant Theory, CMS Books in Mathematics, Springer (2001), §§ 17–18.
• L. Smith, Polynomial Invariants of Finite Groups, A K Peters (1995), § 7.2.

theorem SymmetricAlgebra.ι_dvd_sub_map {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {σ : M →ₗ[R] M} {ℓ : M} (hσ : ∀ (m : M), m - σ m ∈ R ∙ ℓ) (p : SymmetricAlgebra R M) : (ι R M) ℓ ∣ p - (map R σ) p

If m - σ m is a multiple of ℓ for every m ∈ M, then ℓ divides p - σ p for every p in the symmetric algebra, where σ acts on Sym M by SymmetricAlgebra.map.

theorem SymmetricAlgebra.isLeftRegular_ι {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {ℓ : M} [IsDomain R] [Module.Free R M] (hℓ : ℓ ≠ 0) : IsLeftRegular ((ι R M) ℓ)

A nonzero element of a free module over a domain is a nonzerodivisor in the symmetric algebra.

noncomputable def SymmetricAlgebra.dividedDifference {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (σ : M →ₗ[R] M) (ℓ : M) (hσ : ∀ (m : M), m - σ m ∈ R ∙ ℓ) (hℓ : IsLeftRegular ((ι R M) ℓ)) : SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M

The divided-difference operator p ↦ (p - σ p) / ℓ on the symmetric algebra, for a linear endomorphism σ of M such that m - σ m is a multiple of ℓ for every m, and an element ℓ that is a nonzerodivisor in Sym M. It is characterized by ι ℓ * dividedDifference σ ℓ hσ hℓ p = p - σ p (SymmetricAlgebra.dividedDifference_eq_iff).

@[simp]

theorem SymmetricAlgebra.ι_mul_dividedDifference {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {σ : M →ₗ[R] M} {ℓ : M} {hσ : ∀ (m : M), m - σ m ∈ R ∙ ℓ} {hℓ : IsLeftRegular ((ι R M) ℓ)} (p : SymmetricAlgebra R M) : (ι R M) ℓ * (dividedDifference σ ℓ hσ hℓ) p = p - (map R σ) p

The defining identity of the divided-difference operator: ℓ * δ p = p - σ p.

theorem SymmetricAlgebra.dividedDifference_eq_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {σ : M →ₗ[R] M} {ℓ : M} {hσ : ∀ (m : M), m - σ m ∈ R ∙ ℓ} {hℓ : IsLeftRegular ((ι R M) ℓ)} {p q : SymmetricAlgebra R M} : (dividedDifference σ ℓ hσ hℓ) p = q ↔ (ι R M) ℓ * q = p - (map R σ) p

The divided difference of p is the unique q with ℓ * q = p - σ p.

theorem SymmetricAlgebra.mulLeft_comp_dividedDifference {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {σ : M →ₗ[R] M} {ℓ : M} {hσ : ∀ (m : M), m - σ m ∈ R ∙ ℓ} {hℓ : IsLeftRegular ((ι R M) ℓ)} : LinearMap.mulLeft R ((ι R M) ℓ) ∘ₗ dividedDifference σ ℓ hσ hℓ = LinearMap.id - (map R σ).toLinearMap

The operator identity 1 - σ = m_ℓ ∘ δ on the symmetric algebra.

@[simp]

theorem SymmetricAlgebra.dividedDifference_eq_zero_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {σ : M →ₗ[R] M} {ℓ : M} {hσ : ∀ (m : M), m - σ m ∈ R ∙ ℓ} {hℓ : IsLeftRegular ((ι R M) ℓ)} {p : SymmetricAlgebra R M} : (dividedDifference σ ℓ hσ hℓ) p = 0 ↔ (map R σ) p = p

The divided difference of p vanishes exactly when σ fixes p.

@[simp]

theorem SymmetricAlgebra.dividedDifference_algebraMap {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {σ : M →ₗ[R] M} {ℓ : M} {hσ : ∀ (m : M), m - σ m ∈ R ∙ ℓ} {hℓ : IsLeftRegular ((ι R M) ℓ)} (r : R) : (dividedDifference σ ℓ hσ hℓ) ((algebraMap R (SymmetricAlgebra R M)) r) = 0

The divided difference of a scalar vanishes.

theorem SymmetricAlgebra.dividedDifference_ι {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {σ : M →ₗ[R] M} {ℓ : M} {hσ : ∀ (m : M), m - σ m ∈ R ∙ ℓ} {hℓ : IsLeftRegular ((ι R M) ℓ)} {m : M} {c : R} (hc : m - σ m = c • ℓ) : (dividedDifference σ ℓ hσ hℓ) ((ι R M) m) = (algebraMap R (SymmetricAlgebra R M)) c

On a generator ι m, the divided difference is the scalar c with m - σ m = c • ℓ.

theorem SymmetricAlgebra.dividedDifference_mul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {σ : M →ₗ[R] M} {ℓ : M} {hσ : ∀ (m : M), m - σ m ∈ R ∙ ℓ} {hℓ : IsLeftRegular ((ι R M) ℓ)} (p q : SymmetricAlgebra R M) : (dividedDifference σ ℓ hσ hℓ) (p * q) = (dividedDifference σ ℓ hσ hℓ) p * q + (map R σ) p * (dividedDifference σ ℓ hσ hℓ) q

The twisted Leibniz rule δ (p * q) = δ p * q + σ p * δ q.

theorem SymmetricAlgebra.dividedDifference_mul_of_map_eq {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {σ : M →ₗ[R] M} {ℓ : M} {hσ : ∀ (m : M), m - σ m ∈ R ∙ ℓ} {hℓ : IsLeftRegular ((ι R M) ℓ)} {a : SymmetricAlgebra R M} (ha : (map R σ) a = a) (p : SymmetricAlgebra R M) : (dividedDifference σ ℓ hσ hℓ) (a * p) = a * (dividedDifference σ ℓ hσ hℓ) p

The divided-difference operator is linear over the elements fixed by σ.

theorem SymmetricAlgebra.dividedDifference_mem_homogeneousSubmodule {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {σ : M →ₗ[R] M} {ℓ : M} {hσ : ∀ (m : M), m - σ m ∈ R ∙ ℓ} {hℓ : IsLeftRegular ((ι R M) ℓ)} {n : ℕ} {p : SymmetricAlgebra R M} (hp : p ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M (n + 1)) : (dividedDifference σ ℓ hσ hℓ) p ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n

The divided-difference operator lowers degrees by one: it sends the degree-n + 1 part of Sym M to the degree-n part.