Matrix units and the matrix-ring representation

A ring with abstract matrix units eᵢⱼ is isomorphic to a matrix ring over the corner subring of e₀₀. This file packages the class hasMatrixUnits, the construction of matrix units from OrtIdemDiv, and the explicit ring isomorphism R ≃+* Matrix (Fin n) (Fin n) (e₀₀ R e₀₀).

class LeanPool.ArtinWedderburn.hasMatrixUnits (R : Type u_1) [Ring R] (n : ℕ) : Type u_1

Class packaging a system of n × n matrix units eᵢⱼ in a ring R.

• es : Fin n → Fin n → R

  The matrix units indexed by Fin n × Fin n.

• diag_sum_eq_one : ∑ i : Fin n, es i i = 1
• mul_ij_kl_eq_kron_delta_jk_mul_es_il (i j k l : Fin n) : es i j * es k l = if j = k then es i l else 0

theorem LeanPool.ArtinWedderburn.nontrivial_zero_not_one (R : Type u_1) [Ring R] (nontriv : Nontrivial R) : 0 ≠ 1

theorem LeanPool.ArtinWedderburn.nontrivial_ortidem_n_pos (R : Type u_1) [Ring R] (nontriv : Nontrivial R) (ort_idem : OrtIdemDiv R) : 0 < ort_idem.n

theorem LeanPool.ArtinWedderburn.OrtIdem_imply_MatUnits' (R : Type u_1) [Ring R] {n : ℕ} (hn : 0 < n) (diag_es : Fin n → R) (idem : ∀ (i : Fin n), IsIdempotentElem (diag_es i)) (ort : ∀ (i j : Fin n), i ≠ j → PairwiseOrthogonal (diag_es i) (diag_es j)) (sum_eq_one : ∑ i : Fin n, diag_es i = 1) (row_es : Fin n → R) (row_in : ∀ (i : Fin n), row_es i ∈ bothMul (diag_es ⟨0, hn⟩) (diag_es i)) (col_es : Fin n → R) (col_in : ∀ (i : Fin n), col_es i ∈ bothMul (diag_es i) (diag_es ⟨0, hn⟩)) (comp1 : ∀ (i : Fin n), row_es i * col_es i = diag_es ⟨0, hn⟩) (comp2 : ∀ (i : Fin n), col_es i * row_es i = diag_es i) : ∃ (mat_units : hasMatrixUnits R n), hasMatrixUnits.es ⟨0, hn⟩ ⟨0, hn⟩ = diag_es ⟨0, hn⟩

theorem LeanPool.ArtinWedderburn.lemma_2_20' (R : Type u_1) [Ring R] (prime : IsPrimeRing R) (ort_idem : OrtIdemDiv R) (n_pos : 0 < ort_idem.n) : ∃ (mat_units : hasMatrixUnits R ort_idem.n), hasMatrixUnits.es ⟨0, n_pos⟩ ⟨0, n_pos⟩ = ort_idem.f ⟨0, n_pos⟩

theorem LeanPool.ArtinWedderburn.e00_idem (R : Type u_1) [Ring R] {n : ℕ} {hn : 0 < n} [mu : hasMatrixUnits R n] : IsIdempotentElem (hasMatrixUnits.es ⟨0, hn⟩ ⟨0, hn⟩)

@[reducible, inline]

abbrev LeanPool.ArtinWedderburn.e00Cornerring (R : Type u_1) [Ring R] {n : ℕ} {hn : 0 < n} [mu : hasMatrixUnits R n] : NonUnitalSubring R

The corner ring of the (0, 0) matrix unit.

Equations

• LeanPool.ArtinWedderburn.e00Cornerring R = LeanPool.ArtinWedderburn.CornerSubring ⋯

theorem LeanPool.ArtinWedderburn.e00_cornerring_1 (R : Type u_1) [Ring R] {n : ℕ} {hn : 0 < n} [mu : hasMatrixUnits R n] : ↑1 = hasMatrixUnits.es ⟨0, hn⟩ ⟨0, hn⟩

theorem LeanPool.ArtinWedderburn.e00e0i_eq_e_0i (R : Type u_1) [Ring R] {n : ℕ} {hn : 0 < n} [mu : hasMatrixUnits R n] (i : Fin n) : hasMatrixUnits.es ⟨0, hn⟩ ⟨0, hn⟩ * hasMatrixUnits.es ⟨0, hn⟩ i = hasMatrixUnits.es ⟨0, hn⟩ i

