Skip to content

Commit

Permalink
Prove that determinant is multilinear
Browse files Browse the repository at this point in the history
  • Loading branch information
@valis
valis committed Jul 12, 2023
1 parent be495f0 commit 4767938
Show file tree
Hide file tree
Showing 4 changed files with 190 additions and 9 deletions.
75 changes: 71 additions & 4 deletions src/Algebra/Matrix.ard
View file
Original file line number Diff line number Diff line change
@@ -1,11 +1,16 @@
\import Algebra.Group
\import Algebra.Group.Category
\import Algebra.Module
\import Algebra.Module.Category
\import Algebra.Monoid
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Semiring
\import Arith.Fin
\import Data.Array
\import Data.Fin (fsuc)
\import Function.Meta
\import Logic
\import Meta
\import Paths
\import Paths.Meta
Expand All @@ -17,15 +22,28 @@
\func mkMatrix {R : \Type} {n m : Nat} (f : Fin n -> Fin m -> R) : Matrix R n m
=> \new Array (Array R m) n $ \lam i => \new Array R m (f i)

\func matrixFromArrays {R : \Type} {n m : Nat} (M : Array (Array R m) n) : Matrix R n m => M

\func matrixExt {R : \Type} {n m : Nat} {M N : Matrix R n m} (p : \Pi (i : Fin n) (j : Fin m) -> M i j = N i j) : M = N
=> path (\lam i => mkMatrix (\lam j k => p j k i))

\instance MatrixRing (R : Ring) (n : Nat) : Ring (Matrix R n n)
\instance MatrixModule (R : Ring) (n m : Nat) : LModule' R \cowith
| E => Matrix R n m
| zro => mkMatrix $ \lam _ _ => zro
| + M N => mkMatrix $ \lam i j => M i j + N i j
| + => MatrixRing.add
| zro-left => matrixExt $ \lam i j => zro-left
| +-assoc => matrixExt $ \lam i j => +-assoc
| +-comm => matrixExt $ \lam i j => +-comm
| negative M => mkMatrix $ \lam i j => negative (M i j)
| negative-left => matrixExt $ \lam i j => negative-left
| *c a M => mkMatrix $ \lam i j => a * M i j
| *c-assoc => matrixExt $ \lam i j => *-assoc
| *c-ldistr => matrixExt $ \lam i j => ldistr
| *c-rdistr => matrixExt $ \lam i j => rdistr
| ide_*c => matrixExt $ \lam i j => ide-left

