ωConjLieSubmodule — Mathlib

English

Define the ω-conjugation on Lie submodules: ωConjLieSubmodule N consists of elements x whose image under ω is in N.

Русский

Определим операцию ω-коньюгирования на Ли-подмодулях: ωConjLieSubmodule N состоит из элементов x, чьё изображение под ω лежит в N.

LaTeX

$$$\\omegaConjLieSubmodule\\, N := N^{\\omega} = \\{ x \\mid (\\omega b) \\cdot x ∈ N \\}$$$

Lean4

/-- The equivalence `x ↦ ωxω` as an operation on Lie submodules of the Geck construction. -/
def ωConjLieSubmodule : LieSubmodule R (lieAlgebra b) (b.support ⊕ ι → R)
    where
  __ := N.toSubmodule.comap (ω b).toLin'
  lie_mem A {x}
    hx := by
    let A' : lieAlgebra b := ⟨ωConj b _, ωConj_mem_of_mem A.property⟩
    suffices ⁅A', ω b *ᵥ x⁆ ∈ N by simpa [A', mul_assoc] using this
    exact LieSubmodule.lie_mem _ hx

Похожие утверждения