The native projector and its action table

Character, dimension, and normalized projector of a simple submodule on the native carrier; the scalar action, the orthogonality-evaluated action table, idempotency, centrality, and the block rank.

noncomputable def RS.nChar {G : Type u_1} [Group G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) (g : G) : ℂ

The character of a submodule of the regular module.

Equations

• RS.nChar S g = (RS.rhoS S).character g

noncomputable def RS.nDim {G : Type u_1} [Group G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) : ℕ

The dimension of a submodule of the regular module.

Equations

• RS.nDim S = Module.finrank ℂ (RS.subCarrier S)

noncomputable def RS.nCoeff {G : Type u_1} [Group G] [Fintype G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) : G → ℂ

The normalized projector coefficient.

Equations

• RS.nCoeff S g = ↑(RS.nDim S) / ↑(Fintype.card G) * RS.nChar S g⁻¹

noncomputable def RS.nProjector {G : Type u_1} [Group G] [Fintype G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) : MonoidAlgebra ℂ G

The normalized projector.

Equations

• RS.nProjector S = RS.classElem (RS.nCoeff S)

theorem RS.nCoeff_classFun {G : Type u_1} [Group G] [Fintype G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) (g h : G) : nCoeff S (h * g * h⁻¹) = nCoeff S g

The native projector's coefficient is a class function.

theorem RS.mem_subCarrier {G : Type u_1} [Group G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) {t : MonoidAlgebra ℂ G} (ht : t ∈ S) : t ∈ Submodule.restrictScalars ℂ S

Membership transfer to the restricted-scalars form.

theorem RS.classElem_mul_mem_native {G : Type u_1} [Group G] [Fintype G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) (hS : IsSimpleModule (MonoidAlgebra ℂ G) ↥S) (c : G → ℂ) (hc : ∀ (g h : G), c (h * g * h⁻¹) = c g) (t : MonoidAlgebra ℂ G) (ht : t ∈ S) : classElem c * t = ((∑ g : G, c g * nChar S g) / ↑(nDim S)) • t

The native scalar action: a class element multiplies each element of a simple submodule by the character-pairing scalar.

theorem RS.rhoS_isIrreducible {G : Type u_1} [Group G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) (hS : IsSimpleModule (MonoidAlgebra ℂ G) ↥S) : (rhoS S).IsIrreducible

The native representation of a simple submodule is irreducible in the subrepresentation-lattice sense.

theorem RS.nProjector_mul_mem {G : Type u_1} [Group G] [Fintype G] (S T : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) (hS : IsSimpleModule (MonoidAlgebra ℂ G) ↥S) (hT : IsSimpleModule (MonoidAlgebra ℂ G) ↥T) (t : MonoidAlgebra ℂ G) (ht : t ∈ T) : nProjector S * t = (if Nonempty ((rhoS S).Equiv (rhoS T)) then 1 else 0) • t

The native action table: the projector of a simple submodule acts on each simple submodule as 1 or 0 by equivalence.

theorem RS.nProjector_idem {G : Type u_1} [Group G] [Fintype G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) (hS : IsSimpleModule (MonoidAlgebra ℂ G) ↥S) : nProjector S * nProjector S = nProjector S

Idempotency of the native projector.

theorem RS.nProjector_central {G : Type u_1} [Group G] [Fintype G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) (y : MonoidAlgebra ℂ G) : nProjector S * y = y * nProjector S

Centrality of the native projector.

theorem RS.nProjector_coeff_one {G : Type u_1} [Group G] [Fintype G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) : (nProjector S).coeff 1 = ↑(nDim S) ^ 2 / ↑(Fintype.card G)

The projector's coefficient at the identity.

theorem RS.nProjector_block_rank {G : Type u_1} [Group G] [Fintype G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) (hS : IsSimpleModule (MonoidAlgebra ℂ G) ↥S) : Module.finrank ℂ ↥(LinearMap.mulLeft ℂ (nProjector S)).range = nDim S ^ 2

The native block rank.