Ideals generated by a set of elements

This file defines Ideal.span s as the ideal generated by the subset s of the ring.

TODO

Support right ideals, and two-sided ideals over non-commutative rings.

class IsPrincipalIdealRing (R : Type u) [Semiring R] : Prop

A ring is a principal ideal ring if all (left) ideals are principal.

• principal (S : Ideal R) : Submodule.IsPrincipal S

theorem isPrincipalIdealRing_iff (R : Type u) [Semiring R] : IsPrincipalIdealRing R ↔ ∀ (S : Ideal R), Submodule.IsPrincipal S

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 = span s

@[simp]

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

theorem Ideal.mem_span_singleton_sup {α : Type u} [Semiring α] {x y : α} {I : Ideal α} : x ∈ span {y} ⊔ I ↔ ∃ (a : α), ∃ 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 : α), r a b ∧ x + b = a}

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

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

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

@[simp]

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

theorem IsIdempotentElem.ker_toSpanSingleton_eq_span {R : Type u_1} [CommRing R] {e : R} (he : IsIdempotentElem e) : LinearMap.ker (LinearMap.toSpanSingleton R R e) = Ideal.span {1 - e}

theorem IsIdempotentElem.ker_toSpanSingleton_one_sub_eq_span {R : Type u_1} [CommRing R] {e : R} (he : IsIdempotentElem e) : LinearMap.ker (LinearMap.toSpanSingleton R R (1 - e)) = Ideal.span {e}