Mathlib.RingTheory.Ideal.Defs

Ideal abbrev

(R : Type u) [Semiring R]

Full source

/-- 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. -/
abbrev Ideal (R : Type u) [Semiring R] :=
  Submodule R R

Definition of Ideal in a Semiring

Informal description

An ideal $I$ in a semiring $R$ is an additive submonoid of $R$ that is closed under left multiplication by any element of $R$. That is, for any $a \in R$ and $b \in I$, the product $a \cdot b$ belongs to $I$. If $R$ is a ring, then $I$ is additionally required to be an additive subgroup of $R$.

Ideal.IsTwoSided structure

Full source

/-- A left ideal `I : Ideal R` is two-sided if it is also a right ideal. -/
@[mk_iff] class IsTwoSided : Prop where
  mul_mem_of_left {a : α} (b : α) : a ∈ I → a * b ∈ I

Two-sided ideal

Informal description

A left ideal $I$ in a ring $R$ is called *two-sided* if it is also a right ideal, meaning that for any $a \in I$ and $r \in R$, both $a \cdot r$ and $r \cdot a$ belong to $I$.

Ideal.zero_mem theorem

: (0 : α) ∈ I

Full source

protected theorem zero_mem : (0 : α) ∈ I :=
  Submodule.zero_mem I

Zero Element in Ideal

Informal description

For any ideal $I$ in a semiring $R$, the zero element $0$ is contained in $I$.

Ideal.add_mem theorem

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

Full source

protected theorem add_mem : a ∈ I → b ∈ I → a + b ∈ I :=
  Submodule.add_mem I

Additive Closure Property of Ideals

Informal description

For any ideal $I$ in a semiring $R$, if elements $a$ and $b$ belong to $I$, then their sum $a + b$ also belongs to $I$.

Ideal.mul_mem_left theorem

: b ∈ I → a * b ∈ I

Full source

theorem mul_mem_left : b ∈ I → a * b ∈ I :=
  Submodule.smul_mem I a

Left Multiplication Closure Property of Ideals

Informal description

For any ideal $I$ in a semiring $R$ and any elements $a \in R$ and $b \in I$, the product $a \cdot b$ belongs to $I$.

Ideal.mul_mem_right theorem

{α} {a : α} (b : α) [Semiring α] (I : Ideal α) [I.IsTwoSided] (h : a ∈ I) : a * b ∈ I

Full source

theorem mul_mem_right {α} {a : α} (b : α) [Semiring α] (I : Ideal α) [I.IsTwoSided]
    (h : a ∈ I) : a * b ∈ I :=
  IsTwoSided.mul_mem_of_left b h

Right Multiplication Closure Property of Two-Sided Ideals

Informal description

Let $I$ be a two-sided ideal in a semiring $\alpha$. For any elements $a \in I$ and $b \in \alpha$, the product $a \cdot b$ belongs to $I$.

Ideal.ext theorem

{I J : Ideal α} (h : ∀ x, x ∈ I ↔ x ∈ J) : I = J

Full source

@[ext]
theorem ext {I J : Ideal α} (h : ∀ x, x ∈ Ix ∈ I ↔ x ∈ J) : I = J :=
  Submodule.ext h

Extensionality of Ideals

Informal description

Two ideals $I$ and $J$ in a semiring $\alpha$ are equal if and only if they contain the same elements, i.e., for every $x \in \alpha$, $x \in I$ if and only if $x \in J$.

Ideal.unit_mul_mem_iff_mem theorem

{x y : α} (hy : IsUnit y) : y * x ∈ I ↔ x ∈ I

Full source

