Prove that alternating maps are determined by their values on a gener…

…ating set

src/Algebra/Module.ard

@@ -20,12 +20,21 @@
   \lemma cancel {r : R} {a b : E} (i : Monoid.Inv r) (s : r *c a = r *c b) : a = b
     => inv ide_*c *> inv (pmap (`*c a) i.inv-left) *> *c-assoc *> pmap (i.inv *c) s *> inv *c-assoc *> pmap (`*c b) i.inv-left *> ide_*c
 
-  \lemma zro_*c-left {a : E} : 0 *c a = 0
+  \lemma *c_zro-left {a : E} : 0 *c a = 0
     => cancel-left (0 *c a) $ inv *c-rdistr *> simplify
 
-  \lemma zro_*c-right {r : R} : r *c 0 = 0
+  \lemma *c_zro-right {r : R} : r *c 0 = 0
     => cancel-left (r *c 0) $ inv *c-ldistr *> simplify
 
+  \lemma *c_negative-left {r : R} {a : E} : R.negative r *c a = negative (r *c a)
+    => negative-unique (r *c a) (inv *c-rdistr *> pmap (`*c a) R.negative-left *> *c_zro-left) negative-right
+
+  \lemma *c_negative-right {r : R} {a : E} : r *c negative a = negative (r *c a)
+    => negative-unique (r *c a) (inv *c-ldistr *> pmap (r *c) negative-left *> *c_zro-right) negative-right
+
+  \lemma neg_ide_*c {a : E} : -1 *c a = negative a
+    => *c_negative-left *> pmap negative ide_*c
+
   \func isGenerated (l : Array E) : \Prop
     => \Pi (x : E) -> ∃ (c : Array R l.len) (x = BigSum (mkArray (\lam i => c i *c l i)))
 

src/Algebra/Module/Category.ard

@@ -1,23 +1,127 @@
+\import Algebra.Group
 \import Algebra.Group.Category
+\import Algebra.Meta
 \import Algebra.Module
+\import Algebra.Monoid
 \import Algebra.Ring
+\import Arith.Fin
 \import Category
 \import Category.Meta
+\import Data.Array
+\import Data.Fin (fsuc/=)
+\import Data.Or
+\import Function.Meta
+\import Logic
+\import Meta
 \import Paths
 \import Paths.Meta
+\open AddMonoid
 
 \record LinearMap {R : Ring} \extends AddGroupHom {
   \override Dom : LModule { | R => R }
   \override Cod : LModule { | R => R }
   | func-*c {r : R} {x : Dom} : func (r *c x) = r *c func x
+
+  \lemma linearComb {l : Array (\Sigma R Dom)} : func (BigSum (map (\lam p => p.1 *c p.2) l)) = BigSum (map (\lam p => p.1 *c func p.2) l) \elim l
+    | nil => func-zro
+    | a :: l => unfold BigSum $ func-+ *> pmap2 (+) func-*c linearComb
 }
 
 \meta LinearMap' A B => LinearMap { | R => _ | Dom => A | Cod => B }
 
+\lemma linearMap_zro {R : Ring} {A B : LModule' R} : LinearMap' A B { | func a => 0 } \cowith
+  | func-+ => inv zro-left
+  | func-*c => inv B.*c_zro-right
+
+\lemma linearMap_+ {R : Ring} {A B : LModule' R} (f g : LinearMap' A B) : LinearMap' A B { | func a => f a + g a } \cowith
+  | func-+ => pmap2 (+) f.func-+ g.func-+ *> equation
+  | func-*c => pmap2 (+) f.func-*c g.func-*c *> inv *c-ldistr
+
+\lemma linearMap_negative {R : Ring} {A B : LModule' R} (f : LinearMap' A B) : LinearMap' A B { | func a => negative (f a) } \cowith
+  | func-+ => pmap negative f.func-+ *> B.negative_+ *> +-comm
+  | func-*c => pmap negative f.func-*c *> inv B.*c_negative-right
+
 \record BilinearMap {R : Ring} (A B C : LModule' R) (\coerce func : A -> B -> C)
   | linear-left {b : B} : LinearMap' A C { | func => func __ b }
   | linear-right {a : A} : LinearMap' B C { | func => func a }
 
+\func isMultiLinear {R : Ring} {n : Nat} {A B : LModule' R} (f : Array A n -> B) : \Prop \elim n
+  | 0 => \Sigma
+  | suc n => \Pi (l : Array A n) (j : Fin (suc n)) -> LinearMap' A B { | func x => f (insert x l j) }
+  \where {
+    \lemma reduce {n : Nat} (f : Array A (suc n) -> B) (fl : isMultiLinear f) {a : A} : isMultiLinear (\lam l => f (a :: l)) \elim n
+      | 0 => ()
+      | suc n => \lam l j => fl (a :: l) (suc j)
+  }
+
+\lemma isMultilinear_zro {R : Ring} {n : Nat} {A B : LModule' R} : isMultiLinear {R} {n} {A} {B} (\lam x => 0) \elim n
+  | 0 => ()
+  | suc n => \lam l j => linearMap_zro
+
+\lemma isMultilinear_+ {R : Ring} {n : Nat} {A B : LModule' R} {f g : Array A n -> B} (fl : isMultiLinear f) (gl : isMultiLinear g) : isMultiLinear (\lam x => f x + g x) \elim n
+  | 0 => ()
+  | suc n => \lam l j => linearMap_+ (fl l j) (gl l j)
+
+\lemma isMultilinear_negative {R : Ring} {n : Nat} {A B : LModule' R} {f : Array A n -> B} (fl : isMultiLinear f) : isMultiLinear (\lam x => negative (f x)) \elim n
+  | 0 => ()
+  | suc n => \lam l j => linearMap_negative (fl l j)
+
+\func isAlternating {R : Ring} {n : Nat} {A B : LModule' R} (f : Array A n -> B) : \Prop
+  => \Sigma (isMultiLinear f) (\Pi (l : Array A n) -> (\Sigma (i j : Fin n) (i /= j) (l i = l j)) -> f l = 0)
+  \where {
+    \lemma reduce {n : Nat} (f : Array A (suc n) -> B) (fa : isAlternating f) {a : A} : isAlternating (\lam l => f (a :: l))
+      => (isMultiLinear.reduce f fa.1, \lam l s => fa.2 (a :: l) (suc s.1, suc s.2, fsuc/= s.3, s.4))
+
+    \lemma substract1from0 {n : Nat} {f : Array A (suc (suc n)) -> B} (fa : isAlternating f) {a a' : A} {l : Array A n} : f (a :: a' :: l) = f (a - a' :: a' :: l)
+      => inv $ func-+ {fa.1 (a' :: l) 0} *> pmap (_ +) (AddGroupHom.func-negative {fa.1 (a' :: l) 0} *> pmap negative (fa.2 _ (0, 1, (\case __), idp)) *> B.negative_zro) *> zro-right
+
+    \lemma add0to1 {n : Nat} {f : Array A (suc (suc n)) -> B} (fa : isAlternating f) {a a' : A} {l : Array A n} : f (a :: a' :: l) = f (a :: a + a' :: l)
+      => inv $ inv (path (\lam i => f (a :: insert_zro i))) *> func-+ {fa.1 (a :: l) 1} *> pmap2 (+) (fa.2 _ (0, 1, (\case __), inv (path (\lam i => insert_zro i 0)))) (path (\lam i => f (a :: insert_zro i))) *> zro-left
+
+    \lemma alternating_perm {n : Nat} {f : Array A n -> B} (fa : isAlternating f) {l l' : Array A n} (p : Perm l l') : f l = Perm.sign p *c f l' \elim n, l, l', p
+      | 0, nil, nil, perm-nil => inv ide_*c
+      | suc n, x :: l, _ :: l', perm-:: idp p => alternating_perm (reduce (\lam l => f l) fa) p *> pmap (R.pow -1 __ `*c _) (inv Perm.inversions_perm-::)
+      | suc (suc n), x :: x' :: l, _ :: _ :: _, perm-swap idp idp idp =>
+          f (x :: x' :: l)            ==< substract1from0 fa >==
+          f (x - x' :: x' :: l)       ==< add0to1 fa *> simplify >==
+          f (x - x' :: x :: l)        ==< substract1from0 fa *> simplify >==
+          f (negative x' :: x :: l)   ==< pmap (\lam y => f (y :: x :: l)) (inv A.neg_ide_*c) *> func-*c {fa.1 (x :: l) 0} *> inv (pmap (`*c _) ide-left) >==
+          1 * -1 *c f (x' :: x :: l)  `qed
+      | n, l1, l2, perm-trans p1 p2 => alternating_perm fa p1 *> pmap (_ *c) (alternating_perm fa p2) *> inv (pmap (`*c _) (pmap (R.pow -1) Perm.inversions_perm-trans *> R.pow_+) *> *c-assoc)
+  }
+
+\lemma isAlternating_zro {R : Ring} {n : Nat} {A B : LModule' R} : isAlternating {R} {n} {A} {B} (\lam x => 0)
+  => (isMultilinear_zro, \lam _ _ => idp)
+
+\lemma isAlternating_+ {R : Ring} {n : Nat} {A B : LModule' R} {f g : Array A n -> B} (fa : isAlternating f) (ga : isAlternating g) : isAlternating (\lam x => f x + g x)
+  => (isMultilinear_+ fa.1 ga.1, \lam l c => pmap2 (+) (fa.2 l c) (ga.2 l c) *> zro-left)
+
+\lemma isAlternating_negative {R : Ring} {n : Nat} {A B : LModule' R} {f : Array A n -> B} (fa : isAlternating f) : isAlternating (\lam x => negative (f x))
+  => (isMultilinear_negative fa.1, \lam l c => pmap negative (fa.2 l c) *> B.negative_zro)
+
+\lemma alternating-unique {R : Ring} {n : Nat} {A B : LModule' R} (f g : Array A n -> B) (fa : isAlternating f) (ga : isAlternating g)
+  (l : Array A n) (Ag : A.isGenerated l) (fl=gl : f l = g l) (a : Array A n) : f a = g a
+  => B.fromZero $ alternating-unique_zro (\lam x => f x - g x) (isAlternating_+ fa (isAlternating_negative ga)) l Ag (B.toZero fl=gl) a
+  \where {
+    \open FinLinearOrder (FinLinearOrderInst)
+    \open Perm
+
+    \lemma alternating-unique_zro (f : Array A n -> B) (fa : isAlternating f)
+                                  (l : Array A n) (Ag : A.isGenerated l) (fl=0 : f l = 0) (a : Array A n) : f a = 0
+      => aux f fa.1 l Ag a $ \lam c => \case repeats-dec c \with {
+        | inl e => fa.2 (map l c) (e.1, e.2, e.3, pmap l e.4)
+        | inr inj => isAlternating.alternating_perm fa {map l c} {l} (perm-map l (perm-fin c inj)) *> rewrite fl=0 B.*c_zro-right
+      }
+
+    \lemma aux {n : Nat} (f : Array A n -> B) (fl : isMultiLinear f) (l : Array A) (Ag : A.isGenerated l)
+               (a : Array A n) (p : \Pi (c : Array (Fin l.len) n) -> f (map l c) = 0) : f a = 0 \elim n, a
+      | 0, a => p nil
+      | suc n, a0 :: a => \case Ag a0 \with {
+        | inP a0g => rewrite a0g.2 $ inv (pmap f insert_zro) *> LinearMap.linearComb {fl a 0} {\lam j => (a0g.1 j, l j)} *>
+                      BigSum_zro (\lam j => pmap (_ *c) (later $ pmap f insert_zro *> aux (\lam r => f (l j :: r)) (isMultiLinear.reduce f fl) l Ag a (\lam c => p (j :: c))) *> B.*c_zro-right)
+      }
+  }
+
 \instance LModuleCat (R : Ring) : Cat (LModule' R)
   | Hom A B => LinearMap' A B
   | id A => \new LinearMap {

src/Algebra/Monoid.ard

@@ -2,7 +2,7 @@
 \import Algebra.Pointed
 \import Arith.Nat
 \import Data.Array
-\import Data.Fin (fpred)
+\import Data.Fin (fpred, fsuc/=)
 \import Function.Meta
 \import HLevel
 \import Logic
@@ -270,6 +270,9 @@
   | zro-right {x : E} : x + zro = x
   | +-assoc {x y z : E} : (x + y) + z = x + (y + z)
 
+  \lemma negative-unique {x z : E} (y : E) (p : x + y = zro) (q : y + z = zro) : x = z
+    => inv (+-assoc *> pmap (x +) q *> zro-right) *> pmap (`+ z) p *> zro-left
+
   \func BigSum (l : Array E) => Big (+) zro l
 
   \lemma BigSum_++ {l l' : Array E} : BigSum (l ++ l') = BigSum l + BigSum l' \elim l
@@ -286,7 +289,7 @@
 
   \lemma BigSum-unique {l : Array E} (i : Fin l.len) (p : \Pi (j : Fin l.len) -> i /= j -> l j = 0) : BigSum l = l i \elim l, i
     | a :: l, 0 => pmap (a +) (BigSum_zro $ \lam j => p (suc j) (\case __)) *> zro-right
-    | a :: l, suc i => pmap (a +) (BigSum-unique i $ \lam j q => p (suc j) (\lam s => q (pmap (fpred i) s))) *> pmap (`+ l i) (p 0 (\case __)) *> zro-left
+    | a :: l, suc i => pmap (a +) (BigSum-unique i $ \lam j q => p (suc j) (fsuc/= q)) *> pmap (`+ l i) (p 0 (\case __)) *> zro-left
 } \where {
     \use \coerce fromMonoid (M : Monoid) => \new AddMonoid M.E M.ide (M.*) M.ide-left M.ide-right M.*-assoc
     \use \coerce toMonoid (M : AddMonoid) => \new Monoid M.E M.zro (M.+) M.zro-left M.zro-right M.+-assoc

src/Algebra/Ring.ard

@@ -1,7 +1,6 @@
 \import Algebra.Group
 \import Algebra.Monoid
 \import Algebra.Semiring
-\import Data.Array
 \import Logic
 \import Logic.Meta
 \import Paths
@@ -29,14 +28,11 @@
     | 0 => natCoefZero *> inv (pmap negative natCoefZero *> AddGroup.negative_zro)
     | suc n => idp
 
-  \lemma negative_*-left {x y : E} : negative x * y = negative (x * y) =>
-    pmap (\lam (t : Inv {AbGroup.toCGroup (\this : Ring)} (x * y)) => t.inv)
-         (Inv.levelProp {AbGroup.toCGroup (\this : Ring)}
-                     (Inv.lmake {AbGroup.toCGroup (\this : Ring)} (negative x * y) (inv rdistr *> pmap (`* y) negative-left *> zro_*-left))
-                     (Inv.lmake {AbGroup.toCGroup (\this : Ring)} (negative (x * y)) negative-left))
-    \where \open Monoid(Inv)
+  \lemma negative_*-left {x y : E} : negative x * y = negative (x * y)
+    => negative-unique (x * y) (inv rdistr *> pmap (`* y) negative-left *> zro_*-left) negative-right
 
-  \lemma negative_*-right {x y : E} : x * negative y = negative (x * y) => negative_*-left {op \this}
+  \lemma negative_*-right {x y : E} : x * negative y = negative (x * y)
+    => negative_*-left {op \this}
 
   \lemma negative_ide-left {x : E} : negative ide * x = negative x
     => negative_*-left *> pmap negative ide-left

src/Analysis/Calculus/Derivative.ard

@@ -33,24 +33,24 @@
 \func deriv {R : DRing} {A B : LModule' R} {U : A -> \Prop} {f : \Sigma (x : A) (U x) -> B} (d : isDiff f) (x : \Sigma (a : A) (U a)) : LinearMap' A B \cowith
   | func a => (d x a (0, sub-lem x)).1
   | func-+ {a} {a'} =>
-    \have s => cancel-lem (\lam t => \Sigma (U (x.1 + t *c (a + a'))) (U (x.1 + t *c a)) (U (x.1 + t *c a + t *c a'))) (\lam t => (d x (a + a') (t.1, t.2.1)).1) (\lam t => (d (x.1 + t.1 *c a, t.2.2) a' (t.1, t.2.3)).1 + (d x a (t.1, t.2.2)).1) (0, (sub-lem x, sub-lem x, rewrite (A.zro_*c-left, zro-right) (sub-lem x))) $
+    \have s => cancel-lem (\lam t => \Sigma (U (x.1 + t *c (a + a'))) (U (x.1 + t *c a)) (U (x.1 + t *c a + t *c a'))) (\lam t => (d x (a + a') (t.1, t.2.1)).1) (\lam t => (d (x.1 + t.1 *c a, t.2.2) a' (t.1, t.2.3)).1 + (d x a (t.1, t.2.2)).1) (0, (sub-lem x, sub-lem x, rewrite (A.*c_zro-left, zro-right) (sub-lem x))) $
                 \lam t => (d _ _ (_, _)).2 *> pmap (`- _) (pmap f (ext $ rewrite *c-ldistr $ inv +-assoc) *> inv zro-right *> pmap (_ +) (inv negative-left) *> inv +-assoc) *> +-assoc *> inv (pmap2 (+) (d _ _ (_, _)).2 (d _ _ (_, _)).2) *> inv B.*c-ldistr
-    \in s *> +-comm *> pmap (_ +) (isDiff-eq d (pmap (x.1 +) A.zro_*c-left *> zro-right) idp)
+    \in s *> +-comm *> pmap (_ +) (isDiff-eq d (pmap (x.1 +) A.*c_zro-left *> zro-right) idp)
   | func-*c {r} {a} =>
     \have s => cancel-lem (\lam t => \Sigma (U (x.1 + t *c (r *c a))) (U (x.1 + t * r *c a))) (\lam t => (d x (r *c a) (t.1, t.2.1)).1) (\lam t => r *c (d x a (t.1 * r, t.2.2)).1) (0, (sub-lem x, rewrite *c-assoc $ sub-lem x)) $
                 \lam t => later (rewrite ((d x (r *c a) (t.1, t.2.1)).2, (d x a (t.1 * r, t.2.2)).2) $ pmap (f __ - f x) $ ext $ pmap (x.1 +) $ inv *c-assoc) *> *c-assoc
     \in s *> pmap (r *c) (isDiff-eq d idp R.zro_*-left)
   \where
     \lemma sub-lem {A : LModule} {U : A -> \Prop} {a : A} (x : \Sigma (a : A) (U a)) : U (x.1 + 0 *c a)
-      => transportInv U (pmap (x.1 +) A.zro_*c-left *> zro-right) x.2
+      => transportInv U (pmap (x.1 +) A.*c_zro-left *> zro-right) x.2
 
 -- | The derivative of a linear map is the map itself
 \func linear_diff {R : DRing} {A B : LModule' R} (f : LinearMap' A B) : isDiffT f
   => \lam x a t => (f a, rewrite (+-comm,f.func-+) $ inv (simplify f.func-*c))
 
 -- | The derivative of a constant map is zero
 \func const_diff {R : DRing} {A B : LModule' R} (b : B) : isDiffT (\lam (_ : A) => b)
-  => \lam x a t => (0, B.zro_*c-right *> inv negative-right)
+  => \lam x a t => (0, B.*c_zro-right *> inv negative-right)
 
 -- | The derivative of a sum is the sum of derivatives
 \func +_diff {R : DRing} {A B : LModule' R} {U : A -> \Prop} {f g : \Sigma (a : A) (U a) -> B} (df : isDiff f) (dg : isDiff g) : isDiff (\lam x => f x + g x)

src/Data/Array.ard

@@ -307,4 +307,32 @@
              \in perm-trans (perm-remove l j) $ perm-:: lj=0 $ aux (remove1 (l j) l) remove/=0 d $ perm-fin (map (fpred d) (remove1 (l j) l)) $
                   \lam {i} {j} p => remove1-inj l-inj $ inv (fsuc_fpred (remove/=0 i)) *> pmap fsuc p *> fsuc_fpred (remove/=0 j)
       }
+  }
+
+\func index-dec {A : DecSet} (l : Array A) (a : A) : Or (Index a l) (Not (Index a l)) \elim l
+  | nil => inr $ \case __.1
+  | b :: l => \case decideEq b a \with {
+    | yes e => inl (0, e)
+    | no q => \case index-dec l a \with {
+      | inl e => inl (suc e.1, e.2)
+      | inr p => inr $ \case __ \with {
+        | (0, c) => q c
+        | (suc i, c) => p (i,c)
+      }
+    }
+  }
+
+\func repeats-dec {A : DecSet} (l : Array A) : Or (\Sigma (i j : Fin l.len) (i /= j) (l i = l j)) (isInj l) \elim l
+  | nil => inr $ \lam {i} => \case i
+  | a :: l => \case index-dec l a \with {
+    | inl e => inl (suc e.1, 0, (\case __), e.2)
+    | inr q => \case repeats-dec l \with {
+      | inl e => inl (suc e.1, suc e.2, fsuc/= e.3, e.4)
+      | inr p => inr $ \lam {i} {j} => \case \elim i, \elim j \with {
+        | 0, 0 => \lam _ => idp
+        | 0, suc j => \lam r => absurd $ q (j, inv r)
+        | suc i, 0 => \lam r => absurd $ q (i, r)
+        | suc i, suc j => \lam r => pmap fsuc (p r)
+      }
+    }
   }