Elementary identities for Lie algebra weights

This file records general identities for weights that are used by several parts of the Lie algebra weight-space theory. The transport and finrank identities hold over any commutative ring.

Main results

• LieModule.map_weightSpace_le: a Lie-module homomorphism preserves each weight space.
• LieModule.comap_weightSpace_eq_of_injective: the preimage under an injective Lie-module homomorphism is the corresponding source weight space.
• LieModule.map_weightSpace_eq_of_injective: an injective Lie-module homomorphism identifies a weight space with the intersection of the target weight space and its range.
• LieModule.map_weightSpace_eq: a Lie-module equivalence maps each weight space onto the corresponding weight space.
• LieModuleEquiv.finrank_weightSpace_eq: equivalent Lie modules have weight spaces of equal dimension.
• LieSubmodule.toSubmodule_map_weightSpace_incl: inclusion identifies a submodule's weight space with its intersection with the ambient weight space.
• LieSubmodule.finrank_inf_weightSpace: that intersection has the dimension of the submodule's weight space.
• LieSubmodule.toSubmodule_map_genWeightSpace_incl: inclusion identifies a submodule's generalized weight space with its intersection with the ambient generalized weight space.
• LieSubmodule.finrank_inf_genWeightSpace: that intersection has the dimension of the submodule's generalized weight space.
• Ado.Weight.coe_neg_eq_add_of_coe_eq_add: reading a vanishing sum of four weights as an equation between opposite pair sums.

References

The weight-space transport family follows the generalized-weight-space API LieModule.map_genWeightSpace_le through LieModule.map_genWeightSpace_eq in Mathlib.Algebra.Lie.Weights.Basic.

theorem LieModule.map_weightSpace_le {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] (f : M →ₗ⁅R,L⁆ M₂) (χ : L → R) : LieSubmodule.map f (weightSpace M χ) ≤ weightSpace M₂ χ

A morphism of Lie modules sends a weight space into the corresponding weight space.

theorem LieModule.comap_weightSpace_eq_of_injective {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] {f : M →ₗ⁅R,L⁆ M₂} (χ : L → R) (hf : Function.Injective ⇑f) : LieSubmodule.comap f (weightSpace M₂ χ) = weightSpace M χ

The preimage of a weight space under an injective Lie-module homomorphism is the corresponding weight space in the source.

theorem LieModule.map_weightSpace_eq_of_injective {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] {f : M →ₗ⁅R,L⁆ M₂} (χ : L → R) (hf : Function.Injective ⇑f) : LieSubmodule.map f (weightSpace M χ) = weightSpace M₂ χ ⊓ f.range

Under an injective Lie-module homomorphism, the image of a weight space is the intersection of the corresponding target weight space with the range.

theorem LieModule.map_weightSpace_eq {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] (e : M ≃ₗ⁅R,L⁆ M₂) (χ : L → R) : LieSubmodule.map e.toLieModuleHom (weightSpace M χ) = weightSpace M₂ χ

A Lie-module equivalence maps a weight space onto the corresponding weight space.

theorem LieModuleEquiv.finrank_weightSpace_eq {K : Type u_1} {L : Type u_2} {M : Type u_3} {P : Type u_4} [CommRing K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [AddCommGroup P] [Module K P] [LieRingModule L P] [LieModule K L P] (e : M ≃ₗ⁅K,L⁆ P) (χ : L → K) : Module.finrank K ↥(LieModule.weightSpace M χ) = Module.finrank K ↥(LieModule.weightSpace P χ)

Weight-space finrank is an isomorphism invariant. An equivalence of Lie modules over a commutative ring carries the χ-weight space of one module onto that of the other.

theorem LieSubmodule.toSubmodule_map_weightSpace_incl {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {H : LieSubalgebra R L} (N : LieSubmodule R L M) (χ : ↥H → R) : ↑(map (N.incl.restrictLie H) (LieModule.weightSpace (↥N) χ)) = ↑(LieModule.weightSpace M χ) ⊓ ↑N

Inclusion of a Lie submodule identifies its weight space with the intersection of the ambient weight space and its carrier.

theorem LieSubmodule.finrank_inf_weightSpace {L : Type u_2} {M : Type u_3} [LieRing L] [AddCommGroup M] [LieRingModule L M] {K : Type u_4} [CommRing K] [LieAlgebra K L] [Module K M] [LieModule K L M] {H : LieSubalgebra K L} (N : LieSubmodule K L M) (χ : ↥H → K) : Module.finrank K ↥(↑(LieModule.weightSpace M χ) ⊓ ↑N) = Module.finrank K ↥(LieModule.weightSpace (↥N) χ)

The intersection of an ambient weight space with a Lie submodule has the dimension of the corresponding weight space in the submodule.

theorem LieSubmodule.toSubmodule_map_genWeightSpace_incl {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {H : LieSubalgebra R L} [LieRing.IsNilpotent ↥H] (N : LieSubmodule R L M) (χ : ↥H → R) : ↑(map (N.incl.restrictLie H) (LieModule.genWeightSpace (↥N) χ)) = ↑(LieModule.genWeightSpace M χ) ⊓ ↑N

Inclusion of a Lie submodule identifies its generalized weight space with the intersection of the ambient generalized weight space and its carrier.

theorem LieSubmodule.finrank_inf_genWeightSpace {L : Type u_2} {M : Type u_3} [LieRing L] [AddCommGroup M] [LieRingModule L M] {K : Type u_4} [CommRing K] [LieAlgebra K L] [Module K M] [LieModule K L M] {H : LieSubalgebra K L} [LieRing.IsNilpotent ↥H] (N : LieSubmodule K L M) (χ : ↥H → K) : Module.finrank K ↥(↑(LieModule.genWeightSpace M χ) ⊓ ↑N) = Module.finrank K ↥(LieModule.genWeightSpace (↥N) χ)

The intersection of an ambient generalized weight space with a Lie submodule has the dimension of the corresponding generalized weight space in the submodule.

theorem Ado.Weight.coe_neg_eq_add_of_coe_eq_add {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {μ : LieModule.Weight K (↥H) L} {a b c d : ↥H → K} (hsum : a + b + c + d = 0) (hμ : ⇑μ = a + b) : ⇑(-μ) = c + d

If four weights sum to zero and a weight μ names the sum of the first two, then -μ names the sum of the last two.