Mathlib.RingTheory.Ideal.Span

IsPrincipalIdealRing structure

(R : Type u) [Semiring R]

Full source

/-- A ring is a principal ideal ring if all (left) ideals are principal. -/
@[mk_iff]
class IsPrincipalIdealRing (R : Type u) [Semiring R] : Prop where
  principal : ∀ S : Ideal R, S.IsPrincipal

Principal Ideal Ring

Informal description

A ring $R$ is called a *principal ideal ring* if every (left) ideal in $R$ is principal, i.e., generated by a single element.

Ideal.span definition

(s : Set α) : Ideal α

Full source

/-- The ideal generated by a subset of a ring -/
def span (s : Set α) : Ideal α :=
  Submodule.span α s

Ideal generated by a set

Informal description

The ideal generated by a subset $ s $ of a ring $ \alpha $ is the smallest ideal containing $ s $, consisting of all finite linear combinations of elements from $ s $ with coefficients in $ \alpha $.

Ideal.submodule_span_eq theorem

{s : Set α} : Submodule.span α s = Ideal.span s

Full source

@[simp]
theorem submodule_span_eq {s : Set α} : Submodule.span α s = Ideal.span s :=
  rfl

Equality of Submodule Span and Ideal Span in a Ring

Informal description

For any subset $s$ of a ring $\alpha$, the submodule span of $s$ over $\alpha$ is equal to the ideal generated by $s$.

Ideal.span_empty theorem

: span (∅ : Set α) = ⊥

Full source

@[simp]
theorem span_empty : span (∅ : Set α) = ⊥ :=
  Submodule.span_empty

Empty Set Generates Trivial Ideal

Informal description

The ideal generated by the empty set in a ring $\alpha$ is the trivial ideal, i.e., $\operatorname{span}(\emptyset) = \bot$.

Ideal.span_univ theorem

: span (Set.univ : Set α) = ⊤

Full source

@[simp]
theorem span_univ : span (Set.univ : Set α) = ⊤ :=
  Submodule.span_univ

Universal Set Generates Entire Ideal

Informal description

The ideal generated by the universal set in a ring $\alpha$ is equal to the entire ring, i.e., $\operatorname{span}(\text{univ} : \text{Set } \alpha) = \top$.

Ideal.span_union theorem

(s t : Set α) : span (s ∪ t) = span s ⊔ span t

Full source

theorem span_union (s t : Set α) : span (s ∪ t) = spanspan s ⊔ span t :=
  Submodule.span_union _ _

Span of Union Equals Supremum of Spans in Ideal Lattice

Informal description

For any subsets $s$ and $t$ of a ring $\alpha$, the ideal generated by their union $s \cup t$ is equal to the supremum of the ideals generated by $s$ and $t$ individually, i.e., \[ \operatorname{span}(s \cup t) = \operatorname{span}(s) \sqcup \operatorname{span}(t). \]

Ideal.span_iUnion theorem

{ι} (s : ι → Set α) : span (⋃ i, s i) = ⨆ i, span (s i)

Full source

theorem span_iUnion {ι} (s : ι → Set α) : span (⋃ i, s i) = ⨆ i, span (s i) :=
  Submodule.span_iUnion _

Span of Union Equals Supremum of Spans in Ideal Lattice

Informal description

For any indexed family of subsets $s_i$ of a ring $\alpha$, the ideal generated by their union equals the supremum of the ideals generated by each individual subset: \[ \operatorname{span}\left(\bigcup_i s_i\right) = \bigsqcup_i \operatorname{span}(s_i). \]

Ideal.mem_span theorem

{s : Set α} (x) : x ∈ span s ↔ ∀ p : Ideal α, s ⊆ p → x ∈ p

Full source

theorem mem_span {s : Set α} (x) : x ∈ span sx ∈ span s ↔ ∀ p : Ideal α, s ⊆ p → x ∈ p :=
  mem_iInter₂

Characterization of Membership in Ideal Span

Informal description

For any subset $s$ of a ring $\alpha$ and any element $x \in \alpha$, $x$ belongs to the ideal generated by $s$ if and only if for every ideal $p$ of $\alpha$ containing $s$, $x$ belongs to $p$. In symbols: $$x \in \text{span}(s) \leftrightarrow \forall p \trianglelefteq \alpha,\ s \subseteq p \to x \in p$$

Ideal.subset_span theorem

{s : Set α} : s ⊆ span s

Full source

