Basic lemmas for the split even orthogonal Lie algebra

This file records structural matrix lemmas for Mathlib's split type-D Lie algebra that do not depend on a choice of Cartan subalgebra or root system.

Main results

• Matrix.fromBlocks_mem_typeD: a block matrix [[A, B], [C, -Aᵀ]] belongs to the split type-D Lie algebra when its off-diagonal blocks are skew-symmetric.
• LieAlgebra.Orthogonal.typeD.apply_inr_inr, LieAlgebra.Orthogonal.typeD.apply_inl_inr, and LieAlgebra.Orthogonal.typeD.apply_inr_inl: the three block relations satisfied by a type-D matrix.

theorem Matrix.fromBlocks_mem_typeD {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (A B C : Matrix ι ι K) (hB : B.transpose = -B) (hC : C.transpose = -C) : fromBlocks A B C (-A.transpose) ∈ LieAlgebra.Orthogonal.typeD ι K

A block matrix [[A, B], [C, -Aᵀ]] belongs to the split type-D Lie algebra when its off-diagonal blocks are skew-symmetric.

@[simp]

theorem LieAlgebra.Orthogonal.typeD.apply_inr_inr {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (A : ↥(typeD ι K)) (i j : ι) : ↑A (Sum.inr i) (Sum.inr j) = -↑A (Sum.inl j) (Sum.inl i)

In a type-D matrix, the lower-right block is the negative transpose of the upper-left block.

theorem LieAlgebra.Orthogonal.typeD.apply_inl_inr {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (A : ↥(typeD ι K)) (i j : ι) : ↑A (Sum.inl i) (Sum.inr j) = -↑A (Sum.inl j) (Sum.inr i)

In a type-D matrix, the upper-right block is skew-symmetric.

theorem LieAlgebra.Orthogonal.typeD.apply_inr_inl {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (A : ↥(typeD ι K)) (i j : ι) : ↑A (Sum.inr i) (Sum.inl j) = -↑A (Sum.inr j) (Sum.inl i)

In a type-D matrix, the lower-left block is skew-symmetric.