Every admissible lattice has a weight basis

The split maximal torus of TauCeti/Algebra/Lie/UniversalEnveloping/Kostant/RootSubgroup/Torus/Basic.lean, the matrix coordinates of TauCeti/Algebra/Lie/UniversalEnveloping/Kostant/RootSubgroup/Coordinate.lean and the group scheme generated by the root subgroups all take a weight basis of the Kostant-stable lattice M ≤ V as a hypothesis: an integral basis b : Basis η ℤ M together with wt : η → κ → ℤ such that every b x is a joint eigenvector of the designated Cartan operators with integral eigenvalues wt x. This file constructs one, so that nothing downstream has to assume it: a Kostant-stable subgroup that is finitely generated over ℤ and lies in the span of the integral joint weight spaces has a weight basis, and its weights are the finitely many weights of the lattice.

Three ingredients combine. Generic independence of joint eigenspaces separates the integral weights. Humphreys' Lemma 27.1 (TauCeti.UniversalEnvelopingAlgebra.jointWeightComponent_mem_of_kostantStable) says that M contains every joint weight component of each of its elements, which cuts M into weight sublattices summing to M. Finally, torsion-freeness of a rational vector space makes each weight sublattice a finitely generated torsion-free ℤ-module, hence free, because ℤ is a principal ideal domain. Collecting bases of the summands along the resulting internal direct sum (DirectSum.IsInternal.collectedBasis) produces the weight basis, indexed by pairs of a weight and a basis index of that weight sublattice.

The weight of a basis vector is therefore literally the first component of its index, so the weight function needs no separate construction: Sigma.fst is it. Only finitely many weights contribute, by generic finiteness of independent submodules in a finitely generated module (Submodule.finite_ne_bot_of_iSupIndep).

A ℤ-basis of a lattice is never canonical, and neither is this one: bases of the individual weight sublattices are chosen. What is canonical is the decomposition into weight sublattices, so the choice is confined to one weight space at a time.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.jointWeightSpace: the joint eigenspace of the designated Cartan operators for an integral weight.
• TauCeti.UniversalEnvelopingAlgebra.weightSublattice: the weight sublattice cut out of a subgroup M ≤ V by a weight.
• TauCeti.UniversalEnvelopingAlgebra.kostantWeightBasis: the weight basis itself, with TauCeti.UniversalEnvelopingAlgebra.isCartanWeightVector_kostantWeightBasis recording that its vectors have the advertised weights.
• TauCeti.UniversalEnvelopingAlgebra.kostantWeightBasisFin: the same basis indexed by Fin n, which is the shape the coordinate and group-scheme constructions consume.

Main results

• TauCeti.UniversalEnvelopingAlgebra.eq_zero_of_isCartanWeightVector_of_sum_eq_zero: vectors of pairwise distinct integral weights are independent.
• TauCeti.UniversalEnvelopingAlgebra.isInternal_weightSublattice: a Kostant-stable subgroup lying in the span of the integral joint weight spaces is their internal direct sum.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §27.1.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

Weight spaces and weight sublattices

def TauCeti.UniversalEnvelopingAlgebra.jointWeightSpace {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (μ : κ → ℤ) : Submodule ℚ V

The joint weight space of an integral weight μ: the vectors on which every designated Cartan vector h j acts by the scalar μ j.

Equations

• TauCeti.UniversalEnvelopingAlgebra.jointWeightSpace h ρ μ = ⨅ (j : κ), (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h j))).eigenspace ↑(μ j)

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mem_jointWeightSpace_iff {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) {μ : κ → ℤ} {x : V} : x ∈ jointWeightSpace h ρ μ ↔ IsCartanWeightVector h ρ μ x

Membership in a joint weight space is exactly being a weight vector for that weight.

