Congruence relations on rings

This file defines 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.

structure RingCon (R : Type u_1) [Add R] [Mul R] extends Con : Type u_1

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

• r : R → R → Prop
• iseqv : Equivalence ⇑self.toSetoid
• mul' : ∀ {w x y z : R}, self.toSetoid w x → self.toSetoid y z → self.toSetoid (w * y) (x * z)
• add' : ∀ {w x y z : R}, self.toSetoid w x → self.toSetoid y z → self.toSetoid (w + y) (x + z)

  Additive congruence relations are closed under addition

@[reducible]

abbrev RingCon.toAddCon {R : Type u_1} [Add R] [Mul R] (self : RingCon R) : AddCon R

The induced additive congruence from a RingCon.

Equations

• self.toAddCon = { toSetoid := self.toSetoid, add' := ⋯ }

inductive RingConGen.Rel {R : Type u_2} [Add R] [Mul R] (r : R → R → Prop) : R → R → Prop

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

• of: ∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] {r : R → R → Prop} (x y : R), r x y → RingConGen.Rel r x y
• refl: ∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] {r : R → R → Prop} (x : R), RingConGen.Rel r x x
• symm: ∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] {r : R → R → Prop} {x y : R}, RingConGen.Rel r x y → RingConGen.Rel r y x
• trans: ∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] {r : R → R → Prop} {x y z : R}, RingConGen.Rel r x y → RingConGen.Rel r y z → RingConGen.Rel r x z
• add: ∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] {r : R → R → Prop} {w x y z : R}, RingConGen.Rel r w x → RingConGen.Rel r y z → RingConGen.Rel r (w + y) (x + z)
• mul: ∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] {r : R → R → Prop} {w x y z : R}, RingConGen.Rel r w x → RingConGen.Rel r y z → RingConGen.Rel r (w * y) (x * z)

def ringConGen {R : Type u_2} [Add R] [Mul R] (r : R → R → Prop) : RingCon R

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

Equations

• ringConGen r = { r := RingConGen.Rel r, iseqv := ⋯, mul' := ⋯, add' := ⋯ }

instance RingCon.instFunLikeForallProp {R : Type u_2} [Add R] [Mul R] : FunLike (RingCon R) R (R → Prop)

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

Equations

