Finite products of matrix algebras

The dimension and the center of a product Π i, Matₙᵢ(k) of matrix algebras over a field, both read off the sizes nᵢ alone, together with the dimensions that an algebra equivalence A ≃ₐ[k] ∏ᵢ Matₙᵢ(Dᵢ) onto such a product — over an arbitrary family of coefficient algebras Dᵢ — transports back to the algebra A presented. Such a product is what a structure theorem of Artin--Wedderburn type presents an algebra as, and these are the invariants such a presentation transports; nothing here needs the presentation to come from Artin--Wedderburn, nor the coefficients to be division algebras.

• TauCeti.finrank_pi_matrix: over a semiring with the strong rank condition, the dimension of the product is ∑ᵢ nᵢ²;
• TauCeti.centerPiMatrixAlgEquiv: when every size is nonzero the center consists of the tuples of scalar matrices, so it is the algebra ι → k of functions on the index, whose dimension is the number of factors (TauCeti.finrank_center_pi_matrix);
• TauCeti.finiteDimensional_of_algEquiv_pi_matrix: the coefficient algebra of a block of nonzero size in a presentation of a finite-dimensional algebra is itself finite-dimensional. A block of size 0 is the zero ring whatever its coefficients are, so it constrains them not at all: the positivity hypothesis is essential rather than an artefact of the proof;
• TauCeti.finrank_eq_sum_sq_finrank: the dimension count finrank k A = ∑ᵢ nᵢ² · finrank k Dᵢ for an algebra presented as ∏ᵢ Matₙᵢ(Dᵢ). The count itself needs no positivity: a block of size 0 contributes 0 to both sides;
• TauCeti.sq_le_finrank_of_algEquiv_pi_matrix and TauCeti.card_le_finrank_of_algEquiv_pi_matrix: the bounds nᵢ² ≤ finrank k A on the degree of a single block with nontrivial coefficients — no other block plays any part, so the index need not even be finite — and, when every block is nonzero over nontrivial coefficients, Nat.card ι ≤ finrank k A on the number of blocks.

References

The dimension count implements the Layer 2 target "the dimension count" of the semisimple algebras roadmap, pinned there as finrank_eq_sum_sq_finrank; its algebraically closed form lives in TauCeti/RingTheory/Semisimple/DimensionCount.lean. See C. W. Curtis and I. Reiner, Representation Theory of Finite Groups and Associative Algebras, §25, or T. Y. Lam, A First Course in Noncommutative Rings, §3.

theorem TauCeti.finrank_pi_matrix (k : Type u_1) [Semiring k] [StrongRankCondition k] {ι : Type u_2} [Fintype ι] (d : ι → ℕ) : Module.finrank k ((i : ι) → Matrix (Fin (d i)) (Fin (d i)) k) = ∑ i : ι, d i ^ 2

The dimension of a finite product of matrix modules over a semiring with the strong rank condition is the sum of the squares of the sizes.

noncomputable def TauCeti.centerPiMatrixAlgEquiv (k : Type u_1) [Field k] {ι : Type u_2} (d : ι → ℕ) [∀ (i : ι), NeZero (d i)] : ↥(Subalgebra.center k ((i : ι) → Matrix (Fin (d i)) (Fin (d i)) k)) ≃ₐ[k] ι → k

The center of a product of nonzero matrix algebras over a field consists of the tuples of scalar matrices, so it is the algebra of functions on the index.

Equations

• TauCeti.centerPiMatrixAlgEquiv k d = TauCeti.centerPiAlgEquiv.trans (AlgEquiv.piCongrRight fun (i : ι) => TauCeti.centerAlgEquivOfIsCentral k (Matrix (Fin (d i)) (Fin (d i)) k))

@[simp]

theorem TauCeti.algebraMap_centerPiMatrixAlgEquiv_apply (k : Type u_1) [Field k] {ι : Type u_2} (d : ι → ℕ) [∀ (i : ι), NeZero (d i)] (x : ↥(Subalgebra.center k ((i : ι) → Matrix (Fin (d i)) (Fin (d i)) k))) (i : ι) : (algebraMap k (Matrix (Fin (d i)) (Fin (d i)) k)) ((centerPiMatrixAlgEquiv k d) x i) = ↑x i

centerPiMatrixAlgEquiv reads off the scalar of each component: the i-th component of a central tuple is the scalar matrix on the i-th value of the corresponding function.

@[simp]

theorem TauCeti.centerPiMatrixAlgEquiv_symm_apply_coe (k : Type u_1) [Field k] {ι : Type u_2} (d : ι → ℕ) [∀ (i : ι), NeZero (d i)] (f : ι → k) (i : ι) : ↑((centerPiMatrixAlgEquiv k d).symm f) i = (algebraMap k (Matrix (Fin (d i)) (Fin (d i)) k)) (f i)

