Mathlib.RingTheory.Congruence.Basic

RingCon.instSMulQuotient instance

: SMul α c.Quotient

Full source

instance : SMul α c.Quotient := inferInstanceAs (SMul α c.toCon.Quotient)

Scalar Multiplication on Quotient Ring by Congruence Relation

Informal description

For a ring $R$ with a congruence relation $c$ and a scalar multiplication operation by elements of type $\alpha$, the quotient ring $R/c$ inherits a scalar multiplication operation from $R$.

RingCon.coe_smul theorem

(a : α) (x : R) : (↑(a • x) : c.Quotient) = a • (x : c.Quotient)

Full source

@[simp, norm_cast]
theorem coe_smul (a : α) (x : R) : (↑(a • x) : c.Quotient) = a • (x : c.Quotient) :=
  rfl

Scalar Multiplication Commutes with Quotient Projection

Informal description

Let $R$ be a ring with a congruence relation $c$, and let $\alpha$ be a type with a scalar multiplication operation on $R$. For any scalar $a \in \alpha$ and any element $x \in R$, the equivalence class of $a \cdot x$ in the quotient ring $R/c$ is equal to the scalar multiplication of $a$ with the equivalence class of $x$ in $R/c$. In symbols: \[ [a \cdot x] = a \cdot [x] \] where $[ \cdot ]$ denotes the equivalence class in $R/c$.

RingCon.instSMulCommClassQuotient instance

[SMulCommClass α β R] : SMulCommClass α β c.Quotient

Full source

instance [SMulCommClass α β R] : SMulCommClass α β c.Quotient :=
  inferInstanceAs (SMulCommClass α β c.toCon.Quotient)

Commutativity of Scalar Multiplications on Quotient Ring by Congruence Relation

Informal description

For a ring $R$ with a congruence relation $c$ and scalar multiplication operations by elements of types $\alpha$ and $\beta$ that commute on $R$, the scalar multiplications by $\alpha$ and $\beta$ also commute on the quotient ring $R/c$.

RingCon.instIsScalarTowerQuotient instance

[SMul α β] [IsScalarTower α β R] : IsScalarTower α β c.Quotient

Full source

instance [SMul α β] [IsScalarTower α β R] : IsScalarTower α β c.Quotient :=
  inferInstanceAs (IsScalarTower α β c.toCon.Quotient)

Scalar Tower Property on Quotient Ring by Congruence Relation

Informal description

For a ring $R$ with a scalar multiplication operation by elements of types $\alpha$ and $\beta$ that satisfy the scalar tower property (i.e., $(a \cdot b) \cdot r = a \cdot (b \cdot r)$ for all $a \in \alpha$, $b \in \beta$, and $r \in R$), and a congruence relation $c$ on $R$, the quotient ring $R/c$ inherits the scalar tower property from $R$.

RingCon.instIsCentralScalarQuotient instance

[SMul αᵐᵒᵖ R] [IsCentralScalar α R] : IsCentralScalar α c.Quotient

Full source

instance [SMul αᵐᵒᵖ R] [IsCentralScalar α R] : IsCentralScalar α c.Quotient :=
  inferInstanceAs (IsCentralScalar α c.toCon.Quotient)

Central Scalar Multiplication on Quotient Ring by Congruence Relation

Informal description

For a ring $R$ with a scalar multiplication operation by elements of type $\alpha$ and its opposite $\alpha^\text{op}$, if the scalar multiplication by $\alpha$ is central (i.e., $a \cdot r = r \cdot a$ for all $a \in \alpha$ and $r \in R$), then the quotient ring $R/c$ by a congruence relation $c$ inherits the property that scalar multiplication by $\alpha$ is central.

RingCon.isScalarTower_right instance

[Add R] [MulOneClass R] [SMul α R] [IsScalarTower α R R] (c : RingCon R) : IsScalarTower α c.Quotient c.Quotient

Full source