theorem subset_span {s : Set α} : s ⊆ span s :=
  Submodule.subset_span

Ideal Span Contains Generating Set

Informal description

For any subset $s$ of a ring $\alpha$, the ideal generated by $s$ contains $s$, i.e., $s \subseteq \operatorname{span}(s)$.

Ideal.span_le theorem

{s : Set α} {I} : span s ≤ I ↔ s ⊆ I

Full source

theorem span_le {s : Set α} {I} : spanspan s ≤ I ↔ s ⊆ I :=
  Submodule.span_le

Ideal containment criterion: $\operatorname{span}(s) \leq I \leftrightarrow s \subseteq I$

Informal description

For any subset $s$ of a ring $\alpha$ and any ideal $I$ of $\alpha$, the ideal generated by $s$ is contained in $I$ if and only if $s$ is a subset of $I$. In symbols: $$\operatorname{span}(s) \leq I \leftrightarrow s \subseteq I$$

Ideal.span_mono theorem

{s t : Set α} : s ⊆ t → span s ≤ span t

Full source

theorem span_mono {s t : Set α} : s ⊆ t → span s ≤ span t :=
  Submodule.span_mono

Monotonicity of Ideal Span: $s \subseteq t \Rightarrow \operatorname{span}(s) \leq \operatorname{span}(t)$

Informal description

For any subsets $s$ and $t$ of a ring $\alpha$, if $s \subseteq t$, then the ideal generated by $s$ is contained in the ideal generated by $t$, i.e., $\operatorname{span}(s) \leq \operatorname{span}(t)$.

Ideal.span_eq theorem

: span (I : Set α) = I

Full source

@[simp]
theorem span_eq : span (I : Set α) = I :=
  Submodule.span_eq _

Ideal Span of an Ideal Equals Itself

Informal description

For any ideal $I$ of a ring $\alpha$, the ideal generated by $I$ (viewed as a subset of $\alpha$) is equal to $I$ itself, i.e., $\operatorname{span}(I) = I$.

Ideal.span_singleton_one theorem

: span ({ 1 } : Set α) = ⊤

Full source

@[simp]
theorem span_singleton_one : span ({1} : Set α) = ⊤ :=
  (eq_top_iff_one _).2 <| subset_span <| mem_singleton _

Ideal Generated by the Unit Element is the Whole Ring

Informal description

The ideal generated by the singleton set $\{1\}$ in a ring $\alpha$ is equal to the entire ring, i.e., $\operatorname{span}(\{1\}) = \top$.

Ideal.isCompactElement_top theorem

: CompleteLattice.IsCompactElement (⊤ : Ideal α)

Full source

theorem isCompactElement_top : CompleteLattice.IsCompactElement (⊤ : Ideal α) := by
  simpa only [← span_singleton_one] using Submodule.singleton_span_isCompactElement 1

Compactness of the Top Ideal in a Ring's Lattice of Ideals

Informal description

The top element (the entire ring) in the lattice of ideals of a ring $\alpha$ is a compact element.

Ideal.mem_span_insert theorem

{s : Set α} {x y} : x ∈ span (insert y s) ↔ ∃ a, ∃ z ∈ span s, x = a * y + z

Full source

theorem mem_span_insert {s : Set α} {x y} :
    x ∈ span (insert y s)x ∈ span (insert y s) ↔ ∃ a, ∃ z ∈ span s, x = a * y + z :=
  Submodule.mem_span_insert

Characterization of Membership in Ideal Generated by Inserted Set: $x \in \text{span}(\{y\} \cup s) \leftrightarrow \exists a \in \alpha, \exists z \in \text{span}(s), x = a y + z$

Informal description

For any elements $x, y$ in a ring $\alpha$ and any subset $s \subseteq \alpha$, the element $x$ belongs to the ideal generated by $\{y\} \cup s$ if and only if there exists an element $a \in \alpha$ and an element $z$ in the ideal generated by $s$ such that $x = a \cdot y + z$.

Ideal.mem_span_singleton' theorem

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

Full source

theorem mem_span_singleton' {x y : α} : x ∈ span ({y} : Set α)x ∈ span ({y} : Set α) ↔ ∃ a, a * y = x :=
  Submodule.mem_span_singleton

Characterization of Membership in Ideal Generated by Singleton: $x \in \text{span}(\{y\}) \leftrightarrow \exists a \in \alpha, a \cdot y = x$

Informal description

