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
andAddCon
inGroupTheory/Congruence.lean
, such as:- The
CompleteLattice
structure. - The
conGen_eq
lemma, stating thatringConGen r = infₛ {s : RingCon M | ∀ x y, r x y → s x y}∀ x y, r x y → s x y}→ s x y}
.
- The
Ring congruence relations are closed under addition
Ring congruence relations are closed under multiplication
A congruence relation on a type with an addition and multiplication is an equivalence relation which preserves both.
Instances For
- 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.
Instances For
A coercion from a congruence relation to its underlying binary relation.
Equations
- RingCon.instInhabitedRingCon = { default := ringConGen EmptyRelation }
The morphism into the quotient by a congruence relation
Equations
- ↑r = Quotient.mk'' r
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 }
The quotient by a decidable congruence relation has decidable equality.
Equations
- RingCon.instDecidableEqQuotient c = id inferInstance
Basic notation #
The basic algebraic notation, 0
, 1
, +
, *
, -
, ^
, descend naturally under the quotient
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
- RingCon.instNatCastQuotientToAddToAddZeroClassToAddMonoid c = { natCast := fun n => ↑↑n }
Equations
- RingCon.instIntCastQuotientToAddToAddZeroClassToAddMonoidToAddMonoidWithOne c = { intCast := fun z => ↑↑z }
Equations
- RingCon.instInhabitedQuotient c = { default := ↑default }
Algebraic structure #
The operations above on the quotient by c : RingCon R
preseverse the algebraic structure of R
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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.