Marked triple classes with a fixed label

The diagonal quotient defining MarkedIsoClass n lets a relabeling move both the triple and its marked sheet. Equivalently, fix any label i : Fin n and quotient connected triples by only the permutations fixing i. The equivalence sends the stabilizer orbit of t to the marked class of (t, i) and commutes with forgetting the mark.

This gives a fixed-label description of the combinatorial invariant of pointed covers, without identifying pointed classes with literal triples or with unpointed classes.

References

• E. Girondo, G. González-Diez, Introduction to Compact Riemann Surfaces and Dessins d'Enfants, London Mathematical Society Student Texts 79, Cambridge University Press 2012, §2.7.

def TauCeti.ConnectedIsoClass.ofStabilizerOrbit {n : ℕ} (i : Fin n) : MulAction.orbitRel.Quotient (↥(MulAction.stabilizer (Equiv.Perm (Fin n)) i)) (ConnectedTriple n) → ConnectedIsoClass n

Forget a fixed marked label by enlarging its stabilizer to the full relabeling group.

Equations

• TauCeti.ConnectedIsoClass.ofStabilizerOrbit i = Quotient.map' id ⋯

@[simp]

theorem TauCeti.ConnectedIsoClass.ofStabilizerOrbit_mk {n : ℕ} (i : Fin n) (t : ConnectedTriple n) : ofStabilizerOrbit i (Quotient.mk'' t) = mk t

@[simp]

theorem TauCeti.MarkedIsoClass.forget_stabilizerEquiv {n : ℕ} (i : Fin n) (q : MulAction.orbitRel.Quotient (↥(MulAction.stabilizer (Equiv.Perm (Fin n)) i)) (ConnectedTriple n)) : ((stabilizerEquiv i) q).forget = ConnectedIsoClass.ofStabilizerOrbit i q

Forgetting the mark after fixing a label is just passing to the full relabeling orbit.