Chevalley generators from a minuscule weight table

A minuscule weight table for a generalized Cartan matrix determines a representation of the Serre presentation of that matrix: each weight pairs with every simple coroot to -1, 0 or 1, the simple reflections permute the weights, and the raising operator at a node moves a weight whose coordinate is -1 to its reflection and kills every other weight, the lowering operator dually. Every nonzero entry of the resulting matrices is 1, so the representation needs no structure constants. The main application is to minuscule representations of simple Lie algebras, which are determined by such tables. Nothing here needs the diagram to be simply laced: the spin representation of type B and the standard representation of type C are minuscule as well.

This file packages that data as TauCeti.MinusculeWeightTable and builds from it the three families of integral matrices, proves they are an sl₂ triple at each node admitting a weight with coordinate -1 and that they satisfy the Serre relations, and lifts them to a representation of the Serre presentation. A type-specific carrier then supplies only its weight table and reads the whole construction off.

The Cartan matrix is only required to be a generalized Cartan matrix: diagonal entries 2, nonpositive off-diagonal entries, and CM i j = 0 exactly when CM j i = 0. It follows the convention of Matrix.ToLieAlgebra, in which ⁅hᵢ, eⱼ⁆ = CM i j • eⱼ, so CM i j is the pairing of the j-th simple root with the i-th simple coroot. The coordinates are pairings with simple coroots, so the reflection equation reads wt (s_i a) j = wt a j - wt a i * CM j i.

Main declarations

• TauCeti.MinusculeWeightTable: the weight-table data and the conditions on it, with TauCeti.MinusculeWeightTable.ext reducing equality of tables to equality of their Cartan matrices and their weights.
• TauCeti.MinusculeWeightTable.Symmetry: compatible permutations of the simple nodes and weight indices, with derived equivariance laws for reflections and Chevalley generators, and TauCeti.MinusculeWeightTable.Symmetry.rootPerm the permutation it induces on the positive and negative simple-root indices.
• TauCeti.MinusculeWeightTable.raisingMatrix, loweringMatrix and cartanGeneratorMatrix: the integral Chevalley generators the table names.
• TauCeti.MinusculeWeightTable.serreRepresentation: the representation of the Serre presentation they define.

Main results

• TauCeti.MinusculeWeightTable.raisingMatrix_apply, loweringMatrix_apply and cartanGeneratorMatrix_apply: their entry formulas.
• TauCeti.MinusculeWeightTable.raisingMatrix_pow_two and loweringMatrix_pow_two: the raising and lowering matrices square to zero.
• TauCeti.MinusculeWeightTable.isSl2Triple: the three matrices at a node are an sl₂ triple when some weight has coordinate -1 at that node.
• TauCeti.MinusculeWeightTable.isSerreSystem: they satisfy the Serre relations.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §13.4, for the minuscule-orbit description of these representations.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, for the numbering conventions.

structure TauCeti.MinusculeWeightTable (B : Type u_1) (ι : Type u_2) : Type (max u_1 u_2)

A minuscule weight table for a generalized Cartan matrix. The weights are recorded in simple-coroot coordinates, so weight a i is the pairing of the a-th weight with the i-th simple coroot, and the simple reflection at i acts on the table by reflection i.

• cartanMatrix : Matrix B B ℤ

  The Cartan matrix, with the root index second: cartanMatrix i j is the pairing of the j-th simple root with the i-th simple coroot.

• weight : ι → B → ℤ

  The weights, in simple-coroot coordinates.

• reflection : B → ι → ι

  The permutation of the table induced by the i-th simple reflection.

• cartanMatrix_diag (i : B) : self.cartanMatrix i i = 2

  The Cartan matrix has diagonal entries 2.

• cartanMatrix_offDiag_nonpos (i j : B) : i ≠ j → self.cartanMatrix i j ≤ 0

  The off-diagonal entries of the Cartan matrix are nonpositive.

