Quotients of non-commutative rings #
Unfortunately, ideals have only been developed in the commutative case as Ideal,
and it's not immediately clear how one should formalise ideals in the non-commutative case.
In this file, we directly define the quotient of a semiring by any relation, by building a bigger relation that represents the ideal generated by that relation.
We prove the universal properties of the quotient, and recommend avoiding relying on the actual definition, which is made irreducible for this purpose.
Since everything runs in parallel for quotients of R-algebras, we do that case at the same time.
instance
RingCon.instAlgebraQuotient
{S : Type uS}
[CommSemiring S]
{A : Type uA}
[Semiring A]
[Algebra S A]
(c : RingCon A)
:
Algebra S c.Quotient
Equations
- c.instAlgebraQuotient = Algebra.mk (c.mk'.comp (algebraMap S A)) ⋯ ⋯
@[simp]
theorem
RingCon.coe_algebraMap
{S : Type uS}
[CommSemiring S]
{A : Type uA}
[Semiring A]
[Algebra S A]
(c : RingCon A)
(s : S)
:
↑((algebraMap S A) s) = (algebraMap S c.Quotient) s
Given an arbitrary relation r on a ring, we strengthen it to a relation Rel r,
such that the equivalence relation generated by Rel r has x ~ y if and only if
x - y is in the ideal generated by elements a - b such that r a b.
- of: ∀ {R : Type uR} [inst : Semiring R] {r : R → R → Prop} ⦃x y : R⦄, r x y → RingQuot.Rel r x y
- add_left: ∀ {R : Type uR} [inst : Semiring R] {r : R → R → Prop} ⦃a b c : R⦄, RingQuot.Rel r a b → RingQuot.Rel r (a + c) (b + c)
- mul_left: ∀ {R : Type uR} [inst : Semiring R] {r : R → R → Prop} ⦃a b c : R⦄, RingQuot.Rel r a b → RingQuot.Rel r (a * c) (b * c)
- mul_right: ∀ {R : Type uR} [inst : Semiring R] {r : R → R → Prop} ⦃a b c : R⦄, RingQuot.Rel r b c → RingQuot.Rel r (a * b) (a * c)
Instances For
theorem
RingQuot.Rel.add_right
{R : Type uR}
[Semiring R]
{r : R → R → Prop}
⦃a : R⦄
⦃b : R⦄
⦃c : R⦄
(h : RingQuot.Rel r b c)
:
RingQuot.Rel r (a + b) (a + c)
theorem
RingQuot.Rel.neg
{R : Type uR}
[Ring R]
{r : R → R → Prop}
⦃a : R⦄
⦃b : R⦄
(h : RingQuot.Rel r a b)
:
RingQuot.Rel r (-a) (-b)
theorem
RingQuot.Rel.sub_left
{R : Type uR}
[Ring R]
{r : R → R → Prop}
⦃a : R⦄
⦃b : R⦄
⦃c : R⦄
(h : RingQuot.Rel r a b)
:
RingQuot.Rel r (a - c) (b - c)
theorem
RingQuot.Rel.sub_right
{R : Type uR}
[Ring R]
{r : R → R → Prop}
⦃a : R⦄
⦃b : R⦄
⦃c : R⦄
(h : RingQuot.Rel r b c)
:
RingQuot.Rel r (a - b) (a - c)
theorem
RingQuot.Rel.smul
{S : Type uS}
[CommSemiring S]
{A : Type uA}
[Semiring A]
[Algebra S A]
{r : A → A → Prop}
(k : S)
⦃a : A⦄
⦃b : A⦄
(h : RingQuot.Rel r a b)
:
RingQuot.Rel r (k • a) (k • b)
EqvGen (RingQuot.Rel r) is a ring congruence.
Equations
- RingQuot.ringCon r = { r := EqvGen (RingQuot.Rel r), iseqv := ⋯, mul' := ⋯, add' := ⋯ }
Instances For
theorem
RingQuot.eqvGen_rel_eq
{R : Type uR}
[Semiring R]
(r : R → R → Prop)
:
EqvGen (RingQuot.Rel r) = RingConGen.Rel r
Equations
- RingQuot.instNatCast r = { natCast := RingQuot.natCast r }
Equations
- RingQuot.instZero r = { zero := RingQuot.zero r }
Equations
- RingQuot.instOne r = { one := RingQuot.one r }
Equations
- RingQuot.instAdd r = { add := RingQuot.add r }
Equations
- RingQuot.instMul r = { mul := RingQuot.mul r }
Equations
- RingQuot.instNatPow r = { pow := fun (x : RingQuot r) (n : ℕ) => RingQuot.npow r n x }
Equations
- RingQuot.instNeg r = { neg := RingQuot.neg r }
Equations
- RingQuot.instSub r = { sub := RingQuot.sub r }
instance
RingQuot.instSMulOfAlgebra
{R : Type uR}
[Semiring R]
{S : Type uS}
[CommSemiring S]
(r : R → R → Prop)
[Algebra S R]
:
Equations
- RingQuot.instSMulOfAlgebra r = { smul := RingQuot.smul r }
theorem
RingQuot.zero_quot
{R : Type uR}
[Semiring R]
(r : R → R → Prop)
:
{ toQuot := Quot.mk (RingQuot.Rel r) 0 } = 0
theorem
RingQuot.one_quot
{R : Type uR}
[Semiring R]
(r : R → R → Prop)
:
{ toQuot := Quot.mk (RingQuot.Rel r) 1 } = 1
theorem
RingQuot.add_quot
{R : Type uR}
[Semiring R]
(r : R → R → Prop)
{a : R}
{b : R}
:
{ toQuot := Quot.mk (RingQuot.Rel r) a } + { toQuot := Quot.mk (RingQuot.Rel r) b } = { toQuot := Quot.mk (RingQuot.Rel r) (a + b) }
theorem
RingQuot.mul_quot
{R : Type uR}
[Semiring R]
(r : R → R → Prop)
{a : R}
{b : R}
:
{ toQuot := Quot.mk (RingQuot.Rel r) a } * { toQuot := Quot.mk (RingQuot.Rel r) b } = { toQuot := Quot.mk (RingQuot.Rel r) (a * b) }
theorem
RingQuot.pow_quot
{R : Type uR}
[Semiring R]
(r : R → R → Prop)
{a : R}
{n : ℕ}
:
{ toQuot := Quot.mk (RingQuot.Rel r) a } ^ n = { toQuot := Quot.mk (RingQuot.Rel r) (a ^ n) }
theorem
RingQuot.neg_quot
{R : Type uR}
[Ring R]
(r : R → R → Prop)
{a : R}
:
-{ toQuot := Quot.mk (RingQuot.Rel r) a } = { toQuot := Quot.mk (RingQuot.Rel r) (-a) }
theorem
RingQuot.sub_quot
{R : Type uR}
[Ring R]
(r : R → R → Prop)
{a : R}
{b : R}
:
{ toQuot := Quot.mk (RingQuot.Rel r) a } - { toQuot := Quot.mk (RingQuot.Rel r) b } = { toQuot := Quot.mk (RingQuot.Rel r) (a - b) }
theorem
RingQuot.smul_quot
{R : Type uR}
[Semiring R]
{S : Type uS}
[CommSemiring S]
(r : R → R → Prop)
[Algebra S R]
{n : S}
{a : R}
:
n • { toQuot := Quot.mk (RingQuot.Rel r) a } = { toQuot := Quot.mk (RingQuot.Rel r) (n • a) }
instance
RingQuot.instIsScalarTower
{R : Type uR}
[Semiring R]
{S : Type uS}
[CommSemiring S]
{T : Type uT}
(r : R → R → Prop)
[CommSemiring T]
[SMul S T]
[Algebra S R]
[Algebra T R]
[IsScalarTower S T R]
:
IsScalarTower S T (RingQuot r)
Equations
- ⋯ = ⋯
instance
RingQuot.instSMulCommClass
{R : Type uR}
[Semiring R]
{S : Type uS}
[CommSemiring S]
{T : Type uT}
(r : R → R → Prop)
[CommSemiring T]
[Algebra S R]
[Algebra T R]
[SMulCommClass S T R]
:
SMulCommClass S T (RingQuot r)
Equations
- ⋯ = ⋯
Equations
Equations
Equations
- RingQuot.instSemiring r = let __spread.0 := RingQuot.instAddCommMonoid r; let __spread.1 := RingQuot.instMonoidWithZero r; Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯
Equations
- RingQuot.instRing r = let __src := RingQuot.instSemiring r; Ring.mk ⋯ (fun (x : ℤ) (x_1 : RingQuot r) => x • x_1) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
instance
RingQuot.instCommSemiring
{R : Type uR}
[CommSemiring R]
(r : R → R → Prop)
:
CommSemiring (RingQuot r)
Equations
- RingQuot.instCommSemiring r = let __src := RingQuot.instSemiring r; CommSemiring.mk ⋯
Equations
- RingQuot.instCommRing r = let __src := RingQuot.instCommSemiring r; let __src_1 := RingQuot.instRing r; CommRing.mk ⋯
Equations
- RingQuot.instInhabited r = { default := 0 }
instance
RingQuot.instAlgebra
{R : Type uR}
[Semiring R]
{S : Type uS}
[CommSemiring S]
[Algebra S R]
(r : R → R → Prop)
:
Equations
- One or more equations did not get rendered due to their size.
@[irreducible]
The quotient map from a ring to its quotient, as a homomorphism of rings.
Equations
Instances For
theorem
RingQuot.mkRingHom_def
{R : Type u_1}
[Semiring R]
(r : R → R → Prop)
:
RingQuot.mkRingHom r = { toFun := fun (x : R) => { toQuot := Quot.mk (RingQuot.Rel r) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
map_add' := ⋯ }
theorem
RingQuot.mkRingHom_rel
{R : Type uR}
[Semiring R]
{r : R → R → Prop}
{x : R}
{y : R}
(w : r x y)
:
(RingQuot.mkRingHom r) x = (RingQuot.mkRingHom r) y
theorem
RingQuot.ringQuot_ext
{R : Type uR}
[Semiring R]
{T : Type uT}
[Semiring T]
{r : R → R → Prop}
(f : RingQuot r →+* T)
(g : RingQuot r →+* T)
(w : f.comp (RingQuot.mkRingHom r) = g.comp (RingQuot.mkRingHom r))
:
f = g
theorem
RingQuot.lift_def
{R : Type u_1}
[Semiring R]
{T : Type u_2}
[Semiring T]
{r : R → R → Prop}
:
RingQuot.lift = { toFun := fun (f : { f : R →+* T // ∀ ⦃x y : R⦄, r x y → f x = f y }) => RingQuot.preLift ⋯,
invFun := fun (F : RingQuot r →+* T) => ⟨F.comp (RingQuot.mkRingHom r), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
We now verify that in the case of a commutative ring, the RingQuot construction
agrees with the quotient by the appropriate ideal.
def
RingQuot.ringQuotToIdealQuotient
{B : Type uR}
[CommRing B]
(r : B → B → Prop)
:
RingQuot r →+* B ⧸ Ideal.ofRel r
The universal ring homomorphism from RingQuot r to B ⧸ Ideal.ofRel r.
Equations
- RingQuot.ringQuotToIdealQuotient r = RingQuot.lift ⟨Ideal.Quotient.mk (Ideal.ofRel r), ⋯⟩
Instances For
@[simp]
theorem
RingQuot.ringQuotToIdealQuotient_apply
{B : Type uR}
[CommRing B]
(r : B → B → Prop)
(x : B)
:
(RingQuot.ringQuotToIdealQuotient r) ((RingQuot.mkRingHom r) x) = (Ideal.Quotient.mk (Ideal.ofRel r)) x
def
RingQuot.idealQuotientToRingQuot
{B : Type uR}
[CommRing B]
(r : B → B → Prop)
:
B ⧸ Ideal.ofRel r →+* RingQuot r
The universal ring homomorphism from B ⧸ Ideal.ofRel r to RingQuot r.
Equations
Instances For
@[simp]
theorem
RingQuot.idealQuotientToRingQuot_apply
{B : Type uR}
[CommRing B]
(r : B → B → Prop)
(x : B)
:
(RingQuot.idealQuotientToRingQuot r) ((Ideal.Quotient.mk (Ideal.ofRel r)) x) = (RingQuot.mkRingHom r) x
def
RingQuot.ringQuotEquivIdealQuotient
{B : Type uR}
[CommRing B]
(r : B → B → Prop)
:
RingQuot r ≃+* B ⧸ Ideal.ofRel r
The ring equivalence between RingQuot r and (Ideal.ofRel r).quotient
Equations
Instances For
@[irreducible]
def
RingQuot.mkAlgHom
(S : Type u_1)
[CommSemiring S]
{A : Type u_2}
[Semiring A]
[Algebra S A]
(s : A → A → Prop)
:
The quotient map from an S-algebra to its quotient, as a homomorphism of S-algebras.
Equations
Instances For
theorem
RingQuot.mkAlgHom_def
(S : Type u_1)
[CommSemiring S]
{A : Type u_2}
[Semiring A]
[Algebra S A]
(s : A → A → Prop)
:
RingQuot.mkAlgHom S s = let __src := RingQuot.mkRingHom s;
{ toRingHom := __src, commutes' := ⋯ }
@[simp]
theorem
RingQuot.mkAlgHom_coe
(S : Type uS)
[CommSemiring S]
{A : Type uA}
[Semiring A]
[Algebra S A]
(s : A → A → Prop)
:
↑(RingQuot.mkAlgHom S s) = RingQuot.mkRingHom s
theorem
RingQuot.mkAlgHom_rel
(S : Type uS)
[CommSemiring S]
{A : Type uA}
[Semiring A]
[Algebra S A]
{s : A → A → Prop}
{x : A}
{y : A}
(w : s x y)
:
(RingQuot.mkAlgHom S s) x = (RingQuot.mkAlgHom S s) y
theorem
RingQuot.mkAlgHom_surjective
(S : Type uS)
[CommSemiring S]
{A : Type uA}
[Semiring A]
[Algebra S A]
(s : A → A → Prop)
:
theorem
RingQuot.preLiftAlgHom_def
(S : Type u_1)
[CommSemiring S]
{A : Type u_2}
[Semiring A]
[Algebra S A]
{B : Type u_3}
[Semiring B]
[Algebra S B]
{s : A → A → Prop}
{f : A →ₐ[S] B}
(h : ∀ ⦃x y : A⦄, s x y → f x = f y)
:
RingQuot.preLiftAlgHom S h = { toFun := fun (x : RingQuot s) => Quot.lift ⇑f ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
map_add' := ⋯, commutes' := ⋯ }
theorem
RingQuot.liftAlgHom_def
(S : Type u_1)
[CommSemiring S]
{A : Type u_2}
[Semiring A]
[Algebra S A]
{B : Type u_3}
[Semiring B]
[Algebra S B]
{s : A → A → Prop}
:
RingQuot.liftAlgHom S = { toFun := fun (f' : { f : A →ₐ[S] B // ∀ ⦃x y : A⦄, s x y → f x = f y }) => RingQuot.preLiftAlgHom S ⋯,
invFun := fun (F : RingQuot s →ₐ[S] B) => ⟨F.comp (RingQuot.mkAlgHom S s), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
@[irreducible]
def
RingQuot.liftAlgHom
(S : Type u_1)
[CommSemiring S]
{A : Type u_2}
[Semiring A]
[Algebra S A]
{B : Type u_3}
[Semiring B]
[Algebra S B]
{s : A → A → Prop}
:
Any S-algebra homomorphism f : A →ₐ[S] B which respects a relation s : A → A → Prop
factors uniquely through a morphism RingQuot s →ₐ[S] B.
Equations
Instances For
@[simp]
theorem
RingQuot.liftAlgHom_mkAlgHom_apply
(S : Type uS)
[CommSemiring S]
{A : Type uA}
[Semiring A]
[Algebra S A]
{B : Type u₄}
[Semiring B]
[Algebra S B]
(f : A →ₐ[S] B)
{s : A → A → Prop}
(w : ∀ ⦃x y : A⦄, s x y → f x = f y)
(x : A)
:
((RingQuot.liftAlgHom S) ⟨f, w⟩) ((RingQuot.mkAlgHom S s) x) = f x
theorem
RingQuot.liftAlgHom_unique
(S : Type uS)
[CommSemiring S]
{A : Type uA}
[Semiring A]
[Algebra S A]
{B : Type u₄}
[Semiring B]
[Algebra S B]
(f : A →ₐ[S] B)
{s : A → A → Prop}
(w : ∀ ⦃x y : A⦄, s x y → f x = f y)
(g : RingQuot s →ₐ[S] B)
(h : g.comp (RingQuot.mkAlgHom S s) = f)
:
g = (RingQuot.liftAlgHom S) ⟨f, w⟩
theorem
RingQuot.eq_liftAlgHom_comp_mkAlgHom
(S : Type uS)
[CommSemiring S]
{A : Type uA}
[Semiring A]
[Algebra S A]
{B : Type u₄}
[Semiring B]
[Algebra S B]
{s : A → A → Prop}
(f : RingQuot s →ₐ[S] B)
:
f = (RingQuot.liftAlgHom S) ⟨f.comp (RingQuot.mkAlgHom S s), ⋯⟩