English
Equality of two skew-adjoint Lie subalgebras under the equivalence map derived from an isomorphism of matrix algebras.
Русский
Равенство двух Ли-подалгебр кососопряжённых под действием эквивалентности производной из изоморфизма алгебр матриц.
LaTeX
$$Eq (skewAdjointMatricesLieSubalgebra J) (skewAdjointMatricesLieSubalgebra (P^T J P)) under the induced equivalence.$$
Lean4
/-- An equivalence of matrix algebras commuting with the transpose endomorphisms restricts to an
equivalence of Lie algebras of skew-adjoint matrices. -/
def skewAdjointMatricesLieSubalgebraEquivTranspose {m : Type w} [DecidableEq m] [Fintype m]
(e : Matrix n n R ≃ₐ[R] Matrix m m R) (h : ∀ A, (e A)ᵀ = e Aᵀ) :
skewAdjointMatricesLieSubalgebra J ≃ₗ⁅R⁆ skewAdjointMatricesLieSubalgebra (e J) :=
LieEquiv.ofSubalgebras _ _ e.toLieEquiv <| by
ext A
suffices J.IsSkewAdjoint (e.symm A) ↔ (e J).IsSkewAdjoint A by
simpa [-LieSubalgebra.mem_map, LieSubalgebra.mem_map_submodule]
simp only [Matrix.IsSkewAdjoint, Matrix.IsAdjointPair, ← h, ← Function.Injective.eq_iff e.injective, map_mul,
AlgEquiv.apply_symm_apply, map_neg]
