Basic Properties of Simple rings #
A ring R is simple if it has only two two-sided ideals, namely ⊥ and ⊤.
Main results #
IsSimpleRing.instNontrivial: simple rings are non-trivial.DivisionRing.isSimpleRing: division rings are simple.RingHom.injective: every ring homomorphism from a simple ring to a nontrivial ring is injective.IsSimpleRing.iff_injective_ringHom: a ring is simple iff every ring homomorphism to a nontrivial ring is injective.
@[instance 200]
theorem IsSimpleRing.one_mem_of_ne_bot {A : Type u_2} [NonAssocRing A] [IsSimpleRing A] (I : TwoSidedIdeal A) (hI : I ≠ ⊥) :
theorem IsSimpleRing.one_mem_of_ne_zero_mem {A : Type u_2} [NonAssocRing A] [IsSimpleRing A] (I : TwoSidedIdeal A) {x : A} (hx : x ≠ 0) (hxI : x ∈ I) :
theorem IsSimpleRing.of_eq_bot_or_eq_top {R : Type u_1} [NonUnitalNonAssocRing R] [Nontrivial R] (h : ∀ (I : TwoSidedIdeal R), I = ⊥ ∨ I = ⊤) :
theorem IsSimpleRing.injective_ringHom_or_subsingleton_codomain {R : Type u_2} {S : Type u_3} [NonAssocRing R] [IsSimpleRing R] [NonAssocSemiring S] (f : R →+* S) :
theorem RingHom.injective {R : Type u_2} {S : Type u_3} [NonAssocRing R] [IsSimpleRing R] [NonAssocSemiring S] [Nontrivial S] (f : R →+* S) :
theorem IsSimpleRing.iff_injective_ringHom_or_subsingleton_codomain (R : Type u) [NonAssocRing R] [Nontrivial R] :
IsSimpleRing R ↔ ∀ {S : Type u} [inst : NonAssocSemiring S] (f : R →+* S), Function.Injective ⇑f ∨ Subsingleton S
theorem IsSimpleRing.iff_injective_ringHom (R : Type u) [NonAssocRing R] [Nontrivial R] :
IsSimpleRing R ↔ ∀ {S : Type u} [inst : NonAssocSemiring S] [Nontrivial S] (f : R →+* S), Function.Injective ⇑f