Complex vector spaces

src/commutative-algebra/local-commutative-rings.lagda.md

@@ -66,4 +66,24 @@ module _
   is-local-commutative-ring-Local-Commutative-Ring :
     is-local-Commutative-Ring commutative-ring-Local-Commutative-Ring
   is-local-commutative-ring-Local-Commutative-Ring = pr2 A
+
+  zero-Local-Commutative-Ring : type-Local-Commutative-Ring
+  zero-Local-Commutative-Ring = zero-Ring ring-Local-Commutative-Ring
+
+  one-Local-Commutative-Ring : type-Local-Commutative-Ring
+  one-Local-Commutative-Ring = one-Ring ring-Local-Commutative-Ring
+
+  add-Local-Commutative-Ring :
+    type-Local-Commutative-Ring → type-Local-Commutative-Ring →
+    type-Local-Commutative-Ring
+  add-Local-Commutative-Ring = add-Ring ring-Local-Commutative-Ring
+
+  mul-Local-Commutative-Ring :
+    type-Local-Commutative-Ring → type-Local-Commutative-Ring →
+    type-Local-Commutative-Ring
+  mul-Local-Commutative-Ring = mul-Ring ring-Local-Commutative-Ring
+
+  neg-Local-Commutative-Ring :
+    type-Local-Commutative-Ring → type-Local-Commutative-Ring
+  neg-Local-Commutative-Ring = neg-Ring ring-Local-Commutative-Ring
 ```

src/complex-numbers.lagda.md

@@ -4,13 +4,15 @@
 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.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/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-ℝ⁺
+```

src/complex-numbers/multiplicative-inverses-nonzero-complex-numbers.lagda.md

@@ -7,21 +7,34 @@ module complex-numbers.multiplicative-inverses-nonzero-complex-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import commutative-algebra.invertible-elements-commutative-rings
+
 open import complex-numbers.complex-numbers
 open import complex-numbers.conjugation-complex-numbers
+open import complex-numbers.large-ring-of-complex-numbers
 open import complex-numbers.magnitude-complex-numbers
 open import complex-numbers.multiplication-complex-numbers
 open import complex-numbers.nonzero-complex-numbers
+open import complex-numbers.raising-universe-levels-complex-numbers
 open import complex-numbers.similarity-complex-numbers
 
 open import foundation.dependent-pair-types
+open import foundation.disjunction
+open import foundation.empty-types
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
+open import real-numbers.multiplication-nonzero-real-numbers
 open import real-numbers.multiplication-real-numbers
 open import real-numbers.multiplicative-inverses-positive-real-numbers
+open import real-numbers.nonnegative-real-numbers
+open import real-numbers.nonzero-real-numbers
+open import real-numbers.positive-and-negative-real-numbers
+open import real-numbers.positive-real-numbers
 open import real-numbers.rational-real-numbers
+open import real-numbers.similarity-real-numbers
 ```
 
 </details>
@@ -86,3 +99,99 @@ abstract
       ( commutative-mul-ℂ _ _)
       ( right-inverse-law-mul-nonzero-ℂ z)
 ```
