English
A bilinear form Φ on a Lie algebra L is invariant if and only if it lies in the maximal trivial submodule of BilinForm R M under the action of L.
Русский
Билинейная форма Φ на Ли-алгебре L инвариантна тогда и только тогда, когда она принадлежит максимальному тривиальному подмодулю BilinForm под действием L.
LaTeX
$$$$ \text{lieInvariant}(L, \Phi) \iff \ \Phi \in \operatorname{maxTrivSubmodule}_{L}(\text{BilinForm}) . $$$$
Lean4
theorem _root_.LinearMap.BilinForm.lieInvariant_iff [LieAlgebra R L] [LieModule R L M] :
Φ.lieInvariant L ↔ Φ ∈ LieModule.maxTrivSubmodule R L (LinearMap.BilinForm R M) :=
by
refine ⟨fun h x ↦ ?_, fun h x y z ↦ ?_⟩
· ext y z
rw [LieHom.lie_apply, LinearMap.sub_apply, Module.Dual.lie_apply, LinearMap.zero_apply, LinearMap.zero_apply, h,
sub_self]
· replace h := LinearMap.congr_fun₂ (h x) y z
simp only [LieHom.lie_apply, LinearMap.sub_apply, Module.Dual.lie_apply, LinearMap.zero_apply, sub_eq_zero] at h
simp [← h]
