ring_theory.ideal.basic - mathlib3 docs

@[reducible]

def ideal (R : Type u) [semiring R] :

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

source

@[protected]

theorem ideal.zero_mem {α : Type u} [semiring α] (I : ideal α) :

0 ∈ I

source

@[protected]

theorem ideal.add_mem {α : Type u} [semiring α] (I : ideal α) {a b : α} :

a ∈ I → b ∈ I → a + b ∈ I

source

theorem ideal.mul_mem_left {α : Type u} [semiring α] (I : ideal α) (a : α) {b : α} :

b ∈ I → a * b ∈ I

source

@[ext]

theorem ideal.ext {α : Type u} [semiring α] {I J : ideal α} (h : ∀ (x : α), x ∈ I ↔ x ∈ J) :

I = J

source

theorem ideal.sum_mem {α : Type u} [semiring α] (I : ideal α) {ι : Type u_1} {t : finset ι} {f : ι → α} :

(∀ (c : ι), c ∈ t → f c ∈ I) → t.sum (λ (i : ι), f i) ∈ I

source

theorem ideal.eq_top_of_unit_mem {α : Type u} [semiring α] (I : ideal α) (x y : α) (hx : x ∈ I) (h : y * x = 1) :

I = ⊤

source

theorem ideal.eq_top_of_is_unit_mem {α : Type u} [semiring α] (I : ideal α) {x : α} (hx : x ∈ I) (h : is_unit x) :

I = ⊤

source

theorem ideal.eq_top_iff_one {α : Type u} [semiring α] (I : ideal α) :

I = ⊤ ↔ 1 ∈ I

source

theorem ideal.ne_top_iff_one {α : Type u} [semiring α] (I : ideal α) :

I ≠ ⊤ ↔ 1 ∉ I

source

@[simp]

theorem ideal.unit_mul_mem_iff_mem {α : Type u} [semiring α] (I : ideal α) {x y : α} (hy : is_unit y) :

y * x ∈ I ↔ x ∈ I

source

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

source

@[simp]

theorem ideal.submodule_span_eq {α : Type u} [semiring α] {s : set α} :

submodule.span α s = ideal.span s

source

@[simp]

theorem ideal.span_empty {α : Type u} [semiring α] :

ideal.span ∅ = ⊥

source

@[simp]

theorem ideal.span_univ {α : Type u} [semiring α] :

ideal.span set.univ = ⊤

source

theorem ideal.span_union {α : Type u} [semiring α] (s t : set α) :

ideal.span (s ∪ t) = ideal.span s ⊔ ideal.span t

source

theorem ideal.span_Union {α : Type u} [semiring α] {ι : Sort u_1} (s : ι → set α) :

ideal.span (⋃ (i : ι), s i) = ⨆ (i : ι), ideal.span (s i)

source

theorem ideal.mem_span {α : Type u} [semiring α] {s : set α} (x : α) :

x ∈ ideal.span s ↔ ∀ (p : ideal α), s ⊆ ↑p → x ∈ p

source

theorem ideal.subset_span {α : Type u} [semiring α] {s : set α} :

s ⊆ ↑(ideal.span s)

source

theorem ideal.span_le {α : Type u} [semiring α] {s : set α} {I : ideal α} :

ideal.span s ≤ I ↔ s ⊆ ↑I

source

theorem ideal.span_mono {α : Type u} [semiring α] {s t : set α} :

s ⊆ t → ideal.span s ≤ ideal.span t

source

@[simp]

theorem ideal.span_eq {α : Type u} [semiring α] (I : ideal α) :

ideal.span ↑I = I

source

@[simp]

theorem ideal.span_singleton_one {α : Type u} [semiring α] :

ideal.span {1} = ⊤

source

theorem ideal.mem_span_insert {α : Type u} [semiring α] {s : set α} {x y : α} :

x ∈ ideal.span (has_insert.insert y s) ↔ ∃ (a z : α) (H : z ∈ ideal.span s), x = a * y + z

source

theorem ideal.mem_span_singleton' {α : Type u} [semiring α] {x y : α} :

x ∈ ideal.span {y} ↔ ∃ (a : α), a * y = x

source

theorem ideal.span_singleton_le_iff_mem {α : Type u} [semiring α] (I : ideal α) {x : α} :

ideal.span {x} ≤ I ↔ x ∈ I

source

