English
Every matrix M can be expressed as a product of transvections, a diagonal matrix, and transvections again, i.e., M = (L.map toMatrix).prod * diagonal D * (L'.map toMatrix).prod for some L, L' and D.
Русский
Каждая матрица M может быть представлена как произведение транспектаций, диагональной матрицы и транспектаций снова: 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
/-- Reduction to diagonal form by elementary operations is invariant under reindexing. -/
theorem reindex_exists_list_transvec_mul_mul_list_transvec_eq_diagonal (M : Matrix p p 𝕜) (e : p ≃ n)
(H :
∃ (L L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
(L.map toMatrix).prod * Matrix.reindexAlgEquiv 𝕜 _ e M * (L'.map toMatrix).prod = diagonal D) :
∃ (L L' : List (TransvectionStruct p 𝕜)) (D : p → 𝕜),
(L.map toMatrix).prod * M * (L'.map toMatrix).prod = diagonal D :=
by
rcases H with ⟨L₀, L₀', D₀, h₀⟩
refine ⟨L₀.map (reindexEquiv e.symm), L₀'.map (reindexEquiv e.symm), D₀ ∘ e, ?_⟩
have : M = reindexAlgEquiv 𝕜 _ e.symm (reindexAlgEquiv 𝕜 _ e M) := by
simp only [Equiv.symm_symm, submatrix_submatrix, reindex_apply, submatrix_id_id, Equiv.symm_comp_self,
reindexAlgEquiv_apply]
rw [this]
simp only [toMatrix_reindexEquiv_prod, List.map_map, reindexAlgEquiv_apply]
simp only [← reindexAlgEquiv_apply 𝕜, ← reindexAlgEquiv_mul, h₀]
simp only [Equiv.symm_symm, reindex_apply, submatrix_diagonal_equiv, reindexAlgEquiv_apply]