@[simp]
theorem unit_mul_mem_iff_mem {x y : α} (hy : IsUnit y) : y * x ∈ Iy * x ∈ I ↔ x ∈ I := by
  refine ⟨fun h => ?_, fun h => I.mul_mem_left y h⟩
  obtain ⟨y', hy'⟩ := hy.exists_left_inv
  have := I.mul_mem_left y' h
  rwa [← mul_assoc, hy', one_mul] at this

Membership Criterion for Ideal via Unit Multiplication: $y \cdot x \in I \leftrightarrow x \in I$ for $y$ a unit

Informal description

Let $I$ be an ideal in a semiring $\alpha$ and let $y \in \alpha$ be a unit. Then for any $x \in \alpha$, the product $y \cdot x$ belongs to $I$ if and only if $x$ belongs to $I$.

Ideal.pow_mem_of_mem theorem

(ha : a ∈ I) (n : ℕ) (hn : 0 < n) : a ^ n ∈ I

Full source

theorem pow_mem_of_mem (ha : a ∈ I) (n : ℕ) (hn : 0 < n) : a ^ n ∈ I :=
  Nat.casesOn n (Not.elim (by decide))
    (fun m _hm => (pow_succ a m).symm ▸ I.mul_mem_left (a ^ m) ha) hn

Powers of Ideal Elements Remain in Ideal

Informal description

For any element $a$ in an ideal $I$ of a semiring and any positive natural number $n$, the power $a^n$ belongs to $I$.

Ideal.pow_mem_of_pow_mem theorem

{m n : ℕ} (ha : a ^ m ∈ I) (h : m ≤ n) : a ^ n ∈ I

Full source

theorem pow_mem_of_pow_mem {m n : ℕ} (ha : a ^ m ∈ I) (h : m ≤ n) : a ^ n ∈ I := by
  rw [← Nat.add_sub_of_le h, add_comm, pow_add]
  exact I.mul_mem_left _ ha

Power Membership Preservation in Ideals: $a^m \in I \Rightarrow a^n \in I$ for $m \leq n$

Informal description

Let $I$ be an ideal in a semiring $R$. For any element $a \in R$ and natural numbers $m, n$ such that $m \leq n$, if $a^m \in I$, then $a^n \in I$.

Module.eqIdeal definition

(R) {M} [Semiring R] [AddCommMonoid M] [Module R M] (m m' : M) : Ideal R

Full source

/-- For two elements `m` and `m'` in an `R`-module `M`, the set of elements `r : R` with
equal scalar product with `m` and `m'` is an ideal of `R`. If `M` is a group, this coincides
with the kernel of `LinearMap.toSpanSingleton R M (m - m')`. -/
def Module.eqIdeal (R) {M} [Semiring R] [AddCommMonoid M] [Module R M] (m m' : M) : Ideal R where
  carrier := {r : R | r • m = r • m'}
  add_mem' h h' := by simpa [add_smul] using congr($h + $h')
  zero_mem' := by simp_rw [Set.mem_setOf, zero_smul]
  smul_mem' _ _ h := by simpa [mul_smul] using congr(_ • $h)

Ideal of equal scalar action elements

Informal description

For a semiring $R$ and an $R$-module $M$, given two elements $m, m' \in M$, the set $\{r \in R \mid r \cdot m = r \cdot m'\}$ forms an ideal in $R$. This ideal consists of all elements $r \in R$ that have equal scalar action on $m$ and $m'$.

Ideal.instIsTwoSided instance

: I.IsTwoSided

Full source

instance : I.IsTwoSided := ⟨fun b ha ↦ mul_comm b _ ▸ I.smul_mem _ ha⟩

Ideals in Commutative Rings are Two-Sided

Informal description

Every ideal $I$ in a commutative ring is two-sided.

Ideal.instIsTwoSided_1 instance

{α} [CommRing α] (I : Ideal α) : I.IsTwoSided

Full source

instance {α} [CommRing α] (I : Ideal α) : I.IsTwoSided := inferInstance

Ideals in Commutative Rings are Two-Sided

Informal description

For any commutative ring $\alpha$ and any ideal $I$ of $\alpha$, $I$ is a two-sided ideal.

Ideal.mul_unit_mem_iff_mem theorem

{x y : α} (hy : IsUnit y) : x * y ∈ I ↔ x ∈ I

Full source

@[simp]
theorem mul_unit_mem_iff_mem {x y : α} (hy : IsUnit y) : x * y ∈ Ix * y ∈ I ↔ x ∈ I :=
  mul_comm y x ▸ unit_mul_mem_iff_mem I hy

Membership Criterion for Ideal via Right Multiplication by Unit: $x \cdot y \in I \leftrightarrow x \in I$ for $y$ a unit

Informal description

Let $I$ be an ideal in a semiring $\alpha$ and let $y \in \alpha$ be a unit. Then for any $x \in \alpha$, the product $x \cdot y$ belongs to $I$ if and only if $x$ belongs to $I$.

Ideal.mem_of_dvd theorem

(hab : a ∣ b) (ha : a ∈ I) : b ∈ I

Full source

lemma mem_of_dvd (hab : a ∣ b) (ha : a ∈ I) : b ∈ I := by
  obtain ⟨c, rfl⟩ := hab; exact I.mul_mem_right _ ha

Divisibility Membership Criterion for Ideals: $a \mid b \land a \in I \to b \in I$

Informal description

Let $I$ be an ideal in a semiring $R$. For any elements $a, b \in R$, if $a$ divides $b$ (i.e., $a \mid b$) and $a \in I$, then $b \in I$.

Ideal.neg_mem_iff theorem

: -a ∈ I ↔ a ∈ I

Full source

protected theorem neg_mem_iff : -a ∈ I-a ∈ I ↔ a ∈ I :=
  Submodule.neg_mem_iff I

Negation Membership Criterion for Ideals: $-a \in I \leftrightarrow a \in I$

Informal description

For any element $a$ in a ring $R$ and an ideal $I$ of $R$, the negation $-a$ belongs to $I$ if and only if $a$ belongs to $I$.

Ideal.add_mem_iff_left theorem

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

Full source

protected theorem add_mem_iff_left : b ∈ I → (a + b ∈ Ia + b ∈ I ↔ a ∈ I) :=
  Submodule.add_mem_iff_left I

Membership Criterion for Sum in Ideal: Left Additive Case

Informal description

For any ideal $I$ in a semiring $R$ and elements $a, b \in R$, if $b \in I$, then $a + b \in I$ if and only if $a \in I$.

Ideal.add_mem_iff_right theorem

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

Full source

protected theorem add_mem_iff_right : a ∈ I → (a + b ∈ Ia + b ∈ I ↔ b ∈ I) :=
  Submodule.add_mem_iff_right I

Membership Criterion for Sum in Ideal: Right Additive Case

Informal description

For any ideal $I$ in a semiring $R$ and elements $a, b \in R$, if $a \in I$, then $a + b \in I$ if and only if $b \in I$.

Ideal.sub_mem theorem

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

Full source

protected theorem sub_mem : a ∈ I → b ∈ I → a - b ∈ I :=
  Submodule.sub_mem I

Ideal Closure Under Subtraction

Informal description

For any elements $a$ and $b$ in an ideal $I$ of a semiring $R$, the difference $a - b$ also belongs to $I$.

Ideal.mul_sub_mul_mem theorem

[I.IsTwoSided] (h1 : a - b ∈ I) (h2 : c - d ∈ I) : a * c - b * d ∈ I

Full source

theorem mul_sub_mul_mem [I.IsTwoSided]
    (h1 : a - b ∈ I) (h2 : c - d ∈ I) : a * c - b * d ∈ I := by
  rw [show a * c - b * d = (a - b) * c + b * (c - d) by rw [sub_mul, mul_sub]; abel]
  exact I.add_mem (I.mul_mem_right _ h1) (I.mul_mem_left _ h2)

Two-sided ideal closure under product differences: $a - b \in I$ and $c - d \in I$ implies $ac - bd \in I$

Informal description

Let $I$ be a two-sided ideal in a semiring $R$. For any elements $a, b, c, d \in R$ such that $a - b \in I$ and $c - d \in I$, the difference $a \cdot c - b \cdot d$ belongs to $I$.

Mathlib.RingTheory.Ideal.Defs

Implementation notes

TODO