Divided-difference operators of a linear group action

Let ρ be a representation of a group G on a module M, and let g ∈ G and ℓ ∈ M be such that m - ρ g m is a multiple of ℓ for every m. If ℓ is a nonzerodivisor of Sym M, the divided-difference operator δ_g p = (p - g • p) / ℓ of SymmetricAlgebra.dividedDifference is linear not only over the coefficients, but over the whole invariant subalgebra Sym(M)^G, since every invariant is fixed by g. This file bundles it as a Sym(M)^G-linear map. It satisfies the operator identity 1 - g = m_ℓ ∘ δ_g as Sym(M)^G-linear maps, so the same identity holds after applying any additive functor on Sym(M)^G-modules, such as Tor'ₙ(N, -).

The main example is a pseudoreflection. Let ρ be a representation on a vector space V over a field K, and let g fix pointwise a hyperplane ker ℓ, cut out by a nonzero linear form ℓ. Then φ - g • φ is a multiple of ℓ for every linear form φ, where G acts on V* by the contragredient representation Representation.dual (Representation.sub_dual_apply_mem_span_singleton, in TauCeti.RepresentationTheory.Dual). Hence g has a divided-difference operator δ_g f = (f - g • f) / ℓ on the polynomial functions Sym(V*), which is linear over the polynomial invariants Sym(V*)^G, lowers degrees by one, and satisfies the operator identity 1 - g = m_ℓ ∘ δ_g. These operators are the basic tool of the proof that the polynomial invariants of a finite group generated by pseudoreflections form a polynomial algebra.

Main definitions

• Representation.symmetricAlgebraDividedDifference: the divided-difference operator of g, as a linear map over the invariant subalgebra.

Main results

• Representation.map_symmetricAlgebraDividedDifference_comp_map_mulLeft: the operator identity 1 - g = m_ℓ ∘ δ_g after applying an additive functor.
• Representation.iSup_wordKer_symmetricAlgebraDividedDifference_eq_top: the divided-difference operators of any family of elements form a locally nilpotent family of Sym(M)^G-linear maps.

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.

noncomputable def Representation.symmetricAlgebraDividedDifference {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Monoid G] [AddCommGroup M] [Module R M] (ρ : Representation R G M) (g : G) (ℓ : M) (hσ : ∀ (m : M), m - (ρ g) m ∈ R ∙ ℓ) (hℓ : IsLeftRegular ((SymmetricAlgebra.ι R M) ℓ)) : SymmetricAlgebra R M →ₗ[↥ρ.symmetricAlgebraInvariants] SymmetricAlgebra R M

The divided-difference operator p ↦ (p - g • p) / ℓ of g on Sym M, bundled as a linear map over the invariant subalgebra Sym(M)^G. It requires m - ρ g m to be a multiple of ℓ for every m, and ℓ to be a nonzerodivisor in Sym M. Its underlying map is SymmetricAlgebra.dividedDifference (ρ g) ℓ.

@[simp]

theorem Representation.symmetricAlgebraDividedDifference_apply {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Monoid G] [AddCommGroup M] [Module R M] (ρ : Representation R G M) (g : G) (ℓ : M) (hσ : ∀ (m : M), m - (ρ g) m ∈ R ∙ ℓ) (hℓ : IsLeftRegular ((SymmetricAlgebra.ι R M) ℓ)) (p : SymmetricAlgebra R M) : (ρ.symmetricAlgebraDividedDifference g ℓ hσ hℓ) p = (SymmetricAlgebra.dividedDifference (ρ g) ℓ hσ hℓ) p

The bundled divided-difference operator of g is SymmetricAlgebra.dividedDifference.

theorem Representation.iSup_wordKer_symmetricAlgebraDividedDifference_eq_top {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Monoid G] [AddCommGroup M] [Module R M] (ρ : Representation R G M) {ι : Type u_4} (s : ι → G) (ℓ : ι → M) (hσ : ∀ (i : ι) (m : M), m - (ρ (s i)) m ∈ R ∙ ℓ i) (hℓ : ∀ (i : ι), IsLeftRegular ((SymmetricAlgebra.ι R M) (ℓ i))) : ⨆ (d : ℕ), Module.End.wordKer (fun (i : ι) => ρ.symmetricAlgebraDividedDifference (s i) (ℓ i) ⋯ ⋯) d = ⊤

Divided differences are locally nilpotent. Let δ_(s i) be the divided-difference operators of a family s i of elements of G. Every element of Sym M is killed by all sufficiently long composites of the operators δ_(s i): one whose homogeneous components have degree at most d is killed by every composite of d + 1 of them, since each δ_(s i) lowers degrees by one and kills the scalars.

theorem Representation.map_symmetricAlgebraDividedDifference_comp_map_mulLeft {R : Type u} {M : Type v} {G : Type u_1} [CommRing R] [Monoid G] [AddCommGroup M] [Module R M] (ρ : Representation R G M) (g : G) (ℓ : M) (hσ : ∀ (m : M), m - (ρ g) m ∈ R ∙ ℓ) (hℓ : IsLeftRegular ((SymmetricAlgebra.ι R M) ℓ)) {D : Type u_2} [CategoryTheory.Category.{v_1, u_2} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor (ModuleCat ↥ρ.symmetricAlgebraInvariants) D) [F.Additive] : CategoryTheory.CategoryStruct.comp (F.map (ModuleCat.ofHom (ρ.symmetricAlgebraDividedDifference g ℓ hσ hℓ))) (F.map (ModuleCat.ofHom (LinearMap.mulLeft (↥ρ.symmetricAlgebraInvariants) ((SymmetricAlgebra.ι R M) ℓ)))) = CategoryTheory.CategoryStruct.id (F.obj ↧(SymmetricAlgebra R M)) - F.map (ModuleCat.ofHom (ρ.symmetricAlgebraOverInvariants g))

The operator identity 1 - g = m_ℓ ∘ δ_g after applying an additive functor. If m - ρ g m is a multiple of ℓ for every m and ℓ is a nonzerodivisor of Sym M, then for every additive functor F from modules over A = Sym(M)^G to a preadditive category, the divided-difference operator δ_g followed by multiplication by ℓ induces 1 - g on F(Sym M).