English
The indefinite diagonal is reindexed from blocks to the (Unit ⊕ l) ⊕ l arrangement: indefiniteDiagonal (Unit ⊕ l) l R = Matrix.reindexLieEquiv (Equiv.sumAssoc Unit l l).symm (Matrix.fromBlocks 1 0 0 (indefiniteDiagonal l l R)).
Русский
Неопределённая диагональ переводится в блочно-структуру через перестановку: indefiniteDiagonal (Unit ⊕ l) l R = reindex по sumAssoc от блока fromBlocks 1 0 0 indefiniteDiagonal(l,l,R).
LaTeX
$$$ \operatorname{indefiniteDiagonal}(Unit \oplus l, l, R) = \mathrm{Matrix.reindexLieEquiv}(\mathrm{Equiv.sumAssoc(Unit,l,l)}).symm \bigl( \mathrm{Matrix.fromBlocks}(1,0,0,\operatorname{indefiniteDiagonal}(l,l,R)) \bigr). $$$
Lean4
theorem indefiniteDiagonal_assoc :
indefiniteDiagonal (Unit ⊕ l) l R =
Matrix.reindexLieEquiv (Equiv.sumAssoc Unit l l).symm (Matrix.fromBlocks 1 0 0 (indefiniteDiagonal l l R)) :=
by
ext ⟨⟨i₁ | i₂⟩ | i₃⟩ ⟨⟨j₁ | j₂⟩ | j₃⟩ <;>
simp only [indefiniteDiagonal, Matrix.diagonal_apply, Equiv.sumAssoc_apply_inl_inl, Matrix.reindexLieEquiv_apply,
Matrix.submatrix_apply, Equiv.symm_symm, Matrix.reindex_apply, Sum.elim_inl, if_true, Matrix.one_apply_eq,
Matrix.fromBlocks_apply₁₁, Equiv.sumAssoc_apply_inl_inr, if_false, Matrix.fromBlocks_apply₁₂,
Matrix.fromBlocks_apply₂₁, Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr, Sum.elim_inr,
Sum.inl_injective.eq_iff, Sum.inr_injective.eq_iff, reduceCtorEq] <;>
congr 1
