Editing Cauchy–Binet formula (section)

== Proof ==

There are various kinds of proofs that can be given for the Cauchy−Binet formula. The proof below is based on formal manipulations only, and avoids using any particular interpretation of determinants, which may be taken to be defined by the [[Leibniz formula (determinant)|Leibniz formula]]. Only their multilinearity with respect to rows and columns, and their alternating property (vanishing in the presence of equal rows or columns) are used; in particular the multiplicative property of determinants for square matrices is not used, but is rather established (the case ''n''&nbsp;=&nbsp;''m''). The proof is valid for arbitrary commutative coefficient rings.

The formula can be proved in two steps:

# use the fact that both sides are [[Multilinear map|multilinear]] (more precisely 2''m''-linear) in the ''rows'' of ''A'' and the ''columns'' of ''B'', to reduce to the case that each row of ''A'' and each column of ''B'' has only one non-zero entry, which is&nbsp;1.
# handle that case using the functions [''m'']&nbsp;→&nbsp;[''n''] that map respectively the row numbers of ''A'' to the column number of their nonzero entry, and the column numbers of ''B'' to the row number of their nonzero entry.

For step 1, observe that for each row of ''A'' or column of ''B'', and for each ''m''-combination ''S'', the values of det(''AB'') and det(''A''<sub>[''m''],''S''</sub>)det(''B''<sub>''S'',[''m'']</sub>) indeed depend linearly on the row or column. For the latter this is immediate from the multilinear property of the determinant; for the former one must in addition check that taking a linear combination for the row of ''A'' or column of ''B'' while leaving the rest unchanged only affects the corresponding row or column of the product ''AB'', and by the same linear combination. Thus one can work out both sides of the Cauchy−Binet formula by linearity for every row of ''A'' and then also every column of ''B'', writing each of the rows and columns as a linear combination of standard basis vectors. The resulting multiple summations are huge, but they have the same form for both sides: corresponding terms involve the same scalar factor (each is a product of entries of ''A'' and of ''B''), and these terms only differ by involving two different expressions in terms of constant matrices of the kind described above, which expressions should be equal according to the Cauchy−Binet formula. This achieves the reduction of the first step.

Concretely, the multiple summations can be grouped into two summations, one over all functions ''f'':[''m'']&nbsp;→&nbsp;[''n''] that for each row index of ''A'' gives a corresponding column index, and one over all functions ''g'':[''m'']&nbsp;→&nbsp;[''n''] that for each column index of ''B'' gives a corresponding row index. The matrices associated to ''f'' and ''g'' are

:<math>L_f=\bigl((\delta_{f(i),j})_{i\in[m],j\in[n]}\bigr) \quad\text{and}
\quad R_g=\bigl((\delta_{j,g(k)})_{j\in[n],k\in[m]}\bigr)</math>

where "<math>\delta</math>" is the [[Kronecker delta]], and the Cauchy−Binet formula to prove has been rewritten as

: <math>
\begin{align}
& \sum_{f:[m]\to[n]}\sum_{g:[m]\to[n]}p(f,g)\det(L_fR_g) \\[5pt]
= {} & \sum_{f:[m]\to[n]}\sum_{g:[m]\to[n]} p(f,g) \sum_{S\in\tbinom{[n]}m} \det((L_f)_{[m],S}) \det((R_g)_{S,[m]}),
\end{align}
</math>

where ''p''(''f'',''g'') denotes the scalar factor <math>\textstyle(\prod_{i=1}^mA_{i,f(i)})(\prod_{k=1}^mB_{g(k),k})</math>. It remains to prove the Cauchy−Binet formula for ''A''&nbsp;=&nbsp;''L''<sub>''f''</sub> and ''B''&nbsp;=&nbsp;''R''<sub>''g''</sub>, for all ''f'',''g'':[''m'']&nbsp;→&nbsp;[''n''].

For this step 2, if ''f'' fails to be injective then ''L''<sub>''f''</sub> and ''L''<sub>''f''</sub>''R''<sub>''g''</sub> both have two identical rows, and if ''g'' fails to be injective then ''R''<sub>''g''</sub> and ''L''<sub>''f''</sub>''R''<sub>''g''</sub> both have two identical columns; in either case both sides of the identity are zero. Supposing now that both ''f'' and ''g'' are injective maps [''m'']&nbsp;→&nbsp;[''n''], the factor <math>\det((L_f)_{[m],S})</math> on the right is zero unless ''S''&nbsp;=&nbsp;''f''([''m'']), while the factor <math>\det((R_g)_{S,[m]})</math> is zero unless ''S''&nbsp;=&nbsp;''g''([''m'']). So
if the images of ''f'' and ''g'' are different, the right hand side has only null terms, and the left hand side is zero as well since ''L''<sub>''f''</sub>''R''<sub>''g''</sub> has a null row (for ''i'' with <math>f(i)\notin g([m])</math>). In the remaining case where the images of ''f'' and ''g'' are the same, say ''f''([''m''])&nbsp;=&nbsp;''S''&nbsp;=&nbsp;''g''([''m'']), we need to prove that

:<math>\det(L_fR_g)=\det((L_f)_{[m],S})\det((R_g)_{S,[m]}).\,</math>

Let ''h'' be the unique increasing bijection [''m'']&nbsp;→&nbsp;''S'', and ''π'',''σ'' the permutations of [''m''] such that <math>f=h\circ\pi^{-1}</math> and <math>g=h\circ\sigma</math>; then <math>(L_f)_{[m],S}</math> is the [[permutation matrix]] for {{pi}}, <math>(R_g)_{S,[m]}</math> is the permutation matrix for ''σ'', and ''L''<sub>''f''</sub>''R''<sub>''g''</sub> is the permutation matrix for <math>\pi\circ\sigma</math>, and since the determinant of a permutation matrix equals the [[signature (permutation)|signature]] of the permutation, the identity follows from the fact that signatures are multiplicative.

Using multi-linearity with respect to both the rows of ''A'' and the columns of ''B'' in the proof is not necessary; one could use just one of them, say the former, and use that a matrix product ''L''<sub>''f''</sub>''B'' either consists of a permutation of the rows of ''B''<sub>''f''([''m'']),[''m'']</sub> (if ''f'' is injective), or has at least two equal rows.