The dual of a finite-dimensional irreducible Lie module

The dual M* = Module.Dual R M of a Lie module carries the contragredient action ⁅x, f⁆ m = - f ⁅x, m⁆ (Mathlib's Module.Dual.instLieRingModule). This file records the two facts about it that a self-duality statement needs. Nothing here mentions weights, so both are stated for an arbitrary Lie algebra acting on an arbitrary module.

The first is that irreducibility passes to the dual in finite dimensions. If N ≤ M* is stable under the action then so is the set of vectors every functional in N kills, because ⁅x, f⁆ again lies in N. A nonzero N has a proper annihilator, hence a zero one, and in finite dimensions that forces N = ⊤.

The second is that an invariant bilinear form on M is the same datum as a morphism M → M*. That dictionary is already Mathlib's: a bilinear form on M is a linear map M → M*, both LinearMap.BilinForm and Module.Dual being abbreviations; LinearMap.BilinForm.lieInvariant_iff says that invariance is exactly membership of the maximal trivial submodule; and LieModule.maxTrivLinearMapEquivLieModuleHom is the R-linear equivalence between that submodule and the morphism space. Only the consequence for nonvanishing is recorded here. For an irreducible M Schur's lemma then upgrades a nonzero morphism to an equivalence, so carrying a nonzero invariant form and being self-dual are the same condition.

Main results

• LieSubmodule.dualCoannihilator: the Lie submodule of M annihilated by every functional in a Lie submodule of M*, refining Submodule.dualCoannihilator.
• LieModuleHom.lieInvariant_coe: a morphism M → M*, read as a bilinear form on M, is invariant.
• TauCeti.LieModule.exists_ne_zero_lieInvariant_iff_exists_ne_zero_lieModuleHom: a nonzero invariant bilinear form on M is a nonzero morphism M → M*, over any commutative ring.
• TauCeti.LieModule.isIrreducible_dual: the dual of a finite-dimensional irreducible Lie module is irreducible.
• TauCeti.LieModule.exists_ne_zero_lieInvariant_iff_nonempty_lieModuleEquiv_dual: a finite-dimensional irreducible Lie module carries a nonzero invariant bilinear form exactly when it is equivalent to its dual.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §6.1.
• N. Bourbaki, Groupes et algèbres de Lie, Chapitre I, §3.3.

Annihilators of Lie submodules of the dual

def LieSubmodule.dualCoannihilator {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L (Module.Dual R M)) : LieSubmodule R L M

The vectors of M annihilated by every functional in a Lie submodule N of the dual. It is a Lie submodule because N is: if f m = 0 for every f ∈ N, then f ⁅x, m⁆ = -⁅x, f⁆ m = 0, the functional ⁅x, f⁆ again lying in N.

Equations

• N.dualCoannihilator = { toSubmodule := (↑N).dualCoannihilator, lie_mem := ⋯ }

@[simp]

theorem LieSubmodule.mem_dualCoannihilator {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N : LieSubmodule R L (Module.Dual R M)} {m : M} : m ∈ N.dualCoannihilator ↔ ∀ f ∈ N, f m = 0

@[simp]

theorem LieSubmodule.dualCoannihilator_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L (Module.Dual R M)) : ↑N.dualCoannihilator = (↑N).dualCoannihilator

theorem LieSubmodule.eq_bot_of_dualCoannihilator_eq_top {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N : LieSubmodule R L (Module.Dual R M)} (h : N.dualCoannihilator = ⊤) : N = ⊥

Only the zero submodule of the dual annihilates all of M.

Invariant bilinear forms as morphisms to the dual

theorem LieModuleHom.lieInvariant_coe {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (f : M →ₗ⁅R,L⁆ Module.Dual R M) : LinearMap.BilinForm.lieInvariant L ↑f

A morphism M → M* is an invariant bilinear form. A morphism of Lie modules lies in the maximal trivial submodule of the space of linear maps (LieModule.maxTrivLinearMapEquivLieModuleHom), and for a linear map M → M*, that is a bilinear form on M, membership of the maximal trivial submodule is invariance (LinearMap.BilinForm.lieInvariant_iff).

theorem TauCeti.LieModule.exists_ne_zero_lieInvariant_iff_exists_ne_zero_lieModuleHom {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : (∃ (Φ : LinearMap.BilinForm R M), Φ ≠ 0 ∧ LinearMap.BilinForm.lieInvariant L Φ) ↔ ∃ (f : M →ₗ⁅R,L⁆ Module.Dual R M), f ≠ 0

A nonzero invariant bilinear form is a nonzero morphism to the dual. A bilinear form on M is a linear map M → M*, invariance of the form is membership of the maximal trivial submodule (LinearMap.BilinForm.lieInvariant_iff), and LieModule.maxTrivLinearMapEquivLieModuleHom is the linear equivalence of that submodule with the morphism space, so it matches the nonzero forms with the nonzero morphisms.

Irreducibility of the dual

theorem TauCeti.LieModule.isIrreducible_dual {K : Type u} {L : Type v} {M : Type w} [Field K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsIrreducible K L M] : LieModule.IsIrreducible K L (Module.Dual K M)

The dual of a finite-dimensional irreducible Lie module is irreducible. A nonzero Lie submodule N of M* does not annihilate all of M, so its annihilator is a proper Lie submodule of M and therefore zero; the dimension count for annihilators in a finite-dimensional space then makes N all of M*.

Self-duality

theorem TauCeti.LieModule.exists_ne_zero_lieInvariant_iff_nonempty_lieModuleEquiv_dual {K : Type u} {L : Type v} {M : Type w} [Field K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsIrreducible K L M] : (∃ (Φ : LinearMap.BilinForm K M), Φ ≠ 0 ∧ LinearMap.BilinForm.lieInvariant L Φ) ↔ Nonempty (M ≃ₗ⁅K,L⁆ Module.Dual K M)

A finite-dimensional irreducible Lie module carries a nonzero invariant bilinear form exactly when it is self-dual. The form is a morphism M → M*, and by Schur's lemma a nonzero morphism between the irreducible modules M and M* is an equivalence.