theorem ideal.span_singleton_mul_left_unit {α : Type u} [semiring α] {a : α} (h2 : is_unit a) (x : α) :

ideal.span {a * x} = ideal.span {x}

source

theorem ideal.span_insert {α : Type u} [semiring α] (x : α) (s : set α) :

ideal.span (has_insert.insert x s) = ideal.span {x} ⊔ ideal.span s

source

theorem ideal.span_eq_bot {α : Type u} [semiring α] {s : set α} :

ideal.span s = ⊥ ↔ ∀ (x : α), x ∈ s → x = 0

source

@[simp]

theorem ideal.span_singleton_eq_bot {α : Type u} [semiring α] {x : α} :

ideal.span {x} = ⊥ ↔ x = 0

source

theorem ideal.span_singleton_ne_top {α : Type u_1} [comm_semiring α] {x : α} (hx : ¬is_unit x) :

ideal.span {x} ≠ ⊤

source

@[simp]

theorem ideal.span_zero {α : Type u} [semiring α] :

ideal.span 0 = ⊥

source

@[simp]

theorem ideal.span_one {α : Type u} [semiring α] :

ideal.span 1 = ⊤

source

theorem ideal.span_eq_top_iff_finite {α : Type u} [semiring α] (s : set α) :

ideal.span s = ⊤ ↔ ∃ (s' : finset α), ↑s' ⊆ s ∧ ideal.span ↑s' = ⊤

source

theorem ideal.mem_span_singleton_sup {S : Type u_1} [comm_semiring S] {x y : S} {I : ideal S} :

x ∈ ideal.span {y} ⊔ I ↔ ∃ (a b : S) (H : b ∈ I), a * y + b = x

source

def ideal.of_rel {α : Type u} [semiring α] (r : α → α → Prop) :

ideal α

The ideal generated by an arbitrary binary relation.

Equations

ideal.of_rel r = submodule.span α {x : α | ∃ (a b : α) (h : r a b), x + b = a}

source

@[class]

structure ideal.is_prime {α : Type u} [semiring α] (I : ideal α) :

Prop

ne_top' : I ≠ ⊤
mem_or_mem' : ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I

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

Instances of this typeclass

source

theorem ideal.is_prime_iff {α : Type u} [semiring α] {I : ideal α} :

I.is_prime ↔ I ≠ ⊤ ∧ ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I

source

theorem ideal.is_prime.ne_top {α : Type u} [semiring α] {I : ideal α} (hI : I.is_prime) :

I ≠ ⊤

source

theorem ideal.is_prime.mem_or_mem {α : Type u} [semiring α] {I : ideal α} (hI : I.is_prime) {x y : α} :

x * y ∈ I → x ∈ I ∨ y ∈ I

source

theorem ideal.is_prime.mem_or_mem_of_mul_eq_zero {α : Type u} [semiring α] {I : ideal α} (hI : I.is_prime) {x y : α} (h : x * y = 0) :

x ∈ I ∨ y ∈ I

source

theorem ideal.is_prime.mem_of_pow_mem {α : Type u} [semiring α] {I : ideal α} (hI : I.is_prime) {r : α} (n : ℕ) (H : r ^ n ∈ I) :

r ∈ I

source

theorem ideal.not_is_prime_iff {α : Type u} [semiring α] {I : ideal α} :

¬I.is_prime ↔ I = ⊤ ∨ ∃ (x : α) (H : x ∉ I) (y : α) (H : y ∉ I), x * y ∈ I

source

theorem ideal.zero_ne_one_of_proper {α : Type u} [semiring α] {I : ideal α} (h : I ≠ ⊤) :

0 ≠ 1

source

theorem ideal.bot_prime {R : Type u_1} [ring R] [is_domain R] :

⊥.is_prime

source

@[class]

structure ideal.is_maximal {α : Type u} [semiring α] (I : ideal α) :

Prop

out : is_coatom I

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

source

theorem ideal.is_maximal_def {α : Type u} [semiring α] {I : ideal α} :

I.is_maximal ↔ is_coatom I

source

theorem ideal.is_maximal.ne_top {α : Type u} [semiring α] {I : ideal α} (h : I.is_maximal) :

I ≠ ⊤

source

theorem ideal.is_maximal_iff {α : Type u} [semiring α] {I : ideal α} :

I.is_maximal ↔ 1 ∉ I ∧ ∀ (J : ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J

source

theorem ideal.is_maximal.eq_of_le {α : Type u} [semiring α] {I J : ideal α} (hI : I.is_maximal) (hJ : J ≠ ⊤) (IJ : I ≤ J) :

I = J

source

@[protected, instance]

def ideal.is_coatomic {α : Type u} [semiring α] :

is_coatomic (ideal α)

source

theorem ideal.is_maximal.coprime_of_ne {α : Type u} [semiring α] {M M' : ideal α} (hM : M.is_maximal) (hM' : M'.is_maximal) (hne : M ≠ M') :

M ⊔ M' = ⊤

source

theorem ideal.exists_le_maximal {α : Type u} [semiring α] (I : ideal α) (hI : I ≠ ⊤) :

∃ (M : ideal α), M.is_maximal ∧ I ≤ M

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

source

theorem ideal.exists_maximal (α : Type u) [semiring α] [nontrivial α] :

∃ (M : ideal α), M.is_maximal

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

source

@[protected, instance]

def ideal.nontrivial {α : Type u} [semiring α] [nontrivial α] :

nontrivial (ideal α)

source

theorem ideal.maximal_of_no_maximal {R : Type u} [semiring R] {P : ideal R} (hmax : ∀ (m : ideal R), P < m → ¬m.is_maximal) (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

source

theorem ideal.span_pair_comm {α : Type u} [semiring α] {x y : α} :

ideal.span {x, y} = ideal.span {y, x}

source

theorem ideal.mem_span_pair {α : Type u} [semiring α] {x y z : α} :

z ∈ ideal.span {x, y} ↔ ∃ (a b : α), a * x + b * y = z

source

@[simp]

theorem ideal.span_pair_add_mul_left {R : Type u} [comm_ring R] {x y : R} (z : R) :

ideal.span {x + y * z, y} = ideal.span {x, y}

source

@[simp]

theorem ideal.span_pair_add_mul_right {R : Type u} [comm_ring R] {x y : R} (z : R) :

ideal.span {x, y + x * z} = ideal.span {x, y}

source

theorem ideal.is_maximal.exists_inv {α : Type u} [semiring α] {I : ideal α} (hI : I.is_maximal) {x : α} (hx : x ∉ I) :

∃ (y i : α) (H : i ∈ I), y * x + i = 1

source

theorem ideal.mem_sup_left {R : Type u} [semiring R] {S T : ideal R} {x : R} :

x ∈ S → x ∈ S ⊔ T

source

theorem ideal.mem_sup_right {R : Type u} [semiring R] {S T : ideal R} {x : R} :

x ∈ T → x ∈ S ⊔ T

source

theorem ideal.mem_supr_of_mem {R : Type u} [semiring R] {ι : Sort u_1} {S : ι → ideal R} (i : ι) {x : R} :

x ∈ S i → x ∈ supr S

source

theorem ideal.mem_Sup_of_mem {R : Type u} [semiring R] {S : set (ideal R)} {s : ideal R} (hs : s ∈ S) {x : R} :

x ∈ s → x ∈ has_Sup.Sup S

source

theorem ideal.mem_Inf {R : Type u} [semiring R] {s : set (ideal R)} {x : R} :

x ∈ has_Inf.Inf s ↔ ∀ ⦃I : ideal R⦄, I ∈ s → x ∈ I

source

@[simp]

theorem ideal.mem_inf {R : Type u} [semiring R] {I J : ideal R} {x : R} :

x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J

source

@[simp]

theorem ideal.mem_infi {R : Type u} [semiring R] {ι : Sort u_1} {I : ι → ideal R} {x : R} :

x ∈ infi I ↔ ∀ (i : ι), x ∈ I i

source

@[simp]

theorem ideal.mem_bot {R : Type u} [semiring R] {x : R} :

x ∈ ⊥ ↔ x = 0

source

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' := _}

source

theorem ideal.mem_pi {α : Type u} [semiring α] (I : ideal α) (ι : Type v) (x : ι → α) :

x ∈ I.pi ι ↔ ∀ (i : ι), x i ∈ I

source

theorem ideal.Inf_is_prime_of_is_chain {α : Type u} [semiring α] {s : set (ideal α)} (hs : s.nonempty) (hs' : is_chain has_le.le s) (H : ∀ (p : ideal α), p ∈ s → p.is_prime) :

(has_Inf.Inf s).is_prime

source

@[simp]

theorem ideal.mul_unit_mem_iff_mem {α : Type u} [comm_semiring α] (I : ideal α) {x y : α} (hy : is_unit y) :

x * y ∈ I ↔ x ∈ I

source

theorem ideal.mem_span_singleton {α : Type u} [comm_semiring α] {x y : α} :

x ∈ ideal.span {y} ↔ y ∣ x

source

theorem ideal.mem_span_singleton_self {α : Type u} [comm_semiring α] (x : α) :

x ∈ ideal.span {x}

source

theorem ideal.span_singleton_le_span_singleton {α : Type u} [comm_semiring α] {x y : α} :

ideal.span {x} ≤ ideal.span {y} ↔ y ∣ x

source

theorem ideal.span_singleton_eq_span_singleton {α : Type u} [comm_ring α] [is_domain α] {x y : α} :

ideal.span {x} = ideal.span {y} ↔ associated x y

source

theorem ideal.span_singleton_mul_right_unit {α : Type u} [comm_semiring α] {a : α} (h2 : is_unit a) (x : α) :

ideal.span {x * a} = ideal.span {x}

source

theorem ideal.span_singleton_eq_top {α : Type u} [comm_semiring α] {x : α} :

ideal.span {x} = ⊤ ↔ is_unit x

source

theorem ideal.span_singleton_prime {α : Type u} [comm_semiring α] {p : α} (hp : p ≠ 0) :

(ideal.span {p}).is_prime ↔ prime p

source

theorem ideal.is_maximal.is_prime {α : Type u} [comm_semiring α] {I : ideal α} (H : I.is_maximal) :

I.is_prime

source

@[protected, instance]

def ideal.is_maximal.is_prime' {α : Type u} [comm_semiring α] (I : ideal α) [H : I.is_maximal] :

I.is_prime

source

theorem ideal.span_singleton_lt_span_singleton {β : Type v} [comm_ring β] [is_domain β] {x y : β} :

ideal.span {x} < ideal.span {y} ↔ dvd_not_unit y x

source

theorem ideal.factors_decreasing {β : Type v} [comm_ring β] [is_domain β] (b₁ b₂ : β) (h₁ : b₁ ≠ 0) (h₂ : ¬is_unit b₂) :

ideal.span {b₁ * b₂} < ideal.span {b₁}

source

theorem ideal.mul_mem_right {α : Type u} {a : α} (b : α) [comm_semiring α] (I : ideal α) (h : a ∈ I) :

a * b ∈ I

source

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

a ^ n ∈ I

source

theorem ideal.is_prime.mul_mem_iff_mem_or_mem {α : Type u} [comm_semiring α] {I : ideal α} (hI : I.is_prime) {x y : α} :

x * y ∈ I ↔ x ∈ I ∨ y ∈ I

source

theorem ideal.is_prime.pow_mem_iff_mem {α : Type u} [comm_semiring α] {I : ideal α} (hI : I.is_prime) {r : α} (n : ℕ) (hn : 0 < n) :

r ^ n ∈ I ↔ r ∈ I

source

theorem ideal.pow_multiset_sum_mem_span_pow {α : Type u} [comm_semiring α] (s : multiset α) (n : ℕ) :

s.sum ^ (⇑multiset.card s * n + 1) ∈ ideal.span ↑((multiset.map (λ (x : α), x ^ (n + 1)) s).to_finset)

source

theorem ideal.sum_pow_mem_span_pow {α : Type u} [comm_semiring α] {ι : Type u_1} (s : finset ι) (f : ι → α) (n : ℕ) :

s.sum (λ (i : ι), f i) ^ (s.card * n + 1) ∈ ideal.span ((λ (i : ι), f i ^ (n + 1)) '' ↑s)

source

theorem ideal.span_pow_eq_top {α : Type u} [comm_semiring α] (s : set α) (hs : ideal.span s = ⊤) (n : ℕ) :

ideal.span ((λ (x : α), x ^ n) '' s) = ⊤

source

@[protected]

theorem ideal.neg_mem_iff {α : Type u} [ring α] (I : ideal α) {a : α} :

-a ∈ I ↔ a ∈ I

source

@[protected]

theorem ideal.add_mem_iff_left {α : Type u} [ring α] (I : ideal α) {a b : α} :

b ∈ I → (a + b ∈ I ↔ a ∈ I)

source

@[protected]

theorem ideal.add_mem_iff_right {α : Type u} [ring α] (I : ideal α) {a b : α} :

a ∈ I → (a + b ∈ I ↔ b ∈ I)

source

@[protected]

theorem ideal.sub_mem {α : Type u} [ring α] (I : ideal α) {a b : α} :

a ∈ I → b ∈ I → a - b ∈ I

source

theorem ideal.mem_span_insert' {α : Type u} [ring α] {s : set α} {x y : α} :

x ∈ ideal.span (has_insert.insert y s) ↔ ∃ (a : α), x + a * y ∈ ideal.span s

source

@[simp]

theorem ideal.span_singleton_neg {α : Type u} [ring α] (x : α) :

ideal.span {-x} = ideal.span {x}

source

theorem ideal.eq_bot_or_top {K : Type u} [division_semiring K] (I : ideal K) :

I = ⊥ ∨ I = ⊤

All ideals in a division (semi)ring are trivial.

source

@[protected, instance]

def ideal.is_simple_order {K : Type u} [division_semiring K] :

is_simple_order (ideal K)

Ideals of a division_semiring are a simple order. Thanks to the way abbreviations work, this automatically gives a is_simple_module K instance.

source

theorem ideal.eq_bot_of_prime {K : Type u} [division_semiring K] (I : ideal K) [h : I.is_prime] :

I = ⊥

source

theorem ideal.bot_is_maximal {K : Type u} [division_semiring K] :

⊥.is_maximal

source

theorem ideal.mul_sub_mul_mem {R : Type u_1} [comm_ring R] (I : ideal R) {a b c d : R} (h1 : a - b ∈ I) (h2 : c - d ∈ I) :

a * c - b * d ∈ I

source

theorem ring.exists_not_is_unit_of_not_is_field {R : Type u_1} [comm_semiring R] [nontrivial R] (hf : ¬is_field R) :

∃ (x : R) (H : x ≠ 0), ¬is_unit x

source

theorem ring.not_is_field_iff_exists_ideal_bot_lt_and_lt_top {R : Type u_1} [comm_semiring R] [nontrivial R] :

¬is_field R ↔ ∃ (I : ideal R), ⊥ < I ∧ I < ⊤

source

theorem ring.not_is_field_iff_exists_prime {R : Type u_1} [comm_semiring R] [nontrivial R] :

¬is_field R ↔ ∃ (p : ideal R), p ≠ ⊥ ∧ p.is_prime

source

theorem ring.is_field_iff_is_simple_order_ideal {R : Type u_1} [comm_semiring R] :

is_field R ↔ is_simple_order (ideal R)

Also see ideal.is_simple_order 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.

source

theorem ring.ne_bot_of_is_maximal_of_not_is_field {R : Type u_1} [comm_semiring R] [nontrivial R] {M : ideal R} (max : M.is_maximal) (not_field : ¬is_field R) :

M ≠ ⊥

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

source

theorem ideal.bot_lt_of_maximal {R : Type u} [comm_ring R] [nontrivial R] (M : ideal R) [hm : M.is_maximal] (non_field : ¬is_field R) :

⊥ < M

source

def nonunits (α : Type u) [monoid α] :

set α

The set of non-invertible elements of a monoid.

Equations

nonunits α = {a : α | ¬is_unit a}

source

@[simp]

theorem mem_nonunits_iff {α : Type u} {a : α} [monoid α] :

a ∈ nonunits α ↔ ¬is_unit a

source

theorem mul_mem_nonunits_right {α : Type u} {a b : α} [comm_monoid α] :

b ∈ nonunits α → a * b ∈ nonunits α

source

theorem mul_mem_nonunits_left {α : Type u} {a b : α} [comm_monoid α] :

a ∈ nonunits α → a * b ∈ nonunits α

source

theorem zero_mem_nonunits {α : Type u} [semiring α] :

0 ∈ nonunits α ↔ 0 ≠ 1

source

@[simp]

theorem one_not_mem_nonunits {α : Type u} [monoid α] :

1 ∉ nonunits α

source

theorem coe_subset_nonunits {α : Type u} [semiring α] {I : ideal α} (h : I ≠ ⊤) :

↑I ⊆ nonunits α

source

theorem exists_max_ideal_of_mem_nonunits {α : Type u} {a : α} [comm_semiring α] (h : a ∈ nonunits α) :

∃ (I : ideal α), I.is_maximal ∧ a ∈ I

mathlib3 documentation

Ideals over a ring #

Implementation notes #

TODO #