Orthogonal idempotents and matrix units

Develops orthogonal idempotents, builds matrix units from a system of pairwise orthogonal idempotents whose corner rings are division rings, and packages the data as OrtIdem / OrtIdemDiv structures.

def LeanPool.ArtinWedderburn.IsOrthogonal {R : Type u_1} [Ring R] (e f : R) : Prop

Two elements are orthogonal when their products in both orders vanish.

Equations

• LeanPool.ArtinWedderburn.IsOrthogonal e f = (e * f = 0 ∧ f * e = 0)

def LeanPool.ArtinWedderburn.AreOrthogonalIdempotents {R : Type u_1} [Ring R] (e f : R) : Prop

e and f are orthogonal idempotents when each is idempotent and they are orthogonal.

Equations

• LeanPool.ArtinWedderburn.AreOrthogonalIdempotents e f = (IsIdempotentElem e ∧ IsIdempotentElem f ∧ LeanPool.ArtinWedderburn.IsOrthogonal e f)

theorem LeanPool.ArtinWedderburn.leq_neq_lt {R : Type u_1} [Ring R] (I J : Ideal R) : I ≤ J → I ≠ J → I < J

theorem LeanPool.ArtinWedderburn.one_sub_e_larger_span_on_sub_e_sub_f {R : Type u_1} [Ring R] (e f : R) (ef_ort_idem : AreOrthogonalIdempotents e f) (fnz : f ≠ 0) : Ideal.span {1 - e - f} < Ideal.span {1 - e}

theorem LeanPool.ArtinWedderburn.e_span_larger_e_sub_f {R : Type u_1} [Ring R] (e f : R) (h : AreOrthogonalIdempotents (1 - e) f) (fnz : f ≠ 0) : Ideal.span {e - f} < Ideal.span {e}

def LeanPool.ArtinWedderburn.HasMatrixUnits (R : Type u_2) [Ring R] (n : ℕ) : Prop

R has a system of n × n matrix units when there exist n^2 elements es i j summing to 1 on the diagonal and multiplying like matrix units.

Equations

• LeanPool.ArtinWedderburn.HasMatrixUnits R n = ∃ (es : Fin n → Fin n → R), ∑ i : Fin n, es i i = 1 ∧ ∀ (i j k l : Fin n), es i j * es k l = if j = k then es i l else 0

def LeanPool.ArtinWedderburn.kroneckerDelta {R : Type u_1} [Ring R] (n : ℕ) (i j : Fin n) : R

Kronecker delta valued in R: equal to 1 when i = j and 0 otherwise.

Equations

• LeanPool.ArtinWedderburn.kroneckerDelta n i j = if i = j then 1 else 0

def LeanPool.ArtinWedderburn.PairwiseOrthogonal {R : Type u_1} [Ring R] (a b : R) : Prop

Two elements are pairwise orthogonal when both of their products vanish.

Equations

• LeanPool.ArtinWedderburn.PairwiseOrthogonal a b = (a * b = 0 ∧ b * a = 0)

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) : HasMatrixUnits R n

theorem LeanPool.ArtinWedderburn.eRf_nonzero {R : Type u_1} [Ring R] (h : IsPrimeRing R) (e f : R) (he : e ≠ 0) (hf : f ≠ 0) : ∃ (a : R), e * a * f ≠ 0

theorem LeanPool.ArtinWedderburn.both_mul_e_f {R : Type u_1} [Ring R] {e f : R} (idem_e : IsIdempotentElem e) (idem_f : IsIdempotentElem f) (x : R) : x ∈ bothMul e f → e * x = x ∧ x * f = x

theorem LeanPool.ArtinWedderburn.both_mul_add {R : Type u_1} [Ring R] {e f : R} (x y : R) : x ∈ bothMul e f → y ∈ bothMul e f → x + y ∈ bothMul e f

theorem LeanPool.ArtinWedderburn.both_mul_neg {R : Type u_1} [Ring R] {e f : R} (x : R) : x ∈ bothMul e f → -x ∈ bothMul e f