The inverse of centerPiMatrixAlgEquiv assembles a function on the index into the tuple of the corresponding scalar matrices.

theorem TauCeti.finrank_center_pi_matrix (k : Type u_1) [Field k] {ι : Type u_2} (d : ι → ℕ) [Fintype ι] [∀ (i : ι), NeZero (d i)] : Module.finrank k ↥(Subalgebra.center k ((i : ι) → Matrix (Fin (d i)) (Fin (d i)) k)) = Fintype.card ι

The center of a finite product of nonzero matrix algebras over a field has dimension the number of factors.

Dimensions read off a presentation

theorem TauCeti.finiteDimensional_of_algEquiv_pi_matrix (k : Type u_1) [Field k] {ι : Type u_2} {d : ι → ℕ} {A : Type u_3} [Ring A] [Algebra k A] {D : ι → Type u_4} [(i : ι) → Ring (D i)] [(i : ι) → Algebra k (D i)] [FiniteDimensional k A] (e : A ≃ₐ[k] (i : ι) → Matrix (Fin (d i)) (Fin (d i)) (D i)) (i : ι) [NeZero (d i)] : FiniteDimensional k (D i)

The coefficient algebra of a block of nonzero size in a presentation of a finite-dimensional algebra as a product of matrix algebras is itself finite-dimensional, so no such presentation can smuggle an infinite-dimensional coefficient algebra into a nonzero block.

The positivity hypothesis NeZero (d i) is essential and not an artefact of the proof: a block of size 0 is the zero ring whatever its coefficients are, so it constrains D i not at all. Every Artin--Wedderburn presentation supplies that positivity.

theorem TauCeti.finrank_eq_sum_sq_finrank (k : Type u_1) [Field k] {ι : Type u_2} {d : ι → ℕ} {A : Type u_3} [Ring A] [Algebra k A] {D : ι → Type u_4} [(i : ι) → Ring (D i)] [(i : ι) → Algebra k (D i)] [Fintype ι] [FiniteDimensional k A] (e : A ≃ₐ[k] (i : ι) → Matrix (Fin (d i)) (Fin (d i)) (D i)) : Module.finrank k A = ∑ i : ι, d i ^ 2 * Module.finrank k (D i)

The Wedderburn dimension count. If a finite-dimensional k-algebra A is presented as a finite product ∏ᵢ Matₙᵢ(Dᵢ) of matrix algebras, then finrank k A = ∑ᵢ nᵢ² · finrank k Dᵢ.

No positivity is needed: a block of size 0 contributes 0 to both sides, whatever its coefficients are. Only the presentation is used: A is not assumed semisimple, although by RingEquiv.isSemisimpleRing it is one as soon as the coefficients Dᵢ are division algebras.

theorem TauCeti.sq_le_finrank_of_algEquiv_pi_matrix (k : Type u_1) [Field k] {ι : Type u_2} {d : ι → ℕ} {A : Type u_3} [Ring A] [Algebra k A] {D : ι → Type u_4} [(i : ι) → Ring (D i)] [(i : ι) → Algebra k (D i)] [FiniteDimensional k A] (e : A ≃ₐ[k] (i : ι) → Matrix (Fin (d i)) (Fin (d i)) (D i)) (i : ι) [Nontrivial (D i)] : d i ^ 2 ≤ Module.finrank k A

The degree of a block is bounded by the dimension: nᵢ² ≤ finrank k A for a block with nontrivial coefficients in a presentation of a finite-dimensional algebra by matrix algebras.

Only the block i takes part: the bound reads off the surjection of A onto that block alone, so neither the other coefficient algebras nor the finiteness of the index are assumed.

theorem TauCeti.card_le_finrank_of_algEquiv_pi_matrix (k : Type u_1) [Field k] {ι : Type u_2} {d : ι → ℕ} {A : Type u_3} [Ring A] [Algebra k A] {D : ι → Type u_4} [(i : ι) → Ring (D i)] [(i : ι) → Algebra k (D i)] [FiniteDimensional k A] (e : A ≃ₐ[k] (i : ι) → Matrix (Fin (d i)) (Fin (d i)) (D i)) [Finite ι] [∀ (i : ι), NeZero (d i)] [∀ (i : ι), Nontrivial (D i)] : Nat.card ι ≤ Module.finrank k A

The number of blocks is bounded by the dimension: a finite-dimensional algebra presented by nonzero matrix blocks over nontrivial coefficients has at most finrank k A of them.

For the group algebra of a finite group over a splitting field this bounds the number of irreducible representations by the order of the group.