Schur-Weyl duality: S_k image equals centralizer of GL(V) image

symAction_range_eq_centralizer_glAction

Submitter: Kim Morrison.

Notes: One direction of Schur-Weyl duality: the subalgebra of End(V^⊗k) generated by the S_k action (permuting factors) equals the centralizer of the subalgebra generated by the diagonal GL(V) action. Hypothesis `Invertible (k! : R)` over a field is exactly the Maschke condition for R[S_k].

Source: H. Weyl, The Classical Groups, 1939; I. Schur, Über die rationalen Darstellungen der allgemeinen linearen Gruppe, 1927.

Informal solution: Classical proof: any T ∈ End(V^⊗k) commuting with GL(V) acts the same way on tensors related by g^⊗k for every g, and by polarization (which uses k! invertible) the subalgebra {g^⊗k : g ∈ GL(V)} linearly spans the image of Sym^k(End V) in End(V^⊗k). Together with the semisimplicity of R[S_k] (Maschke, from the same k! hypothesis) and double commutant for finite-dimensional semisimple algebras, T lies in the R-subalgebra generated by the S_k action.

theorem declaration uses `sorry`symAction_range_eq_centralizer_glAction {R : Type*} [Field R]
    {M : Type*} [AddCommGroup M] [Module R M] [FiniteDimensional R M]
    {k : ℕ} [Invertible (k.factorial : R)] :
    Algebra.adjoin R (Set.range (LeanEval.RepresentationTheory.symAction R M k)) =
      Subalgebra.centralizer R (Set.range (LeanEval.RepresentationTheory.glAction R M k)) := byR:Type u_1inst✝⁴:Field RM:Type u_2inst✝³:AddCommGroup Minst✝²:Module R Minst✝¹:FiniteDimensional R Mk:ℕinst✝:Invertible ↑k.factorial⊢ Algebra.adjoin R (Set.range ⇑(symAction R M k)) = Subalgebra.centralizer R (Set.range ⇑(glAction R M k))
  sorryAll goals completed! 🐙

Solved by

Not yet solved.