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 } }