theorem LeanPool.ArtinWedderburn.both_mul_sub {R : Type u_1} [Ring R] {e f : R} (x y : R) : x ∈ bothMul e f → y ∈ bothMul e f → x - y ∈ bothMul e f

theorem LeanPool.ArtinWedderburn.both_mul_mul {R : Type u_1} [Ring R] {e f : R} (x y : R) : x ∈ bothMul e f → y ∈ bothMul f e → x * y ∈ bothMul e e

structure LeanPool.ArtinWedderburn.twoNiceIdempotents {R : Type u_1} [Ring R] (e f : R) : Type u_1

Witnesses for the "nice idempotents" property: elements u ∈ eRf, v ∈ fRe with u * v = e and v * u = f.

• u : R

  The element of eRf whose product with v recovers e.

• v : R

  The element of fRe whose product with u recovers f.

• u_mem : self.u ∈ bothMul e f
• v_mem : self.v ∈ bothMul f e
• u_mul_v : self.u * self.v = e
• v_mul_u : self.v * self.u = f

theorem LeanPool.ArtinWedderburn.lemma_2_19 {R : Type u_1} [Ring R] (h : IsPrimeRing R) (e f : R) (idem_e : IsIdempotentElem e) (idem_f : IsIdempotentElem f) (heRe : IsDivisionRing ↥(CornerSubring idem_e)) (hfRf : IsDivisionRing ↥(CornerSubring idem_f)) : ∃ (u : R) (v : R), u ∈ bothMul e f ∧ v ∈ bothMul f e ∧ u * v = e ∧ v * u = f

noncomputable def LeanPool.ArtinWedderburn.lemma219' {R : Type u_1} [Ring R] (h : IsPrimeRing R) (e f : R) (idem_e : IsIdempotentElem e) (idem_f : IsIdempotentElem f) (heRe : IsDivisionRing ↥(CornerSubring idem_e)) (hfRf : IsDivisionRing ↥(CornerSubring idem_f)) : twoNiceIdempotents e f

Packaging of lemma_2_19 as a twoNiceIdempotents structure.

Equations

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

theorem LeanPool.ArtinWedderburn.f_in_corner_othogonal {R : Type u_1} [Ring R] (e f : R) (idem_e : IsIdempotentElem e) (f_mem : f ∈ bothMul (1 - e) (1 - e)) : IsOrthogonal e f

theorem LeanPool.ArtinWedderburn.e_idem_to_e_val_idem {R : Type u_1} [Ring R] {e : R} {idem_e : IsIdempotentElem e} {x : ↥(CornerSubring idem_e)} (idem_x : IsIdempotentElem x) : IsIdempotentElem ↑x

theorem LeanPool.ArtinWedderburn.sum_orthogonal_idem_is_idem {R : Type u_1} [Ring R] (e f : R) (h : AreOrthogonalIdempotents e f) : IsIdempotentElem (e + f)

theorem LeanPool.ArtinWedderburn.prod_orthogonal_idem_is_idem {R : Type u_1} [Ring R] (e f : R) (_idem_e : IsIdempotentElem e) (idem_f : IsIdempotentElem f) (h : IsOrthogonal e f) : IsIdempotentElem (f * (1 - e))

theorem LeanPool.ArtinWedderburn.e_f_orhogonal_f_1_sub_e_eq_f {R : Type u_1} [Ring R] (e f : R) (h : IsOrthogonal e f) : f * (1 - e) = f

theorem LeanPool.ArtinWedderburn.f_mem_corner_e_e_sub_f_idem {R : Type u_1} [Ring R] (e : R) (idem_e : IsIdempotentElem e) (f : ↥(CornerSubring idem_e)) (idem_f : IsIdempotentElem f) : IsIdempotentElem (e - ↑f)

theorem LeanPool.ArtinWedderburn.ort_comm {R : Type u_1} [Ring R] (e f : R) (ort : IsOrthogonal e f) : IsOrthogonal f e

theorem LeanPool.ArtinWedderburn.orth_coercion {R : Type u_1} [Ring R] (e : R) (idem_e : IsIdempotentElem e) (x y : ↥(CornerSubring idem_e)) (ort : IsOrthogonal x y) : IsOrthogonal ↑x ↑y

