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]

def 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 : 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 : ι), c ∈ t → f c ∈ I) → (Finset.sum t fun i => f i) ∈ I

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

@[simp]

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

def Ideal.span {α : Type u} [Semiring α] (s : Set α) : Ideal α

The ideal generated by a subset of a ring

Equations

• Ideal.span s = Submodule.span α s

@[simp]

theorem Ideal.submodule_span_eq {α : Type u} [Semiring α] {s : Set α} : Submodule.span α s = Ideal.span s

@[simp]

theorem Ideal.span_empty {α : Type u} [Semiring α] : Ideal.span ∅ = ⊥

@[simp]

theorem Ideal.span_univ {α : Type u} [Semiring α] : Ideal.span Set.univ = ⊤

theorem Ideal.span_union {α : Type u} [Semiring α] (s : Set α) (t : Set α) : Ideal.span (s ∪ t) = Ideal.span s ⊔ Ideal.span t

theorem Ideal.span_iUnion {α : Type u} [Semiring α] {ι : Sort u_1} (s : ι → Set α) : Ideal.span (⋃ (i : ι), s i) = ⨆ (i : ι), Ideal.span (s i)

theorem Ideal.mem_span {α : Type u} [Semiring α] {s : Set α} (x : α) : x ∈ Ideal.span s ↔ ∀ (p : Ideal α), s ⊆ ↑p → x ∈ p

theorem Ideal.subset_span {α : Type u} [Semiring α] {s : Set α} : s ⊆ ↑(Ideal.span s)

theorem Ideal.span_le {α : Type u} [Semiring α] {s : Set α} {I : Ideal α} : Ideal.span s ≤ I ↔ s ⊆ ↑I

theorem Ideal.span_mono {α : Type u} [Semiring α] {s : Set α} {t : Set α} : s ⊆ t → Ideal.span s ≤ Ideal.span t

@[simp]

theorem Ideal.span_eq {α : Type u} [Semiring α] (I : Ideal α) : Ideal.span ↑I = I

@[simp]

theorem Ideal.span_singleton_one {α : Type u} [Semiring α] : Ideal.span {1} = ⊤

theorem Ideal.isCompactElement_top {α : Type u} [Semiring α] : CompleteLattice.IsCompactElement ⊤

theorem Ideal.mem_span_insert {α : Type u} [Semiring α] {s : Set α} {x : α} {y : α} : x ∈ Ideal.span (insert y s) ↔ ∃ a z, z ∈ Ideal.span s ∧ x = a * y + z

theorem Ideal.mem_span_singleton' {α : Type u} [Semiring α] {x : α} {y : α} : x ∈ Ideal.span {y} ↔ ∃ a, a * y = x

theorem Ideal.span_singleton_le_iff_mem {α : Type u} [Semiring α] (I : Ideal α) {x : α} : Ideal.span {x} ≤ I ↔ x ∈ I

theorem Ideal.span_singleton_mul_left_unit {α : Type u} [Semiring α] {a : α} (h2 : IsUnit a) (x : α) : Ideal.span {a * x} = Ideal.span {x}

theorem Ideal.span_insert {α : Type u} [Semiring α] (x : α) (s : Set α) : Ideal.span (insert x s) = Ideal.span {x} ⊔ Ideal.span s

theorem Ideal.span_eq_bot {α : Type u} [Semiring α] {s : Set α} : Ideal.span s = ⊥ ↔ ∀ (x : α), x ∈ s → x = 0

@[simp]

theorem Ideal.span_singleton_eq_bot {α : Type u} [Semiring α] {x : α} : Ideal.span {x} = ⊥ ↔ x = 0

theorem Ideal.span_singleton_ne_top {α : Type u_1} [CommSemiring α] {x : α} (hx : ¬IsUnit x) : Ideal.span {x} ≠ ⊤

@[simp]

theorem Ideal.span_zero {α : Type u} [Semiring α] : Ideal.span 0 = ⊥

@[simp]

theorem Ideal.span_one {α : Type u} [Semiring α] : Ideal.span 1 = ⊤

theorem Ideal.span_eq_top_iff_finite {α : Type u} [Semiring α] (s : Set α) : Ideal.span s = ⊤ ↔ ∃ s', ↑s' ⊆ s ∧ Ideal.span ↑s' = ⊤

theorem Ideal.mem_span_singleton_sup {S : Type u_1} [CommSemiring S] {x : S} {y : S} {I : Ideal S} : x ∈ Ideal.span {y} ⊔ I ↔ ∃ a b, b ∈ I ∧ a * y + b = x

def Ideal.ofRel {α : Type u} [Semiring α] (r : α → α → Prop) : Ideal α

The ideal generated by an arbitrary binary relation.

Equations

• Ideal.ofRel r = Submodule.span α {x | ∃ a b _h, x + b = a}

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

