Schur–Weyl duality

DefinitionPermutation action of the symmetric group on tensor powers#✓fully proved

Let \(R\) be a commutative semiring, \(M\) an \(R\)-module and \(k\) a natural number. The symmetric group \(S_k\) of permutations of \(\{1, \dots, k\}\) acts on the \(k\)-th tensor power \(M^{\otimes k}\) by permuting tensor factors: this is the monoid homomorphism from \(S_k\) to the \(R\)-linear endomorphisms of \(M^{\otimes k}\) that sends \(\sigma\) to the map \(v_1 \otimes \cdots \otimes v_k \mapsto v_{\sigma^{-1}(1)} \otimes \cdots \otimes v_{\sigma^{-1}(k)}\).

def symAction (R M : Type*) [CommSemiring R] [AddCommMonoid M] [Module R M] (k : ℕ) :
    Equiv.Perm (Fin k) →* Module.End R (⨂[R]^k M) where
  toFun σ := (PiTensorProduct.reindex R (fun _ : Fin k => M) σ).toLinearMap
  map_one' := by
    ext x
    simp only [LinearEquiv.coe_coe, LinearMap.coe_compMultilinearMap, Function.comp_apply,
      PiTensorProduct.reindex_tprod, Module.End.one_apply]
    rfl
  map_mul' σ τ := by
    ext x
    simp only [Module.End.mul_apply, LinearEquiv.coe_coe, LinearMap.coe_compMultilinearMap,
      Function.comp_apply, PiTensorProduct.reindex_tprod]
    rfl

Used by 2

Used bySchur–Weyl duality: the general linear side · Schur–Weyl duality: the symmetric group side

DefinitionDiagonal action of the general linear group on tensor powers#✓fully proved

Let \(R\) be a commutative semiring, \(M\) an \(R\)-module and \(k\) a natural number. Write \(\mathrm{GL}(M)\) for the group of invertible \(R\)-linear endomorphisms of \(M\). The diagonal action of \(\mathrm{GL}(M)\) on the \(k\)-th tensor power \(M^{\otimes k}\) is the monoid homomorphism from \(\mathrm{GL}(M)\) to the \(R\)-linear endomorphisms of \(M^{\otimes k}\) that sends \(g\) to \(g^{\otimes k}\), so that \(g \cdot (v_1 \otimes \cdots \otimes v_k) = g v_1 \otimes \cdots \otimes g v_k\).

def glAction (R M : Type*) [CommSemiring R] [AddCommMonoid M] [Module R M] (k : ℕ) :
    (M →ₗ[R] M)ˣ →* Module.End R (⨂[R]^k M) where
  toFun g := PiTensorProduct.map (fun _ : Fin k => (g : M →ₗ[R] M))
  map_one' := by ext x; simp
  map_mul' g h := by ext x; simp

Used by 2

Used bySchur–Weyl duality: the general linear side · Schur–Weyl duality: the symmetric group side

TheoremSchur–Weyl duality: the symmetric group side#●ready to prove

Let \(R\) be a field, \(M\) a finite-dimensional vector space over \(R\), and \(k\) a natural number such that \(k!\) is invertible in \(R\). In the algebra of \(R\)-linear endomorphisms of the tensor power \(M^{\otimes k}\), the subalgebra generated by the image of the action of the symmetric group \(S_k\) by permuting tensor factors equals the centralizer of the image of the diagonal action \(g \mapsto g^{\otimes k}\) of \(\mathrm{GL}(M)\).

public theorem_wanted 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 (symAction R M k)) =
      Subalgebra.centralizer R (Set.range (glAction R M k))

Sources

• H. Weyl, The Classical Groups, 1939; I. Schur, Über die rationalen Darstellungen der allgemeinen linearen Gruppe, 1927. Problem symAction_range_eq_centralizer_glAction of the lean-eval benchmark.

Uses 2

Statement usesDiagonal action of the general linear group on tensor powers · Permutation action of the symmetric group on tensor powers

TheoremSchur–Weyl duality: the general linear side#●ready to prove

Let \(R\) be a field, \(M\) a finite-dimensional vector space over \(R\), and \(k\) a natural number such that \(k!\) is invertible in \(R\). In the algebra of \(R\)-linear endomorphisms of the tensor power \(M^{\otimes k}\), the subalgebra generated by the image of the diagonal action \(g \mapsto g^{\otimes k}\) of \(\mathrm{GL}(M)\) equals the centralizer of the image of the action of the symmetric group \(S_k\) by permuting tensor factors.

public theorem_wanted 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 (glAction R M k)) =
      Subalgebra.centralizer R (Set.range (symAction R M k))

Sources

• H. Weyl, The Classical Groups, 1939; I. Schur, Über die rationalen Darstellungen der allgemeinen linearen Gruppe, 1927. Problem glAction_range_eq_centralizer_symAction of the lean-eval benchmark.

Uses 2

Statement usesDiagonal action of the general linear group on tensor powers · Permutation action of the symmetric group on tensor powers

2 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.