mathlib documentation

algebra.ring_quot

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!

Since everything runs in parallel for quotients of R-algebras, we do that case at the same time.

inductive ring_quot.rel {R : Type u₁} [semiring R] (r : R → R → Prop) (a a_1 : R) :

Prop

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.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)

def ring_quot {R : Type u₁} [semiring R] (r : R → R → Prop) :

Type u₁

The quotient of a ring by an arbitrary relation.

Equations

ring_quot r = quot (ring_quot.rel r)

@[instance]

def ring_quot.semiring {R : Type u₁} [semiring R] (r : R → R → Prop) :

semiring (ring_quot r)

Equations

ring_quot.semiring r = {add := quot.map₂ has_add.add ring_quot.rel.add_right ring_quot.rel.add_left, add_assoc := _, zero := quot.mk (ring_quot.rel r) 0, zero_add := _, add_zero := _, add_comm := _, mul := quot.map₂ has_mul.mul ring_quot.rel.mul_right ring_quot.rel.mul_left, mul_assoc := _, one := quot.mk (ring_quot.rel r) 1, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}

@[instance]

def ring_quot.ring {R : Type u₁} [ring R] (r : R → R → Prop) :

ring (ring_quot r)

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 := _, neg := quot.map (λ (a : R), -a) ring_quot.rel.neg, add_left_neg := _, add_comm := _, mul := semiring.mul (ring_quot.semiring r), mul_assoc := _, one := semiring.one (ring_quot.semiring r), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}

@[instance]

def ring_quot.comm_semiring {R : Type u₁} [comm_semiring R] (r : R → R → Prop) :

comm_semiring (ring_quot r)

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 := _, add_comm := _, mul := semiring.mul (ring_quot.semiring r), mul_assoc := _, one := semiring.one (ring_quot.semiring r), one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, mul_comm := _}

@[instance]

def ring_quot.comm_ring {R : Type u₁} [comm_ring R] (r : R → R → Prop) :

comm_ring (ring_quot r)

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 := _, neg := ring.neg (ring_quot.ring r), add_left_neg := _, add_comm := _, mul := comm_semiring.mul (ring_quot.comm_semiring r), mul_assoc := _, one := comm_semiring.one (ring_quot.comm_semiring r), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}

@[instance]

def ring_quot.algebra {S : Type u₂} [comm_semiring S] {A : Type u₃} [semiring A] [algebra S A] (s : A → A → Prop) :

algebra S (ring_quot s)

Equations