instance isScalarTower_right [Add R] [MulOneClass R] [SMul α R] [IsScalarTower α R R]
    (c : RingCon R) : IsScalarTower α c.Quotient c.Quotient where
  smul_assoc _ := Quotient.ind₂' fun _ _ => congr_arg Quotient.mk'' <| smul_mul_assoc _ _ _

Scalar Multiplication Compatibility in Quotient Rings by Congruence Relations

Informal description

For a ring $R$ with a scalar multiplication operation by elements of type $\alpha$ that is compatible with the ring multiplication (i.e., $a \cdot (x \cdot y) = (a \cdot x) \cdot y$ for all $a \in \alpha$ and $x, y \in R$), and a congruence relation $c$ on $R$, the quotient ring $R/c$ inherits a compatible scalar multiplication operation where $a \cdot ([x] \cdot [y]) = (a \cdot [x]) \cdot [y]$ for all $a \in \alpha$ and equivalence classes $[x], [y] \in R/c$.

RingCon.smulCommClass instance

 [Add R] [MulOneClass R] [SMul α R] [IsScalarTower α R R] [SMulCommClass α R R] (c : RingCon R) :
  SMulCommClass α c.Quotient c.Quotient

Full source

instance smulCommClass [Add R] [MulOneClass R] [SMul α R] [IsScalarTower α R R]
    [SMulCommClass α R R] (c : RingCon R) : SMulCommClass α c.Quotient c.Quotient where
  smul_comm _ := Quotient.ind₂' fun _ _ => congr_arg Quotient.mk'' <| (mul_smul_comm _ _ _).symm

Commutativity of Scalar Multiplication on Quotient Ring by Congruence Relation

Informal description

For a type $R$ with addition and multiplication, a scalar multiplication operation by elements of type $\alpha$, and a ring congruence relation $c$ on $R$, if the scalar multiplication on $R$ is commutative (i.e., $a \cdot (x \cdot y) = x \cdot (a \cdot y)$ for all $a \in \alpha$ and $x, y \in R$), then the induced scalar multiplication on the quotient ring $R/c$ is also commutative.

RingCon.smulCommClass' instance

 [Add R] [MulOneClass R] [SMul α R] [IsScalarTower α R R] [SMulCommClass R α R] (c : RingCon R) :
  SMulCommClass c.Quotient α c.Quotient

Full source

instance smulCommClass' [Add R] [MulOneClass R] [SMul α R] [IsScalarTower α R R]
    [SMulCommClass R α R] (c : RingCon R) : SMulCommClass c.Quotient α c.Quotient :=
  haveI := SMulCommClass.symm R α R
  SMulCommClass.symm _ _ _

Commutativity of Scalar Multiplication in Quotient Rings by Congruence Relations (Reversed)

Informal description

For a type $R$ with addition and multiplication, a scalar multiplication operation by elements of type $\alpha$, and a ring congruence relation $c$ on $R$, if the scalar multiplication on $R$ satisfies the commutativity condition $x \cdot (a \cdot y) = a \cdot (x \cdot y)$ for all $a \in \alpha$ and $x, y \in R$, then the induced scalar multiplication on the quotient ring $R/c$ also satisfies this commutativity condition.

RingCon.instDistribMulActionQuotientOfIsScalarTower instance

 [Monoid α] [NonAssocSemiring R] [DistribMulAction α R] [IsScalarTower α R R] (c : RingCon R) :
  DistribMulAction α c.Quotient

Full source

