Define the field of complex numbers

src/Algebra/Ordered.ard

@@ -6,9 +6,11 @@
 \import Algebra.Ring
 \import Algebra.Semiring
 \import Arith.Nat
+\import Data.Array
 \import Data.Or
 \import Function.Meta
 \import Logic
+\import Logic.Meta
 \import Meta
 \import Order.Lattice
 \import Order.LinearOrder
@@ -55,6 +57,14 @@
     | 0, nil, nil => <=-refl
     | suc n, a :: l, a' :: l' => <=_+ (p 0) $ BigSum_<= \lam j => p (suc j)
 
+  \lemma BigSum_>=0 {l : Array E} (q : \Pi (j : Fin l.len) -> 0 <= l j) : 0 <= BigSum l
+    => transport (`<= _) BigSum_replicate0 $ BigSum_<= {_} {_} {replicate l.len zro} q
+
+  \lemma BigSum_>0 {l : Array E} (q : \Pi (j : Fin l.len) -> 0 <= l j) (p : ∃ (j : Fin l.len) (0 < l j)) : 0 < BigSum l \elim l, p
+    | nil, inP ((),_)
+    | a :: l, inP (0, p) => transport (`< _) zro-right $ <=_+-right p $ BigSum_>=0 \lam j => q (suc j)
+    | a :: l, inP (suc j, p) => transport (`< _) zro-right $ <=_+-left (q 0) $ BigSum_>0 (\lam j => q (suc j)) $ inP (j,p)
+
   \lemma meet_+-left {a b c : E} : a + b ∧ c = (a + b) ∧ (a + c)
     => <=-antisymmetric (meet-univ (<=_+ <=-refl meet-left) (<=_+ <=-refl meet-right)) \lam p =>
         \have t => LinearOrder.meet/=left $ <_/= $ <_+-cancel-left a $ p <∘l meet-left
@@ -278,6 +288,18 @@
       | byRight (_,r) => r
     }
 
+  \lemma square_>=0 {x : E} : 0 <= x * x
+    => \lam xx<0 => \case <_*-cancel-left (transportInv (_ <) zro_*-right xx<0) \with {
+      | byLeft (x>0,x<0) => <-irreflexive (x<0 <∘ x>0)
+      | byRight (x<0,x>0) => <-irreflexive (x<0 <∘ x>0)
+    }
+
+  \lemma sum_squares_>0 {l : Array E} (p : ∃ (j : Fin l.len) (0 < l j || l j < 0)) : 0 < BigSum (map (\lam x => x * x) l) \elim p
+    | inP (j,p) => BigSum_>0 (\lam j => square_>=0) $ inP $ later (j, \case \elim p \with {
+      | byLeft p => <_*_positive_positive p p
+      | byRight p => <_*_negative_negative p p
+    })
+
   \lemma inv-positive (t : Inv {\this}) (p : t > 0) : t.inv > 0
     => \case <_*-cancel-left (transport2 (<) (inv zro_*-right) (inv t.inv-right) zro<ide) \with {
       | byLeft q => q.2

src/Algebra/Ring/Local.ard

@@ -11,13 +11,13 @@
 \class LocalRing \extends Ring, NonZeroRing {
   | locality (x : E) : Inv x || Inv (x + ide)
 
-  \lemma sum1=>eitherInv (x y : E) (x+y=1 : x + y = ide) : Inv x || Inv y => \case locality (negative x) \with {
+  \lemma sum1=>eitherInv {x y : E} (x+y=1 : x + y = ide) : Inv x || Inv y => \case locality (negative x) \with {
     | byLeft -x_inv => byLeft (rewriteI negative-isInv (Ring.negative_inv -x_inv))
     | byRight [-x+1]_inv => byRight (rewriteEq (pmap (negative x +) x+y=1) [-x+1]_inv)
   }
 
   \lemma sumInv=>eitherInv {x y : E} (q : Inv (x + y)) : Inv x || Inv y =>
-    \case sum1=>eitherInv (q.inv * x) (q.inv * y) (inv ldistr *> q.inv-left) \with {
+    \case sum1=>eitherInv (inv ldistr *> q.inv-left) \with {
       | byLeft s => byLeft (Inv.factor-right (\new LInv q.inv (x + y) q.inv-right) s)
       | byRight s => byRight (Inv.factor-right (\new LInv q.inv (x + y) q.inv-right) s)
     }

src/Arith/Complex.ard

@@ -0,0 +1,56 @@
+\import Algebra.Field
+\import Algebra.Group
+\import Algebra.Meta
+\import Algebra.Monoid
+\import Algebra.Ordered
+\import Algebra.Ring
+\import Algebra.Ring.Local
+\import Algebra.Semiring
+\import Arith.Real
+\import Function.Meta
+\import Logic
+\import Meta
+\import Order.StrictOrder
+\import Paths
+\import Paths.Meta
+\import Topology.CoverSpace.Real
+
+\record Complex (re im : Real)
+
+\instance ComplexField : Field Complex
+  | zro => \new Complex 0 0
+  | + (x y : Complex) => \new Complex (x.re + y.re) (x.im + y.im)
+  | zro-left => ext (zro-left, zro-left)
+  | +-assoc => ext (+-assoc, +-assoc)
+  | +-comm => ext (+-comm, +-comm)
+  | CMonoid => ComplexMonoid
+  | ldistr => ext (equation, equation)
+  | negative (x : Complex) => \new Complex (negative x.re) (negative x.im)
+  | negative-left => ext (negative-left, negative-left)
+  | zro/=ide p => zro/=ide $ pmap (\lam (x : Complex) => x.re) p
+  | locality (x : Complex) => \case locality x.re \with {
+    | byLeft r => byLeft $ inv-char.2 $ byLeft r
+    | byRight r => byRight $ inv-char.2 $ byLeft r
+  }
+  | #0-tight c => ext (AddGroup.#0-tight \lam p => c $ inv-char.2 $ byLeft p, AddGroup.#0-tight \lam p => c $ inv-char.2 $ byRight p)
+  \where {
+    \open Monoid(Inv)
+
+    \instance ComplexMonoid : CMonoid Complex
+      | ide => \new Complex 1 0
+      | * (x y : Complex) => \new Complex (x.re * y.re - x.im * y.im) (x.re * y.im + x.im * y.re)
+      | ide-left => ext (equation, equation)
+      | *-assoc => ext (equation, equation)
+      | *-comm => ext (pmap2 (__ - __) *-comm *-comm, +-comm *> pmap2 (+) *-comm *-comm)
+
+    \lemma inv-char {x : Complex} : Inv x <-> Inv x.re || Inv x.im
+      => (\lam p => \case RealField.sum1=>eitherInv {_} {negative _} $ pmap (\lam (x : Complex) => x.re) (Inv.inv-left {p}) \with {
+                      | byLeft r => byLeft (Inv.cfactor-right r)
+                      | byRight r => byRight $ Inv.cfactor-right $ transportInv Inv Ring.negative_*-left r
+                    },
+          \lam p => \have d : Inv (x.re * x.re + x.im * x.im) => RealField.positive=>#0 $ RealField.>0_pos {x.re * x.re + x.im * x.im} (transport (0 <) linarith $ RealField.sum_squares_>0 {x.re,x.im} \case \elim p \with {
+                      | byLeft r => inP (0, ||.map real_<_L.2 real_<_U.2 $ #0=>eitherPosOrNeg r)
+                      | byRight r => inP (1, ||.map real_<_L.2 real_<_U.2 $ #0=>eitherPosOrNeg r)
+                    })
+                    \in Inv.lmake (\new Complex (x.re * d.inv) (negative (x.im * d.inv))) $ ext (equation {usingOnly d.inv-left}, equation))
+  }

src/Arith/Real.ard

@@ -486,6 +486,16 @@
     | inP (a,a<x) => inP (a, real_<_L.2 a<x)
   }
 
+\lemma <=_L-char {x y : Real} : x <= y <-> (\Pi {a : Rat} -> x.L a -> y.L a)
+  => (\lam h a<x => \case L-rounded a<x \with {
+    | inP (b,b<x,a<b) => \case y.LU-located a<b \with {
+      | byLeft a<y => a<y
+      | byRight y<b => absurd $ h $ real_<-char.2 $ inP (b,y<b,b<x)
+    }
+  }, \lam f p => \case real_<-char.1 p \with {
+    | inP (a,y<a,a<x) => y.LU-disjoint (f a<x) y<a
+  })
+
 \lemma real-located {x a b : Real} (p : a < b) : a < x || x < b
   => \case real_<-char.1 p \with {
     | inP (a',a<a',a'<b) => \case L-rounded a'<b \with {

src/Topology/CoverSpace/Real.ard

@@ -439,20 +439,6 @@
             | inP (a,a<x,a>0), inP (a',a'<y,a'>0) => ((*_positive-char x>0 y>0 {a *' a' - 1} {d}).2 $ inP (a, b, a', b', a>0, a'>0, (a<x,x<b), (a'<y,y<b'), linarith, bb'<d)).2
           })
 
-    \lemma <=_L-char {x y : Real} : x RealField.<= y <-> (\Pi {a : Rat} -> x.L a -> y.L a)
-      => (\lam p => aux.1 \lam q => p q, aux.2 __ __)
-      \where {
-        \protected \lemma aux {x y : Real} : Not (y < x) <-> (\Pi {a : Rat} -> x.L a -> y.L a)
-          => (\lam h a<x => \case L-rounded a<x \with {
-                | inP (b,b<x,a<b) => \case y.LU-located a<b \with {
-                  | byLeft a<y => a<y
-                  | byRight y<b => absurd $ h $ real_<-char.2 $ inP (b,y<b,b<x)
-                }
-              }, \lam f p => \case real_<-char.1 p \with {
-                | inP (a,y<a,a<x) => y.LU-disjoint (f a<x) y<a
-              })
-      }
-
     \func pos-inv {x : Real} (x>0 : x.L 0) : Real \cowith
       | L a => a <= 0 || x.U (finv a)
       | L-inh => inP (0, byLeft <=-refl)