Raising the universe level of complex numbers

Content created by Louis Wasserman.

Created on 2025-11-11.
Last modified on 2025-11-26.

module complex-numbers.raising-universe-levels-complex-numbers where
Imports 
open import complex-numbers.complex-numbers
open import complex-numbers.similarity-complex-numbers

open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.negated-equality
open import foundation.universe-levels

open import real-numbers.raising-universe-levels-real-numbers
open import real-numbers.rational-real-numbers

Idea

For every universe 𝒰 there is a type of complex numbers ℂ relative to 𝒰, ℂ 𝒰. Given a larger universe 𝒱, then we may raise a complex number z from the universe 𝒰 to a similar complex number in the universe 𝒱.

Definition

raise-ℂ : {l1 : Level} (l2 : Level) → ℂ l1 → ℂ (l1 ⊔ l2)
raise-ℂ l (a +iℂ b) = raise-ℝ l a +iℂ raise-ℝ l b

Properties

Complex numbers are similar to their raised-universe equivalents

abstract
  sim-raise-ℂ : {l1 : Level} (l2 : Level) (z : ℂ l1) → sim-ℂ z (raise-ℂ l2 z)
  sim-raise-ℂ l (a +iℂ b) = ( sim-raise-ℝ l a , sim-raise-ℝ l b)

abstract
  sim-raise-ℂ' : {l1 : Level} (l2 : Level) (z : ℂ l1) → sim-ℂ (raise-ℂ l2 z) z
  sim-raise-ℂ' l2 z = symmetric-sim-ℂ (sim-raise-ℂ l2 z)

raise-ℂ l zero-ℂ ≠ raise-ℂ l one-ℂ

abstract
  neq-raise-zero-one-ℂ : (l : Level) → raise-ℂ l zero-ℂ ≠ raise-ℂ l one-ℂ
  neq-raise-zero-one-ℂ l 0=1ℂ = neq-raise-zero-one-ℝ l (ap re-ℂ 0=1ℂ)

Recent changes