# mathlib3documentation

ring_theory.congruence

# Congruence relations on rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines congruence relations on rings, which extend con and add_con 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 #

• ring_con R: the type of congruence relations respecting + and *.
• ring_con_gen r: the inductively defined smallest ring congruence relation containing a given binary relation.

## TODO #

• Use this for ring_quot too.
• Copy across more API from con and add_con in group_theory/congruence.lean, such as:
• The complete_lattice structure.
• The con_gen_eq lemma, stating that ring_con_gen r = Inf {s : ring_con M | ∀ x y, r x y → s x y}.
structure ring_con (R : Type u_1) [has_add R] [has_mul R] :
Type u_1

A congruence relation on a type with an addition and multiplication is an equivalence relation which preserves both.

Instances for ring_con
inductive ring_con_gen.rel {R : Type u_2} [has_add R] [has_mul R] (r : R R Prop) :
R R Prop

The inductively defined smallest ring congruence relation containing a given binary relation.

def ring_con_gen {R : Type u_2} [has_add R] [has_mul R] (r : R R Prop) :

The inductively defined smallest ring congruence relation containing a given binary relation.

Equations
def ring_con.to_add_con {R : Type u_2} [has_add R] [has_mul R] (c : ring_con R) :

Every ring_con is also an add_con

Equations
def ring_con.to_con {R : Type u_2} [has_add R] [has_mul R] (c : ring_con R) :
con R

Every ring_con is also a con

Equations
@[protected, instance]
def ring_con.has_coe_to_fun {R : Type u_2} [has_add R] [has_mul R] :
(λ (_x : ring_con R), R R Prop)

A coercion from a congruence relation to its underlying binary relation.

Equations
@[simp]
theorem ring_con.rel_eq_coe {R : Type u_2} [has_add R] [has_mul R] (c : ring_con R) :
@[protected]
theorem ring_con.refl {R : Type u_2} [has_add R] [has_mul R] (c : ring_con R) (x : R) :
c x x
@[protected]
theorem ring_con.symm {R : Type u_2} [has_add R] [has_mul R] (c : ring_con R) {x y : R} :
c x y c y x
@[protected]
theorem ring_con.trans {R : Type u_2} [has_add R] [has_mul R] (c : ring_con R) {x y z : R} :
c x y c y z c x z
@[protected]
theorem ring_con.add {R : Type u_2} [has_add R] [has_mul R] (c : ring_con R) {w x y z : R} :
c w x c y z c (w + y) (x + z)
@[protected]
theorem ring_con.mul {R : Type u_2} [has_add R] [has_mul R] (c : ring_con R) {w x y z : R} :
c w x c y z c (w * y) (x * z)
@[simp]
theorem ring_con.rel_mk {R : Type u_2} [has_add R] [has_mul R] {s : setoid R} {ha : {w x y z : R}, x z setoid.r (w + y) (x + z)} {hm : {w x y z : R}, x z setoid.r (w * y) (x * z)} {a b : R} :
{to_setoid := s, add' := ha, mul' := hm} a b b
@[protected, instance]
def ring_con.inhabited {R : Type u_2} [has_add R] [has_mul R] :
Equations
@[protected]
def ring_con.quotient {R : Type u_2} [has_add R] [has_mul R] (c : ring_con R) :
Type u_2

Defining the quotient by a congruence relation of a type with addition and multiplication.

Equations
Instances for ring_con.quotient
@[protected, instance]
def ring_con.quotient.has_coe_t {R : Type u_2} [has_add R] [has_mul R] (c : ring_con R) :

Coercion from a type with addition and multiplication to its quotient by a congruence relation.

Equations
@[protected, instance]
def ring_con.quotient.decidable_eq {R : Type u_2} [has_add R] [has_mul R] (c : ring_con R) [d : Π (a b : R), decidable (c a b)] :

The quotient by a decidable congruence relation has decidable equality.

Equations
@[simp]
theorem ring_con.quot_mk_eq_coe {R : Type u_2} [has_add R] [has_mul R] (c : ring_con R) (x : R) :
quot.mk c x = x
@[protected, simp]
theorem ring_con.eq {R : Type u_2} [has_add R] [has_mul R] (c : ring_con R) {a b : R} :
a = b c a b

Two elements are related by a congruence relation c iff they are represented by the same element of the quotient by c.

### Basic notation #

The basic algebraic notation, 0, 1, +, *, -, ^, descend naturally under the quotient

