The rational form of a minuscule weight table

The raising and lowering generators named by a minuscule weight table have zero-one integer entries, while its diagonal Cartan generators contain the integral weights. Coercing these entries into ℚ gives matrices satisfying the same Serre relations: entrywise coercion is a homomorphism of Lie rings and the adjoint action does not depend on the base ring. The resulting matrices define a representation of the rational Serre algebra on the rational coordinate space of the index type.

Main declarations

• TauCeti.MinusculeWeightTable.Symmetry.moduleEquiv: the rational coordinate permutation induced by a table symmetry.
• TauCeti.MinusculeWeightTable.raisingMatrixQ, loweringMatrixQ and cartanGeneratorMatrixQ: the rational Chevalley generators.
• TauCeti.MinusculeWeightTable.rationalSerreRepresentation: the representation of the rational Serre presentation they define.

Main results

• TauCeti.MinusculeWeightTable.raisingMatrixQ_apply, loweringMatrixQ_apply and cartanGeneratorMatrixQ_apply: their entry formulas.
• TauCeti.MinusculeWeightTable.raisingMatrixQ_pow_two and loweringMatrixQ_pow_two: the raising and lowering matrices are square-zero.
• TauCeti.MinusculeWeightTable.Symmetry.raisingMatrixQ_submatrix and loweringMatrixQ_submatrix: a table symmetry carries each rational raising or lowering matrix to the one at the image node.
• TauCeti.MinusculeWeightTable.isSerreSystemQ: the rational generators satisfy the Serre relations of the table's Cartan matrix.
• TauCeti.MinusculeWeightTable.isSl2TripleQ: the rational generators at a nonzero node form an sl₂ triple.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§26--27.

The coordinate permutation of a symmetry

def TauCeti.MinusculeWeightTable.Symmetry.moduleEquiv {B : Type u_1} {ι : Type u_2} {T : MinusculeWeightTable B ι} (S : T.Symmetry) : (ι → ℚ) ≃ₗ[ℚ] ι → ℚ

The coordinate permutation of the rational module induced by a table symmetry. It carries the standard basis vector at a to the standard basis vector at S.indexPerm a, so a coordinate vector v to v ∘ S.indexPerm⁻¹.

Equations

• S.moduleEquiv = LinearEquiv.piCongrLeft' ℚ (fun (x : ι) => ℚ) S.indexPerm

@[simp]

theorem TauCeti.MinusculeWeightTable.Symmetry.moduleEquiv_apply {B : Type u_1} {ι : Type u_2} {T : MinusculeWeightTable B ι} (S : T.Symmetry) (v : ι → ℚ) (a : ι) : S.moduleEquiv v a = v ((Equiv.symm S.indexPerm) a)

@[simp]

theorem TauCeti.MinusculeWeightTable.Symmetry.moduleEquiv_single {B : Type u_1} {ι : Type u_2} {T : MinusculeWeightTable B ι} (S : T.Symmetry) [DecidableEq ι] (a : ι) : S.moduleEquiv (Pi.single a 1) = Pi.single (S.indexPerm a) 1

The coordinate permutation of a symmetry carries each standard basis vector to the one at the permuted index.

@[simp]

theorem TauCeti.MinusculeWeightTable.Symmetry.moduleEquiv_one {B : Type u_1} {ι : Type u_2} {T : MinusculeWeightTable B ι} : moduleEquiv 1 = 1

@[simp]

theorem TauCeti.MinusculeWeightTable.Symmetry.moduleEquiv_mul {B : Type u_1} {ι : Type u_2} {T : MinusculeWeightTable B ι} (S R : T.Symmetry) : (S * R).moduleEquiv = S.moduleEquiv * R.moduleEquiv

@[simp]

theorem TauCeti.MinusculeWeightTable.Symmetry.moduleEquiv_pow {B : Type u_1} {ι : Type u_2} {T : MinusculeWeightTable B ι} (S : T.Symmetry) (m : ℕ) : (S ^ m).moduleEquiv = S.moduleEquiv ^ m

The rational Chevalley generators

noncomputable def TauCeti.MinusculeWeightTable.raisingMatrixQ {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) (i : B) : Matrix ι ι ℚ

The rational raising matrix of the i-th simple root.

Equations

• T.raisingMatrixQ i = (TauCeti.matrixIntCastLieHom ℚ) (T.raisingMatrix i)

noncomputable def TauCeti.MinusculeWeightTable.loweringMatrixQ {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) (i : B) : Matrix ι ι ℚ

The rational lowering matrix of the i-th simple root.

Equations

• T.loweringMatrixQ i = (TauCeti.matrixIntCastLieHom ℚ) (T.loweringMatrix i)

noncomputable def TauCeti.MinusculeWeightTable.cartanGeneratorMatrixQ {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) (i : B) : Matrix ι ι ℚ

