Ideals over a ring

This file defines Ideal R, the type of (left) ideals over a ring R. Note that over commutative rings, left ideals and two-sided ideals are equivalent.

Implementation notes

Ideal R is implemented using Submodule R R, where • is interpreted as *.

TODO

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

@[reducible, inline]

abbrev Ideal (R : Type u) [Semiring R] : Type u

A (left) ideal in a semiring R is an additive submonoid s such that a * b ∈ s whenever b ∈ s. If R is a ring, then s is an additive subgroup.

Equations

• Ideal R = Submodule R R

theorem Ideal.zero_mem {α : Type u} [Semiring α] (I : Ideal α) : 0 ∈ I

theorem Ideal.add_mem {α : Type u} [Semiring α] (I : Ideal α) {a : α} {b : α} : a ∈ I → b ∈ I → a + b ∈ I

theorem Ideal.mul_mem_left {α : Type u} [Semiring α] (I : Ideal α) (a : α) {b : α} : b ∈ I → a * b ∈ I

theorem Ideal.ext_iff {α : Type u} [Semiring α] {I : Ideal α} {J : Ideal α} : I = J ↔ ∀ (x : α), x ∈ I ↔ x ∈ J

theorem Ideal.ext {α : Type u} [Semiring α] {I : Ideal α} {J : Ideal α} (h : ∀ (x : α), x ∈ I ↔ x ∈ J) : I = J

theorem Ideal.sum_mem {α : Type u} [Semiring α] (I : Ideal α) {ι : Type u_1} {t : Finset ι} {f : ι → α} : (∀ c ∈ t, f c ∈ I) → ∑ i ∈ t, f i ∈ I

@[simp]

theorem Ideal.unit_mul_mem_iff_mem {α : Type u} [Semiring α] (I : Ideal α) {x : α} {y : α} (hy : IsUnit y) : y * x ∈ I ↔ x ∈ I

@[simp]

theorem Ideal.mul_unit_mem_iff_mem {α : Type u} [CommSemiring α] (I : Ideal α) {x : α} {y : α} (hy : IsUnit y) : x * y ∈ I ↔ x ∈ I

theorem Ideal.mul_mem_right {α : Type u} {a : α} (b : α) [CommSemiring α] (I : Ideal α) (h : a ∈ I) : a * b ∈ I

theorem Ideal.mem_of_dvd {α : Type u} {a : α} {b : α} [CommSemiring α] (I : Ideal α) (hab : a ∣ b) (ha : a ∈ I) : b ∈ I

theorem Ideal.pow_mem_of_mem {α : Type u} {a : α} [CommSemiring α] (I : Ideal α) (ha : a ∈ I) (n : ℕ) (hn : 0 < n) : a ^ n ∈ I

theorem Ideal.pow_mem_of_pow_mem {α : Type u} {a : α} [CommSemiring α] (I : Ideal α) {m : ℕ} {n : ℕ} (ha : a ^ m ∈ I) (h : m ≤ n) : a ^ n ∈ I

theorem Ideal.neg_mem_iff {α : Type u} [Ring α] (I : Ideal α) {a : α} : -a ∈ I ↔ a ∈ I

theorem Ideal.add_mem_iff_left {α : Type u} [Ring α] (I : Ideal α) {a : α} {b : α} : b ∈ I → (a + b ∈ I ↔ a ∈ I)

theorem Ideal.add_mem_iff_right {α : Type u} [Ring α] (I : Ideal α) {a : α} {b : α} : a ∈ I → (a + b ∈ I ↔ b ∈ I)

theorem Ideal.sub_mem {α : Type u} [Ring α] (I : Ideal α) {a : α} {b : α} : a ∈ I → b ∈ I → a - b ∈ I

theorem Ideal.mul_sub_mul_mem {R : Type u_1} [CommRing R] (I : Ideal R) {a : R} {b : R} {c : R} {d : R} (h1 : a - b ∈ I) (h2 : c - d ∈ I) : a * c - b * d ∈ I