• ne_top' : I ≠ ⊤

  The prime ideal is not the entire ring.

• mem_or_mem' : ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I

  If a product lies in the prime ideal, then at least one element lies in the prime ideal.

An ideal P of a ring R is prime if P ≠ R and xy ∈ P → x ∈ P ∨ y ∈ P

theorem Ideal.isPrime_iff {α : Type u} [Semiring α] {I : Ideal α} : Ideal.IsPrime I ↔ I ≠ ⊤ ∧ ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I

theorem Ideal.IsPrime.ne_top {α : Type u} [Semiring α] {I : Ideal α} (hI : Ideal.IsPrime I) : I ≠ ⊤

theorem Ideal.IsPrime.mem_or_mem {α : Type u} [Semiring α] {I : Ideal α} (hI : Ideal.IsPrime I) {x : α} {y : α} : x * y ∈ I → x ∈ I ∨ y ∈ I

theorem Ideal.IsPrime.mem_or_mem_of_mul_eq_zero {α : Type u} [Semiring α] {I : Ideal α} (hI : Ideal.IsPrime I) {x : α} {y : α} (h : x * y = 0) : x ∈ I ∨ y ∈ I

theorem Ideal.IsPrime.mem_of_pow_mem {α : Type u} [Semiring α] {I : Ideal α} (hI : Ideal.IsPrime I) {r : α} (n : ℕ) (H : r ^ n ∈ I) : r ∈ I

theorem Ideal.not_isPrime_iff {α : Type u} [Semiring α] {I : Ideal α} : ¬Ideal.IsPrime I ↔ I = ⊤ ∨ ∃ x _hx y _hy, x * y ∈ I

theorem Ideal.zero_ne_one_of_proper {α : Type u} [Semiring α] {I : Ideal α} (h : I ≠ ⊤) : 0 ≠ 1

theorem Ideal.bot_prime {R : Type u_1} [Ring R] [IsDomain R] : Ideal.IsPrime ⊥

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

• out : IsCoatom I

  The maximal ideal is a coatom in the ordering on ideals; that is, it is not the entire ring, and there are no other proper ideals strictly containing it.

An ideal is maximal if it is maximal in the collection of proper ideals.

theorem Ideal.isMaximal_def {α : Type u} [Semiring α] {I : Ideal α} : Ideal.IsMaximal I ↔ IsCoatom I

theorem Ideal.IsMaximal.ne_top {α : Type u} [Semiring α] {I : Ideal α} (h : Ideal.IsMaximal I) : I ≠ ⊤

theorem Ideal.isMaximal_iff {α : Type u} [Semiring α] {I : Ideal α} : Ideal.IsMaximal I ↔ ¬1 ∈ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → ¬x ∈ I → x ∈ J → 1 ∈ J

theorem Ideal.IsMaximal.eq_of_le {α : Type u} [Semiring α] {I : Ideal α} {J : Ideal α} (hI : Ideal.IsMaximal I) (hJ : J ≠ ⊤) (IJ : I ≤ J) : I = J

instance Ideal.instIsCoatomicIdealToPartialOrderInstOmegaCompletePartialOrderCompleteLatticeToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleInstOrderTopSubmoduleToLEToPreorderInstPartialOrderSetLike {α : Type u} [Semiring α] : IsCoatomic (Ideal α)

Equations

• One or more equations did not get rendered due to their size.

theorem Ideal.IsMaximal.coprime_of_ne {α : Type u} [Semiring α] {M : Ideal α} {M' : Ideal α} (hM : Ideal.IsMaximal M) (hM' : Ideal.IsMaximal M') (hne : M ≠ M') : M ⊔ M' = ⊤

theorem Ideal.exists_le_maximal {α : Type u} [Semiring α] (I : Ideal α) (hI : I ≠ ⊤) : ∃ M, Ideal.IsMaximal M ∧ I ≤ M

Krull's theorem: if I is an ideal that is not the whole ring, then it is included in some maximal ideal.

theorem Ideal.exists_maximal (α : Type u) [Semiring α] [Nontrivial α] : ∃ M, Ideal.IsMaximal M

Krull's theorem: a nontrivial ring has a maximal ideal.

instance Ideal.instNontrivialIdeal {α : Type u} [Semiring α] [Nontrivial α] : Nontrivial (Ideal α)

Equations

• @Ideal.instNontrivialIdeal = @Ideal.instNontrivialIdeal.proof_1

theorem Ideal.maximal_of_no_maximal {R : Type u} [Semiring R] {P : Ideal R} (hmax : ∀ (m : Ideal R), P < m → ¬Ideal.IsMaximal m) (J : Ideal R) (hPJ : P < J) : J = ⊤

If P is not properly contained in any maximal ideal then it is not properly contained in any proper ideal