For any elements $x$ and $y$ in a ring $\alpha$, the element $x$ belongs to the ideal generated by $\{y\}$ if and only if there exists an element $a \in \alpha$ such that $a \cdot y = x$.

Ideal.mem_span_singleton_self theorem

(x : α) : x ∈ span ({ x } : Set α)

Full source

theorem mem_span_singleton_self (x : α) : x ∈ span ({x} : Set α) :=
  Submodule.mem_span_singleton_self x

Self-Containment in Ideal Generated by Singleton: $x \in \text{span}(\{x\})$

Informal description

For any element $x$ in a ring $\alpha$, the element $x$ is contained in the ideal generated by the singleton set $\{x\}$, i.e., $x \in \text{span}(\{x\})$.

Ideal.span_singleton_le_iff_mem theorem

{x : α} : span { x } ≤ I ↔ x ∈ I

Full source

theorem span_singleton_le_iff_mem {x : α} : spanspan {x} ≤ I ↔ x ∈ I :=
  Submodule.span_singleton_le_iff_mem _ _

Containment of Singleton-Generated Ideal in Ideal $I$ is Equivalent to Membership of $x$ in $I$

Informal description

For any element $x$ in a ring $\alpha$ and any ideal $I$ of $\alpha$, the ideal generated by the singleton set $\{x\}$ is contained in $I$ if and only if $x$ belongs to $I$. In other words: $$\text{span}(\{x\}) \leq I \leftrightarrow x \in I$$

Ideal.span_singleton_mul_left_unit theorem

{a : α} (h2 : IsUnit a) (x : α) : span ({a * x} : Set α) = span { x }

Full source

