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.
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)
:
Function.Injective โf โจ Subsingleton S
theorem
RingHom.injective
{R : Type u_2}
{S : Type u_3}
[NonAssocRing R]
[IsSimpleRing R]
[NonAssocSemiring S]
[Nontrivial S]
(f : R โ+* S)
:
Function.Injective โf
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