Documentation

Mathlib.Algebra.Lie.TraceForm

The trace and Killing forms of a Lie algebra. #

Let L be a Lie algebra with coefficients in a commutative ring R. Suppose M is a finite, free R-module and we have a representation φ : L → End M. This data induces a natural bilinear form B on L, called the trace form associated to M; it is defined as B(x, y) = Tr (φ x) (φ y).

In the special case that M is L itself and φ is the adjoint representation, the trace form is known as the Killing form.

We define the trace / Killing form in this file and prove some basic properties.

Main definitions #

noncomputable def LieModule.traceForm (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :

A finite, free representation of a Lie algebra L induces a bilinear form on L called the trace Form. See also killingForm.

Equations
Instances For
    theorem LieModule.traceForm_apply_apply (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (y : L) :
    ((LieModule.traceForm R L M) x) y = (LinearMap.trace R M) ((LieModule.toEnd R L M) x ∘ₗ (LieModule.toEnd R L M) y)
    theorem LieModule.traceForm_comm (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (y : L) :
    ((LieModule.traceForm R L M) x) y = ((LieModule.traceForm R L M) y) x
    theorem LieModule.traceForm_isSymm (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
    @[simp]
    theorem LieModule.traceForm_flip (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
    theorem LieModule.traceForm_apply_lie_apply (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (y : L) (z : L) :

    The trace form of a Lie module is compatible with the action of the Lie algebra.

    See also LieModule.traceForm_apply_lie_apply'.

    theorem LieModule.traceForm_apply_lie_apply' (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (y : L) (z : L) :

    Given a representation M of a Lie algebra L, the action of any x : L is skew-adjoint wrt the trace form.

    @[simp]
    theorem LieModule.lie_traceForm_eq_zero (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) :

    This lemma justifies the terminology "invariant" for trace forms.

    @[simp]
    @[simp]
    theorem LieModule.traceForm_genWeightSpace_eq (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Free R M] [IsDomain R] [IsPrincipalIdealRing R] [LieAlgebra.IsNilpotent R L] [IsNoetherian R M] [LieModule.LinearWeights R L M] (χ : LR) (x : L) (y : L) :
    theorem LieModule.traceForm_eq_zero_if_mem_lcs_of_mem_ucs (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {x : L} {y : L} (k : ) (hx : x .lcs L k) (hy : y LieSubmodule.ucs k ) :
    ((LieModule.traceForm R L M) x) y = 0

    The upper and lower central series of L are orthogonal wrt the trace form of any Lie module M.

    theorem LieModule.traceForm_apply_eq_zero_of_mem_lcs_of_mem_center (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {x : L} {y : L} (hx : x LieModule.lowerCentralSeries R L L 1) (hy : y LieAlgebra.center R L) :
    ((LieModule.traceForm R L M) x) y = 0
    @[simp]
    theorem LieModule.traceForm_eq_zero_of_isTrivial (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieModule.IsTrivial L M] :
    theorem LieModule.eq_zero_of_mem_genWeightSpace_mem_posFitting (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] {B : LinearMap.BilinForm R M} (hB : ∀ (x : L) (m n : M), (B x, m) n = -(B m) x, n) {m₀ : M} {m₁ : M} (hm₀ : m₀ LieModule.genWeightSpace M 0) (hm₁ : m₁ LieModule.posFittingComp R L M) :
    (B m₀) m₁ = 0

    Given a bilinear form B on a representation M of a nilpotent Lie algebra L, if B is invariant (in the sense that the action of L is skew-adjoint wrt B) then components of the Fitting decomposition of M are orthogonal wrt B.

    theorem LieModule.trace_toEnd_eq_zero_of_mem_lcs (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {k : } {x : L} (hk : 1 k) (hx : x LieModule.lowerCentralSeries R L L k) :
    (LinearMap.trace R M) ((LieModule.toEnd R L M) x) = 0
    @[simp]
    theorem LieModule.traceForm_lieSubalgebra_mk_left (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (L' : LieSubalgebra R L) {x : L} (hx : x L') (y : L') :
    ((LieModule.traceForm R (↥L') M) x, hx) y = ((LieModule.traceForm R L M) x) y
    @[simp]
    theorem LieModule.traceForm_lieSubalgebra_mk_right (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (L' : LieSubalgebra R L) {x : L'} {y : L} (hy : y L') :
    ((LieModule.traceForm R (↥L') M) x) y, hy = ((LieModule.traceForm R L M) x) y

    A nilpotent Lie algebra with a representation whose trace form is non-singular is Abelian.

    theorem LieSubmodule.trace_eq_trace_restrict_of_le_idealizer {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Free R M] [Module.Finite R M] [IsDomain R] [IsPrincipalIdealRing R] (N : LieSubmodule R L M) (I : LieIdeal R L) (h : I N.idealizer) (x : L) {y : L} (hy : y I) (hy' : optParam (∀ mN, ((LieModule.toEnd R L M) x ∘ₗ (LieModule.toEnd R L M) y) m N) ) :
    (LinearMap.trace R M) ((LieModule.toEnd R L M) x ∘ₗ (LieModule.toEnd R L M) y) = (LinearMap.trace R N) (((LieModule.toEnd R L M) x ∘ₗ (LieModule.toEnd R L M) y).restrict hy')
    theorem LieSubmodule.traceForm_eq_of_le_idealizer {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Free R M] [Module.Finite R M] [IsDomain R] [IsPrincipalIdealRing R] (N : LieSubmodule R L M) (I : LieIdeal R L) (h : I N.idealizer) :
    LieModule.traceForm R I N = (LieModule.traceForm R L M).restrict (lieIdealSubalgebra R L I).toSubmodule
    theorem LieSubmodule.traceForm_eq_zero_of_isTrivial {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Free R M] [Module.Finite R M] [IsDomain R] [IsPrincipalIdealRing R] (N : LieSubmodule R L M) (I : LieIdeal R L) (h : I N.idealizer) (x : L) {y : L} (hy : y I) [LieModule.IsTrivial I N] :
    (LinearMap.trace R M) ((LieModule.toEnd R L M) x ∘ₗ (LieModule.toEnd R L M) y) = 0

    Note that this result is slightly stronger than it might look at first glance: we only assume that N is trivial over I rather than all of L. This means that it applies in the important case of an Abelian ideal (which has M = L and N = I).

    @[reducible, inline]
    noncomputable abbrev killingForm (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] :

    A finite, free (as an R-module) Lie algebra L carries a bilinear form on L.

    This is a specialisation of LieModule.traceForm to the adjoint representation of L.

    Equations
    Instances For
      theorem killingForm_apply_apply (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) (y : L) :
      ((killingForm R L) x) y = (LinearMap.trace R L) ((LieAlgebra.ad R L) x ∘ₗ (LieAlgebra.ad R L) y)
      theorem killingForm_eq_zero_of_mem_zeroRoot_mem_posFitting (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R H] {x₀ : L} {x₁ : L} (hx₀ : x₀ LieAlgebra.zeroRootSubalgebra R L H) (hx₁ : x₁ LieModule.posFittingComp R (↥H) L) :
      ((killingForm R L) x₀) x₁ = 0
      noncomputable def LieIdeal.killingCompl (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) :

      The orthogonal complement of an ideal with respect to the killing form is an ideal.

      Equations
      Instances For
        @[simp]
        theorem LieIdeal.toSubmodule_killingCompl (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) :
        (LieIdeal.killingCompl R L I) = (killingForm R L).orthogonal I
        @[simp]
        theorem LieIdeal.mem_killingCompl (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) {x : L} :
        x LieIdeal.killingCompl R L I yI, ((killingForm R L) y) x = 0
        theorem LieIdeal.restrict_killingForm (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) :
        (killingForm R L).restrict (lieIdealSubalgebra R L I).toSubmodule = LieModule.traceForm R (↥I) L
        theorem LieIdeal.killingForm_eq (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [Module.Free R L] [Module.Finite R L] [IsDomain R] [IsPrincipalIdealRing R] :
        killingForm R I = (killingForm R L).restrict (lieIdealSubalgebra R L I).toSubmodule
        theorem LieModule.traceForm_eq_sum_finrank_nsmul_mul (K : Type u_2) (L : Type u_3) (M : Type u_4) [LieRing L] [AddCommGroup M] [LieRingModule L M] [Field K] [LieAlgebra K L] [Module K M] [LieModule K L M] [FiniteDimensional K M] [LieAlgebra.IsNilpotent K L] [LieModule.LinearWeights K L M] [LieModule.IsTriangularizable K L M] (x : L) (y : L) :
        ((LieModule.traceForm K L M) x) y = χ : LieModule.Weight K L M, Module.finrank K (LieModule.genWeightSpace M χ) (χ x * χ y)