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 {α : Type u} [Semiring α] {I J : Ideal α} (h : ∀ (x : α), x ∈ I ↔ x ∈ J) : I = J

@[simp]

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

def Module.eqIdeal (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (m m' : M) : Ideal R

For two elements m and m' in an R-module M, the set of elements r : R with equal scalar product with m and m' is an ideal of R. If M is a group, this coincides with the kernel of LinearMap.toSpanSingleton R M (m - m').

Equations

• Module.eqIdeal R m m' = { carrier := {r : R | r • m = r • m'}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[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 b c d : R} (h1 : a - b ∈ I) (h2 : c - d ∈ I) : a * c - b * d ∈ I