Mathlib.RingTheory.TwoSidedIdeal.Lattice

TwoSidedIdeal.instSemilatticeSup instance

: SemilatticeSup (TwoSidedIdeal R)

Full source

instance : SemilatticeSup (TwoSidedIdeal R) where
  sup I J := { ringCon := I.ringCon ⊔ J.ringCon }
  le_sup_left I J :=  by rw [ringCon_le_iff]; exact le_sup_left
  le_sup_right I J := by rw [ringCon_le_iff]; exact le_sup_right
  sup_le I J K h1 h2 := by rw [ringCon_le_iff] at h1 h2 ⊢; exact sup_le h1 h2

Join-Semilattice Structure on Two-Sided Ideals

Informal description

The collection of two-sided ideals of a ring $R$ forms a join-semilattice, where the partial order is given by inclusion and the join operation is the sum of ideals.

TwoSidedIdeal.sup_ringCon theorem

(I J : TwoSidedIdeal R) : (I ⊔ J).ringCon = I.ringCon ⊔ J.ringCon

Full source

lemma sup_ringCon (I J : TwoSidedIdeal R) : (I ⊔ J).ringCon = I.ringCon ⊔ J.ringCon := rfl

Supremum of Two-Sided Ideals Preserves Ring Congruence Relation

Informal description

For any two two-sided ideals $I$ and $J$ of a ring $R$, the ring congruence relation associated with the supremum $I \sqcup J$ is equal to the supremum of the ring congruence relations associated with $I$ and $J$ individually. That is, $(I \sqcup J).\text{ringCon} = I.\text{ringCon} \sqcup J.\text{ringCon}$.

TwoSidedIdeal.mem_sup_left theorem

{I J : TwoSidedIdeal R} {x : R} (h : x ∈ I) : x ∈ I ⊔ J

Full source

lemma mem_sup_left {I J : TwoSidedIdeal R} {x : R} (h : x ∈ I) :
    x ∈ I ⊔ J :=
  (show I ≤ I ⊔ J from le_sup_left) h

Element in Left Ideal Belongs to Supremum of Two Ideals

Informal description

For any two-sided ideals $I$ and $J$ in a ring $R$, if an element $x \in R$ belongs to $I$, then $x$ also belongs to the supremum $I \sqcup J$ of the two ideals.

TwoSidedIdeal.mem_sup_right theorem

{I J : TwoSidedIdeal R} {x : R} (h : x ∈ J) : x ∈ I ⊔ J

Full source

lemma mem_sup_right {I J : TwoSidedIdeal R} {x : R} (h : x ∈ J) :
    x ∈ I ⊔ J :=
  (show J ≤ I ⊔ J from le_sup_right) h

Membership in Supremum of Two-Sided Ideals from Right Ideal

Informal description

For any two-sided ideals $I$ and $J$ of a ring $R$, and any element $x \in R$, if $x \in J$, then $x$ is in the supremum $I \sqcup J$ of the two ideals.

TwoSidedIdeal.mem_sup theorem

{I J : TwoSidedIdeal R} {x : R} : x ∈ I ⊔ J ↔ ∃ y ∈ I, ∃ z ∈ J, y + z = x

Full source

