Dual bases for the Killing form

For a Lie algebra with nondegenerate Killing form, every basis has a Killing-dual basis. This file develops its coordinate equations and the canonical basis-independent contraction of a bilinear map against a basis and its Killing dual.

Main definitions

• Ado.killingDualBasis: the basis dual to a given one under the Killing form.

Main results

• Ado.sum_killingForm_killingDualBasis_eq_trace: contraction against a Killing-dual basis computes the trace.
• Ado.sum_apply_killingDualBasis_eq: contraction of a bilinear map against a basis and its Killing dual is independent of the basis.
• Ado.sum_apply_killingDualBasis_of_isAdjointPair: a Killing-adjoint pair may be moved between the two slots of the contraction.
• Ado.sum_apply_lie_killingDualBasis_add_eq_zero: the canonical contraction is invariant under the adjoint action.

The Killing-dual basis

noncomputable def Ado.killingDualBasis {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] {ι : Type u_1} [DecidableEq ι] [Fintype ι] (b : Module.Basis ι K L) : Module.Basis ι K L

The basis of L dual to b under the Killing form: κ (b i) (killingDualBasis b j) is 1 when i = j and 0 otherwise (Ado.killingForm_killingDualBasis).

Equations

• Ado.killingDualBasis b = (killingForm K L).dualBasis ⋯ b

@[simp]

theorem Ado.killingForm_killingDualBasis {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] {ι : Type u_1} [DecidableEq ι] [Fintype ι] (b : Module.Basis ι K L) (i j : ι) : ((killingForm K L) (b i)) ((killingDualBasis b) j) = if i = j then 1 else 0

The defining biorthogonality of the Killing-dual basis.

@[simp]

theorem Ado.killingForm_killingDualBasis_left {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] {ι : Type u_1} [DecidableEq ι] [Fintype ι] (b : Module.Basis ι K L) (i j : ι) : ((killingForm K L) ((killingDualBasis b) i)) (b j) = if i = j then 1 else 0

The symmetric orientation of the defining biorthogonality of the Killing-dual basis.

@[simp]

theorem Ado.killingDualBasis_repr {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] {ι : Type u_1} [DecidableEq ι] [Fintype ι] (b : Module.Basis ι K L) (v : L) (i : ι) : ((killingDualBasis b).repr v) i = ((killingForm K L) (b i)) v

Coordinates in the Killing-dual basis are Killing pairings against b.

@[simp]

theorem Ado.killingDualBasis_killingDualBasis {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] {ι : Type u_1} [DecidableEq ι] [Fintype ι] (b : Module.Basis ι K L) : killingDualBasis (killingDualBasis b) = b

Conjugating twice returns the original basis: the Killing-dual basis of the Killing-dual basis of b is b.

theorem Ado.repr_eq_killingForm {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] {ι : Type u_1} [DecidableEq ι] [Fintype ι] (b : Module.Basis ι K L) (v : L) (i : ι) : (b.repr v) i = ((killingForm K L) v) ((killingDualBasis b) i)

Coordinates in b are Killing pairings against the Killing-dual basis.

theorem Ado.sum_killingForm_smul_basis {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] {ι : Type u_1} [DecidableEq ι] [Fintype ι] (b : Module.Basis ι K L) (v : L) : ∑ i : ι, ((killingForm K L) v) ((killingDualBasis b) i) • b i = v

Expansion in b, with the coefficients read off by the Killing-dual basis.

theorem Ado.sum_killingForm_smul_killingDualBasis {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] {ι : Type u_1} [DecidableEq ι] [Fintype ι] (b : Module.Basis ι K L) (v : L) : ∑ i : ι, ((killingForm K L) (b i)) v • (killingDualBasis b) i = v

Expansion in the Killing-dual basis, with the coefficients read off by b.

theorem Ado.sum_killingForm_killingDualBasis_eq_trace {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] {ι : Type u_1} [DecidableEq ι] [Fintype ι] (b : Module.Basis ι K L) (p : L →ₗ[K] L) : ∑ i : ι, ((killingForm K L) (p (b i))) ((killingDualBasis b) i) = (LinearMap.trace K L) p

The sum ∑ᵢ κ (p xᵢ) yᵢ along a basis and its Killing-dual basis is the trace of p. The Killing-dual basis reads off the coordinates in b (Ado.repr_eq_killingForm), so the sum is the sum of the diagonal entries of the matrix of p.

The canonical invariant element ∑ᵢ xᵢ ⊗ yᵢ

theorem Ado.sum_apply_killingDualBasis_eq {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] {W : Type w} [AddCommGroup W] [Module K W] (f : L →ₗ[K] L →ₗ[K] W) {ι : Type u_1} {ι' : Type u_2} [DecidableEq ι] [Fintype ι] [DecidableEq ι'] [Fintype ι'] (b : Module.Basis ι K L) (c : Module.Basis ι' K L) : ∑ i : ι, (f (b i)) ((killingDualBasis b) i) = ∑ j : ι', (f (c j)) ((killingDualBasis c) j)

The sum ∑ᵢ f xᵢ yᵢ of a bilinear map along a basis and its Killing-dual basis does not depend on the basis. Expanding each c j in the basis b produces exactly the coefficients that expand killingDualBasis b i in killingDualBasis c.

theorem Ado.sum_apply_killingDualBasis_of_isAdjointPair {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] {W : Type w} [AddCommGroup W] [Module K W] (f : L →ₗ[K] L →ₗ[K] W) {ι : Type u_1} [DecidableEq ι] [Fintype ι] (b : Module.Basis ι K L) {p q : L →ₗ[K] L} (hpq : LinearMap.IsAdjointPair (killingForm K L) (killingForm K L) ⇑p ⇑q) : ∑ i : ι, (f (p (b i))) ((killingDualBasis b) i) = ∑ i : ι, (f (b i)) (q ((killingDualBasis b) i))

A Killing-adjoint pair of operators may be moved from one slot to the other. If κ (p x) y is κ x (q y) then applying p to the basis vectors and applying q to their Killing duals give the same sum, because both expand to ∑ᵢ ∑ⱼ κ (p xᵢ) yⱼ • f xⱼ yᵢ.

theorem Ado.sum_apply_lie_killingDualBasis_add_eq_zero {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] {W : Type w} [AddCommGroup W] [Module K W] (f : L →ₗ[K] L →ₗ[K] W) {ι : Type u_1} [DecidableEq ι] [Fintype ι] (b : Module.Basis ι K L) (z : L) : ∑ i : ι, (f ⁅z, b i⁆) ((killingDualBasis b) i) + ∑ i : ι, (f (b i)) ⁅z, (killingDualBasis b) i⁆ = 0

The element ∑ᵢ xᵢ ⊗ yᵢ is invariant under the adjoint action. Read through a bilinear map f, the Leibniz expansion of the adjoint action of z vanishes, because the two coefficient families it produces are negatives of each other by the invariance of the Killing form.