The exceptional affine Dynkin diagrams as stars

The exceptional simply-laced affine Dynkin diagrams are three-armed stars. This file identifies the arm-coordinate numbering of TauCeti.AffineDynkinType.graph with the canonical star indices used by TauCeti.starCartanMatrix:

  affine E₆ = T₃,₃,₃,    affine E₇ = T₂,₄,₄,    affine E₈ = T₂,₃,₆.

The parameters in TauCeti.StarIndex count vertices beyond the centre, so the corresponding arm vectors are ![2, 2, 2], ![1, 3, 3], and ![1, 2, 5]. The explicit equivalences below send the star centre to affine node 0 and number every arm outwards. They identify both the generalized Cartan matrices and their diagram graphs, allowing results about stars to be applied directly to the affine exceptional types.

Main definitions

• TauCeti.AffineDynkinType.starIndexEquivE6, starIndexEquivE7, and starIndexEquivE8 are the explicit relabellings from the three canonical star index types to the affine node types.
• TauCeti.AffineDynkinType.starGraphIsoE6, starGraphIsoE7, and starGraphIsoE8 identify the corresponding star diagrams with the affine exceptional diagrams.

References

The star descriptions follow V. Kac, Infinite dimensional Lie algebras, 3rd ed., Chapter 4 and Table Aff 1.

noncomputable def TauCeti.AffineDynkinType.starIndexEquivE6 : StarIndex ![2, 2, 2] ≃ Fin E6.nodes

The arm-coordinate relabelling from the star T₃,₃,₃ to affine E₆. It sends the centre to node 0 and sends the vertices on arms i = 0, 1, 2, in order away from the centre, to 1, 2, to 3, 4, and to 5, 6, respectively.

Equations

• TauCeti.AffineDynkinType.starIndexEquivE6 = Equiv.ofBijective TauCeti.AffineDynkinType.e6StarEmbedding✝ TauCeti.AffineDynkinType.starIndexEquivE6._proof_1✝

@[simp]

theorem TauCeti.AffineDynkinType.starIndexEquivE6_none : starIndexEquivE6 none = 0

The affine E₆ star relabelling sends the centre to node 0.

@[simp]

theorem TauCeti.AffineDynkinType.starIndexEquivE6_some (i : Fin 3) (s : Fin (![2, 2, 2] i)) : starIndexEquivE6 (some ⟨i, s⟩) = ⟨2 * ↑i + ↑s + 1, ⋯⟩

The affine E₆ star relabelling sends an arm vertex to its prescribed affine node.

@[simp]

theorem TauCeti.AffineDynkinType.starIndexEquivE6_symm_apply (v : Fin 7) : starIndexEquivE6.symm v = ![none, some ⟨0, ⟨0, starIndexEquivE6_symm_apply._proof_1⟩⟩, some ⟨0, ⟨1, starIndexEquivE6_symm_apply._proof_2⟩⟩, some ⟨1, ⟨0, starIndexEquivE6_symm_apply._proof_3⟩⟩, some ⟨1, ⟨1, starIndexEquivE6_symm_apply._proof_4⟩⟩, some ⟨2, ⟨0, starIndexEquivE6_symm_apply._proof_5⟩⟩, some ⟨2, ⟨1, starIndexEquivE6_symm_apply._proof_6⟩⟩] v

The inverse affine E₆ relabelling, listed in affine-node order.

noncomputable def TauCeti.AffineDynkinType.starIndexEquivE7 : StarIndex ![1, 3, 3] ≃ Fin E7.nodes

The arm-coordinate relabelling from the star T₂,₄,₄ to affine E₇. It sends the centre to node 0 and sends the vertices on arms i = 0, 1, 2, in order away from the centre, to 1, to 2, 3, 4, and to 5, 6, 7, respectively.

Equations

• TauCeti.AffineDynkinType.starIndexEquivE7 = Equiv.ofBijective TauCeti.AffineDynkinType.e7StarEmbedding✝ TauCeti.AffineDynkinType.starIndexEquivE7._proof_1✝

@[simp]

theorem TauCeti.AffineDynkinType.starIndexEquivE7_none : starIndexEquivE7 none = 0

The affine E₇ star relabelling sends the centre to node 0.

@[simp]

theorem TauCeti.AffineDynkinType.starIndexEquivE7_some (i : Fin 3) (s : Fin (![1, 3, 3] i)) : starIndexEquivE7 (some ⟨i, s⟩) = ⟨if ↑i = 0 then 1 else if ↑i = 1 then 2 + ↑s else 5 + ↑s, ⋯⟩

The affine E₇ star relabelling sends an arm vertex to its prescribed affine node.

@[simp]