instance [Monoid α] [NonAssocSemiring R] [DistribMulAction α R] [IsScalarTower α R R]
    (c : RingCon R) : DistribMulAction α c.Quotient :=
  { c.toCon.mulAction with
    smul_zero := fun _ => congr_arg toQuotient <| smul_zero _
    smul_add := fun _ => Quotient.ind₂' fun _ _ => congr_arg toQuotient <| smul_add _ _ _ }

Distributive Multiplicative Action on Quotient Ring by Congruence Relation

Informal description

For any monoid $\alpha$ acting distributively on a non-associative semiring $R$ with the action compatible with multiplication (i.e., $a \cdot (x \cdot y) = (a \cdot x) \cdot y$ for all $a \in \alpha$ and $x, y \in R$), and any ring congruence relation $c$ on $R$, the quotient ring $R/c$ inherits a distributive multiplicative action by $\alpha$.

RingCon.instMulSemiringActionQuotientOfIsScalarTower instance

 [Monoid α] [Semiring R] [MulSemiringAction α R] [IsScalarTower α R R] (c : RingCon R) : MulSemiringAction α c.Quotient

Full source

instance [Monoid α] [Semiring R] [MulSemiringAction α R] [IsScalarTower α R R] (c : RingCon R) :
    MulSemiringAction α c.Quotient :=
  { smul_one := fun _ => congr_arg toQuotient <| smul_one _
    smul_mul := fun _ => Quotient.ind₂' fun _ _ => congr_arg toQuotient <|
      MulSemiringAction.smul_mul _ _ _ }

Multiplicative Semiring Action on Quotient Ring by Congruence Relation

Informal description

For any monoid $\alpha$ acting multiplicatively on a semiring $R$ with the action compatible with multiplication (i.e., $a \cdot (x \cdot y) = (a \cdot x) \cdot y$ for all $a \in \alpha$ and $x, y \in R$), and any ring congruence relation $c$ on $R$, the quotient ring $R/c$ inherits a multiplicative semiring action by $\alpha$.

RingCon.instLE instance

: LE (RingCon R)

Full source

/-- For congruence relations `c, d` on a type `M` with multiplication and addition, `c ≤ d` iff
`∀ x y ∈ M`, `x` is related to `y` by `d` if `x` is related to `y` by `c`. -/
instance : LE (RingCon R) where
  le c d := ∀ ⦃x y⦄, c x y → d x y

Partial Order on Ring Congruence Relations

Informal description

For any type $R$ with addition and multiplication, the collection of ring congruence relations on $R$ is equipped with a partial order $\leq$, where for two congruence relations $c$ and $d$, $c \leq d$ if and only if for all $x, y \in R$, whenever $x$ is related to $y$ under $c$, then $x$ is also related to $y$ under $d$.

RingCon.le_def theorem

{c d : RingCon R} : c ≤ d ↔ ∀ {x y}, c x y → d x y

Full source

/-- Definition of `≤` for congruence relations. -/
theorem le_def {c d : RingCon R} : c ≤ d ↔ ∀ {x y}, c x y → d x y :=
  Iff.rfl

Definition of Partial Order on Ring Congruence Relations

Informal description

For any two ring congruence relations $c$ and $d$ on a ring $R$, the relation $c \leq d$ holds if and only if for all $x, y \in R$, whenever $x$ is congruent to $y$ under $c$, then $x$ is also congruent to $y$ under $d$.

RingCon.instInfSet instance

: InfSet (RingCon R)

Full source

/-- The infimum of a set of congruence relations on a given type with multiplication and
addition. -/
instance : InfSet (RingCon R) where
  sInf S :=
    { r := fun x y => ∀ c : RingCon R, c ∈ S → c x y
      iseqv :=
        ⟨fun x c _hc => c.refl x, fun h c hc => c.symm <| h c hc, fun h1 h2 c hc =>
          c.trans (h1 c hc) <| h2 c hc⟩
      add' := fun h1 h2 c hc => c.add (h1 c hc) <| h2 c hc
      mul' := fun h1 h2 c hc => c.mul (h1 c hc) <| h2 c hc }

Infimum of Ring Congruence Relations

Informal description

For any type $R$ with addition and multiplication, the collection of ring congruence relations on $R$ has an infimum structure. Given a set $S$ of ring congruence relations, their infimum $\bigwedge S$ is the greatest ring congruence relation contained in every relation in $S$.

RingCon.sInf_toSetoid theorem

(S : Set (RingCon R)) : (sInf S).toSetoid = sInf ((·.toSetoid) '' S)

Full source

/-- The infimum of a set of congruence relations is the same as the infimum of the set's image
    under the map to the underlying equivalence relation. -/
theorem sInf_toSetoid (S : Set (RingCon R)) : (sInf S).toSetoid = sInf ((·.toSetoid) '' S) :=
  Setoid.ext fun x y =>
    ⟨fun h r ⟨c, hS, hr⟩ => by rw [← hr]; exact h c hS, fun h c hS => h c.toSetoid ⟨c, hS, rfl⟩⟩

Infimum of Ring Congruence Relations Preserves Underlying Equivalence Relation

Informal description

For any set $S$ of ring congruence relations on a ring $R$, the underlying equivalence relation of the infimum of $S$ is equal to the infimum of the set of underlying equivalence relations obtained by applying the `toSetoid` function to each element of $S$. In other words, \[ \left(\bigwedge S\right).\text{toSetoid} = \bigwedge \{c.\text{toSetoid} \mid c \in S\}. \]

RingCon.coe_sInf theorem

(S : Set (RingCon R)) : ⇑(sInf S) = sInf ((⇑) '' S)

Full source

/-- The infimum of a set of congruence relations is the same as the infimum of the set's image
    under the map to the underlying binary relation. -/
@[simp, norm_cast]
theorem coe_sInf (S : Set (RingCon R)) : ⇑(sInf S) = sInf ((⇑) '' S) := by
  ext; simp only [sInf_image, iInf_apply, iInf_Prop_eq]; rfl

Infimum of Ring Congruence Relations Equals Infimum of Their Underlying Relations

Informal description

For any set $S$ of ring congruence relations on a ring $R$, the underlying binary relation of the infimum of $S$ is equal to the infimum of the set of underlying binary relations obtained by applying the coercion function to each element of $S$. In other words, \[ \bigwedge S = \bigwedge \{c \mid c \in S\}. \]

RingCon.coe_iInf theorem

{ι : Sort*} (f : ι → RingCon R) : ⇑(iInf f) = ⨅ i, ⇑(f i)

Full source

@[simp, norm_cast]
theorem coe_iInf {ι : Sort*} (f : ι → RingCon R) : ⇑(iInf f) = ⨅ i, ⇑(f i) := by
  rw [iInf, coe_sInf, ← Set.range_comp, sInf_range, Function.comp_def]

Infimum of Ring Congruence Relations Preserves Underlying Relations

Informal description

For any indexed family of ring congruence relations $(f_i)_{i \in \iota}$ on a ring $R$, the underlying binary relation of the infimum of the family is equal to the infimum of the underlying binary relations of each $f_i$. That is, \[ \bigwedge_{i \in \iota} f_i = \bigwedge_{i \in \iota} (f_i). \]

RingCon.instPartialOrder instance

: PartialOrder (RingCon R)

Full source

instance : PartialOrder (RingCon R) where
  le_refl _c _ _ := id
  le_trans _c1 _c2 _c3 h1 h2 _x _y h := h2 <| h1 h
  le_antisymm _c _d hc hd := ext fun _x _y => ⟨fun h => hc h, fun h => hd h⟩

Partial Order on Ring Congruence Relations

Informal description

For any type $R$ with addition and multiplication, the collection of ring congruence relations on $R$ forms a partial order under inclusion.

RingCon.instCompleteLattice instance

: CompleteLattice (RingCon R)

Full source

/-- The complete lattice of congruence relations on a given type with multiplication and
addition. -/
instance : CompleteLattice (RingCon R) where
  __ := completeLatticeOfInf (RingCon R) fun s =>
    ⟨fun r hr x y h => (h : ∀ r ∈ s, (r : RingCon R) x y) r hr,
      fun _r hr _x _y h _r' hr' => hr hr' h⟩
  inf c d :=
    { toSetoid := c.toSetoid ⊓ d.toSetoid
      mul' := fun h1 h2 => ⟨c.mul h1.1 h2.1, d.mul h1.2 h2.2⟩
      add' := fun h1 h2 => ⟨c.add h1.1 h2.1, d.add h1.2 h2.2⟩ }
  inf_le_left _ _ := fun _ _ h => h.1
  inf_le_right _ _ := fun _ _ h => h.2
  le_inf _ _ _ hb hc := fun _ _ h => ⟨hb h, hc h⟩
  top :=
    { (⊤ : Setoid R) with
      mul' := fun _ _ => trivial
      add' := fun _ _ => trivial }
  le_top _ := fun _ _ _h => trivial
  bot :=
    { (⊥ : Setoid R) with
      mul' := congr_arg₂ _
      add' := congr_arg₂ _ }
  bot_le c := fun x _y h => h ▸ c.refl x

Complete Lattice Structure on Ring Congruence Relations

Informal description

For any type $R$ with addition and multiplication, the collection of ring congruence relations on $R$ forms a complete lattice. The partial order is given by inclusion, where the infimum of a set of congruence relations is their intersection, and the supremum is the smallest congruence relation containing all of them.

RingCon.coe_top theorem

: ⇑(⊤ : RingCon R) = ⊤

Full source

@[simp, norm_cast]
theorem coe_top : ⇑(⊤ : RingCon R) = ⊤ := rfl

Top Ring Congruence is Universal Relation

Informal description

The top element in the lattice of ring congruence relations on $R$ corresponds to the universal relation, where every pair of elements in $R$ is related. That is, the function representation of the top congruence relation $\top$ is equal to the universal relation $\top$ on $R$.

RingCon.coe_bot theorem

: ⇑(⊥ : RingCon R) = Eq

Full source

@[simp, norm_cast]
theorem coe_bot : ⇑(⊥ : RingCon R) = Eq := rfl

Bottom Ring Congruence is Equality Relation

Informal description

The bottom element in the lattice of ring congruence relations on $R$ corresponds to the equality relation. That is, the function representation of the bottom congruence relation $\bot$ is equal to the equality relation on $R$.

RingCon.coe_inf theorem

{c d : RingCon R} : ⇑(c ⊓ d) = ⇑c ⊓ ⇑d

Full source

/-- The infimum of two congruence relations equals the infimum of the underlying binary
operations. -/
@[simp, norm_cast]
theorem coe_inf {c d : RingCon R} : ⇑(c ⊓ d) = ⇑c ⊓ ⇑d := rfl

Infimum of Ring Congruence Relations is Pointwise Infimum

Informal description

For any two ring congruence relations $c$ and $d$ on a ring $R$, the function representation of their infimum $c \sqcap d$ is equal to the pointwise infimum of the function representations of $c$ and $d$. That is, for all $x, y \in R$, $(c \sqcap d)(x, y) = c(x, y) \sqcap d(x, y)$.

RingCon.inf_iff_and theorem

{c d : RingCon R} {x y} : (c ⊓ d) x y ↔ c x y ∧ d x y

Full source

/-- Definition of the infimum of two congruence relations. -/
theorem inf_iff_and {c d : RingCon R} {x y} : (c ⊓ d) x y ↔ c x y ∧ d x y :=
  Iff.rfl

Characterization of Infimum of Ring Congruence Relations

Informal description

For any two ring congruence relations $c$ and $d$ on a ring $R$ (or more generally, a type with addition and multiplication), and for any elements $x, y \in R$, the infimum relation $c \sqcap d$ relates $x$ and $y$ if and only if both $c$ relates $x$ and $y$ and $d$ relates $x$ and $y$. In other words, $(c \sqcap d)(x, y) \leftrightarrow c(x, y) \land d(x, y)$.

RingCon.instNontrivial instance

[Nontrivial R] : Nontrivial (RingCon R)

Full source

instance [Nontrivial R] : Nontrivial (RingCon R) where
  exists_pair_ne :=
    let ⟨x, y, ne⟩ := exists_pair_ne R
    ⟨⊥, ⊤, ne_of_apply_ne (· x y) <| by simp [ne]⟩

Nontriviality of Ring Congruence Relations on Nontrivial Rings

Informal description

For any nontrivial ring $R$, the collection of ring congruence relations on $R$ is also nontrivial.

RingCon.instSubsingleton instance

[Subsingleton R] : Subsingleton (RingCon R)

Full source

instance [Subsingleton R] : Subsingleton (RingCon R) where
  allEq c c' := ext fun r r' ↦ by simp_rw [Subsingleton.elim r' r, c.refl, c'.refl]

Subsingleton Ring Implies Subsingleton Ring Congruence Relations

Informal description

For any ring $R$ that is a subsingleton (i.e., has at most one element), the type of ring congruence relations on $R$ is also a subsingleton.

RingCon.nontrivial_iff theorem

: Nontrivial (RingCon R) ↔ Nontrivial R

Full source

theorem nontrivial_iff : NontrivialNontrivial (RingCon R) ↔ Nontrivial R := by
  cases subsingleton_or_nontrivial R
  on_goal 1 => simp_rw [← not_subsingleton_iff_nontrivial, not_iff_not]
  all_goals exact iff_of_true inferInstance ‹_›

Nontriviality of Ring Congruence Relations $\leftrightarrow$ Nontriviality of Ring

Informal description

The type of ring congruence relations on a ring $R$ is nontrivial (contains at least two distinct relations) if and only if the ring $R$ itself is nontrivial (contains at least two distinct elements).

RingCon.subsingleton_iff theorem

: Subsingleton (RingCon R) ↔ Subsingleton R

Full source

theorem subsingleton_iff : SubsingletonSubsingleton (RingCon R) ↔ Subsingleton R := by
  simp_rw [← not_nontrivial_iff_subsingleton, nontrivial_iff]

Subsingleton Quotient Ring iff Subsingleton Original Ring

Informal description

The quotient ring $R$ modulo a congruence relation is a subsingleton (has at most one element) if and only if the original ring $R$ is a subsingleton.

RingCon.ringConGen_eq theorem

(r : R → R → Prop) : ringConGen r = sInf {s : RingCon R | ∀ x y, r x y → s x y}

Full source

/-- The inductively defined smallest congruence relation containing a binary relation `r` equals
    the infimum of the set of congruence relations containing `r`. -/
theorem ringConGen_eq (r : R → R → Prop) :
    ringConGen r = sInf {s : RingCon R | ∀ x y, r x y → s x y} :=
  le_antisymm
    (fun _x _y H =>
      RingConGen.Rel.recOn H (fun _ _ h _ hs => hs _ _ h) (RingCon.refl _)
        (fun _ => RingCon.symm _) (fun _ _ => RingCon.trans _)
        (fun _ _ h1 h2 c hc => c.add (h1 c hc) <| h2 c hc)
        (fun _ _ h1 h2 c hc => c.mul (h1 c hc) <| h2 c hc))
    (sInf_le fun _ _ => RingConGen.Rel.of _ _)

Smallest Ring Congruence Relation as Infimum of Containing Relations

Informal description

For any type $R$ with addition and multiplication, and any binary relation $r$ on $R$, the smallest ring congruence relation containing $r$ is equal to the infimum of all ring congruence relations on $R$ that contain $r$. In other words, $\text{ringConGen}(r) = \bigwedge \{s \in \text{RingCon}(R) \mid \forall x y, r(x,y) \to s(x,y)\}$.

RingCon.ringConGen_le theorem

{r : R → R → Prop} {c : RingCon R} (h : ∀ x y, r x y → c x y) : ringConGen r ≤ c

Full source

/-- The smallest congruence relation containing a binary relation `r` is contained in any
    congruence relation containing `r`. -/
theorem ringConGen_le {r : R → R → Prop} {c : RingCon R}
    (h : ∀ x y, r x y → c x y) : ringConGen r ≤ c := by
  rw [ringConGen_eq]; exact sInf_le h

Minimality of Generated Ring Congruence Relation

Informal description

For any type $R$ with addition and multiplication, given a binary relation $r$ on $R$ and a ring congruence relation $c$ on $R$ such that $r(x,y) \to c(x,y)$ for all $x,y \in R$, the smallest ring congruence relation containing $r$ is contained in $c$. In other words, if $r \subseteq c$, then $\text{ringConGen}(r) \leq c$.

RingCon.ringConGen_mono theorem

{r s : R → R → Prop} (h : ∀ x y, r x y → s x y) : ringConGen r ≤ ringConGen s

Full source

/-- Given binary relations `r, s` with `r` contained in `s`, the smallest congruence relation
    containing `s` contains the smallest congruence relation containing `r`. -/
theorem ringConGen_mono {r s : R → R → Prop} (h : ∀ x y, r x y → s x y) :
    ringConGen r ≤ ringConGen s :=
  ringConGen_le fun x y hr => RingConGen.Rel.of _ _ <| h x y hr

Monotonicity of the Smallest Ring Congruence Relation

Informal description

For any type $R$ with addition and multiplication, and for any two binary relations $r$ and $s$ on $R$ such that $r(x,y) \to s(x,y)$ for all $x,y \in R$, the smallest ring congruence relation containing $r$ is contained in the smallest ring congruence relation containing $s$. That is, $\text{ringConGen}(r) \leq \text{ringConGen}(s)$.

RingCon.ringConGen_of_ringCon theorem

(c : RingCon R) : ringConGen c = c

Full source

/-- Congruence relations equal the smallest congruence relation in which they are contained. -/
theorem ringConGen_of_ringCon (c : RingCon R) : ringConGen c = c :=
  le_antisymm (by rw [ringConGen_eq]; exact sInf_le fun _ _ => id) RingConGen.Rel.of

Smallest Ring Congruence Relation Containing Itself is Itself

Informal description

For any ring congruence relation $c$ on a type $R$ with addition and multiplication, the smallest ring congruence relation containing $c$ is equal to $c$ itself. That is, $\text{ringConGen}(c) = c$.

RingCon.ringConGen_idem theorem

(r : R → R → Prop) : ringConGen (ringConGen r) = ringConGen r

Full source

/-- The map sending a binary relation to the smallest congruence relation in which it is
    contained is idempotent. -/
theorem ringConGen_idem (r : R → R → Prop) : ringConGen (ringConGen r) = ringConGen r :=
  ringConGen_of_ringCon _

Idempotence of Ring Congruence Generation

Informal description

For any binary relation $r$ on a type $R$ with addition and multiplication, the smallest ring congruence relation generated by $r$ is idempotent. That is, applying the generation process twice yields the same result as applying it once: $\text{ringConGen}(\text{ringConGen}(r)) = \text{ringConGen}(r)$.

RingCon.sup_eq_ringConGen theorem

(c d : RingCon R) : c ⊔ d = ringConGen fun x y => c x y ∨ d x y

Full source

/-- The supremum of congruence relations `c, d` equals the smallest congruence relation containing
    the binary relation '`x` is related to `y` by `c` or `d`'. -/
theorem sup_eq_ringConGen (c d : RingCon R) : c ⊔ d = ringConGen fun x y => c x y ∨ d x y := by
  rw [ringConGen_eq]
  apply congr_arg sInf
  simp only [le_def, or_imp, ← forall_and]

Supremum of Ring Congruences as Generated Relation

Informal description

For any two ring congruence relations $c$ and $d$ on a ring $R$, their supremum $c \sqcup d$ in the lattice of congruence relations is equal to the smallest ring congruence relation containing the binary relation defined by $x \sim y$ if and only if $x \sim_c y$ or $x \sim_d y$.

RingCon.sup_def theorem

{c d : RingCon R} : c ⊔ d = ringConGen (⇑c ⊔ ⇑d)

Full source

/-- The supremum of two congruence relations equals the smallest congruence relation containing
    the supremum of the underlying binary operations. -/
theorem sup_def {c d : RingCon R} : c ⊔ d = ringConGen (⇑c ⊔ ⇑d) := by
  rw [sup_eq_ringConGen]; rfl

Supremum of Ring Congruences as Generated Pointwise Supremum

Informal description

For any two ring congruence relations $c$ and $d$ on a ring $R$, their supremum $c \sqcup d$ is equal to the smallest ring congruence relation containing the pointwise supremum of the underlying binary relations of $c$ and $d$.

RingCon.sSup_eq_ringConGen theorem

(S : Set (RingCon R)) : sSup S = ringConGen fun x y => ∃ c : RingCon R, c ∈ S ∧ c x y

Full source

/-- The supremum of a set of congruence relations `S` equals the smallest congruence relation
    containing the binary relation 'there exists `c ∈ S` such that `x` is related to `y` by
    `c`'. -/
theorem sSup_eq_ringConGen (S : Set (RingCon R)) :
    sSup S = ringConGen fun x y => ∃ c : RingCon R, c ∈ S ∧ c x y := by
  rw [ringConGen_eq]
  apply congr_arg sInf
  ext
  exact ⟨fun h _ _ ⟨r, hr⟩ => h hr.1 hr.2, fun h r hS _ _ hr => h _ _ ⟨r, hS, hr⟩⟩

Supremum of Ring Congruence Relations as Generated Relation

Informal description

For any set $S$ of ring congruence relations on a type $R$ with addition and multiplication, the supremum of $S$ is equal to the smallest ring congruence relation containing the binary relation "there exists a congruence relation $c \in S$ such that $x$ is related to $y$ under $c$". In other words, \[ \bigvee S = \text{ringConGen} \left( \lambda x y, \exists c \in S, c(x, y) \right). \]

RingCon.sSup_def theorem

{S : Set (RingCon R)} : sSup S = ringConGen (sSup (@Set.image (RingCon R) (R → R → Prop) (⇑) S))

Full source

/-- The supremum of a set of congruence relations is the same as the smallest congruence relation
    containing the supremum of the set's image under the map to the underlying binary relation. -/
theorem sSup_def {S : Set (RingCon R)} :
    sSup S = ringConGen (sSup (@Set.image (RingCon R) (R → R → Prop) (⇑) S)) := by
  rw [sSup_eq_ringConGen, sSup_image]
  congr with (x y)
  simp only [sSup_image, iSup_apply, iSup_Prop_eq, exists_prop, rel_eq_coe]

Supremum of Ring Congruence Relations as Generated Supremum of Binary Relations

Informal description

For any set $S$ of ring congruence relations on a type $R$ with addition and multiplication, the supremum of $S$ is equal to the smallest ring congruence relation containing the supremum of the image of $S$ under the canonical map from ring congruence relations to binary relations. In other words, \[ \bigvee S = \text{ringConGen}\left(\bigvee \{\, c \mid c \in S \,\}\right), \] where $\bigvee$ on the right denotes the supremum of binary relations.

RingCon.gi definition

: @GaloisInsertion (R → R → Prop) (RingCon R) _ _ ringConGen (⇑)

Full source

/-- There is a Galois insertion of congruence relations on a type with multiplication and addition
`R` into binary relations on `R`. -/
protected def gi : @GaloisInsertion (R → R → Prop) (RingCon R) _ _ ringConGen (⇑) where
  choice r _h := ringConGen r
  gc _r c :=
    ⟨fun H _ _ h => H <| RingConGen.Rel.of _ _ h, fun H =>
      ringConGen_of_ringCon c ▸ ringConGen_mono H⟩
  le_l_u x := (ringConGen_of_ringCon x).symm ▸ le_refl x
  choice_eq _ _ := rfl

Galois insertion for ring congruence relations

Informal description

There is a Galois insertion between the set of binary relations on a type $R$ with addition and multiplication and the set of ring congruence relations on $R$. The lower adjoint is the function `ringConGen` that generates the smallest ring congruence relation containing a given binary relation, and the upper adjoint is the canonical inclusion map from ring congruence relations to binary relations.

Mathlib.RingTheory.Congruence.Basic

Main Definitions

TODO