The degree and the division ring of a matrix presentation are invariants

Artin--Wedderburn presents a simple Artinian ring as a matrix ring Matᵢ(D) over a division ring, and a semisimple ring as a finite product of such blocks. Mathlib supplies the presentation but says nothing about how much of it is determined by the ring: RingEquiv.card_blocks_eq shows the number of blocks is an invariant and RingEquiv.exists_simpleSubmodule_of_pi_matrix matches the blocks with the simple modules, but both are silent about the two remaining pieces of data, the size ι of a block and its division ring D. This file determines both, for a single block: it does not treat a product of blocks; RingEquiv.wedderburn_blocks_unique applies the result here after matching the factors of two product presentations.

The content is a description of those two data of A = Matᵢ(D) in terms that transport along a ring isomorphism. The column module ι → D, on which A acts by Matrix.mulVec, is a simple A-module (TauCeti.Matrix.isSimpleModule_pi), its endomorphism ring is Dᵐᵒᵖ (TauCeti.Matrix.mulOppositeRingEquivEnd), and the regular module is the direct sum of the Fintype.card ι columns (TauCeti.Matrix.linearEquivPi). So the size is the length of the regular module, and the division ring is the opposite endomorphism ring of a minimal left ideal. Both are manifestly invariant, and a ring isomorphism f : R ≃+* Matᵢ(D), read through RingEquiv.toSemilinearEquiv as an f-semilinear isomorphism of regular modules, carries them back to R. For a K-algebra presentation, the same transport is upgraded to an algebra equivalence of endomorphism rings, so the resulting comparison keeps the chosen base algebra fixed.

Main results

• TauCeti.Matrix.isSimpleModule_pi, TauCeti.Matrix.mulOppositeRingEquivEnd, TauCeti.Matrix.mulOppositeAlgEquivEnd, TauCeti.Matrix.linearEquivPi: the column module of Matᵢ(D) is simple with endomorphism ring Dᵐᵒᵖ, as a ring and over any shared base algebra, and the regular module is Fintype.card ι copies of it.
• TauCeti.length_eq_card_of_ringEquiv_matrix: a ring presented as Matᵢ(D) has regular module of length Fintype.card ι.
• TauCeti.nonempty_end_ringEquiv_of_ringEquiv_matrix and TauCeti.nonempty_end_algEquiv_of_algEquiv_matrix: for a ring presented as Matᵢ(D), the endomorphism ring of any simple left ideal is Dᵐᵒᵖ, with an algebra-linear form over a shared base.
• TauCeti.card_eq_of_ringEquiv_matrix, TauCeti.nonempty_ringEquiv_of_ringEquiv_matrix and the packaged TauCeti.wedderburn_data_unique: two matrix presentations of the same ring have the same size and isomorphic division rings. Their algebra-linear counterparts are TauCeti.nonempty_algEquiv_of_algEquiv_matrix and TauCeti.nonempty_algEquiv_matrix_iff.
• TauCeti.nonempty_ringEquiv_matrix_iff: the resulting classification, that Matᵢ(D) ≃+* Mat_κ(E) holds exactly when ι and κ have the same cardinality and D ≃+* E, with TauCeti.nonempty_algEquiv_matrix_iff its algebra-linear counterpart.

Implementation notes

The index type ι is an arbitrary Fintype, not Fin n; the Fin n shape that the Artin--Wedderburn theorems produce is the corollary TauCeti.wedderburn_data_unique. Nonempty ι is essential and not decoration wherever the division ring is involved: Mat_∅(D) is the trivial ring for every D, so an empty block determines no D at all. It is the hypothesis NeZero n supplies in IsSemisimpleRing.exists_ringEquiv_pi_matrix_divisionRing and in RingEquiv.card_blocks_eq. The statements about the size alone hold for every ι, the empty case saying that the trivial ring has regular module of length 0, and are stated without it.

Everything is stated for the left regular module, matching the convention of IsSemisimpleRing, so the simple module is the column module -- on which a matrix acts by Matrix.mulVec -- and the endomorphism ring, acting on the other side, comes out as Dᵐᵒᵖ rather than D. This is also Mathlib's convention in IsSimpleRing.exists_ringEquiv_matrix_end_mulOpposite.

Note that DecidableEq ι is needed to make Matᵢ(D) a ring, but not to state the ring-equivalence transport results, whose types mention only the multiplication and addition of Matᵢ(D); those are therefore stated without it and use classical internally. The algebra-equivalence counterparts do assume DecidableEq ι, because the Algebra K (Matrix ι ι D) instance uses the full matrix-ring structure.