• cartanMatrix_zero_comm (i j : B) : self.cartanMatrix i j = 0 ↔ self.cartanMatrix j i = 0

  An entry of the Cartan matrix vanishes exactly when its transpose entry does.

• weight_eq_neg_one_or_eq_zero_or_eq_one (a : ι) (i : B) : self.weight a i = -1 ∨ self.weight a i = 0 ∨ self.weight a i = 1

  Minusculeness: every coordinate of every weight is -1, 0 or 1.

• weight_reflection (i : B) (a : ι) (j : B) : self.weight (self.reflection i a) j = self.weight a j - self.weight a i * self.cartanMatrix j i

  The reflection equation wt (s_i a) j = wt a j - wt a i * CM j i.

• weight_injective : Function.Injective self.weight

  Distinct indices name distinct weights.

Extensionality

theorem TauCeti.MinusculeWeightTable.ext {B : Type u_1} {ι : Type u_2} {T₁ T₂ : MinusculeWeightTable B ι} (hcartan : T₁.cartanMatrix = T₂.cartanMatrix) (hweight : T₁.weight = T₂.weight) : T₁ = T₂

A minuscule weight table is determined by its Cartan matrix and its weights. The simple reflections are determined by them through the reflection equation, the weights being injective, and the remaining fields are proofs.

theorem TauCeti.MinusculeWeightTable.ext_iff {B : Type u_1} {ι : Type u_2} {T₁ T₂ : MinusculeWeightTable B ι} : T₁ = T₂ ↔ T₁.cartanMatrix = T₂.cartanMatrix ∧ T₁.weight = T₂.weight

Symmetries

structure TauCeti.MinusculeWeightTable.Symmetry {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) : Type (max u_1 u_2)

A symmetry of a minuscule weight table. It consists of compatible permutations of the simple nodes and the weight indices which preserve the Cartan matrix and the weight coordinates. The reflection permutations and Chevalley-generator matrices are then equivariant automatically.

• nodePerm : Equiv.Perm B

  The induced permutation of the simple nodes.

• indexPerm : Equiv.Perm ι

  The induced permutation of the weight indices.

• weight_apply (a : ι) (i : B) : T.weight (self.indexPerm a) (self.nodePerm i) = T.weight a i

  The weight coordinates are equivariant for the two permutations.

• cartanMatrix_apply (i j : B) : T.cartanMatrix (self.nodePerm i) (self.nodePerm j) = T.cartanMatrix i j

  The node permutation preserves the Cartan matrix.

theorem TauCeti.MinusculeWeightTable.Symmetry.ext {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) {S R : T.Symmetry} (hnode : S.nodePerm = R.nodePerm) (hindex : S.indexPerm = R.indexPerm) : S = R

Two symmetries of a minuscule weight table are equal when their node and weight-index permutations are equal.

theorem TauCeti.MinusculeWeightTable.Symmetry.ext_iff {B : Type u_1} {ι : Type u_2} {T : MinusculeWeightTable B ι} {S R : T.Symmetry} : S = R ↔ S.nodePerm = R.nodePerm ∧ S.indexPerm = R.indexPerm

theorem TauCeti.MinusculeWeightTable.Symmetry.permPair_injective {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) : Function.Injective fun (S : T.Symmetry) => (S.nodePerm, S.indexPerm)

A symmetry is determined by its pair of node and weight-index permutations.

def TauCeti.MinusculeWeightTable.Symmetry.identity {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) : T.Symmetry

The identity symmetry of a minuscule weight table.

Equations

• TauCeti.MinusculeWeightTable.Symmetry.identity T = { nodePerm := 1, indexPerm := 1, weight_apply := ⋯, cartanMatrix_apply := ⋯ }

def TauCeti.MinusculeWeightTable.Symmetry.comp {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) (S R : T.Symmetry) : T.Symmetry

The composite of two symmetries of a minuscule weight table.

Equations

