Lie representations induced from Clifford modules

A Lie homomorphism into the skew-adjoint endomorphisms of a nondegenerate quadratic module lifts through the quadratic realization in its Clifford algebra. Composing this lift with any Clifford action makes the target Clifford module a module for the original Lie algebra.

Main results

• CliffordAlgebra.quadraticLift: the quadratic realization of a skew-adjoint Lie action.
• CliffordAlgebra.quadraticLift_lie_ι: its defining action on Clifford generators.
• CliffordAlgebra.quadraticLift_injective_iff: the lift is injective exactly when the skew-adjoint action it lifts is.
• CliffordAlgebra.cliffordInducedRep: the induced Lie representation on a Clifford module.
• CliffordAlgebra.cliffordInducedRep_apply: its defining equation.
• CliffordAlgebra.cliffordDerivationRep: the induced representation on the Clifford algebra by inner derivations.
• CliffordAlgebra.cliffordDerivationRep_apply: its defining commutator equation.
• CliffordAlgebra.adjointCliffordHom: the quadratic lift of the adjoint representation for a Killing-semisimple Lie algebra.
• CliffordAlgebra.adjointCliffordHom_lie_ι: the lift acts on Clifford generators by the original adjoint action.
• CliffordAlgebra.adjointCliffordHom_injective: the lift is injective, since the adjoint action it encodes is faithful.

noncomputable def CliffordAlgebra.quadraticLift {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) {L : Type w} [LieRing L] [LieAlgebra K L] (θ : L →ₗ⁅K⁆ ↥(skewAdjointLieSubalgebra (QuadraticMap.polarBilin Q))) : L →ₗ⁅K⁆ CliffordAlgebra Q

Lift a skew-adjoint Lie action through the quadratic realization in the Clifford algebra.

Equations

• CliffordAlgebra.quadraticLift Q hQ θ = (CliffordAlgebra.quadraticLieSubalgebra Q).incl.comp ((CliffordAlgebra.soEquivQuadratic Q hQ).comp θ)

@[simp]

theorem CliffordAlgebra.quadraticLift_apply {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) {L : Type w} [LieRing L] [LieAlgebra K L] (θ : L →ₗ⁅K⁆ ↥(skewAdjointLieSubalgebra (QuadraticMap.polarBilin Q))) (x : L) : (quadraticLift Q hQ θ) x = ↑((soEquivQuadratic Q hQ) (θ x))

The quadratic lift is the quadratic realization of the supplied skew-adjoint action.

theorem CliffordAlgebra.quadraticLift_mem_quadraticLieSubalgebra {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) {L : Type w} [LieRing L] [LieAlgebra K L] (θ : L →ₗ⁅K⁆ ↥(skewAdjointLieSubalgebra (QuadraticMap.polarBilin Q))) (x : L) : (quadraticLift Q hQ θ) x ∈ quadraticLieSubalgebra Q

Values of the quadratic lift lie in the quadratic Lie subalgebra.

theorem CliffordAlgebra.quadraticLift_lie_ι {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) {L : Type w} [LieRing L] [LieAlgebra K L] (θ : L →ₗ⁅K⁆ ↥(skewAdjointLieSubalgebra (QuadraticMap.polarBilin Q))) (x : L) (v : V) : ⁅(quadraticLift Q hQ θ) x, (ι Q) v⁆ = (ι Q) (↑(θ x) v)

The quadratic lift acts on Clifford generators through the supplied skew-adjoint action.

theorem CliffordAlgebra.quadraticLift_injective_iff {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) {L : Type w} [LieRing L] [LieAlgebra K L] (θ : L →ₗ⁅K⁆ ↥(skewAdjointLieSubalgebra (QuadraticMap.polarBilin Q))) : Function.Injective ⇑(quadraticLift Q hQ θ) ↔ Function.Injective ⇑θ

The quadratic lift is injective exactly when the action it lifts is. The lift is the skew-adjoint action followed by the quadratic realization equivalence and the inclusion of the quadratic Lie subalgebra, both of which are injective.

noncomputable def CliffordAlgebra.cliffordInducedRep {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) {L : Type w} [LieRing L] [LieAlgebra K L] (θ : L →ₗ⁅K⁆ ↥(skewAdjointLieSubalgebra (QuadraticMap.polarBilin Q))) {S : Type x} [AddCommGroup S] [Module K S] (ρ : CliffordAlgebra Q →ₐ[K] Module.End K S) : L →ₗ⁅K⁆ Module.End K S

