Dimension bounds through the commutant

A representation factoring through an algebra of dimension at most B ^ 2 has dimension at most B times the dimension of its commutant. Each simple constituent has dimension at most B, by native block faithfulness, and the commutant dimension bounds the number of simple summands, counted with multiplicity.

theorem RS.nDim_sq_le_finrank_of_projector_ne_zero {G : Type u_1} [Group G] [Fintype G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) (hS : IsSimpleModule (MonoidAlgebra ℂ G) ↥S) {A : Type u_4} [Ring A] [Algebra ℂ A] [FiniteDimensional ℂ A] (φ : MonoidAlgebra ℂ G →ₐ[ℂ] A) (hne : φ (nProjector S) ≠ 0) : nDim S ^ 2 ≤ Module.finrank ℂ A

A nonzero native block in a finite-dimensional algebra has at least the square of its simple constituent's dimension.

theorem RS.finrank_le_sqrt_mul_commutant {G : Type u_1} {V : Type u_2} [Group G] [Finite G] [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) {A : Type u_4} [Ring A] [Algebra ℂ A] [FiniteDimensional ℂ A] (φ : MonoidAlgebra ℂ G →ₐ[ℂ] A) (hker : ∀ (x : MonoidAlgebra ℂ G), φ x = 0 → ρ.asAlgebraHom x = 0) : Module.finrank ℂ V ≤ (Module.finrank ℂ A).sqrt * Module.finrank ℂ (ρ.IntertwiningMap ρ)

The dimension of a finite-group representation is bounded by the square root of the dimension of a factoring algebra, times the dimension of its commutant.

theorem RS.finrank_le_mul_commutant {G : Type u_1} {V : Type u_2} [Group G] [Finite G] [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) {A : Type u_4} [Ring A] [Algebra ℂ A] [FiniteDimensional ℂ A] (φ : MonoidAlgebra ℂ G →ₐ[ℂ] A) (hker : ∀ (x : MonoidAlgebra ℂ G), φ x = 0 → ρ.asAlgebraHom x = 0) (B : ℕ) (hB : Module.finrank ℂ A ≤ B ^ 2) : Module.finrank ℂ V ≤ B * Module.finrank ℂ (ρ.IntertwiningMap ρ)

If a finite-group representation factors through an algebra of dimension at most B ^ 2, its dimension is at most B times the dimension of its commutant.

theorem RS.finrank_sq_le_mul_commutant_sq {G : Type u_1} {V : Type u_2} [Group G] [Finite G] [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) {A : Type u_4} [Ring A] [Algebra ℂ A] [FiniteDimensional ℂ A] (φ : MonoidAlgebra ℂ G →ₐ[ℂ] A) (hker : ∀ (x : MonoidAlgebra ℂ G), φ x = 0 → ρ.asAlgebraHom x = 0) : Module.finrank ℂ V ^ 2 ≤ Module.finrank ℂ A * Module.finrank ℂ (ρ.IntertwiningMap ρ) ^ 2

The square of the representation dimension is at most the factoring algebra dimension times the square of the commutant dimension.