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, such as:
  • The CompleteLattice structure.
  • The conGen_eq lemma, stating that ringConGen r = infₛ {s : RingCon M | ∀ x y, r x y → s x y}∀ x y, r x y → s x y}→ s x y}.

ink

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

• Ring congruence relations are closed under addition

  add' : ∀ {w x y z : R}, Setoid.r w x → Setoid.r y z → Setoid.r (w + y) (x + z)

• Ring congruence relations are closed under multiplication

  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.

ink

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

• of: ∀ {R : Type u_1} [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_1} [inst : Add R] [inst_1 : Mul R] {r : R → R → Prop} (x : R), RingConGen.Rel r x x
• symm: ∀ {R : Type u_1} [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_1} [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_1} [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_1} [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)

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

ink

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

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

Equations

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

ink

def RingCon.toAddCon {R : Type u_1} [inst : Add R] [inst : Mul R] (c : RingCon R) : AddCon R

Every ring_con is also an AddCon

Equations

• RingCon.toAddCon c = { toSetoid := c.toSetoid, add' := (_ : ∀ {w x y z : R}, Setoid.r w x → Setoid.r y z → Setoid.r (w + y) (x + z)) }

ink

def RingCon.toCon {R : Type u_1} [inst : Add R] [inst : Mul R] (c : RingCon R) : Con R

Every RingCon is also a Con

Equations

• RingCon.toCon c = { toSetoid := c.toSetoid, mul' := (_ : ∀ {w x y z : R}, Setoid.r w x → Setoid.r y z → Setoid.r (w * y) (x * z)) }

ink

instance RingCon.instFunLikeRingConForAllProp {R : Type u_1} [inst : Add R] [inst : Mul R] : FunLike (RingCon R) R fun x => R → Prop

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

Equations

• RingCon.instFunLikeRingConForAllProp = { coe := fun c => Setoid.r, coe_injective' := (_ : ∀ (x y : RingCon R), (fun c => Setoid.r) x = (fun c => Setoid.r) y → x = y) }

ink

@[simp]

theorem RingCon.rel_eq_coe {R : Type u_1} [inst : Add R] [inst : Mul R] (c : RingCon R) : Setoid.r = ↑c

ink

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

theorem RingCon.rel_mk {R : Type u_1} [inst : Add R] [inst : 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 : R} {b : R} : ↑{ toSetoid := s, add' := ha, mul' := hm } a b ↔ Setoid.r a b

ink

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

Equations

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

ink

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

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

Equations

• RingCon.Quotient c = Quotient c.toSetoid

ink

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

The morphism into the quotient by a congruence relation

Equations

• ↑r = Quotient.mk'' r

ink

instance RingCon.instCoeTCQuotient {R : Type u_1} [inst : Add R] [inst : 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 }

ink

instance RingCon.instDecidableEqQuotient {R : Type u_1} [inst : Add R] [inst : 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 = id inferInstance

ink

@[simp]

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

ink

@[simp]

theorem RingCon.eq {R : Type u_1} [inst : Add R] [inst : 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

ink

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

Equations

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

ink

@[simp]

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

ink

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

Equations

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

ink

@[simp]

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

ink

instance RingCon.instZeroQuotientToAdd {R : Type u_1} [inst : AddZeroClass R] [inst : Mul R] (c : RingCon R) : Zero (RingCon.Quotient c)

Equations

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

ink

@[simp]

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

ink

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

Equations

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

ink

@[simp]

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

ink

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

Equations

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

ink

@[simp]

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

ink

instance RingCon.instNegQuotientToAddToAddZeroClassToAddMonoidToSubNegMonoid {R : Type u_1} [inst : AddGroup R] [inst : Mul R] (c : RingCon R) : Neg (RingCon.Quotient c)

Equations

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

ink

@[simp]

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

ink

instance RingCon.instSubQuotientToAddToAddZeroClassToAddMonoidToSubNegMonoid {R : Type u_1} [inst : AddGroup R] [inst : Mul R] (c : RingCon R) : Sub (RingCon.Quotient c)

Equations

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

ink

@[simp]

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

ink

instance RingCon.hasZsmul {R : Type u_1} [inst : AddGroup R] [inst : Mul R] (c : RingCon R) : SMul ℤ (RingCon.Quotient c)

Equations

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

ink

@[simp]

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

ink

instance RingCon.hasNsmul {R : Type u_1} [inst : AddMonoid R] [inst : Mul R] (c : RingCon R) : SMul ℕ (RingCon.Quotient c)

Equations

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

ink

@[simp]

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

ink

instance RingCon.instPowQuotientToMulToMulOneClassNat {R : Type u_1} [inst : Add R] [inst : Monoid R] (c : RingCon R) : Pow (RingCon.Quotient c) ℕ

Equations

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

ink

@[simp]

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

ink

instance RingCon.instNatCastQuotientToAddToAddZeroClassToAddMonoid {R : Type u_1} [inst : AddMonoidWithOne R] [inst : Mul R] (c : RingCon R) : NatCast (RingCon.Quotient c)

Equations

• RingCon.instNatCastQuotientToAddToAddZeroClassToAddMonoid c = { natCast := fun n => ↑↑n }

ink

@[simp]

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

ink

instance RingCon.instIntCastQuotientToAddToAddZeroClassToAddMonoidToAddMonoidWithOne {R : Type u_1} [inst : AddGroupWithOne R] [inst : Mul R] (c : RingCon R) : IntCast (RingCon.Quotient c)

Equations

• RingCon.instIntCastQuotientToAddToAddZeroClassToAddMonoidToAddMonoidWithOne c = { intCast := fun z => ↑↑z }

ink

@[simp]

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

ink

instance RingCon.instInhabitedQuotient {R : Type u_1} [inst : Inhabited R] [inst : Add R] [inst : 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 preseverse the algebraic structure of R.

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

instance RingCon.instCommRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToMul {R : Type u_1} [inst : CommRing R] (c : RingCon R) : CommRing (RingCon.Quotient c)

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

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

Equations

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