English
There is a Lie algebra equivalence typeBEquivSo' between typeB l R and so'(Sum Unit l) l R, for invertible 2 in R.
Русский
Существует эквивалентность Ли-алгебр typeB l R ≃ so'(Sum Unit l) l R при инвертируемости 2 в R.
LaTeX
$$$ typeBEquivSo'(l,R) : typeB(l,R) \simeq_{R} so'(Sum Unit l, l; R). $$$
Lean4
/-- An equivalence between two possible definitions of the classical Lie algebra of type B. -/
noncomputable def typeBEquivSo' [Invertible (2 : R)] : typeB l R ≃ₗ⁅R⁆ so' (Unit ⊕ l) l R :=
by
apply (skewAdjointMatricesLieSubalgebraEquiv (JB l R) (PB l R) (by infer_instance)).trans
symm
apply
(skewAdjointMatricesLieSubalgebraEquivTranspose (indefiniteDiagonal (Sum Unit l) l R)
(Matrix.reindexAlgEquiv _ _ (Equiv.sumAssoc PUnit l l)) (Matrix.transpose_reindex _ _)).trans
apply LieEquiv.ofEq
ext A
rw [jb_transform, ← val_unitOfInvertible (2 : R), ← Units.smul_def, LieSubalgebra.mem_coe, LieSubalgebra.mem_coe,
mem_skewAdjointMatricesLieSubalgebra_unit_smul]
simp [indefiniteDiagonal_assoc, S]
