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

source

structure ring_con (R : Type u_1) [has_add R] [has_mul R] :

Type u_1

to_setoid : setoid R
add' : ∀ {w x y z : R}, setoid.r w x → setoid.r y z → setoid.r (w + y) (x + z)
mul' : ∀ {w x y z : R}, setoid.r w x → setoid.r y z → setoid.r (w * y) (x * z)

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

Instances for ring_con

ring_con.has_sizeof_inst
ring_con.has_coe_to_fun
ring_con.inhabited

source

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

R → R → Prop

of : ∀ {R : Type u_2} [_inst_1 : has_add R] [_inst_2 : has_mul R] {r : R → R → Prop} (x y : R), r x y → ring_con_gen.rel r x y
refl : ∀ {R : Type u_2} [_inst_1 : has_add R] [_inst_2 : has_mul R] {r : R → R → Prop} (x : R), ring_con_gen.rel r x x
symm : ∀ {R : Type u_2} [_inst_1 : has_add R] [_inst_2 : has_mul R] {r : R → R → Prop} {x y : R}, ring_con_gen.rel r x y → ring_con_gen.rel r y x
trans : ∀ {R : Type u_2} [_inst_1 : has_add R] [_inst_2 : has_mul R] {r : R → R → Prop} {x y z : R}, ring_con_gen.rel r x y → ring_con_gen.rel r y z → ring_con_gen.rel r x z
add : ∀ {R : Type u_2} [_inst_1 : has_add R] [_inst_2 : has_mul R] {r : R → R → Prop} {w x y z : R}, ring_con_gen.rel r w x → ring_con_gen.rel r y z → ring_con_gen.rel r (w + y) (x + z)
mul : ∀ {R : Type u_2} [_inst_1 : has_add R] [_inst_2 : has_mul R] {r : R → R → Prop} {w x y z : R}, ring_con_gen.rel r w x → ring_con_gen.rel r y z → ring_con_gen.rel r (w * y) (x * z)

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

source

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

ring_con R

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

Equations

ring_con_gen r = {to_setoid := {r := ring_con_gen.rel r, iseqv := _}, add' := _, mul' := _}

source

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

add_con R

Every ring_con is also an add_con

Equations

