# The lattice of ideals in a ring #

Some basic results on lattice operations on ideals: `⊥`, `⊤`, `⊔`, `⊓`.

## TODO #

Support right ideals, and two-sided ideals over non-commutative rings.

source
@[instance 100]
instance Ideal.instIsTwoSidedBot {α : Type u} [Semiring α] :
⊥.IsTwoSided
source
@[instance 100]
instance Ideal.instIsTwoSidedTop {α : Type u} [Semiring α] :
⊤.IsTwoSided
source
@[instance 100]
instance Ideal.instIsTwoSidedIInf {α : Type u} [Semiring α] {ι : Sort u_1} (I : ι → Ideal α) [∀ (i : ι), (I i).IsTwoSided] :
(⨅ (i : ι), I i).IsTwoSided
source
theorem Ideal.eq_top_of_unit_mem {α : Type u} [Semiring α] (I : Ideal α) (x y : α) (hx : x ∈ I) (h : y * x = 1) :
I = ⊤
source
theorem Ideal.eq_top_of_isUnit_mem {α : Type u} [Semiring α] (I : Ideal α) {x : α} (hx : x ∈ I) (h : IsUnit x) :
I = ⊤
source
theorem Ideal.eq_top_iff_one {α : Type u} [Semiring α] (I : Ideal α) :
I = ⊤ ↔ 1 ∈ I
source
theorem Ideal.ne_top_iff_one {α : Type u} [Semiring α] (I : Ideal α) :
I ≠ ⊤ ↔ 1 ∉ I
source
theorem Ideal.mem_sup_left {R : Type u} [Semiring R] {S T : Ideal R} {x : R} :
x ∈ S → x ∈ S ⊔ T
source
theorem Ideal.mem_sup_right {R : Type u} [Semiring R] {S T : Ideal R} {x : R} :
x ∈ T → x ∈ S ⊔ T
source
theorem Ideal.mem_iSup_of_mem {R : Type u} [Semiring R] {ι : Sort u_1} {S : ι → Ideal R} (i : ι) {x : R} :
x ∈ S i → x ∈ iSup S
source
theorem Ideal.mem_sSup_of_mem {R : Type u} [Semiring R] {S : Set (Ideal R)} {s : Ideal R} (hs : s ∈ S) {x : R} :
x ∈ s → x ∈ sSup S
source
theorem Ideal.mem_sInf {R : Type u} [Semiring R] {s : Set (Ideal R)} {x : R} :
x ∈ sInf s ↔ ∀ ⦃I : Ideal R⦄, I ∈ s → x ∈ I
source
theorem Ideal.mem_inf {R : Type u} [Semiring R] {I J : Ideal R} {x : R} :
x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J
source
theorem Ideal.mem_iInf {R : Type u} [Semiring R] {ι : Sort u_1} {I : ι → Ideal R} {x : R} :
x ∈ iInf I ↔ ∀ (i : ι), x ∈ I i
source
theorem Ideal.mem_bot {R : Type u} [Semiring R] {x : R} :
x ∈ ⊥ ↔ x = 0
source
theorem Ideal.eq_bot_or_top {K : Type u} [DivisionSemiring K] (I : Ideal K) :
I = ⊥ ∨ I = ⊤

All ideals in a division (semi)ring are trivial.