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

Quotient ringsπŸ”—

Let RR be a ring and IβŠ†RI \sube R be an ideal. Because rings have an underlying abelian group, the ideal IβŠ†RI \sube R determines a normal subgroup II of RR’s additive group, so that we may form the quotient group R/IR/I. And since ideals are closed under multiplication1, we can extend RR’s multiplication to a multiplication operation on R/IR/I in a canonical way! In that case, we refer to R/IR/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 xyxy is invariant under equivalence for both xx and yy (and we may treat them separately for comprehensibility’s sake).

    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][ax] = [ay] supposing that [x]=[y][x] = [y], i.e.Β that (xβˆ’y)∈I(x - y) \in I. But since II is an ideal, we have (axβˆ’ay)∈I(ax - ay) \in I, thus [ax]=[ay][ax] = [ay]. And on the other side, we have the same thing: Since (xβˆ’y)∈I(x - y) \in I, also (xaβˆ’ya)∈I(xa - ya) \in I, so [xa]=[ya][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/IR/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 RR’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 = R/I.idl
  make-R/I .+-invr {x} = R/I.inverser {x}
  make-R/I .+-assoc {x} {y} {z} = sym $ R/I.associative {x} {y} {z}
  make-R/I .1R = inc R.1r
  make-R/I ._*_ = quot-mul
  make-R/I .+-comm {x} {y} =
    Coeq-elim-propβ‚‚ {C = Ξ» x y β†’ x R/I.⋆ y ≑ y R/I.⋆ x} (Ξ» x y β†’ hlevel 1)
      (Ξ» x y β†’ ap Coeq.inc R.+-commutes) x y
  make-R/I .*-idl {x} =
    Coeq-elim-prop {C = Ξ» x β†’ quot-mul (inc R.1r) x ≑ x} (Ξ» _ β†’ hlevel 1)
      (Ξ» x β†’ ap Coeq.inc R.*-idl) x
  make-R/I .*-idr {x} =
    Coeq-elim-prop {C = Ξ» x β†’ quot-mul x (inc R.1r) ≑ x} (Ξ» _ β†’ hlevel 1)
      (Ξ» x β†’ ap Coeq.inc R.*-idr) x
  make-R/I .*-assoc {x} {y} {z} =
    Coeq-elim-prop₃
      {C = Ξ» x y z β†’ quot-mul (quot-mul x y) z ≑ quot-mul x (quot-mul y z)}
      (Ξ» _ _ _ β†’ hlevel 1) (Ξ» x y z β†’ ap Coeq.inc (sym R.*-associative)) x y z
  make-R/I .*-distribl {x} {y} {z} =
    Coeq-elim-prop₃
      {C = Ξ» x y z β†’ quot-mul x (y R/I.⋆ z) ≑ quot-mul x y R/I.⋆ quot-mul x z}
      (Ξ» _ _ _ β†’ hlevel 1) (Ξ» x y z β†’ ap Coeq.inc R.*-distribl) x y z
  make-R/I .*-distribr {x} {y} {z} =
    Coeq-elim-prop₃
      {C = Ξ» x y z β†’ quot-mul (y R/I.⋆ z) x ≑ quot-mul y x R/I.⋆ quot-mul z x}
      (Ξ» _ _ _ β†’ hlevel 1) (Ξ» x y z β†’ ap Coeq.inc R.*-distribr) x y z
  R/I : Ring β„“
  R/I = from-make-ring make-R/I

As a quick aside, if II is a complemented ideal (equivalently: a decidable ideal), and RR 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 : Discrete ⌞ R ⌟ β†’ (βˆ€ x β†’ Dec (x ∈ I)) β†’ Discrete ⌞ R/I ⌟
  Discrete-ring-quotient rdisc dec∈I = Discrete-quotient
    (normal-subgroup→congruence R.additive-group I.ideal→normal)
    rdisc
    (Ξ» x y β†’ dec∈I (x R.- y))

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