Basic infrastructure for Lie modules

This file supplies general constructions for Lie modules that are missing from Mathlib.

Main definitions

• Ado.LieModuleEquiv.ofBijective: a bijective morphism of Lie modules is an equivalence.
• Ado.LieModuleEquiv.restrictLie: an equivalence of Lie modules over a Lie algebra, read as one over a Lie subalgebra.
• Ado.LieModuleEquiv.congrRight and Ado.LieModuleEquiv.congrLeft: postcomposition and precomposition with an equivalence of Lie modules, as linear equivalences of morphism spaces.
• Ado.lieAnnihilator: the Lie subalgebra of elements annihilating a vector in a Lie module.
• LieHom.lieIdealComap: a Lie homomorphism restricted to the preimage of a Lie ideal, as a Lie homomorphism into that ideal.

Main results

• Module.Basis.repr_lie_eq_sum: a Lie bracket coordinate is a weighted sum of bracket columns.

• Ado.LieModuleHom.instFiniteDimensional: the morphism space of two finite-dimensional Lie modules is finite-dimensional.

• Ado.lieSpan_le_lieAnnihilator: a vector annihilated by a generating set is annihilated by the Lie subalgebra it generates.

• Ado.mem_lieAnnihilator: membership in lieAnnihilator R L v is equivalent to vanishing of the Lie action on v.

• LieHom.map_ad_pow: a Lie homomorphism carries (ad x) ^ n y to (ad (f x)) ^ n (f y).

• LieHom.isNilpotent_ad_of_surjective: adjoint nilpotence descends along a surjective Lie homomorphism.

• LieHom.lieIdealComap_injective: the restriction of an injective Lie homomorphism to the preimage of a Lie ideal is injective.

• LieSubmodule.lie_iSup: bracketing with a Lie ideal distributes over suprema of Lie submodules.

• Ado.ad_pow_apply_eq_ad_pow_apply: iterating the adjoint action gives the same element whichever base ring the Lie algebra is read over.

• Ado.isTrivial_of_forall_lie_eq_zero_of_lieSpan_eq_top: a Lie module generated by a vector annihilated by the Lie algebra is trivial.

