Endomorphisms acting on alternating maps as derivations

An endomorphism f of M acts on alternating maps ω : M [⋀^ι]→ₗ[R] N by applying f to one argument at a time and summing, f.alternatingDerivation ω v = ∑ i, ω (update v i (f (v i))). This is the infinitesimal form of the action ω ↦ ω ∘ g of automorphisms g of M. The commutator of two such derivations is the derivation of the commutator of the endomorphisms, taken in the opposite order (LinearMap.alternatingDerivation_alternatingDerivation_sub), they commute with linear maps of coefficients, and inserting a first argument x splits off the term in which f hits x (LinearMap.curryLeft_alternatingDerivation).

For a Lie algebra acting on M and on N, these derivations supply the contribution of the arguments to the action of the Lie algebra on alternating maps from M to N: the action of x is the action on values minus alternatingDerivation of the action of x on M. For M = L with the adjoint action this is the Lie derivative of Chevalley–Eilenberg cochains.

Implementation notes

The definition and the proofs of alternation and of the commutator formula were adapted from the continuous real version ContinuousLinearMap.alternatingDerivation in TauCeti.Topology.Algebra.Module.Alternating.AlmostComplexType, which is now built on this file.

def LinearMap.alternatingDerivation {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Fintype ι] [DecidableEq ι] (f : M →ₗ[R] M) : M [⋀^ι]→ₗ[R] N →ₗ[R] M [⋀^ι]→ₗ[R] N

An endomorphism f of M acts on alternating maps on M as a derivation: the result is the sum, over all arguments, of the alternating map with f applied to that argument.

@[simp]

theorem LinearMap.alternatingDerivation_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Fintype ι] [DecidableEq ι] (f : M →ₗ[R] M) (ω : M [⋀^ι]→ₗ[R] N) (v : ι → M) : (f.alternatingDerivation ω) v = ∑ i : ι, ω (Function.update v i (f (v i)))

The value of the derivation: the sum of the values with f applied to one argument.

@[simp]

theorem LinearMap.alternatingDerivation_add {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Fintype ι] [DecidableEq ι] (f g : M →ₗ[R] M) : (f + g).alternatingDerivation = f.alternatingDerivation + g.alternatingDerivation

The derivation is additive in the endomorphism.

@[simp]

theorem LinearMap.alternatingDerivation_sub {R : Type u_1} {ι : Type u_5} [CommSemiring R] [Fintype ι] [DecidableEq ι] {M : Type u_6} {N : Type u_7} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f g : M →ₗ[R] M) : (f - g).alternatingDerivation = f.alternatingDerivation - g.alternatingDerivation

The derivation is compatible with subtraction of endomorphisms.

theorem LinearMap.alternatingDerivation_compAlternatingMap {R : Type u_1} {M : Type u_2} {N : Type u_3} {N₂ : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid N₂] [Module R N₂] [Fintype ι] [DecidableEq ι] (f : M →ₗ[R] M) (g : N →ₗ[R] N₂) (ω : M [⋀^ι]→ₗ[R] N) : f.alternatingDerivation (g.compAlternatingMap ω) = g.compAlternatingMap (f.alternatingDerivation ω)

The derivation commutes with linear maps of coefficients.

theorem LinearMap.alternatingDerivation_alternatingDerivation_sub {R : Type u_1} {M : Type u_2} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] {N : Type u_6} [AddCommGroup N] [Module R N] (f g : M →ₗ[R] M) (ω : M [⋀^ι]→ₗ[R] N) : f.alternatingDerivation (g.alternatingDerivation ω) - g.alternatingDerivation (f.alternatingDerivation ω) = (g ∘ₗ f).alternatingDerivation ω - (f ∘ₗ g).alternatingDerivation ω

The commutator of the derivations induced by two endomorphisms is induced by their commutator, taken in the opposite order since the endomorphisms act on the arguments.

theorem LinearMap.curryLeft_alternatingDerivation {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {n : ℕ} (f : M →ₗ[R] M) (ω : M [⋀^Fin (n + 1)]→ₗ[R] N) (x : M) : (f.alternatingDerivation ω).curryLeft x = f.alternatingDerivation (ω.curryLeft x) + ω.curryLeft (f x)

Inserting x as the first argument of f.alternatingDerivation ω splits off the term in which f is applied to x.