Mathlib.RingTheory.Ideal.Lattice

Ideal.instIsTwoSidedBot instance

: IsTwoSided (⊥ : Ideal α)

Full source

instance (priority := low) : IsTwoSided (⊥ : Ideal α) :=
  ⟨fun _ h ↦ by rw [h, zero_mul]; exact zero_mem _⟩

The Bottom Ideal is Two-Sided

Informal description

The bottom ideal $\bot$ in a ring $\alpha$ is a two-sided ideal.

Ideal.instIsTwoSidedTop instance

: IsTwoSided (⊤ : Ideal α)

Full source

instance (priority := low) : IsTwoSided (⊤ : Ideal α) := ⟨fun _ _ ↦ trivial⟩

The Top Ideal is Two-Sided

Informal description

The top ideal $\top$ in a ring $\alpha$ is a two-sided ideal.

Ideal.instIsTwoSidedIInf instance

{ι} (I : ι → Ideal α) [∀ i, (I i).IsTwoSided] : (⨅ i, I i).IsTwoSided

Full source

instance (priority := low) {ι} (I : ι → Ideal α) [∀ i, (I i).IsTwoSided] : (⨅ i, I i).IsTwoSided :=
  ⟨fun _ h ↦ (Submodule.mem_iInf _).mpr (mul_mem_right _ _ <| (Submodule.mem_iInf _).mp h ·)⟩

Infimum of Two-Sided Ideals is Two-Sided

Informal description

For any indexed family of two-sided ideals $I_i$ in a ring $\alpha$, the infimum $\bigsqcap_i I_i$ is also a two-sided ideal.

Ideal.ne_top_iff_one theorem

: I ≠ ⊤ ↔ (1 : α) ∉ I

Full source

theorem ne_top_iff_one : I ≠ ⊤I ≠ ⊤ ↔ (1 : α) ∉ I :=
  not_congr I.eq_top_iff_one

Characterization of Proper Ideals via Unit Exclusion

Informal description

An ideal $I$ in a ring $\alpha$ is not equal to the top ideal $\top$ if and only if the multiplicative identity $1$ is not an element of $I$.

Ideal.mem_sup_left theorem

{S T : Ideal R} : ∀ {x : R}, x ∈ S → x ∈ S ⊔ T

Full source

theorem mem_sup_left {S T : Ideal R} : ∀ {x : R}, x ∈ S → x ∈ S ⊔ T :=
  @le_sup_left _ _ S T

Membership in Left Ideal Implies Membership in Supremum of Ideals

Informal description

For any two ideals $S$ and $T$ in a ring $R$, if an element $x \in R$ belongs to $S$, then $x$ also belongs to the supremum (join) of $S$ and $T$, denoted $S \sqcup T$.

Ideal.mem_sup_right theorem

{S T : Ideal R} : ∀ {x : R}, x ∈ T → x ∈ S ⊔ T

Full source

theorem mem_sup_right {S T : Ideal R} : ∀ {x : R}, x ∈ T → x ∈ S ⊔ T :=
  @le_sup_right _ _ S T

Membership in Right Ideal Implies Membership in Supremum of Ideals

Informal description

For any two ideals $S$ and $T$ in a ring $R$, if an element $x \in R$ belongs to $T$, then $x$ also belongs to the supremum (join) of $S$ and $T$, denoted $S \sqcup T$.

Ideal.mem_iSup_of_mem theorem

{ι : Sort*} {S : ι → Ideal R} (i : ι) : ∀ {x : R}, x ∈ S i → x ∈ iSup S

Full source

theorem mem_iSup_of_mem {ι : Sort*} {S : ι → Ideal R} (i : ι) : ∀ {x : R}, x ∈ S i → x ∈ iSup S :=
  @le_iSup _ _ _ S _

Element in Component Ideal Implies Element in Supremum of Ideals

Informal description

For any family of ideals $\{S_i\}_{i \in \iota}$ in a ring $R$, if an element $x \in R$ belongs to some ideal $S_i$, then $x$ also belongs to the supremum $\bigsqcup_{i \in \iota} S_i$ of the family.