ring_quot.algebra s = {to_has_scalar := {smul := λ (r : S), quot.map (has_scalar.smul r) _}, to_ring_hom := {to_fun := λ (r : S), quot.mk (ring_quot.rel s) (⇑(algebra_map S A) r), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}

@[instance]

def ring_quot.inhabited {R : Type u₁} [semiring R] (r : R → R → Prop) :

inhabited (ring_quot r)

Equations

ring_quot.inhabited r = {default := 0}

def ring_quot.mk_ring_hom {R : Type u₁} [semiring R] (r : R → R → Prop) :

R →+* ring_quot r

The quotient map from a ring to its quotient, as a homomorphism of rings.

Equations

ring_quot.mk_ring_hom r = {to_fun := quot.mk (ring_quot.rel r), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

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

theorem ring_quot.mk_ring_hom_surjective {R : Type u₁} [semiring R] (r : R → R → Prop) :

function.surjective ⇑(ring_quot.mk_ring_hom r)

@[ext]

theorem ring_quot.ring_quot_ext {R : Type u₁} [semiring R] {T : Type u₄} [semiring T] {r : R → R → Prop} (f g : ring_quot r →+* T) (w : f.comp (ring_quot.mk_ring_hom r) = g.comp (ring_quot.mk_ring_hom r)) :

f = g

def ring_quot.lift {R : Type u₁} [semiring R] {T : Type u₄} [semiring T] (f : R →+* T) {r : R → R → Prop} (w : ∀ ⦃x y : R⦄, r x y → ⇑f x = ⇑f y) :

ring_quot r →+* T

Any ring homomorphism f : R →+* T which respects a relation r : R → R → Prop factors through a morphism ring_quot r →+* T.

Equations

ring_quot.lift f w = {to_fun := quot.lift ⇑f _, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

@[simp]

theorem ring_quot.lift_mk_ring_hom_apply {R : Type u₁} [semiring R] {T : Type u₄} [semiring T] (f : R →+* T) {r : R → R → Prop} (w : ∀ ⦃x y : R⦄, r x y → ⇑f x = ⇑f y) (x : R) :

⇑(ring_quot.lift f w) (⇑(ring_quot.mk_ring_hom r) x) = ⇑f x

theorem ring_quot.lift_unique {R : Type u₁} [semiring R] {T : Type u₄} [semiring T] (f : R →+* T) {r : R → R → Prop} (w : ∀ ⦃x y : R⦄, r x y → ⇑f x = ⇑f y) (g : ring_quot r →+* T) (h : g.comp (ring_quot.mk_ring_hom r) = f) :

g = ring_quot.lift f w

theorem ring_quot.eq_lift_comp_mk_ring_hom {R : Type u₁} [semiring R] {T : Type u₄} [semiring T] {r : R → R → Prop} (f : ring_quot r →+* T) :

f = ring_quot.lift (f.comp (ring_quot.mk_ring_hom r)) _

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 →+* (ideal.of_rel r).quotient

The universal ring homomorphism from ring_quot r to (ideal.of_rel r).quotient.

Equations

ring_quot.ring_quot_to_ideal_quotient r = ring_quot.lift (ideal.quotient.mk (ideal.of_rel r)) _

@[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) :

(ideal.of_rel r).quotient →+* ring_quot r

The universal ring homomorphism from (ideal.of_rel r).quotient to ring_quot r.

Equations

ring_quot.ideal_quotient_to_ring_quot r = ideal.quotient.lift (ideal.of_rel r) (ring_quot.mk_ring_hom r) _

@[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 ≃+* (ideal.of_rel r).quotient

The ring equivalence between ring_quot r and (ideal.of_rel r).quotient

Equations

ring_quot.ring_quot_equiv_ideal_quotient r = ring_equiv.of_hom_inv (ring_quot.ring_quot_to_ideal_quotient r) (ring_quot.ideal_quotient_to_ring_quot r) _ _

def ring_quot.mk_alg_hom (S : Type u₂) [comm_semiring S] {A : Type u₃} [semiring A] [algebra S A] (s : A → A → Prop) :

A →ₐ[S] ring_quot s

The quotient map from an S-algebra to its quotient, as a homomorphism of S-algebras.

Equations

ring_quot.mk_alg_hom S s = {to_fun := (ring_quot.mk_ring_hom s).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

@[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) :

↑(ring_quot.mk_alg_hom S s) = ring_quot.mk_ring_hom s

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) :

function.surjective ⇑(ring_quot.mk_alg_hom S s)

@[ext]

theorem ring_quot.ring_quot_ext' (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} (f g : ring_quot s →ₐ[S] B) (w : f.comp (ring_quot.mk_alg_hom S s) = g.comp (ring_quot.mk_alg_hom S s)) :

f = g

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] (f : A →ₐ[S] B) {s : A → A → Prop} (w : ∀ ⦃x y : A⦄, s x y → ⇑f x = ⇑f y) :

ring_quot s →ₐ[S] B

Any S-algebra homomorphism f : A →ₐ[S] B which respects a relation s : A → A → Prop factors through a morphism ring_quot s →ₐ[S] B.

Equations

ring_quot.lift_alg_hom S f w = {to_fun := quot.lift ⇑f _, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

@[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

theorem ring_quot.eq_lift_alg_hom_comp_mk_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} (f : ring_quot s →ₐ[S] B) :

f = ring_quot.lift_alg_hom S (f.comp (ring_quot.mk_alg_hom S s)) _