Skew-adjoint Lie algebras

A basis identifies matrices skew-adjoint for the Gram matrix of a bilinear form with endomorphisms skew-adjoint for the form itself. This file packages that identification as TauCeti.skewAdjointLieEquivOfBasis.

The adjoint action of a Lie algebra carrying an invariant bilinear form

A bilinear form B on a Lie algebra L is invariant when B ⁅x, y⁆ z = -B y ⁅x, z⁆ (LinearMap.BilinForm.lieInvariant). Read with x fixed, that equation says exactly that the endomorphism ad x is skew-adjoint for B: invariance of a form and skew-adjointness of the adjoint action are the same statement, transposed. So a Lie algebra with an invariant form maps to the Lie algebra of skew-adjoint endomorphisms of that form, by x ↦ ad x, and the map is a homomorphism because ad already is.

This file builds that homomorphism, TauCeti.LieAlgebra.adSkewAdjoint, against skewAdjointLieSubalgebra — Mathlib's 𝔰𝔬 of a bilinear form — and identifies the kernel of its polar-form specialization TauCeti.LieAlgebra.adjointSO with the centre. The two names differ only in their codomain: adSkewAdjoint lands in the skew-adjoint endomorphisms of B itself, while adjointSO, the roadmap-pinned map, lands in those of the polar form. The form the latter targets is not B itself but the polar form of the quadratic form x ↦ B x x, which is B + B.flip; that is the shape a Clifford algebra consumes, since the Clifford relation ι v * ι v = Q v polarizes to polar Q. For symmetric B the polar form is 2 • B; skew-adjointness for B always implies skew-adjointness for 2 • B, and the two conditions agree when 2 is invertible in R, but not in general. Stating the codomain against QuadraticMap.polarBilin avoids a factor of two travelling with every later use.

The motivating instance is the Killing form of a Lie algebra, whose quadratic form is TauCeti.LieAlgebra.killingQuadraticForm. It is invariant (LieModule.traceForm_lieInvariant) and symmetric, so ad maps L into the skew-adjoint endomorphisms of the polar form 2 • κ; when L is Killing-semisimple and 2 is invertible the form is moreover nondegenerate, which is the hypothesis under which the skew-adjoint endomorphisms are the quadratic elements of the Clifford algebra Cliff(L, κ) (CliffordAlgebra.soEquivQuadratic). Composing the two is the adjoint quadratic lift L → Cliff(L, κ) whose left-regular action is the subject of Kostant's isotypy theorem; that composite is not built here.

Main definitions

• TauCeti.skewAdjointLieEquivOfBasis: the basis transport from skew-adjoint matrices to skew-adjoint endomorphisms.
• TauCeti.LieAlgebra.adSkewAdjoint: the adjoint action of a Lie algebra carrying an invariant bilinear form B, as a Lie algebra homomorphism into the skew-adjoint endomorphisms of B.
• TauCeti.LieAlgebra.adjointSO: the same map read into the skew-adjoint endomorphisms of the polar form.
• TauCeti.LieAlgebra.killingQuadraticForm: the Killing form read as a quadratic form.

Main results

• TauCeti.mem_skewAdjointMatricesLieSubalgebra_toMatrix_iff: matrix skew-adjointness for a Gram matrix is equivalent to basis-free skew-adjointness.
• TauCeti.LieAlgebra.ad_mem_skewAdjointSubmodule: invariance of a form is skew-adjointness of the adjoint action.
• TauCeti.LieAlgebra.ker_adSkewAdjoint: the kernel of adSkewAdjoint is the centre, so the map is injective exactly when the centre is trivial (TauCeti.LieAlgebra.adSkewAdjoint_injective_iff); the same for the polar-form and Killing specializations (TauCeti.LieAlgebra.ker_adjointSO, TauCeti.LieAlgebra.ker_killingAdjointSO).
• TauCeti.LieAlgebra.polarBilin_killingQuadraticForm: the polar form of the Killing quadratic form is 2 • killingForm.
• TauCeti.LieAlgebra.killingQuadraticForm_nondegenerate: over a ring in which 2 is invertible, the Killing quadratic form of a Killing-semisimple Lie algebra is nondegenerate.
• Module.Basis.dualBasis_polarBilin_killingQuadraticForm_apply: the basis dual for the polar form is half the Killing-dual basis.

