English
An invertible change of basis induces a Lie algebra equivalence between the skew-adjoint Lie subalgebras before and after the conjugation.
Русский
Обратимый переход по базису порождает эквивалентность Ли-подалгебр до и после конъюгации.
LaTeX
$$There is a LieEquiv between skewAdjointMatricesLieSubalgebra J and skewAdjointMatricesLieSubalgebra (P^T J P) induced by conjugation by P.$$
Lean4
/-- An invertible matrix `P` gives a Lie algebra equivalence between those endomorphisms that are
skew-adjoint with respect to a square matrix `J` and those with respect to `PᵀJP`. -/
def skewAdjointMatricesLieSubalgebraEquiv (P : Matrix n n R) (h : Invertible P) :
skewAdjointMatricesLieSubalgebra J ≃ₗ⁅R⁆ skewAdjointMatricesLieSubalgebra (Pᵀ * J * P) :=
LieEquiv.ofSubalgebras _ _ (P.lieConj h).symm <| by
ext A
suffices P.lieConj h A ∈ skewAdjointMatricesSubmodule J ↔ A ∈ skewAdjointMatricesSubmodule (Pᵀ * J * P)
by
simp only [Submodule.mem_map_equiv, LieSubalgebra.mem_map_submodule]
exact this
simp [Matrix.IsSkewAdjoint, J.isAdjointPair_equiv _ _ P (isUnit_of_invertible P)]
