The Lie module of alternating maps

Let M and N be modules over a Lie algebra L. Then L acts on the alternating maps ω : M [⋀^ι]→ₗ[R] N by ⁅x, ω⁆ v = ⁅x, ω v⁆ - ∑ i, ω (update v i ⁅x, v i⁆), extending Mathlib's action LinearMap.instLieRingModule on linear maps. The first term is the action on the values and the second is the derivation induced by the action on the arguments (LinearMap.alternatingDerivation). For M = L acting on itself by the adjoint action, these are the cochains of the Chevalley–Eilenberg complex of L with coefficients in N, and ⁅x, ω⁆ is the Lie derivative of ω along x.

Inserting a first argument intertwines the action up to the action on that argument (AlternatingMap.curryLeft_lie); this is the identity [L_x, ι_y] = ι_{[x, y]} between Lie derivatives and interior products.

References

• C. Chevalley and S. Eilenberg, Cohomology theory of Lie groups and Lie algebras, Trans. Amer. Math. Soc. 63 (1948), 85–124.

@[instance_reducible]

instance AlternatingMap.instBracket {R : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] [Fintype ι] [DecidableEq ι] : Bracket L (M [⋀^ι]→ₗ[R] N)

A Lie algebra acting on M and N acts on alternating maps from M to N, on the values and, as a derivation, on the arguments.

theorem AlternatingMap.lie_def {R : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] [Fintype ι] [DecidableEq ι] (x : L) (ω : M [⋀^ι]→ₗ[R] N) : ⁅x, ω⁆ = (LinearMap.compAlternatingMapₗ R ((LieModule.toEnd R L N) x)) ω - (LinearMap.alternatingDerivation ((LieModule.toEnd R L M) x)) ω

The action splits into the action on values and the derivation on arguments.

@[simp]

theorem AlternatingMap.lie_apply {R : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] [Fintype ι] [DecidableEq ι] (x : L) (ω : M [⋀^ι]→ₗ[R] N) (v : ι → M) : ⁅x, ω⁆ v = ⁅x, ω v⁆ - ∑ i : ι, ω (Function.update v i ⁅x, v i⁆)

The value of ⁅x, ω⁆: the action on the value of ω, minus the values of ω with x acting on one argument at a time.

@[instance_reducible]

instance AlternatingMap.instLieRingModule {R : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] [Fintype ι] [DecidableEq ι] : LieRingModule L (M [⋀^ι]→ₗ[R] N)

The action on alternating maps is a Lie ring module: the actions on values commute with the derivations, and both are representations.

instance AlternatingMap.instLieModule {R : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] [Fintype ι] [DecidableEq ι] : LieModule R L (M [⋀^ι]→ₗ[R] N)

The action on alternating maps is R-bilinear.

theorem AlternatingMap.curryLeft_lie {R : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] {n : ℕ} (x : L) (ω : M [⋀^Fin (n + 1)]→ₗ[R] N) (y : M) : ⁅x, ω⁆.curryLeft y = ⁅x, ω.curryLeft y⁆ - ω.curryLeft ⁅x, y⁆

Inserting y as the first argument of ⁅x, ω⁆ is the action of x on ω.curryLeft y, corrected by inserting ⁅x, y⁆ instead.