Ring of real numbers

src/real-numbers.lagda.md

@@ -9,6 +9,7 @@ open import real-numbers.absolute-value-real-numbers public
 open import real-numbers.addition-lower-dedekind-real-numbers public
 open import real-numbers.addition-real-numbers public
 open import real-numbers.addition-upper-dedekind-real-numbers public
+open import real-numbers.additive-group-of-real-numbers public
 open import real-numbers.apartness-real-numbers public
 open import real-numbers.arithmetically-located-dedekind-cuts public
 open import real-numbers.binary-maximum-real-numbers public
@@ -38,6 +39,7 @@ open import real-numbers.minimum-inhabited-finitely-enumerable-subsets-real-numb
 open import real-numbers.minimum-lower-dedekind-real-numbers public
 open import real-numbers.minimum-upper-dedekind-real-numbers public
 open import real-numbers.multiplication-real-numbers public
+open import real-numbers.multiplicative-monoid-of-real-numbers public
 open import real-numbers.negation-lower-upper-dedekind-real-numbers public
 open import real-numbers.negation-real-numbers public
 open import real-numbers.nonnegative-real-numbers public
@@ -48,6 +50,7 @@ open import real-numbers.rational-real-numbers public
 open import real-numbers.rational-upper-dedekind-real-numbers public
 open import real-numbers.real-numbers-from-lower-dedekind-real-numbers public
 open import real-numbers.real-numbers-from-upper-dedekind-real-numbers public
+open import real-numbers.ring-of-real-numbers public
 open import real-numbers.saturation-inequality-real-numbers public
 open import real-numbers.similarity-real-numbers public
 open import real-numbers.square-roots-nonnegative-real-numbers public

src/real-numbers/addition-real-numbers.lagda.md

@@ -33,12 +33,6 @@ open import foundation.propositional-truncations
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
-open import group-theory.abelian-groups
-open import group-theory.commutative-monoids
-open import group-theory.groups
-open import group-theory.monoids
-open import group-theory.semigroups
-
 open import logic.functoriality-existential-quantification
 
 open import real-numbers.addition-lower-dedekind-real-numbers
@@ -485,41 +479,6 @@ module _
             by sim-eq-ℝ (ap (_+ℝ neg-ℝ y) (left-unit-law-add-ℝ _)))
 ```
 
-### The Abelian group of real numbers at `lzero` under addition
-
-```agda
-semigroup-add-ℝ-lzero : Semigroup (lsuc lzero)
-semigroup-add-ℝ-lzero =
-  ( ℝ-Set lzero ,
-    add-ℝ ,
-    associative-add-ℝ)
-
-monoid-add-ℝ-lzero : Monoid (lsuc lzero)
-monoid-add-ℝ-lzero =
-  ( semigroup-add-ℝ-lzero ,
-    zero-ℝ ,
-    left-unit-law-add-ℝ ,
-    right-unit-law-add-ℝ)
-
-commutative-monoid-add-ℝ-lzero : Commutative-Monoid (lsuc lzero)
-commutative-monoid-add-ℝ-lzero =
-  ( monoid-add-ℝ-lzero ,
-    commutative-add-ℝ)
-
-group-add-ℝ-lzero : Group (lsuc lzero)
-group-add-ℝ-lzero =
-  ( ( semigroup-add-ℝ-lzero) ,
-    ( zero-ℝ , left-unit-law-add-ℝ , right-unit-law-add-ℝ) ,
-    ( neg-ℝ ,
-      eq-sim-ℝ ∘ left-inverse-law-add-ℝ ,
-      eq-sim-ℝ ∘ right-inverse-law-add-ℝ))
-
-abelian-group-add-ℝ-lzero : Ab (lsuc lzero)
-abelian-group-add-ℝ-lzero =
-  ( group-add-ℝ-lzero ,
-    commutative-add-ℝ)
-```
-
 ### If `x + y` is similar to `0`, then `y` is similar to `-x` and `x` is similar to `-y`
 
 ```agda

src/real-numbers/additive-group-of-real-numbers.lagda.md

