English
There is a Lie algebra isomorphism between typeD and so' defined via a skew adjoint subalgebra equivalence, compatible with the JD/PD pair.
Русский
Существует изоморфизм Ли-алгебр между typeD и so', задаваемый через эквивалентность косо-сопряжённых подалгебр и совместимость с парами JD/PD.
LaTeX
$$$ typeDEquivSo'(l,R) : typeD(l,R) \simeq_{R} so'(l,l;R). $$$
Lean4
/-- An equivalence between two possible definitions of the classical Lie algebra of type D. -/
noncomputable def typeDEquivSo' [Fintype l] [Invertible (2 : R)] : typeD l R ≃ₗ⁅R⁆ so' l l R :=
by
apply (skewAdjointMatricesLieSubalgebraEquiv (JD l R) (PD l R) (by infer_instance)).trans
apply LieEquiv.ofEq
ext A
rw [jd_transform, ← val_unitOfInvertible (2 : R), ← Units.smul_def, LieSubalgebra.mem_coe,
mem_skewAdjointMatricesLieSubalgebra_unit_smul]
rfl
