行列¶

Matrix m n R は，行添字 m，列添字 n，成分型 R の行列です．自然数ではなく任意の有限型で添字づけられる点が，紙の数学と少し違います． Fin m を使うと，通常の m 行 n 列行列を表せます．

#check Matrix
#check Matrix.of
#check Matrix.det
#check Matrix.toLin

section Matrices

variable {K : Type*} [Field K]

example (A B : Matrix (Fin 2) (Fin 3) K) (i : Fin 2) (j : Fin 3) :
    (A + B) i j = A i j + B i j := by
  rfl

example (A : Matrix (Fin 2) (Fin 3) K) (i : Fin 3) (j : Fin 2) :
    Aᵀ i j = A j i := by
  rfl

example (A : Matrix (Fin 2) (Fin 3) K) (v : Fin 3 → K) (i : Fin 2) :
    (A *ᵥ v) i = ∑ j, A i j * v j := by
  rfl

example : Matrix.det (1 : Matrix (Fin 2) (Fin 2) K) = 1 := by
  simp

end Matrices

行列は成分を計算したいときに便利です．一方，抽象的な線形代数の証明では LinearMap を使う方が自然です．基底を固定すると，線形写像と行列を対応させることができます．

演習問題¶

Matrix (Fin 2) (Fin 2) K の単位行列の行列式が 1 であることを，simp 以外の方法でも調べてください．
```
-- 解答例: `Matrix.det_one` が単位行列の行列式を述べる定理です．
#check Matrix.det_one
```

行列と線形写像の橋渡しとして Matrix.toLin の型を読み，どこで基底が必要になるか説明してください．

-- 解答例: `Matrix.toLin` は，始域と終域の基底を使って行列を線形写像に変換します．
#check Matrix.toLin