The matching of the blocks of two product presentations is proved downstream in TauCeti/RingTheory/Semisimple/Wedderburn/Uniqueness.lean: the coordinate central idempotents recover the factor permutation, and the theorem in this file then identifies the data in each factor.

References

See T. Y. Lam, A First Course in Noncommutative Rings, GTM 131, §3, or C. W. Curtis and I. Reiner, Representation Theory of Finite Groups and Associative Algebras, §26.

theorem TauCeti.Matrix.exists_mulVec_eq {ι : Type u_1} [Fintype ι] {D : Type u_2} [DivisionSemiring D] {v : ι → D} (hv : v ≠ 0) (w : ι → D) : ∃ (A : Matrix ι ι D), A.mulVec v = w

A nonzero column vector generates the column module. Over a division semiring one can solve A *ᵥ v = w for A as soon as v ≠ 0: put w in the column of A indexed by a coordinate where v does not vanish, scaled by the inverse of that coordinate.

def TauCeti.Matrix.rightMul {ι : Type u_1} [Fintype ι] {D : Type u_2} [DecidableEq ι] [Semiring D] (d : D) : Module.End (Matrix ι ι D) (ι → D)

Right multiplication by an element of D on column vectors. It commutes with left multiplication by a matrix, so it is an endomorphism of the column module, and these are all of them (TauCeti.Matrix.mulOppositeRingEquivEnd).

Equations