theorem LeanPool.ArtinWedderburn.iso_idem_to_idem {R : Type u_1} [Ring R] (R' : Type u_2) [Ring R'] (φ : R ≃+* R') (e : R) (idem_e : IsIdempotentElem e) : IsIdempotentElem (φ e)

theorem LeanPool.ArtinWedderburn.iso_orthogonal_to_orthogonal {R : Type u_1} [Ring R] (R' : Type u_2) [Ring R'] (φ : R ≃+* R') (x y : R) (ort : IsOrthogonal x y) : IsOrthogonal (φ x) (φ y)

theorem LeanPool.ArtinWedderburn.artinian_ring_has_minimal_left_ideal_of_element {R : Type u_1} [Ring R] [IsArtinian R R] [Nontrivial R] : ∃ (I : Ideal R), IsAtom I

theorem LeanPool.ArtinWedderburn.prime_and_artinian_esists_idem_corner_div {R : Type u_1} [Ring R] [Nontrivial R] (h : IsPrimeRing R) (h' : IsArtinian R R) : ∃ (e : R), e ≠ 0 ∧ IsIdempotentElem e ∧ IsDivisionSubring (CornerSubringNonUnital e) e

structure LeanPool.ArtinWedderburn.OrtIdem (R : Type u_2) [Ring R] : Type u_2

A finite system of pairwise orthogonal idempotents of R summing to 1.

• n : ℕ

  Number of idempotents in the system.

• f : Fin self.n → R

  The idempotents indexed by Fin n.

• h (i : Fin self.n) : IsIdempotentElem (self.f i)
• sum_one : ∑ i : Fin self.n, self.f i = 1
• orthogonal (i j : Fin self.n) : i ≠ j → IsOrthogonal (self.f i) (self.f j)

structure LeanPool.ArtinWedderburn.OrtIdemDiv (R : Type u_2) [Ring R] extends LeanPool.ArtinWedderburn.OrtIdem R : Type u_2

An OrtIdem whose corner rings are all division rings.

• n : ℕ
• f : Fin self.n → R
• h (i : Fin self.n) : IsIdempotentElem (self.f i)
• sum_one : ∑ i : Fin self.n, self.f i = 1
• orthogonal (i j : Fin self.n) : i ≠ j → IsOrthogonal (self.f i) (self.f j)
• div (i : Fin self.n) : IsDivisionRing ↥(CornerSubring ⋯)

def LeanPool.ArtinWedderburn.isomorphicOrtIdem {R : Type u_1} [Ring R] (R' : Type u_2) [Ring R'] (φ : R ≃+* R') (hoi : OrtIdem R) : OrtIdem R'

Transport an OrtIdem R along a ring isomorphism φ : R ≃+* R'.

Equations

• LeanPool.ArtinWedderburn.isomorphicOrtIdem R' φ hoi = { n := hoi.n, f := fun (i : Fin hoi.n) => φ (hoi.f i), h := ⋯, sum_one := ⋯, orthogonal := ⋯ }

def LeanPool.ArtinWedderburn.ringIsoToCornerIso {R : Type u_1} [Ring R] (R' : Type u_2) [Ring R'] (φ : R ≃+* R') (e : R) (idem_e : IsIdempotentElem e) : ↥(CornerSubring idem_e) ≃+* ↥(CornerSubring ⋯)

A ring isomorphism φ : R ≃+* R' induces a ring isomorphism between the corner rings of an idempotent and of its image under φ.

Equations

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

def LeanPool.ArtinWedderburn.isomorphicOrtIdemDiv {R : Type u_1} [Ring R] {R' : Type u_2} [Ring R'] (φ : R ≃+* R') (hoi : OrtIdemDiv R) : OrtIdemDiv R'

Transport an OrtIdemDiv R along a ring isomorphism φ : R ≃+* R'.

Equations

• LeanPool.ArtinWedderburn.isomorphicOrtIdemDiv φ hoi = { toOrtIdem := LeanPool.ArtinWedderburn.isomorphicOrtIdem R' φ hoi.toOrtIdem, div := ⋯ }