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
.
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
Additive congruence relations are closed under addition
Instances For
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)
Instances For
The inductively defined smallest ring congruence relation containing a given binary relation.
Equations
- ringConGen r = { r := RingConGen.Rel r, iseqv := ⋯, mul' := ⋯, add' := ⋯ }
Instances For
Equations
- RingCon.instInhabited = { default := ringConGen EmptyRelation }
Pulling back a RingCon
across a ring homomorphism.
Instances For
The quotient by a decidable congruence relation has decidable equality.
Equations
- c.instDecidableEqQuotientOfDecidableCoeForallProp = inferInstanceAs (DecidableEq (Quotient c.toSetoid))
Basic notation #
The basic algebraic notation, 0
, 1
, +
, *
, -
, ^
, descend naturally under the quotient
Equations
- c.instAddQuotient = inferInstanceAs (Add c.toAddCon.Quotient)
Equations
- c.instMulQuotient = inferInstanceAs (Mul c.Quotient)
Equations
- c.instZeroQuotient = inferInstanceAs (Zero c.toAddCon.Quotient)
Equations
- c.instOneQuotient = inferInstanceAs (One c.Quotient)
Equations
- c.instSMulQuotient = inferInstanceAs (SMul α c.Quotient)
Equations
- c.instNegQuotient = inferInstanceAs (Neg c.toAddCon.Quotient)
Equations
- c.instSubQuotient = inferInstanceAs (Sub c.toAddCon.Quotient)
Alias of RingCon.coe_natCast
.
Alias of RingCon.coe_intCast
.
Algebraic structure #
The operations above on the quotient by c : RingCon R
preserve the algebraic structure of R
.
Equations
- c.instNonUnitalNonAssocSemiringQuotient = Function.Surjective.nonUnitalNonAssocSemiring Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- c.instNonAssocSemiringQuotient = Function.Surjective.nonAssocSemiring Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- c.instNonUnitalSemiringQuotient = Function.Surjective.nonUnitalSemiring Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- c.instSemiringQuotient = Function.Surjective.semiring Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- c.instCommSemiringQuotient = Function.Surjective.commSemiring Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- c.instNonUnitalNonAssocRingQuotient = Function.Surjective.nonUnitalNonAssocRing Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- c.instNonAssocRingQuotient = Function.Surjective.nonAssocRing Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- c.instNonUnitalRingQuotient = Function.Surjective.nonUnitalRing Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- c.instRingQuotient = Function.Surjective.ring Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- c.instCommRingQuotient = Function.Surjective.commRing Quotient.mk'' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- c.instDistribMulActionQuotientOfIsScalarTower = DistribMulAction.mk ⋯ ⋯
Equations
- c.instMulSemiringActionQuotientOfIsScalarTower = MulSemiringAction.mk ⋯ ⋯
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' := ⋯ }
Instances For
Lattice structure #
The API in this section is copied from Mathlib/GroupTheory/Congruence.lean
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
.
The infimum of a set of congruence relations on a given type with multiplication and addition.
Equations
- RingCon.instPartialOrder = PartialOrder.mk ⋯
The complete lattice of congruence relations on a given type with multiplication and addition.
Equations
- RingCon.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- ⋯ = ⋯
The inductively defined smallest congruence relation containing a binary relation r
equals
the infimum of the set of congruence relations containing r
.
The smallest congruence relation containing a binary relation r
is contained in any
congruence relation containing r
.
Given binary relations r, s
with r
contained in s
, the smallest congruence relation
containing s
contains the smallest congruence relation containing r
.
Congruence relations equal the smallest congruence relation in which they are contained.
The map sending a binary relation to the smallest congruence relation in which it is contained is idempotent.
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
'.
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.
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 := ⋯ }