• TauCeti.MinusculeWeightTable.Symmetry.comp T S R = { nodePerm := S.nodePerm * R.nodePerm, indexPerm := S.indexPerm * R.indexPerm, weight_apply := ⋯, cartanMatrix_apply := ⋯ }

def TauCeti.MinusculeWeightTable.Symmetry.inverse {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) (S : T.Symmetry) : T.Symmetry

The inverse of a symmetry of a minuscule weight table.

Equations

• TauCeti.MinusculeWeightTable.Symmetry.inverse T S = { nodePerm := S.nodePerm⁻¹, indexPerm := S.indexPerm⁻¹, weight_apply := ⋯, cartanMatrix_apply := ⋯ }

@[instance_reducible]

instance TauCeti.MinusculeWeightTable.Symmetry.instOne {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) : One T.Symmetry

Equations

• TauCeti.MinusculeWeightTable.Symmetry.instOne T = { one := TauCeti.MinusculeWeightTable.Symmetry.identity T }

@[instance_reducible]

instance TauCeti.MinusculeWeightTable.Symmetry.instMul {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) : Mul T.Symmetry

Equations

• TauCeti.MinusculeWeightTable.Symmetry.instMul T = { mul := TauCeti.MinusculeWeightTable.Symmetry.comp T }

@[instance_reducible]

instance TauCeti.MinusculeWeightTable.Symmetry.instInv {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) : Inv T.Symmetry

Equations

• TauCeti.MinusculeWeightTable.Symmetry.instInv T = { inv := TauCeti.MinusculeWeightTable.Symmetry.inverse T }

@[simp]

theorem TauCeti.MinusculeWeightTable.Symmetry.one_nodePerm {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) : nodePerm 1 = 1

@[simp]

theorem TauCeti.MinusculeWeightTable.Symmetry.one_indexPerm {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) : indexPerm 1 = 1

@[simp]

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

@[simp]

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

@[simp]

theorem TauCeti.MinusculeWeightTable.Symmetry.inv_nodePerm {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) (S : T.Symmetry) : S⁻¹.nodePerm = S.nodePerm⁻¹

@[simp]

theorem TauCeti.MinusculeWeightTable.Symmetry.inv_indexPerm {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) (S : T.Symmetry) : S⁻¹.indexPerm = S.indexPerm⁻¹

@[instance_reducible]

instance TauCeti.MinusculeWeightTable.Symmetry.instGroup {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) : Group T.Symmetry

The symmetries of a minuscule weight table form a group under simultaneous composition of their node and weight-index permutations.

Equations

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

@[simp]

theorem TauCeti.MinusculeWeightTable.Symmetry.reflection_apply {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) (S : T.Symmetry) (i : B) (a : ι) : T.reflection (S.nodePerm i) (S.indexPerm a) = S.indexPerm (T.reflection i a)

A symmetry of a minuscule weight table intertwines its simple reflections.

def TauCeti.MinusculeWeightTable.Symmetry.rootPerm {B : Type u_1} {ι : Type u_2} {T : MinusculeWeightTable B ι} (S : T.Symmetry) : Equiv.Perm (B ⊕ B)

The permutation of the positive and negative simple-root indices induced by a table symmetry: its node permutation on both copies.

Equations

• S.rootPerm = S.nodePerm.sumCongr S.nodePerm

@[simp]

theorem TauCeti.MinusculeWeightTable.Symmetry.rootPerm_inl {B : Type u_1} {ι : Type u_2} {T : MinusculeWeightTable B ι} (S : T.Symmetry) (i : B) : S.rootPerm (Sum.inl i) = Sum.inl (S.nodePerm i)

@[simp]

theorem TauCeti.MinusculeWeightTable.Symmetry.rootPerm_inr {B : Type u_1} {ι : Type u_2} {T : MinusculeWeightTable B ι} (S : T.Symmetry) (i : B) : S.rootPerm (Sum.inr i) = Sum.inr (S.nodePerm i)

