Covers of the thrice-punctured sphere are classified by their permutation triples

A connected cover of the thrice-punctured sphere U = ℂ ∖ {0, 1} of degree n can be rigidified at the basepoint b = 1/2 in three ways (TauCeti.ConnectedFiberNumberedCover, TauCeti.ConnectedPointedCover, TauCeti.ConnectedCover), and each rigidification has its own combinatorial invariant:

• a cover with numbered fibre has a literal connected permutation triple, its monodromy triple along the peripheral loops (IsCoveringMap.monodromyTriple);
• a bare cover has the isomorphism class of that triple (TauCeti.ConnectedIsoClass), obtained from any numbering;
• a pointed cover has the class of that triple with the label of the chosen point marked, modulo relabeling the triple and the label together (TauCeti.MarkedIsoClass).

Each invariant is constant on isomorphism classes of covers, so descends to a map out of the corresponding quotient. The three maps commute with the forgetful maps between the rigidifications and their combinatorial counterparts.

This file proves that each of the three maps is bijective, and packages each as an equivalence. At the numbered level injectivity is the statement that a numbered cover is determined by its numbered monodromy (TauCeti.connectedFiberNumberedCoverIso_iff_permCongrHom_comp_monodromyPerm_eq), together with the fact that periph0 and periph1 generate π₁(U, b), so that the triple determines the monodromy representation (TauCeti.ThricePuncturedSphere.permutationTriple_injective). Surjectivity is the realisation of every connected triple by a cover: since π₁(U, b) is free on periph0 and periph1, every triple is the triple of a representation of π₁(U, b) (TauCeti.ThricePuncturedSphere.permutationTriple_surjective), transitive when the triple is connected, and every such representation is the numbered monodromy of a cover (TauCeti.ConnectedFiberNumberedCover.exists_permCongrHom_comp_monodromyPerm_eq). The other two levels follow by equivariance for relabeling, since forgetting the numbering, or keeping only one labelled point, is passing to the relabeling orbits on both sides.

Main declarations

• TauCeti.ConnectedFiberNumberedCover.connectedTriple: the connected monodromy triple of a cover with numbered fibre, with connectedTriple_eq_connectedTriple_iff: two numbered covers have the same triple exactly when they are isomorphic.
• TauCeti.ConnectedFiberNumberedCoverClass.triple, TauCeti.ConnectedCoverClass.isoClass, TauCeti.ConnectedPointedCoverClass.markedClass: the three classifying maps.
• TauCeti.ConnectedFiberNumberedCoverClass.triple_bijective, TauCeti.ConnectedCoverClass.isoClass_bijective, TauCeti.ConnectedPointedCoverClass.markedClass_bijective: their bijectivity, with the injective and surjective halves stated separately.
• TauCeti.ConnectedFiberNumberedCoverClass.tripleEquiv, TauCeti.ConnectedCoverClass.isoClassEquiv, TauCeti.ConnectedPointedCoverClass.markedClassEquiv: the three classifications, as equivalences.
• TauCeti.ConnectedFiberNumberedCoverClass.isoClass_forgetNumbering, TauCeti.ConnectedFiberNumberedCoverClass.markedClass_markLabel, TauCeti.ConnectedPointedCoverClass.isoClass_forgetPoint: compatibility with the forgetful maps.

References

• E. Girondo and G. González-Diez, Introduction to Compact Riemann Surfaces and Dessins d'Enfants, London Mathematical Society Student Texts 79, Cambridge University Press, 2012, Theorem 2.61 (covers with the same branch values are isomorphic exactly when their monodromies are conjugate).
• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, §1.3 (the classification of covering spaces).

Numbered covers and literal triples

noncomputable def TauCeti.ConnectedFiberNumberedCover.connectedTriple {n : ℕ} (c : ConnectedFiberNumberedCover ThricePuncturedSphere.basePt n) : ConnectedTriple n

The monodromy triple of a connected cover of ℂ ∖ {0, 1} with numbered fibre over 1/2, as a connected triple: it is connected because the total space is path connected.

Equations

• c.connectedTriple = ⟨⋯.monodromyTriple c.ν, ⋯⟩

@[simp]

theorem TauCeti.ConnectedFiberNumberedCover.coe_connectedTriple {n : ℕ} (c : ConnectedFiberNumberedCover ThricePuncturedSphere.basePt n) : ↑c.connectedTriple = ⋯.monodromyTriple c.ν

@[simp]

theorem TauCeti.ConnectedFiberNumberedCover.connectedTriple_smul {n : ℕ} (c : ConnectedFiberNumberedCover ThricePuncturedSphere.basePt n) (τ : Equiv.Perm (Fin n)) : (τ • c).connectedTriple = τ • c.connectedTriple

