コミュータティブ（可換）リング（環）上方にて、スクウェアマトリックス（正方行列）たちのプロダクト（積）のデターミナント（行列式）はマトリックス（行列）たちのデターミナント（行列式）たちのプロダクト（積）であることの記述/証明
話題
About: マトリックス（行列）たちスペース（空間）
この記事の目次
開始コンテキスト
- 読者は、リング（環）上方のスクウェアマトリックス（正方行列）のデターミナント（行列式）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意のコミュータティブ（可換）リング（環）上方にて、任意のスクウェアマトリックス（正方行列）たちのプロダクト（積）のデターミナント（行列式）は当該マトリックス（行列）たちのデターミナント（行列式）たちのプロダクト（積）であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(R\): \(\in \{\text{ 全てのコミュータティブ（可換）リング（環）たち }\}\)
\(n\): \(\in \mathbb{N} \setminus \{0\}\)
\(M\): \(\in \{\text{ 全ての } n \times n R \text{ マトリックス（行列）たち }\}\)
\(M'\): \(\in \{\text{ 全ての } n \times n R \text{ マトリックス（行列）たち }\}\)
//
ステートメント（言明）たち:
\(det (M M') = det M det M'\)
//
2: 証明
全体戦略: ステップ1: \(M M'\)の各列はいくつかの列たちの合計であることを見て、\(det M M'\)を分解して、対応するデターミナント（行列式）たちの合計とする; ステップ2: 各デターミナント（行列式）の各列はあるファクター（因子）を持つことを見て、当該ファクター（因子）を当該デターミナント（行列式）の外に取り出す; ステップ3: あるデターミナント（行列式）は、当該インデックスたちコンビネーションが互いに異なる時のみ非ゼロであることを見て、非ゼロ項たちのみを残す; ステップ4: 本命題を結論する。
ステップ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}\)。
各列は\(\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}\): 単一インデックス\(m_l\)を使うことができる。
したがって、\(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}\)、コミュータティブ（可換）リング（環）上方のスクウェアマトリックス（正方行列）のデターミナント（行列式）のあるプロパティによって。
ステップ2:
各デターミナント（行列式）の各\(l\)-番目列は\(M'^{m_l}_l\)ファクター（因子）を持つ、それは、当該デターミナント（行列式）の外へ取り出すことができる、コミュータティブ（可換）リング（環）上方のスクウェアマトリックス（正方行列）のデターミナント（行列式）のあるプロパティによって、したがって、\(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}\)。
ステップ3:
\(det \begin{pmatrix} M^1_{m_1} & ... & M^1_{m_n} \\ ... \\ M^n_{m_1} & ... & M^n_{m_n} \end{pmatrix}\)は、\((m_1, ..., m_n)\)が互いに異なる時のみ非ゼロである、コミュータティブ（可換）リング（環）上方のスクウェアマトリックス（正方行列）のデターミナント（行列式）のあるプロパティによって: そうでなければ、それは重複列たちを持つことになる。
したがって、非ゼロ項たちに関する限り、\((m_1, ..., m_n)\)は\((1, ..., n)\)のあるパーミュテーション（並べ替え）である、したがって、私たちは、\(\sum_{m_1, ..., m_n \in \{1, ..., n\}}\)の中で\(\sum_{\sigma \in S_n}\)だけを必要とする。
ステップ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}\)。
しかし、\(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}\)、コミュータティブ（可換）リング（環）上方のスクウェアマトリックス（正方行列）のデターミナント（行列式）のあるプロパティによって。
したがって、\(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\)。
