description/proof of that over commutative ring, determinant of product of square matrices is product of determinants of matrices
Topics
About: matrices space
The table of contents of this article
Starting Context
- The reader knows a definition of determinant of square matrix over ring.
Target Context
- The reader will have a description and a proof of the proposition that over any commutative ring, the determinant of the product of any square matrices is the product of the determinants of the matrices.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\(R\): \(\in \{\text{ the commutative rings }\}\)
\(n\): \(\in \mathbb{N} \setminus \{0\}\)
\(M\): \(\in \{\text{ the } n \times n R \text{ matrices }\}\)
\(M'\): \(\in \{\text{ the } n \times n R \text{ matrices }\}\)
//
Statements:
\(det (M M') = det M det M'\)
//
2: Proof
Whole Strategy: Step 1: see that each column of \(M M'\) is the sum of some columns, and decompose \(det M M'\) as the sum of the corresponding determinants; Step 2: see that each column of each determinant has a factor, and take the factor out of the determinant; Step 3: see that a determinant is nonzero only when the indexes combination is distinct, and keep only the nonzero terms; Step 4: conclude the proposition.
Step 1:
\(M M' = \begin{pmatrix} M^j_m M'^m_l \end{pmatrix} = \begin{pmatrix} M^1_{m^1_1} M'^{m^1_1}_1 & ... & M^1_{m^1_n} M'^{m^1_n}_n \\ ... \\ M^n_{m^n_1} M'^{m^n_1}_1 & ... & M^n_{m^n_n} M'^{m^n_n}_n \end{pmatrix}\).
Each column is \(\begin{pmatrix} M^1_{m^1_l} M'^{m^1_l}_l \\ ... \\ M^n_{m^n_l} M'^{m^n_l}_l \end{pmatrix} = \sum_{m_l \in \{1, ..., n\}} \begin{pmatrix} M^1_{m_l} M'^{m_l}_l \\ ... \\ M^n_{m_l} M'^{m_l}_l \end{pmatrix}\): we can use the single index, \(m_l\).
So, \(det (M M') = \sum_{m_1 \in \{1, ..., n\}} det \begin{pmatrix} M^1_{m_1} M'^{m_1}_1 & M^1_{m^1_2} M'^{m^1_2}_2 & ... & M^1_{m^1_n} M'^{m^1_n}_n \\ ... \\ M^n_{m_1} M'^{m_1}_1 & M^n_{m^n_2} M'^{m^n_2}_2 & ... & M^n_{m^n_n} M'^{m^n_n}_n \end{pmatrix} = ... = \sum_{m_1, ..., m_n \in \{1, ..., n\}} det \begin{pmatrix} M^1_{m_1} M'^{m_1}_1 & ... & M^1_{m_n} M'^{m_n}_n \\ ... \\ M^n_{m_1} M'^{m_1}_1 & ... & M^n_{m_n} M'^{m_n}_n \end{pmatrix}\), by a property of determinant of square matrix over commutative ring.
Step 2:
Each \(l\)-th column of each determinant has the \(M'^{m_l}_l\) factor, which can be taken out of the determinant, by a property of determinant of square matrix over commutative ring, so, \(det (M M') = \sum_{m_1, ..., m_n \in \{1, ..., n\}} M'^{m_1}_1 ... M'^{m_n}_n det \begin{pmatrix} M^1_{m_1} & ... & M^1_{m_n} \\ ... \\ M^n_{m_1} & ... & M^n_{m_n} \end{pmatrix}\).
Step 3:
\(det \begin{pmatrix} M^1_{m_1} & ... & M^1_{m_n} \\ ... \\ M^n_{m_1} & ... & M^n_{m_n} \end{pmatrix}\) is nonzero only when \((m_1, ..., m_n)\) is distinct, by a property of determinant of square matrix over commutative ring: otherwise, it would have some duplicate columns.
So, as far as the nonzero terms are concerned, \((m_1, ..., m_n)\) is a permutation of \((1, ..., n)\), so, we need only \(\sum_{\sigma \in S_n}\) in \(\sum_{m_1, ..., m_n \in \{1, ..., n\}}\).
Step 4:
\(det (M M') = \sum_{\sigma \in S_n} M'^{\sigma_1}_1 ... M'^{\sigma_n}_n det \begin{pmatrix} M^1_{\sigma_1} & ... & M^1_{\sigma_n} \\ ... \\ M^n_{\sigma_1} & ... & M^n_{\sigma_n} \end{pmatrix}\).
But \(det \begin{pmatrix} M^1_{\sigma_1} & ... & M^1_{\sigma_n} \\ ... \\ M^n_{\sigma_1} & ... & M^n_{\sigma_n} \end{pmatrix} = sgn \sigma det \begin{pmatrix} M^1_1 & ... & M^1_n \\ ... \\ M^n_1 & ... & M^n_n \end{pmatrix}\), by a property of determinant of square matrix over commutative ring.
So, \(det (M M') = \sum_{\sigma \in S_n} M'^{\sigma_1}_1 ... M'^{\sigma_n}_n sgn \sigma det \begin{pmatrix} M^1_1 & ... & M^1_n \\ ... \\ M^n_1 & ... & M^n_n \end{pmatrix} = det M' det M\).
