lieCharacterEquivLinearDual — Mathlib

English

For an abelian Lie algebra L, characters are in natural one-to-one correspondence with linear functionals on L.

Русский

Для абелевой алгебры Ли характеры естественно соответствуют линейным функцияалам на L.

LaTeX

$$$$ \operatorname{LieCharacter}(R,L) \cong \operatorname{Module.Dual}(R,L) \quad \text{if } L \text{ is abelian}. $$$$

Lean4

/-- For an Abelian Lie algebra, characters are just linear forms. -/
@[simps! apply symm_apply]
def lieCharacterEquivLinearDual [IsLieAbelian L] : LieCharacter R L ≃ Module.Dual R L
    where
  toFun χ := (χ : L →ₗ[R] R)
  invFun
    ψ :=
    { ψ with
      map_lie' := fun {x y} => by
        rw [LieModule.IsTrivial.trivial, LieRing.of_associative_ring_bracket, mul_comm, sub_self,
          LinearMap.toFun_eq_coe, LinearMap.map_zero] }

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