# Congruence relations on rings #

This file contains basic results concerning congruence relations on rings, which extend `Con` and `AddCon` on monoids and additive monoids.

Most of the time you likely want to use the `Ideal.Quotient` API that is built on top of this.

## Main Definitions #

- `RingCon R`: the type of congruence relations respecting `+` and `*`.
- `RingConGen r`: the inductively defined smallest ring congruence relation containing a given binary relation.

## TODO #

- Use this for `RingQuot` too.
- Copy across more API from `Con` and `AddCon` in `GroupTheory/Congruence.lean`.

### Scalar multiplication #

The operation of scalar multiplication `•` descends naturally to the quotient.

source
instance RingCon.instSMulQuotient {α : Type u_1} {R : Type u_3} [Add R] [MulOneClass R] [SMul α R] [IsScalarTower α R R] (c : RingCon R) :
SMul α c.Quotient
Equations

- c.instSMulQuotient = inferInstanceAs (SMul α c.Quotient)

source
@[simp]
theorem RingCon.coe_smul {α : Type u_1} {R : Type u_3} [Add R] [MulOneClass R] [SMul α R] [IsScalarTower α R R] (c : RingCon R) (a : α) (x : R) :
↑(a • x) = a • ↑x
source
instance RingCon.instSMulCommClassQuotient {α : Type u_1} {β : Type u_2} {R : Type u_3} [Add R] [MulOneClass R] [SMul α R] [IsScalarTower α R R] [SMul β R] [IsScalarTower β R R] (c : RingCon R) [SMulCommClass α β R] :
SMulCommClass α β c.Quotient
source
instance RingCon.instIsScalarTowerQuotient {α : Type u_1} {β : Type u_2} {R : Type u_3} [Add R] [MulOneClass R] [SMul α R] [IsScalarTower α R R] [SMul β R] [IsScalarTower β R R] (c : RingCon R) [SMul α β] [IsScalarTower α β R] :
IsScalarTower α β c.Quotient
source
instance RingCon.instIsCentralScalarQuotient {α : Type u_1} {R : Type u_3} [Add R] [MulOneClass R] [SMul α R] [IsScalarTower α R R] (c : RingCon R) [SMul α ᵐᵒᵖ R] [IsCentralScalar α R] :
IsCentralScalar α c.Quotient
source
instance RingCon.isScalarTower_right {α : Type u_1} {R : Type u_3} [Add R] [MulOneClass R] [SMul α R] [IsScalarTower α R R] (c : RingCon R) :
IsScalarTower α c.Quotient c.Quotient
source
instance RingCon.smulCommClass {α : Type u_1} {R : Type u_3} [Add R] [MulOneClass R] [SMul α R] [IsScalarTower α R R] [SMulCommClass α R R] (c : RingCon R) :
SMulCommClass α c.Quotient c.Quotient
source
instance RingCon.smulCommClass' {α : Type u_1} {R : Type u_3} [Add R] [MulOneClass R] [SMul α R] [IsScalarTower α R R] [SMulCommClass R α R] (c : RingCon R) :
SMulCommClass c.Quotient α c.Quotient
source
instance RingCon.instDistribMulActionQuotientOfIsScalarTower {α : Type u_1} {R : Type u_3} [Monoid α] [NonAssocSemiring R] [DistribMulAction α R] [IsScalarTower α R R] (c : RingCon R) :
DistribMulAction α c.Quotient
Equations

- c.instDistribMulActionQuotientOfIsScalarTower = { toMulAction := c.mulAction, smul_zero := ⋯, smul_add := ⋯ }

source
instance RingCon.instMulSemiringActionQuotientOfIsScalarTower {α : Type u_1} {R : Type u_3} [Monoid α] [Semiring R] [MulSemiringAction α R] [IsScalarTower α R R] (c : RingCon R) :
MulSemiringAction α c.Quotient
Equations

- c.instMulSemiringActionQuotientOfIsScalarTower = { toDistribMulAction := c.instDistribMulActionQuotientOfIsScalarTower, smul_one := ⋯, smul_mul := ⋯ }

### Lattice structure #

The API in this section is copied from `Mathlib/GroupTheory/Congruence.lean`

