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} [Semiring α] (I : Ideal α) (ι : Type v) : Ideal (ι → α)

I^n as an ideal of R^n.

Equations

• I.pi ι = { carrier := {x : ι → α | ∀ (i : ι), x i ∈ I}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

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

theorem Ideal.add_pow_mem_of_pow_mem_of_le {α : Type u} {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} {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} [CommSemiring α] [DecidableEq α] (s : Multiset α) (n : ℕ) : s.sum ^ (Multiset.card s * n + 1) ∈ Ideal.span ↑(Multiset.map (fun (x : α) => x ^ (n + 1)) s).toFinset

theorem Ideal.sum_pow_mem_span_pow {α : Type u} [CommSemiring α] {ι : Type u_1} (s : Finset ι) (f : ι → α) (n : ℕ) : (∑ i ∈ s, f i) ^ (s.card * 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) = ⊤

def Ideal.equivFinTwo (K : Type u) [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.

Equations

• Ideal.equivFinTwo K = { toFun := fun (I : Ideal K) => if I = ⊥ then 0 else 1, invFun := ![⊥, ⊤], left_inv := ⋯, right_inv := ⋯ }

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

Equations

• ⋯ = ⋯

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

• ⋯ = ⋯

theorem Ring.exists_not_isUnit_of_not_isField {R : Type u_1} [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_1} [CommSemiring R] [Nontrivial R] : ¬IsField R ↔ ∃ (I : Ideal R), ⊥ < I ∧ I < ⊤

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

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 : 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} [CommSemiring R] [Nontrivial R] (M : Ideal R) [hm : M.IsMaximal] (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 α

@[simp]

theorem map_mem_nonunits_iff {α : Type u} {β : Type v} {F : Type w} [Monoid α] [Monoid β] [FunLike F α β] [MonoidHomClass F α β] (f : F) [IsLocalHom f] (a : α) : f a ∈ nonunits β ↔ a ∈ 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 α), I.IsMaximal ∧ a ∈ I