English
There exists a decomposition of any matrix as a product of transvections, a diagonal, and transvections, i.e., M = (L.map toMatrix).prod * diagonal D * (L'.map toMatrix).prod for some L,L' and D.
Русский
Существует разложение любой матрицы как произведение транспектаций, диагонали и транспектаций: M = (L.map toMatrix).prod * diagonal D * (L'.map toMatrix).prod.
LaTeX
$$$\exists L\,L' : List (TransvectionStruct n 𝕜),\; D : n → 𝕜,\; M = (L.map toMatrix).prod * diagonal D * (L'.map toMatrix).prod$$$
Lean4
/-- Induction principle for matrices based on transvections: if a property is true for all diagonal
matrices, all transvections, and is stable under product, then it is true for all matrices. This is
the useful way to say that matrices are generated by diagonal matrices and transvections.
We state a slightly more general version: to prove a property for a matrix `M`, it suffices to
assume that the diagonal matrices we consider have the same determinant as `M`. This is useful to
obtain similar principles for `SLₙ` or `GLₙ`. -/
theorem diagonal_transvection_induction (P : Matrix n n 𝕜 → Prop) (M : Matrix n n 𝕜)
(hdiag : ∀ D : n → 𝕜, det (diagonal D) = det M → P (diagonal D))
(htransvec : ∀ t : TransvectionStruct n 𝕜, P t.toMatrix) (hmul : ∀ A B, P A → P B → P (A * B)) : P M :=
by
rcases exists_list_transvec_mul_diagonal_mul_list_transvec M with ⟨L, L', D, h⟩
have PD : P (diagonal D) := hdiag D (by simp [h])
suffices H :
∀ (L₁ L₂ : List (TransvectionStruct n 𝕜)) (E : Matrix n n 𝕜),
P E → P ((L₁.map toMatrix).prod * E * (L₂.map toMatrix).prod)
by
rw [h]
apply H L L'
exact PD
intro L₁ L₂ E PE
induction L₁ with
| nil =>
simp only [Matrix.one_mul, List.prod_nil, List.map]
induction L₂ generalizing E with
| nil => simpa
| cons t L₂ IH =>
simp only [← Matrix.mul_assoc, List.prod_cons, List.map]
apply IH
exact hmul _ _ PE (htransvec _)
| cons t L₁ IH =>
simp only [Matrix.mul_assoc, List.prod_cons, List.map] at IH ⊢
exact hmul _ _ (htransvec _) IH
