The space of morphisms between irreducible Lie modules

Let M and N be irreducible Lie modules over a Lie algebra L. A nonzero morphism M → N has kernel and range that are Lie submodules, so both are trivial or everything; being nonzero forces the kernel to be ⊥ and the range to be ⊤, and the morphism is an equivalence (TauCeti.LieModule.bijective_of_ne_zero). So the morphism space is zero unless M and N are equivalent.

Over an algebraically closed field the other case is just as rigid. Schur's lemma (TauCeti.exists_forall_apply_eq_smul) makes every self-morphism of a finite-dimensional irreducible module a scalar, so the endomorphism space is the line spanned by the identity, and transporting along an equivalence gives the same for M → N. Together:

dim_K (M →ₗ⁅K,L⁆ N) = 1 if M ≃ₗ⁅K,L⁆ N, and 0 otherwise.

That dichotomy is the input a multiplicity count needs: in a decomposition of M into irreducibles, each summand contributes 1 to dim_K (S →ₗ⁅K,L⁆ M) when it is equivalent to S and 0 when it is not. Reading the multiplicity off dim_K (S →ₗ⁅K,L⁆ M) needs one further ingredient, additivity of the morphism space over a direct sum; that is TauCeti.LieModule.lieModuleHomDirectSumEquiv of TauCeti/Algebra/Lie/DirectSum.lean, and this file goes no further than the two-irreducible dimension count.

Main results

• TauCeti.LieModule.bijective_of_ne_zero: a nonzero morphism between irreducible Lie modules is bijective, over an arbitrary commutative ring.
• TauCeti.LieModule.eq_zero_of_isEmpty_lieModuleEquiv and TauCeti.LieModule.subsingleton_lieModuleHom_of_isEmpty_lieModuleEquiv: inequivalent irreducible Lie modules admit only the zero morphism.
• TauCeti.LieModule.nonempty_lieModuleEquiv_iff_exists_ne_zero: two irreducible Lie modules are equivalent exactly when some morphism between them is nonzero.
• TauCeti.LieModule.finrank_lieModuleHom_self: the endomorphisms of a finite-dimensional irreducible Lie module over an algebraically closed field are the scalars, so the endomorphism space is a line.
• TauCeti.LieModule.finiteDimensional_lieModuleHom_of_isIrreducible: the morphism space from a finite-dimensional irreducible to any irreducible is finite-dimensional.
• TauCeti.LieModule.finrank_lieModuleHom_eq_one_iff, TauCeti.LieModule.finrank_lieModuleHom_eq_zero_iff and TauCeti.LieModule.finrank_lieModuleHom_le_one: the dimension of the morphism space is 1 when the two irreducible modules are equivalent and 0 when they are not, packaged as TauCeti.LieModule.finrank_lieModuleHom.

Implementation notes

Schur's lemma itself, TauCeti.exists_forall_apply_eq_smul, stays in TauCeti/Algebra/Lie/Weights/Central.lean, where it is proved and where the central weight of an irreducible module consumes it. This file is its consequence for whole morphism spaces, which needs the morphism-space linear structure and nothing about weights.

Roadmap

This is the uniqueness input for the multiplicity m_λ = dim Hom_L(L(λ), M) of the decomposition toolkit in Layer 6 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md (the isotypicMultiplicity target of its Suggested.lean, whose "Hom definition is the one that makes uniqueness automatic"): the morphism space between irreducibles has dimension 1 or 0 according as they are equivalent. The multiplicity theorem itself is LieModule.isotypicMultiplicity_eq_ncard_of_isInternal of TauCeti/Algebra/Lie/Multiplicity.lean, which adds to this file the additivity of the morphism space over a direct-sum decomposition; the L(λ)-indexed form additionally needs the irreducible quotient L(λ).

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §6.1.
• The statements mirror the categorical CategoryTheory.finrank_hom_simple_simple of Mathlib/CategoryTheory/Preadditive/Schur.lean, which is unavailable here: Mathlib has no category of Lie modules over a fixed Lie algebra.

Over an arbitrary commutative ring

theorem TauCeti.LieModule.bijective_of_ne_zero {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] [LieModule.IsIrreducible R L M] [LieModule.IsIrreducible R L N] {f : M →ₗ⁅R,L⁆ N} (hf : f ≠ 0) : Function.Bijective ⇑f

Schur's lemma for Lie modules, in its bijectivity form: a nonzero morphism between irreducible Lie modules is bijective. Its kernel is a Lie submodule of M other than ⊤ and its range is a Lie submodule of N other than ⊥, and irreducibility leaves no other option.

theorem TauCeti.LieModule.nonempty_lieModuleEquiv_of_ne_zero {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] [LieModule.IsIrreducible R L M] [LieModule.IsIrreducible R L N] {f : M →ₗ⁅R,L⁆ N} (hf : f ≠ 0) : Nonempty (M ≃ₗ⁅R,L⁆ N)

A nonzero morphism between irreducible Lie modules makes them equivalent.

theorem TauCeti.LieModule.eq_zero_of_isEmpty_lieModuleEquiv {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] [LieModule.IsIrreducible R L M] [LieModule.IsIrreducible R L N] (h : IsEmpty (M ≃ₗ⁅R,L⁆ N)) (f : M →ₗ⁅R,L⁆ N) : f = 0

Inequivalent irreducible Lie modules admit only the zero morphism.

theorem TauCeti.LieModule.subsingleton_lieModuleHom_of_isEmpty_lieModuleEquiv {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] [LieModule.IsIrreducible R L M] [LieModule.IsIrreducible R L N] (h : IsEmpty (M ≃ₗ⁅R,L⁆ N)) : Subsingleton (M →ₗ⁅R,L⁆ N)

