Symmetry of the vertex star

All legs of a vertex star meet the same vertex, so any boundary permutation is absorbed: the star class is symmetric. This is the S_d-invariance that makes the vertex coordinates well defined on multiset data.

noncomputable def RS.vertexStarRelabelEquiv (d : ℕ) (σ : Fin d ≃ Fin d) : ((vertexStar d).relabel σ).Equiv (vertexStar d)

The vertex star absorbs any boundary relabelling.

Equations

• RS.vertexStarRelabelEquiv d σ = { flagEquiv := σ.sumCongr σ, vertexEquiv := Equiv.refl Unit, attach_comm := ⋯, pairing_comm := ⋯, circles_eq := ⋯ }

theorem RS.vertexStarClass_perm {R : ℕ} (f : EdgeRankParameter R) (d : ℕ) (σ : Fin d ≃ Fin d) : ((HomSpace.comp f 0 d d) (vertexStarClass f d)) (bundleMapClass f σ) = vertexStarClass f d

S_d-invariance of the vertex star class: composing with any permutation bundle map is absorbed.