Minimal left ideals and idempotents

For a minimal (atom) left ideal I with I * I ≠ 0, this file extracts an idempotent generator e of I and shows that the corner subring eRe is a division subring.

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

The set I * a = {x * a | x ∈ I} as a subset of R.

Equations

• LeanPool.ArtinWedderburn.subIdealSet I a = {r : R | ∃ x ∈ I, r = x * a}

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

The left ideal I * a consisting of elements x * a for x ∈ I.

Equations

• LeanPool.ArtinWedderburn.subIdeal I a = { carrier := LeanPool.ArtinWedderburn.subIdealSet I a, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem LeanPool.ArtinWedderburn.sub_ideal_le_ideal {R : Type u_1} [Ring R] (I : Ideal R) (a : R) (h : a ∈ I) : subIdeal I a ≤ I

theorem LeanPool.ArtinWedderburn.mul_ne_zero_imply_set_ne_zero {R : Type u_1} [Ring R] (I J : Ideal R) (h : I * J ≠ ⊥) : ∃ x ∈ I, ∃ y ∈ J, x * y ≠ 0

theorem LeanPool.ArtinWedderburn.ideal_sq_ne_bot_imply_subideal_ne_bot {R : Type u_1} [Ring R] (I : Ideal R) (h : I * I ≠ ⊥) : ∃ y ∈ I, subIdeal I y ≠ ⊥

theorem LeanPool.ArtinWedderburn.ideal_sq_ne_bot_imply_subideal_ne_bot2 {R : Type u_1} [Ring R] (I : Ideal R) (h : I * I ≠ ⊥) : ∃ y ∈ I, y ≠ 0 ∧ subIdeal I y ≠ ⊥

theorem LeanPool.ArtinWedderburn.le_and_not_lt_eq {R : Type u_1} [Ring R] (I J : Ideal R) (h1 : I ≤ J) (h2 : ¬I < J) : I = J

theorem LeanPool.ArtinWedderburn.minimal_ideal_I_sq_nonzero_exists_el {R : Type u_1} [Ring R] (I : Ideal R) (hI : IsAtom I) (hII : I * I ≠ ⊥) : ∃ y ∈ I, subIdeal I y = I

theorem LeanPool.ArtinWedderburn.minimal_ideal_I_sq_nonzero_exists_el2 {R : Type u_1} [Ring R] (I : Ideal R) (hI : IsAtom I) (hII : I * I ≠ ⊥) : ∃ y ∈ I, y ≠ 0 ∧ subIdeal I y = I

theorem LeanPool.ArtinWedderburn.minimal_ideal_I_sq_nonzero_exists_els2 {R : Type u_1} [Ring R] (I : Ideal R) (hI : IsAtom I) (hII : I * I ≠ ⊥) : ∃ y ∈ I, y ≠ 0 ∧ subIdeal I y = I ∧ ∃ e ∈ I, e ≠ 0 ∧ y = e * y

theorem LeanPool.ArtinWedderburn.minimal_ideal_I_sq_nonzero_exists_els {R : Type u_1} [Ring R] (I : Ideal R) (hI : IsAtom I) (hII : I * I ≠ ⊥) : ∃ y ∈ I, subIdeal I y = I ∧ ∃ e ∈ I, y = e * y

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

The left ideal of elements in I that annihilate a on the right.

Equations

• LeanPool.ArtinWedderburn.elemAnn I a = { carrier := {x : R | x ∈ I ∧ x * a = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem LeanPool.ArtinWedderburn.elem_ann_le_ideal {R : Type u_1} [Ring R] (I : Ideal R) (a : R) : elemAnn I a ≤ I

theorem LeanPool.ArtinWedderburn.e_semiidem {R : Type u_1} [Ring R] (I : Ideal R) (e y : R) (he : e ∈ I) (h : e * y = y) : e * e - e ∈ elemAnn I y

theorem LeanPool.ArtinWedderburn.strict_contain {R : Type u_1} [Ring R] (I J : Ideal R) (hleq : I ≤ J) (hneq : ∃ x ∈ J, x ∉ I) : I < J

theorem LeanPool.ArtinWedderburn.ideal_neq_bot_if_has_nonzero_el {R : Type u_1} [Ring R] (I : Ideal R) (h : ∃ x ∈ I, x ≠ 0) : I ≠ ⊥

theorem LeanPool.ArtinWedderburn.nonzero_ideal_in_min_ideal {R : Type u_1} [Ring R] (I J : Ideal R) (atom_I : IsAtom I) (Jnz : J ≠ ⊥) (hJsubI : J ≤ I) : J = I

theorem LeanPool.ArtinWedderburn.minimal_ideal_I_sq_nonzero_exists_idem {R : Type u_1} [Ring R] (I : Ideal R) (h_atom_I : IsAtom I) (hII : I * I ≠ ⊥) : ∃ e ∈ I, e ≠ 0 ∧ IsIdempotentElem e ∧ Ideal.span {e} = I

theorem LeanPool.ArtinWedderburn.corner_ring_div {R : Type u_1} [Ring R] (I : Ideal R) (h_atom_I : IsAtom I) (e : R) (e_in_I : e ∈ I) (henz : e ≠ 0) (he_idem : IsIdempotentElem e) : IsDivisionSubring (CornerSubringNonUnital e) e

theorem LeanPool.ArtinWedderburn.minimal_ideal_I_sq_nonzero_exists_idem_and_div {R : Type u_1} [Ring R] (I : Ideal R) (h_atom_I : IsAtom I) (hII : I * I ≠ ⊥) : ∃ e ∈ I, e ≠ 0 ∧ IsIdempotentElem e ∧ Ideal.span {e} = I ∧ IsDivisionSubring (CornerSubringNonUnital e) e