English
Over a ring containing an element i with i^2 = -1, there exists a Lie algebra isomorphism between the indefinite orthogonal Lie algebra so′(p,q;R) and the definite orthogonal Lie algebra so(p⊕q;R).
Русский
Пусть в кольце найдётся элемент i с i^2 = -1. Существует изоморфизм Ли-алгебр между бесконечно неопределимой ортогональной алгеброй so′(p,q;R) и определённой so(p⊕q;R).
LaTeX
$$$ soIndefiniteEquiv_{p,q,R,i} : so'(p,q;R) \cong_{R} so((p\oplus q);R).$$$$
Lean4
/-- An equivalence between the indefinite and definite orthogonal Lie algebras, over a ring
containing a square root of -1. -/
noncomputable def soIndefiniteEquiv {i : R} (hi : i * i = -1) : so' p q R ≃ₗ⁅R⁆ so (p ⊕ q) R :=
by
apply (skewAdjointMatricesLieSubalgebraEquiv (indefiniteDiagonal p q R) (Pso p q R i) (invertiblePso p q R hi)).trans
apply LieEquiv.ofEq
ext A; rw [indefiniteDiagonal_transform p q R hi]; rfl
