English
Given a matrix M with nonzero bottom-right entry, applying the left product of the first k transvections from listTransvecCol M does not change the last row in the sense that the last row remains zero in the off-diagonal blocks after multiplication by the partial product.
Русский
При условии ненулевого нижнего правого элемента M, применение частичного левого умножения на первые k транспектаций из listTransvecCol M сохраняет последнюю строку в канонической форме блок-диагональности.
LaTeX
$$$\forall k, k \le r,\; (\forall i, ( (listTransvecCol\,M).drop\,k).prod * M)(inr\,unit)(inl\,i) = 0$$$
Lean4
/-- Inductive step for the reduction: if one knows that any size `r` matrix can be reduced to
diagonal form by elementary operations, then one deduces it for matrices over `Fin r ⊕ Unit`. -/
theorem exists_list_transvec_mul_mul_list_transvec_eq_diagonal_induction
(IH :
∀ M : Matrix (Fin r) (Fin r) 𝕜,
∃ (L₀ L₀' : List (TransvectionStruct (Fin r) 𝕜)) (D₀ : Fin r → 𝕜),
(L₀.map toMatrix).prod * M * (L₀'.map toMatrix).prod = diagonal D₀)
(M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) :
∃ (L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (D : Fin r ⊕ Unit → 𝕜),
(L.map toMatrix).prod * M * (L'.map toMatrix).prod = diagonal D :=
by
rcases exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec M with ⟨L₁, L₁', hM⟩
let M' := (L₁.map toMatrix).prod * M * (L₁'.map toMatrix).prod
let M'' := toBlocks₁₁ M'
rcases IH M'' with ⟨L₀, L₀', D₀, h₀⟩
set c := M' (inr unit) (inr unit)
refine ⟨L₀.map (sumInl Unit) ++ L₁, L₁' ++ L₀'.map (sumInl Unit), Sum.elim D₀ fun _ => M' (inr unit) (inr unit), ?_⟩
suffices
(L₀.map (toMatrix ∘ sumInl Unit)).prod * M' * (L₀'.map (toMatrix ∘ sumInl Unit)).prod =
diagonal (Sum.elim D₀ fun _ => c)
by simpa [M', c, Matrix.mul_assoc]
have : M' = fromBlocks M'' 0 0 (diagonal fun _ => c) :=
by
rw [← fromBlocks_toBlocks M', hM.1, hM.2]
rfl
rw [this]
simp [h₀]
