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 Setoid.r
• mul' : ∀ {w x y z : R}, Setoid.r w x → Setoid.r y z → Setoid.r (w * y) (x * z)
• add' : ∀ {w x y z : R}, Setoid.r w x → Setoid.r y z → Setoid.r (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

• RingCon.toAddCon self = { 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 = { toCon := { toSetoid := { r := RingConGen.Rel r, iseqv := ⋯ }, mul' := ⋯ }, add' := ⋯ }

instance RingCon.instFunLikeRingConForAllProp {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.instFunLikeRingConForAllProp = { coe := fun (c : RingCon R) => Setoid.r, coe_injective' := ⋯ }

theorem RingCon.rel_eq_coe {R : Type u_2} [Add R] [Mul R] (c : RingCon R) : Setoid.r = ⇑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)

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

Equations

• RingCon.instInhabitedRingCon = { 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}, Setoid.r w x → Setoid.r y z → Setoid.r (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.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

• RingCon.Quotient c = Quotient c.toSetoid

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

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 (RingCon.Quotient c)

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

See Note [use has_coe_t].

Equations

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

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

The quotient by a decidable congruence relation has decidable equality.

Equations

• RingCon.instDecidableEqQuotient c = 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 (RingCon.Quotient c)

Equations

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

@[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 (RingCon.Quotient c)

Equations

• RingCon.instMulQuotient c = inferInstanceAs (Mul (Con.Quotient c.toCon))

@[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.instZeroQuotientToAdd {R : Type u_2} [AddZeroClass R] [Mul R] (c : RingCon R) : Zero (RingCon.Quotient c)

Equations

• RingCon.instZeroQuotientToAdd c = inferInstanceAs (Zero (AddCon.Quotient (RingCon.toAddCon c)))

@[simp]

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

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

Equations

• RingCon.instOneQuotientToMul c = inferInstanceAs (One (Con.Quotient c.toCon))

@[simp]

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

instance RingCon.instSMulQuotientToMul {α : Type u_1} {R : Type u_2} [Add R] [MulOneClass R] [SMul α R] [IsScalarTower α R R] (c : RingCon R) : SMul α (RingCon.Quotient c)

Equations

• RingCon.instSMulQuotientToMul c = inferInstanceAs (SMul α (Con.Quotient c.toCon))

@[simp]

theorem RingCon.coe_smul {α : Type u_1} {R : Type u_2} [Add R] [MulOneClass R] [SMul α R] [IsScalarTower α R R] (c : RingCon R) (a : α) (x : R) : ↑(a • x) = a • ↑x

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

Equations

• RingCon.instNegQuotientToAddToAddSemigroupToAddMonoidToSubNegMonoid c = inferInstanceAs (Neg (AddCon.Quotient (RingCon.toAddCon c)))

@[simp]

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

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

Equations

• RingCon.instSubQuotientToAddToAddSemigroupToAddMonoidToSubNegMonoid c = inferInstanceAs (Sub (AddCon.Quotient (RingCon.toAddCon c)))

@[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 ℤ (RingCon.Quotient c)

Equations

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

@[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 ℕ (RingCon.Quotient c)

Equations

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

@[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.instPowQuotientToMulToMulOneClassNat {R : Type u_2} [Add R] [Monoid R] (c : RingCon R) : Pow (RingCon.Quotient c) ℕ

Equations

• RingCon.instPowQuotientToMulToMulOneClassNat c = inferInstanceAs (Pow (Con.Quotient c.toCon) ℕ)

@[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.instNatCastQuotientToAddToAddSemigroupToAddMonoid {R : Type u_2} [AddMonoidWithOne R] [Mul R] (c : RingCon R) : NatCast (RingCon.Quotient c)

Equations

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

@[simp]

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

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

Equations

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

@[simp]

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

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

Equations

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

Algebraic structure

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

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

Equations

• RingCon.instNonUnitalNonAssocSemiringQuotientToAddToDistribToMul c = Function.Surjective.nonUnitalNonAssocSemiring Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• RingCon.instNonAssocSemiringQuotientToAddToDistribToNonUnitalNonAssocSemiringToMul c = Function.Surjective.nonAssocSemiring Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• RingCon.instNonUnitalSemiringQuotientToAddToDistribToNonUnitalNonAssocSemiringToMul c = Function.Surjective.nonUnitalSemiring Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• RingCon.instSemiringQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonAssocSemiringToMul c = Function.Surjective.semiring Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• RingCon.instCommSemiringQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonAssocSemiringToSemiringToMul c = Function.Surjective.commSemiring Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• RingCon.instNonUnitalNonAssocRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToMul c = Function.Surjective.nonUnitalNonAssocRing Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• RingCon.instNonAssocRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToMul c = Function.Surjective.nonAssocRing Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• RingCon.instNonUnitalRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToMul c = Function.Surjective.nonUnitalRing Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• RingCon.instRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToMul c = Function.Surjective.ring Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

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

instance RingCon.isScalarTower_right {α : Type u_1} {R : Type u_2} [Add R] [MulOneClass R] [SMul α R] [IsScalarTower α R R] (c : RingCon R) : IsScalarTower α (RingCon.Quotient c) (RingCon.Quotient c)

Equations

• ⋯ = ⋯

instance RingCon.smulCommClass {α : Type u_1} {R : Type u_2} [Add R] [MulOneClass R] [SMul α R] [IsScalarTower α R R] [SMulCommClass α R R] (c : RingCon R) : SMulCommClass α (RingCon.Quotient c) (RingCon.Quotient c)

Equations

• ⋯ = ⋯

instance RingCon.smulCommClass' {α : Type u_1} {R : Type u_2} [Add R] [MulOneClass R] [SMul α R] [IsScalarTower α R R] [SMulCommClass R α R] (c : RingCon R) : SMulCommClass (RingCon.Quotient c) α (RingCon.Quotient c)

Equations

• ⋯ = ⋯

instance RingCon.instDistribMulActionQuotientToAddToDistribToNonUnitalNonAssocSemiringToMulToAddMonoidToAddMonoidWithOneToAddCommMonoidWithOneInstNonAssocSemiringQuotientToAddToDistribToNonUnitalNonAssocSemiringToMul {α : Type u_1} {R : Type u_2} [Monoid α] [NonAssocSemiring R] [DistribMulAction α R] [IsScalarTower α R R] (c : RingCon R) : DistribMulAction α (RingCon.Quotient c)

Equations

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

instance RingCon.instMulSemiringActionQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonAssocSemiringToMulInstSemiringQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonAssocSemiringToMul {α : Type u_1} {R : Type u_2} [Monoid α] [Semiring R] [MulSemiringAction α R] [IsScalarTower α R R] (c : RingCon R) : MulSemiringAction α (RingCon.Quotient c)

Equations

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

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

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

Equations

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

Lattice structure

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

instance RingCon.instLERingCon {R : Type u_2} [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.instLERingCon = { le := fun (c d : RingCon R) => ∀ ⦃x y : R⦄, c x y → d x y }

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

Definition of ≤ for congruence relations.

instance RingCon.instInfSetRingCon {R : Type u_2} [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.instInfSetRingCon = { sInf := fun (S : Set (RingCon R)) => { toCon := { toSetoid := { r := fun (x y : R) => ∀ c ∈ S, c x y, iseqv := ⋯ }, mul' := ⋯ }, add' := ⋯ } }

theorem RingCon.sInf_toSetoid {R : Type u_2} [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.

@[simp]

theorem RingCon.coe_sInf {R : Type u_2} [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.

@[simp]

theorem RingCon.coe_iInf {R : Type u_2} [Add R] [Mul R] {ι : Sort u_3} (f : ι → RingCon R) : ⇑(iInf f) = ⨅ (i : ι), ⇑(f i)

instance RingCon.instPartialOrderRingCon {R : Type u_2} [Add R] [Mul R] : PartialOrder (RingCon R)

Equations

• RingCon.instPartialOrderRingCon = PartialOrder.mk ⋯

instance RingCon.instCompleteLatticeRingCon {R : Type u_2} [Add R] [Mul R] : CompleteLattice (RingCon R)

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

Equations

• RingCon.instCompleteLatticeRingCon = let __spread.0 := completeLatticeOfInf (RingCon R) ⋯; CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem RingCon.coe_top {R : Type u_2} [Add R] [Mul R] : ⇑⊤ = ⊤

@[simp]

theorem RingCon.coe_inf {R : Type u_2} [Add R] [Mul R] {c : RingCon R} {d : RingCon R} : ⇑(c ⊓ d) = ⇑c ⊓ ⇑d

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

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

Definition of the infimum of two congruence relations.

theorem RingCon.ringConGen_eq {R : Type u_2} [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.

theorem RingCon.ringConGen_le {R : Type u_2} [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.

theorem RingCon.ringConGen_mono {R : Type u_2} [Add R] [Mul R] {r : R → R → Prop} {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.

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

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

theorem RingCon.ringConGen_idem {R : Type u_2} [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.

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

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

theorem RingCon.sSup_eq_ringConGen {R : Type u_2} [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'.

theorem RingCon.sSup_def {R : Type u_2} [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.

def RingCon.gi (R : Type u_2) [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 := ⋯ }