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

Instances For

• Ideal.instFinite
• Ideal.instHasQuotient
• Ideal.instHasQuotient_1
• Ideal.instIdemCommSemiring
• Ideal.instIsCoatomic
• Ideal.instNoZeroDivisors
• Ideal.instNontrivial
• Ideal.isSimpleOrder
• Submodule.algebraIdeal
• Submodule.moduleSubmodule
• instNonUnitalSubringClassIdeal
• instNonUnitalSubsemiringClassIdeal

class Ideal.IsTwoSided {α : Type u} [Semiring α] (I : Ideal α) : Prop

A left ideal I : Ideal R is two-sided if it is also a right ideal.

• mul_mem_of_left {a : α} (b : α) : a ∈ I → a * b ∈ I

Instances

• Ideal.IsTwoSided.instHMul
• Ideal.IsTwoSided.instHPowNat
• Ideal.instIsTwoSided
• Ideal.instIsTwoSidedBot
• Ideal.instIsTwoSidedComap
• Ideal.instIsTwoSidedForallPi
• Ideal.instIsTwoSidedIInf
• Ideal.instIsTwoSidedMapRingHomOfRingHomSurjective
• Ideal.instIsTwoSidedTop
• Ideal.instIsTwoSided_1
• RingHom.instIsTwoSidedKer
• Submodule.instIsTwoSidedColon
• instIsTwoSidedAnnihilator

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.mul_mem_right {α : Type u_1} {a : α} (b : α) [Semiring α] (I : Ideal α) [I.IsTwoSided] (h : a ∈ 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

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

theorem Ideal.pow_mem_of_pow_mem {α : Type u} [Semiring α] (I : Ideal α) {a : α} {m n : ℕ} (ha : a ^ m ∈ I) (h : m ≤ n) : a ^ n ∈ 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' := ⋯ }

instance Ideal.instIsTwoSided {α : Type u} [CommSemiring α] (I : Ideal α) : I.IsTwoSided

instance Ideal.instIsTwoSided_1 {α : Type u_1} [CommRing α] (I : Ideal α) : I.IsTwoSided

@[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.mem_of_dvd {α : Type u} {a b : α} [CommSemiring α] (I : Ideal α) (hab : a ∣ b) (ha : a ∈ I) : b ∈ 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 {α : Type u} [Ring α] (I : Ideal α) {a b c d : α} [I.IsTwoSided] (h1 : a - b ∈ I) (h2 : c - d ∈ I) : a * c - b * d ∈ I