open import Algebra.Group.Cat.Base
open import Algebra.Group.Subgroup
open import Algebra.Ring.Ideal
open import Algebra.Prelude
open import Algebra.Group
open import Algebra.Ring

open import Data.Power
open import Data.Dec

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

open Ring-on (R .snd)
private module R = Ring-on (R .snd)


# Quotient ringsπ

Let be a ring and be an ideal. Because rings have an underlying abelian group, the ideal determines a normal subgroup of additive group, so that we may form the quotient group And since ideals are closed under multiplication1, we can extend multiplication to a multiplication operation on in a canonical way! In that case, we refer to as a quotient ring.

module _ {I : β β R β} (idl : is-ideal R I) where
private module I = is-ideal idl


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 is invariant under equivalence for both and (and we may treat them separately for comprehensibilityβs sake).

  private
quot-grp : Group _
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 supposing that i.e.Β that But since is an ideal, we have thus And on the other side, we have the same thing: Since also so

      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 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 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 is a complemented ideal (equivalently: a decidable ideal), and 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