@[simp]

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

@[simp]

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

@[simp]

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

The reflected weights

@[simp]

theorem TauCeti.MinusculeWeightTable.weight_reflection_self {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) (i : B) (a : ι) : T.weight (T.reflection i a) i = -T.weight a i

A simple reflection negates the corresponding simple-coroot coordinate.

@[simp]

theorem TauCeti.MinusculeWeightTable.reflection_apply_apply {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) (i : B) (a : ι) : T.reflection i (T.reflection i a) = a

A simple reflection is an involution on the table.

theorem TauCeti.MinusculeWeightTable.weight_reflection_of_cartanMatrix_eq_zero {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) (i j : B) (a : ι) (hij : T.cartanMatrix i j = 0) : T.weight (T.reflection i a) j = T.weight a j

A reflection at a node orthogonal to j leaves the j-th coordinate alone.

theorem TauCeti.MinusculeWeightTable.reflection_comm_of_cartanMatrix_eq_zero {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) (i j : B) (a : ι) (hij : T.cartanMatrix i j = 0) : T.reflection i (T.reflection j a) = T.reflection j (T.reflection i a)

Reflections at two orthogonal nodes commute on the table.

The raising and lowering targets

The Chevalley generators

def TauCeti.MinusculeWeightTable.raisingMatrix {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) [DecidableEq ι] (i : B) : Matrix ι ι ℤ

The raising matrix of the i-th simple root on the integral weight basis.

Equations

• T.raisingMatrix i = (TauCeti.MinusculeWeightTable.raisingPEquiv✝ T i).symm.toMatrix

def TauCeti.MinusculeWeightTable.loweringMatrix {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) [DecidableEq ι] (i : B) : Matrix ι ι ℤ

The lowering matrix of the i-th simple root on the integral weight basis.

Equations

• T.loweringMatrix i = (TauCeti.MinusculeWeightTable.raisingPEquiv✝ T i).toMatrix

def TauCeti.MinusculeWeightTable.cartanGeneratorMatrix {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) [DecidableEq ι] (i : B) : Matrix ι ι ℤ

The diagonal matrix of the i-th simple coroot on the integral weight basis.

Equations

• T.cartanGeneratorMatrix i = Matrix.diagonal fun (b : ι) => T.weight b i

@[simp]

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

The entry formula for a simple raising matrix.

@[simp]

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

The entry formula for a simple lowering matrix.

@[simp]

theorem TauCeti.MinusculeWeightTable.raisingMatrix_map_col {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) [DecidableEq ι] {R : Type u_3} [CommRing R] (i : B) (a : ι) : ((T.raisingMatrix i).map Int.cast).col a = if T.weight a i = -1 then Pi.single (T.reflection i a) 1 else 0

The column of a raising matrix over any commutative ring is the reflected coordinate vector exactly at a raising edge, and otherwise is zero.

@[simp]

theorem TauCeti.MinusculeWeightTable.loweringMatrix_map_col {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) [DecidableEq ι] {R : Type u_3} [CommRing R] (i : B) (a : ι) : ((T.loweringMatrix i).map Int.cast).col a = if T.weight a i = 1 then Pi.single (T.reflection i a) 1 else 0

The column of a lowering matrix over any commutative ring is the reflected coordinate vector exactly at a lowering edge, and otherwise is zero.

@[simp]

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

The entry formula for a simple Cartan generator matrix.

theorem TauCeti.MinusculeWeightTable.Symmetry.raisingMatrix_apply {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) [DecidableEq ι] (S : T.Symmetry) (i : B) (a b : ι) : T.raisingMatrix (S.nodePerm i) (S.indexPerm a) (S.indexPerm b) = T.raisingMatrix i a b

A table symmetry carries each raising matrix to the matrix at the image node, entrywise along the weight-index permutation.