Relabeling the fibre relabels the triple.

theorem TauCeti.ConnectedFiberNumberedCover.connectedTriple_eq_connectedTriple_iff {n : ℕ} {c c' : ConnectedFiberNumberedCover ThricePuncturedSphere.basePt n} : c.connectedTriple = c'.connectedTriple ↔ ConnectedFiberNumberedCoverIso c c'

Two covers of ℂ ∖ {0, 1} with numbered fibres have the same triple exactly when they are isomorphic, by an isomorphism preserving every label.

noncomputable def TauCeti.ConnectedFiberNumberedCoverClass.triple {n : ℕ} : ConnectedFiberNumberedCoverClass ThricePuncturedSphere.basePt n → ConnectedTriple n

The connected triple of an isomorphism class of numbered covers of ℂ ∖ {0, 1}.

Equations

• TauCeti.ConnectedFiberNumberedCoverClass.triple = TauCeti.ConnectedFiberNumberedCoverClass.lift TauCeti.ConnectedFiberNumberedCover.connectedTriple ⋯

@[simp]

theorem TauCeti.ConnectedFiberNumberedCoverClass.triple_mk {n : ℕ} (c : ConnectedFiberNumberedCover ThricePuncturedSphere.basePt n) : (mk c).triple = c.connectedTriple

@[simp]

theorem TauCeti.ConnectedFiberNumberedCoverClass.triple_smul {n : ℕ} (τ : Equiv.Perm (Fin n)) (C : ConnectedFiberNumberedCoverClass ThricePuncturedSphere.basePt n) : (τ • C).triple = τ • C.triple

Relabeling a numbered class relabels its triple.

theorem TauCeti.ConnectedFiberNumberedCoverClass.triple_injective {n : ℕ} : Function.Injective triple

A numbered cover of ℂ ∖ {0, 1} is determined up to isomorphism by its triple.

theorem TauCeti.ConnectedFiberNumberedCoverClass.triple_surjective {n : ℕ} : Function.Surjective triple

Every connected triple is the triple of a numbered cover of ℂ ∖ {0, 1}.

theorem TauCeti.ConnectedFiberNumberedCoverClass.triple_bijective {n : ℕ} : Function.Bijective triple

The triple of a class of numbered covers of ℂ ∖ {0, 1} is a bijection onto connected triples.

noncomputable def TauCeti.ConnectedFiberNumberedCoverClass.tripleEquiv {n : ℕ} : ConnectedFiberNumberedCoverClass ThricePuncturedSphere.basePt n ≃ ConnectedTriple n

Numbered covers of ℂ ∖ {0, 1} up to label-preserving isomorphism are classified by their connected triples.

Equations

• TauCeti.ConnectedFiberNumberedCoverClass.tripleEquiv = Equiv.ofBijective TauCeti.ConnectedFiberNumberedCoverClass.triple ⋯

@[simp]

theorem TauCeti.ConnectedFiberNumberedCoverClass.tripleEquiv_apply {n : ℕ} (C : ConnectedFiberNumberedCoverClass ThricePuncturedSphere.basePt n) : tripleEquiv C = C.triple

@[simp]

theorem TauCeti.ConnectedFiberNumberedCoverClass.triple_tripleEquiv_symm {n : ℕ} (t : ConnectedTriple n) : (tripleEquiv.symm t).triple = t

The numbered cover class realising a connected triple has that triple.

Bare covers and isomorphism classes of triples

noncomputable def TauCeti.ConnectedCoverClass.isoClass {n : ℕ} (C : ConnectedCoverClass ThricePuncturedSphere.basePt n) : ConnectedIsoClass n

The isomorphism class of the triple of a connected cover of ℂ ∖ {0, 1}: the relabeling orbit of the triple of any numbering of the cover (isoClass_forgetNumbering).

Equations

• C.isoClass = Quotient.map' TauCeti.ConnectedFiberNumberedCoverClass.triple ⋯ (TauCeti.ConnectedFiberNumberedCoverClass.orbitRelQuotientEquiv.symm C)

@[simp]

theorem TauCeti.ConnectedFiberNumberedCoverClass.isoClass_forgetNumbering {n : ℕ} (C : ConnectedFiberNumberedCoverClass ThricePuncturedSphere.basePt n) : C.forgetNumbering.isoClass = ConnectedIsoClass.mk C.triple

Forgetting the numbering of a cover is passing to the isomorphism class of its triple.

theorem TauCeti.ConnectedCoverClass.isoClass_injective {n : ℕ} : Function.Injective isoClass

A connected cover of ℂ ∖ {0, 1} is determined up to isomorphism by the isomorphism class of its triple.

theorem TauCeti.ConnectedCoverClass.isoClass_surjective {n : ℕ} : Function.Surjective isoClass

Every isomorphism class of connected triples is the class of the triple of a connected cover of ℂ ∖ {0, 1}.

theorem TauCeti.ConnectedCoverClass.isoClass_bijective {n : ℕ} : Function.Bijective isoClass

The isomorphism class of the triple of a class of connected covers of ℂ ∖ {0, 1} is a bijection onto isomorphism classes of connected triples.

noncomputable def TauCeti.ConnectedCoverClass.isoClassEquiv {n : ℕ} : ConnectedCoverClass ThricePuncturedSphere.basePt n ≃ ConnectedIsoClass n

Connected covers of ℂ ∖ {0, 1} of degree n up to isomorphism are classified by the isomorphism classes of connected triples of degree n.

Equations

• TauCeti.ConnectedCoverClass.isoClassEquiv = Equiv.ofBijective TauCeti.ConnectedCoverClass.isoClass ⋯

@[simp]

theorem TauCeti.ConnectedCoverClass.isoClassEquiv_apply {n : ℕ} (C : ConnectedCoverClass ThricePuncturedSphere.basePt n) : isoClassEquiv C = C.isoClass

@[simp]

theorem TauCeti.ConnectedCoverClass.isoClass_isoClassEquiv_symm {n : ℕ} (c : ConnectedIsoClass n) : (isoClassEquiv.symm c).isoClass = c

The cover class realising an isomorphism class of connected triples has that class.

Pointed covers and marked triples

noncomputable def TauCeti.ConnectedPointedCoverClass.markedClass {n : ℕ} (C : ConnectedPointedCoverClass ThricePuncturedSphere.basePt n) : MarkedIsoClass n

The marked class of a pointed connected cover of ℂ ∖ {0, 1}: the triple of any numbering of the cover, with the label of the chosen point marked, modulo relabeling triple and label together (markedClass_markLabel).

Equations

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

@[simp]

theorem TauCeti.ConnectedFiberNumberedCoverClass.markedClass_markLabel {n : ℕ} (C : ConnectedFiberNumberedCoverClass ThricePuncturedSphere.basePt n) (i : Fin n) : (C.markLabel i).markedClass = MarkedIsoClass.mk C.triple i

Keeping only the point labelled i of a numbered cover is marking the label i of its triple.

@[simp]

theorem TauCeti.ConnectedPointedCoverClass.isoClass_forgetPoint {n : ℕ} (C : ConnectedPointedCoverClass ThricePuncturedSphere.basePt n) : C.forgetPoint.isoClass = C.markedClass.forget

Forgetting the chosen point of a cover is forgetting the marked label of its marked class.

theorem TauCeti.ConnectedPointedCoverClass.markedClass_injective {n : ℕ} : Function.Injective markedClass

A pointed connected cover of ℂ ∖ {0, 1} is determined up to pointed isomorphism by its marked class.

theorem TauCeti.ConnectedPointedCoverClass.markedClass_surjective {n : ℕ} : Function.Surjective markedClass

Every marked class of connected triples is the marked class of a pointed connected cover of ℂ ∖ {0, 1}.

theorem TauCeti.ConnectedPointedCoverClass.markedClass_bijective {n : ℕ} : Function.Bijective markedClass

The marked class of a class of pointed connected covers of ℂ ∖ {0, 1} is a bijection onto marked classes of connected triples.

noncomputable def TauCeti.ConnectedPointedCoverClass.markedClassEquiv {n : ℕ} : ConnectedPointedCoverClass ThricePuncturedSphere.basePt n ≃ MarkedIsoClass n

Pointed connected covers of ℂ ∖ {0, 1} of degree n up to pointed isomorphism are classified by connected triples of degree n with a marked label, modulo relabeling both.

Equations

• TauCeti.ConnectedPointedCoverClass.markedClassEquiv = Equiv.ofBijective TauCeti.ConnectedPointedCoverClass.markedClass ⋯

@[simp]

theorem TauCeti.ConnectedPointedCoverClass.markedClassEquiv_apply {n : ℕ} (C : ConnectedPointedCoverClass ThricePuncturedSphere.basePt n) : markedClassEquiv C = C.markedClass

@[simp]

theorem TauCeti.ConnectedPointedCoverClass.markedClass_markedClassEquiv_symm {n : ℕ} (c : MarkedIsoClass n) : (markedClassEquiv.symm c).markedClass = c

The pointed cover class realising a marked class of connected triples has that marked class.