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

@[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.iSup_eq_span {α : Type u} [Semiring α] {ι : Sort u_1} (p : ι → Ideal α) : ⨆ (i : ι), p i = span (⋃ (i : ι), ↑(p 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 α] : 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_range_self {α : Type u} [Semiring α] {β : Type u_1} {f : β → α} {x : β} : f x ∈ span (Set.range f)

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}

@[simp]

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

@[simp]

theorem Ideal.span_singleton_zero {α : Type u} [Semiring α] : span {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_insert_zero {α : Type u} [Semiring α] {s : Set α} : span (insert 0 s) = span s

@[simp]

theorem Ideal.span_sdiff_singleton_zero {α : Type u} [Semiring α] {s : Set α} : span (s \ {0}) = span s

@[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.

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_zero {α : Type u} [Semiring α] (x : α) : span {x, 0} = span {x}

theorem Ideal.span_range_eq_iSup {α : Type u} [Semiring α] {ι : Type u_1} (x : ι → α) : span (Set.range x) = ⨆ (i : ι), span {x i}

theorem Ideal.span_range_eq_span_range_support {α : Type u} [Semiring α] {ι : Type u_1} (x : ι → α) : span (Set.range x) = span (Set.range fun (i : ↑(Function.support x)) => x ↑i)

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

@[simp]

theorem Ideal.span_pair_eq_span_left_iff_dvd {α : Type u} [CommSemiring α] {x y : α} : span {x, y} = span {x} ↔ x ∣ y

@[simp]

theorem Ideal.span_pair_eq_span_right_iff_dvd {α : Type u} [CommSemiring α] {x y : α} : span {x, y} = span {y} ↔ y ∣ x

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_iff_of_associated {α : Type u} [CommSemiring α] {I : Ideal α} {x y : α} (h : Associated x y) : x ∈ I ↔ y ∈ I

theorem Ideal.mem_span_insert' {α : Type u} [Ring α] (x y : α) (s : Set α) : 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}

@[simp]

theorem Ideal.span_insert_neg {α : Type u} [Ring α] (x : α) (s : Set α) : span (insert (-x) s) = span (insert x s)

@[simp]

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

@[simp]

theorem Ideal.span_pair_add_right {α : Type u} [Ring α] (x y : α) : span {x + y, y} = span {x, y}

@[simp]

theorem Ideal.span_pair_add_left {α : Type u} [Ring α] (x y : α) : span {x, y + x} = span {x, y}

@[simp]

theorem Ideal.span_pair_right_add {α : Type u} [Ring α] (x y : α) : span {y + x, y} = span {x, y}

@[simp]

theorem Ideal.span_pair_left_add {α : Type u} [Ring α] (x y : α) : span {x, x + y} = span {x, y}

@[simp]

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

@[simp]

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

@[simp]

theorem Ideal.span_pair_sub_right' {α : Type u} [Ring α] (x y : α) : span {x, x - y} = span {x, y}

@[simp]

theorem Ideal.span_pair_sub_left' {α : Type u} [Ring α] (x y : α) : span {y - x, y} = span {x, y}

@[simp]

theorem Ideal.span_singleton_abs {α : Type u} [Ring α] (x : α) [LinearOrder α] : span {|x|} = span {x}

@[simp]

theorem Ideal.span_insert_abs {α : Type u} [Ring α] (x : α) (s : Set α) [LinearOrder α] : span (insert |x| s) = span (insert x s)

@[simp]

theorem Ideal.span_pair_abs {α : Type u} [Ring α] (x y : α) [LinearOrder α] : span {x, |y|} = span {x, y}

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Ideal.span_pair_sub_right_mul {α : Type u} [CommRing α] (x y z : α) : span {x - y * z, y} = span {x, y}

@[simp]

theorem Ideal.span_pair_sub_left_mul {α : Type u} [CommRing α] (x y z : α) : span {x, y - x * z} = span {x, y}

@[simp]

theorem Ideal.span_pair_sub_mul_right {α : Type u} [CommRing α] (x y z : α) : span {x - z * y, y} = span {x, y}

@[simp]

theorem Ideal.span_pair_sub_mul_left {α : Type u} [CommRing α] (x y z : α) : span {x, y - z * x} = span {x, y}

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

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

instance instIsPrincipalSpanSingletonSet {R : Type u_1} [Semiring R] {x : R} : Submodule.IsPrincipal (Ideal.span {x})