Similarity of complex numbers

Content created by Louis Wasserman.

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

module complex-numbers.similarity-complex-numbers where
Imports 
open import complex-numbers.complex-numbers

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

open import real-numbers.similarity-real-numbers

Idea

Two complex numbers are similar if their real and imaginary parts are similar.

Definition

sim-prop-ℂ : {l1 l2 : Level} → ℂ l1 → ℂ l2 → Prop (l1 ⊔ l2)
sim-prop-ℂ (a , b) (c , d) = sim-prop-ℝ a c ∧ sim-prop-ℝ b d

sim-ℂ : {l1 l2 : Level} → ℂ l1 → ℂ l2 → UU (l1 ⊔ l2)
sim-ℂ a+bi c+di = type-Prop (sim-prop-ℂ a+bi c+di)

Properties

Similarity is reflexive

abstract
  refl-sim-ℂ : {l : Level} (z : ℂ l) → sim-ℂ z z
  refl-sim-ℂ (a , b) = (refl-sim-ℝ a , refl-sim-ℝ b)

Similarity is symmetric

abstract
  symmetric-sim-ℂ :
    {l1 l2 : Level} {x : ℂ l1} {y : ℂ l2} → sim-ℂ x y → sim-ℂ y x
  symmetric-sim-ℂ (a~c , b~d) = (symmetric-sim-ℝ a~c , symmetric-sim-ℝ b~d)

Similarity is transitive

abstract
  transitive-sim-ℂ :
    {l1 l2 l3 : Level} (x : ℂ l1) (y : ℂ l2) (z : ℂ l3) →
    sim-ℂ y z → sim-ℂ x y → sim-ℂ x z
  transitive-sim-ℂ (a , b) (c , d) (e , f) (c~e , d~f) (a~c , b~d) =
    ( transitive-sim-ℝ a c e c~e a~c , transitive-sim-ℝ b d f d~f b~d)

Similarity characterizes equality at a universe level

abstract
  eq-sim-ℂ : {l : Level} {x y : ℂ l} → sim-ℂ x y → x ＝ y
  eq-sim-ℂ (a~c , b~d) = eq-ℂ (eq-sim-ℝ a~c) (eq-sim-ℝ b~d)

Recent changes