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.

@[instance 100]

instance Ideal.instIsTwoSidedBot {α : Type u} [Semiring α] : ⊥.IsTwoSided

@[instance 100]

instance Ideal.instIsTwoSidedTop {α : Type u} [Semiring α] : ⊤.IsTwoSided

@[instance 100]

instance Ideal.instIsTwoSidedIInf {α : Type u} [Semiring α] {ι : Sort u_1} (I : ι → Ideal α) [∀ (i : ι), (I i).IsTwoSided] : (⨅ (i : ι), I i).IsTwoSided

theorem Ideal.eq_top_of_unit_mem {α : Type u} [Semiring α] (I : Ideal α) (x y : α) (hx : x ∈ I) (h : y * x = 1) : I = ⊤

theorem Ideal.eq_top_of_isUnit_mem {α : Type u} [Semiring α] (I : Ideal α) {x : α} (hx : x ∈ I) (h : IsUnit x) : I = ⊤

theorem Ideal.eq_top_iff_one {α : Type u} [Semiring α] (I : Ideal α) : I = ⊤ ↔ 1 ∈ I

theorem Ideal.ne_top_iff_one {α : Type u} [Semiring α] (I : Ideal α) : I ≠ ⊤ ↔ 1 ∉ I

theorem Ideal.mem_sup_left {R : Type u} [Semiring R] {S T : Ideal R} {x : R} : x ∈ S → x ∈ S ⊔ T

theorem Ideal.mem_sup_right {R : Type u} [Semiring R] {S T : Ideal R} {x : R} : x ∈ T → x ∈ S ⊔ T

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

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

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

theorem Ideal.mem_inf {R : Type u} [Semiring R] {I J : Ideal R} {x : R} : x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J

theorem Ideal.mem_iInf {R : Type u} [Semiring R] {ι : Sort u_1} {I : ι → Ideal R} {x : R} : x ∈ iInf I ↔ ∀ (i : ι), x ∈ I i

theorem Ideal.mem_bot {R : Type u} [Semiring R] {x : R} : x ∈ ⊥ ↔ x = 0

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.