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

• @jzuiddam with Claude Opus 4.7 (1M context) on May 7, 2026

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 8, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on May 13, 2026 (proof)

• @GanjinZero with Seed Prover (ByteDance) on May 20, 2026