Ideals over a ring

This file contains an assortment of definitions and results for 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.

def Ideal.pi {ι : Type u_1} {α : ι → Type u_5} [(i : ι) → Semiring (α i)] (I : (i : ι) → Ideal (α i)) : Ideal ((i : ι) → α i)

Πᵢ Iᵢ as an ideal of Πᵢ Rᵢ.

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

@[instance 100]

instance Ideal.instIsTwoSidedForallPi {ι : Type u_1} {α : ι → Type u_5} [(i : ι) → Semiring (α i)] (I : (i : ι) → Ideal (α i)) [∀ (i : ι), (I i).IsTwoSided] : (pi I).IsTwoSided

theorem Ideal.add_pow_mem_of_pow_mem_of_le_of_commute {α : Type u_6} [Semiring α] (I : Ideal α) {a b : α} {m n k : ℕ} (ha : a ^ m ∈ I) (hb : b ^ n ∈ I) (hk : m + n ≤ k + 1) (hab : Commute a b) : (a + b) ^ k ∈ I

theorem Ideal.add_pow_add_pred_mem_of_pow_mem_of_commute {α : Type u_6} [Semiring α] (I : Ideal α) {a b : α} {m n : ℕ} (ha : a ^ m ∈ I) (hb : b ^ n ∈ I) (hab : Commute a b) : (a + b) ^ (m + n - 1) ∈ I

theorem Ideal.add_pow_mem_of_pow_mem_of_le {α : Type u_2} {a b : α} [CommSemiring α] (I : Ideal α) {m n k : ℕ} (ha : a ^ m ∈ I) (hb : b ^ n ∈ I) (hk : m + n ≤ k + 1) : (a + b) ^ k ∈ I

theorem Ideal.add_pow_add_pred_mem_of_pow_mem {α : Type u_2} {a b : α} [CommSemiring α] (I : Ideal α) {m n : ℕ} (ha : a ^ m ∈ I) (hb : b ^ n ∈ I) : (a + b) ^ (m + n - 1) ∈ I

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

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

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

theorem Ideal.span_range_pow_eq_top {α : Type u_2} [CommSemiring α] (s : Set α) (hs : span s = ⊤) (n : ↑s → ℕ) : span (Set.range fun (x : ↑s) => ↑x ^ n x) = ⊤

theorem Ideal.prod_mem {α : Type u_2} [CommSemiring α] {ι : Type u_5} {f : ι → α} {s : Finset ι} (I : Ideal α) {i : ι} (hi : i ∈ s) (hfi : f i ∈ I) : ∏ i ∈ s, f i ∈ I

def Ideal.equivFinTwo (K : Type u_5) [DivisionSemiring K] [DecidableEq (Ideal K)] : Ideal K ≃ Fin 2

A bijection between (left) ideals of a division ring and {0, 1}, sending ⊥ to 0 and ⊤ to 1.

instance Ideal.instFinite {K : Type u_5} [DivisionSemiring K] : Finite (Ideal K)

instance Ideal.isSimpleOrder {K : Type u_5} [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.

theorem Ring.exists_not_isUnit_of_not_isField {R : Type u_5} [CommSemiring R] [Nontrivial R] (hf : ¬IsField R) : ∃ (x : R) (_ : x ≠ 0), ¬IsUnit x

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

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

theorem Ring.isField_iff_isSimpleOrder_ideal {R : Type u_5} [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_5} [CommSemiring R] [Nontrivial R] {M : Ideal R} (max : M.IsMaximal) (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_5} [CommSemiring R] [Nontrivial R] (M : Ideal R) [hm : M.IsMaximal] (non_field : ¬IsField R) : ⊥ < M