@[protected, instance]
def ring_con.quotient.has_add {R : Type u_2} [has_add R] [has_mul R] (c : ring_con R) :
Equations
@[simp, norm_cast]
theorem ring_con.coe_add {R : Type u_2} [has_add R] [has_mul R] (c : ring_con R) (x y : R) :
(x + y) = x + y
@[protected, instance]
def ring_con.quotient.has_mul {R : Type u_2} [has_add R] [has_mul R] (c : ring_con R) :
Equations
@[simp, norm_cast]
theorem ring_con.coe_mul {R : Type u_2} [has_add R] [has_mul R] (c : ring_con R) (x y : R) :
(x * y) = x * y
@[protected, instance]
def ring_con.quotient.has_zero {R : Type u_2} [has_mul R] (c : ring_con R) :
Equations
@[simp, norm_cast]
theorem ring_con.coe_zero {R : Type u_2} [has_mul R] (c : ring_con R) :
0 = 0
@[protected, instance]
def ring_con.quotient.has_one {R : Type u_2} [has_add R] (c : ring_con R) :
Equations
@[simp, norm_cast]
theorem ring_con.coe_one {R : Type u_2} [has_add R] (c : ring_con R) :
1 = 1
@[protected, instance]
def ring_con.quotient.has_smul {α : Type u_1} {R : Type u_2} [has_add R] [ R] [ R] (c : ring_con R) :
Equations
@[simp, norm_cast]
theorem ring_con.coe_smul {α : Type u_1} {R : Type u_2} [has_add R] [ R] [ R] (c : ring_con R) (a : α) (x : R) :
(a x) = a x
@[protected, instance]
def ring_con.quotient.has_neg {R : Type u_2} [add_group R] [has_mul R] (c : ring_con R) :
Equations
@[simp, norm_cast]
theorem ring_con.coe_neg {R : Type u_2} [add_group R] [has_mul R] (c : ring_con R) (x : R) :
@[protected, instance]
def ring_con.quotient.has_sub {R : Type u_2} [add_group R] [has_mul R] (c : ring_con R) :
Equations
@[simp, norm_cast]
theorem ring_con.coe_sub {R : Type u_2} [add_group R] [has_mul R] (c : ring_con R) (x y : R) :
(x - y) = x - y
@[protected, instance]
def ring_con.has_zsmul {R : Type u_2} [add_group R] [has_mul R] (c : ring_con R) :
Equations
@[simp, norm_cast]
theorem ring_con.coe_zsmul {R : Type u_2} [add_group R] [has_mul R] (c : ring_con R) (z : ) (x : R) :
(z x) = z x
@[protected, instance]
def ring_con.has_nsmul {R : Type u_2} [add_monoid R] [has_mul R] (c : ring_con R) :
Equations
@[simp, norm_cast]
theorem ring_con.coe_nsmul {R : Type u_2} [add_monoid R] [has_mul R] (c : ring_con R) (n : ) (x : R) :
(n x) = n x
@[protected, instance]
def ring_con.nat.has_pow {R : Type u_2} [has_add R] [monoid R] (c : ring_con R) :
Equations
@[simp, norm_cast]
theorem ring_con.coe_pow {R : Type u_2} [has_add R] [monoid R] (c : ring_con R) (x : R) (n : ) :
(x ^ n) = x ^ n
@[protected, instance]
def ring_con.quotient.has_nat_cast {R : Type u_2} [has_mul R] (c : ring_con R) :
Equations
@[simp, norm_cast]
theorem ring_con.coe_nat_cast {R : Type u_2} [has_mul R] (c : ring_con R) (n : ) :
@[protected, instance]
def ring_con.quotient.has_int_cast {R : Type u_2} [has_mul R] (c : ring_con R) :
Equations
@[simp, norm_cast]
theorem ring_con.coe_int_cast {R : Type u_2} [has_mul R] (c : ring_con R) (n : ) :
@[protected, instance]
def ring_con.quotient.inhabited {R : Type u_2} [inhabited R] [has_add R] [has_mul R] (c : ring_con R) :
Equations

### Algebraic structure #

The operations above on the quotient by c : ring_con R preseverse the algebraic structure of R.

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def ring_con.quotient.semiring {R : Type u_2} [semiring R] (c : ring_con R) :
Equations
• = _ _ _ _
@[protected, instance]
def ring_con.quotient.comm_semiring {R : Type u_2} (c : ring_con R) :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
• = _ _ _ _ _ _
@[protected, instance]
Equations
@[protected, instance]
def ring_con.quotient.ring {R : Type u_2} [ring R] (c : ring_con R) :
Equations
• = _ _ _ _ _ _ _ _
@[protected, instance]
def ring_con.quotient.comm_ring {R : Type u_2} [comm_ring R] (c : ring_con R) :
Equations
• = _ _ _ _ _ _ _
@[protected, instance]
def ring_con.is_scalar_tower_right {α : Type u_1} {R : Type u_2} [has_add R] [ R] [ R] (c : ring_con R) :
@[protected, instance]
def ring_con.smul_comm_class {α : Type u_1} {R : Type u_2} [has_add R] [ R] [ R] [ R] (c : ring_con R) :
@[protected, instance]
def ring_con.smul_comm_class' {α : Type u_1} {R : Type u_2} [has_add R] [ R] [ R] [ R] (c : ring_con R) :
@[protected, instance]
def ring_con.quotient.distrib_mul_action {α : Type u_1} {R : Type u_2} [monoid α] [ R] [ R] (c : ring_con R) :
Equations
@[protected, instance]
def ring_con.quotient.mul_semiring_action {α : Type u_1} {R : Type u_2} [monoid α] [semiring R] [ R] [ R] (c : ring_con R) :
Equations
def ring_con.mk' {R : Type u_2} (c : ring_con R) :

The natural homomorphism from a ring to its quotient by a congruence relation.

Equations