Exact sequences and generalized weight spaces

Let a nilpotent Lie algebra L act on finite-dimensional triangularizable modules. This file proves that a surjective homomorphism of L-modules remains surjective after restriction to any generalized weight space. Consequently a short exact sequence of modules restricts to a short exact sequence on every generalized weight space, and the dimensions of corresponding weight spaces are additive.

The nontrivial point is surjectivity. Given a vector of weight χ in the target, choose an arbitrary preimage and decompose it into generalized weight components. Equivariance sends each component into the corresponding target weight space. Projecting the resulting sum onto χ therefore gives a preimage lying in the χ-weight space.

Main definitions and results

• TauCeti.genWeightSpaceMap: the restriction of a Lie-module homomorphism to a generalized weight space.
• TauCeti.genWeightSpaceMap_surjective: surjectivity is preserved by this restriction for finite-dimensional triangularizable modules.
• TauCeti.genWeightSpaceMap_exact: an exact pair restricts to an exact pair when its first map is injective.
• TauCeti.finrank_genWeightSpace_add_finrank_genWeightSpace_eq: generalized weight-space dimensions are additive in a short exact sequence.

Roadmap

This is the weight-space input for additivity of formal characters in Layer 6, "Formal characters", of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §22.5.

def TauCeti.genWeightSpaceMap {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (f : M →ₗ⁅R,L⁆ N) (χ : L → R) : ↥(LieModule.genWeightSpace M χ) →ₗ[R] ↥(LieModule.genWeightSpace N χ)

The restriction of a Lie-module homomorphism to the generalized weight space at χ.

Equations

• TauCeti.genWeightSpaceMap f χ = ↑(LieModuleHom.codRestrict (LieModule.genWeightSpace N χ) (f.comp (LieModule.genWeightSpace M χ).incl) ⋯)

@[simp]

theorem TauCeti.coe_genWeightSpaceMap_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (f : M →ₗ⁅R,L⁆ N) (χ : L → R) (m : ↥(LieModule.genWeightSpace M χ)) : ↑((genWeightSpaceMap f χ) m) = f ↑m

Restricting a Lie-module homomorphism to a generalized weight space does not change its underlying values.

theorem TauCeti.genWeightSpaceMap_injective {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (f : M →ₗ⁅R,L⁆ N) (χ : L → R) (hf : Function.Injective ⇑f) : Function.Injective ⇑(genWeightSpaceMap f χ)

An injective Lie-module homomorphism is injective on every generalized weight space.

Surjective maps

theorem TauCeti.genWeightSpaceMap_surjective {K : Type u} {L : Type v} {M : Type w} {N : Type w₁} [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent 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] [FiniteDimensional K N] [LieModule.IsTriangularizable K L M] [LieModule.IsTriangularizable K L N] (f : M →ₗ⁅K,L⁆ N) (hf : Function.Surjective ⇑f) (χ : L → K) : Function.Surjective ⇑(genWeightSpaceMap f χ)

A surjective homomorphism between finite-dimensional triangularizable Lie modules maps every generalized weight space onto the corresponding generalized weight space.

Short exact sequences

theorem TauCeti.genWeightSpaceMap_exact {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] [AddCommGroup P] [Module R P] [LieRingModule L P] [LieModule R L P] (f : M →ₗ⁅R,L⁆ N) (g : N →ₗ⁅R,L⁆ P) (h : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (χ : L → R) : Function.Exact ⇑(genWeightSpaceMap f χ) ⇑(genWeightSpaceMap g χ)

An exact pair of Lie-module homomorphisms restricts to an exact pair on each generalized weight space when the first homomorphism is injective.

theorem TauCeti.finrank_genWeightSpace_add_finrank_genWeightSpace_eq {K : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent 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] [AddCommGroup P] [Module K P] [LieRingModule L P] [LieModule K L P] [FiniteDimensional K N] [FiniteDimensional K P] [LieModule.IsTriangularizable K L N] [LieModule.IsTriangularizable K L P] (f : M →ₗ⁅K,L⁆ N) (g : N →ₗ⁅K,L⁆ P) (h : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) (χ : L → K) : Module.finrank K ↥(LieModule.genWeightSpace M χ) + Module.finrank K ↥(LieModule.genWeightSpace P χ) = Module.finrank K ↥(LieModule.genWeightSpace N χ)

Generalized weight-space dimensions are additive in a short exact sequence.