Native block faithfulness

The representation map of the native carrier is injective on the block (kill criterion plus the faithfulness trick) and surjective onto the submodule endomorphisms (dimension count over canonical instances); the sandwich identity of a nonzero block element then pulls back to express the projector in the two-sided ideal it generates, so an algebra map vanishing on a block element but not on the projector is impossible.

@[reducible, inline]

noncomputable abbrev RS.nPsi {G : Type u_1} [Group G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) : MonoidAlgebra ℂ G →ₐ[ℂ] Module.End ℂ (subCarrier S)

The native representation map.

Equations

• RS.nPsi S = (RS.rhoS S).asAlgebraHom

theorem RS.nPsi_eq_zero_iff {G : Type u_1} [Group G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) (y : MonoidAlgebra ℂ G) : (nPsi S) y = 0 ↔ ∀ t ∈ S, y * t = 0

The kill criterion for the native action.

theorem RS.kills_of_equiv_kills_native {G : Type u_1} [Group G] (S T : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) (hequiv : Nonempty ((rhoS S).Equiv (rhoS T))) (y : MonoidAlgebra ℂ G) (hy : ∀ s ∈ S, y * s = 0) (t : MonoidAlgebra ℂ G) : t ∈ T → y * t = 0

Annihilation transports along equivalences of the native representations.

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

A block element acting as zero on its simple kills every simple submodule.

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

The projector acts as the identity on its own simple.

@[reducible, inline]

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

The native block.

Equations

• RS.natBlock S = (LinearMap.mulLeft ℂ (RS.nProjector S)).range

noncomputable def RS.stdEquiv {G : Type u_1} [Group G] [Fintype G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) : subCarrier S ≃ₗ[ℂ] Fin (nDim S) → ℂ

The standard-coordinates equivalence of the carrier.

Equations

• RS.stdEquiv S = (Module.finBasis ℂ (RS.subCarrier S)).equivFun

noncomputable def RS.mPsi {G : Type u_1} [Group G] [Fintype G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) (y : MonoidAlgebra ℂ G) : (Fin (nDim S) → ℂ) →ₗ[ℂ] Fin (nDim S) → ℂ

The block map in standard coordinates.

Equations

• RS.mPsi S y = (↑(RS.stdEquiv S) ∘ₗ (RS.nPsi S) y) ∘ₗ ↑(RS.stdEquiv S).symm

theorem RS.mPsi_apply {G : Type u_1} [Group G] [Fintype G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) (y : MonoidAlgebra ℂ G) (v : Fin (nDim S) → ℂ) : (mPsi S y) v = (stdEquiv S) (((nPsi S) y) ((stdEquiv S).symm v))

The coordinate form of the block map, unfolded.

theorem RS.mPsi_mul {G : Type u_1} [Group G] [Fintype G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) (y y' : MonoidAlgebra ℂ G) : mPsi S (y * y') = mPsi S y ∘ₗ mPsi S y'

It carries multiplication to composition.

theorem RS.mPsi_zero_iff {G : Type u_1} [Group G] [Fintype G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) (y : MonoidAlgebra ℂ G) : mPsi S y = 0 ↔ (nPsi S) y = 0

It vanishes exactly when the block map does, the coordinates being an isomorphism.

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

The projector acts as the identity on the carrier.

noncomputable def RS.mPsiLin {G : Type u_1} [Group G] [Fintype G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) : ↥(natBlock S) →ₗ[ℂ] (Fin (nDim S) → ℂ) →ₗ[ℂ] Fin (nDim S) → ℂ

The standard-coordinates block map on the block.

Equations

• RS.mPsiLin S = { toFun := fun (y : ↥(RS.natBlock S)) => RS.mPsi S ↑y, map_add' := ⋯, map_smul' := ⋯ }

theorem RS.mPsiLin_injective {G : Type u_1} [Group G] [Fintype G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) (hS : IsSimpleModule (MonoidAlgebra ℂ G) ↥S) : Function.Injective ⇑(mPsiLin S)

The coordinate block map is injective.

theorem RS.mPsiLin_surjective {G : Type u_1} [Group G] [Fintype G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) (hS : IsSimpleModule (MonoidAlgebra ℂ G) ↥S) : Function.Surjective ⇑(mPsiLin S)

And surjective onto the endomorphisms, by a dimension count — so the block is the full matrix algebra of its carrier.

theorem RS.nProjector_block_faithful {G : Type u_1} [Group G] [Fintype G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) (hS : IsSimpleModule (MonoidAlgebra ℂ G) ↥S) {B : Type u_2} [Ring B] [Algebra ℂ B] (φ : MonoidAlgebra ℂ G →ₐ[ℂ] B) (hφ : φ (nProjector S) ≠ 0) (x : MonoidAlgebra ℂ G) (h0 : φ (nProjector S * x) = 0) : nProjector S * x = 0

Native block faithfulness: an algebra map that does not kill the projector is injective on its block.