Prime rings

Defines IsPrimeRing R (the ideal product version) and proves equivalence to the elementwise version aRb = 0 → a = 0 ∨ b = 0 and to the two-sided ideal version. Concludes that simple rings are prime.

def LeanPool.ArtinWedderburn.IsPrimeRing (R : Type u_2) [Ring R] : Prop

A ring is prime when the product of two left ideals can be zero only if at least one of the factors is zero.

Equations

• LeanPool.ArtinWedderburn.IsPrimeRing R = ∀ (I J : Ideal R), I * J = ⊥ → I = ⊥ ∨ J = ⊥

theorem LeanPool.ArtinWedderburn.prime_ring_equiv {R : Type u_1} [Ring R] : IsPrimeRing R ↔ ∀ (a b : R), bothMul a b = {0} → a = 0 ∨ b = 0

theorem LeanPool.ArtinWedderburn.span_le_two_sided_span {R : Type u_1} [Ring R] (S : Set R) : Ideal.span S ≤ TwoSidedIdeal.asIdeal (TwoSidedIdeal.span S)

theorem LeanPool.ArtinWedderburn.two_sided_ideal_equality {R : Type u_1} [Ring R] (I J : TwoSidedIdeal R) : I = J ↔ ↑I = ↑J

theorem LeanPool.ArtinWedderburn.ideal_equality {R : Type u_1} [Ring R] (I J : Ideal R) : I = J ↔ ↑I = ↑J

theorem LeanPool.ArtinWedderburn.equal_sets {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) : ↑(TwoSidedIdeal.asIdeal I) = ↑I

theorem LeanPool.ArtinWedderburn.ideal_eq_to_two_sided_ideal_eq {R : Type u_1} [Ring R] (I J : TwoSidedIdeal R) : I = J ↔ TwoSidedIdeal.asIdeal I = TwoSidedIdeal.asIdeal J

theorem LeanPool.ArtinWedderburn.two_sided_bot_iff_set_zero {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) : I = ⊥ ↔ ↑I = {0}

theorem LeanPool.ArtinWedderburn.ideal_bot_iff_set_zero {R : Type u_1} [Ring R] (I : Ideal R) : I = ⊥ ↔ ↑I = {0}

theorem LeanPool.ArtinWedderburn.ideal_bot {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) : I = ⊥ ↔ TwoSidedIdeal.asIdeal I = ⊥

theorem LeanPool.ArtinWedderburn.ideal_span_sub_two_sided_ideal_span {R : Type u_1} [Ring R] (S : Set R) : Ideal.span S ≤ TwoSidedIdeal.asIdeal (TwoSidedIdeal.span S)

theorem LeanPool.ArtinWedderburn.same_prod {R : Type u_1} [Ring R] (I J : TwoSidedIdeal R) : I * J = ⊥ → TwoSidedIdeal.asIdeal I * TwoSidedIdeal.asIdeal J = ⊥

theorem LeanPool.ArtinWedderburn.prime_ring_implies_prime_by_two_sided {R : Type u_1} [Ring R] : IsPrimeRing R → ∀ (I J : TwoSidedIdeal R), I * J = ⊥ → I = ⊥ ∨ J = ⊥

theorem LeanPool.ArtinWedderburn.two_sided_span_bot_el_zero {R : Type u_1} [Ring R] (a : R) : TwoSidedIdeal.span {a} = ⊥ → a = 0

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

The two-sided multiplicative closure RaR = {y * a * z | y, z : R} of a.

Equations

• LeanPool.ArtinWedderburn.mulClosure a = {x : R | ∃ (y : R) (z : R), x = y * a * z}

theorem LeanPool.ArtinWedderburn.mul_closure_left {R : Type u_1} [Ring R] (a x y : R) : y ∈ mulClosure a → x * y ∈ mulClosure a

theorem LeanPool.ArtinWedderburn.mul_closure_right {R : Type u_1} [Ring R] (a y x : R) : y ∈ mulClosure a → y * x ∈ mulClosure a