lemma mem_sup {I J : TwoSidedIdeal R} {x : R} :
    x ∈ I ⊔ Jx ∈ I ⊔ J ↔ ∃ y ∈ I, ∃ z ∈ J, y + z = x := by
  constructor
  · let s : TwoSidedIdeal R := .mk'
      {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}
      ⟨0, ⟨zero_mem _, ⟨0, ⟨zero_mem _, zero_add _⟩⟩⟩⟩
      (by rintro _ _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩ ⟨a, ⟨ha, ⟨b, ⟨hb, rfl⟩⟩⟩⟩;
          exact ⟨x + a, ⟨add_mem _ hx ha, ⟨y + b, ⟨add_mem _ hy hb, by abel⟩⟩⟩⟩)
      (by rintro _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩
          exact ⟨-x, ⟨neg_mem _ hx, ⟨-y, ⟨neg_mem _ hy, by abel⟩⟩⟩⟩)
      (by rintro r _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩
          exact ⟨_, ⟨mul_mem_left _ _ _ hx, ⟨_, ⟨mul_mem_left _ _ _ hy, mul_add _ _ _ |>.symm⟩⟩⟩⟩)
      (by rintro r _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩
          exact ⟨_, ⟨mul_mem_right _ _ _ hx, ⟨_, ⟨mul_mem_right _ _ _ hy, add_mul _ _ _ |>.symm⟩⟩⟩⟩)
    suffices (I.ringCon ⊔ J.ringCon) ≤ s.ringCon by
      intro h; convert this h; rw [rel_iff, sub_zero, mem_mk']; rfl
    refine sup_le (fun x y h => ?_) (fun x y h => ?_) <;> rw [rel_iff] at h ⊢ <;> rw [mem_mk']
    exacts [⟨_, ⟨h, ⟨0, ⟨zero_mem _, add_zero _⟩⟩⟩⟩, ⟨0, ⟨zero_mem _, ⟨_, ⟨h, zero_add _⟩⟩⟩⟩]
  · rintro ⟨y, ⟨hy, ⟨z, ⟨hz, rfl⟩⟩⟩⟩; exact add_mem _ (mem_sup_left hy) (mem_sup_right hz)

Characterization of Membership in Supremum of Two-Sided Ideals: $x \in I \sqcup J \leftrightarrow \exists y \in I, \exists z \in J, y + z = x$

Informal description

For any two-sided ideals $I$ and $J$ in a ring $R$, an element $x \in R$ belongs to the supremum $I \sqcup J$ if and only if there exist elements $y \in I$ and $z \in J$ such that $y + z = x$.

TwoSidedIdeal.instSemilatticeInf instance

: SemilatticeInf (TwoSidedIdeal R)

Full source

instance : SemilatticeInf (TwoSidedIdeal R) where
  inf I J := { ringCon := I.ringCon ⊓ J.ringCon }
  inf_le_left I J := by rw [ringCon_le_iff]; exact inf_le_left
  inf_le_right I J := by rw [ringCon_le_iff]; exact inf_le_right
  le_inf I J K h1 h2 := by rw [ringCon_le_iff] at h1 h2 ⊢; exact le_inf h1 h2

Meet-Semilattice Structure on Two-Sided Ideals

Informal description

The collection of two-sided ideals of a ring $R$ forms a meet-semilattice, where the partial order is given by inclusion and the meet operation is the intersection of ideals.

TwoSidedIdeal.inf_ringCon theorem

(I J : TwoSidedIdeal R) : (I ⊓ J).ringCon = I.ringCon ⊓ J.ringCon

Full source

lemma inf_ringCon (I J : TwoSidedIdeal R) : (I ⊓ J).ringCon = I.ringCon ⊓ J.ringCon := rfl

Intersection of Two-Sided Ideals and Their Ring Congruence Relations

Informal description

For any two two-sided ideals $I$ and $J$ of a ring $R$, the ring congruence relation associated with their intersection $I \sqcap J$ is equal to the infimum of the ring congruence relations associated with $I$ and $J$ individually. That is, $(I \sqcap J).\text{ringCon} = I.\text{ringCon} \sqcap J.\text{ringCon}$.

TwoSidedIdeal.mem_inf theorem

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

Full source

lemma mem_inf {I J : TwoSidedIdeal R} {x : R} :
    x ∈ I ⊓ Jx ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J :=
  Iff.rfl

Membership in Intersection of Two-Sided Ideals

Informal description

For any two-sided ideals $I$ and $J$ in a ring $R$ and any element $x \in R$, we have $x \in I \sqcap J$ if and only if $x \in I$ and $x \in J$.

TwoSidedIdeal.instSupSet instance

: SupSet (TwoSidedIdeal R)

Full source

instance : SupSet (TwoSidedIdeal R) where
  sSup s := { ringCon := sSup <| TwoSidedIdeal.ringConTwoSidedIdeal.ringCon '' s }

Complete Lattice Structure on Two-Sided Ideals

Informal description

The collection of two-sided ideals of a ring $R$ forms a complete lattice with respect to inclusion, where the supremum of a set of ideals is the smallest ideal containing all of them.

TwoSidedIdeal.sSup_ringCon theorem

(S : Set (TwoSidedIdeal R)) : (sSup S).ringCon = sSup (TwoSidedIdeal.ringCon '' S)

Full source

lemma sSup_ringCon (S : Set (TwoSidedIdeal R)) :
    (sSup S).ringCon = sSup (TwoSidedIdeal.ringConTwoSidedIdeal.ringCon '' S) := rfl

Supremum of Two-Sided Ideals Preserves Ring Congruence Relation

Informal description

For any set $S$ of two-sided ideals in a ring $R$, the ring congruence relation associated with the supremum of $S$ is equal to the supremum of the set of ring congruence relations associated with each ideal in $S$. That is, $$(\bigvee S).\text{ringCon} = \bigvee \{I.\text{ringCon} \mid I \in S\}.$$

TwoSidedIdeal.iSup_ringCon theorem

{ι : Type*} (I : ι → TwoSidedIdeal R) : (⨆ i, I i).ringCon = ⨆ i, (I i).ringCon

Full source

lemma iSup_ringCon {ι : Type*} (I : ι → TwoSidedIdeal R) :
    (⨆ i, I i).ringCon = ⨆ i, (I i).ringCon := by
  simp only [iSup, sSup_ringCon]; congr; ext; simp

Supremum of Two-Sided Ideals Preserves Ring Congruence Relation

Informal description

For any family of two-sided ideals $\{I_i\}_{i \in \iota}$ in a ring $R$, the ring congruence relation associated with the supremum of the ideals is equal to the supremum of the ring congruence relations associated with each ideal $I_i$. That is, $$ \left(\bigsqcup_{i \in \iota} I_i\right).\text{ringCon} = \bigsqcup_{i \in \iota} (I_i.\text{ringCon}). $$

TwoSidedIdeal.instCompleteSemilatticeSup instance

: CompleteSemilatticeSup (TwoSidedIdeal R)

Full source

instance : CompleteSemilatticeSup (TwoSidedIdeal R) where
  sSup_le s I h := by simp_rw [ringCon_le_iff] at h ⊢; exact sSup_le <| by aesop
  le_sSup s I hI := by rw [ringCon_le_iff]; exact le_sSup <| by aesop

Complete Semilattice Structure on Two-Sided Ideals

Informal description

The collection of two-sided ideals of a ring $R$ forms a complete semilattice with respect to inclusion, where every subset of ideals has a supremum.

TwoSidedIdeal.instInfSet instance

: InfSet (TwoSidedIdeal R)

Full source

instance : InfSet (TwoSidedIdeal R) where
  sInf s := { ringCon := sInf <| TwoSidedIdeal.ringConTwoSidedIdeal.ringCon '' s }

Infimum Structure on Two-Sided Ideals

Informal description

For any ring $R$, the collection of two-sided ideals of $R$ has an infimum structure. Given a set $S$ of two-sided ideals, their infimum $\bigwedge S$ is the greatest two-sided ideal contained in every ideal in $S$.

TwoSidedIdeal.sInf_ringCon theorem

(S : Set (TwoSidedIdeal R)) : (sInf S).ringCon = sInf (TwoSidedIdeal.ringCon '' S)

Full source

lemma sInf_ringCon (S : Set (TwoSidedIdeal R)) :
    (sInf S).ringCon = sInf (TwoSidedIdeal.ringConTwoSidedIdeal.ringCon '' S) := rfl

Infimum of Two-Sided Ideals Preserves Ring Congruence Relation

Informal description

For any set $S$ of two-sided ideals in a ring $R$, the ring congruence relation associated with the infimum of $S$ is equal to the infimum of the set of ring congruence relations associated with each ideal in $S$. That is, \[ (\bigwedge S).\text{ringCon} = \bigwedge \{I.\text{ringCon} \mid I \in S\}. \]

TwoSidedIdeal.iInf_ringCon theorem

{ι : Type*} (I : ι → TwoSidedIdeal R) : (⨅ i, I i).ringCon = ⨅ i, (I i).ringCon

Full source

lemma iInf_ringCon {ι : Type*} (I : ι → TwoSidedIdeal R) :
    (⨅ i, I i).ringCon = ⨅ i, (I i).ringCon := by
  simp only [iInf, sInf_ringCon]; congr!; ext; simp

Infimum of Two-Sided Ideals Preserves Ring Congruence Relation

Informal description

For any family of two-sided ideals $\{I_i\}_{i \in \iota}$ in a ring $R$, the ring congruence relation associated with the infimum of the ideals is equal to the infimum of the ring congruence relations associated with each ideal. That is, $$ \left(\bigwedge_{i} I_i\right).\text{ringCon} = \bigwedge_{i} (I_i.\text{ringCon}). $$

TwoSidedIdeal.instCompleteSemilatticeInf instance

: CompleteSemilatticeInf (TwoSidedIdeal R)

Full source

instance : CompleteSemilatticeInf (TwoSidedIdeal R) where
  le_sInf s I h := by simp_rw [ringCon_le_iff] at h ⊢; exact le_sInf <| by aesop
  sInf_le s I hI := by rw [ringCon_le_iff]; exact sInf_le <| by aesop

Complete Meet-Semilattice Structure on Two-Sided Ideals

Informal description

The collection of two-sided ideals of a ring $R$ forms a complete meet-semilattice, where every subset of ideals has an infimum (greatest lower bound) with respect to inclusion.

TwoSidedIdeal.mem_iInf theorem

{ι : Type*} {I : ι → TwoSidedIdeal R} {x : R} : x ∈ iInf I ↔ ∀ i, x ∈ I i

Full source

lemma mem_iInf {ι : Type*} {I : ι → TwoSidedIdeal R} {x : R} :
    x ∈ iInf Ix ∈ iInf I ↔ ∀ i, x ∈ I i :=
  show (∀ _, _) ↔ _ by simp [mem_iff]

Characterization of Membership in Infimum of Two-Sided Ideals

Informal description

For any indexed family of two-sided ideals $I_i$ in a ring $R$ and any element $x \in R$, $x$ belongs to the infimum $\bigsqcap_i I_i$ if and only if $x$ belongs to $I_i$ for every index $i$.

TwoSidedIdeal.mem_sInf theorem

{S : Set (TwoSidedIdeal R)} {x : R} : x ∈ sInf S ↔ ∀ I ∈ S, x ∈ I

Full source

lemma mem_sInf {S : Set (TwoSidedIdeal R)} {x : R} :
    x ∈ sInf Sx ∈ sInf S ↔ ∀ I ∈ S, x ∈ I :=
  show (∀ _, _) ↔ _ by simp [mem_iff]

Characterization of Infimum Membership for Two-Sided Ideals

Informal description

For any set $S$ of two-sided ideals in a ring $R$ and any element $x \in R$, the element $x$ belongs to the infimum (greatest lower bound) of $S$ if and only if $x$ belongs to every ideal $I \in S$. In symbols: $$ x \in \bigwedge S \leftrightarrow (\forall I \in S, x \in I) $$

TwoSidedIdeal.instTop instance

: Top (TwoSidedIdeal R)

Full source

instance : Top (TwoSidedIdeal R) where
  top := { ringCon := ⊤ }

The Top Element in the Lattice of Two-Sided Ideals

Informal description

The collection of two-sided ideals in a ring $R$ has a top element, which is the ideal consisting of all elements of $R$.

TwoSidedIdeal.top_ringCon theorem

: (⊤ : TwoSidedIdeal R).ringCon = ⊤

Full source

lemma top_ringCon : (⊤ : TwoSidedIdeal R).ringCon = ⊤ := rfl

Top Ideal's Congruence Relation is the Top Congruence Relation

Informal description

The ring congruence relation associated with the top element (the entire ring) in the lattice of two-sided ideals of a ring $R$ is equal to the top congruence relation on $R$.

TwoSidedIdeal.mem_top theorem

{x : R} : x ∈ (⊤ : TwoSidedIdeal R)

Full source

@[simp]
lemma mem_top {x : R} : x ∈ (⊤: TwoSidedIdeal R) := trivial

Every Ring Element Belongs to the Top Ideal

Informal description

For any element $x$ in a ring $R$, $x$ belongs to the top two-sided ideal of $R$ (i.e., the ideal consisting of all elements of $R$).

TwoSidedIdeal.instBot instance

: Bot (TwoSidedIdeal R)

Full source

instance : Bot (TwoSidedIdeal R) where
  bot := { ringCon := ⊥ }

Existence of Zero Ideal as Bottom Element in Two-Sided Ideals

Informal description

The collection of two-sided ideals of a ring $R$ has a bottom element $\bot$, which is the zero ideal $\{0\}$.

TwoSidedIdeal.bot_ringCon theorem

: (⊥ : TwoSidedIdeal R).ringCon = ⊥

Full source

lemma bot_ringCon : (⊥ : TwoSidedIdeal R).ringCon = ⊥ := rfl

Ring Congruence of Zero Ideal is Bottom Element

Informal description

The ring congruence relation associated with the zero ideal $\bot$ in the lattice of two-sided ideals of a ring $R$ is equal to the bottom element $\bot$ of the complete lattice of ring congruence relations on $R$.

TwoSidedIdeal.mem_bot theorem

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

Full source

@[simp]
lemma mem_bot {x : R} : x ∈ (⊥ : TwoSidedIdeal R)x ∈ (⊥ : TwoSidedIdeal R) ↔ x = 0 :=
  Iff.rfl

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

Informal description

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

TwoSidedIdeal.instCompleteLattice instance

: CompleteLattice (TwoSidedIdeal R)

Full source

instance : CompleteLattice (TwoSidedIdeal R) where
  __ := (inferInstance : SemilatticeSup (TwoSidedIdeal R))
  __ := (inferInstance : SemilatticeInf (TwoSidedIdeal R))
  __ := (inferInstance : CompleteSemilatticeSup (TwoSidedIdeal R))
  __ := (inferInstance : CompleteSemilatticeInf (TwoSidedIdeal R))
  le_top _ := by rw [ringCon_le_iff]; exact le_top
  bot_le _ := by rw [ringCon_le_iff]; exact bot_le

Complete Lattice Structure on Two-Sided Ideals

Informal description

The collection of two-sided ideals of a ring $R$ forms a complete lattice, where the partial order is given by inclusion, the meet operation is the intersection of ideals, the join operation is the sum of ideals, the bottom element is the zero ideal $\{0\}$, and the top element is the entire ring $R$.

TwoSidedIdeal.coe_bot theorem

: ((⊥ : TwoSidedIdeal R) : Set R) = {0}

Full source

@[simp]
lemma coe_bot : ((⊥ : TwoSidedIdeal R) : Set R) = {0} := rfl

Characterization of the Zero Ideal as $\{0\}$ in Two-Sided Ideals

Informal description

The zero ideal $\bot$ in the lattice of two-sided ideals of a ring $R$ corresponds to the singleton set $\{0\}$ when viewed as a subset of $R$.

TwoSidedIdeal.coe_top theorem

: ((⊤ : TwoSidedIdeal R) : Set R) = Set.univ

Full source

@[simp]
lemma coe_top : ((⊤ : TwoSidedIdeal R) : Set R) = Set.univ := rfl

Top Two-Sided Ideal Equals Universal Set

Informal description

The top element in the lattice of two-sided ideals of a ring $R$, when viewed as a subset of $R$, is equal to the universal set of $R$. That is, $\top = R$ as sets.

TwoSidedIdeal.one_mem_iff theorem

{R : Type*} [NonAssocRing R] (I : TwoSidedIdeal R) : (1 : R) ∈ I ↔ I = ⊤

Full source

lemma one_mem_iff {R : Type*} [NonAssocRing R] (I : TwoSidedIdeal R) :
    (1 : R) ∈ I(1 : R) ∈ I ↔ I = ⊤ :=
  ⟨fun h => eq_top_iff.2 fun x _ => by simpa using I.mul_mem_left x _ h, fun h ↦ h.symm ▸ trivial⟩

Characterization of the Whole Ring via Identity Element in Two-Sided Ideals

Informal description

For any two-sided ideal $I$ in a non-associative ring $R$, the multiplicative identity $1$ is an element of $I$ if and only if $I$ is equal to the entire ring $R$ (i.e., the top element in the lattice of two-sided ideals).