open import 1Lab.Function.Embedding

open import Algebra.Ring

open import Cat.Displayed.Univalence.Thin
open import Cat.Prelude hiding (_*_ ; _+_)

open import Data.Int.Properties
open import Data.Int.Base

import Algebra.Ring.Reasoning as Kit

module Algebra.Ring.Commutative where

open Ring-on using (_*_)

Commutative ringsπŸ”—

This module is not very mathematically interesting: All it exists to do is to package commutative rings together into one datum.

record CRing-on {β„“} (R : Type β„“) : Type β„“ where
  field
    has-ring-on : Ring-on R
    *-commutes  : βˆ€ {x y} β†’ has-ring-on ._*_ x y ≑ has-ring-on ._*_ y x
  open Ring-on has-ring-on public


CRing-structure : βˆ€ β„“ β†’ Thin-structure β„“ CRing-on
CRing-structure β„“ = Full-substructure β„“ CRing-on Ring-on emb (Ring-structure β„“) where
  open CRing-on
  emb : βˆ€ X β†’ CRing-on X β†ͺ Ring-on X
  emb X .fst = has-ring-on
  emb X .snd y (r , p) (s , q) =
    Ξ£-pathp (Ξ» i β†’
      record { has-ring-on = (p βˆ™ sym q) i
              ; *-commutes  = Ξ» {x} {y} j β†’
                is-set→squarep (λ i j → CRing-on.has-is-set r)
                  (Ξ» i β†’ (p βˆ™ sym q) i ._*_ x y)
                  (r .*-commutes)
                  (s .*-commutes)
                  (Ξ» i β†’ (p βˆ™ sym q) i ._*_ y x)
                  i j
              })
      (commutesβ†’square (βˆ™-cancelr p q βˆ™ sym (βˆ™-idr p)))

CRings : βˆ€ β„“ β†’ Precategory (lsuc β„“) β„“
CRings β„“ = Structured-objects (CRing-structure β„“)

CRing : βˆ€ β„“ β†’ Type (lsuc β„“)
CRing β„“ = CRings β„“ .Precategory.Ob

module CRing {β„“} (R : CRing β„“) where
  ring : Ring β„“
  ring .fst = R .fst
  ring .snd = record { CRing-on (R .snd) }

  open CRing-on (R .snd) using (*-commutes ; _+_ ; _*_ ; -_ ; _-_ ; 1r ; 0r) public
  open Kit ring hiding (_+_ ; _*_ ; -_ ; _-_ ; 1r ; 0r) public

is-commutative-ring : βˆ€ {β„“} (R : Ring β„“) β†’ Type _
is-commutative-ring R = βˆ€ {x y} β†’ x R.* y ≑ y R.* x where
  module R = Ring-on (R .snd)

β„€-comm : CRing lzero
β„€-comm = record { fst = el! Int ; snd = record { has-ring-on = β„€ .snd ; *-commutes = Ξ» {x y} β†’ *β„€-commutative x y } }