The Lie representation on a Clifford module induced through the quadratic realization.

Equations

• CliffordAlgebra.cliffordInducedRep Q hQ θ ρ = ρ.toLieHom.comp (CliffordAlgebra.quadraticLift Q hQ θ)

@[simp]

theorem CliffordAlgebra.cliffordInducedRep_apply {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) {L : Type w} [LieRing L] [LieAlgebra K L] (θ : L →ₗ⁅K⁆ ↥(skewAdjointLieSubalgebra (QuadraticMap.polarBilin Q))) {S : Type x} [AddCommGroup S] [Module K S] (ρ : CliffordAlgebra Q →ₐ[K] Module.End K S) (y : L) : (cliffordInducedRep Q hQ θ ρ) y = ρ ↑((soEquivQuadratic Q hQ) (θ y))

The induced representation acts through the quadratic realization and the Clifford action.

noncomputable def CliffordAlgebra.cliffordDerivationRep {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) {L : Type w} [LieRing L] [LieAlgebra K L] (θ : L →ₗ⁅K⁆ ↥(skewAdjointLieSubalgebra (QuadraticMap.polarBilin Q))) : L →ₗ⁅K⁆ Module.End K (CliffordAlgebra Q)

The representation on the Clifford algebra induced by the inner derivations of the quadratic realization.

Equations

• CliffordAlgebra.cliffordDerivationRep Q hQ θ = (LieAlgebra.ad K (CliffordAlgebra Q)).comp (CliffordAlgebra.quadraticLift Q hQ θ)

@[simp]

theorem CliffordAlgebra.cliffordDerivationRep_apply {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) {L : Type w} [LieRing L] [LieAlgebra K L] (θ : L →ₗ⁅K⁆ ↥(skewAdjointLieSubalgebra (QuadraticMap.polarBilin Q))) (y : L) (c : CliffordAlgebra Q) : ((cliffordDerivationRep Q hQ θ) y) c = ⁅↑((soEquivQuadratic Q hQ) (θ y)), c⁆

The induced derivation representation acts by commutator with the quadratic realization.

noncomputable def CliffordAlgebra.adjointCliffordHom (K : Type u) (L : Type v) [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [Invertible 2] [LieAlgebra.IsKilling K L] : L →ₗ⁅K⁆ CliffordAlgebra (TauCeti.LieAlgebra.killingQuadraticForm K L)

The quadratic lift of the adjoint representation of a Killing-semisimple Lie algebra into the Clifford algebra of its Killing quadratic form.

Equations

• CliffordAlgebra.adjointCliffordHom K L = CliffordAlgebra.quadraticLift (TauCeti.LieAlgebra.killingQuadraticForm K L) ⋯ (TauCeti.LieAlgebra.killingAdjointSO K L)

@[simp]

theorem CliffordAlgebra.adjointCliffordHom_apply (K : Type u) (L : Type v) [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [Invertible 2] [LieAlgebra.IsKilling K L] (x : L) : (adjointCliffordHom K L) x = ↑((soEquivQuadratic (TauCeti.LieAlgebra.killingQuadraticForm K L) ⋯) ((TauCeti.LieAlgebra.killingAdjointSO K L) x))

The adjoint Clifford homomorphism is the quadratic realization of the Killing adjoint action.

theorem CliffordAlgebra.adjointCliffordHom_lie_ι (K : Type u) (L : Type v) [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [Invertible 2] [LieAlgebra.IsKilling K L] (x y : L) : ⁅(adjointCliffordHom K L) x, (ι (TauCeti.LieAlgebra.killingQuadraticForm K L)) y⁆ = (ι (TauCeti.LieAlgebra.killingQuadraticForm K L)) ⁅x, y⁆

The adjoint quadratic lift acts on Clifford generators by the original adjoint action.

theorem CliffordAlgebra.adjointCliffordHom_injective (K : Type u) (L : Type v) [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [Invertible 2] [LieAlgebra.IsKilling K L] : Function.Injective ⇑(adjointCliffordHom K L)

The adjoint quadratic lift of a Killing-semisimple Lie algebra is injective. The lift is injective exactly when the adjoint action it lifts is (CliffordAlgebra.quadraticLift_injective_iff), and that action is faithful because the centre of a Killing-semisimple Lie algebra vanishes.