module Algebra.Ring.Quotient {β} (R : Ring β) where

# Quotient ringsπ

Let
$R$
be a ring and
$IβR$
be an ideal. Because rings have an underlying abelian group, the ideal
$IβR$
determines a normal subgroup
$I$
of
$Rβs$
additive group, so that we may form the quotient group
$R/I.$
And since ideals are closed under multiplication^{1}, we
can extend
$Rβs$
multiplication to a multiplication operation on
$R/I$
in a canonical way! In that case, we refer to
$R/I$
as a **quotient ring**.

Really, the bulk of the construction has already been done (in the section about quotient groups), so all that remains is the following construction: We want to show that $xy$ is invariant under equivalence for both $x$ and $y$ (and we may treat them separately for comprehensibilityβs sake).

private quot-grp : Group _ quot-grp = R.additive-group /α΄³ I.idealβnormal module R/I = Group-on (quot-grp .snd)

quot-mul : β quot-grp β β β quot-grp β β β quot-grp β quot-mul = Coeq-recβ squash (Ξ» x y β inc (x R.* y)) (Ξ» a (_ , _ , r) β p1 a r) (Ξ» a (_ , _ , r) β p2 a r) where

On one side, we must show that $[ax]=[ay]$ supposing that $[x]=[y],$ i.e.Β that $(xβy)βI.$ But since $I$ is an ideal, we have $(axβay)βI,$ thus $[ax]=[ay].$ And on the other side, we have the same thing: Since $(xβy)βI,$ also $(xaβya)βI,$ so $[xa]=[ya].$

p1 : β a {x y} (r : (x R.- y) β I) β inc (x R.* a) β‘ inc (y R.* a) p1 a {x} {y} x-yβI = quot $ subst (_β I) (R.*-distribr β ap (x R.* a R.+_) (sym R.neg-*-l)) (I.has-*α΅£ a x-yβI) p2 : β a {x y} (r : (x R.- y) β I) β inc (a R.* x) β‘ inc (a R.* y) p2 a {x} {y} x-yβI = quot $ subst (_β I) (R.*-distribl β ap (a R.* x R.+_) (sym R.neg-*-r)) (I.has-*β a x-yβI)

##
Showing that this extends to a ring structure on
$R/I$
is annoying, but not non-trivial, so we keep in this `<details>`

fold. Most of the proof
is appealing to the elimination principle(s) for quotients into
propositions, then applying
$Rβs$
laws.

open make-ring make-R/I : make-ring β quot-grp β make-R/I .ring-is-set = squash make-R/I .0R = inc 0r make-R/I ._+_ = R/I._β_ make-R/I .-_ = R/I.inverse make-R/I .+-idl x = R/I.idl make-R/I .+-invr x = R/I.inverser {x} make-R/I .+-assoc x y z = R/I.associative {x} {y} {z} make-R/I .1R = inc R.1r make-R/I ._*_ = quot-mul make-R/I .+-comm = elim! Ξ» x y β ap Coeq.inc R.+-commutes make-R/I .*-idl = elim! Ξ» x β ap Coeq.inc R.*-idl make-R/I .*-idr = elim! Ξ» x β ap Coeq.inc R.*-idr make-R/I .*-assoc = elim! Ξ» x y z β ap Coeq.inc R.*-associative make-R/I .*-distribl = elim! Ξ» x y z β ap Coeq.inc R.*-distribl make-R/I .*-distribr = elim! Ξ» x y z β ap Coeq.inc R.*-distribr

R/I : Ring β R/I = to-ring make-R/I

As a quick aside, if $I$ is a complemented ideal (equivalently: a decidable ideal), and $R$ is a discrete ring, then the quotient ring is also discrete. This is a specialisation of a general result about decidable quotient sets, but we mention it here regardless:

Discrete-ring-quotient : (β x β Dec (x β I)) β Discrete β R/I β Discrete-ring-quotient decβI = Discrete-quotient (normal-subgroupβcongruence R.additive-group I.idealβnormal) (Ξ» x y β decβI (x R.- y))

recall that all our rings are commutative, so theyβre closed under multiplication by a constant on either sideβ©οΈ