theorem TauCeti.AffineDynkinType.starIndexEquivE7_symm_apply (v : Fin 8) : starIndexEquivE7.symm v = ![none, some ⟨0, ⟨0, starIndexEquivE7_symm_apply._proof_1⟩⟩, some ⟨1, ⟨0, starIndexEquivE7_symm_apply._proof_2⟩⟩, some ⟨1, ⟨1, starIndexEquivE7_symm_apply._proof_3⟩⟩, some ⟨1, ⟨2, starIndexEquivE7_symm_apply._proof_4⟩⟩, some ⟨2, ⟨0, starIndexEquivE7_symm_apply._proof_5⟩⟩, some ⟨2, ⟨1, starIndexEquivE7_symm_apply._proof_6⟩⟩, some ⟨2, ⟨2, starIndexEquivE7_symm_apply._proof_7⟩⟩] v

The inverse affine E₇ relabelling, listed in affine-node order.

noncomputable def TauCeti.AffineDynkinType.starIndexEquivE8 : StarIndex ![1, 2, 5] ≃ Fin E8.nodes

The arm-coordinate relabelling from the star T₂,₃,₆ to affine E₈. It sends the centre to node 0 and sends the vertices on arms i = 0, 1, 2, in order away from the centre, to 1, to 2, 3, and to 4, 5, 6, 7, 8, respectively.

Equations

• TauCeti.AffineDynkinType.starIndexEquivE8 = Equiv.ofBijective TauCeti.AffineDynkinType.e8StarEmbedding✝ TauCeti.AffineDynkinType.starIndexEquivE8._proof_1✝

@[simp]

theorem TauCeti.AffineDynkinType.starIndexEquivE8_none : starIndexEquivE8 none = 0

The affine E₈ star relabelling sends the centre to node 0.

@[simp]

theorem TauCeti.AffineDynkinType.starIndexEquivE8_some (i : Fin 3) (s : Fin (![1, 2, 5] i)) : starIndexEquivE8 (some ⟨i, s⟩) = ⟨if ↑i = 0 then 1 else if ↑i = 1 then 2 + ↑s else 4 + ↑s, ⋯⟩

The affine E₈ star relabelling sends an arm vertex to its prescribed affine node.

@[simp]

theorem TauCeti.AffineDynkinType.starIndexEquivE8_symm_apply (v : Fin 9) : starIndexEquivE8.symm v = ![none, some ⟨0, ⟨0, starIndexEquivE8_symm_apply._proof_1⟩⟩, some ⟨1, ⟨0, starIndexEquivE8_symm_apply._proof_2⟩⟩, some ⟨1, ⟨1, starIndexEquivE8_symm_apply._proof_3⟩⟩, some ⟨2, ⟨0, starIndexEquivE8_symm_apply._proof_4⟩⟩, some ⟨2, ⟨1, starIndexEquivE8_symm_apply._proof_5⟩⟩, some ⟨2, ⟨2, starIndexEquivE8_symm_apply._proof_6⟩⟩, some ⟨2, ⟨3, starIndexEquivE8_symm_apply._proof_7⟩⟩, some ⟨2, ⟨4, starIndexEquivE8_symm_apply._proof_8⟩⟩] v

The inverse affine E₈ relabelling, listed in affine-node order.

Cartan matrix descriptions

theorem TauCeti.AffineDynkinType.starCartanMatrix_two_two_two_eq_submatrix_E6 : starCartanMatrix ![2, 2, 2] = E6.cartanMatrix.submatrix ⇑starIndexEquivE6 ⇑starIndexEquivE6

Affine E₆ is the star T₃,₃,₃: after the explicit arm-coordinate relabelling, its generalized Cartan matrix is the canonical star matrix with three arms of length two beyond the centre.

theorem TauCeti.AffineDynkinType.starCartanMatrix_one_three_three_eq_submatrix_E7 : starCartanMatrix ![1, 3, 3] = E7.cartanMatrix.submatrix ⇑starIndexEquivE7 ⇑starIndexEquivE7

Affine E₇ is the star T₂,₄,₄: after the explicit arm-coordinate relabelling, its generalized Cartan matrix is the canonical star matrix with arms of lengths one, three and three beyond the centre.

theorem TauCeti.AffineDynkinType.starCartanMatrix_one_two_five_eq_submatrix_E8 : starCartanMatrix ![1, 2, 5] = E8.cartanMatrix.submatrix ⇑starIndexEquivE8 ⇑starIndexEquivE8

Affine E₈ is the star T₂,₃,₆: after the explicit arm-coordinate relabelling, its generalized Cartan matrix is the canonical star matrix with arms of lengths one, two and five beyond the centre.