theorem Ideal.span_pair_comm {α : Type u} [Semiring α] {x : α} {y : α} : Ideal.span {x, y} = Ideal.span {y, x}

theorem Ideal.mem_span_pair {α : Type u} [Semiring α] {x : α} {y : α} {z : α} : z ∈ Ideal.span {x, y} ↔ ∃ a b, a * x + b * y = z

@[simp]

theorem Ideal.span_pair_add_mul_left {R : Type u} [CommRing R] {x : R} {y : R} (z : R) : Ideal.span {x + y * z, y} = Ideal.span {x, y}

@[simp]

theorem Ideal.span_pair_add_mul_right {R : Type u} [CommRing R] {x : R} {y : R} (z : R) : Ideal.span {x, y + x * z} = Ideal.span {x, y}

theorem Ideal.IsMaximal.exists_inv {α : Type u} [Semiring α] {I : Ideal α} (hI : Ideal.IsMaximal I) {x : α} (hx : ¬x ∈ I) : ∃ y i, i ∈ I ∧ y * x + i = 1

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

theorem Ideal.mem_sup_right {R : Type u} [Semiring R] {S : Ideal R} {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

@[simp]

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

@[simp]

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

@[simp]

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

def Ideal.pi {α : Type u} [Semiring α] (I : Ideal α) (ι : Type v) : Ideal (ι → α)

I^n as an ideal of R^n.

Equations

• One or more equations did not get rendered due to their size.

theorem Ideal.mem_pi {α : Type u} [Semiring α] (I : Ideal α) (ι : Type v) (x : ι → α) : x ∈ Ideal.pi I ι ↔ ∀ (i : ι), x i ∈ I

theorem Ideal.sInf_isPrime_of_isChain {α : Type u} [Semiring α] {s : Set (Ideal α)} (hs : Set.Nonempty s) (hs' : IsChain (fun x x_1 => x ≤ x_1) s) (H : ∀ (p : Ideal α), p ∈ s → Ideal.IsPrime p) : Ideal.IsPrime (sInf s)

@[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_span_singleton {α : Type u} [CommSemiring α] {x : α} {y : α} : x ∈ Ideal.span {y} ↔ y ∣ x

theorem Ideal.mem_span_singleton_self {α : Type u} [CommSemiring α] (x : α) : x ∈ Ideal.span {x}

theorem Ideal.span_singleton_le_span_singleton {α : Type u} [CommSemiring α] {x : α} {y : α} : Ideal.span {x} ≤ Ideal.span {y} ↔ y ∣ x

theorem Ideal.span_singleton_eq_span_singleton {α : Type u} [CommRing α] [IsDomain α] {x : α} {y : α} : Ideal.span {x} = Ideal.span {y} ↔ Associated x y

theorem Ideal.span_singleton_mul_right_unit {α : Type u} [CommSemiring α] {a : α} (h2 : IsUnit a) (x : α) : Ideal.span {x * a} = Ideal.span {x}

theorem Ideal.span_singleton_eq_top {α : Type u} [CommSemiring α] {x : α} : Ideal.span {x} = ⊤ ↔ IsUnit x

theorem Ideal.span_singleton_prime {α : Type u} [CommSemiring α] {p : α} (hp : p ≠ 0) : Ideal.IsPrime (Ideal.span {p}) ↔ Prime p

theorem Ideal.IsMaximal.isPrime {α : Type u} [CommSemiring α] {I : Ideal α} (H : Ideal.IsMaximal I) : Ideal.IsPrime I

instance Ideal.IsMaximal.isPrime' {α : Type u} [CommSemiring α] (I : Ideal α) [_H : Ideal.IsMaximal I] : Ideal.IsPrime I

Equations

• (_ : ∀ [_H : Ideal.IsMaximal I], Ideal.IsPrime I) = (_ : Ideal.IsMaximal I → Ideal.IsPrime I)

theorem Ideal.span_singleton_lt_span_singleton {β : Type v} [CommRing β] [IsDomain β] {x : β} {y : β} : Ideal.span {x} < Ideal.span {y} ↔ DvdNotUnit y x

theorem Ideal.factors_decreasing {β : Type v} [CommRing β] [IsDomain β] (b₁ : β) (b₂ : β) (h₁ : b₁ ≠ 0) (h₂ : ¬IsUnit b₂) : Ideal.span {b₁ * b₂} < Ideal.span {b₁}

theorem Ideal.mul_mem_right {α : Type u} {a : α} (b : α) [CommSemiring α] (I : Ideal α) (h : a ∈ I) : a * 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.IsPrime.mul_mem_iff_mem_or_mem {α : Type u} [CommSemiring α] {I : Ideal α} (hI : Ideal.IsPrime I) {x : α} {y : α} : x * y ∈ I ↔ x ∈ I ∨ y ∈ I

theorem Ideal.IsPrime.pow_mem_iff_mem {α : Type u} [CommSemiring α] {I : Ideal α} (hI : Ideal.IsPrime I) {r : α} (n : ℕ) (hn : 0 < n) : r ^ n ∈ I ↔ r ∈ I

theorem Ideal.pow_multiset_sum_mem_span_pow {α : Type u} [CommSemiring α] [DecidableEq α] (s : Multiset α) (n : ℕ) : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ Ideal.span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))

theorem Ideal.sum_pow_mem_span_pow {α : Type u} [CommSemiring α] {ι : Type u_1} (s : Finset ι) (f : ι → α) (n : ℕ) : (Finset.sum s fun i => f i) ^ (Finset.card s * n + 1) ∈ Ideal.span ((fun i => f i ^ (n + 1)) '' ↑s)

theorem Ideal.span_pow_eq_top {α : Type u} [CommSemiring α] (s : Set α) (hs : Ideal.span s = ⊤) (n : ℕ) : Ideal.span ((fun x => x ^ n) '' s) = ⊤

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.mem_span_insert' {α : Type u} [Ring α] {s : Set α} {x : α} {y : α} : x ∈ Ideal.span (insert y s) ↔ ∃ a, x + a * y ∈ Ideal.span s

@[simp]

theorem Ideal.span_singleton_neg {α : Type u} [Ring α] (x : α) : Ideal.span {-x} = Ideal.span {x}

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.

instance Ideal.isSimpleOrder {K : Type u} [DivisionSemiring K] : IsSimpleOrder (Ideal K)

Ideals of a DivisionSemiring are a simple order. Thanks to the way abbreviations work, this automatically gives an IsSimpleModule K instance.

Equations

• @Ideal.isSimpleOrder = @Ideal.isSimpleOrder.proof_1

theorem Ideal.eq_bot_of_prime {K : Type u} [DivisionSemiring K] (I : Ideal K) [h : Ideal.IsPrime I] : I = ⊥

theorem Ideal.bot_isMaximal {K : Type u} [DivisionSemiring K] : Ideal.IsMaximal ⊥

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

theorem Ring.exists_not_isUnit_of_not_isField {R : Type u_1} [CommSemiring R] [Nontrivial R] (hf : ¬IsField R) : ∃ x _hx, ¬IsUnit x

theorem Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top {R : Type u_1} [CommSemiring R] [Nontrivial R] : ¬IsField R ↔ ∃ I, ⊥ < I ∧ I < ⊤

theorem Ring.not_isField_iff_exists_prime {R : Type u_1} [CommSemiring R] [Nontrivial R] : ¬IsField R ↔ ∃ p, p ≠ ⊥ ∧ Ideal.IsPrime p

theorem Ring.isField_iff_isSimpleOrder_ideal {R : Type u_1} [CommSemiring R] : IsField R ↔ IsSimpleOrder (Ideal R)

Also see Ideal.isSimpleOrder for the forward direction as an instance when R is a division (semi)ring.

This result actually holds for all division semirings, but we lack the predicate to state it.

theorem Ring.ne_bot_of_isMaximal_of_not_isField {R : Type u_1} [CommSemiring R] [Nontrivial R] {M : Ideal R} (max : Ideal.IsMaximal M) (not_field : ¬IsField R) : M ≠ ⊥

When a ring is not a field, the maximal ideals are nontrivial.

theorem Ideal.bot_lt_of_maximal {R : Type u} [CommRing R] [Nontrivial R] (M : Ideal R) [hm : Ideal.IsMaximal M] (non_field : ¬IsField R) : ⊥ < M

def nonunits (α : Type u) [Monoid α] : Set α

The set of non-invertible elements of a monoid.

Equations

• nonunits α = {a | ¬IsUnit a}

@[simp]

theorem mem_nonunits_iff {α : Type u} {a : α} [Monoid α] : a ∈ nonunits α ↔ ¬IsUnit a

theorem mul_mem_nonunits_right {α : Type u} {a : α} {b : α} [CommMonoid α] : b ∈ nonunits α → a * b ∈ nonunits α

theorem mul_mem_nonunits_left {α : Type u} {a : α} {b : α} [CommMonoid α] : a ∈ nonunits α → a * b ∈ nonunits α

theorem zero_mem_nonunits {α : Type u} [Semiring α] : 0 ∈ nonunits α ↔ 0 ≠ 1

@[simp]

theorem one_not_mem_nonunits {α : Type u} [Monoid α] : ¬1 ∈ nonunits α

theorem coe_subset_nonunits {α : Type u} [Semiring α] {I : Ideal α} (h : I ≠ ⊤) : ↑I ⊆ nonunits α

theorem exists_max_ideal_of_mem_nonunits {α : Type u} {a : α} [CommSemiring α] (h : a ∈ nonunits α) : ∃ I, Ideal.IsMaximal I ∧ a ∈ I