def TauCeti.UniversalEnvelopingAlgebra.weightSublattice {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (μ : κ → ℤ) : Submodule ℤ ↥M

The weight sublattice of weight μ of a subgroup M ≤ V: the part of M on which every designated Cartan vector h j acts by the scalar μ j.

Equations

• TauCeti.UniversalEnvelopingAlgebra.weightSublattice h ρ M μ = Submodule.comap M.subtype.toIntLinearMap (Submodule.restrictScalars ℤ (TauCeti.UniversalEnvelopingAlgebra.jointWeightSpace h ρ μ))

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mem_weightSublattice_iff {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) {μ : κ → ℤ} {x : ↥M} : x ∈ weightSublattice h ρ M μ ↔ IsCartanWeightVector h ρ μ ↑x

Independence of weight vectors

theorem TauCeti.UniversalEnvelopingAlgebra.eq_zero_of_isCartanWeightVector_of_sum_eq_zero {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) {s : Finset (κ → ℤ)} {w : (κ → ℤ) → V} (hw : ∀ l ∈ s, IsCartanWeightVector h ρ l (w l)) (hsum : ∑ l ∈ s, w l = 0) {l₀ : κ → ℤ} (hl₀ : l₀ ∈ s) : w l₀ = 0

Weight vectors of pairwise distinct weights are independent. If a finite family of joint eigenvectors of the designated Cartan operators, indexed by pairwise distinct integral weights, sums to zero, then every member of the family is zero.

theorem TauCeti.UniversalEnvelopingAlgebra.iSupIndep_weightSublattice {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) : iSupIndep (weightSublattice h ρ M)

The weight sublattices of a subgroup are independent.

theorem TauCeti.UniversalEnvelopingAlgebra.iSup_weightSublattice_eq_top {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hV : ∀ (x : ↥M), ↑x ∈ ⨆ (μ : κ → ℤ), jointWeightSpace h ρ μ) : ⨆ (μ : κ → ℤ), weightSublattice h ρ M μ = ⊤

A Kostant-stable subgroup is spanned by its weight sublattices, provided each of its elements lies in the span of the joint weight spaces.

theorem TauCeti.UniversalEnvelopingAlgebra.isInternal_weightSublattice {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) [DecidableEq (κ → ℤ)] (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hV : ∀ (x : ↥M), ↑x ∈ ⨆ (μ : κ → ℤ), jointWeightSpace h ρ μ) : DirectSum.IsInternal (weightSublattice h ρ M)

An admissible lattice is the direct sum of its weight sublattices. The DecidableEq hypothesis is the one DirectSum.IsInternal itself carries; the constructions below supply it classically, so it does not propagate into the weight basis.

The weight basis

instance TauCeti.UniversalEnvelopingAlgebra.instFreeWeightSublattice {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) [Module.Finite ℤ ↥M] (μ : κ → ℤ) : Module.Free ℤ ↥(weightSublattice h ρ M μ)

The weight sublattices of a finitely generated lattice in a rational vector space are finitely generated and torsion-free, hence free: ℤ is a principal ideal domain.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantWeightBasis {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) [Module.Finite ℤ ↥M] (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hV : ∀ (x : ↥M), ↑x ∈ ⨆ (μ : κ → ℤ), jointWeightSpace h ρ μ) : Module.Basis ((μ : κ → ℤ) × Module.Free.ChooseBasisIndex ℤ ↥(weightSublattice h ρ M μ)) ℤ ↥M

A weight basis of an admissible lattice. A finitely generated Kostant-stable subgroup lying in the span of the integral weight spaces has a basis of weight vectors: collect a basis of each weight sublattice along the direct-sum decomposition.

The weight of the basis vector indexed by a is the first component a.1 of its index, so Sigma.fst is the weight function such a basis is paired with; TauCeti.UniversalEnvelopingAlgebra.isCartanWeightVector_kostantWeightBasis is the corresponding weight hypothesis.

Equations

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

theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeightBasis_mem {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) [Module.Finite ℤ ↥M] (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hV : ∀ (x : ↥M), ↑x ∈ ⨆ (μ : κ → ℤ), jointWeightSpace h ρ μ) (a : (μ : κ → ℤ) × Module.Free.ChooseBasisIndex ℤ ↥(weightSublattice h ρ M μ)) : (kostantWeightBasis e h ρ M hM hV) a ∈ weightSublattice h ρ M a.fst

Each vector of the weight basis lies in the weight sublattice its index names.

theorem TauCeti.UniversalEnvelopingAlgebra.isCartanWeightVector_kostantWeightBasis {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) [Module.Finite ℤ ↥M] (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hV : ∀ (x : ↥M), ↑x ∈ ⨆ (μ : κ → ℤ), jointWeightSpace h ρ μ) (a : (μ : κ → ℤ) × Module.Free.ChooseBasisIndex ℤ ↥(weightSublattice h ρ M μ)) : IsCartanWeightVector h ρ a.fst ↑((kostantWeightBasis e h ρ M hM hV) a)

The weight basis consists of weight vectors, of the weights recorded by the first component of the index. This is the weight hypothesis that the split maximal torus, the matrix coordinates and the generated group scheme take as given.

theorem TauCeti.UniversalEnvelopingAlgebra.finite_kostantWeightBasis_index {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) [Module.Finite ℤ ↥M] (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hV : ∀ (x : ↥M), ↑x ∈ ⨆ (μ : κ → ℤ), jointWeightSpace h ρ μ) : Finite ((μ : κ → ℤ) × Module.Free.ChooseBasisIndex ℤ ↥(weightSublattice h ρ M μ))

The index of the weight basis is finite, since the lattice is finitely generated.

theorem TauCeti.UniversalEnvelopingAlgebra.nat_card_kostantWeightBasis_index_eq_finrank {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) [Module.Finite ℤ ↥M] (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hV : ∀ (x : ↥M), ↑x ∈ ⨆ (μ : κ → ℤ), jointWeightSpace h ρ μ) : Nat.card ((μ : κ → ℤ) × Module.Free.ChooseBasisIndex ℤ ↥(weightSublattice h ρ M μ)) = Module.finrank ℤ ↥M

The weight basis has one vector for each unit of rank: its index has cardinality the rank of the lattice, which is therefore the length of the Fin-indexed reindexing TauCeti.UniversalEnvelopingAlgebra.kostantWeightBasisFin.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantWeightBasisIndexEquivFin {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) [Module.Finite ℤ ↥M] (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hV : ∀ (x : ↥M), ↑x ∈ ⨆ (μ : κ → ℤ), jointWeightSpace h ρ μ) : (μ : κ → ℤ) × Module.Free.ChooseBasisIndex ℤ ↥(weightSublattice h ρ M μ) ≃ Fin (Nat.card ((μ : κ → ℤ) × Module.Free.ChooseBasisIndex ℤ ↥(weightSublattice h ρ M μ)))

The numbering of the weight-basis index by Fin n along which the weight basis is reindexed; it exists because the index is finite.

Equations

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

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantWeightBasisFin {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) [Module.Finite ℤ ↥M] (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hV : ∀ (x : ↥M), ↑x ∈ ⨆ (μ : κ → ℤ), jointWeightSpace h ρ μ) : Module.Basis (Fin (Nat.card ((μ : κ → ℤ) × Module.Free.ChooseBasisIndex ℤ ↥(weightSublattice h ρ M μ)))) ℤ ↥M

The weight basis reindexed by Fin n, the shape in which the coordinate and group-scheme constructions read a basis of an admissible lattice.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeightBasisFin_apply {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) [Module.Finite ℤ ↥M] (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hV : ∀ (x : ↥M), ↑x ∈ ⨆ (μ : κ → ℤ), jointWeightSpace h ρ μ) (x : Fin (Nat.card ((μ : κ → ℤ) × Module.Free.ChooseBasisIndex ℤ ↥(weightSublattice h ρ M μ)))) : (kostantWeightBasisFin e h ρ M hM hV) x = (kostantWeightBasis e h ρ M hM hV) ((kostantWeightBasisIndexEquivFin e h ρ M hM hV).symm x)

The Fin-indexed weight basis is the weight basis read through the numbering of its index.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantWeightFin {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) [Module.Finite ℤ ↥M] (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hV : ∀ (x : ↥M), ↑x ∈ ⨆ (μ : κ → ℤ), jointWeightSpace h ρ μ) : Fin (Nat.card ((μ : κ → ℤ) × Module.Free.ChooseBasisIndex ℤ ↥(weightSublattice h ρ M μ))) → κ → ℤ

The weight of the x-th vector of the Fin-indexed weight basis.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantWeightFin e h ρ M hM hV x = ((TauCeti.UniversalEnvelopingAlgebra.kostantWeightBasisIndexEquivFin e h ρ M hM hV).symm x).fst

theorem TauCeti.UniversalEnvelopingAlgebra.isCartanWeightVector_kostantWeightBasisFin {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) [Module.Finite ℤ ↥M] (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hV : ∀ (x : ↥M), ↑x ∈ ⨆ (μ : κ → ℤ), jointWeightSpace h ρ μ) (x : Fin (Nat.card ((μ : κ → ℤ) × Module.Free.ChooseBasisIndex ℤ ↥(weightSublattice h ρ M μ)))) : IsCartanWeightVector h ρ (kostantWeightFin e h ρ M hM hV x) ↑((kostantWeightBasisFin e h ρ M hM hV) x)

The Fin-indexed weight basis consists of weight vectors of the recorded weights.