\(n \times n\)フィールド（体）マトリックス（行列）たちのリング（環）に対して、もしも、要素に別要素を左または右から掛けたものが\(1\)である場合、別要素はインバース（逆）であることの記述/証明
話題
About: リング（環）
この記事の目次
開始コンテキスト
- 読者は、\(n \times n\)リング（環）マトリックス（行列）たちのリング（環）の定義を知っている。
- 読者は、任意のリング（環）に対して、もしも、任意の要素があるインバース（逆）を持ち当該要素に任意の別要素を左または右から掛けたものが\(1\)である場合、当該別要素が唯一インバース（逆）であるという命題を認めている。
- 読者は、任意のコミュータティブ（可換）リング（環）上方にて、任意のスクウェアマトリックス（正方行列）たちのプロダクト（積）のデターミナント（行列式）は当該マトリックス（行列）たちのデターミナント（行列式）たちのプロダクト（積）であるという命題を認めている。
- 読者は、任意のフィールド（体）上方にて、任意のスクウェアマトリックス（正方行列）はインバース（逆）を持つ、もしも、そのデターミナント（行列式）が非ゼロである場合、そしてその場合に限って、そして、インバース（逆）はこれであるという命題を認めている。
ターゲットコンテキスト
- 読者は、任意の、\(n \times n\)フィールド（体）マトリックス（行列）たちのリング（環）に対して、もしも、任意の要素に任意の別要素を左または右から掛けたものが\(1\)である場合、当該別要素はインバース（逆）であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(F\): \(\in \{\text{ 全てのフィールド（体）たち }\}\)
\(n\): \(\in \mathbb{N} \setminus \{0\}\)
\(M_n (F)\): \(= n \times n F \text{ マトリックス（行列）たちのリング（環） }\)
\(M\): \(\in M_n (F)\)
//
ステートメント（言明）たち:
(
\(\exists M' \in M_n (F) (M' M = I)\)
\(\implies\)
\(M' = M^{- 1}\)
)
\(\land\)
(
\(\exists M' \in M_n (F) (M M' = I)\)
\(\implies\)
\(M' = M^{- 1}\)
)
//
2: 注
任意のリング（環）に対して、もしも、任意の要素があるインバース（逆）を持ち当該要素に任意の別要素を左または右から掛けたものが\(1\)である場合、当該別要素が唯一インバース（逆）であるという命題と比較のこと: 本命題に対しては、\(M\)は、インバーティブル（可逆）であると事前仮定する必要がない、それは、\(F\)があるフィールド（体）であることによる。
3: Proof
Whole Strategy: see that \(M\) is invertible and apply the proposition that for any ring, if any element has an inverse and the element multiplied by any another element from left or right is \(1\), the another element is the inverse; Step 1: suppose that \(M' M = I\); Step 2: take \(det (M' M) = det I\) and see that \(M\) is invertible; Step 3: suppose that \(M M' = I\); Step 4: take \(det (M M') = det I\) and see that \(M\) is invertible.
Step 1:
Let us suppose that \(M' M = I\).
Step 2:
\(det (M' M) = det I = 1\), but the left hand side is \(det M' det M\), by 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
So, \(det M \neq 0\).
\(M\) has an inverse, by the proposition that over any field, any square matrix has the inverse if and only if its determinant is nonzero, and the inverse is this.
So, by the proposition that for any ring, if any element has an inverse and the element multiplied by any another element from left or right is \(1\), the another element is the inverse, \(M' = M^{- 1}\).
Step 3:
Let us suppose that \(M M' = I\).
Step 4:
\(det (M M') = det I = 1\), but the left hand side is \(det M det M'\), by 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
So, \(det M \neq 0\).
\(M\) has an inverse, by the proposition that over any field, any square matrix has the inverse if and only if its determinant is nonzero, and the inverse is this.
So, by the proposition that for any ring, if any element has an inverse and the element multiplied by any another element from left or right is \(1\), the another element is the inverse, \(M' = M^{- 1}\).
