Complex vector spaces (#1692)

Builds on #1688, #1689, and #1684.

Author: lowasser

src/complex-numbers.lagda.md

@@ -4,13 +4,16 @@
 module complex-numbers where
 
 open import complex-numbers.addition-complex-numbers public
+open import complex-numbers.addition-nonzero-complex-numbers public
 open import complex-numbers.apartness-complex-numbers public
 open import complex-numbers.complex-numbers public
 open import complex-numbers.conjugation-complex-numbers public
 open import complex-numbers.eisenstein-integers public
+open import complex-numbers.field-of-complex-numbers public
 open import complex-numbers.gaussian-integers public
 open import complex-numbers.large-additive-group-of-complex-numbers public
 open import complex-numbers.large-ring-of-complex-numbers public
+open import complex-numbers.local-ring-of-complex-numbers public
 open import complex-numbers.magnitude-complex-numbers public
 open import complex-numbers.multiplication-complex-numbers public
 open import complex-numbers.multiplicative-inverses-nonzero-complex-numbers public

src/complex-numbers/addition-nonzero-complex-numbers.lagda.md

@@ -0,0 +1,53 @@
+# Addition of nonzero complex numbers
+
+```agda
+module complex-numbers.addition-nonzero-complex-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import complex-numbers.addition-complex-numbers
+open import complex-numbers.complex-numbers
+open import complex-numbers.nonzero-complex-numbers
+
+open import foundation.disjunction
+open import foundation.functoriality-disjunction
+open import foundation.universe-levels
+
+open import real-numbers.addition-nonzero-real-numbers
+open import real-numbers.nonzero-real-numbers
+```
+
+</details>
+
+## Idea
+
+This file describes properties of
+[addition](complex-numbers.addition-complex-numbers.md) of
+[nonzero](complex-numbers.nonzero-complex-numbers.md)
+[complex numbers](complex-numbers.complex-numbers.md).
+
+## Properties
+
+### If the sum of two complex numbers is nonzero, one of them is nonzero
+
+```agda
+abstract
+  is-nonzero-either-is-nonzero-add-ℂ :
+    {l1 l2 : Level} (z : ℂ l1) (w : ℂ l2) → is-nonzero-ℂ (z +ℂ w) →
+    disjunction-type (is-nonzero-ℂ z) (is-nonzero-ℂ w)
+  is-nonzero-either-is-nonzero-add-ℂ z@(a +iℂ b) w@(c +iℂ d) =
+    elim-disjunction
+      ( is-nonzero-prop-ℂ z ∨ is-nonzero-prop-ℂ w)
+      ( λ a+c≠0 →
+        map-disjunction
+          ( inl-disjunction)
+          ( inl-disjunction)
+          ( is-nonzero-either-is-nonzero-add-ℝ a c a+c≠0))
+      ( λ b+d≠0 →
+        map-disjunction
+          ( inr-disjunction)
+          ( inr-disjunction)
+          ( is-nonzero-either-is-nonzero-add-ℝ b d b+d≠0))
+```

src/complex-numbers/apartness-complex-numbers.lagda.md

@@ -8,7 +8,9 @@ module complex-numbers.apartness-complex-numbers where
 
 ```agda
 open import complex-numbers.complex-numbers
+open import complex-numbers.similarity-complex-numbers
 
+open import foundation.apartness-relations
 open import foundation.dependent-pair-types
 open import foundation.disjunction
 open import foundation.empty-types
@@ -17,6 +19,7 @@ open import foundation.functoriality-disjunction
 open import foundation.large-apartness-relations
 open import foundation.negation
 open import foundation.propositions
+open import foundation.tight-apartness-relations
 open import foundation.universe-levels
 
 open import real-numbers.apartness-real-numbers
@@ -100,3 +103,42 @@ symmetric-Large-Apartness-Relation large-apartness-relation-ℂ =
 cotransitive-Large-Apartness-Relation large-apartness-relation-ℂ =
   cotransitive-apart-ℂ
 ```
+
+### The apartness relation of complex numbers at a particular universe level
+
+```agda
+apartness-relation-ℂ : (l : Level) → Apartness-Relation l (ℂ l)
+apartness-relation-ℂ l =
+  apartness-relation-Large-Apartness-Relation large-apartness-relation-ℂ l
+```
+
+### If two complex numbers at the same universe level are not apart, they are equal
+
+```agda
+abstract
+  is-tight-apartness-relation-ℂ :
+    (l : Level) → is-tight-Apartness-Relation (apartness-relation-ℂ l)
+  is-tight-apartness-relation-ℂ l (a +iℂ b) (c +iℂ d) ¬a+ib#c+id =
+    eq-ℂ
+      ( is-tight-apartness-relation-ℝ l a c (¬a+ib#c+id ∘ inl-disjunction))
+      ( is-tight-apartness-relation-ℝ l b d (¬a+ib#c+id ∘ inr-disjunction))
+
+tight-apartness-relation-ℂ : (l : Level) → Tight-Apartness-Relation l (ℂ l)
+tight-apartness-relation-ℂ l =
+  ( apartness-relation-ℂ l ,
+    is-tight-apartness-relation-ℂ l)
+```
+
+### Apartness is preserved by similarity
+
+```agda
+abstract
+  apart-right-sim-ℂ :
+    {l1 l2 l3 : Level} →
+    (z : ℂ l1) (x : ℂ l2) (y : ℂ l3) →
+    sim-ℂ x y → apart-ℂ z x → apart-ℂ z y
+  apart-right-sim-ℂ (a +iℂ b) (c +iℂ d) (e +iℂ f) (c~e , d~f) =
+    map-disjunction
+      ( apart-right-sim-ℝ a c e c~e)
+      ( apart-right-sim-ℝ b d f d~f)
+```

src/complex-numbers/complex-numbers.lagda.md

@@ -14,6 +14,7 @@ open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.equality-cartesian-product-types
 open import foundation.identity-types
+open import foundation.negated-equality
 open import foundation.sets
 open import foundation.universe-levels
 
@@ -99,6 +100,14 @@ i-ℂ : ℂ lzero
 i-ℂ = (zero-ℝ , one-ℝ)
 ```
 
+### `0 ≠ 1` in the complex numbers
+
+```agda
+abstract
+  neq-zero-one-ℂ : zero-ℂ ≠ one-ℂ
+  neq-zero-one-ℂ 0=1ℂ = neq-zero-one-ℝ (ap re-ℂ 0=1ℂ)
+```
+
 ### Negation of complex numbers
 
 ```agda

src/complex-numbers/field-of-complex-numbers.lagda.md

@@ -0,0 +1,65 @@
+# The field of complex numbers
+
+```agda
+module complex-numbers.field-of-complex-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.heyting-fields
+open import commutative-algebra.invertible-elements-commutative-rings
+
+open import complex-numbers.apartness-complex-numbers
+open import complex-numbers.complex-numbers
+open import complex-numbers.large-ring-of-complex-numbers
+open import complex-numbers.local-ring-of-complex-numbers
+open import complex-numbers.multiplicative-inverses-nonzero-complex-numbers
+open import complex-numbers.raising-universe-levels-complex-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.negation
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+The [complex numbers](complex-numbers.complex-numbers.md) form a
+[Heyting field](commutative-algebra.heyting-fields.md).
+
+## Definition
+
+```agda
+abstract
+  is-zero-is-noninvertible-commutative-ring-ℂ :
+    (l : Level) (z : ℂ l) →
+    ¬ (is-invertible-element-Commutative-Ring (commutative-ring-ℂ l) z) →
+    z ＝ raise-ℂ l zero-ℂ
+  is-zero-is-noninvertible-commutative-ring-ℂ l z ¬inv-z =
+    is-tight-apartness-relation-ℂ l z (raise-ℂ l zero-ℂ)
+      ( λ z#0 →
+        ¬inv-z
+          ( is-invertible-is-nonzero-ℂ
+            ( z)
+            ( apart-right-sim-ℂ
+              ( z)
+              ( raise-ℂ l zero-ℂ)
+              ( zero-ℂ)
+              ( sim-raise-ℂ' l zero-ℂ)
+              ( z#0))))
+
+is-heyting-field-local-commutative-ring-ℂ :
+  (l : Level) →
+  is-heyting-field-Local-Commutative-Ring (local-commutative-ring-ℂ l)
+is-heyting-field-local-commutative-ring-ℂ l =
+  ( neq-raise-zero-one-ℂ l ,
+    is-zero-is-noninvertible-commutative-ring-ℂ l)
+
+heyting-field-ℂ : (l : Level) → Heyting-Field (lsuc l)
+heyting-field-ℂ l =
+  ( local-commutative-ring-ℂ l ,
+    is-heyting-field-local-commutative-ring-ℂ l)
+```

src/complex-numbers/local-ring-of-complex-numbers.lagda.md

@@ -0,0 +1,50 @@
+# The local ring of complex numbers
+
+```agda
+module complex-numbers.local-ring-of-complex-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.local-commutative-rings
+
+open import complex-numbers.addition-complex-numbers
+open import complex-numbers.addition-nonzero-complex-numbers
+open import complex-numbers.large-ring-of-complex-numbers
+open import complex-numbers.multiplicative-inverses-nonzero-complex-numbers
+open import complex-numbers.nonzero-complex-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.functoriality-disjunction
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+The
+[commutative ring of complex numbers](complex-numbers.large-ring-of-complex-numbers.md)
+is [local](commutative-algebra.local-commutative-rings.md).
+
+## Definition
+
+```agda
+is-local-commutative-ring-ℂ :
+  (l : Level) → is-local-Commutative-Ring (commutative-ring-ℂ l)
+is-local-commutative-ring-ℂ l z w is-invertible-z+w =
+  map-disjunction
+    ( is-invertible-is-nonzero-ℂ z)
+    ( is-invertible-is-nonzero-ℂ w)
+    ( is-nonzero-either-is-nonzero-add-ℂ
+      ( z)
+      ( w)
+      ( is-nonzero-is-invertible-ℂ
+        ( z +ℂ w)
+        ( is-invertible-z+w)))
+
+local-commutative-ring-ℂ : (l : Level) → Local-Commutative-Ring (lsuc l)
+local-commutative-ring-ℂ l =
+  ( commutative-ring-ℂ l , is-local-commutative-ring-ℂ l)
+```

src/complex-numbers/magnitude-complex-numbers.lagda.md

@@ -12,11 +12,14 @@ module complex-numbers.magnitude-complex-numbers where
 open import complex-numbers.complex-numbers
 open import complex-numbers.conjugation-complex-numbers
 open import complex-numbers.multiplication-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.identity-types
 open import foundation.universe-levels
 
+open import real-numbers.absolute-value-real-numbers
 open import real-numbers.addition-nonnegative-real-numbers
 open import real-numbers.addition-real-numbers
 open import real-numbers.dedekind-real-numbers
@@ -25,6 +28,7 @@ open import real-numbers.multiplication-nonnegative-real-numbers
 open import real-numbers.multiplication-real-numbers
 open import real-numbers.negation-real-numbers
 open import real-numbers.nonnegative-real-numbers
+open import real-numbers.positive-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
@@ -225,3 +229,67 @@ abstract
       ＝ magnitude-ℂ z *ℝ magnitude-ℂ w
         by ap real-ℝ⁰⁺ (distributive-sqrt-mul-ℝ⁰⁺ _ _)
 ```
+
+### The magnitude of a real number as a complex number is its absolute value
+
+```agda
+abstract
+  magnitude-complex-ℝ :
+    {l : Level} (x : ℝ l) → magnitude-ℂ (complex-ℝ x) ＝ abs-ℝ x
+  magnitude-complex-ℝ {l} x =
+    equational-reasoning
+      real-sqrt-ℝ⁰⁺
+        ( nonnegative-square-ℝ x +ℝ⁰⁺ nonnegative-square-ℝ (raise-ℝ l zero-ℝ))
+      ＝
+        real-sqrt-ℝ⁰⁺
+          ( nonnegative-square-ℝ x +ℝ⁰⁺ nonnegative-square-ℝ zero-ℝ)
+        by
+          ap
+            ( real-sqrt-ℝ⁰⁺)
+            ( eq-ℝ⁰⁺ _ _
+              ( eq-sim-ℝ
+                ( preserves-sim-left-add-ℝ _ _ _
+                  ( preserves-sim-square-ℝ
+                    ( symmetric-sim-ℝ (sim-raise-ℝ l zero-ℝ))))))
+      ＝ real-sqrt-ℝ⁰⁺ (nonnegative-square-ℝ x +ℝ⁰⁺ zero-ℝ⁰⁺)
+        by ap real-sqrt-ℝ⁰⁺ (eq-ℝ⁰⁺ _ _ (ap-add-ℝ refl square-zero-ℝ))
+      ＝ real-sqrt-ℝ⁰⁺ (nonnegative-square-ℝ x)
+        by ap real-sqrt-ℝ⁰⁺ (eq-ℝ⁰⁺ _ _ (right-unit-law-add-ℝ _))
+      ＝ abs-ℝ x
+        by inv (eq-abs-sqrt-square-ℝ x)
+```
+
+### Similar complex numbers have similar magnitudes
+
+```agda
+abstract
+  preserves-sim-squared-magnitude-ℂ :
+    {l1 l2 : Level} {z : ℂ l1} {w : ℂ l2} →
+    sim-ℂ z w → sim-ℝ (squared-magnitude-ℂ z) (squared-magnitude-ℂ w)
+  preserves-sim-squared-magnitude-ℂ (a~c , b~d) =
+    preserves-sim-add-ℝ
+      ( preserves-sim-square-ℝ a~c)
+      ( preserves-sim-square-ℝ b~d)
+
+  preserves-sim-magnitude-ℂ :
+    {l1 l2 : Level} {z : ℂ l1} {w : ℂ l2} →
+    sim-ℂ z w → sim-ℝ (magnitude-ℂ z) (magnitude-ℂ w)
+  preserves-sim-magnitude-ℂ z~w =
+    preserves-sim-sqrt-ℝ⁰⁺ _ _ (preserves-sim-squared-magnitude-ℂ z~w)
+```
+
+### The magnitude of `one-ℂ` is `one-ℝ`
+
+```agda
+abstract
+  magnitude-one-ℂ : magnitude-ℂ one-ℂ ＝ one-ℝ
+  magnitude-one-ℂ =
+    equational-reasoning
+      magnitude-ℂ one-ℂ
+      ＝ magnitude-ℂ (complex-ℝ one-ℝ)
+        by ap magnitude-ℂ (inv eq-complex-one-ℝ)
+      ＝ abs-ℝ one-ℝ
+        by magnitude-complex-ℝ one-ℝ
+      ＝ one-ℝ
+        by abs-real-ℝ⁺ one-ℝ⁺
+```