Multiplicative inverses of nonzero complex numbers (#1684)

Builds on #1679.

Author: lowasser

src/complex-numbers.lagda.md

@@ -4,12 +4,17 @@
 module complex-numbers where
 
 open import complex-numbers.addition-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.magnitude-complex-numbers public
 open import complex-numbers.multiplication-complex-numbers public
+open import complex-numbers.multiplicative-inverses-nonzero-complex-numbers public
+open import complex-numbers.nonzero-complex-numbers public
 open import complex-numbers.raising-universe-levels-complex-numbers public
 open import complex-numbers.similarity-complex-numbers public
 ```

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

@@ -0,0 +1,102 @@
+# Apartness of complex numbers
+
+```agda
+module complex-numbers.apartness-complex-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import complex-numbers.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.functoriality-disjunction
+open import foundation.large-apartness-relations
+open import foundation.negation
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import real-numbers.apartness-real-numbers
+```
+
+</details>
+
+## Idea
+
+Two [complex numbers](complex-numbers.complex-numbers.md) are
+{{#concept "apart" Disambiguation="complex numbers" Agda=apart-ℂ}} if their
+[real](real-numbers.dedekind-real-numbers.md) parts are
+[apart](real-numbers.apartness-real-numbers.md) [or](foundation.disjunction.md)
+their imaginary parts are [apart].
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level} (z : ℂ l1) (w : ℂ l2)
+  where
+
+  apart-prop-ℂ : Prop (l1 ⊔ l2)
+  apart-prop-ℂ =
+    (apart-prop-ℝ (re-ℂ z) (re-ℂ w)) ∨ (apart-prop-ℝ (im-ℂ z) (im-ℂ w))
+
+  apart-ℂ : UU (l1 ⊔ l2)
+  apart-ℂ = type-Prop apart-prop-ℂ
+```
+
+## Properties
+
+### Apartness is antireflexive
+
+```agda
+abstract
+  antireflexive-apart-ℂ : {l : Level} (z : ℂ l) → ¬ (apart-ℂ z z)
+  antireflexive-apart-ℂ (a , b) =
+    elim-disjunction
+      ( empty-Prop)
+      ( antireflexive-apart-ℝ a)
+      ( antireflexive-apart-ℝ b)
+```
+
+### Apartness is symmetric
+
+```agda
+abstract
+  symmetric-apart-ℂ :
+    {l1 l2 : Level} (z : ℂ l1) (w : ℂ l2) → apart-ℂ z w → apart-ℂ w z
+  symmetric-apart-ℂ (a , b) (c , d) =
+    map-disjunction symmetric-apart-ℝ symmetric-apart-ℝ
+```
+
+### Apartness is cotransitive
+
+```agda
+abstract
+  cotransitive-apart-ℂ :
+    {l1 l2 l3 : Level} (x : ℂ l1) (y : ℂ l2) (z : ℂ l3) →
+    apart-ℂ x y → disjunction-type (apart-ℂ x z) (apart-ℂ z y)
+  cotransitive-apart-ℂ x@(a , b) y@(c , d) z@(e , f) =
+    elim-disjunction
+      ( (apart-prop-ℂ x z) ∨ (apart-prop-ℂ z y))
+      ( map-disjunction inl-disjunction inl-disjunction ∘
+        cotransitive-apart-ℝ a c e)
+      ( map-disjunction inr-disjunction inr-disjunction ∘
+        cotransitive-apart-ℝ b d f)
+```
+
+### Apartness on the complex numbers is a large apartness relation
+
+```agda
+large-apartness-relation-ℂ : Large-Apartness-Relation _⊔_ ℂ
+apart-prop-Large-Apartness-Relation large-apartness-relation-ℂ =
+  apart-prop-ℂ
+antirefl-Large-Apartness-Relation large-apartness-relation-ℂ =
+  antireflexive-apart-ℂ
+symmetric-Large-Apartness-Relation large-apartness-relation-ℂ =
+  symmetric-apart-ℂ
+cotransitive-Large-Apartness-Relation large-apartness-relation-ℂ =
+  cotransitive-apart-ℂ
+```

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

@@ -38,6 +38,8 @@ are numbers of the form `a + bi`, where `a` and `b` are
 ℂ : (l : Level) → UU (lsuc l)
 ℂ l = ℝ l × ℝ l
 
+pattern _+iℂ_ x y = (x , y)
+
 re-ℂ : {l : Level} → ℂ l → ℝ l
 re-ℂ = pr1
 
@@ -81,13 +83,6 @@ complex-ℤ[i] : ℤ[i] → ℂ lzero
 complex-ℤ[i] (a , b) = (real-ℤ a , real-ℤ b)
 ```
 
-### The conjugate of a complex number
-
-```agda
-conjugate-ℂ : {l : Level} → ℂ l → ℂ l
-conjugate-ℂ (a , b) = (a , neg-ℝ b)
-```
-
 ### Important complex numbers
 
 ```agda
@@ -110,3 +105,11 @@ i-ℂ = (zero-ℝ , one-ℝ)
 neg-ℂ : {l : Level} → ℂ l → ℂ l
 neg-ℂ (a , b) = (neg-ℝ a , neg-ℝ b)
 ```
+
+### `complex-ℝ one-ℝ` is equal to `one-ℂ`
+
+```agda
+abstract
+  eq-complex-one-ℝ : complex-ℝ one-ℝ ＝ one-ℂ
+  eq-complex-one-ℝ = eq-ℂ refl (inv (eq-raise-ℝ zero-ℝ))
+```

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

@@ -0,0 +1,42 @@
+# Conjugation of complex numbers
+
+```agda
+module complex-numbers.conjugation-complex-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import complex-numbers.complex-numbers
+
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import real-numbers.negation-real-numbers
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "conjugate" WDID=Q381040 WD="complex conjugate" Disambiguation="of a complex number" Agda=conjugate-ℂ}}
+of a [complex number](complex-numbers.complex-numbers.md) `a + bi` is `a - bi`.
+
+## Definition
+
+```agda
+conjugate-ℂ : {l : Level} → ℂ l → ℂ l
+conjugate-ℂ (a +iℂ b) = a +iℂ neg-ℝ b
+```
+
+## Properties
+
+### Conjugation is an involution
+
+```agda
+abstract
+  is-involution-conjugate-ℂ :
+    {l : Level} (z : ℂ l) → conjugate-ℂ (conjugate-ℂ z) ＝ z
+  is-involution-conjugate-ℂ (a +iℂ b) = eq-ℂ refl (neg-neg-ℝ b)
+```