Basic Properties of Simple rings #
A ring R is simple if it has only two two-sided ideals, namely ⊥ and ⊤.
Main results #
IsSimpleRing.nontrivial: 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
IsSimpleRing.instIsSimpleOrderTwoSidedIdeal
{R : Type u_1}
[NonUnitalNonAssocRing R]
[IsSimpleRing R]
:
instance
IsSimpleRing.instNontrivial
{R : Type u_1}
[NonUnitalNonAssocRing R]
[simple : IsSimpleRing R]
:
theorem
IsSimpleRing.one_mem_of_ne_bot
{A : Type u_2}
[NonAssocRing A]
[IsSimpleRing A]
(I : TwoSidedIdeal A)
(hI : I ≠ ⊥)
:
1 ∈ 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)
:
1 ∈ 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] [inst_1 : Nontrivial S] (f : R →+* S), Function.Injective ⇑f