• RingCon.instFunLikeForallProp = { coe := fun (c : RingCon R) => ⇑c.toSetoid, coe_injective' := ⋯ }

theorem RingCon.rel_eq_coe {R : Type u_2} [Add R] [Mul R] (c : RingCon R) : ⇑c.toSetoid = ⇑c

@[simp]

theorem RingCon.toCon_coe_eq_coe {R : Type u_2} [Add R] [Mul R] (c : RingCon R) : ⇑c.toCon = ⇑c

theorem RingCon.refl {R : Type u_2} [Add R] [Mul R] (c : RingCon R) (x : R) : c x x

theorem RingCon.symm {R : Type u_2} [Add R] [Mul R] (c : RingCon R) {x : R} {y : R} : c x y → c y x

theorem RingCon.trans {R : Type u_2} [Add R] [Mul R] (c : RingCon R) {x : R} {y : R} {z : R} : c x y → c y z → c x z

theorem RingCon.add {R : Type u_2} [Add R] [Mul R] (c : RingCon R) {w : R} {x : R} {y : R} {z : R} : c w x → c y z → c (w + y) (x + z)

theorem RingCon.mul {R : Type u_2} [Add R] [Mul R] (c : RingCon R) {w : R} {x : R} {y : R} {z : R} : c w x → c y z → c (w * y) (x * z)

theorem RingCon.sub {S : Type u_3} [AddGroup S] [Mul S] (t : RingCon S) {a : S} {b : S} {c : S} {d : S} (h : t a b) (h' : t c d) : t (a - c) (b - d)

theorem RingCon.neg {S : Type u_3} [AddGroup S] [Mul S] (t : RingCon S) {a : S} {b : S} (h : t a b) : t (-a) (-b)

theorem RingCon.nsmul {S : Type u_3} [AddGroup S] [Mul S] (t : RingCon S) (m : ℕ) {x : S} {y : S} (hx : t x y) : t (m • x) (m • y)

theorem RingCon.zsmul {S : Type u_3} [AddGroup S] [Mul S] (t : RingCon S) (z : ℤ) {x : S} {y : S} (hx : t x y) : t (z • x) (z • y)

instance RingCon.instInhabited {R : Type u_2} [Add R] [Mul R] : Inhabited (RingCon R)

Equations

• RingCon.instInhabited = { default := ringConGen EmptyRelation }

@[simp]

theorem RingCon.rel_mk {R : Type u_2} [Add R] [Mul R] {s : Con R} {h : ∀ {w x y z : R}, s.toSetoid w x → s.toSetoid y z → s.toSetoid (w + y) (x + z)} {a : R} {b : R} : { toCon := s, add' := h } a b ↔ s a b

theorem RingCon.ext' {R : Type u_2} [Add R] [Mul R] {c : RingCon R} {d : RingCon R} (H : ⇑c = ⇑d) : c = d

The map sending a congruence relation to its underlying binary relation is injective.

theorem RingCon.ext {R : Type u_2} [Add R] [Mul R] {c : RingCon R} {d : RingCon R} (H : ∀ (x y : R), c x y ↔ d x y) : c = d

Extensionality rule for congruence relations.

def RingCon.comap {R : Type u_3} {R' : Type u_4} {F : Type u_5} [Add R] [Add R'] [FunLike F R R'] [AddHomClass F R R'] [Mul R] [Mul R'] [MulHomClass F R R'] (J : RingCon R') (f : F) : RingCon R

Pulling back a RingCon across a ring homomorphism.

Equations

• J.comap f = { toCon := Con.comap ⇑f ⋯ J.toCon, add' := ⋯ }

def RingCon.Quotient {R : Type u_2} [Add R] [Mul R] (c : RingCon R) : Type u_2

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

Equations

• c.Quotient = Quotient c.toSetoid

def RingCon.toQuotient {R : Type u_2} [Add R] [Mul R] {c : RingCon R} (r : R) : c.Quotient

The morphism into the quotient by a congruence relation

Equations

• ↑r = Quotient.mk'' r

instance RingCon.instCoeTCQuotient {R : Type u_2} [Add R] [Mul R] (c : RingCon R) : CoeTC 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

• c.instCoeTCQuotient = { coe := RingCon.toQuotient }

@[instance 500]

instance RingCon.instDecidableEqQuotientOfDecidableCoeForallProp {R : Type u_2} [Add R] [Mul R] (c : RingCon R) [_d : (a b : R) → Decidable (c a b)] : DecidableEq c.Quotient

The quotient by a decidable congruence relation has decidable equality.

Equations

• c.instDecidableEqQuotientOfDecidableCoeForallProp = inferInstanceAs (DecidableEq (Quotient c.toSetoid))

@[simp]

theorem RingCon.quot_mk_eq_coe {R : Type u_2} [Add R] [Mul R] (c : RingCon R) (x : R) : Quot.mk (⇑c) x = ↑x

@[simp]

theorem RingCon.eq {R : Type u_2} [Add R] [Mul R] (c : RingCon R) {a : R} {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

instance RingCon.instAddQuotient {R : Type u_2} [Add R] [Mul R] (c : RingCon R) : Add c.Quotient

Equations

• c.instAddQuotient = inferInstanceAs (Add c.toAddCon.Quotient)

@[simp]

theorem RingCon.coe_add {R : Type u_2} [Add R] [Mul R] (c : RingCon R) (x : R) (y : R) : ↑(x + y) = ↑x + ↑y

instance RingCon.instMulQuotient {R : Type u_2} [Add R] [Mul R] (c : RingCon R) : Mul c.Quotient

Equations

• c.instMulQuotient = inferInstanceAs (Mul c.Quotient)

@[simp]

theorem RingCon.coe_mul {R : Type u_2} [Add R] [Mul R] (c : RingCon R) (x : R) (y : R) : ↑(x * y) = ↑x * ↑y

instance RingCon.instZeroQuotient {R : Type u_2} [AddZeroClass R] [Mul R] (c : RingCon R) : Zero c.Quotient

Equations

• c.instZeroQuotient = inferInstanceAs (Zero c.toAddCon.Quotient)

@[simp]

theorem RingCon.coe_zero {R : Type u_2} [AddZeroClass R] [Mul R] (c : RingCon R) : ↑0 = 0

instance RingCon.instOneQuotient {R : Type u_2} [Add R] [MulOneClass R] (c : RingCon R) : One c.Quotient

Equations

• c.instOneQuotient = inferInstanceAs (One c.Quotient)

@[simp]

theorem RingCon.coe_one {R : Type u_2} [Add R] [MulOneClass R] (c : RingCon R) : ↑1 = 1

instance RingCon.instNegQuotient {R : Type u_2} [AddGroup R] [Mul R] (c : RingCon R) : Neg c.Quotient

Equations

• c.instNegQuotient = inferInstanceAs (Neg c.toAddCon.Quotient)

@[simp]

theorem RingCon.coe_neg {R : Type u_2} [AddGroup R] [Mul R] (c : RingCon R) (x : R) : ↑(-x) = -↑x

instance RingCon.instSubQuotient {R : Type u_2} [AddGroup R] [Mul R] (c : RingCon R) : Sub c.Quotient

Equations

• c.instSubQuotient = inferInstanceAs (Sub c.toAddCon.Quotient)

@[simp]

theorem RingCon.coe_sub {R : Type u_2} [AddGroup R] [Mul R] (c : RingCon R) (x : R) (y : R) : ↑(x - y) = ↑x - ↑y

instance RingCon.hasZSMul {R : Type u_2} [AddGroup R] [Mul R] (c : RingCon R) : SMul ℤ c.Quotient

Equations

• c.hasZSMul = inferInstanceAs (SMul ℤ c.toAddCon.Quotient)

@[simp]

theorem RingCon.coe_zsmul {R : Type u_2} [AddGroup R] [Mul R] (c : RingCon R) (z : ℤ) (x : R) : ↑(z • x) = z • ↑x

instance RingCon.hasNSMul {R : Type u_2} [AddMonoid R] [Mul R] (c : RingCon R) : SMul ℕ c.Quotient

Equations

• c.hasNSMul = inferInstanceAs (SMul ℕ c.toAddCon.Quotient)

@[simp]

theorem RingCon.coe_nsmul {R : Type u_2} [AddMonoid R] [Mul R] (c : RingCon R) (n : ℕ) (x : R) : ↑(n • x) = n • ↑x

instance RingCon.instPowQuotientNat {R : Type u_2} [Add R] [Monoid R] (c : RingCon R) : Pow c.Quotient ℕ

Equations

• c.instPowQuotientNat = inferInstanceAs (Pow c.Quotient ℕ)

@[simp]

theorem RingCon.coe_pow {R : Type u_2} [Add R] [Monoid R] (c : RingCon R) (x : R) (n : ℕ) : ↑(x ^ n) = ↑x ^ n

instance RingCon.instNatCastQuotient {R : Type u_2} [AddMonoidWithOne R] [Mul R] (c : RingCon R) : NatCast c.Quotient

Equations

• c.instNatCastQuotient = { natCast := fun (n : ℕ) => ↑↑n }

@[simp]

theorem RingCon.coe_natCast {R : Type u_2} [AddMonoidWithOne R] [Mul R] (c : RingCon R) (n : ℕ) : ↑↑n = ↑n

@[deprecated RingCon.coe_natCast]

theorem RingCon.coe_nat_cast {R : Type u_2} [AddMonoidWithOne R] [Mul R] (c : RingCon R) (n : ℕ) : ↑↑n = ↑n

Alias of RingCon.coe_natCast.

instance RingCon.instIntCastQuotient {R : Type u_2} [AddGroupWithOne R] [Mul R] (c : RingCon R) : IntCast c.Quotient

Equations

• c.instIntCastQuotient = { intCast := fun (z : ℤ) => ↑↑z }

@[simp]

theorem RingCon.coe_intCast {R : Type u_2} [AddGroupWithOne R] [Mul R] (c : RingCon R) (n : ℕ) : ↑↑n = ↑n

@[deprecated RingCon.coe_intCast]

theorem RingCon.coe_int_cast {R : Type u_2} [AddGroupWithOne R] [Mul R] (c : RingCon R) (n : ℕ) : ↑↑n = ↑n

Alias of RingCon.coe_intCast.

instance RingCon.instInhabitedQuotient {R : Type u_2} [Inhabited R] [Add R] [Mul R] (c : RingCon R) : Inhabited c.Quotient

Equations

• c.instInhabitedQuotient = { default := ↑default }

Algebraic structure

The operations above on the quotient by c : RingCon R preserve the algebraic structure of R.

instance RingCon.instNonUnitalNonAssocSemiringQuotient {R : Type u_2} [NonUnitalNonAssocSemiring R] (c : RingCon R) : NonUnitalNonAssocSemiring c.Quotient

Equations

• c.instNonUnitalNonAssocSemiringQuotient = Function.Surjective.nonUnitalNonAssocSemiring Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯

instance RingCon.instNonAssocSemiringQuotient {R : Type u_2} [NonAssocSemiring R] (c : RingCon R) : NonAssocSemiring c.Quotient

Equations

• c.instNonAssocSemiringQuotient = Function.Surjective.nonAssocSemiring Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance RingCon.instNonUnitalSemiringQuotient {R : Type u_2} [NonUnitalSemiring R] (c : RingCon R) : NonUnitalSemiring c.Quotient

Equations

• c.instNonUnitalSemiringQuotient = Function.Surjective.nonUnitalSemiring Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯

instance RingCon.instSemiringQuotient {R : Type u_2} [Semiring R] (c : RingCon R) : Semiring c.Quotient

Equations

• c.instSemiringQuotient = Function.Surjective.semiring Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance RingCon.instCommSemiringQuotient {R : Type u_2} [CommSemiring R] (c : RingCon R) : CommSemiring c.Quotient

Equations

• c.instCommSemiringQuotient = Function.Surjective.commSemiring Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance RingCon.instNonUnitalNonAssocRingQuotient {R : Type u_2} [NonUnitalNonAssocRing R] (c : RingCon R) : NonUnitalNonAssocRing c.Quotient

Equations

• c.instNonUnitalNonAssocRingQuotient = Function.Surjective.nonUnitalNonAssocRing Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance RingCon.instNonAssocRingQuotient {R : Type u_2} [NonAssocRing R] (c : RingCon R) : NonAssocRing c.Quotient

Equations

• c.instNonAssocRingQuotient = Function.Surjective.nonAssocRing Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance RingCon.instNonUnitalRingQuotient {R : Type u_2} [NonUnitalRing R] (c : RingCon R) : NonUnitalRing c.Quotient

Equations

• c.instNonUnitalRingQuotient = Function.Surjective.nonUnitalRing Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance RingCon.instRingQuotient {R : Type u_2} [Ring R] (c : RingCon R) : Ring c.Quotient

Equations

• c.instRingQuotient = Function.Surjective.ring Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance RingCon.instCommRingQuotient {R : Type u_2} [CommRing R] (c : RingCon R) : CommRing c.Quotient

Equations

• c.instCommRingQuotient = Function.Surjective.commRing Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def RingCon.mk' {R : Type u_2} [NonAssocSemiring R] (c : RingCon R) : R →+* c.Quotient

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

Equations

• c.mk' = { toFun := RingCon.toQuotient, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }