Basic infrastructure for Lie modules

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

Main definitions

• TauCeti.LieModuleEquiv.ofBijective: a bijective morphism of Lie modules is an equivalence.
• TauCeti.LieModuleEquiv.restrictLie: an equivalence of Lie modules over a Lie algebra, read as one over a Lie subalgebra.
• TauCeti.LieModuleEquiv.congrRight and TauCeti.LieModuleEquiv.congrLeft: postcomposition and precomposition with an equivalence of Lie modules, as linear equivalences of morphism spaces.
• TauCeti.lieAnnihilator: the Lie subalgebra of elements annihilating a vector in a Lie module.

Main results

• TauCeti.LieModuleHom.sum_apply: a finite sum of morphisms of Lie modules is evaluated summandwise.
• TauCeti.LieModuleHom.instFiniteDimensional: the morphism space of two finite-dimensional Lie modules is finite-dimensional.
• TauCeti.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).
• TauCeti.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 TauCeti.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

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

@[simp]

theorem TauCeti.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 TauCeti.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

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

@[simp]

theorem TauCeti.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 TauCeti.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

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

@[simp]

theorem TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.LieModuleEquiv.congrRight.

Equations

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

@[simp]

theorem TauCeti.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 TauCeti.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

@[simp]

theorem TauCeti.LieModuleHom.sum_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] {ι : Type w₂} {s : Finset ι} (F : ι → M →ₗ⁅R,L⁆ N) (m : M) : (∑ i ∈ s, F i) m = ∑ i ∈ s, (F i) m

A finite sum of morphisms of Lie modules is evaluated summandwise.

instance TauCeti.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.

def TauCeti.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

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

@[simp]

theorem TauCeti.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 TauCeti.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.

@[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.