Conjugation of complex numbers

Content created by Louis Wasserman.

Created on 2025-11-16.
Last modified on 2026-01-11.

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

open import foundation.action-on-identifications-functions
open import foundation.identity-types
open import foundation.universe-levels

open import real-numbers.dedekind-real-numbers
open import real-numbers.negation-real-numbers
open import real-numbers.raising-universe-levels-real-numbers

Idea

The conjugate of a complex number a + bi is a - bi.

Definition

conjugate-ℂ : {l : Level} → ℂ l → ℂ l
conjugate-ℂ (a +iℂ b) = a +iℂ neg-ℝ b

Properties

Conjugation is an involution

abstract
  is-involution-conjugate-ℂ :
    {l : Level} (z : ℂ l) → conjugate-ℂ (conjugate-ℂ z) ＝ z
  is-involution-conjugate-ℂ (a +iℂ b) = eq-ℂ refl (neg-neg-ℝ b)

Conjugating raised complex numbers

abstract
  conjugate-raise-ℂ :
    {l0 : Level} (l : Level) (z : ℂ l0) →
    conjugate-ℂ (raise-ℂ l z) ＝ raise-ℂ l (conjugate-ℂ z)
  conjugate-raise-ℂ l (a +iℂ b) = eq-ℂ refl (neg-raise-ℝ l b)

The conjugate of one-ℂ is one-ℂ

abstract
  conjugate-one-ℂ : conjugate-ℂ one-ℂ ＝ one-ℂ
  conjugate-one-ℂ = eq-ℂ refl neg-zero-ℝ

The conjugate of complex-ℝ x is complex-ℝ x

abstract
  conjugate-complex-ℝ :
    {l : Level} (x : ℝ l) → conjugate-ℂ (complex-ℝ x) ＝ complex-ℝ x
  conjugate-complex-ℝ {l} x =
    eq-ℂ refl (neg-raise-ℝ _ _ ∙ ap (raise-ℝ l) neg-zero-ℝ)

Recent changes