Automorphisms of a star fixing its centre permute the arms

Used for the twists θ = ρ^l of Lemma A.2 (periodic-mesh-calculations.tex): an automorphism of a star model fixing the centre preserves depths and maps arm i onto an arm θ i of the same length, vertex by vertex.

theorem MultiplicativeBasisDeformations.arm_image {t : ℕ} {L : Fin t → ℕ} (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), starAdj a b ↔ starAdj (ρ a) (ρ b)) (h0 : ρ none = none) (i : Fin t) (j : ℕ) (hj : j < L i + 1) : ∃ (i' : Fin t) (hj' : j < L i' + 1), ρ (some ⟨i, ⟨j, hj⟩⟩) = some ⟨i', ⟨j, hj'⟩⟩ ∧ ∀ j₀ ≤ j, ∀ (hj₀' : j₀ < L i + 1), ∃ (hj₀'' : j₀ < L i' + 1), ρ (some ⟨i, ⟨j₀, hj₀'⟩⟩) = some ⟨i', ⟨j₀, hj₀''⟩⟩

The image of the vertex j of arm i lies at depth j + 1, on some arm.

theorem MultiplicativeBasisDeformations.arm_perm {t : ℕ} {L : Fin t → ℕ} (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), starAdj a b ↔ starAdj (ρ a) (ρ b)) (h0 : ρ none = none) : ∃ (θ : Equiv.Perm (Fin t)), (∀ (i : Fin t), L (θ i) = L i) ∧ ∀ (i : Fin t) (j : ℕ) (hj : j < L i + 1), ∃ (hj' : j < L (θ i) + 1), ρ (some ⟨i, ⟨j, hj⟩⟩) = some ⟨θ i, ⟨j, hj'⟩⟩

An automorphism fixing the centre permutes the arms, preserving their lengths.