@@ -0,0 +1,70 @@
+# The additive group of Dedekind real numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module real-numbers.additive-group-of-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.universe-levels
+
+open import group-theory.abelian-groups
+open import group-theory.commutative-monoids
+open import group-theory.groups
+open import group-theory.monoids
+open import group-theory.semigroups
+
+open import real-numbers.addition-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.negation-real-numbers
+open import real-numbers.rational-real-numbers
+open import real-numbers.similarity-real-numbers
+```
+
+</details>
+
+## Idea
+
+The [real numbers](real-numbers.dedekind-real-numbers.md) form an
+[abelian group](group-theory.abelian-groups.md) under
+[addition](real-numbers.addition-real-numbers.md).
+
+## Definition
+
+```agda
+semigroup-add-ℝ-lzero : Semigroup (lsuc lzero)
+semigroup-add-ℝ-lzero =
+  ( ℝ-Set lzero ,
+    add-ℝ ,
+    associative-add-ℝ)
+
+monoid-add-ℝ-lzero : Monoid (lsuc lzero)
+monoid-add-ℝ-lzero =
+  ( semigroup-add-ℝ-lzero ,
+    zero-ℝ ,
+    left-unit-law-add-ℝ ,
+    right-unit-law-add-ℝ)
+
+commutative-monoid-add-ℝ-lzero : Commutative-Monoid (lsuc lzero)
+commutative-monoid-add-ℝ-lzero =
+  ( monoid-add-ℝ-lzero ,
+    commutative-add-ℝ)
+
+group-add-ℝ-lzero : Group (lsuc lzero)
+group-add-ℝ-lzero =
+  ( ( semigroup-add-ℝ-lzero) ,
+    ( zero-ℝ , left-unit-law-add-ℝ , right-unit-law-add-ℝ) ,
+    ( neg-ℝ ,
+      eq-sim-ℝ ∘ left-inverse-law-add-ℝ ,
+      eq-sim-ℝ ∘ right-inverse-law-add-ℝ))
+
+ab-add-ℝ-lzero : Ab (lsuc lzero)
+ab-add-ℝ-lzero =
+  ( group-add-ℝ-lzero ,
+    commutative-add-ℝ)
+```

src/real-numbers/multiplicative-monoid-of-real-numbers.lagda.md

@@ -0,0 +1,52 @@
+# The multiplicative monoid of real numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module real-numbers.multiplicative-monoid-of-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import group-theory.commutative-monoids
+open import group-theory.monoids
+open import group-theory.semigroups
+
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.multiplication-real-numbers
+open import real-numbers.rational-real-numbers
+```
+
+</details>
+
+## Idea
+
+The [real numbers](real-numbers.dedekind-real-numbers.md) form a
+[commutative monoid](group-theory.commutative-monoids.md) under
+[multiplication](real-numbers.multiplication-real-numbers.md).
+
+## Definition
+
+```agda
+semigroup-mul-ℝ-lzero : Semigroup (lsuc lzero)
+semigroup-mul-ℝ-lzero =
+  ( ℝ-Set lzero ,
+    mul-ℝ ,
+    associative-mul-ℝ)
+
+monoid-mul-ℝ-lzero : Monoid (lsuc lzero)
+monoid-mul-ℝ-lzero =
+  ( semigroup-mul-ℝ-lzero ,
+    one-ℝ ,
+    left-unit-law-mul-ℝ ,
+    right-unit-law-mul-ℝ)
+
+commutative-monoid-mul-ℝ-lzero : Commutative-Monoid (lsuc lzero)
+commutative-monoid-mul-ℝ-lzero =
+  ( monoid-mul-ℝ-lzero ,
+    commutative-mul-ℝ)
+```

src/real-numbers/ring-of-real-numbers.lagda.md

@@ -0,0 +1,49 @@
+# The ring of real numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module real-numbers.ring-of-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.commutative-rings
+
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import real-numbers.additive-group-of-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.multiplication-real-numbers
+open import real-numbers.rational-real-numbers
+
+open import ring-theory.rings
+```
+
+</details>
+
+## Idea
+
+The [real numbers](real-numbers.dedekind-real-numbers.md) form a
+[commutative ring](commutative-algebra.commutative-rings.md) under
+[multiplication](real-numbers.multiplication-real-numbers.md) and
+[addition](real-numbers.addition-real-numbers.md).
+
+## Definition
+
+```agda
+ring-ℝ-lzero : Ring (lsuc lzero)
+ring-ℝ-lzero =
+  ( ab-add-ℝ-lzero ,
+    ( mul-ℝ , associative-mul-ℝ) ,
+    ( one-ℝ , left-unit-law-mul-ℝ , right-unit-law-mul-ℝ) ,
+    left-distributive-mul-add-ℝ ,
+    right-distributive-mul-add-ℝ)
+
+commutative-ring-ℝ-lzero : Commutative-Ring (lsuc lzero)
+commutative-ring-ℝ-lzero =
+  ( ring-ℝ-lzero ,
+    commutative-mul-ℝ)
+```