Nice ideals and the induction step in Artin–Wedderburn

A nice ideal is an idempotent ideal whose corner ring is OrtIdemDiv. We prove that in a prime artinian ring, every ideal is nice.

def LeanPool.ArtinWedderburn.IdemIdeal {R : Type u_1} [Ring R] (I : Ideal R) : Prop

An ideal is idempotent-generated when it is the (left) span of a single idempotent.

Equations

• LeanPool.ArtinWedderburn.IdemIdeal I = ∃ (e : R), IsIdempotentElem e ∧ I = Ideal.span {e}

def LeanPool.ArtinWedderburn.NiceIdeal {R : Type u_1} [Ring R] (I : Ideal R) : Type u_1

An ideal is nice when, whenever it is generated by an idempotent e, the corner ring eRe admits an OrtIdemDiv decomposition.

Equations

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

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

def LeanPool.ArtinWedderburn.zeroIdealNice {R : Type u_1} [Ring R] : NiceIdeal ⊥

The zero ideal is a nice ideal.

Equations

• LeanPool.ArtinWedderburn.zeroIdealNice a✝ e idem_e h = { n := 0, f := fun (x : Fin 0) => 0, h := ⋯, sum_one := ⋯, orthogonal := ⋯, div := ⋯ }

def LeanPool.ArtinWedderburn.idempotents {α : Type u_2} {n : ℕ} (x : α) (h : Fin n → α) : Fin (n + 1) → α

Extend a list of n elements with an extra entry x in front, yielding n + 1 elements.

Equations

• LeanPool.ArtinWedderburn.idempotents x h i = Fin.cases x h i

theorem LeanPool.ArtinWedderburn.idempotents_first {α : Type u_2} {n : ℕ} (x : α) (h : Fin n → α) : idempotents x h 0 = x

theorem LeanPool.ArtinWedderburn.idempotents_rest {α : Type u_2} {n : ℕ} (x : α) (h : Fin n → α) (i : Fin n) : idempotents x h i.succ = h i

theorem LeanPool.ArtinWedderburn.extend_idempotents {R : Type u_1} [Ring R] {n : ℕ} (f : R) (idem_f : IsIdempotentElem f) (es : Fin n → R) (h : ∀ (i : Fin n), IsIdempotentElem (es i)) (i : Fin (n + 1)) : IsIdempotentElem (idempotents f es i)

theorem LeanPool.ArtinWedderburn.i_nonzero_succ {n : ℕ} (i : Fin (n + 1)) (i_nonzero : i ≠ 0) : ∃ (k : Fin n), i = k.succ

theorem LeanPool.ArtinWedderburn.bot_eq_span_zero {R : Type u_1} [Ring R] (I : Ideal R) (e : R) (h_bot : I ≠ ⊥) (h_span : I = Ideal.span {e}) : e ≠ 0

def LeanPool.ArtinWedderburn.extensionOfOrtIdem {R : Type u_1} [Ring R] (e : R) (idem_e : IsIdempotentElem e) (oi : OrtIdem ↥(CornerSubring ⋯)) : OrtIdem R

Prepend the idempotent e to an OrtIdem system on the corner ring of 1 - e to obtain an OrtIdem R.

Equations

• LeanPool.ArtinWedderburn.extensionOfOrtIdem e idem_e oi = { n := oi.n + 1, f := LeanPool.ArtinWedderburn.idempotents e fun (i : Fin oi.n) => ↑(oi.f i), h := ⋯, sum_one := ⋯, orthogonal := ⋯ }

def LeanPool.ArtinWedderburn.extensionOfOrtIdemDiv {R : Type u_1} [Ring R] (e : R) (idem_e : IsIdempotentElem e) (div_e : IsDivisionRing ↥(CornerSubring idem_e)) (oid : OrtIdemDiv ↥(CornerSubring ⋯)) : OrtIdemDiv R

Combine the idempotent e (with division corner) with an OrtIdemDiv system on the corner ring of 1 - e to obtain an OrtIdemDiv R.

Equations

• LeanPool.ArtinWedderburn.extensionOfOrtIdemDiv e idem_e div_e oid = { toOrtIdem := LeanPool.ArtinWedderburn.extensionOfOrtIdem e idem_e oid.toOrtIdem, div := ⋯ }

noncomputable def LeanPool.ArtinWedderburn.subidealsNiceIdealNice {R : Type u_1} [Ring R] (h_prime : IsPrimeRing R) (h_art : IsArtinian R R) (I : Ideal R) (hi : (J : Ideal R) → J < I → NiceIdeal J) : NiceIdeal I

Induction step of Artin–Wedderburn: if every proper subideal of I is nice, then I itself is nice.

Equations

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

noncomputable def LeanPool.ArtinWedderburn.accIdealNice {R : Type u_1} [Ring R] (h_prime : IsPrimeRing R) (h_art : IsArtinian R R) (I : Ideal R) (h_acc : Acc (fun (x y : Ideal R) => x < y) I) : NiceIdeal I

Well-founded induction along < lifting subidealsNiceIdealNice: every accessible ideal in a prime artinian ring is nice.

Equations

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