• TauCeti.Matrix.rightMul d = { toFun := fun (v : ι → D) (i : ι) => v i * d, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.Matrix.rightMul_apply {ι : Type u_1} [Fintype ι] {D : Type u_2} [DecidableEq ι] [Semiring D] (d : D) (v : ι → D) (i : ι) : (rightMul d) v i = v i * d

def TauCeti.Matrix.linearEquivPi (ι : Type u_1) [Fintype ι] (D : Type u_2) [DecidableEq ι] [Semiring D] : Matrix ι ι D ≃ₗ[Matrix ι ι D] ι → ι → D

The regular module of a matrix ring is the direct sum of its columns. Left multiplication acts on each column separately, so Matᵢ(D) is Fintype.card ι copies of the column module.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Matrix.linearEquivPi_apply {ι : Type u_1} [Fintype ι] {D : Type u_2} [DecidableEq ι] [Semiring D] (A : Matrix ι ι D) (j i : ι) : (linearEquivPi ι D) A j i = A i j

@[simp]

theorem TauCeti.Matrix.linearEquivPi_symm_apply {ι : Type u_1} [Fintype ι] {D : Type u_2} [DecidableEq ι] [Semiring D] (f : ι → ι → D) (i j : ι) : (linearEquivPi ι D).symm f i j = f j i

instance TauCeti.Matrix.isSimpleModule_pi {ι : Type u_1} [Fintype ι] {D : Type u_2} [DecidableEq ι] [DivisionRing D] [Nonempty ι] : IsSimpleModule (Matrix ι ι D) (ι → D)

The column module of a matrix ring over a division ring is simple. This is the simple module of the Wedderburn block Matᵢ(D); since a matrix ring over a division ring is simple Artinian, every simple Matᵢ(D)-module is isomorphic to it.

noncomputable def TauCeti.Matrix.mulOppositeRingEquivEnd (ι : Type u_1) [Fintype ι] (D : Type u_2) [DecidableEq ι] [DivisionRing D] [Nonempty ι] : Dᵐᵒᵖ ≃+* Module.End (Matrix ι ι D) (ι → D)

The endomorphism ring of the column module of Matᵢ(D) is Dᵐᵒᵖ. An endomorphism commutes with the matrices carrying one coordinate to another, so it is right multiplication by the single scalar recording its value at a standard basis vector. The multiplication is reversed because the scalars act on the side opposite to the matrices.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Matrix.mulOppositeRingEquivEnd_apply {ι : Type u_1} [Fintype ι] {D : Type u_2} [DecidableEq ι] [DivisionRing D] [Nonempty ι] (d : Dᵐᵒᵖ) : (mulOppositeRingEquivEnd ι D) d = rightMul (MulOpposite.unop d)

noncomputable def TauCeti.Matrix.mulOppositeAlgEquivEnd (ι : Type u_1) [Fintype ι] (D : Type u_2) [DecidableEq ι] [DivisionRing D] (K : Type u_3) [CommSemiring K] [Algebra K D] [Nonempty ι] : Dᵐᵒᵖ ≃ₐ[K] Module.End (Matrix ι ι D) (ι → D)

The endomorphism algebra of the column module of Matᵢ(D) is Dᵐᵒᵖ.

This is the algebra-linear refinement of TauCeti.Matrix.mulOppositeRingEquivEnd. The scalar from K acts on a column on the left, while the displayed endomorphism acts on the right; these agree because the image of K is central in every K-algebra.

Equations

• TauCeti.Matrix.mulOppositeAlgEquivEnd ι D K = AlgEquiv.ofRingEquiv ⋯

@[simp]

theorem TauCeti.Matrix.mulOppositeAlgEquivEnd_apply {ι : Type u_1} [Fintype ι] {D : Type u_2} [DecidableEq ι] [DivisionRing D] (K : Type u_3) [CommSemiring K] [Algebra K D] [Nonempty ι] (d : Dᵐᵒᵖ) : (mulOppositeAlgEquivEnd ι D K) d = rightMul (MulOpposite.unop d)

The algebra equivalence with the endomorphisms of the column module sends d to right multiplication by d.unop.

theorem TauCeti.Matrix.length_self_eq_card (ι : Type u_1) [Fintype ι] (D : Type u_2) [DecidableEq ι] [DivisionRing D] : Module.length (Matrix ι ι D) (Matrix ι ι D) = ↑(Fintype.card ι)

The regular module of Matᵢ(D) has length Fintype.card ι: it is the direct sum of its Fintype.card ι columns, and each column is simple. For empty ι both sides are 0, the ring being trivial.

theorem TauCeti.length_eq_card_of_ringEquiv_matrix {R : Type u_1} [Ring R] {ι : Type u_2} [Fintype ι] {D : Type u_3} [DivisionRing D] (f : R ≃+* Matrix ι ι D) : Module.length R R = ↑(Fintype.card ι)

The size of a matrix presentation is the length of the regular module, hence an invariant of the ring: a ring isomorphism f : R ≃+* Matᵢ(D) is an f-semilinear isomorphism of regular modules, so it identifies the two lattices of left ideals.

theorem TauCeti.nonempty_end_algEquiv_of_algEquiv_matrix {R : Type u_1} [Ring R] {ι : Type u_2} [Fintype ι] {D : Type u_3} [DivisionRing D] {K : Type u_4} [CommSemiring K] [Algebra K R] [DecidableEq ι] [Algebra K D] [Nonempty ι] (f : R ≃ₐ[K] Matrix ι ι D) (I : Submodule R R) [IsSimpleModule R ↥I] : Nonempty (Module.End R ↥I ≃ₐ[K] Dᵐᵒᵖ)

The endomorphism algebra of a simple left ideal determines the division algebra in an algebra presentation.

This is the algebra-linear refinement of TauCeti.nonempty_end_ringEquiv_of_ringEquiv_matrix. Conjugation along the semilinear transport of the ideal preserves K because the presentation is a K-algebra equivalence; conjugation between the two simple modules is already linear over the matrix algebra.

theorem TauCeti.nonempty_end_ringEquiv_of_ringEquiv_matrix {R : Type u_1} [Ring R] {ι : Type u_2} [Fintype ι] {D : Type u_3} [DivisionRing D] [Nonempty ι] (f : R ≃+* Matrix ι ι D) (I : Submodule R R) [IsSimpleModule R ↥I] : Nonempty (Module.End R ↥I ≃+* Dᵐᵒᵖ)

The division ring of a matrix presentation is the opposite endomorphism ring of any simple left ideal, hence an invariant of the ring.

The f-semilinear isomorphism of regular modules carries I to a simple left ideal of Matᵢ(D) and identifies the two endomorphism rings; over the simple Artinian ring Matᵢ(D) that ideal is isomorphic to the column module, whose endomorphism ring is Dᵐᵒᵖ.

theorem TauCeti.card_eq_of_ringEquiv_matrix {R : Type u_1} [Ring R] {ι : Type u_2} [Fintype ι] {D : Type u_3} [DivisionRing D] {κ : Type u_4} [Fintype κ] {E : Type u_5} [DivisionRing E] (f : R ≃+* Matrix ι ι D) (g : R ≃+* Matrix κ κ E) : Fintype.card ι = Fintype.card κ

The size of a matrix presentation is unique: two presentations of one ring as a matrix ring over a division ring have equally many rows.

theorem TauCeti.nonempty_algEquiv_of_algEquiv_matrix {R : Type u_1} [Ring R] {ι : Type u_2} [Fintype ι] {D : Type u_3} [DivisionRing D] {κ : Type u_4} [Fintype κ] {E : Type u_5} [DivisionRing E] {K : Type u_6} [CommSemiring K] [Algebra K R] [DecidableEq ι] [Algebra K D] [DecidableEq κ] [Algebra K E] [Nonempty ι] [Nonempty κ] (f : R ≃ₐ[K] Matrix ι ι D) (g : R ≃ₐ[K] Matrix κ κ E) : Nonempty (D ≃ₐ[K] E)

The division algebra in a matrix presentation of a K-algebra is unique up to K-algebra isomorphism.

Both division algebras are obtained as the opposite endomorphism algebra of one minimal left ideal of R. The common ideal makes the resulting isomorphism preserve the specified copy of K, which need not follow from ring-level Wedderburn uniqueness alone.

theorem TauCeti.nonempty_algEquiv_matrix_iff {ι : Type u_2} [Fintype ι] {D : Type u_3} [DivisionRing D] {κ : Type u_4} [Fintype κ] {E : Type u_5} [DivisionRing E] {K : Type u_6} [CommSemiring K] [DecidableEq ι] [Algebra K D] [DecidableEq κ] [Algebra K E] [Nonempty ι] [Nonempty κ] : Nonempty (Matrix ι ι D ≃ₐ[K] Matrix κ κ E) ↔ Fintype.card ι = Fintype.card κ ∧ Nonempty (D ≃ₐ[K] E)

Matrix algebras over division algebras are classified over their shared base. They are isomorphic as K-algebras exactly when their index types have the same cardinality and their coefficient division algebras are isomorphic as K-algebras.

theorem TauCeti.nonempty_ringEquiv_of_ringEquiv_matrix {R : Type u_1} [Ring R] {ι : Type u_2} [Fintype ι] {D : Type u_3} [DivisionRing D] {κ : Type u_4} [Fintype κ] {E : Type u_5} [DivisionRing E] [Nonempty ι] [Nonempty κ] (f : R ≃+* Matrix ι ι D) (g : R ≃+* Matrix κ κ E) : Nonempty (D ≃+* E)

The division ring of a matrix presentation is unique up to isomorphism: two presentations of one ring as a matrix ring over a division ring have isomorphic division rings.

Both division rings are computed from a single minimal left ideal of the ring, so no comparison of choices is needed: they are the two readings of one and the same endomorphism ring.

theorem TauCeti.nonempty_ringEquiv_matrix_iff {ι : Type u_2} [Fintype ι] {D : Type u_3} [DivisionRing D] {κ : Type u_4} [Fintype κ] {E : Type u_5} [DivisionRing E] [Nonempty ι] [Nonempty κ] : Nonempty (Matrix ι ι D ≃+* Matrix κ κ E) ↔ Fintype.card ι = Fintype.card κ ∧ Nonempty (D ≃+* E)

Matrix rings over division rings are classified by their size and their division ring. Two of them are isomorphic exactly when they have equally many rows and isomorphic division rings.

The forward direction is the uniqueness above, applied to the two presentations of Matᵢ(D) given by the identity and by the isomorphism; the converse reindexes along an equivalence of the two index types (Matrix.reindexRingEquiv) and then transports the entries (RingEquiv.mapMatrix).

theorem TauCeti.wedderburn_data_unique {R : Type u_1} [Ring R] {D : Type u_3} [DivisionRing D] {E : Type u_5} [DivisionRing E] {n m : ℕ} [NeZero n] [NeZero m] (f : R ≃+* Matrix (Fin n) (Fin n) D) (g : R ≃+* Matrix (Fin m) (Fin m) E) : n = m ∧ Nonempty (D ≃+* E)

Uniqueness of the Wedderburn data of a simple Artinian ring. Two presentations of a ring as a matrix ring over a division ring have the same degree and isomorphic division rings.

This is the Fin n shape produced by IsSimpleRing.exists_ringEquiv_matrix_divisionRing; the positivity hypotheses NeZero n are the ones that theorem supplies, and they are essential, since Mat₀(D) is the trivial ring for every D.