Normed complex vector spaces

Content created by Louis Wasserman.

Created on 2026-03-22.
Last modified on 2026-03-22.

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

module linear-algebra.normed-complex-vector-spaces where
Imports 
open import complex-numbers.complex-numbers
open import complex-numbers.magnitude-complex-numbers

open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.propositions
open import foundation.subtypes
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import group-theory.abelian-groups

open import linear-algebra.complex-vector-spaces
open import linear-algebra.normed-real-vector-spaces
open import linear-algebra.seminormed-complex-vector-spaces

open import metric-spaces.equality-of-metric-spaces
open import metric-spaces.metric-spaces

open import real-numbers.dedekind-real-numbers
open import real-numbers.inequality-real-numbers
open import real-numbers.rational-real-numbers
open import real-numbers.zero-real-numbers

Idea

A norm on a complex vector space V is a seminorm p on V that is extensional: if p(v) = 0, then v is the zero vector.

A complex vector space equipped with such a norm is called a normed vector space.

A norm on a complex vector space induces a located metric space on the vector space, defined by the neighborhood relation that v and w are in an ε-neighborhood of each other if p(v - w) ≤ ε.

Definition

module _
  {l1 l2 : Level} (V : ℂ-Vector-Space l1 l2) (p : seminorm-ℂ-Vector-Space V)
  where

  is-norm-prop-seminorm-ℂ-Vector-Space : Prop (l1 ⊔ l2)
  is-norm-prop-seminorm-ℂ-Vector-Space =
    Π-Prop
      ( type-ℂ-Vector-Space V)
      ( λ v →
        hom-Prop
          ( is-zero-prop-ℝ (pr1 p v))
          ( is-zero-prop-ℂ-Vector-Space V v))

  is-norm-seminorm-ℂ-Vector-Space : UU (l1 ⊔ l2)
  is-norm-seminorm-ℂ-Vector-Space =
    type-Prop is-norm-prop-seminorm-ℂ-Vector-Space

norm-ℂ-Vector-Space : {l1 l2 : Level} → ℂ-Vector-Space l1 l2 → UU (lsuc l1 ⊔ l2)
norm-ℂ-Vector-Space V = type-subtype (is-norm-prop-seminorm-ℂ-Vector-Space V)

Normed-ℂ-Vector-Space : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
Normed-ℂ-Vector-Space l1 l2 = Σ (ℂ-Vector-Space l1 l2) norm-ℂ-Vector-Space

module _
  {l1 l2 : Level}
  (V : Normed-ℂ-Vector-Space l1 l2)
  where

  vector-space-Normed-ℂ-Vector-Space : ℂ-Vector-Space l1 l2
  vector-space-Normed-ℂ-Vector-Space = pr1 V

  norm-Normed-ℂ-Vector-Space :
    norm-ℂ-Vector-Space vector-space-Normed-ℂ-Vector-Space
  norm-Normed-ℂ-Vector-Space = pr2 V

  seminorm-Normed-ℂ-Vector-Space :
    seminorm-ℂ-Vector-Space vector-space-Normed-ℂ-Vector-Space
  seminorm-Normed-ℂ-Vector-Space = pr1 norm-Normed-ℂ-Vector-Space

  seminormed-vector-space-Normed-ℂ-Vector-Space :
    Seminormed-ℂ-Vector-Space l1 l2
  seminormed-vector-space-Normed-ℂ-Vector-Space =
    ( vector-space-Normed-ℂ-Vector-Space , seminorm-Normed-ℂ-Vector-Space)

  type-Normed-ℂ-Vector-Space : UU l2
  type-Normed-ℂ-Vector-Space =
    type-ℂ-Vector-Space vector-space-Normed-ℂ-Vector-Space

  ab-Normed-ℂ-Vector-Space : Ab l2
  ab-Normed-ℂ-Vector-Space =
    ab-ℂ-Vector-Space vector-space-Normed-ℂ-Vector-Space

  zero-Normed-ℂ-Vector-Space : type-Normed-ℂ-Vector-Space
  zero-Normed-ℂ-Vector-Space = zero-Ab ab-Normed-ℂ-Vector-Space

  add-Normed-ℂ-Vector-Space :
    type-Normed-ℂ-Vector-Space → type-Normed-ℂ-Vector-Space →
    type-Normed-ℂ-Vector-Space
  add-Normed-ℂ-Vector-Space = add-Ab ab-Normed-ℂ-Vector-Space

  neg-Normed-ℂ-Vector-Space :
    type-Normed-ℂ-Vector-Space → type-Normed-ℂ-Vector-Space
  neg-Normed-ℂ-Vector-Space = neg-Ab ab-Normed-ℂ-Vector-Space

  diff-Normed-ℂ-Vector-Space :
    type-Normed-ℂ-Vector-Space → type-Normed-ℂ-Vector-Space →
    type-Normed-ℂ-Vector-Space
  diff-Normed-ℂ-Vector-Space = right-subtraction-Ab ab-Normed-ℂ-Vector-Space

  mul-Normed-ℂ-Vector-Space :
    ℂ l1 → type-Normed-ℂ-Vector-Space → type-Normed-ℂ-Vector-Space
  mul-Normed-ℂ-Vector-Space =
    mul-ℂ-Vector-Space vector-space-Normed-ℂ-Vector-Space

Properties

A normed complex vector space is a normed real vector space

normed-real-vector-space-Normed-ℂ-Vector-Space :
  {l1 l2 : Level} → Normed-ℂ-Vector-Space l1 l2 → Normed-ℝ-Vector-Space l1 l2
normed-real-vector-space-Normed-ℂ-Vector-Space (V , (p , S) , H) =
  ( real-vector-space-ℂ-Vector-Space V ,
    ( p , is-seminorm-real-ℂ-Vector-Space V p S) ,
    H)

The metric space of a normed complex vector space

metric-space-Normed-ℂ-Vector-Space :
  {l1 l2 : Level} → Normed-ℂ-Vector-Space l1 l2 → Metric-Space l2 l1
metric-space-Normed-ℂ-Vector-Space V =
  metric-space-Normed-ℝ-Vector-Space
    ( normed-real-vector-space-Normed-ℂ-Vector-Space V)

Recent changes