The large ring of real numbers (#1664)

Author: lowasser

src/commutative-algebra.lagda.md

@@ -36,6 +36,7 @@ open import commutative-algebra.invertible-elements-commutative-rings public
 open import commutative-algebra.isomorphisms-commutative-rings public
 open import commutative-algebra.joins-ideals-commutative-rings public
 open import commutative-algebra.joins-radical-ideals-commutative-rings public
+open import commutative-algebra.large-commutative-rings public
 open import commutative-algebra.local-commutative-rings public
 open import commutative-algebra.maximal-ideals-commutative-rings public
 open import commutative-algebra.multiples-of-elements-commutative-rings public

src/commutative-algebra/large-commutative-rings.lagda.md

@@ -0,0 +1,124 @@
+# Large commutative rings
+
+```agda
+module commutative-algebra.large-commutative-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.commutative-rings
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.large-binary-relations
+open import foundation.large-similarity-relations
+open import foundation.sets
+open import foundation.universe-levels
+
+open import group-theory.large-commutative-monoids
+
+open import ring-theory.large-rings
+```
+
+</details>
+
+## Idea
+
+A {{#concept "large commutative ring" Agda=Large-Commutative-Ring}} is a
+[large ring](ring-theory.large-rings.md) with a commutative multiplicative
+operation.
+
+## Definition
+
+```agda
+record Large-Commutative-Ring
+  (α : Level → Level) (β : Level → Level → Level) : UUω where
+
+  constructor
+    make-Large-Commutative-Ring
+
+  field
+    large-ring-Large-Commutative-Ring : Large-Ring α β
+
+  type-Large-Commutative-Ring : (l : Level) → UU (α l)
+  type-Large-Commutative-Ring =
+    type-Large-Ring large-ring-Large-Commutative-Ring
+
+  set-Large-Commutative-Ring : (l : Level) → Set (α l)
+  set-Large-Commutative-Ring = set-Large-Ring large-ring-Large-Commutative-Ring
+
+  add-Large-Commutative-Ring :
+    {l1 l2 : Level} →
+    type-Large-Commutative-Ring l1 →
+    type-Large-Commutative-Ring l2 →
+    type-Large-Commutative-Ring (l1 ⊔ l2)
+  add-Large-Commutative-Ring = add-Large-Ring large-ring-Large-Commutative-Ring
+
+  zero-Large-Commutative-Ring : type-Large-Commutative-Ring lzero
+  zero-Large-Commutative-Ring =
+    zero-Large-Ring large-ring-Large-Commutative-Ring
+
+  sim-prop-Large-Commutative-Ring :
+    Large-Relation-Prop β type-Large-Commutative-Ring
+  sim-prop-Large-Commutative-Ring =
+    sim-prop-Large-Ring large-ring-Large-Commutative-Ring
+
+  sim-Large-Commutative-Ring : Large-Relation β type-Large-Commutative-Ring
+  sim-Large-Commutative-Ring = sim-Large-Ring large-ring-Large-Commutative-Ring
+
+  raise-Large-Commutative-Ring :
+    {l1 : Level} (l2 : Level) (x : type-Large-Commutative-Ring l1) →
+    type-Large-Commutative-Ring (l1 ⊔ l2)
+  raise-Large-Commutative-Ring =
+    raise-Large-Ring large-ring-Large-Commutative-Ring
+
+  mul-Large-Commutative-Ring :
+    {l1 l2 : Level} →
+    type-Large-Commutative-Ring l1 →
+    type-Large-Commutative-Ring l2 →
+    type-Large-Commutative-Ring (l1 ⊔ l2)
+  mul-Large-Commutative-Ring = mul-Large-Ring large-ring-Large-Commutative-Ring
+
+  field
+    commutative-mul-Large-Commutative-Ring :
+      {l1 l2 : Level} →
+      (a : type-Large-Commutative-Ring l1) →
+      (b : type-Large-Commutative-Ring l2) →
+      mul-Large-Commutative-Ring a b ＝ mul-Large-Commutative-Ring b a
+
+open Large-Commutative-Ring public
+```
+
+## Properties
+
+### Small commutative rings from large commutative rings
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (R : Large-Commutative-Ring α β)
+  where
+
+  commutative-ring-Large-Commutative-Ring : (l : Level) → Commutative-Ring (α l)
+  commutative-ring-Large-Commutative-Ring l =
+    ( ring-Large-Ring (large-ring-Large-Commutative-Ring R) l ,
+      commutative-mul-Large-Commutative-Ring R)
+```
+
+### The multiplicative large commutative monoid of a large commutative ring
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (R : Large-Commutative-Ring α β)
+  where
+
+  multiplicative-large-commutative-monoid-Large-Commutative-Ring :
+    Large-Commutative-Monoid α β
+  multiplicative-large-commutative-monoid-Large-Commutative-Ring =
+    make-Large-Commutative-Monoid
+      ( multiplicative-large-monoid-Large-Ring
+        ( large-ring-Large-Commutative-Ring R))
+      ( commutative-mul-Large-Commutative-Ring R)
+```

src/group-theory/large-abelian-groups.lagda.md

@@ -12,6 +12,7 @@ open import foundation.dependent-pair-types
 open import foundation.embeddings
 open import foundation.identity-types
 open import foundation.large-binary-relations
+open import foundation.large-similarity-relations
 open import foundation.logical-equivalences
 open import foundation.sets
 open import foundation.universe-levels
@@ -77,6 +78,11 @@ module _
   {α : Level → Level} {β : Level → Level → Level} (G : Large-Ab α β)
   where
 
+  large-similarity-relation-Large-Ab :
+    Large-Similarity-Relation β (type-Large-Ab G)
+  large-similarity-relation-Large-Ab =
+    large-similarity-relation-Large-Group (large-group-Large-Ab G)
+
   sim-prop-Large-Ab : Large-Relation-Prop β (type-Large-Ab G)
   sim-prop-Large-Ab = sim-prop-Large-Group (large-group-Large-Ab G)
 
@@ -169,7 +175,37 @@ module _
     raise-unit-lzero-Large-Group (large-group-Large-Ab G)
 ```
 
-### The negative of the identity is the identity
+### Group properties of large abelian groups
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level} (G : Large-Ab α β)
+  where
+
+  associative-add-Large-Ab :
+    {l1 l2 l3 : Level} →
+    (a : type-Large-Ab G l1) →
+    (b : type-Large-Ab G l2) →
+    (c : type-Large-Ab G l3) →
+    add-Large-Ab G (add-Large-Ab G a b) c ＝
+    add-Large-Ab G a (add-Large-Ab G b c)
+  associative-add-Large-Ab =
+    associative-mul-Large-Group (large-group-Large-Ab G)
+
+  left-unit-law-add-Large-Ab :
+    {l : Level} (x : type-Large-Ab G l) →
+    add-Large-Ab G (zero-Large-Ab G) x ＝ x
+  left-unit-law-add-Large-Ab =
+    left-unit-law-mul-Large-Group (large-group-Large-Ab G)
+
+  right-unit-law-add-Large-Ab :
+    {l : Level} (x : type-Large-Ab G l) →
+    add-Large-Ab G x (zero-Large-Ab G) ＝ x
+  right-unit-law-add-Large-Ab =
+    right-unit-law-mul-Large-Group (large-group-Large-Ab G)
+```
+
+### The negation of the identity is the identity
 
 ```agda
 module _

src/group-theory/large-groups.lagda.md

@@ -15,6 +15,7 @@ open import foundation.equivalences
 open import foundation.identity-types
 open import foundation.involutions
 open import foundation.large-binary-relations
+open import foundation.large-similarity-relations
 open import foundation.logical-equivalences
 open import foundation.propositional-maps
 open import foundation.propositions
@@ -74,6 +75,11 @@ record Large-Group (α : Level → Level) (β : Level → Level → Level) : UU
   unit-Large-Group : type-Large-Group lzero
   unit-Large-Group = unit-Large-Monoid large-monoid-Large-Group
 
+  large-similarity-relation-Large-Group :
+    Large-Similarity-Relation β type-Large-Group
+  large-similarity-relation-Large-Group =
+    large-similarity-relation-Large-Monoid large-monoid-Large-Group
+
   sim-prop-Large-Group : Large-Relation-Prop β type-Large-Group
   sim-prop-Large-Group = sim-prop-Large-Monoid large-monoid-Large-Group
 

src/real-numbers.lagda.md

@@ -32,6 +32,9 @@ open import real-numbers.inhabited-finitely-enumerable-subsets-real-numbers publ
 open import real-numbers.inhabited-totally-bounded-subsets-real-numbers public
 open import real-numbers.isometry-addition-real-numbers public
 open import real-numbers.isometry-negation-real-numbers public
+open import real-numbers.large-additive-group-of-real-numbers public
+open import real-numbers.large-multiplicative-monoid-of-real-numbers public
+open import real-numbers.large-ring-of-real-numbers public
 open import real-numbers.limits-sequences-real-numbers public
 open import real-numbers.lipschitz-continuity-multiplication-real-numbers public
 open import real-numbers.lower-dedekind-real-numbers public

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

@@ -48,6 +48,7 @@ open import real-numbers.dedekind-real-numbers
 open import real-numbers.lower-dedekind-real-numbers
 open import real-numbers.negation-lower-upper-dedekind-real-numbers
 open import real-numbers.negation-real-numbers
+open import real-numbers.raising-universe-levels-real-numbers
 open import real-numbers.rational-real-numbers
 open import real-numbers.similarity-real-numbers
 open import real-numbers.upper-dedekind-real-numbers
@@ -256,6 +257,22 @@ abstract
       ( λ y → sim-ℝ y zero-ℝ)
       ( commutative-add-ℝ x (neg-ℝ x))
       ( right-inverse-law-add-ℝ x)
+
+  eq-right-inverse-law-add-ℝ :
+    {l : Level} (x : ℝ l) → x +ℝ neg-ℝ x ＝ raise-ℝ l zero-ℝ
+  eq-right-inverse-law-add-ℝ x =
+    eq-sim-ℝ
+      ( transitive-sim-ℝ _ _ _
+        ( sim-raise-ℝ _ zero-ℝ)
+        ( right-inverse-law-add-ℝ x))
+
+  eq-left-inverse-law-add-ℝ :
+    {l : Level} (x : ℝ l) → neg-ℝ x +ℝ x ＝ raise-ℝ l zero-ℝ
+  eq-left-inverse-law-add-ℝ x =
+    eq-sim-ℝ
+      ( transitive-sim-ℝ _ _ _
+        ( sim-raise-ℝ _ zero-ℝ)
+        ( left-inverse-law-add-ℝ x))
 ```
 
 ### Addition on the real numbers preserves similarity

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

@@ -0,0 +1,88 @@
+# The large additive group of Dedekind real numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module real-numbers.large-additive-group-of-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.universe-levels
+
+open import group-theory.abelian-groups
+open import group-theory.large-abelian-groups
+open import group-theory.large-commutative-monoids
+open import group-theory.large-groups
+open import group-theory.large-monoids
+open import group-theory.large-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.raising-universe-levels-real-numbers
+open import real-numbers.rational-real-numbers
+open import real-numbers.similarity-real-numbers
+```
+
+</details>
+
+## Idea
+
+The [Dedekind real numbers](real-numbers.dedekind-real-numbers.md) form a
+[large abelian group](group-theory.large-abelian-groups.md) under
+[addition](real-numbers.addition-real-numbers.md).
+
+## Definition
+
+```agda
+large-semigroup-add-ℝ : Large-Semigroup lsuc
+large-semigroup-add-ℝ =
+  make-Large-Semigroup
+    ( ℝ-Set)
+    ( add-ℝ)
+    ( associative-add-ℝ)
+
+large-monoid-add-ℝ : Large-Monoid lsuc (_⊔_)
+large-monoid-add-ℝ =
+  make-Large-Monoid
+    ( large-semigroup-add-ℝ)
+    ( large-similarity-relation-sim-ℝ)
+    ( raise-ℝ)
+    ( sim-raise-ℝ)
+    ( λ a b a~b c d c~d → preserves-sim-add-ℝ a~b c~d)
+    ( zero-ℝ)
+    ( left-unit-law-add-ℝ)
+    ( right-unit-law-add-ℝ)
+
+large-commutative-monoid-add-ℝ : Large-Commutative-Monoid lsuc (_⊔_)
+large-commutative-monoid-add-ℝ =
+  make-Large-Commutative-Monoid
+    ( large-monoid-add-ℝ)
+    ( commutative-add-ℝ)
+
+large-group-add-ℝ : Large-Group lsuc (_⊔_)
+large-group-add-ℝ =
+  make-Large-Group
+    ( large-monoid-add-ℝ)
+    ( neg-ℝ)
+    ( λ _ _ → preserves-sim-neg-ℝ)
+    ( eq-left-inverse-law-add-ℝ)
+    ( eq-right-inverse-law-add-ℝ)
+
+large-ab-add-ℝ : Large-Ab lsuc (_⊔_)
+large-ab-add-ℝ =
+  make-Large-Ab
+    ( large-group-add-ℝ)
+    ( commutative-add-ℝ)
+```
+
+## Properties
+
+### The small abelian group of real numbers at a universe level
+
+```agda
+ab-add-ℝ : (l : Level) → Ab (lsuc l)
+ab-add-ℝ = ab-Large-Ab large-ab-add-ℝ
+```