The rational Cartan generator matrix of the i-th simple coroot.

Equations

• T.cartanGeneratorMatrixQ i = (TauCeti.matrixIntCastLieHom ℚ) (T.cartanGeneratorMatrix i)

@[simp]

theorem TauCeti.MinusculeWeightTable.raisingMatrixQ_apply {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) (i : B) (a b : ι) : T.raisingMatrixQ i a b = if T.weight b i = -1 ∧ a = T.reflection i b then 1 else 0

The entries of a rational raising matrix are the zero-one coefficients of the integral one.

@[simp]

theorem TauCeti.MinusculeWeightTable.loweringMatrixQ_apply {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) (i : B) (a b : ι) : T.loweringMatrixQ i a b = if T.weight b i = 1 ∧ a = T.reflection i b then 1 else 0

The entries of a rational lowering matrix are the zero-one coefficients of the integral one.

@[simp]

theorem TauCeti.MinusculeWeightTable.cartanGeneratorMatrixQ_apply {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) (i : B) (a b : ι) : T.cartanGeneratorMatrixQ i a b = if a = b then ↑(T.weight b i) else 0

The rational Cartan generator is diagonal with the table's weights on its diagonal.

@[simp]

theorem TauCeti.MinusculeWeightTable.raisingMatrixQ_pow_two {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) (i : B) : T.raisingMatrixQ i ^ 2 = 0

Every rational raising matrix is square-zero.

@[simp]

theorem TauCeti.MinusculeWeightTable.loweringMatrixQ_pow_two {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) (i : B) : T.loweringMatrixQ i ^ 2 = 0

Every rational lowering matrix is square-zero.

@[simp]

theorem TauCeti.MinusculeWeightTable.Symmetry.raisingMatrixQ_submatrix {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] {T : MinusculeWeightTable B ι} (S : T.Symmetry) (i : B) : (T.raisingMatrixQ (S.nodePerm i)).submatrix ⇑S.indexPerm ⇑S.indexPerm = T.raisingMatrixQ i

Reindexing a rational raising matrix by a table symmetry gives the rational raising matrix at the original node.

@[simp]

theorem TauCeti.MinusculeWeightTable.Symmetry.loweringMatrixQ_submatrix {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] {T : MinusculeWeightTable B ι} (S : T.Symmetry) (i : B) : (T.loweringMatrixQ (S.nodePerm i)).submatrix ⇑S.indexPerm ⇑S.indexPerm = T.loweringMatrixQ i

Reindexing a rational lowering matrix by a table symmetry gives the rational lowering matrix at the original node.

The rational Serre presentation

theorem TauCeti.MinusculeWeightTable.isSerreSystemQ {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) : IsSerreSystem ℚ T.cartanMatrix T.cartanGeneratorMatrixQ T.raisingMatrixQ T.loweringMatrixQ

The rational matrices of a minuscule weight table satisfy the Serre relations of its Cartan matrix.

theorem TauCeti.MinusculeWeightTable.isSl2TripleQ {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) (i : B) (hi : ∃ (a : ι), T.weight a i ≠ 0) : IsSl2Triple (T.cartanGeneratorMatrixQ i) (T.raisingMatrixQ i) (T.loweringMatrixQ i)

At a node carrying a weight of nonzero coordinate, the rational Cartan, raising, and lowering matrices form an sl₂ triple.

noncomputable def TauCeti.MinusculeWeightTable.rationalSerreRepresentation {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) [DecidableEq B] : Matrix.ToLieAlgebra ℚ T.cartanMatrix →ₗ⁅ℚ⁆ Matrix ι ι ℚ

The rational representation of the Serre presentation named by a minuscule weight table.

Equations

• T.rationalSerreRepresentation = TauCeti.serreLift ⋯

@[simp]

theorem TauCeti.MinusculeWeightTable.rationalSerreRepresentation_serreH {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) [DecidableEq B] (i : B) : T.rationalSerreRepresentation (serreH ℚ T.cartanMatrix i) = T.cartanGeneratorMatrixQ i

The rational representation sends a Cartan generator to its diagonal weight matrix.

@[simp]

theorem TauCeti.MinusculeWeightTable.rationalSerreRepresentation_serreE {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) [DecidableEq B] (i : B) : T.rationalSerreRepresentation (serreE ℚ T.cartanMatrix i) = T.raisingMatrixQ i

The rational representation sends a positive generator to its raising matrix.

@[simp]

theorem TauCeti.MinusculeWeightTable.rationalSerreRepresentation_serreF {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) [DecidableEq B] (i : B) : T.rationalSerreRepresentation (serreF ℚ T.cartanMatrix i) = T.loweringMatrixQ i

The rational representation sends a negative generator to its lowering matrix.