theorem LeanPool.ArtinWedderburn.ei0e00_eq_e_ei0 (R : Type u_1) [Ring R] {n : ℕ} {hn : 0 < n} [mu : hasMatrixUnits R n] (i : Fin n) : hasMatrixUnits.es i ⟨0, hn⟩ * hasMatrixUnits.es ⟨0, hn⟩ ⟨0, hn⟩ = hasMatrixUnits.es i ⟨0, hn⟩

theorem LeanPool.ArtinWedderburn.ei0e0j_eq_eij (R : Type u_1) [Ring R] {n : ℕ} {hn : 0 < n} [mu : hasMatrixUnits R n] (i j : Fin n) : hasMatrixUnits.es i ⟨0, hn⟩ * hasMatrixUnits.es ⟨0, hn⟩ j = hasMatrixUnits.es i j

def LeanPool.ArtinWedderburn.ijCorner (R : Type u_1) [Ring R] {n : ℕ} {hn : 0 < n} [mu : hasMatrixUnits R n] (i j : Fin n) (a : R) : ↥(CornerSubring ⋯)

The (i, j)-component e₀ᵢ * a * eⱼ₀ of a : R in the corner ring of e₀₀.

Equations

• LeanPool.ArtinWedderburn.ijCorner R i j a = ⟨LeanPool.ArtinWedderburn.hasMatrixUnits.es ⟨0, hn⟩ i * a * LeanPool.ArtinWedderburn.hasMatrixUnits.es j ⟨0, hn⟩, ⋯⟩

@[reducible, inline]

abbrev LeanPool.ArtinWedderburn.matrixCorner (R : Type u_1) [Ring R] {n : ℕ} {hn : 0 < n} [mu : hasMatrixUnits R n] : Type u_1

The matrix ring Matrix (Fin n) (Fin n) (e₀₀ R e₀₀).

Equations

• LeanPool.ArtinWedderburn.matrixCorner R = Matrix (Fin n) (Fin n) ↥(LeanPool.ArtinWedderburn.e00Cornerring R)

def LeanPool.ArtinWedderburn.ringToMatrixRing (R : Type u_1) [Ring R] (n : ℕ) (hn : 0 < n) (mu : hasMatrixUnits R n) : R → Matrix (Fin n) (Fin n) ↥(e00Cornerring R)

The map sending a : R to the matrix with entries e₀ᵢ * a * eⱼ₀.

Equations

• LeanPool.ArtinWedderburn.ringToMatrixRing R n hn mu a i j = LeanPool.ArtinWedderburn.ijCorner R i j a

theorem LeanPool.ArtinWedderburn.ring_to_matrix_ring_additive (R : Type u_1) [Ring R] {n : ℕ} {hn : 0 < n} [mu : hasMatrixUnits R n] (a b : R) : ringToMatrixRing R n hn mu (a + b) = ringToMatrixRing R n hn mu a + ringToMatrixRing R n hn mu b

theorem LeanPool.ArtinWedderburn.matrixunit_iz_zi_eq_ii (R : Type u_1) [Ring R] {n : ℕ} {hn : 0 < n} [mu : hasMatrixUnits R n] (i : Fin n) : hasMatrixUnits.es i i = hasMatrixUnits.es i ⟨0, hn⟩ * hasMatrixUnits.es ⟨0, hn⟩ i

theorem LeanPool.ArtinWedderburn.one_eq_sum_es_00e_00e (R : Type u_1) [Ring R] (n : ℕ) (hn : 0 < n) (mu : hasMatrixUnits R n) : 1 = ∑ i : Fin n, hasMatrixUnits.es i ⟨0, hn⟩ * hasMatrixUnits.es ⟨0, hn⟩ i

theorem LeanPool.ArtinWedderburn.ring_to_matrix_ring_multiplicative (R : Type u_1) [Ring R] {n : ℕ} {hn : 0 < n} [mu : hasMatrixUnits R n] (a b : R) : ringToMatrixRing R n hn mu (a * b) = ringToMatrixRing R n hn mu a * ringToMatrixRing R n hn mu b

theorem LeanPool.ArtinWedderburn.matrix_one {n : ℕ} (S : Type u_2) [One S] [Zero S] [DecidableEq (Fin n)] : 1 = fun (i j : Fin n) => if i = j then 1 else 0

theorem LeanPool.ArtinWedderburn.corner_matrix_zero_equiv (R : Type u_1) [Ring R] {n : ℕ} [mu : hasMatrixUnits R n] (a : R) : (∀ (i j : Fin n), hasMatrixUnits.es i i * a * hasMatrixUnits.es j j = 0) ↔ a = 0

theorem LeanPool.ArtinWedderburn.corner_matrix_zero_crit (R : Type u_1) [Ring R] {n : ℕ} {hn : 0 < n} [mu : hasMatrixUnits R n] (a : R) : (∀ (i j : Fin n), ijCorner R i j a = 0) → a = 0