theorem LeanPool.ArtinWedderburn.mul_closure_sub_span {R : Type u_1} [Ring R] (a : R) : mulClosure a ⊆ ↑(TwoSidedIdeal.span {a})

theorem LeanPool.ArtinWedderburn.ideal_mul_closure {R : Type u_1} [Ring R] (a : R) : ↑(AddSubgroup.closure (mulClosure a)) = ↑(TwoSidedIdeal.span (mulClosure a))

theorem LeanPool.ArtinWedderburn.sub_span {R : Type u_1} [Ring R] (s : Set R) (I : TwoSidedIdeal R) : s ⊆ ↑I → TwoSidedIdeal.span s ≤ I

theorem LeanPool.ArtinWedderburn.span_mul_closure_eq_span {R : Type u_1} [Ring R] (a : R) : TwoSidedIdeal.span (mulClosure a) = TwoSidedIdeal.span {a}

theorem LeanPool.ArtinWedderburn.both_mul_zero {R : Type u_1} [Ring R] {a b x y : R} (hab : bothMul a b = {0}) (hx : x ∈ mulClosure a) (hy : y ∈ mulClosure b) : x * y = 0

theorem LeanPool.ArtinWedderburn.span_mul_closure_bot_forall {R : Type u_1} [Ring R] {a b x y : R} (hab : bothMul a b = {0}) (hx : x ∈ AddSubgroup.closure (mulClosure a)) (hy : y ∈ mulClosure b) : x * y = 0

theorem LeanPool.ArtinWedderburn.span_mul_closure_bot_forall' {R : Type u_1} [Ring R] {a b x y : R} (hab : bothMul a b = {0}) (hx : x ∈ TwoSidedIdeal.span {a}) (hy : y ∈ mulClosure b) : x * y = 0

theorem LeanPool.ArtinWedderburn.span_mul_closure_bot {R : Type u_1} [Ring R] (a b : R) (hab : bothMul a b = {0}) : ↑(TwoSidedIdeal.span {a}) * mulClosure b = {0}

theorem LeanPool.ArtinWedderburn.two_sided_span_bot_forall {R : Type u_1} [Ring R] {a b x y : R} (hab : bothMul a b = {0}) (hx : x ∈ TwoSidedIdeal.span {a}) (hy : y ∈ AddSubgroup.closure (mulClosure b)) : x * y = 0

theorem LeanPool.ArtinWedderburn.span_mul_span_bot' {R : Type u_1} [Ring R] (a b : R) (hab : bothMul a b = {0}) : ↑(TwoSidedIdeal.span {a}) * ↑(AddSubgroup.closure (mulClosure b)) = {0}

theorem LeanPool.ArtinWedderburn.span_mul_span_bot {R : Type u_1} [Ring R] (a b : R) (hab : bothMul a b = {0}) : ↑(TwoSidedIdeal.span {a}) * ↑(TwoSidedIdeal.span {b}) = {0}

theorem LeanPool.ArtinWedderburn.bothmul_zero_implies_prod_zero {R : Type u_1} [Ring R] (a b : R) : bothMul a b = {0} → TwoSidedIdeal.span {a} * TwoSidedIdeal.span {b} = ⊥

theorem LeanPool.ArtinWedderburn.prime_for_two_sided_implies_condition2 {R : Type u_1} [Ring R] : (∀ (I J : TwoSidedIdeal R), I * J = ⊥ → I = ⊥ ∨ J = ⊥) → ∀ (a b : R), bothMul a b = {0} → a = 0 ∨ b = 0

theorem LeanPool.ArtinWedderburn.prime_ring_equiv' {R : Type u_1} [Ring R] : IsPrimeRing R ↔ ∀ (I J : TwoSidedIdeal R), I * J = ⊥ → I = ⊥ ∨ J = ⊥

theorem LeanPool.ArtinWedderburn.simple_ring_is_prime {R : Type u_1} [Ring R] [IsSimpleRing R] : IsPrimeRing R