English
The orthogonal of a bilinear form Φ with respect to a Lie submodule N coincides with the orthogonal defined on submodules: the two notions are the same when viewed as submodules of M.
Русский
Ортогональность относительно подмодуля N совпадает с ортогональностью как подмодуля: две концепции совпадают на основании подмодуля M.
LaTeX
$$$$ (\text{orthogonal } \Phi \; h\Phi_{\text{inv}} \, N)^{\text{submodule}} = \Phi\text{.orthogonal } N^{\text{submodule}}. $$$$
Lean4
/-- The orthogonal complement of a Lie submodule `N` with respect to an invariant bilinear form `Φ` is
the Lie submodule of elements `y` such that `Φ x y = 0` for all `x ∈ N`.
-/
@[simps!]
def orthogonal (hΦ_inv : Φ.lieInvariant L) (N : LieSubmodule R L M) : LieSubmodule R L M
where
__ := Φ.orthogonal N
lie_mem
{x
y} :=
by
suffices (∀ n ∈ N, Φ n y = 0) → ∀ n ∈ N, Φ n ⁅x, y⁆ = 0 by
simpa only [LinearMap.BilinForm.isOrtho_def, -- and some default simp lemmas
AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, Submodule.mem_toAddSubmonoid,
LinearMap.BilinForm.mem_orthogonal_iff, LieSubmodule.mem_toSubmodule]
intro H a ha
rw [← neg_eq_zero, ← hΦ_inv]
exact H _ <| N.lie_mem ha