+
+### If a complex number has a multiplicative inverse, it is nonzero
+
+```agda
+abstract
+  is-nonzero-has-right-inverse-mul-ℂ :
+    {l1 l2 : Level} (z : ℂ l1) (w : ℂ l2) → sim-ℂ (z *ℂ w) one-ℂ →
+    is-nonzero-ℂ z
+  is-nonzero-has-right-inverse-mul-ℂ z w zw=1 =
+    is-nonzero-is-positive-magnitude-ℂ
+      ( z)
+      ( elim-disjunction
+        ( is-positive-prop-ℝ (magnitude-ℂ z))
+        ( λ |z|<0 →
+          ex-falso
+            ( is-not-negative-and-nonnegative-ℝ
+              ( |z|<0 , is-nonnegative-real-ℝ⁰⁺ (nonnegative-magnitude-ℂ z))))
+        ( id)
+        ( pr1
+          ( is-nonzero-factors-is-nonzero-mul-ℝ
+            ( (magnitude-ℂ z))
+            ( (magnitude-ℂ w))
+            ( is-nonzero-sim-ℝ
+              ( symmetric-sim-ℝ
+                ( similarity-reasoning-ℝ
+                  (magnitude-ℂ z) *ℝ (magnitude-ℂ w)
+                  ~ℝ magnitude-ℂ (z *ℂ w)
+                    by sim-eq-ℝ (inv (distributive-magnitude-mul-ℂ z w))
+                  ~ℝ magnitude-ℂ one-ℂ
+                    by preserves-sim-magnitude-ℂ zw=1
+                  ~ℝ one-ℝ
+                    by sim-eq-ℝ magnitude-one-ℂ))
+              ( is-nonzero-is-positive-ℝ is-positive-one-ℝ)))))
+
+  is-nonzero-has-left-inverse-mul-ℂ :
+    {l1 l2 : Level} (z : ℂ l1) (w : ℂ l2) → sim-ℂ (z *ℂ w) one-ℂ →
+    is-nonzero-ℂ w
+  is-nonzero-has-left-inverse-mul-ℂ z w zw=1 =
+    is-nonzero-has-right-inverse-mul-ℂ
+      ( w)
+      ( z)
+      ( tr (λ x → sim-ℂ x one-ℂ) (commutative-mul-ℂ z w) zw=1)
+```
+
+### The multiplicative inverse of a nonzero complex number is nonzero
+
+```agda
+abstract
+  is-nonzero-complex-inv-nonzero-ℂ :
+    {l : Level} (z : nonzero-ℂ l) → is-nonzero-ℂ (complex-inv-nonzero-ℂ z)
+  is-nonzero-complex-inv-nonzero-ℂ z =
+    is-nonzero-has-left-inverse-mul-ℂ
+      ( _)
+      ( _)
+      ( right-inverse-law-mul-nonzero-ℂ z)
+
+inv-nonzero-ℂ : {l : Level} → nonzero-ℂ l → nonzero-ℂ l
+inv-nonzero-ℂ z = (complex-inv-nonzero-ℂ z , is-nonzero-complex-inv-nonzero-ℂ z)
+```
+
+### A complex number is invertible if and only if it is nonzero
+
+```agda
+abstract
+  is-nonzero-is-invertible-ℂ :
+    {l : Level} (z : ℂ l) →
+    is-invertible-element-Commutative-Ring (commutative-ring-ℂ l) z →
+    is-nonzero-ℂ z
+  is-nonzero-is-invertible-ℂ z (w , zw=1 , _) =
+    is-nonzero-has-right-inverse-mul-ℂ
+      ( z)
+      ( w)
+      ( transitive-sim-ℂ _ _ _
+        ( symmetric-sim-ℂ (sim-raise-ℂ _ one-ℂ))
+        ( sim-eq-ℂ zw=1))
+
+  is-invertible-is-nonzero-ℂ :
+    {l : Level} (z : ℂ l) → is-nonzero-ℂ z →
+    is-invertible-element-Commutative-Ring (commutative-ring-ℂ l) z
+  is-invertible-is-nonzero-ℂ z z≠0 =
+    ( complex-inv-nonzero-ℂ (z , z≠0) ,
+      eq-sim-ℂ
+        ( similarity-reasoning-ℂ
+          z *ℂ complex-inv-nonzero-ℂ (z , z≠0)
+          ~ℂ one-ℂ
+            by right-inverse-law-mul-nonzero-ℂ (z , z≠0)
+          ~ℂ raise-ℂ _ one-ℂ
+            by sim-raise-ℂ _ one-ℂ) ,
+      eq-sim-ℂ
+        ( similarity-reasoning-ℂ
+          complex-inv-nonzero-ℂ (z , z≠0) *ℂ z
+          ~ℂ one-ℂ
+            by left-inverse-law-mul-nonzero-ℂ (z , z≠0)
+          ~ℂ raise-ℂ _ one-ℂ
+            by sim-raise-ℂ _ one-ℂ))
+```