noncomputable def Ado.LieModuleEquiv.ofBijective {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (hf : Function.Bijective ⇑f) : M ≃ₗ⁅R,L⁆ N

A bijective morphism of Lie modules is an equivalence of Lie modules. This is the Lie module analogue of LieEquiv.ofBijective.

Equations

• Ado.LieModuleEquiv.ofBijective f hf = { toFun := ⇑f, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯, invFun := (LinearEquiv.ofBijective (↑f) hf).invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Ado.LieModuleEquiv.ofBijective_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (hf : Function.Bijective ⇑f) (m : M) : (ofBijective f hf) m = f m

noncomputable def Ado.LieModuleEquiv.restrictLie {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieAlgebra R L] (e : M ≃ₗ⁅R,L⁆ N) (L' : LieSubalgebra R L) : M ≃ₗ⁅R,↥L'⁆ N

An equivalence of L-modules is an equivalence of L'-modules for a Lie subalgebra L' ≤ L, with the same underlying map. This is Mathlib's LieModuleHom.restrictLie for equivalences.

Equations

• Ado.LieModuleEquiv.restrictLie e L' = Ado.LieModuleEquiv.ofBijective (e.restrictLie L') ⋯

@[simp]

theorem Ado.LieModuleEquiv.coe_restrictLie {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieAlgebra R L] (e : M ≃ₗ⁅R,L⁆ N) (L' : LieSubalgebra R L) : ⇑(restrictLie e L') = ⇑e

def Ado.LieModuleEquiv.congrRight {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] {P : Type w₂} [AddCommGroup P] [Module R P] [LieRingModule L P] [LieAlgebra R L] [LieModule R L N] [LieModule R L P] (e : N ≃ₗ⁅R,L⁆ P) : (M →ₗ⁅R,L⁆ N) ≃ₗ[R] M →ₗ⁅R,L⁆ P

Postcomposition with an equivalence of Lie modules, as an R-linear equivalence (M →ₗ⁅R,L⁆ N) ≃ₗ[R] (M →ₗ⁅R,L⁆ P) of morphism spaces. This is the Lie-module analogue of LinearEquiv.congrRight, which is unavailable here because a LieModuleHom is not a LinearMap.

Equations

• Ado.LieModuleEquiv.congrRight e = { toFun := fun (f : M →ₗ⁅R,L⁆ N) => e.comp f, map_add' := ⋯, map_smul' := ⋯, invFun := fun (g : M →ₗ⁅R,L⁆ P) => e.symm.comp g, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Ado.LieModuleEquiv.congrRight_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] {P : Type w₂} [AddCommGroup P] [Module R P] [LieRingModule L P] [LieAlgebra R L] [LieModule R L N] [LieModule R L P] (e : N ≃ₗ⁅R,L⁆ P) (f : M →ₗ⁅R,L⁆ N) (m : M) : ((congrRight e) f) m = e (f m)

@[simp]

theorem Ado.LieModuleEquiv.congrRight_symm_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] {P : Type w₂} [AddCommGroup P] [Module R P] [LieRingModule L P] [LieAlgebra R L] [LieModule R L N] [LieModule R L P] (e : N ≃ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ P) (m : M) : ((congrRight e).symm g) m = e.symm (g m)

def Ado.LieModuleEquiv.congrLeft {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] {P : Type w₂} [AddCommGroup P] [Module R P] [LieRingModule L P] [LieAlgebra R L] [LieModule R L P] (e : M ≃ₗ⁅R,L⁆ N) : (M →ₗ⁅R,L⁆ P) ≃ₗ[R] N →ₗ⁅R,L⁆ P

Precomposition with an equivalence of Lie modules, as an R-linear equivalence (M →ₗ⁅R,L⁆ P) ≃ₗ[R] (N →ₗ⁅R,L⁆ P) of morphism spaces. This is the source-variable companion of Ado.LieModuleEquiv.congrRight.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Ado.LieModuleEquiv.congrLeft_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] {P : Type w₂} [AddCommGroup P] [Module R P] [LieRingModule L P] [LieAlgebra R L] [LieModule R L P] (e : M ≃ₗ⁅R,L⁆ N) (f : M →ₗ⁅R,L⁆ P) (n : N) : ((congrLeft e) f) n = f (e.symm n)

@[simp]

theorem Ado.LieModuleEquiv.congrLeft_symm_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] {P : Type w₂} [AddCommGroup P] [Module R P] [LieRingModule L P] [LieAlgebra R L] [LieModule R L P] (e : M ≃ₗ⁅R,L⁆ N) (g : N →ₗ⁅R,L⁆ P) (m : M) : ((congrLeft e).symm g) m = g (e m)

Morphism spaces of Lie modules

