Invariant forms on finite products of perfect Lie algebras

An invariant bilinear form pairs distinct perfect factors to zero. Consequently an invariant symmetric form on a finite product of perfect Lie algebras is uniquely the sum of the pullbacks of its restrictions to the factors. TauCeti.LieModule.invariantFormsPiEquiv packages this as a linear equivalence, with forward and inverse evaluation formulas and a dimension formula. This describes the independent level parameters for semisimple current algebras.

The orthogonality argument uses only perfectness, not nondegeneracy of the form, characteristic zero, or simplicity of the factors.

References

• V. G. Kac, Infinite-Dimensional Lie Algebras, Chapter 7, for invariant forms and levels on semisimple current algebras.

theorem LinearMap.BilinForm.lieInvariant.apply_pi_single_eq_zero {ι : Type u_1} {R : Type u_2} {L : ι → Type u_3} [CommRing R] [DecidableEq ι] [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] {Φ : LinearMap.BilinForm R ((i : ι) → L i)} (hΦ : lieInvariant ((i : ι) → L i) Φ) {i j : ι} (hi : LieAlgebra.derivedSeries R (L i) 1 = ⊤) (hij : i ≠ j) (x : L i) (y : L j) : (Φ (Pi.single i x)) (Pi.single j y) = 0

An invariant form pairs a perfect factor to zero with every distinct factor. Symmetry of the form and perfectness of the second factor are not required.

def TauCeti.LieModule.invariantFormsPiRestrict {ι : Type u_1} {R : Type u_2} {L : ι → Type u_3} [CommRing R] [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [DecidableEq ι] (i : ι) : ↥(invariantForms R ((i : ι) → L i) ((i : ι) → L i)) →ₗ[R] ↥(invariantForms R (L i) (L i))

Restrict an invariant symmetric form on a product to a single factor.

@[simp]

theorem TauCeti.LieModule.invariantFormsPiRestrict_apply {ι : Type u_1} {R : Type u_2} {L : ι → Type u_3} [CommRing R] [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [DecidableEq ι] (i : ι) (Φ : ↥(invariantForms R ((i : ι) → L i) ((i : ι) → L i))) (x y : L i) : (↑((invariantFormsPiRestrict i) Φ) x) y = (↑Φ (Pi.single i x)) (Pi.single i y)

def TauCeti.LieModule.invariantFormsPiSum {ι : Type u_1} {R : Type u_2} {L : ι → Type u_3} [CommRing R] [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [Fintype ι] : ((i : ι) → ↥(invariantForms R (L i) (L i))) →ₗ[R] ↥(invariantForms R ((i : ι) → L i) ((i : ι) → L i))

Sum the pullbacks of invariant symmetric forms along the coordinate projections.

@[simp]

theorem TauCeti.LieModule.invariantFormsPiSum_apply {ι : Type u_1} {R : Type u_2} {L : ι → Type u_3} [CommRing R] [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [Fintype ι] (Φ : (i : ι) → ↥(invariantForms R (L i) (L i))) (x y : (i : ι) → L i) : (↑(invariantFormsPiSum Φ) x) y = ∑ i : ι, (↑(Φ i) (x i)) (y i)

@[simp]

theorem TauCeti.LieModule.invariantFormsPiRestrict_sum {ι : Type u_1} {R : Type u_2} {L : ι → Type u_3} [CommRing R] [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [Fintype ι] [DecidableEq ι] (Φ : (i : ι) → ↥(invariantForms R (L i) (L i))) (i : ι) : (invariantFormsPiRestrict i) (invariantFormsPiSum Φ) = Φ i

Restriction to a factor recovers the corresponding summand.

theorem TauCeti.LieModule.invariantForms_apply_eq_sum {ι : Type u_1} {R : Type u_2} {L : ι → Type u_3} [CommRing R] [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [Fintype ι] [DecidableEq ι] (hL : ∀ (i : ι), LieAlgebra.derivedSeries R (L i) 1 = ⊤) (Φ : ↥(invariantForms R ((i : ι) → L i) ((i : ι) → L i))) (x y : (i : ι) → L i) : (↑Φ x) y = ∑ i : ι, (↑Φ (Pi.single i (x i))) (Pi.single i (y i))

An invariant form on a finite product of perfect Lie algebras is the sum of its diagonal blocks. In particular it has no mixed terms.

@[simp]

theorem TauCeti.LieModule.invariantFormsPiSum_restrict {ι : Type u_1} {R : Type u_2} {L : ι → Type u_3} [CommRing R] [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [Fintype ι] [DecidableEq ι] (hL : ∀ (i : ι), ⁅⊤, ⊤⁆ = ⊤) (Φ : ↥(invariantForms R ((i : ι) → L i) ((i : ι) → L i))) : (invariantFormsPiSum fun (i : ι) => (invariantFormsPiRestrict i) Φ) = Φ

Summing the restrictions reconstructs a form on a finite product of perfect Lie algebras.

def TauCeti.LieModule.invariantFormsPiEquiv {ι : Type u_1} {R : Type u_2} {L : ι → Type u_3} [CommRing R] [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [Fintype ι] [DecidableEq ι] (hL : ∀ (i : ι), LieAlgebra.derivedSeries R (L i) 1 = ⊤) : ↥(invariantForms R ((i : ι) → L i) ((i : ι) → L i)) ≃ₗ[R] (i : ι) → ↥(invariantForms R (L i) (L i))

Invariant symmetric forms on a finite product of perfect Lie algebras are exactly families of invariant symmetric forms on its factors. The inverse sums coordinate pullbacks.

@[simp]

theorem TauCeti.LieModule.invariantFormsPiEquiv_apply {ι : Type u_1} {R : Type u_2} {L : ι → Type u_3} [CommRing R] [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [Fintype ι] [DecidableEq ι] (hL : ∀ (i : ι), LieAlgebra.derivedSeries R (L i) 1 = ⊤) (Φ : ↥(invariantForms R ((i : ι) → L i) ((i : ι) → L i))) (i : ι) : (invariantFormsPiEquiv hL) Φ i = (invariantFormsPiRestrict i) Φ

@[simp]

theorem TauCeti.LieModule.invariantFormsPiEquiv_symm_apply {ι : Type u_1} {R : Type u_2} {L : ι → Type u_3} [CommRing R] [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [Fintype ι] [DecidableEq ι] (hL : ∀ (i : ι), LieAlgebra.derivedSeries R (L i) 1 = ⊤) (Φ : (i : ι) → ↥(invariantForms R (L i) (L i))) : (invariantFormsPiEquiv hL).symm Φ = invariantFormsPiSum Φ

theorem TauCeti.LieModule.finrank_invariantForms_pi {ι : Type u_1} {L : ι → Type u_3} [(i : ι) → LieRing (L i)] [Fintype ι] {K : Type u_4} [Field K] [(i : ι) → LieAlgebra K (L i)] [∀ (i : ι), Module.Finite K ↥(invariantForms K (L i) (L i))] (hL : ∀ (i : ι), LieAlgebra.derivedSeries K (L i) 1 = ⊤) : Module.finrank K ↥(invariantForms K ((i : ι) → L i) ((i : ι) → L i)) = ∑ i : ι, Module.finrank K ↥(invariantForms K (L i) (L i))

The dimension of invariant symmetric forms on a finite product of perfect Lie algebras is the sum of the dimensions for its factors.