open import 1Lab.Equiv.Embedding

open import Algebra.Prelude
open import Algebra.Ring

module Algebra.Ring.Commutative where

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 hiding (_β†ͺ_)
    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 (βˆ™-cancel-r p q βˆ™ sym (βˆ™-id-r p)))

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

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

module CRing {β„“} (R : CRing β„“) where
  open CRing-on (R .snd) public