source
instance RingCon.instLE {R : Type u_3} [Add R] [Mul R] :
LE (RingCon R)

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`.

Equations

- RingCon.instLE = { le := fun (c d : RingCon R) => ∀ ⦃x y : R⦄, c x y → d x y }

source
theorem RingCon.le_def {R : Type u_3} [Add R] [Mul R] {c d : RingCon R} :
c ≤ d ↔ ∀ {x y : R}, c x y → d x y

Definition of `≤` for congruence relations.

source
instance RingCon.instInfSet {R : Type u_3} [Add R] [Mul R] :
InfSet (RingCon R)

The infimum of a set of congruence relations on a given type with multiplication and addition.

Equations

- RingCon.instInfSet = { sInf := fun (S : Set (RingCon R)) => { r := fun (x y : R) => ∀ c ∈ S, c x y, iseqv := ⋯, mul' := ⋯, add' := ⋯ } }

source
theorem RingCon.sInf_toSetoid {R : Type u_3} [Add R] [Mul R] (S : Set (RingCon R)) :
(sInf S).toSetoid = sInf ((fun (x : RingCon R) => x.toSetoid) '' S)

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.

source
@[simp]
theorem RingCon.coe_sInf {R : Type u_3} [Add R] [Mul R] (S : Set (RingCon R)) :
⇑(sInf S) = sInf (DFunLike.coe '' S)

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.

source
@[simp]
theorem RingCon.coe_iInf {R : Type u_3} [Add R] [Mul R] {ι : Sort u_4} (f : ι → RingCon R) :
⇑(iInf f) = ⨅ (i : ι), ⇑(f i)
source
instance RingCon.instPartialOrder {R : Type u_3} [Add R] [Mul R] :
PartialOrder (RingCon R)
Equations

- RingCon.instPartialOrder = { toLE := RingCon.instLE, lt := fun (a b : RingCon R) => a ≤ b ∧ ¬b ≤ a, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

source
instance RingCon.instCompleteLattice {R : Type u_3} [Add R] [Mul R] :
CompleteLattice (RingCon R)

The complete lattice of congruence relations on a given type with multiplication and addition.

Equations

- One or more equations did not get rendered due to their size.

source
@[simp]
theorem RingCon.coe_top {R : Type u_3} [Add R] [Mul R] :
⇑⊤ = ⊤
source
@[simp]
theorem RingCon.coe_bot {R : Type u_3} [Add R] [Mul R] :
⇑⊥ = Eq
source
@[simp]
theorem RingCon.coe_inf {R : Type u_3} [Add R] [Mul R] {c d : RingCon R} :
⇑(c ⊓ d) = ⇑c ⊓ ⇑d

The infimum of two congruence relations equals the infimum of the underlying binary operations.

source
theorem RingCon.inf_iff_and {R : Type u_3} [Add R] [Mul R] {c d : RingCon R} {x y : R} :
(c ⊓ d) x y ↔ c x y ∧ d x y

Definition of the infimum of two congruence relations.

source
instance RingCon.instNontrivial {R : Type u_3} [Add R] [Mul R] [Nontrivial R] :
Nontrivial (RingCon R)
source
instance RingCon.instSubsingleton {R : Type u_3} [Add R] [Mul R] [Subsingleton R] :
Subsingleton (RingCon R)
source
theorem RingCon.nontrivial_iff {R : Type u_3} [Add R] [Mul R] :
Nontrivial (RingCon R) ↔ Nontrivial R
source
theorem RingCon.subsingleton_iff {R : Type u_3} [Add R] [Mul R] :
Subsingleton (RingCon R) ↔ Subsingleton R
source
theorem RingCon.ringConGen_eq {R : Type u_3} [Add R] [Mul R] (r : R → R → Prop) :
ringConGen r = sInf {s : RingCon R | ∀ (x y : R), r x y → s x y}

The inductively defined smallest congruence relation containing a binary relation `r` equals the infimum of the set of congruence relations containing `r`.

source
theorem RingCon.ringConGen_le {R : Type u_3} [Add R] [Mul R] {r : R → R → Prop} {c : RingCon R} (h : ∀ (x y : R), r x y → c x y) :
ringConGen r ≤ c

The smallest congruence relation containing a binary relation `r` is contained in any congruence relation containing `r`.

source
theorem RingCon.ringConGen_mono {R : Type u_3} [Add R] [Mul R] {r s : R → R → Prop} (h : ∀ (x y : R), r x y → s x y) :
ringConGen r ≤ ringConGen s

Given binary relations `r, s` with `r` contained in `s`, the smallest congruence relation containing `s` contains the smallest congruence relation containing `r`.

source
theorem RingCon.ringConGen_of_ringCon {R : Type u_3} [Add R] [Mul R] (c : RingCon R) :
ringConGen ⇑c = c

Congruence relations equal the smallest congruence relation in which they are contained.

source
theorem RingCon.ringConGen_idem {R : Type u_3} [Add R] [Mul R] (r : R → R → Prop) :
ringConGen ⇑(ringConGen r) = ringConGen r

The map sending a binary relation to the smallest congruence relation in which it is contained is idempotent.

source
theorem RingCon.sup_eq_ringConGen {R : Type u_3} [Add R] [Mul R] (c d : RingCon R) :
c ⊔ d = ringConGen fun (x y : R) => c x y ∨ d x y

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`'.

source
theorem RingCon.sup_def {R : Type u_3} [Add R] [Mul R] {c d : RingCon R} :
c ⊔ d = ringConGen (⇑c ⊔ ⇑d)

The supremum of two congruence relations equals the smallest congruence relation containing the supremum of the underlying binary operations.

source
theorem RingCon.sSup_eq_ringConGen {R : Type u_3} [Add R] [Mul R] (S : Set (RingCon R)) :
sSup S = ringConGen fun (x y : R) => ∃ c ∈ S, c x y

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`'.

source
theorem RingCon.sSup_def {R : Type u_3} [Add R] [Mul R] {S : Set (RingCon R)} :
sSup S = ringConGen (sSup (DFunLike.coe '' S))

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.

source
def RingCon.gi (R : Type u_3) [Add R] [Mul R] :
GaloisInsertion ringConGen DFunLike.coe

There is a Galois insertion of congruence relations on a type with multiplication and addition `R` into binary relations on `R`.

Equations

- RingCon.gi R = { choice := fun (r : R → R → Prop) (_h : ⇑(ringConGen r) ≤ r) => ringConGen r, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

Instances For