instance Ado.LieModuleHom.instFiniteDimensional {K : Type u} {L : Type v} {M : Type w} {N : Type w₁} [Field K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [AddCommGroup N] [Module K N] [LieRingModule L N] [LieModule K L N] [FiniteDimensional K N] : FiniteDimensional K (M →ₗ⁅K,L⁆ N)

The morphism space of two finite-dimensional Lie modules is finite-dimensional: by LieModule.maxTrivLinearMapEquivLieModuleHom it is the maximal trivial submodule of the finite-dimensional space of all linear maps between them.

theorem LieSubmodule.lie_iSup {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieAlgebra R L] {ι : Type u_1} (I : LieIdeal R L) (N : ι → LieSubmodule R L M) : ⁅I, ⨆ (i : ι), N i⁆ = ⨆ (i : ι), ⁅I, N i⁆

Bracketing with a Lie ideal distributes over suprema of Lie submodules.

def Ado.lieAnnihilator (R : Type u) (L : Type v) {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieAlgebra R L] [LieModule R L M] (v : M) : LieSubalgebra R L

The elements of L annihilating a fixed vector v form a Lie subalgebra: the bracket is linear in its left argument, and the Leibniz rule lie_lie closes the set under brackets.

Equations

• Ado.lieAnnihilator R L v = { carrier := {x : L | ⁅x, v⁆ = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯, lie_mem' := ⋯ }

@[simp]

theorem Ado.mem_lieAnnihilator (R : Type u) (L : Type v) {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieAlgebra R L] [LieModule R L M] {v : M} {x : L} : x ∈ lieAnnihilator R L v ↔ ⁅x, v⁆ = 0

Membership in the annihilator of a vector is exactly vanishing of the Lie action.

theorem Ado.lieSpan_le_lieAnnihilator (R : Type u) (L : Type v) {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieAlgebra R L] [LieModule R L M] {s : Set L} {v : M} (hs : ∀ x ∈ s, ⁅x, v⁆ = 0) : LieSubalgebra.lieSpan R L s ≤ lieAnnihilator R L v

A vector annihilated by a set of Lie elements is annihilated by the Lie subalgebra that set generates. The annihilator is a Lie subalgebra, so the universal property of lieSpan promotes vanishing on a generating set to vanishing on the whole span.

theorem Ado.isTrivial_of_forall_lie_eq_zero_of_lieSpan_eq_top {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieAlgebra R L] [LieModule R L M] {v : M} (h : ∀ (x : L), ⁅x, v⁆ = 0) (hgen : LieSubmodule.lieSpan R L {v} = ⊤) : LieModule.IsTrivial L M

A Lie module generated by a vector annihilated by every element of the Lie algebra is trivial.

theorem Ado.ad_pow_apply_eq_ad_pow_apply {L : Type u_1} [LieRing L] (R : Type u_2) (S : Type u_3) [CommRing R] [CommRing S] [LieAlgebra R L] [LieAlgebra S L] (x y : L) (k : ℕ) : ((LieAlgebra.ad R L) x ^ k) y = ((LieAlgebra.ad S L) x ^ k) y

The adjoint action does not depend on the base ring. A Lie algebra over two commutative rings has one bracket, so iterating ad over either ring gives the same element. This reads a higher Serre relation proved over ℤ as the relation asked of a Lie algebra over ℚ.

@[simp]

theorem LieHom.map_ad_pow {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (x : L) (n : ℕ) (y : L) : f (((LieAlgebra.ad R L) x ^ n) y) = ((LieAlgebra.ad R L') (f x) ^ n) (f y)

A Lie homomorphism carries the iterated adjoint action. f ((ad x) ^ n y) is (ad (f x)) ^ n (f y); relations of the form (ad x) ^ n y = 0, such as Serre's, are transported along a homomorphism by this.

theorem LieHom.isNilpotent_ad_of_surjective {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (hf : Function.Surjective ⇑f) {x : L} (hx : IsNilpotent ((LieAlgebra.ad R L) x)) : IsNilpotent ((LieAlgebra.ad R L') (f x))

Adjoint nilpotence descends along a surjective Lie homomorphism. In particular it descends to a quotient by any Lie ideal, without a finiteness or characteristic hypothesis.

def LieHom.lieIdealComap {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (I : LieIdeal R L') : ↥(LieIdeal.comap f I) →ₗ⁅R⁆ ↥I

The restriction of a Lie homomorphism f to the preimage of a Lie ideal I, as a Lie homomorphism into I. This is the Lie analogue of LinearMap.submoduleComap.

Equations

• f.lieIdealComap I = { toFun := fun (x : ↥(LieIdeal.comap f I)) => ⟨f ↑x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

@[simp]

theorem LieHom.coe_lieIdealComap_apply {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (I : LieIdeal R L') (x : ↥(LieIdeal.comap f I)) : ↑((f.lieIdealComap I) x) = f ↑x

theorem LieHom.lieIdealComap_injective {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (I : LieIdeal R L') (hf : Function.Injective ⇑f) : Function.Injective ⇑(f.lieIdealComap I)

The restriction of an injective Lie homomorphism to the preimage of a Lie ideal is injective.

theorem Module.Basis.repr_lie_eq_sum {R : Type u_1} {L : Type u_2} {ι : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [Fintype ι] (b : Basis ι R L) (X Y : L) (k : ι) : (b.repr ⁅X, Y⁆) k = ∑ i : ι, (b.repr X) i * (b.repr ⁅b i, Y⁆) k

A bracket coordinate is the sum of the bracket columns weighted by the first argument's basis coordinates.