English
There exist L and L' such that the left-right product with transvection matrices yields a matrix that is block-diagonal.
Русский
Существуют L и L' такие, что левостороннее и правостороннее произведение транспектаций приводит к блочно-диагональной форме.
LaTeX
$$$\exists L\,L' : List (TransvectionStruct n 𝕜),\; (L.map toMatrix).prod * M * (L'.map toMatrix).prod = IsTwoBlockDiagonal$$$
Lean4
/-- There exist two lists of `TransvectionStruct` such that multiplying by them on the left and
on the right makes a matrix block-diagonal. -/
theorem exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) :
∃ L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜),
IsTwoBlockDiagonal ((L.map toMatrix).prod * M * (L'.map toMatrix).prod) :=
by
by_cases H : IsTwoBlockDiagonal M
·
refine
⟨List.nil, List.nil, by simpa using H⟩
-- we have already proved this when the last coefficient is nonzero
by_cases hM : M (inr unit) (inr unit) ≠ 0
· exact exists_isTwoBlockDiagonal_of_ne_zero M hM
push_neg at hM
simp only [not_and_or, IsTwoBlockDiagonal, toBlocks₁₂, toBlocks₂₁, ← Matrix.ext_iff] at H
have : ∃ i : Fin r, M (inl i) (inr unit) ≠ 0 ∨ M (inr unit) (inl i) ≠ 0 :=
by
rcases H with H | H
· contrapose! H
rintro i ⟨⟩
exact (H i).1
· contrapose! H
rintro ⟨⟩ j
exact (H j).2
rcases this with ⟨i, h | h⟩
· let M' := transvection (inr Unit.unit) (inl i) 1 * M
have hM' : M' (inr unit) (inr unit) ≠ 0 := by simpa [M', hM]
rcases exists_isTwoBlockDiagonal_of_ne_zero M' hM' with ⟨L, L', hLL'⟩
rw [Matrix.mul_assoc] at hLL'
refine ⟨L ++ [⟨inr unit, inl i, by simp, 1⟩], L', ?_⟩
simp only [List.map_append, List.prod_append, Matrix.mul_one, toMatrix_mk, List.prod_cons, List.prod_nil, List.map,
Matrix.mul_assoc (L.map toMatrix).prod]
exact hLL'
· let M' := M * transvection (inl i) (inr unit) 1
have hM' : M' (inr unit) (inr unit) ≠ 0 := by simpa [M', hM]
rcases exists_isTwoBlockDiagonal_of_ne_zero M' hM' with ⟨L, L', hLL'⟩
refine ⟨L, ⟨inl i, inr unit, by simp, 1⟩ :: L', ?_⟩
simp only [← Matrix.mul_assoc, toMatrix_mk, List.prod_cons, List.map]
rw [Matrix.mul_assoc (L.map toMatrix).prod]
exact hLL'
