Nuprl Definition : det-fun
These properties characterize the determinant up to a multiplicative constant.
⌜λM.|M|⌝ is such a function (see Error :matrix-det-is-det-fun)
and we prove that any such function d is equal to
λM.((d I) * (determinant(n;r) M))
where the primitive recursive function ⌜determinant(n;r)⌝
expands by minors of the first row.
(see Error :det-fun-is-determinant)
A corollary is that the two versions of the determinant
(the "Leibnitz" form
|M| == Σ{r} f ∈ permutations-list(n). let k = Π(r) 0 ≤ i < n. M[i,f i] in if permutation-sign(n;f)=1 then k else (-r k)
and the "Laplace" form
determinant(n;r) ==
primrec(n;λm.1;λn',d,m. (Σ(r) 0 ≤ i < n' + 1. if isEven(i) then m[0,i] else -r m[0,i] fi * (d matrix-minor(0;i;m))))
are equal (Error :matrix-det-is-determinant).
We include the property that when two distinct rows are equal then
the determinant is 0, because for rings of characteristic 2, this does
not follow from the property that swapping rows reverses the sign.
.⋅
det-fun(r;n) ==
{d:Matrix(n;n;r) ⟶ |r||
(∀i:ℕn. ∀k:|r|. ∀M:Matrix(n;n;r). ((d matrix-mul-row(r;k;i;M)) = (k * (d M)) ∈ |r|))
∧ (∀i:ℕn. ∀row:ℕn ⟶ |r|. ∀M:Matrix(n;n;r).
((d matrix(if x=i then (row y) +r M[x,y] else M[x,y]))
= ((d matrix(if x=i then row y else M[x,y])) +r (d M))
∈ |r|))
∧ (∀i,j:ℕn. ((¬(i = j ∈ ℤ)) ⇒ (∀M:Matrix(n;n;r). ((d matrix-swap-rows(M;i;j)) = (-r (d M)) ∈ |r|))))
∧ (∀i,j:ℕn.
((¬(i = j ∈ ℤ)) ⇒ (∀M:Matrix(n;n;r). ((matrix-swap-rows(M;i;j) = M ∈ Matrix(n;n;r)) ⇒ ((d M) = 0 ∈ |r|)))))}
Definitions occuring in Statement :
matrix-mul-row: matrix-mul-row(r;k;i;M),
matrix-swap-rows: matrix-swap-rows(M;i;j),
mx: matrix(M[x; y]),
matrix-ap: M[i,j],
matrix: Matrix(n;m;r),
int_seg: {i..j-},
infix_ap: x f y,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
int_eq: if a=b then c else d,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
int: ℤ,
equal: s = t ∈ T,
rng_times: *,
rng_minus: -r,
rng_zero: 0,
rng_plus: +r,
rng_car: |r|
Definitions occuring in definition :
set: {x:A| B[x]} ,
matrix-mul-row: matrix-mul-row(r;k;i;M),
rng_times: *,
function: x:A ⟶ B[x],
infix_ap: x f y,
rng_plus: +r,
mx: matrix(M[x; y]),
int_eq: if a=b then c else d,
matrix-ap: M[i,j],
and: P ∧ Q,
rng_minus: -r,
int_seg: {i..j-},
natural_number: $n,
not: ¬A,
int: ℤ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
matrix: Matrix(n;m;r),
matrix-swap-rows: matrix-swap-rows(M;i;j),
equal: s = t ∈ T,
rng_car: |r|,
apply: f a,
rng_zero: 0
FDL editor aliases :
det-fun
Latex:
det-fun(r;n) ==
\{d:Matrix(n;n;r) {}\mrightarrow{} |r||
(\mforall{}i:\mBbbN{}n. \mforall{}k:|r|. \mforall{}M:Matrix(n;n;r). ((d matrix-mul-row(r;k;i;M)) = (k * (d M))))
\mwedge{} (\mforall{}i:\mBbbN{}n. \mforall{}row:\mBbbN{}n {}\mrightarrow{} |r|. \mforall{}M:Matrix(n;n;r).
((d matrix(if x=i then (row y) +r M[x,y] else M[x,y]))
= ((d matrix(if x=i then row y else M[x,y])) +r (d M))))
\mwedge{} (\mforall{}i,j:\mBbbN{}n. ((\mneg{}(i = j)) {}\mRightarrow{} (\mforall{}M:Matrix(n;n;r). ((d matrix-swap-rows(M;i;j)) = (-r (d M))))))
\mwedge{} (\mforall{}i,j:\mBbbN{}n.
((\mneg{}(i = j)) {}\mRightarrow{} (\mforall{}M:Matrix(n;n;r). ((matrix-swap-rows(M;i;j) = M) {}\mRightarrow{} ((d M) = 0)))))\}
Date html generated:
2018_05_21-PM-09_36_43
Last ObjectModification:
2017_12_13-PM-05_04_37
Theory : matrices
Home
Index