def LeanPool.ArtinWedderburn.ringToMatrixRingHom (R : Type u_1) [Ring R] {n : ℕ} {hn : 0 < n} [mu : hasMatrixUnits R n] : R →+* Matrix (Fin n) (Fin n) ↥(e00Cornerring R)

The ring homomorphism from R to the matrix ring over its e₀₀ corner ring.

Equations

• LeanPool.ArtinWedderburn.ringToMatrixRingHom R = { toFun := LeanPool.ArtinWedderburn.ringToMatrixRing R n hn mu, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

def LeanPool.ArtinWedderburn.matrixToRing (R : Type u_1) [Ring R] (n : ℕ) (hn : 0 < n) (mu : hasMatrixUnits R n) : Matrix (Fin n) (Fin n) ↥(e00Cornerring R) → R

Reassemble a ring element from its matrix of corner components by summing eᵢ₀ * M i j * e₀ⱼ.

Equations

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

theorem LeanPool.ArtinWedderburn.e0k_left_mul_sum (R : Type u_1) [Ring R] {n : ℕ} {hn : 0 < n} [mu : hasMatrixUnits R n] {k : Fin n} {f : Fin n → R} : hasMatrixUnits.es ⟨0, hn⟩ k * ∑ i : Fin n, hasMatrixUnits.es i ⟨0, hn⟩ * f i = hasMatrixUnits.es ⟨0, hn⟩ ⟨0, hn⟩ * f k

theorem LeanPool.ArtinWedderburn.right_mul_sum_e0k (R : Type u_1) [Ring R] {n : ℕ} {hn : 0 < n} [mu : hasMatrixUnits R n] {k : Fin n} {f : Fin n → R} : (∑ i : Fin n, f i * hasMatrixUnits.es ⟨0, hn⟩ i) * hasMatrixUnits.es k ⟨0, hn⟩ = f k * hasMatrixUnits.es ⟨0, hn⟩ ⟨0, hn⟩

theorem LeanPool.ArtinWedderburn.matrixcorner1 (R : Type u_1) [Ring R] {n : ℕ} {hn : 0 < n} [mu : hasMatrixUnits R n] : 1 = fun (i j : Fin n) => if i = j then 1 else 0

theorem LeanPool.ArtinWedderburn.e00_unit (R : Type u_1) [Ring R] {n : ℕ} {hn : 0 < n} [mu : hasMatrixUnits R n] (a : ↥(e00Cornerring R)) : hasMatrixUnits.es ⟨0, hn⟩ ⟨0, hn⟩ * ↑a = ↑a

theorem LeanPool.ArtinWedderburn.unit_e00 (R : Type u_1) [Ring R] {n : ℕ} {hn : 0 < n} [mu : hasMatrixUnits R n] (a : ↥(e00Cornerring R)) : ↑a * hasMatrixUnits.es ⟨0, hn⟩ ⟨0, hn⟩ = ↑a

noncomputable def LeanPool.ArtinWedderburn.ringToMatrixIso (R : Type u_1) [Ring R] {n : ℕ} {hn : 0 < n} [mu : hasMatrixUnits R n] : R ≃+* Matrix (Fin n) (Fin n) ↥(e00Cornerring R)

A ring with matrix units eᵢⱼ is ring-isomorphic to the matrix ring over the corner ring of e₀₀.

Equations

• LeanPool.ArtinWedderburn.ringToMatrixIso R = RingEquiv.ofBijective (LeanPool.ArtinWedderburn.ringToMatrixRingHom R) ⋯

noncomputable def LeanPool.ArtinWedderburn.ringWithMatrixUnitsIsomorphicToMatrixRing (R : Type u_1) [Ring R] (n : ℕ) (hn : 0 < n) (mu : hasMatrixUnits R n) : R ≃+* Matrix (Fin n) (Fin n) ↥(e00Cornerring R)

Lemma 2.17: a ring with matrix units is ring-isomorphic to the matrix ring over the corner ring of e₀₀.

Equations

• LeanPool.ArtinWedderburn.ringWithMatrixUnitsIsomorphicToMatrixRing R n hn mu = LeanPool.ArtinWedderburn.ringToMatrixIso R

@[reducible]

noncomputable def LeanPool.ArtinWedderburn.HasMatrixUnitsToHasMatrixUnits (R : Type u_1) [Ring R] {n : ℕ} (mu : HasMatrixUnits R n) : hasMatrixUnits R n

Convert a proof of HasMatrixUnits (a Prop) into a hasMatrixUnits instance (a class) via choice.

Equations

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