doc-next-gen

Mathlib.RingTheory.SimpleRing.Basic

Module docstring

{"# 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.

"}

IsSimpleRing.one_mem_of_ne_bot theorem
{A : Type*} [NonAssocRing A] [IsSimpleRing A] (I : TwoSidedIdeal A) (hI : I ≠ ⊥) : (1 : A) ∈ I
Full source 
lemma one_mem_of_ne_bot {A : Type*} [NonAssocRing A] [IsSimpleRing A] (I : TwoSidedIdeal A)
    (hI : I ≠ ⊥) : (1 : A) ∈ I :=
  (eq_bot_or_eq_top I).resolve_left hI ▸ ⟨⟩
Inclusion of Unity in Nonzero Ideal of Simple Ring
Informal description
Let $A$ be a simple non-associative ring and $I$ be a two-sided ideal of $A$. If $I$ is not the zero ideal, then the multiplicative identity $1$ belongs to $I$.
IsSimpleRing.one_mem_of_ne_zero_mem theorem
{A : Type*} [NonAssocRing A] [IsSimpleRing A] (I : TwoSidedIdeal A) {x : A} (hx : x ≠ 0) (hxI : x ∈ I) : (1 : A) ∈ I
Full source 
lemma one_mem_of_ne_zero_mem {A : Type*} [NonAssocRing A] [IsSimpleRing A] (I : TwoSidedIdeal A)
    {x : A} (hx : x ≠ 0) (hxI : x ∈ I) : (1 : A) ∈ I :=
  one_mem_of_ne_bot I (by rintro rfl; exact hx hxI)
Nonzero Element in Ideal Implies Unity in Simple Ring
Informal description
Let $A$ be a simple non-associative ring and $I$ be a two-sided ideal of $A$. If there exists a nonzero element $x \in I$ (i.e., $x \neq 0$), then the multiplicative identity $1$ belongs to $I$.
IsSimpleRing.of_eq_bot_or_eq_top theorem
[Nontrivial R] (h : ∀ I : TwoSidedIdeal R, I = ⊥ ∨ I = ⊤) : IsSimpleRing R
Full source 
lemma of_eq_bot_or_eq_top [Nontrivial R] (h : ∀ I : TwoSidedIdeal R, I = ⊥ ∨ I = ⊤) :
    IsSimpleRing R where
  simple.eq_bot_or_eq_top := h
Characterization of Simple Rings via Ideals
Informal description
Let $R$ be a nontrivial ring. If every two-sided ideal $I$ of $R$ is either the zero ideal $\{0\}$ or the entire ring $R$ itself, then $R$ is a simple ring.
DivisionRing.isSimpleRing instance
(A : Type*) [DivisionRing A] : IsSimpleRing A
Full source 
instance _root_.DivisionRing.isSimpleRing (A : Type*) [DivisionRing A] : IsSimpleRing A :=
  .of_eq_bot_or_eq_top <| fun I ↦ by
    rw [or_iff_not_imp_left, ← I.one_mem_iff]
    intro H
    obtain ⟨x, hx1, hx2 : x ≠ 0⟩ := SetLike.exists_of_lt (bot_lt_iff_ne_bot.mpr H : ⊥ < I)
    simpa [inv_mul_cancel₀ hx2] using I.mul_mem_left x⁻¹ _ hx1
Division Rings are Simple Rings
Informal description
Every division ring $A$ is a simple ring.
IsSimpleRing.injective_ringHom_or_subsingleton_codomain theorem
{R S : Type*} [NonAssocRing R] [IsSimpleRing R] [NonAssocSemiring S] (f : R →+* S) : Function.Injective f ∨ Subsingleton S
Full source 
lemma injective_ringHom_or_subsingleton_codomain
    {R S : Type*} [NonAssocRing R] [IsSimpleRing R] [NonAssocSemiring S]
    (f : R →+* S) : Function.InjectiveFunction.Injective f ∨ Subsingleton S :=
  simple.eq_bot_or_eq_top (TwoSidedIdeal.ker f) |>.imp (TwoSidedIdeal.ker_eq_bot _ |>.1)
    (fun h => subsingleton_iff_zero_eq_one.1 <| by
      have mem : 1 ∈ TwoSidedIdeal.ker f := h.symm ▸ TwoSidedIdeal.mem_top _
      rwa [TwoSidedIdeal.mem_ker, map_one, eq_comm] at mem)
Injective Homomorphism or Codomain Trivial for Simple Rings
Informal description
Let $R$ be a simple ring and $S$ be a non-associative semiring. For any ring homomorphism $f \colon R \to S$, either $f$ is injective or $S$ is a subsingleton (i.e., has at most one element).
RingHom.injective theorem
{R S : Type*} [NonAssocRing R] [IsSimpleRing R] [NonAssocSemiring S] [Nontrivial S] (f : R →+* S) : Function.Injective f
Full source 
protected theorem _root_.RingHom.injective
    {R S : Type*} [NonAssocRing R] [IsSimpleRing R] [NonAssocSemiring S] [Nontrivial S]
    (f : R →+* S) : Function.Injective f :=
  injective_ringHom_or_subsingleton_codomain f |>.resolve_right fun r => not_subsingleton _ r
Injectivity of Ring Homomorphisms from Simple Rings to Nontrivial Semirings
Informal description
Let $R$ be a simple ring and $S$ be a nontrivial non-associative semiring. Then every ring homomorphism $f \colon R \to S$ is injective.
IsSimpleRing.iff_injective_ringHom_or_subsingleton_codomain theorem
(R : Type u) [NonAssocRing R] [Nontrivial R] : IsSimpleRing R ↔ ∀ {S : Type u} [NonAssocSemiring S] (f : R →+* S), Function.Injective f ∨ Subsingleton S
Full source 
lemma iff_injective_ringHom_or_subsingleton_codomain (R : Type u) [NonAssocRing R] [Nontrivial R] :
    IsSimpleRingIsSimpleRing R ↔
    ∀ {S : Type u} [NonAssocSemiring S] (f : R →+* S), Function.Injective f ∨ Subsingleton S where
  mp _ _ _ := injective_ringHom_or_subsingleton_codomain
  mpr H := of_eq_bot_or_eq_top fun I => H I.ringCon.mk' |>.imp
    (fun h => le_antisymm
      (fun _ hx => TwoSidedIdeal.ker_eq_bot _ |>.2 h ▸ I.ker_ringCon_mk'.symm ▸ hx) bot_le)
    (fun h => le_antisymm le_top fun x _ => I.mem_iff _ |>.2 (Quotient.eq'.1 (h.elim x 0)))
Characterization of Simple Rings via Injectivity or Trivial Codomain of Homomorphisms
Informal description
A nontrivial non-associative ring $R$ is simple if and only if for every non-associative semiring $S$ and every ring homomorphism $f \colon R \to S$, either $f$ is injective or $S$ is a subsingleton (i.e., has at most one element).
IsSimpleRing.iff_injective_ringHom theorem
(R : Type u) [NonAssocRing R] [Nontrivial R] : IsSimpleRing R ↔ ∀ {S : Type u} [NonAssocSemiring S] [Nontrivial S] (f : R →+* S), Function.Injective f
Full source 
lemma iff_injective_ringHom (R : Type u) [NonAssocRing R] [Nontrivial R] :
    IsSimpleRingIsSimpleRing R ↔
    ∀ {S : Type u} [NonAssocSemiring S] [Nontrivial S] (f : R →+* S), Function.Injective f :=
  iff_injective_ringHom_or_subsingleton_codomain R |>.trans <|
    ⟨fun H _ _ _ f => H f |>.resolve_right (by simpa [not_subsingleton_iff_nontrivial]),
      fun H S _ f => subsingleton_or_nontrivial S |>.recOn Or.inr fun _ => Or.inl <| H f⟩
Characterization of Simple Rings via Injectivity of Homomorphisms to Nontrivial Semirings
Informal description
A nontrivial non-associative ring $R$ is simple if and only if every ring homomorphism $f \colon R \to S$ to a nontrivial non-associative semiring $S$ is injective.