Star models of Dynkin trees

The finite trees of Proposition 4.1 are stars: a centre with arms. The star model StarV L has the centre none and, on arm i, the vertices some ⟨i, k⟩ for k ≤ L i, the vertex k being at distance k + 1 from the centre. Paths are stars with at most two arms; D_n, E_6, E_7, E_8 have three arms of lengths (1, 1, n - 3), (1, 2, 2), (1, 2, 3), (1, 2, 4).

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.StarV {t : ℕ} (L : Fin t → ℕ) : Type

The vertices of the star with arms of lengths L i + 1.

def MultiplicativeBasisDeformations.starAdj {t : ℕ} {L : Fin t → ℕ} : StarV L → StarV L → Prop

Adjacency in the star model.

def MultiplicativeBasisDeformations.starGraph {t : ℕ} (L : Fin t → ℕ) : SimpleGraph (StarV L)

The star as a simple graph.

@[instance_reducible]

instance MultiplicativeBasisDeformations.instDecidableRelStarVAdjStarGraph {t : ℕ} (L : Fin t → ℕ) : DecidableRel (starGraph L).Adj

def MultiplicativeBasisDeformations.starDepth {t : ℕ} {L : Fin t → ℕ} : StarV L → ℕ

The distance of a star vertex from the centre.

def MultiplicativeBasisDeformations.starOrient {t : ℕ} {L : Fin t → ℕ} (x y : StarV L) : Prop

Orientation away from the centre.

theorem MultiplicativeBasisDeformations.starAdj_depth {t : ℕ} {L : Fin t → ℕ} {x y : StarV L} (h : starAdj x y) : starDepth y = starDepth x + 1 ∨ starDepth x = starDepth y + 1

@[instance_reducible]

instance MultiplicativeBasisDeformations.instDecidableRelStarVStarOrient {t : ℕ} {L : Fin t → ℕ} : DecidableRel starOrient