The morphism space between inequivalent irreducible Lie modules is trivial.

theorem TauCeti.LieModule.nonempty_lieModuleEquiv_iff_exists_ne_zero {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] [LieModule.IsIrreducible R L M] [LieModule.IsIrreducible R L N] : Nonempty (M ≃ₗ⁅R,L⁆ N) ↔ ∃ (f : M →ₗ⁅R,L⁆ N), f ≠ 0

Two irreducible Lie modules are equivalent exactly when they admit a nonzero morphism.

Over an algebraically closed field

theorem TauCeti.LieModule.finrank_lieModuleHom_self (K : Type u) (L : Type v) (M : Type w) [Field K] [IsAlgClosed 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] : Module.finrank K (M →ₗ⁅K,L⁆ M) = 1

The endomorphism space of a finite-dimensional irreducible Lie module is a line. Over an algebraically closed field Schur's lemma makes every endomorphism a scalar multiple of the identity, and the identity is nonzero because an irreducible module is nontrivial.

theorem TauCeti.LieModule.finrank_lieModuleHom_eq_one_of_nonempty_lieModuleEquiv (K : Type u) (L : Type v) {M : Type w} {N : Type w₁} [Field K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [AddCommGroup N] [Module K N] [LieRingModule L N] [LieModule K L N] [FiniteDimensional K M] [LieModule.IsIrreducible K L M] (h : Nonempty (M ≃ₗ⁅K,L⁆ N)) : Module.finrank K (M →ₗ⁅K,L⁆ N) = 1

Equivalent finite-dimensional irreducible Lie modules have a one-dimensional morphism space: postcomposing with the equivalence identifies it with the endomorphism space.

theorem TauCeti.LieModule.finrank_lieModuleHom_eq_zero_of_isEmpty_lieModuleEquiv (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] [AddCommGroup N] [Module K N] [LieRingModule L N] [LieModule K L N] [LieModule.IsIrreducible K L M] [LieModule.IsIrreducible K L N] (h : IsEmpty (M ≃ₗ⁅K,L⁆ N)) : Module.finrank K (M →ₗ⁅K,L⁆ N) = 0

Inequivalent irreducible Lie modules have a zero-dimensional morphism space.

theorem TauCeti.LieModule.finiteDimensional_lieModuleHom_of_isIrreducible (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] [AddCommGroup N] [Module K N] [LieRingModule L N] [LieModule K L N] [FiniteDimensional K M] [LieModule.IsIrreducible K L M] [LieModule.IsIrreducible K L N] : FiniteDimensional K (M →ₗ⁅K,L⁆ N)

The morphism space from a finite-dimensional irreducible Lie module to any irreducible Lie module is finite-dimensional: it is either trivial, when the two modules are inequivalent, or, transported along an equivalence, the endomorphism space of the finite-dimensional M.

theorem TauCeti.LieModule.finrank_lieModuleHom_eq_one_iff (K : Type u) (L : Type v) {M : Type w} {N : Type w₁} [Field K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [AddCommGroup N] [Module K N] [LieRingModule L N] [LieModule K L N] [FiniteDimensional K M] [LieModule.IsIrreducible K L M] [LieModule.IsIrreducible K L N] : Module.finrank K (M →ₗ⁅K,L⁆ N) = 1 ↔ Nonempty (M ≃ₗ⁅K,L⁆ N)

The morphism space of two finite-dimensional irreducible Lie modules is one-dimensional exactly when they are equivalent.

theorem TauCeti.LieModule.finrank_lieModuleHom_eq_zero_iff (K : Type u) (L : Type v) {M : Type w} {N : Type w₁} [Field K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [AddCommGroup N] [Module K N] [LieRingModule L N] [LieModule K L N] [FiniteDimensional K M] [LieModule.IsIrreducible K L M] [LieModule.IsIrreducible K L N] : Module.finrank K (M →ₗ⁅K,L⁆ N) = 0 ↔ IsEmpty (M ≃ₗ⁅K,L⁆ N)

The morphism space of two finite-dimensional irreducible Lie modules vanishes exactly when they are inequivalent.

theorem TauCeti.LieModule.finrank_lieModuleHom_le_one (K : Type u) (L : Type v) {M : Type w} {N : Type w₁} [Field K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [AddCommGroup N] [Module K N] [LieRingModule L N] [LieModule K L N] [FiniteDimensional K M] [LieModule.IsIrreducible K L M] [LieModule.IsIrreducible K L N] : Module.finrank K (M →ₗ⁅K,L⁆ N) ≤ 1

The morphism space of two finite-dimensional irreducible Lie modules is at most a line.

theorem TauCeti.LieModule.finrank_lieModuleHom (K : Type u) (L : Type v) {M : Type w} {N : Type w₁} [Field K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [AddCommGroup N] [Module K N] [LieRingModule L N] [LieModule K L N] [FiniteDimensional K M] [LieModule.IsIrreducible K L M] [LieModule.IsIrreducible K L N] : Module.finrank K (M →ₗ⁅K,L⁆ N) = if Nonempty (M ≃ₗ⁅K,L⁆ N) then 1 else 0

Schur's lemma for finite-dimensional irreducible Lie modules over an algebraically closed field, in its dimension form: the morphism space is a line for equivalent modules and zero for inequivalent ones. This is the per-summand contribution that a multiplicity count of S in M reads off dim_K (S →ₗ⁅K,L⁆ M), which additivity of the morphism space over a decomposition of M supplies: TauCeti.LieModule.finrank_lieModuleHom_eq_sum_of_isInternal of TauCeti/Algebra/Lie/Submodule/DirectSum.lean.