\instance MatrixRing (R : Ring) (n : Nat) : Ring (Matrix R n n)
| AbGroup => MatrixModule R n n
| ide : Matrix R n n => mkMatrix $ \lam i j => \case decideEq i j \with {
| yes _ => R.ide
| no _ => zro
Expand All @@ -36,8 +54,6 @@
| *-assoc => product-assoc
| ldistr => matrix_ldistr
| rdistr => matrix_rdistr
| negative M => mkMatrix $ \lam i j => negative (M i j)
| negative-left => matrixExt $ \lam i j => negative-left
\where {
\open AddMonoid

Expand All @@ -63,4 +79,55 @@

\lemma matrix_rdistr {R : Ring} {n m k : Nat} {M N : Matrix R n m} {L : Matrix R m k} : product (add M N) L = add (product M L) (product N L)
=> matrixExt $ \lam i j => pmap BigSum (arrayExt $ \lam k => rdistr) *> R.BigSum_+
}

\func determinant {R : CRing} {n : Nat} (M : Matrix R n n) : R \elim n
| 0 => 1
| suc n => determinantN {R} {suc n} 0 M
\where {
\func minor {R : \Type} {n m : Nat} (M : Matrix R (suc n) (suc m)) (i0 : Fin (suc n)) (j0 : Fin (suc m)) : Matrix R n m
=> map (skip __ j0) (skip M i0)

\lemma multilinear {R : CRing} {n : Nat} : isMultiLinear {R} {n} {ArrayLModule n (RingLModule R)} {RingLModule R} (\lam M => determinant M) \elim n
| 0 => ()
| suc n => determinantN.multilinear {R} {suc n} 0
}

\func determinantN {R : CRing} {n : Nat} (k : Fin n) (M : Matrix R n n) : R \elim n
| 0 => 1
| suc n => R.BigSum $ \lam i => M i k * R.pow -1 (i Nat.+ k) * determinant (minor M i k)
\where {
\open determinant(minor)
\open skip_replace_/=
\open ArrayLModule

\lemma minor_insert {R : CRing} {n m : Nat} {i : Fin (suc n)} {x : Array R (suc m)} {l : Array (Array R (suc m)) n} {j : Fin (suc m)}
: minor (insert x l i) i j = \new Array (Array R m) n (\lam i => skip (l i) j)
=> path (\lam i' => map (skip __ j) (skip_insert_= i'))

\lemma aux/= {R : CRing} {n m : Nat} {j i : Fin (suc n)} (p : j /= i) {k : Fin (suc m)} {x : Array R (suc m)} {M : Array (Array R (suc m)) n}
: insert {Array R (suc m)} x M j i k = M (newIndex (\lam q => p (inv q))) k \elim n, j, i, M
| _, 0, 0, _ => absurd (p idp)
| suc n, 0, suc i, y :: M => idp
| suc n, suc j, 0, y :: M => idp
| suc n, suc j, suc i, y :: M => aux/= (\lam q => p (pmap fsuc q))

\func minor_replace {R : CRing} {n : Nat} {i k : Fin (suc n)} {M : Array (Array R (suc n)) (suc n)} {j : Fin (suc n)} {x : Array R (suc n)} (p : j /= i)
: minor (replace M j x) i k = replace (minor M i k) (newIndex p) (skip x k)
=> path (\lam i => map (skip __ k) (skip_replace_/= p i)) *> pmap matrixFromArrays (map_replace (skip __ k))

\lemma multilinear {R : CRing} {n : Nat} (k : Fin n) : isMultiLinear {R} {n} {ArrayLModule n (RingLModule R)} {RingLModule R} (\lam M => determinantN k M) \elim n
| 0 => ()
| suc n => isMultilinear_BigSum {R} {suc n} {ArrayLModule (suc n) (RingLModule R)} (\lam i M => M i k * R.pow -1 (i Nat.+ k) * determinant (minor M i k)) $ \lam i M j => \case decideEq j i \with {
| yes e => \new LinearMap {
| func-+ {a} {b} => rewrite e $ *-assoc *> pmap {Array R (suc n)} (__ k * _) (insert-index {Array R (suc n)}) *> rdistr *> pmap2 (+)
(pmap (\lam x => _ * (_ * determinant x)) (minor_insert *> inv minor_insert) *> inv (*-assoc *> pmap {Array R (suc n)} (__ k * _) (insert-index {Array R (suc n)})))
(pmap (\lam x => _ * (_ * determinant x)) (minor_insert *> inv minor_insert) *> inv (*-assoc *> pmap {Array R (suc n)} (__ k * _) (insert-index {Array R (suc n)})))
| func-*c {r} {a} => rewrite e $ *-assoc *> pmap {Array R (suc n)} (__ k * _) (insert-index {Array R (suc n)}) *> *-assoc *> pmap (r *) (pmap (\lam x => _ * (_ * determinant x)) (minor_insert *> inv minor_insert) *> inv (*-assoc *> pmap {Array R (suc n)} (__ k * _) (insert-index {Array R (suc n)})))
}
| no q => \new LinearMap {
| func-+ => rewrite (aux/= q, aux/= q, aux/= q) $ pmap (_ *) (inv (path (\lam i' => determinant (minor (replace_insert {_} {M} {j} {replicate (suc n) R.zro} i') i k))) *> pmap determinant (minor_replace q) *> rewrite skip_+ (func-+ {isMultiLinear.toReplace {R} {_} {_} {n} determinant.multilinear _ _} *> pmap2 (determinant __ + determinant __) (inv (minor_replace q) *> path (\lam i' => minor (replace_insert i') i k)) (inv (minor_replace q) *> path (\lam i' => minor (replace_insert i') i k)))) *> ldistr
| func-*c {r} {x} => rewrite (aux/= q, aux/= q) $ pmap (_ * _ * __) (inv (path (\lam i' => determinant (minor (replace_insert {_} {M} {j} {replicate (suc n) R.zro} i') i k))) *> pmap determinant (minor_replace q) *> rewrite skip_*c (func-*c {isMultiLinear.toReplace {R} {_} {_} {n} determinant.multilinear _ _} *> pmap (r * determinant __) (inv (minor_replace q))) *> path (\lam i' => r * determinant (minor (replace_insert i') i k)) *> *-comm) *> inv *-assoc *> *-comm
}
}
}
36 changes: 36 additions & 0 deletions src/Algebra/Module.ard
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,14 @@
\lemma neg_ide_*c {a : E} : -1 *c a = negative a
=> *c_negative-left *> pmap negative ide_*c