Implementation notes

The pinned signature in the roadmap's Suggested.lean carries a symmetry hypothesis on B and works over a field. Neither is used: invariance of B already forces invariance of B.flip (TauCeti.LieAlgebra.lieInvariant_flip), hence of the polar form B + B.flip, and the argument is a rearrangement of the invariance equation valid over any commutative ring. Symmetry is used only where it genuinely bites, in polarBilin_killingQuadraticForm, which is stated for the Killing form rather than hypothesised. Carrying an unused hypothesis on a def would in any case be rejected by the unusedArguments linter.

The polar form and nondegeneracy of the Killing quadratic form are the general facts LinearMap.BilinMap.polarBilin_toQuadraticMap_of_flip and LinearMap.BilinForm.Nondegenerate.toQuadraticMap of TauCeti/LinearAlgebra/QuadraticForm/Radical.lean applied to the Killing form, which is symmetric; nothing in either argument is about the Killing form.

The stability of invariance under flipping and addition is a statement about a form on any Lie module M over L, the generality in which Mathlib defines lieInvariant, and is stated that way here; only from ad_mem_skewAdjointSubmodule on, where the adjoint action enters, is the module L itself.

theorem TauCeti.mem_skewAdjointMatricesLieSubalgebra_toMatrix_iff {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {n : Type w} [Fintype n] [DecidableEq n] (b : Module.Basis n R M) (B : LinearMap.BilinForm R M) {J : Matrix n n R} (hJ : (LinearMap.BilinForm.toMatrix b) B = J) (f : Module.End R M) : (LinearMap.toMatrix b b) f ∈ skewAdjointMatricesLieSubalgebra J ↔ f ∈ skewAdjointLieSubalgebra B

An endomorphism is skew-adjoint for a bilinear form exactly when its matrix in a basis is skew-adjoint for the Gram matrix of the form.

noncomputable def TauCeti.skewAdjointLieEquivOfBasis {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {n : Type w} [Fintype n] [DecidableEq n] (b : Module.Basis n R M) (B : LinearMap.BilinForm R M) {J : Matrix n n R} (hJ : (LinearMap.BilinForm.toMatrix b) B = J) : ↥(skewAdjointMatricesLieSubalgebra J) ≃ₗ⁅R⁆ ↥(skewAdjointLieSubalgebra B)

A basis transports the Lie algebra of matrices skew-adjoint for a Gram matrix to the basis-free Lie algebra of skew-adjoint endomorphisms.

Equations

• TauCeti.skewAdjointLieEquivOfBasis b B hJ = LieEquiv.ofSubalgebras (skewAdjointMatricesLieSubalgebra J) (skewAdjointLieSubalgebra B) (Matrix.toLinAlgEquiv b).toLieEquiv ⋯

@[simp]

theorem TauCeti.coe_skewAdjointLieEquivOfBasis_apply {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {n : Type w} [Fintype n] [DecidableEq n] (b : Module.Basis n R M) (B : LinearMap.BilinForm R M) {J : Matrix n n R} (hJ : (LinearMap.BilinForm.toMatrix b) B = J) (A : ↥(skewAdjointMatricesLieSubalgebra J)) : ↑((skewAdjointLieEquivOfBasis b B hJ) A) = (Matrix.toLinAlgEquiv b) ↑A

The basis transport from skew-adjoint matrices acts by the corresponding matrix endomorphism.

theorem TauCeti.LieAlgebra.lieInvariant_flip {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] {B : LinearMap.BilinForm R M} (hB : LinearMap.BilinForm.lieInvariant L B) : LinearMap.BilinForm.lieInvariant L (LinearMap.flip B)

The flip of an invariant bilinear form is invariant: invariance is the equation B ⁅x, y⁆ z = -B y ⁅x, z⁆, and reading it with the roles of y and z exchanged is the same equation for the flip.

theorem TauCeti.LieAlgebra.lieInvariant_add {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] {B C : LinearMap.BilinForm R M} (hB : LinearMap.BilinForm.lieInvariant L B) (hC : LinearMap.BilinForm.lieInvariant L C) : LinearMap.BilinForm.lieInvariant L (B + C)

Invariance is preserved by sums, the two invariance equations adding termwise.

theorem TauCeti.LieAlgebra.lieInvariant_polarBilin {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] {B : LinearMap.BilinForm R M} (hB : LinearMap.BilinForm.lieInvariant L B) : LinearMap.BilinForm.lieInvariant L (LinearMap.BilinMap.toQuadraticMap B).polarBilin

The polar form of the quadratic form y ↦ B y y of an invariant B is again invariant: it is B + B.flip, and both summands are.

theorem TauCeti.LieAlgebra.ad_mem_skewAdjointSubmodule {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {B : LinearMap.BilinForm R L} (hB : LinearMap.BilinForm.lieInvariant L B) (x : L) : (LieAlgebra.ad R L) x ∈ LinearMap.skewAdjointSubmodule B

Invariance is skew-adjointness of the adjoint action. The invariance equation B ⁅x, y⁆ z = -B y ⁅x, z⁆, read with x held fixed, says that ad x is skew-adjoint for B.

def TauCeti.LieAlgebra.adSkewAdjoint {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (B : LinearMap.BilinForm R L) (hB : LinearMap.BilinForm.lieInvariant L B) : L →ₗ⁅R⁆ ↥(skewAdjointLieSubalgebra B)

The adjoint homomorphism ad : L →ₗ⁅R⁆ 𝔰𝔬(L, B) of a Lie algebra carrying an invariant bilinear form B: ad x is skew-adjoint for B, and ad is a Lie algebra homomorphism.

Equations

• TauCeti.LieAlgebra.adSkewAdjoint B hB = { toFun := fun (x : L) => ⟨(LieAlgebra.ad R L) x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

@[simp]

theorem TauCeti.LieAlgebra.coe_adSkewAdjoint {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (B : LinearMap.BilinForm R L) (hB : LinearMap.BilinForm.lieInvariant L B) (x : L) : ↑((adSkewAdjoint B hB) x) = (LieAlgebra.ad R L) x

adSkewAdjoint is ad with its codomain restricted: as an endomorphism of L it is ad x.

@[simp]

theorem TauCeti.LieAlgebra.ker_adSkewAdjoint {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (B : LinearMap.BilinForm R L) (hB : LinearMap.BilinForm.lieInvariant L B) : (adSkewAdjoint B hB).ker = LieAlgebra.center R L

The kernel of the adjoint homomorphism is the centre, since adSkewAdjoint is ad with its codomain restricted.

theorem TauCeti.LieAlgebra.adSkewAdjoint_injective_iff {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (B : LinearMap.BilinForm R L) (hB : LinearMap.BilinForm.lieInvariant L B) : Function.Injective ⇑(adSkewAdjoint B hB) ↔ LieAlgebra.center R L = ⊥

The adjoint homomorphism is injective exactly when the centre of L is trivial.

def TauCeti.LieAlgebra.adjointSO {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (B : LinearMap.BilinForm R L) (hB : LinearMap.BilinForm.lieInvariant L B) : L →ₗ⁅R⁆ ↥(skewAdjointLieSubalgebra (LinearMap.BilinMap.toQuadraticMap B).polarBilin)

The adjoint homomorphism read into the skew-adjoint endomorphisms of the polar form of x ↦ B x x, which is B + B.flip, and is 2 • B for symmetric B. Skew-adjointness for B implies skew-adjointness for the polar form, the converse needing 2 to be cancellable; the polar form is what the Clifford algebra of B sees.

Equations

• TauCeti.LieAlgebra.adjointSO B hB = TauCeti.LieAlgebra.adSkewAdjoint (LinearMap.BilinMap.toQuadraticMap B).polarBilin ⋯

@[simp]

theorem TauCeti.LieAlgebra.coe_adjointSO {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (B : LinearMap.BilinForm R L) (hB : LinearMap.BilinForm.lieInvariant L B) (x : L) : ↑((adjointSO B hB) x) = (LieAlgebra.ad R L) x

The polar-form specialization is again ad with its codomain restricted.

theorem TauCeti.LieAlgebra.adjointSO_apply {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (B : LinearMap.BilinForm R L) (hB : LinearMap.BilinForm.lieInvariant L B) (x y : L) : ↑((adjointSO B hB) x) y = ⁅x, y⁆

The polar-form specialization acts by the bracket. This is the equation the roadmap pins adjointSO by; it is not @[simp], since coe_adjointSO together with LieAlgebra.ad_apply already rewrites the left-hand side.

@[simp]

theorem TauCeti.LieAlgebra.ker_adjointSO {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (B : LinearMap.BilinForm R L) (hB : LinearMap.BilinForm.lieInvariant L B) : (adjointSO B hB).ker = LieAlgebra.center R L

The kernel of the adjoint homomorphism is the centre, since adjointSO is ad with its codomain restricted.

theorem TauCeti.LieAlgebra.adjointSO_injective_iff {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (B : LinearMap.BilinForm R L) (hB : LinearMap.BilinForm.lieInvariant L B) : Function.Injective ⇑(adjointSO B hB) ↔ LieAlgebra.center R L = ⊥

The adjoint homomorphism is injective exactly when the centre of L is trivial.

noncomputable def TauCeti.LieAlgebra.killingQuadraticForm (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : QuadraticForm R L

The Killing quadratic form x ↦ κ(x, x) of a Lie algebra. This is the form whose Clifford algebra carries Kostant's isotypic left-regular module; it is nondegenerate whenever L is Killing-semisimple and 2 is invertible in R (killingQuadraticForm_nondegenerate).

Equations

• TauCeti.LieAlgebra.killingQuadraticForm R L = LinearMap.BilinMap.toQuadraticMap (killingForm R L)

@[simp]

theorem TauCeti.LieAlgebra.killingQuadraticForm_apply (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) : (killingQuadraticForm R L) x = ((killingForm R L) x) x

The Killing quadratic form evaluates at x to κ(x, x). This is the equation the roadmap pins killingQuadraticForm by.

@[simp]

theorem TauCeti.LieAlgebra.polarBilin_killingQuadraticForm (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : QuadraticMap.polarBilin (killingQuadraticForm R L) = 2 • killingForm R L

The polar form of the Killing quadratic form is 2 • κ: here the symmetry of the Killing form does the work, collapsing κ + κ.flip.

theorem TauCeti.LieAlgebra.killingQuadraticForm_nondegenerate (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] [Invertible 2] [LieAlgebra.IsKilling R L] : QuadraticMap.Nondegenerate

The Killing quadratic form is nondegenerate for a Killing-semisimple Lie algebra over a ring in which 2 is invertible. Both hypotheses are needed: IsKilling is nondegeneracy of κ itself, and without an invertible 2 the polar form of a quadratic form is a weaker invariant than the form.

noncomputable def TauCeti.LieAlgebra.killingAdjointSO (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : L →ₗ⁅R⁆ ↥(skewAdjointLieSubalgebra (QuadraticMap.polarBilin (killingQuadraticForm R L)))

The adjoint homomorphism of a Lie algebra into the skew-adjoint endomorphisms of the polar form 2 • κ of its Killing quadratic form (polarBilin_killingQuadraticForm). This is the homomorphism whose composite with the quadratic realization inside Cliff(L, κ) is the adjoint quadratic lift of Kostant's theorem.

Equations

• TauCeti.LieAlgebra.killingAdjointSO R L = TauCeti.LieAlgebra.adjointSO (killingForm R L) ⋯

@[simp]

theorem TauCeti.LieAlgebra.coe_killingAdjointSO (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) : ↑((killingAdjointSO R L) x) = (LieAlgebra.ad R L) x

The Killing specialization is again ad with its codomain restricted.

@[simp]

theorem TauCeti.LieAlgebra.ker_killingAdjointSO (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : (killingAdjointSO R L).ker = LieAlgebra.center R L

The kernel of the Killing adjoint homomorphism is the centre.

theorem TauCeti.LieAlgebra.killingAdjointSO_injective_iff (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : Function.Injective ⇑(killingAdjointSO R L) ↔ LieAlgebra.center R L = ⊥

The Killing adjoint homomorphism is injective exactly when the centre of L is trivial.

@[simp]

theorem Module.Basis.dualBasis_polarBilin_killingQuadraticForm_apply {K : Type u} [Field K] [Invertible 2] {ι : Type w} [Fintype ι] [DecidableEq ι] {L : Type v} [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] (b : Basis ι K L) (i : ι) : ((2 • killingForm K L).dualBasis ⋯ b) i = 2⁻¹ • (TauCeti.killingDualBasis b) i

The basis dual to b for the polar form of the Killing quadratic form is half the Killing-dual basis. The factor records that this polar form is 2 • killingForm K L.