English
The matrix of a composition equals the product of the matrices, in reverse order.
Русский
Матрица композиции равна произведению матриц в обратном порядке.
LaTeX
$$$$ o.matrixDecomposition(z \\gg w)(i) = o.matrixDecomposition(w)(i) \\; o.matrixDecomposition(z)(i). $$$$
Lean4
theorem matrixDecomposition_comp (o : HomOrthogonal s) {α β γ : Type} [Finite α] [Fintype β] [Finite γ] {f : α → ι}
{g : β → ι} {h : γ → ι} (z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b))
(w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)) (i : ι) :
o.matrixDecomposition (z ≫ w) i = o.matrixDecomposition w i * o.matrixDecomposition z i :=
by
ext ⟨c, ⟨⟩⟩ ⟨a, j_property⟩
simp only [Set.mem_preimage, Set.mem_singleton_iff] at j_property
simp only [Matrix.mul_apply, Limits.biproduct.components, HomOrthogonal.matrixDecomposition_apply, Category.comp_id,
Category.id_comp, Category.assoc, End.mul_def, eqToHom_refl, eqToHom_trans_assoc]
conv_lhs => rw [← Category.id_comp w, ← biproduct.total]
simp only [Preadditive.sum_comp, Preadditive.comp_sum]
apply Finset.sum_congr_set
· simp
· intro b nm
simp only [Set.mem_preimage, Set.mem_singleton_iff] at nm
simp only [Category.assoc]
convert comp_zero
convert comp_zero
convert comp_zero
convert comp_zero
simp only [o.eq_zero nm]