c.to_add_con = {to_setoid := c.to_setoid, add' := _}

source

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

c.to_con = {to_setoid := c.to_setoid, mul' := _}

source

@[protected, instance]

def ring_con.has_coe_to_fun {R : Type u_2} [has_add R] [has_mul R] :

has_coe_to_fun (ring_con R) (λ (_x : ring_con R), R → R → Prop)

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

Equations

ring_con.has_coe_to_fun = {coe := λ (c : ring_con R), setoid.r}

source

@[simp]

theorem ring_con.rel_eq_coe {R : Type u_2} [has_add R] [has_mul R] (c : ring_con R) :

setoid.r = ⇑c

source

@[protected]

theorem ring_con.refl {R : Type u_2} [has_add R] [has_mul R] (c : ring_con R) (x : R) :

⇑c x x

source

@[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

source

@[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

source

@[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)

source

@[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)

source

@[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}, setoid.r w x → setoid.r y z → setoid.r (w + y) (x + z)} {hm : ∀ {w x y z : R}, setoid.r w x → setoid.r y z → setoid.r (w * y) (x * z)} {a b : R} :

⇑{to_setoid := s, add' := ha, mul' := hm} a b ↔ setoid.r a b

source

@[protected, instance]

def ring_con.inhabited {R : Type u_2} [has_add R] [has_mul R] :

inhabited (ring_con R)

Equations

ring_con.inhabited = {default := ring_con_gen empty_relation}

source

@[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

c.quotient = quotient c.to_setoid

Instances for ring_con.quotient

source

@[protected, instance]

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

has_coe_t R c.quotient

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

See Note [use has_coe_t].

Equations

ring_con.quotient.has_coe_t c = {coe := quotient.mk c.to_setoid}

source

@[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)] :

decidable_eq c.quotient

The quotient by a decidable congruence relation has decidable equality.

Equations

ring_con.quotient.decidable_eq c = quotient.decidable_eq

source

@[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

source

@[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

source

@[protected, instance]

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

has_add c.quotient

Equations

ring_con.quotient.has_add c = c.to_add_con.has_add

source

@[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

source

@[protected, instance]

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

has_mul c.quotient

Equations

ring_con.quotient.has_mul c = c.to_con.has_mul

source

@[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

source

@[protected, instance]

def ring_con.quotient.has_zero {R : Type u_2} [add_zero_class R] [has_mul R] (c : ring_con R) :

has_zero c.quotient

Equations

ring_con.quotient.has_zero c = add_con.quotient.has_zero c.to_add_con

source

@[simp, norm_cast]

theorem ring_con.coe_zero {R : Type u_2} [add_zero_class R] [has_mul R] (c : ring_con R) :

↑0 = 0

source

@[protected, instance]

def ring_con.quotient.has_one {R : Type u_2} [has_add R] [mul_one_class R] (c : ring_con R) :

has_one c.quotient

Equations

ring_con.quotient.has_one c = con.quotient.has_one c.to_con

source

@[simp, norm_cast]

theorem ring_con.coe_one {R : Type u_2} [has_add R] [mul_one_class R] (c : ring_con R) :

↑1 = 1

source

@[protected, instance]

def ring_con.quotient.has_smul {α : Type u_1} {R : Type u_2} [has_add R] [mul_one_class R] [has_smul α R] [is_scalar_tower α R R] (c : ring_con R) :

has_smul α c.quotient

Equations

ring_con.quotient.has_smul c = c.to_con.has_smul

source

@[simp, norm_cast]

theorem ring_con.coe_smul {α : Type u_1} {R : Type u_2} [has_add R] [mul_one_class R] [has_smul α R] [is_scalar_tower α R R] (c : ring_con R) (a : α) (x : R) :

↑(a • x) = a • ↑x

source

@[protected, instance]

def ring_con.quotient.has_neg {R : Type u_2} [add_group R] [has_mul R] (c : ring_con R) :

has_neg c.quotient

Equations

ring_con.quotient.has_neg c = c.to_add_con.has_neg

source

@[simp, norm_cast]

theorem ring_con.coe_neg {R : Type u_2} [add_group R] [has_mul R] (c : ring_con R) (x : R) :

↑-x = -↑x

source

@[protected, instance]

def ring_con.quotient.has_sub {R : Type u_2} [add_group R] [has_mul R] (c : ring_con R) :

has_sub c.quotient

Equations

ring_con.quotient.has_sub c = c.to_add_con.has_sub

source

@[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

source

@[protected, instance]

def ring_con.has_zsmul {R : Type u_2} [add_group R] [has_mul R] (c : ring_con R) :

has_smul ℤ c.quotient

Equations

c.has_zsmul = add_con.quotient.has_zsmul c.to_add_con

source

@[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

source

@[protected, instance]

def ring_con.has_nsmul {R : Type u_2} [add_monoid R] [has_mul R] (c : ring_con R) :

has_smul ℕ c.quotient

Equations

c.has_nsmul = add_con.quotient.has_nsmul c.to_add_con

source

@[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

source

@[protected, instance]

def ring_con.nat.has_pow {R : Type u_2} [has_add R] [monoid R] (c : ring_con R) :

has_pow c.quotient ℕ

Equations

ring_con.nat.has_pow c = con.nat.has_pow c.to_con

source

@[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

source

@[protected, instance]

def ring_con.quotient.has_nat_cast {R : Type u_2} [add_monoid_with_one R] [has_mul R] (c : ring_con R) :

has_nat_cast c.quotient

Equations

ring_con.quotient.has_nat_cast c = {nat_cast := λ (n : ℕ), ↑↑n}

source

@[simp, norm_cast]

theorem ring_con.coe_nat_cast {R : Type u_2} [add_monoid_with_one R] [has_mul R] (c : ring_con R) (n : ℕ) :

↑↑n = ↑n

source

@[protected, instance]

def ring_con.quotient.has_int_cast {R : Type u_2} [add_group_with_one R] [has_mul R] (c : ring_con R) :

has_int_cast c.quotient

Equations

ring_con.quotient.has_int_cast c = {int_cast := λ (z : ℤ), ↑↑z}

source

@[simp, norm_cast]

theorem ring_con.coe_int_cast {R : Type u_2} [add_group_with_one R] [has_mul R] (c : ring_con R) (n : ℕ) :

↑↑n = ↑n

source

@[protected, instance]

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

inhabited c.quotient

Equations

ring_con.quotient.inhabited c = {default := ↑inhabited.default}

Algebraic structure #

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

source

@[protected, instance]

def ring_con.quotient.non_unital_non_assoc_semiring {R : Type u_2} [non_unital_non_assoc_semiring R] (c : ring_con R) :

non_unital_non_assoc_semiring c.quotient

Equations

ring_con.quotient.non_unital_non_assoc_semiring c = function.surjective.non_unital_non_assoc_semiring quotient.mk' _ _ _ _ _

source

@[protected, instance]

def ring_con.quotient.non_assoc_semiring {R : Type u_2} [non_assoc_semiring R] (c : ring_con R) :

non_assoc_semiring c.quotient

Equations

ring_con.quotient.non_assoc_semiring c = function.surjective.non_assoc_semiring quotient.mk' _ _ _ _ _ _ _

source

@[protected, instance]

def ring_con.quotient.non_unital_semiring {R : Type u_2} [non_unital_semiring R] (c : ring_con R) :

non_unital_semiring c.quotient

Equations

ring_con.quotient.non_unital_semiring c = function.surjective.non_unital_semiring quotient.mk' _ _ _ _ _

source

@[protected, instance]

def ring_con.quotient.semiring {R : Type u_2} [semiring R] (c : ring_con R) :

semiring c.quotient

Equations

ring_con.quotient.semiring c = function.surjective.semiring quotient.mk' _ _ _ _ _ _ _ _

source

@[protected, instance]

def ring_con.quotient.comm_semiring {R : Type u_2} [comm_semiring R] (c : ring_con R) :

comm_semiring c.quotient

Equations

ring_con.quotient.comm_semiring c = function.surjective.comm_semiring quotient.mk' _ _ _ _ _ _ _ _

source

@[protected, instance]

def ring_con.quotient.non_unital_non_assoc_ring {R : Type u_2} [non_unital_non_assoc_ring R] (c : ring_con R) :

non_unital_non_assoc_ring c.quotient

Equations

ring_con.quotient.non_unital_non_assoc_ring c = function.surjective.non_unital_non_assoc_ring quotient.mk' _ _ _ _ _ _ _ _

source

@[protected, instance]

def ring_con.quotient.non_assoc_ring {R : Type u_2} [non_assoc_ring R] (c : ring_con R) :

non_assoc_ring c.quotient

Equations

ring_con.quotient.non_assoc_ring c = function.surjective.non_assoc_ring quotient.mk' _ _ _ _ _ _ _ _ _ _ _

source

@[protected, instance]

def ring_con.quotient.non_unital_ring {R : Type u_2} [non_unital_ring R] (c : ring_con R) :

non_unital_ring c.quotient

Equations

ring_con.quotient.non_unital_ring c = function.surjective.non_unital_ring quotient.mk' _ _ _ _ _ _ _ _

source

@[protected, instance]

def ring_con.quotient.ring {R : Type u_2} [ring R] (c : ring_con R) :

ring c.quotient

Equations

ring_con.quotient.ring c = function.surjective.ring quotient.mk' _ _ _ _ _ _ _ _ _ _ _ _

source

@[protected, instance]

def ring_con.quotient.comm_ring {R : Type u_2} [comm_ring R] (c : ring_con R) :

comm_ring c.quotient

Equations

ring_con.quotient.comm_ring c = function.surjective.comm_ring quotient.mk' _ _ _ _ _ _ _ _ _ _ _ _

source

@[protected, instance]

def ring_con.is_scalar_tower_right {α : Type u_1} {R : Type u_2} [has_add R] [mul_one_class R] [has_smul α R] [is_scalar_tower α R R] (c : ring_con R) :

is_scalar_tower α c.quotient c.quotient

source

@[protected, instance]

def ring_con.smul_comm_class {α : Type u_1} {R : Type u_2} [has_add R] [mul_one_class R] [has_smul α R] [is_scalar_tower α R R] [smul_comm_class α R R] (c : ring_con R) :

smul_comm_class α c.quotient c.quotient

source

@[protected, instance]

def ring_con.smul_comm_class' {α : Type u_1} {R : Type u_2} [has_add R] [mul_one_class R] [has_smul α R] [is_scalar_tower α R R] [smul_comm_class R α R] (c : ring_con R) :

smul_comm_class c.quotient α c.quotient

source

@[protected, instance]

def ring_con.quotient.distrib_mul_action {α : Type u_1} {R : Type u_2} [monoid α] [non_assoc_semiring R] [distrib_mul_action α R] [is_scalar_tower α R R] (c : ring_con R) :

distrib_mul_action α c.quotient

Equations

ring_con.quotient.distrib_mul_action c = {to_mul_action := {to_has_smul := {smul := has_smul.smul (ring_con.quotient.has_smul c)}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}

source

@[protected, instance]

def ring_con.quotient.mul_semiring_action {α : Type u_1} {R : Type u_2} [monoid α] [semiring R] [mul_semiring_action α R] [is_scalar_tower α R R] (c : ring_con R) :

mul_semiring_action α c.quotient

Equations

ring_con.quotient.mul_semiring_action c = {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := has_smul.smul (ring_con.quotient.has_smul c)}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, smul_one := _, smul_mul := _}

source

def ring_con.mk' {R : Type u_2} [non_assoc_semiring R] (c : ring_con R) :

R →+* c.quotient

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

Equations

c.mk' = {to_fun := quotient.mk' c.to_setoid, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}