\lemma *c_BigSum-left {l : Array R} {a : E} : R.BigSum l *c a = BigSum (\lam i => l i *c a) \elim l
| nil => *c_zro-left
| r :: l => *c-rdistr *> pmap (_ +) *c_BigSum-left

\lemma *c_BigSum-right {r : R} {l : Array E} : r *c BigSum l = BigSum (\lam i => r *c l i) \elim l
| nil => *c_zro-right
| a :: l => *c-ldistr *> pmap (_ +) *c_BigSum-right

\func isGenerated (l : Array E) : \Prop
=> \Pi (x : E) -> ∃ (c : Array R l.len) (x = BigSum (mkArray (\lam i => c i *c l i)))

Expand Down Expand Up @@ -75,6 +83,34 @@
| *c-rdistr => ext (\lam j => *c-rdistr)
| ide_*c => ext (\lam j => ide_*c)

\instance ArrayLModule {R : Ring} (n : Nat) (M : LModule' R) : LModule (Array M n) { | R => R }
| zro _ => 0
| + f g j => f j + g j
| zro-left => arrayExt (\lam j => zro-left)
| zro-right => arrayExt (\lam j => zro-right)
| +-assoc => arrayExt (\lam j => +-assoc)
| negative f j => negative (f j)
| negative-left => arrayExt (\lam j => negative-left)
| +-comm => arrayExt (\lam j => +-comm)
| *c r f j => r *c f j
| *c-assoc => arrayExt (\lam j => *c-assoc)
| *c-ldistr => arrayExt (\lam j => *c-ldistr)
| *c-rdistr => arrayExt (\lam j => *c-rdistr)
| ide_*c => arrayExt (\lam j => ide_*c)
\where {
\lemma skip_*c {R : CRing} {n : Nat} {r : R} {l : Array R (suc n)} {k : Fin (suc n)}
: skip (r *c {ArrayLModule _ (RingLModule R)} l) k = r *c {ArrayLModule _ (RingLModule R)} skip l k \elim n, l, k
| 0, a :: nil, 0 => idp
| suc n, a :: l, 0 => idp
| suc n, a :: l, suc k => path (\lam i => r *c a :: skip_*c i)

\lemma skip_+ {R : CRing} {n : Nat} {l l' : Array R (suc n)} {k : Fin (suc n)}
: skip (l + {ArrayLModule _ (RingLModule R)} l') k = skip l k + {ArrayLModule _ (RingLModule R)} skip l' k \elim n, l, l', k
| 0, a :: nil, a' :: nil, 0 => idp
| suc n, a :: l, a' :: l', 0 => idp
| suc n, a :: l, a' :: l', suc k => path (\lam i => a + a' :: skip_+ i)
}

\func homLModule (f : RingHom) : LModule' f.Dom \cowith
| AbGroup => f.Cod
| *c x y => f x * y
Expand Down
22 changes: 22 additions & 0 deletions src/Algebra/Module/Category.ard
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,10 @@
| func-+ => pmap negative f.func-+ *> B.negative_+ *> +-comm
| func-*c => pmap negative f.func-*c *> inv B.*c_negative-right

\lemma linearMap_BigSum {R : Ring} {A B : LModule' R} {m : Nat} (f : Fin m -> LinearMap' A B) : LinearMap' A B { | func a => BigSum (\lam i => f i a) } \cowith
| func-+ => cong (ext (\lam i => func-+)) *> B.BigSum_+
| func-*c => cong (ext (\lam i => func-*c)) *> inv B.*c_BigSum-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 }
Expand All @@ -52,6 +56,20 @@
\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 fromReplace {n : Nat} {f : Array A n -> B} (p : \Pi (l : Array A n) (j : Fin n) -> LinearMap' A B { | func x => f (replace l j x) }) : isMultiLinear f \elim n
| 0 => ()
| suc n => \lam l j => \new LinearMap {
| func-+ => inv (pmap f (replace_insert {_} {l} {j} {A.zro})) *> func-+ {p _ j} *> pmap2 (+) (pmap f replace_insert) (pmap f replace_insert)
| func-*c => inv (pmap f (replace_insert {_} {l} {j} {A.zro})) *> func-*c {p _ j} *> pmap (_ *c) (pmap f replace_insert)
}

\lemma toReplace {n : Nat} {f : Array A n -> B} (fl : isMultiLinear f) (l : Array A n) (j : Fin n) : LinearMap' A B { | func x => f (replace l j x) } \elim n
| 0 => \case j
| suc n => \new LinearMap {
| func-+ => inv (pmap f insert_skip) *> func-+ {fl _ j} *> pmap2 (f __ + f __) insert_skip insert_skip
| func-*c => inv (pmap f insert_skip) *> func-*c {fl _ j} *> pmap (_ *c f __) insert_skip
}
}

\lemma isMultilinear_zro {R : Ring} {n : Nat} {A B : LModule' R} : isMultiLinear {R} {n} {A} {B} (\lam x => 0) \elim n
Expand All @@ -66,6 +84,10 @@
| 0 => ()
| suc n => \lam l j => linearMap_negative (fl l j)

\lemma isMultilinear_BigSum {R : Ring} {n : Nat} {A B : LModule' R} {m : Nat} (f : Fin m -> Array A n -> B) (fl : \Pi (j : Fin m) -> isMultiLinear (f j)) : isMultiLinear (\lam x => B.BigSum (\lam i => f i x)) \elim n
| 0 => ()
| suc n => \lam l j => linearMap_BigSum (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 {
Expand Down
66 changes: 61 additions & 5 deletions src/Data/Array.ard
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
\import Algebra.Meta
\import Algebra.Ring
\import Arith.Fin
\import Data.Bool
Expand All @@ -16,7 +17,7 @@

\func mkArray {A : \Type} {n : Nat} (f : Fin n -> A) => \new Array A n f

\func arrayExt {A : \Type} {n : Nat} {l l' : Array A n} (p : \Pi (j : Fin n) -> l j = l' j) : l = {Array A n} l'
\func arrayExt {A : \Type} {n : Nat} {l l' : Array A n} (p : \Pi (j : Fin n) -> l j = l' j) : l = l'
=> path (\lam i => \new Array A n (\lam j => p j i))

\func tail {n : Nat} {A : Fin (suc n) -> \Type} (a : DArray A) : DArray (\lam j => A (suc j)) \elim a
Expand Down Expand Up @@ -247,9 +248,64 @@
| b :: l, 0 => a :: b :: l
| b :: l, suc j => b :: insert a l j

\func insert_zro {A : \Type} {n : Nat} {a : A} {l : Array A n} : insert a l 0 = {Array A (suc n)} a :: l \elim n, l
| 0, nil => path (\lam _ => a :: nil)
| suc n, b :: l => path (\lam _ => a :: b :: l)
\func insert_zro {A : \Type} {n : Nat} {a : A} {l : Array A n} : insert a l 0 = a :: l \elim n, l
| 0, nil => idp
| suc n, b :: l => idp

\func insert-index {A : \Type} {a : A} {l : Array A} {j : Fin (suc l.len)} : insert a l j j = a \elim l, j
| nil, 0 => idp
| b :: l, 0 => idp
| b :: l, suc j => insert-index

\func skip {A : \Type} {n : Nat} (l : Array A (suc n)) (k : Fin (suc n)) : Array A n \elim n, l, k
| n, _ :: l, 0 => l
| suc n, a :: l, suc k => a :: skip l k

\func replace {A : \Type} (l : Array A) (i : Fin l.len) (a : A) : Array A l.len \elim l, i
| b :: l, 0 => a :: l
| b :: l, suc i => b :: replace l i a

\func replace_insert {A : \Type} {l : Array A} {i : Fin (suc l.len)} {a b : A} : replace (insert a l i) i b = insert b l i \elim l, i
| nil, 0 => idp
| c :: l, 0 => idp
| c :: l, suc i => cong replace_insert

\func skip_replace_= {A : \Type} {n : Nat} {l : Array A (suc n)} {i : Fin (suc n)} {a : A}
: skip (replace l i a) i = skip l i \elim n, l, i
| 0, b :: l, 0 => idp
| suc n, b :: l, 0 => idp
| suc n, b :: l, suc i => path (\lam i => b :: skip_replace_= i)

\func skip_replace_/= {A : \Type} {n : Nat} {l : Array A (suc n)} {j i : Fin (suc n)} {a : A} (p : j /= i)
: skip (replace l j a) i = replace (skip l i) (newIndex p) a \elim n, l, j, i
| _, _, 0, 0 => absurd (p idp)
| suc n, b :: l, 0, suc 0 => idp
| suc n, b :: l, 0, suc (suc i) => idp
| suc n, b :: l, suc j, 0 => idp
| suc n, b :: l, suc j, suc i => cong (skip_replace_/= _)
\where {
\func newIndex {n : Nat} {j i : Fin (suc n)} (p : i /= j) : Fin n \elim n, j, i
| _, 0, 0 => absurd (p idp)
| suc n, 0, suc i => i
| suc n, suc j, 0 => 0
| suc n, suc j, suc i => suc $ newIndex (\lam q => p (pmap fsuc q))
}

\func map_replace {A B : \Type} (f : A -> B) {l : Array A} {i : Fin l.len} {a : A}
: map f (replace l i a) = replace (map f l) i (f a) \elim l, i
| b :: l, 0 => idp
| b :: l, suc i => path (\lam i => f b :: map_replace f i)

\func insert_skip {A : \Type} {n : Nat} {l : Array A (suc n)} {k : Fin (suc n)} {a : A}
: insert a (skip l k) k = replace l k a \elim n, l, k
| 0, b :: nil, 0 => idp
| suc n, b :: l, 0 => idp
| suc n, b :: l, suc k => cong insert_skip

\func skip_insert_= {A : \Type} {n : Nat} {a : A} {l : Array A n} {j : Fin (suc n)} : skip (insert a l j) j = l \elim n, l, j
| 0, nil, 0 => idp
| suc n, b :: l, 0 => idp
| suc n, b :: l, suc j => cong skip_insert_=

\data Perm {A : \Type} {n : Nat} (l1 l2 : Array A n) \elim n, l1, l2
| 0, nil, nil => perm-nil
Expand Down Expand Up @@ -299,7 +355,7 @@
| suc (suc n) => aux2 {suc n} l l-inj 0
\where {
\func aux {n : Nat} (l : Array (Fin (suc n)) n) (q : \Pi (j : Fin n) -> l j /= 0) (d : Fin n) (r : Perm (map (fpred d) l) (\lam j => j)) : Perm l (\lam j => suc j)
=> transport {Array (Fin (suc n)) n} (Perm __ _) (arrayExt $ \lam j => fsuc_fpred (q j)) $ perm-map fsuc {n} r
=> transport (Perm __ _) (arrayExt $ \lam j => fsuc_fpred (q j)) $ perm-map fsuc {n} r

\func aux2 {n : Nat} (l : Array (Fin (suc n)) (suc n)) (l-inj : isInj l) (d : Fin n) : Perm l (\lam j => j)
=> \have | (j,lj=0) => isDFin.isSplit {Fin (suc n)} (isDFin.fromPigeonhole (finFin _)) l l-inj 0
Expand Down

0 comments on commit 4767938

Please sign in to comment.