theorem TauCeti.MinusculeWeightTable.Symmetry.loweringMatrix_apply {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) [DecidableEq ι] (S : T.Symmetry) (i : B) (a b : ι) : T.loweringMatrix (S.nodePerm i) (S.indexPerm a) (S.indexPerm b) = T.loweringMatrix i a b

A table symmetry carries each lowering matrix to the matrix at the image node, entrywise along the weight-index permutation.

theorem TauCeti.MinusculeWeightTable.Symmetry.cartanGeneratorMatrix_apply {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) [DecidableEq ι] (S : T.Symmetry) (i : B) (a b : ι) : T.cartanGeneratorMatrix (S.nodePerm i) (S.indexPerm a) (S.indexPerm b) = T.cartanGeneratorMatrix i a b

A table symmetry carries each Cartan-generator matrix to the matrix at the image node, entrywise along the weight-index permutation.

@[simp]

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

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

@[simp]

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

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

@[simp]

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

Reindexing a Cartan-generator matrix by a table symmetry gives the Cartan-generator matrix at the original node.

The Serre relations

@[simp]

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

The raising matrix at each node squares to zero. The raising operator carries a weight of coordinate -1 to its reflection, whose coordinate is 1, and kills every weight of coordinate 1, so two raising steps never compose.

@[simp]

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

The lowering matrix at each node squares to zero, dually to the raising matrix.

theorem TauCeti.MinusculeWeightTable.isSl2Triple {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) [DecidableEq ι] [Fintype ι] (i : B) (hi : ∃ (a : ι), T.weight a i = -1) : IsSl2Triple (T.cartanGeneratorMatrix i) (T.raisingMatrix i) (T.loweringMatrix i)

At a node carrying a weight of coordinate -1, the three integral matrices of the table form an sl₂ triple. The hypothesis is what makes the Cartan generator nonzero; at a node whose coordinates all vanish the three matrices are zero, and IsSl2Triple asks its h to be nonzero.

theorem TauCeti.MinusculeWeightTable.raisingMatrix_eq_zero {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) [DecidableEq ι] (i : B) (hi : ¬∃ (a : ι), T.weight a i = -1) : T.raisingMatrix i = 0

A node no weight is negative at carries the zero raising matrix.

theorem TauCeti.MinusculeWeightTable.loweringMatrix_eq_zero {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) [DecidableEq ι] (i : B) (hi : ¬∃ (a : ι), T.weight a i = -1) : T.loweringMatrix i = 0

A node no weight is negative at carries the zero lowering matrix, a weight of coordinate 1 reflecting to one of coordinate -1.

theorem TauCeti.MinusculeWeightTable.isSerreSystem {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) [DecidableEq ι] [Fintype ι] : IsSerreSystem ℤ T.cartanMatrix T.cartanGeneratorMatrix T.raisingMatrix T.loweringMatrix

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

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

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

Equations

• T.serreRepresentation = TauCeti.serreLift ⋯

@[simp]

theorem TauCeti.MinusculeWeightTable.serreRepresentation_serreH {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) [DecidableEq ι] [Fintype ι] [DecidableEq B] (i : B) : T.serreRepresentation (serreH ℤ T.cartanMatrix i) = T.cartanGeneratorMatrix i

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

@[simp]

theorem TauCeti.MinusculeWeightTable.serreRepresentation_serreE {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) [DecidableEq ι] [Fintype ι] [DecidableEq B] (i : B) : T.serreRepresentation (serreE ℤ T.cartanMatrix i) = T.raisingMatrix i

The representation sends a positive generator to its raising matrix.

@[simp]

theorem TauCeti.MinusculeWeightTable.serreRepresentation_serreF {B : Type u_1} {ι : Type u_2} (T : MinusculeWeightTable B ι) [DecidableEq ι] [Fintype ι] [DecidableEq B] (i : B) : T.serreRepresentation (serreF ℤ T.cartanMatrix i) = T.loweringMatrix i

The representation sends a negative generator to its lowering matrix.