theorem span_singleton_mul_left_unit {a : α} (h2 : IsUnit a) (x : α) :
    span ({a * x} : Set α) = span {x} := by
  apply le_antisymm <;> rw [span_singleton_le_iff_mem, mem_span_singleton']
  exacts [⟨a, rfl⟩, ⟨_, h2.unit.inv_mul_cancel_left x⟩]

Equality of ideals generated by $a \cdot x$ and $x$ for invertible $a$

Informal description

For any element $a$ in a ring $\alpha$ that is a unit (i.e., invertible), and for any element $x \in \alpha$, the ideal generated by the singleton set $\{a \cdot x\}$ is equal to the ideal generated by the singleton set $\{x\}$. In other words: $$\operatorname{span}(\{a \cdot x\}) = \operatorname{span}(\{x\}).$$

Ideal.span_insert theorem

(x) (s : Set α) : span (insert x s) = span ({ x } : Set α) ⊔ span s

Full source

theorem span_insert (x) (s : Set α) : span (insert x s) = spanspan ({x} : Set α) ⊔ span s :=
  Submodule.span_insert x s

Span of Insertion Equals Supremum of Singleton Span and Set Span

Informal description

For any element $x$ in a ring $\alpha$ and any subset $s \subseteq \alpha$, the ideal generated by the set $\{x\} \cup s$ is equal to the supremum of the ideal generated by $\{x\}$ and the ideal generated by $s$, i.e., $$\operatorname{span}(\{x\} \cup s) = \operatorname{span}(\{x\}) \sqcup \operatorname{span}(s).$$

Ideal.span_eq_bot theorem

{s : Set α} : span s = ⊥ ↔ ∀ x ∈ s, (x : α) = 0

Full source

theorem span_eq_bot {s : Set α} : spanspan s = ⊥ ↔ ∀ x ∈ s, (x : α) = 0 :=
  Submodule.span_eq_bot

Characterization of Zero Ideal via Span of a Set

Informal description

For any subset $s$ of a ring $\alpha$, the ideal generated by $s$ is the zero ideal if and only if every element $x \in s$ is zero, i.e., $$\operatorname{span}(s) = 0 \leftrightarrow \forall x \in s, x = 0.$$

Ideal.span_singleton_eq_bot theorem

{x} : span ({ x } : Set α) = ⊥ ↔ x = 0

Full source

@[simp]
theorem span_singleton_eq_bot {x} : spanspan ({x} : Set α) = ⊥ ↔ x = 0 :=
  Submodule.span_singleton_eq_bot

Span of Singleton is Zero Ideal if and only if Element is Zero

Informal description

For any element $x$ in a ring $\alpha$, the ideal generated by the singleton set $\{x\}$ is the zero ideal if and only if $x$ is zero, i.e., $\mathrm{span}(\{x\}) = 0 \leftrightarrow x = 0$.

Ideal.span_singleton_ne_top theorem

{α : Type*} [CommSemiring α] {x : α} (hx : ¬IsUnit x) : Ideal.span ({ x } : Set α) ≠ ⊤

Full source

theorem span_singleton_ne_top {α : Type*} [CommSemiring α] {x : α} (hx : ¬IsUnit x) :
    Ideal.spanIdeal.span ({x} : Set α) ≠ ⊤ :=
  (Ideal.ne_top_iff_one _).mpr fun h1 =>
    let ⟨y, hy⟩ := Ideal.mem_span_singleton'.mp h1
    hx ⟨⟨x, y, mul_comm y x ▸ hy, hy⟩, rfl⟩

Non-unit elements generate proper ideals in commutative semirings

Informal description

Let $\alpha$ be a commutative semiring and $x \in \alpha$ be a non-unit element. Then the ideal generated by the singleton set $\{x\}$ is not equal to the entire ring $\alpha$.

Ideal.span_zero theorem

: span (0 : Set α) = ⊥

Full source

@[simp]
theorem span_zero : span (0 : Set α) = ⊥ := by rw [← Set.singleton_zero, span_singleton_eq_bot]

Span of Zero is Zero Ideal

Informal description

The ideal generated by the singleton set $\{0\}$ in a ring $\alpha$ is equal to the zero ideal, i.e., $\mathrm{span}(\{0\}) = 0$.

Ideal.span_one theorem

: span (1 : Set α) = ⊤

Full source

@[simp]
theorem span_one : span (1 : Set α) = ⊤ := by rw [← Set.singleton_one, span_singleton_one]

Ideal Generated by the Unit Element is the Whole Ring

Informal description

The ideal generated by the singleton set $\{1\}$ in a ring $\alpha$ is equal to the entire ring, i.e., $\operatorname{span}(\{1\}) = \top$.

Ideal.span_eq_top_iff_finite theorem

(s : Set α) : span s = ⊤ ↔ ∃ s' : Finset α, ↑s' ⊆ s ∧ span (s' : Set α) = ⊤

Full source

theorem span_eq_top_iff_finite (s : Set α) :
    spanspan s = ⊤ ↔ ∃ s' : Finset α, ↑s' ⊆ s ∧ span (s' : Set α) = ⊤ := by
  simp_rw [eq_top_iff_one]
  exact ⟨Submodule.mem_span_finite_of_mem_span, fun ⟨s', h₁, h₂⟩ => span_mono h₁ h₂⟩

Finite Generation Criterion for Unit Ideal: $\operatorname{span}(s) = \top \Leftrightarrow \exists$ finite $s' \subseteq s$ with $\operatorname{span}(s') = \top$

Informal description

For any subset $s$ of a ring $\alpha$, the ideal generated by $s$ is equal to the entire ring if and only if there exists a finite subset $s' \subseteq s$ such that the ideal generated by $s'$ is also equal to the entire ring.

Ideal.mem_span_singleton_sup theorem

{x y : α} {I : Ideal α} : x ∈ Ideal.span { y } ⊔ I ↔ ∃ a : α, ∃ b ∈ I, a * y + b = x

Full source

theorem mem_span_singleton_sup {x y : α} {I : Ideal α} :
    x ∈ Ideal.span {y} ⊔ Ix ∈ Ideal.span {y} ⊔ I ↔ ∃ a : α, ∃ b ∈ I, a * y + b = x := by
  rw [Submodule.mem_sup]
  constructor
  · rintro ⟨ya, hya, b, hb, rfl⟩
    obtain ⟨a, rfl⟩ := mem_span_singleton'.mp hya
    exact ⟨a, b, hb, rfl⟩
  · rintro ⟨a, b, hb, rfl⟩
    exact ⟨a * y, Ideal.mem_span_singleton'.mpr ⟨a, rfl⟩, b, hb, rfl⟩

Membership in Ideal Generated by Singleton Union Another Ideal via Linear Combination

Informal description

For any elements $x, y$ in a ring $\alpha$ and any ideal $I$ of $\alpha$, the element $x$ belongs to the ideal generated by $\{y\}$ combined with $I$ if and only if there exist elements $a \in \alpha$ and $b \in I$ such that $x = a \cdot y + b$.

Ideal.ofRel definition

(r : α → α → Prop) : Ideal α

Full source

/-- The ideal generated by an arbitrary binary relation.
-/
def ofRel (r : α → α → Prop) : Ideal α :=
  Submodule.span α { x | ∃ a b, r a b ∧ x + b = a }

Ideal generated by a relation

Informal description

Given a binary relation $r$ on a ring $\alpha$, the ideal generated by $r$ is the smallest ideal containing all elements of the form $a - b$ where $r(a, b)$ holds. In other words, it is the span of the set $\{x \mid \exists a b, r(a, b) \text{ and } x = a - b\}$.

Ideal.zero_ne_one_of_proper theorem

{I : Ideal α} (h : I ≠ ⊤) : (0 : α) ≠ 1

Full source

theorem zero_ne_one_of_proper {I : Ideal α} (h : I ≠ ⊤) : (0 : α) ≠ 1 := fun hz =>
  I.ne_top_iff_one.1 h <| hz ▸ I.zero_mem

Non-triviality of Proper Ideals: $0 \neq 1$

Informal description

For any proper ideal $I$ in a ring $\alpha$ (i.e., $I \neq \top$), the zero element $0$ is not equal to the multiplicative identity $1$.

Ideal.span_pair_comm theorem

{x y : α} : (span { x, y } : Ideal α) = span { y, x }

Full source

theorem span_pair_comm {x y : α} : (span {x, y} : Ideal α) = span {y, x} := by
  simp only [span_insert, sup_comm]

Commutativity of Ideal Generation for Pairs: $\langle x, y \rangle = \langle y, x \rangle$

Informal description

For any elements $x$ and $y$ in a ring $\alpha$, the ideal generated by the set $\{x, y\}$ is equal to the ideal generated by $\{y, x\}$.

Ideal.mem_span_pair theorem

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

Full source

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

Characterization of Elements in the Ideal Generated by a Pair: $z \in \langle x, y \rangle \leftrightarrow \exists a, b, z = a x + b y$

Informal description

For any elements $x, y, z$ in a ring $\alpha$, the element $z$ belongs to the ideal generated by $\{x, y\}$ if and only if there exist elements $a, b \in \alpha$ such that $z = a \cdot x + b \cdot y$.

Ideal.span_pair_add_mul_left theorem

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

Full source

@[simp]
theorem span_pair_add_mul_left {R : Type u} [CommRing R] {x y : R} (z : R) :
    (span {x + y * z, y} : Ideal R) = span {x, y} := by
  ext
  rw [mem_span_pair, mem_span_pair]
  exact
    ⟨fun ⟨a, b, h⟩ =>
      ⟨a, b + a * z, by
        rw [← h]
        ring1⟩,
      fun ⟨a, b, h⟩ =>
      ⟨a, b - a * z, by
        rw [← h]
        ring1⟩⟩

Ideal Equality: $\langle x + y z, y \rangle = \langle x, y \rangle$ in a Commutative Ring

Informal description

Let $R$ be a commutative ring, and let $x, y, z \in R$. The ideal generated by $\{x + y \cdot z, y\}$ is equal to the ideal generated by $\{x, y\}$.

Ideal.span_pair_add_mul_right theorem

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

Full source

@[simp]
theorem span_pair_add_mul_right {R : Type u} [CommRing R] {x y : R} (z : R) :
    (span {x, y + x * z} : Ideal R) = span {x, y} := by
  rw [span_pair_comm, span_pair_add_mul_left, span_pair_comm]

Ideal Equality: $\langle x, y + x z \rangle = \langle x, y \rangle$ in a Commutative Ring

Informal description

Let $R$ be a commutative ring, and let $x, y, z \in R$. The ideal generated by $\{x, y + x \cdot z\}$ is equal to the ideal generated by $\{x, y\}$.

Ideal.mem_span_singleton theorem

{x y : α} : x ∈ span ({ y } : Set α) ↔ y ∣ x

Full source

theorem mem_span_singleton {x y : α} : x ∈ span ({y} : Set α)x ∈ span ({y} : Set α) ↔ y ∣ x :=
  mem_span_singleton'.trans <| exists_congr fun _ => by rw [eq_comm, mul_comm]

Membership in Principal Ideal via Divisibility: $x \in \langle y \rangle \leftrightarrow y \mid x$

Informal description

For any elements $x$ and $y$ in a ring $\alpha$, the element $x$ belongs to the ideal generated by $\{y\}$ if and only if $y$ divides $x$ in $\alpha$.

Ideal.span_singleton_le_span_singleton theorem

{x y : α} : span ({ x } : Set α) ≤ span ({ y } : Set α) ↔ y ∣ x

Full source

theorem span_singleton_le_span_singleton {x y : α} :
    spanspan ({x} : Set α) ≤ span ({y} : Set α) ↔ y ∣ x :=
  span_le.trans <| singleton_subset_iff.trans mem_span_singleton

Containment of Principal Ideals via Divisibility: $\langle x \rangle \subseteq \langle y \rangle \leftrightarrow y \mid x$

Informal description

For any elements $x$ and $y$ in a ring $\alpha$, the ideal generated by $\{x\}$ is contained in the ideal generated by $\{y\}$ if and only if $y$ divides $x$ in $\alpha$. In symbols: $$\langle x \rangle \subseteq \langle y \rangle \leftrightarrow y \mid x$$

Ideal.span_singleton_eq_span_singleton theorem

 {α : Type u} [CommSemiring α] [IsDomain α] {x y : α} : span ({ x } : Set α) = span ({ y } : Set α) ↔ Associated x y

Full source

theorem span_singleton_eq_span_singleton {α : Type u} [CommSemiring α] [IsDomain α] {x y : α} :
    spanspan ({x} : Set α) = span ({y} : Set α) ↔ Associated x y := by
  rw [← dvd_dvd_iff_associated, le_antisymm_iff, and_comm]
  apply and_congr <;> rw [span_singleton_le_span_singleton]

Equality of Principal Ideals via Associated Elements: $\langle x \rangle = \langle y \rangle \leftrightarrow x \sim y$

Informal description

Let $\alpha$ be a commutative semiring with no zero divisors, and let $x, y \in \alpha$. The ideal generated by $\{x\}$ is equal to the ideal generated by $\{y\}$ if and only if $x$ and $y$ are associated elements (i.e., there exists a unit $u$ such that $x = u \cdot y$ or $y = u \cdot x$). In symbols: $$\langle x \rangle = \langle y \rangle \leftrightarrow x \sim y.$$

Ideal.span_singleton_mul_right_unit theorem

{a : α} (h2 : IsUnit a) (x : α) : span ({x * a} : Set α) = span { x }

Full source

theorem span_singleton_mul_right_unit {a : α} (h2 : IsUnit a) (x : α) :
    span ({x * a} : Set α) = span {x} := by rw [mul_comm, span_singleton_mul_left_unit h2]

Equality of ideals generated by $x \cdot a$ and $x$ for invertible $a$

Informal description

For any element $a$ in a ring $\alpha$ that is a unit (i.e., invertible), and for any element $x \in \alpha$, the ideal generated by the singleton set $\{x \cdot a\}$ is equal to the ideal generated by the singleton set $\{x\}$. In other words: $$\operatorname{span}(\{x \cdot a\}) = \operatorname{span}(\{x\}).$$

Ideal.span_singleton_eq_top theorem

{x} : span ({ x } : Set α) = ⊤ ↔ IsUnit x

Full source

@[simp]
theorem span_singleton_eq_top {x} : spanspan ({x} : Set α) = ⊤ ↔ IsUnit x := by
  rw [isUnit_iff_dvd_one, ← span_singleton_le_span_singleton, span_singleton_one, eq_top_iff]

Principal Ideal Generated by Unit is the Whole Ring: $\langle x \rangle = \top \leftrightarrow x$ is a unit

Informal description

For an element $x$ in a ring $\alpha$, the ideal generated by $\{x\}$ is equal to the entire ring if and only if $x$ is a unit. In symbols: $$\langle x \rangle = \top \leftrightarrow \text{$x$ is a unit}.$$

Ideal.factors_decreasing theorem

 [IsDomain α] (b₁ b₂ : α) (h₁ : b₁ ≠ 0) (h₂ : ¬IsUnit b₂) : span ({b₁ * b₂} : Set α) < span { b₁ }

Full source

theorem factors_decreasing [IsDomain α] (b₁ b₂ : α) (h₁ : b₁ ≠ 0) (h₂ : ¬IsUnit b₂) :
    span ({b₁ * b₂} : Set α) < span {b₁} :=
  lt_of_le_not_le
    (Ideal.span_le.2 <| singleton_subset_iff.2 <| Ideal.mem_span_singleton.2 ⟨b₂, rfl⟩) fun h =>
    h₂ <| isUnit_of_dvd_one <|
        (mul_dvd_mul_iff_left h₁).1 <| by rwa [mul_one, ← Ideal.span_singleton_le_span_singleton]

Strict Ideal Containment for Non-Unit Factors in Integral Domains: $\langle b_1 b_2 \rangle < \langle b_1 \rangle$

Informal description

Let $\alpha$ be an integral domain, and let $b_1, b_2 \in \alpha$ such that $b_1 \neq 0$ and $b_2$ is not a unit. Then the ideal generated by $b_1 b_2$ is strictly contained in the ideal generated by $b_1$, i.e., $$\langle b_1 b_2 \rangle < \langle b_1 \rangle.$$

Ideal.mem_span_insert' theorem

{s : Set α} {x y} : x ∈ span (insert y s) ↔ ∃ a, x + a * y ∈ span s

Full source

theorem mem_span_insert' {s : Set α} {x y} : x ∈ span (insert y s)x ∈ span (insert y s) ↔ ∃ a, x + a * y ∈ span s :=
  Submodule.mem_span_insert'

Characterization of Elements in Ideal Generated by Inserted Set: $x \in \text{span}(\{y\} \cup s) \leftrightarrow \exists a, x + a y \in \text{span}(s)$

Informal description

For any elements $x, y$ in a ring $\alpha$ and any subset $s \subseteq \alpha$, the element $x$ belongs to the ideal generated by $\{y\} \cup s$ if and only if there exists an element $a \in \alpha$ such that $x + a \cdot y$ belongs to the ideal generated by $s$.

Ideal.span_singleton_neg theorem

(x : α) : (span {-x} : Ideal α) = span { x }

Full source

@[simp]
theorem span_singleton_neg (x : α) : (span {-x} : Ideal α) = span {x} := by
  ext
  simp only [mem_span_singleton']
  exact ⟨fun ⟨y, h⟩ => ⟨-y, h ▸ neg_mul_comm y x⟩, fun ⟨y, h⟩ => ⟨-y, h ▸ neg_mul_neg y x⟩⟩

Equality of Ideals Generated by Negated and Original Elements

Informal description

For any element $x$ in a ring $\alpha$, the ideal generated by the singleton set $\{-x\}$ is equal to the ideal generated by the singleton set $\{x\}$, i.e., $\text{span}(\{-x\}) = \text{span}(\{x\})$.

IsIdempotentElem.ker_toSpanSingleton_eq_span theorem

: LinearMap.ker (LinearMap.toSpanSingleton R R e) = Ideal.span {1 - e}

Full source

theorem ker_toSpanSingleton_eq_span :
    LinearMap.ker (LinearMap.toSpanSingleton R R e) = Ideal.span {1 - e} := SetLike.ext fun x ↦ by
  rw [Ideal.mem_span_singleton']
  refine ⟨fun h ↦ ⟨x, by rw [mul_sub, show x * e = 0 from h, mul_one, sub_zero]⟩, fun h ↦ ?_⟩
  obtain ⟨x, rfl⟩ := h
  show x * (1 - e) * e = 0
  rw [mul_assoc, sub_mul, one_mul, he, sub_self, mul_zero]

Kernel of Scalar Multiplication by Idempotent Equals Ideal Generated by Complement

Informal description

For an idempotent element $e$ in a ring $R$, the kernel of the linear map $R \to R$ sending $r$ to $r \cdot e$ is equal to the ideal generated by $1 - e$, i.e., $\ker(r \mapsto r \cdot e) = \text{span}(\{1 - e\})$.

IsIdempotentElem.ker_toSpanSingleton_one_sub_eq_span theorem

: LinearMap.ker (LinearMap.toSpanSingleton R R (1 - e)) = Ideal.span { e }

Full source

theorem ker_toSpanSingleton_one_sub_eq_span :
    LinearMap.ker (LinearMap.toSpanSingleton R R (1 - e)) = Ideal.span {e} := by
  rw [ker_toSpanSingleton_eq_span he.one_sub, sub_sub_cancel]

Kernel of Scalar Multiplication by Complement of Idempotent Equals Ideal Generated by Idempotent

Informal description

For an idempotent element $e$ in a ring $R$, the kernel of the linear map $R \to R$ sending $r$ to $r \cdot (1 - e)$ is equal to the ideal generated by $e$, i.e., $\ker(r \mapsto r \cdot (1 - e)) = \text{span}(\{e\})$.

TODO