Matrix units inside a block

Inside each block of the symmetric-group algebra the central idempotent P.e μ of a SchurPackage splits as a sum of P.dim μ orthogonal nonzero idempotents (SchurPackage.exists_block_units).

The route is through a simple submodule of the regular module lying inside the block, which exists because the group algebra is semisimple and the idempotent is nonzero (exists_simple_of_central_idem). The native action on such a carrier sends the idempotent to the identity, is surjective onto the endomorphisms of the carrier (nPsi_surjective, from mPsiLin_surjective), and is injective on the block (block_faithful); comparing dimensions against block_rank identifies the dimension of the carrier with P.dim μ, and the rank-one projections attached to a basis of the carrier (basisProj) pull back to the required family of units.

noncomputable def RS.basisProj {V : Type u_1} [AddCommGroup V] [Module ℂ V] {d : ℕ} (b : Module.Basis (Fin d) ℂ V) (i : Fin d) : Module.End ℂ V

The rank-one idempotent attached to a basis vector: the projection onto the i-th coordinate line of the basis b.

Equations

• RS.basisProj b i = (b.coord i).smulRight (b i)

theorem RS.basisProj_apply {V : Type u_1} [AddCommGroup V] [Module ℂ V] {d : ℕ} (b : Module.Basis (Fin d) ℂ V) (i : Fin d) (m : V) : (basisProj b i) m = (b.repr m) i • b i

The projection scales the i-th coordinate back onto the i-th basis vector.

theorem RS.basisProj_mul_self {V : Type u_1} [AddCommGroup V] [Module ℂ V] {d : ℕ} (b : Module.Basis (Fin d) ℂ V) (i : Fin d) : basisProj b i * basisProj b i = basisProj b i

Each basis projection is idempotent.

theorem RS.basisProj_mul_ne {V : Type u_1} [AddCommGroup V] [Module ℂ V] {d : ℕ} (b : Module.Basis (Fin d) ℂ V) {i j : Fin d} (hij : i ≠ j) : basisProj b i * basisProj b j = 0

Distinct basis projections are orthogonal.

theorem RS.sum_basisProj {V : Type u_1} [AddCommGroup V] [Module ℂ V] {d : ℕ} (b : Module.Basis (Fin d) ℂ V) : ∑ i : Fin d, basisProj b i = 1

The basis projections sum to the identity.

theorem RS.basisProj_ne_zero {V : Type u_1} [AddCommGroup V] [Module ℂ V] {d : ℕ} (b : Module.Basis (Fin d) ℂ V) (i : Fin d) : basisProj b i ≠ 0

Each basis projection is nonzero.

theorem RS.exists_simple_of_central_idem {G : Type u_2} [Group G] [Finite G] (e : MonoidAlgebra ℂ G) (hidem : e * e = e) (hcentral : ∀ (x : MonoidAlgebra ℂ G), e * x = x * e) (hne : e ≠ 0) : ∃ (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)), IsSimpleModule (MonoidAlgebra ℂ G) ↥S ∧ ∀ s ∈ S, e * s = s

Every nonzero central idempotent of a complex group algebra has a simple submodule of the regular module inside its block: a simple submodule on which it multiplies as the identity.

theorem RS.nPsi_eq_one_of_forall_eq {G : Type u_2} [Group G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) (e : MonoidAlgebra ℂ G) (he : ∀ s ∈ S, e * s = s) : (nPsi S) e = 1

An element multiplying a submodule of the regular module as the identity acts as the identity endomorphism of its carrier.

theorem RS.nPsi_surjective {G : Type u_2} [Group G] [Finite G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) (hS : IsSimpleModule (MonoidAlgebra ℂ G) ↥S) : Function.Surjective ⇑(nPsi S)

The native action of a simple submodule of the regular module is surjective onto the endomorphisms of its carrier.

theorem RS.SchurPackage.exists_block_units (P : SchurPackage) (μ : YoungDiagram) : ∃ (u : Fin (P.dim μ) → SymGroupAlgebra μ.card), (∀ (i : Fin (P.dim μ)), u i * u i = u i) ∧ (∀ (i j : Fin (P.dim μ)), i ≠ j → u i * u j = 0) ∧ (∀ (i : Fin (P.dim μ)), P.e μ * u i = u i) ∧ (∀ (i : Fin (P.dim μ)), u i * P.e μ = u i) ∧ ∑ i : Fin (P.dim μ), u i = P.e μ ∧ ∀ (i : Fin (P.dim μ)), u i ≠ 0

Block units: inside each block of the symmetric-group algebra, the central idempotent P.e μ splits as a sum of P.dim μ orthogonal nonzero idempotents of the block.