Quotients of non-commutative rings #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
@[protected, instance]
def
ring_con.quotient.algebra
{S : Type u₂}
[comm_semiring S]
{A : Type u₃}
[semiring A]
[algebra S A]
(c : ring_con A) :
Equations
- ring_con.quotient.algebra c = {to_has_smul := {smul := has_smul.smul (ring_con.quotient.has_smul c)}, to_ring_hom := c.mk'.comp (algebra_map S A), commutes' := _, smul_def' := _}
@[simp, norm_cast]
theorem
ring_con.coe_algebra_map
{S : Type u₂}
[comm_semiring S]
{A : Type u₃}
[semiring A]
[algebra S A]
(c : ring_con A)
(s : S) :
↑(⇑(algebra_map S A) s) = ⇑(algebra_map S c.quotient) s
- of : ∀ {R : Type u₁} [_inst_1 : semiring R] {r : R → R → Prop} ⦃x y : R⦄, r x y → ring_quot.rel r x y
- add_left : ∀ {R : Type u₁} [_inst_1 : semiring R] {r : R → R → Prop} ⦃a b c : R⦄, ring_quot.rel r a b → ring_quot.rel r (a + c) (b + c)
- mul_left : ∀ {R : Type u₁} [_inst_1 : semiring R] {r : R → R → Prop} ⦃a b c : R⦄, ring_quot.rel r a b → ring_quot.rel r (a * c) (b * c)
- mul_right : ∀ {R : Type u₁} [_inst_1 : semiring R] {r : R → R → Prop} ⦃a b c : R⦄, ring_quot.rel r b c → ring_quot.rel r (a * b) (a * c)
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.
theorem
ring_quot.rel.add_right
{R : Type u₁}
[semiring R]
{r : R → R → Prop}
⦃a b c : R⦄
(h : ring_quot.rel r b c) :
ring_quot.rel r (a + b) (a + c)
theorem
ring_quot.rel.neg
{R : Type u₁}
[ring R]
{r : R → R → Prop}
⦃a b : R⦄
(h : ring_quot.rel r a b) :
ring_quot.rel r (-a) (-b)
theorem
ring_quot.rel.sub_left
{R : Type u₁}
[ring R]
{r : R → R → Prop}
⦃a b c : R⦄
(h : ring_quot.rel r a b) :
ring_quot.rel r (a - c) (b - c)
theorem
ring_quot.rel.sub_right
{R : Type u₁}
[ring R]
{r : R → R → Prop}
⦃a b c : R⦄
(h : ring_quot.rel r b c) :
ring_quot.rel r (a - b) (a - c)
theorem
ring_quot.rel.smul
{S : Type u₂}
[comm_semiring S]
{A : Type u₃}
[semiring A]
[algebra S A]
{r : A → A → Prop}
(k : S)
⦃a b : A⦄
(h : ring_quot.rel r a b) :
ring_quot.rel r (k • a) (k • b)
eqv_gen (ring_quot.rel r) is a ring congruence.
- to_quot : quot (ring_quot.rel r)
The quotient of a ring by an arbitrary relation.
Instances for ring_quot
- ring_quot.has_sizeof_inst
- ring_quot.has_zero
- ring_quot.has_one
- ring_quot.has_add
- ring_quot.has_mul
- ring_quot.nat.has_pow
- ring_quot.has_neg
- ring_quot.has_sub
- ring_quot.has_smul
- ring_quot.semiring
- ring_quot.ring
- ring_quot.comm_semiring
- ring_quot.comm_ring
- ring_quot.inhabited
- ring_quot.algebra
- ring_quot.is_scalar_tower
- ring_quot.smul_comm_class
@[protected, instance]
def
ring_quot.has_smul
{R : Type u₁}
[semiring R]
{S : Type u₂}
[comm_semiring S]
(r : R → R → Prop)
[algebra S R] :
Equations
- ring_quot.has_smul r = {smul := smul r _inst_5}
theorem
ring_quot.zero_quot
{R : Type u₁}
[semiring R]
(r : R → R → Prop) :
{to_quot := quot.mk (ring_quot.rel r) 0} = 0
theorem
ring_quot.one_quot
{R : Type u₁}
[semiring R]
(r : R → R → Prop) :
{to_quot := quot.mk (ring_quot.rel r) 1} = 1
theorem
ring_quot.add_quot
{R : Type u₁}
[semiring R]
(r : R → R → Prop)
{a b : R} :
{to_quot := quot.mk (ring_quot.rel r) a} + {to_quot := quot.mk (ring_quot.rel r) b} = {to_quot := quot.mk (ring_quot.rel r) (a + b)}
theorem
ring_quot.mul_quot
{R : Type u₁}
[semiring R]
(r : R → R → Prop)
{a b : R} :
{to_quot := quot.mk (ring_quot.rel r) a} * {to_quot := quot.mk (ring_quot.rel r) b} = {to_quot := quot.mk (ring_quot.rel r) (a * b)}
theorem
ring_quot.neg_quot
{R : Type u₁}
[ring R]
(r : R → R → Prop)
{a : R} :
-{to_quot := quot.mk (ring_quot.rel r) a} = {to_quot := quot.mk (ring_quot.rel r) (-a)}
theorem
ring_quot.sub_quot
{R : Type u₁}
[ring R]
(r : R → R → Prop)
{a b : R} :
{to_quot := quot.mk (ring_quot.rel r) a} - {to_quot := quot.mk (ring_quot.rel r) b} = {to_quot := quot.mk (ring_quot.rel r) (a - b)}
theorem
ring_quot.smul_quot
{R : Type u₁}
[semiring R]
{S : Type u₂}
[comm_semiring S]
(r : R → R → Prop)
[algebra S R]
{n : S}
{a : R} :
n • {to_quot := quot.mk (ring_quot.rel r) a} = {to_quot := quot.mk (ring_quot.rel r) (n • a)}
@[protected, instance]
Equations
- ring_quot.semiring r = {add := has_add.add (ring_quot.has_add r), add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := has_smul.smul (ring_quot.has_smul r), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul (ring_quot.has_mul r), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := 1, one_mul := _, mul_one := _, nat_cast := nat_cast r, nat_cast_zero := _, nat_cast_succ := _, npow := λ (n : ℕ) (x : ring_quot r), x ^ n, npow_zero' := _, npow_succ' := _}
@[protected, instance]
Equations
- ring_quot.ring r = {add := semiring.add (ring_quot.semiring r), add_assoc := _, zero := semiring.zero (ring_quot.semiring r), zero_add := _, add_zero := _, nsmul := semiring.nsmul (ring_quot.semiring r), nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg (ring_quot.has_neg r), sub := has_sub.sub (ring_quot.has_sub r), sub_eq_add_neg := _, zsmul := has_smul.smul (ring_quot.has_smul r), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := add_comm_group_with_one.int_cast._default semiring.nat_cast semiring.add _ semiring.zero _ _ semiring.nsmul _ _ semiring.one _ _ has_neg.neg has_sub.sub _ has_smul.smul _ _ _ _, nat_cast := semiring.nat_cast (ring_quot.semiring r), one := semiring.one (ring_quot.semiring r), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := semiring.mul (ring_quot.semiring r), mul_assoc := _, one_mul := _, mul_one := _, npow := semiring.npow (ring_quot.semiring r), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
@[protected, instance]
Equations
- ring_quot.comm_semiring r = {add := semiring.add (ring_quot.semiring r), add_assoc := _, zero := semiring.zero (ring_quot.semiring r), zero_add := _, add_zero := _, nsmul := semiring.nsmul (ring_quot.semiring r), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul (ring_quot.semiring r), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one (ring_quot.semiring r), one_mul := _, mul_one := _, nat_cast := semiring.nat_cast (ring_quot.semiring r), nat_cast_zero := _, nat_cast_succ := _, npow := semiring.npow (ring_quot.semiring r), npow_zero' := _, npow_succ' := _, mul_comm := _}
@[protected, instance]
Equations
- ring_quot.comm_ring r = {add := comm_semiring.add (ring_quot.comm_semiring r), add_assoc := _, zero := comm_semiring.zero (ring_quot.comm_semiring r), zero_add := _, add_zero := _, nsmul := comm_semiring.nsmul (ring_quot.comm_semiring r), nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg (ring_quot.ring r), sub := ring.sub (ring_quot.ring r), sub_eq_add_neg := _, zsmul := ring.zsmul (ring_quot.ring r), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast (ring_quot.ring r), nat_cast := comm_semiring.nat_cast (ring_quot.comm_semiring r), one := comm_semiring.one (ring_quot.comm_semiring r), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := comm_semiring.mul (ring_quot.comm_semiring r), mul_assoc := _, one_mul := _, mul_one := _, npow := comm_semiring.npow (ring_quot.comm_semiring r), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
@[protected, instance]
def
ring_quot.algebra
{R : Type u₁}
[semiring R]
{S : Type u₂}
[comm_semiring S]
[algebra S R]
(r : R → R → Prop) :
Equations
- ring_quot.algebra r = {to_has_smul := {smul := has_smul.smul (ring_quot.has_smul r)}, to_ring_hom := {to_fun := λ (r_1 : S), {to_quot := quot.mk (ring_quot.rel r) (⇑(algebra_map S R) r_1)}, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
@[irreducible]
The quotient map from a ring to its quotient, as a homomorphism of rings.
theorem
ring_quot.mk_ring_hom_rel
{R : Type u₁}
[semiring R]
{r : R → R → Prop}
{x y : R}
(w : r x y) :
⇑(ring_quot.mk_ring_hom r) x = ⇑(ring_quot.mk_ring_hom r) y
@[irreducible]
Any ring homomorphism f : R →+* T which respects a relation r : R → R → Prop
factors uniquely through a morphism ring_quot r →+* T.
Equations
- ring_quot.lift = {to_fun := λ (f' : {f // ∀ ⦃x y : R⦄, r x y → ⇑f x = ⇑f y}), let f : R →+* T := ↑f' in {to_fun := λ (x : ring_quot r), quot.lift ⇑f _ x.to_quot, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, inv_fun := λ (F : ring_quot r →+* T), ⟨F.comp (ring_quot.mk_ring_hom r), _⟩, left_inv := _, right_inv := _}
We now verify that in the case of a commutative ring, the ring_quot construction
agrees with the quotient by the appropriate ideal.
def
ring_quot.ring_quot_to_ideal_quotient
{B : Type u₁}
[comm_ring B]
(r : B → B → Prop) :
ring_quot r →+* B ⧸ ideal.of_rel r
The universal ring homomorphism from ring_quot r to B ⧸ ideal.of_rel r.
Equations
@[simp]
theorem
ring_quot.ring_quot_to_ideal_quotient_apply
{B : Type u₁}
[comm_ring B]
(r : B → B → Prop)
(x : B) :
⇑(ring_quot.ring_quot_to_ideal_quotient r) (⇑(ring_quot.mk_ring_hom r) x) = ⇑(ideal.quotient.mk (ideal.of_rel r)) x
def
ring_quot.ideal_quotient_to_ring_quot
{B : Type u₁}
[comm_ring B]
(r : B → B → Prop) :
B ⧸ ideal.of_rel r →+* ring_quot r
The universal ring homomorphism from B ⧸ ideal.of_rel r to ring_quot r.
Equations
@[simp]
theorem
ring_quot.ideal_quotient_to_ring_quot_apply
{B : Type u₁}
[comm_ring B]
(r : B → B → Prop)
(x : B) :
⇑(ring_quot.ideal_quotient_to_ring_quot r) (⇑(ideal.quotient.mk (ideal.of_rel r)) x) = ⇑(ring_quot.mk_ring_hom r) x
def
ring_quot.ring_quot_equiv_ideal_quotient
{B : Type u₁}
[comm_ring B]
(r : B → B → Prop) :
ring_quot r ≃+* B ⧸ ideal.of_rel r
The ring equivalence between ring_quot r and (ideal.of_rel r).quotient
theorem
ring_quot.rel.star
{R : Type u₁}
[semiring R]
(r : R → R → Prop)
[star_ring R]
(hr : ∀ (a b : R), r a b → r (has_star.star a) (has_star.star b))
⦃a b : R⦄
(h : ring_quot.rel r a b) :
ring_quot.rel r (has_star.star a) (has_star.star b)
theorem
ring_quot.star'_quot
{R : Type u₁}
[semiring R]
(r : R → R → Prop)
[star_ring R]
(hr : ∀ (a b : R), r a b → r (has_star.star a) (has_star.star b))
{a : R} :
star' r hr {to_quot := quot.mk (ring_quot.rel r) a} = {to_quot := quot.mk (ring_quot.rel r) (has_star.star a)}
def
ring_quot.star_ring
{R : Type u₁}
[semiring R]
[star_ring R]
(r : R → R → Prop)
(hr : ∀ (a b : R), r a b → r (has_star.star a) (has_star.star b)) :
Transfer a star_ring instance through a quotient, if the quotient is invariant to star
Equations
- ring_quot.star_ring r hr = {to_star_semigroup := {to_has_involutive_star := {to_has_star := {star := star' r hr}, star_involutive := _}, star_mul := _}, star_add := _}
@[irreducible]
def
ring_quot.mk_alg_hom
(S : Type u₂)
[comm_semiring S]
{A : Type u₃}
[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.
@[simp]
theorem
ring_quot.mk_alg_hom_coe
(S : Type u₂)
[comm_semiring S]
{A : Type u₃}
[semiring A]
[algebra S A]
(s : A → A → Prop) :
theorem
ring_quot.mk_alg_hom_rel
(S : Type u₂)
[comm_semiring S]
{A : Type u₃}
[semiring A]
[algebra S A]
{s : A → A → Prop}
{x y : A}
(w : s x y) :
⇑(ring_quot.mk_alg_hom S s) x = ⇑(ring_quot.mk_alg_hom S s) y
theorem
ring_quot.mk_alg_hom_surjective
(S : Type u₂)
[comm_semiring S]
{A : Type u₃}
[semiring A]
[algebra S A]
(s : A → A → Prop) :
@[irreducible]
def
ring_quot.lift_alg_hom
(S : Type u₂)
[comm_semiring S]
{A : Type u₃}
[semiring A]
[algebra S A]
{B : Type u₄}
[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 ring_quot s →ₐ[S] B.
Equations
- ring_quot.lift_alg_hom S = {to_fun := λ (f' : {f // ∀ ⦃x y : A⦄, s x y → ⇑f x = ⇑f y}), let f : A →ₐ[S] B := ↑f' in {to_fun := λ (x : ring_quot s), quot.lift ⇑f _ x.to_quot, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}, inv_fun := λ (F : ring_quot s →ₐ[S] B), ⟨F.comp (ring_quot.mk_alg_hom S s), _⟩, left_inv := _, right_inv := _}
@[simp]
theorem
ring_quot.lift_alg_hom_mk_alg_hom_apply
(S : Type u₂)
[comm_semiring S]
{A : Type u₃}
[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) :
⇑(⇑(ring_quot.lift_alg_hom S) ⟨f, w⟩) (⇑(ring_quot.mk_alg_hom S s) x) = ⇑f x
theorem
ring_quot.lift_alg_hom_unique
(S : Type u₂)
[comm_semiring S]
{A : Type u₃}
[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 : ring_quot s →ₐ[S] B)
(h : g.comp (ring_quot.mk_alg_hom S s) = f) :
g = ⇑(ring_quot.lift_alg_hom S) ⟨f, w⟩