English
An isomorphism of modules that transports a bilinear form B to a conjugate form B' induces a Lie algebra equivalence between the corresponding skew-adjoint Lie subalgebras.
Русский
Изоморфизм модулей, переводящий билинейную форму B в сопряжённую форму B', порождает эквивалентность Ли-подалгебр кососопряжённых относительно этих форм.
LaTeX
$$There exists a LieEquiv between \(skewAdjointLieSubalgebra\, (B.compl_{12} (e) e)\) and \(skewAdjointLieSubalgebra\, B\) induced by the isomorphism e, i.e., a Lie algebra isomorphism coming from conjugation by e.$$
Lean4
/-- An equivalence of modules with bilinear forms gives equivalence of Lie algebras of skew-adjoint
endomorphisms. -/
def skewAdjointLieSubalgebraEquiv :
skewAdjointLieSubalgebra (B.compl₁₂ (e : N →ₗ[R] M) e) ≃ₗ⁅R⁆ skewAdjointLieSubalgebra B :=
by
apply LieEquiv.ofSubalgebras _ _ e.lieConj
ext f
simp only [Submodule.mem_map_equiv, LieSubalgebra.mem_map_submodule]
exact (LinearMap.isPairSelfAdjoint_equiv (B := -B) (F := B) e f).symm