Graph descriptions

noncomputable def TauCeti.AffineDynkinType.starGraphIsoE6 : diagramGraph (starCartanMatrix ![2, 2, 2]) ≃g E6.graph

The graph isomorphism T₃,₃,₃ ≅ affine E₆ induced by the explicit arm-coordinate relabelling.

Equations

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

@[simp]

theorem TauCeti.AffineDynkinType.starGraphIsoE6_apply (v : StarIndex ![2, 2, 2]) : starGraphIsoE6 v = starIndexEquivE6 v

The star graph isomorphism for affine E₆ has the prescribed arm-coordinate map.

@[simp]

theorem TauCeti.AffineDynkinType.starGraphIsoE6_symm_apply (v : Fin 7) : starGraphIsoE6.symm v = ![none, some ⟨0, ⟨0, starIndexEquivE6_symm_apply._proof_1⟩⟩, some ⟨0, ⟨1, starIndexEquivE6_symm_apply._proof_2⟩⟩, some ⟨1, ⟨0, starIndexEquivE6_symm_apply._proof_3⟩⟩, some ⟨1, ⟨1, starIndexEquivE6_symm_apply._proof_4⟩⟩, some ⟨2, ⟨0, starIndexEquivE6_symm_apply._proof_5⟩⟩, some ⟨2, ⟨1, starIndexEquivE6_symm_apply._proof_6⟩⟩] v

The inverse affine E₆ graph isomorphism, listed in affine-node order.

noncomputable def TauCeti.AffineDynkinType.starGraphIsoE7 : diagramGraph (starCartanMatrix ![1, 3, 3]) ≃g E7.graph

The graph isomorphism T₂,₄,₄ ≅ affine E₇ induced by the explicit arm-coordinate relabelling.

Equations

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

@[simp]

theorem TauCeti.AffineDynkinType.starGraphIsoE7_apply (v : StarIndex ![1, 3, 3]) : starGraphIsoE7 v = starIndexEquivE7 v

The star graph isomorphism for affine E₇ has the prescribed arm-coordinate map.

@[simp]

theorem TauCeti.AffineDynkinType.starGraphIsoE7_symm_apply (v : Fin 8) : starGraphIsoE7.symm v = ![none, some ⟨0, ⟨0, starIndexEquivE7_symm_apply._proof_1⟩⟩, some ⟨1, ⟨0, starIndexEquivE7_symm_apply._proof_2⟩⟩, some ⟨1, ⟨1, starIndexEquivE7_symm_apply._proof_3⟩⟩, some ⟨1, ⟨2, starIndexEquivE7_symm_apply._proof_4⟩⟩, some ⟨2, ⟨0, starIndexEquivE7_symm_apply._proof_5⟩⟩, some ⟨2, ⟨1, starIndexEquivE7_symm_apply._proof_6⟩⟩, some ⟨2, ⟨2, starIndexEquivE7_symm_apply._proof_7⟩⟩] v

The inverse affine E₇ graph isomorphism, listed in affine-node order.

noncomputable def TauCeti.AffineDynkinType.starGraphIsoE8 : diagramGraph (starCartanMatrix ![1, 2, 5]) ≃g E8.graph

The graph isomorphism T₂,₃,₆ ≅ affine E₈ induced by the explicit arm-coordinate relabelling.

Equations

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

@[simp]

theorem TauCeti.AffineDynkinType.starGraphIsoE8_apply (v : StarIndex ![1, 2, 5]) : starGraphIsoE8 v = starIndexEquivE8 v

The star graph isomorphism for affine E₈ has the prescribed arm-coordinate map.

@[simp]

theorem TauCeti.AffineDynkinType.starGraphIsoE8_symm_apply (v : Fin 9) : starGraphIsoE8.symm v = ![none, some ⟨0, ⟨0, starIndexEquivE8_symm_apply._proof_1⟩⟩, some ⟨1, ⟨0, starIndexEquivE8_symm_apply._proof_2⟩⟩, some ⟨1, ⟨1, starIndexEquivE8_symm_apply._proof_3⟩⟩, some ⟨2, ⟨0, starIndexEquivE8_symm_apply._proof_4⟩⟩, some ⟨2, ⟨1, starIndexEquivE8_symm_apply._proof_5⟩⟩, some ⟨2, ⟨2, starIndexEquivE8_symm_apply._proof_6⟩⟩, some ⟨2, ⟨3, starIndexEquivE8_symm_apply._proof_7⟩⟩, some ⟨2, ⟨4, starIndexEquivE8_symm_apply._proof_8⟩⟩] v

The inverse affine E₈ graph isomorphism, listed in affine-node order.