The large multiplicative monoid of Dedekind real numbers

Content created by Louis Wasserman.

Created on 2025-11-06.
Last modified on 2026-03-06.

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

module real-numbers.large-multiplicative-monoid-of-real-numbers where
Imports 
open import foundation.universe-levels

open import group-theory.commutative-monoids
open import group-theory.large-commutative-monoids
open import group-theory.large-monoids
open import group-theory.large-semigroups

open import real-numbers.dedekind-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 real-numbers.similarity-real-numbers

Idea

The Dedekind real numbers form a large commutative monoid under multiplication.

Definition

large-semigroup-mul-ℝ : Large-Semigroup lsuc (_⊔_)
large-semigroup-mul-ℝ =
  make-Large-Semigroup
    ( cumulative-large-set-ℝ)
    ( sim-preserving-binary-operator-mul-ℝ)
    ( associative-mul-ℝ)

large-monoid-mul-ℝ : Large-Monoid lsuc (_⊔_)
large-monoid-mul-ℝ =
  make-Large-Monoid
    ( large-semigroup-mul-ℝ)
    ( one-ℝ)
    ( left-unit-law-mul-ℝ)
    ( right-unit-law-mul-ℝ)

large-commutative-monoid-mul-ℝ : Large-Commutative-Monoid lsuc (_⊔_)
large-commutative-monoid-mul-ℝ =
  make-Large-Commutative-Monoid
    ( large-monoid-mul-ℝ)
    ( commutative-mul-ℝ)

Properties

The small commutative monoid of real numbers at a universe level

commutative-monoid-mul-ℝ : (l : Level) → Commutative-Monoid (lsuc l)
commutative-monoid-mul-ℝ =
  commutative-monoid-Large-Commutative-Monoid large-commutative-monoid-mul-ℝ

Recent changes