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

glAction_range_eq_centralizer_symAction

Submitter: Kim Morrison.

Notes: The other direction of Schur-Weyl duality: the subalgebra of End(V^⊗k) generated by the diagonal GL(V) action equals the centralizer of the subalgebra generated by the S_k action.

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

Informal solution: By polarization over R with k! invertible, the subalgebra generated by {g^⊗k : g ∈ GL(V)} is precisely the image of Sym^k(End V), i.e., the endomorphisms of V^⊗k fixed by the S_k-action on tensor factors of End V. An endomorphism of V^⊗k fixed by this action is exactly one commuting with the S_k action on V^⊗k.

theorem declaration uses `sorry`glAction_range_eq_centralizer_symAction {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.glAction R M k)) =
      Subalgebra.centralizer R (Set.range (LeanEval.RepresentationTheory.symAction 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 ⇑(glAction R M k)) = Subalgebra.centralizer R (Set.range ⇑(symAction R M k))
  sorryAll goals completed! 🐙

Solved by

Not yet solved.