English
An auxiliary induction lemma: given the diagonal induction lemma for Fin r, one can extend it to Fin r ⊕ Unit by using the block decomposition and transvections to finish the diagonal reduction.
Русский
Дополнительная лемма индукции по диагоналям: имея диагональную индукцию для Fin r, её можно расширить до Fin r ⊕ Unit, используя блочную декомпозицию и транспектации.
LaTeX
$$$\exists L,L',D : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜),\; (L.map toMatrix).prod * M * (L'.map toMatrix).prod = diagonal D$$$
Lean4
/-- Any matrix can be written as the product of transvections, a diagonal matrix, and
transvections. -/
theorem exists_list_transvec_mul_diagonal_mul_list_transvec (M : Matrix n n 𝕜) :
∃ (L L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
M = (L.map toMatrix).prod * diagonal D * (L'.map toMatrix).prod :=
by
rcases exists_list_transvec_mul_mul_list_transvec_eq_diagonal M with ⟨L, L', D, h⟩
refine ⟨L.reverse.map TransvectionStruct.inv, L'.reverse.map TransvectionStruct.inv, D, ?_⟩
suffices
M =
(L.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod * (L.map toMatrix).prod * M *
((L'.map toMatrix).prod * (L'.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod)
by simpa [← h, Matrix.mul_assoc]
rw [reverse_inv_prod_mul_prod, prod_mul_reverse_inv_prod, Matrix.one_mul, Matrix.mul_one]
