Add +-*-commutativeRing structure to Data.Rational (ℚ) via ℚᵘ (#1212)

Author: rwe

CHANGELOG.md

@@ -278,7 +278,13 @@ Other minor additions
   recompute       : .(Coprime n d) → Coprime n d
   ```
 
-* Added new types and constructors to `Data.Rational.Unnormalised`:
+* Add proof to `Algebra.Morphism.RingMonomorphism`:
+ ```agda
+ isCommutativeRing : IsCommutativeRing _≈₂_ _⊕_ _⊛_ ⊝_ 0#₂ 1#₂ →
+                     IsCommutativeRing _≈₁_ _+_ _*_ -_ 0# 1#
+ ```
+
+* Added new types and constructors to `Data.Rational`:
   ```agda
   NonZero     : Pred ℚ 0ℓ
   Positive    : Pred ℚ 0ℓ
@@ -295,6 +301,12 @@ Other minor additions
   nonNegative : p ≥ 0ℚ → NonNegative p
   ```
 
+* Added proofs to `Data.Rational.Properties`:
+ ```agda
+  +-*-isCommutativeRing : IsCommutativeRing _+_ _*_ -_ 0ℚ 1ℚ
+  +-*-commutativeRing   : CommutativeRing 0ℓ 0ℓ
+ ```
+
 * Added new types and constructors to `Data.Rational.Unnormalised`
   ```agda
   _≠_         : Rel ℚᵘ 0ℓ

src/Algebra/Morphism/RingMonomorphism.agda

@@ -127,3 +127,10 @@ isRing isRing = record
   ; distrib          = distrib R.+-isGroup R.*-isMagma R.distrib
   ; zero             = zero R.+-isGroup R.*-isMagma R.zero
   } where module R = IsRing isRing
+
+isCommutativeRing : IsCommutativeRing _≈₂_ _⊕_ _⊛_ ⊝_ 0#₂ 1#₂ →
+                    IsCommutativeRing _≈₁_ _+_ _*_ -_ 0# 1#
+isCommutativeRing isCommRing = record
+  { isRing = isRing C.isRing
+  ; *-comm = *-comm C.*-isMagma C.*-comm
+  } where module C = IsCommutativeRing isCommRing

src/Data/Rational/Properties.agda

@@ -818,6 +818,9 @@ private
 +-*-isRing : IsRing _+_ _*_ -_ 0ℚ 1ℚ
 +-*-isRing = *-Monomorphism.isRing ℚᵘ.+-*-isRing
 
++-*-isCommutativeRing : IsCommutativeRing _+_ _*_ -_ 0ℚ 1ℚ
++-*-isCommutativeRing = *-Monomorphism.isCommutativeRing ℚᵘ.+-*-isCommutativeRing
+
 ------------------------------------------------------------------------
 -- Packages
 
@@ -846,6 +849,11 @@ private
   { isRing = +-*-isRing
   }
 
++-*-commutativeRing : CommutativeRing 0ℓ 0ℓ
++-*-commutativeRing = record
+  { isCommutativeRing = +-*-isCommutativeRing
+  }
+
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------