Ideal.mem_sSup_of_mem theorem

{S : Set (Ideal R)} {s : Ideal R} (hs : s ∈ S) : ∀ {x : R}, x ∈ s → x ∈ sSup S

Full source

theorem mem_sSup_of_mem {S : Set (Ideal R)} {s : Ideal R} (hs : s ∈ S) :
    ∀ {x : R}, x ∈ s → x ∈ sSup S :=
  @le_sSup _ _ _ _ hs

Element in Ideal Implies Element in Supremum of Ideals

Informal description

For any set $S$ of ideals in a ring $R$ and any ideal $s \in S$, if an element $x \in R$ belongs to $s$, then $x$ also belongs to the supremum (join) of all ideals in $S$, denoted $\bigsqcup S$.

Ideal.mem_sInf theorem

{s : Set (Ideal R)} {x : R} : x ∈ sInf s ↔ ∀ ⦃I⦄, I ∈ s → x ∈ I

Full source

theorem mem_sInf {s : Set (Ideal R)} {x : R} : x ∈ sInf sx ∈ sInf s ↔ ∀ ⦃I⦄, I ∈ s → x ∈ I :=
  ⟨fun hx I his => hx I ⟨I, iInf_pos his⟩, fun H _I ⟨_J, hij⟩ => hij ▸ fun _S ⟨hj, hS⟩ => hS ▸ H hj⟩

Characterization of Elements in the Infimum of a Set of Ideals: $x \in \bigsqcap S \leftrightarrow \forall I \in S, x \in I$

Informal description

For any set $S$ of ideals in a ring $R$ and any element $x \in R$, $x$ belongs to the infimum (meet) $\bigsqcap S$ of the set of ideals if and only if $x$ belongs to every ideal $I \in S$.

Ideal.mem_inf theorem

{I J : Ideal R} {x : R} : x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J

Full source

@[simp 1001] -- Porting note: increased priority to appease `simpNF`
theorem mem_inf {I J : Ideal R} {x : R} : x ∈ I ⊓ Jx ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J :=
  Iff.rfl

Characterization of Elements in the Meet of Two Ideals: $x \in I \sqcap J \leftrightarrow x \in I \land x \in J$

Informal description

For any two ideals $I$ and $J$ in a ring $R$ and any element $x \in R$, $x$ belongs to the infimum (meet) $I \sqcap J$ if and only if $x$ belongs to both $I$ and $J$.

Ideal.mem_iInf theorem

{ι : Sort*} {I : ι → Ideal R} {x : R} : x ∈ iInf I ↔ ∀ i, x ∈ I i

Full source

@[simp 1001] -- Porting note: increased priority to appease `simpNF`
theorem mem_iInf {ι : Sort*} {I : ι → Ideal R} {x : R} : x ∈ iInf Ix ∈ iInf I ↔ ∀ i, x ∈ I i :=
  Submodule.mem_iInf _

Characterization of Elements in the Infimum of Ideals: $x \in \bigsqcap_i I_i \leftrightarrow \forall i, x \in I_i$

Informal description

For any family of ideals $\{I_i\}_{i \in \iota}$ in a ring $R$ and any element $x \in R$, we have $x \in \bigsqcap_i I_i$ if and only if $x \in I_i$ for every $i \in \iota$.

Ideal.mem_bot theorem

{x : R} : x ∈ (⊥ : Ideal R) ↔ x = 0

Full source

@[simp 1001] -- Porting note: increased priority to appease `simpNF`
theorem mem_bot {x : R} : x ∈ (⊥ : Ideal R)x ∈ (⊥ : Ideal R) ↔ x = 0 :=
  Submodule.mem_bot _

Characterization of Elements in the Zero Ideal: $x \in \bot \leftrightarrow x = 0$

Informal description

For any element $x$ in a ring $R$, $x$ belongs to the bottom ideal (the zero ideal) if and only if $x$ is equal to $0$.

TODO