The large ring of Dedekind real numbers

Content created by Louis Wasserman.

Created on 2025-11-06.
Last modified on 2025-11-10.

{-# OPTIONS --lossy-unification #-}

module real-numbers.large-ring-of-real-numbers where
Imports 
open import commutative-algebra.commutative-rings
open import commutative-algebra.homomorphisms-commutative-rings
open import commutative-algebra.large-commutative-rings

open import elementary-number-theory.ring-of-rational-numbers

open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels

open import real-numbers.large-additive-group-of-real-numbers
open import real-numbers.multiplication-real-numbers
open import real-numbers.raising-universe-levels-real-numbers
open import real-numbers.rational-real-numbers

open import ring-theory.large-rings

Idea

The Dedekind real numbers form a large commutative ring under addition and multiplication.

Definition

large-ring-ℝ : Large-Ring lsuc (_⊔_)
large-ring-ℝ =
  make-Large-Ring
    ( large-ab-add-ℝ)
    ( mul-ℝ)
    ( λ _ _ a~a' _ _ → preserves-sim-mul-ℝ a~a')
    ( one-ℝ)
    ( associative-mul-ℝ)
    ( left-unit-law-mul-ℝ)
    ( right-unit-law-mul-ℝ)
    ( left-distributive-mul-add-ℝ)
    ( right-distributive-mul-add-ℝ)

large-commutative-ring-ℝ : Large-Commutative-Ring lsuc (_⊔_)
large-commutative-ring-ℝ =
  make-Large-Commutative-Ring
    ( large-ring-ℝ)
    ( commutative-mul-ℝ)

Properties

The small commutative ring of real numbers at a universe level

commutative-ring-ℝ : (l : Level) → Commutative-Ring (lsuc l)
commutative-ring-ℝ =
  commutative-ring-Large-Commutative-Ring large-commutative-ring-ℝ

The canonical embedding of rational numbers in the real numbers is a ring homomorphism

hom-ring-real-ℚ :
  hom-Commutative-Ring commutative-ring-ℚ (commutative-ring-ℝ lzero)
hom-ring-real-ℚ =
  ( hom-ab-add-real-ℚ , inv (mul-real-ℚ _ _) , eq-raise-ℝ _)

Raising the universe level of real numbers is a ring homomorphism

hom-ring-raise-ℝ :
  (l1 l2 : Level) →
  hom-Commutative-Ring (commutative-ring-ℝ l1) (commutative-ring-ℝ (l1 ⊔ l2))
hom-ring-raise-ℝ = hom-raise-Large-Commutative-Ring large-commutative-ring-ℝ

Recent changes