The monodromy triple of a cover of the thrice-punctured sphere

A covering map p : E → U of the thrice-punctured sphere U = ℂ ∖ {0, 1} whose fibre over the basepoint b = 1/2 is numbered, ν : p ⁻¹' {b} ≃ Fin n, has a permutation triple: the monodromy permutations of the numbered fibre along the three peripheral elements periph0, periph1, periphInf of π₁(U, b),

σ_i = ν.permCongr (monodromy of periph_i).

Monodromy is a homomorphism π₁(U, b) →* Equiv.Perm (p ⁻¹' {b}) with no ᵐᵒᵖ (IsCoveringMap.monodromyPerm), so the relation periphInf * periph1 * periph0 = 1 becomes the relation σinf * σ1 * σ0 = 1 of a permutation triple on the nose.

The construction factors through representations. Any homomorphism ρ : π₁(U, b) →* Equiv.Perm (Fin n) has the triple (ρ periph0, ρ periph1, ρ periphInf), and since periph0 and periph1 generate π₁(U, b), that triple determines ρ, its monodromy group is the image of ρ, and conjugating ρ relabels it. Since π₁(U, b) is free on periph0 and periph1, every permutation triple arises from some ρ.

For a cover, the triple records the cover faithfully in the following senses.

• It is connected exactly when the total space is path connected: path lifting identifies the monodromy orbits on the fibre with the path components of E, and a nonempty fibre is the same as a nonempty total space.
• It is unchanged by a map of covers over U that respects the numberings.
• Renumbering the fibre by a permutation τ relabels the triple by τ. Hence the isomorphism class of the triple does not depend on the numbering, and is an invariant of the cover up to homeomorphism over U.

Main declarations

• TauCeti.ThricePuncturedSphere.permutationTriple: the triple of a representation of π₁(U, b) on Fin n, with monodromyGroup_permutationTriple, isConnected_permutationTriple_iff, permutationTriple_conj_comp, permutationTriple_injective and permutationTriple_surjective.
• IsCoveringMap.monodromyTriple: the monodromy triple of a cover of U with numbered fibre, with its components monodromyTriple_σ0, monodromyTriple_σ1, monodromyTriple_σinf.
• IsCoveringMap.isConnected_monodromyTriple_iff: the triple is connected exactly when the total space is path connected.
• IsCoveringMap.monodromyTriple_eq_of_comp_eq: a map of covers respecting the numberings preserves the triple.
• IsCoveringMap.monodromyTriple_trans: renumbering the fibre relabels the triple.
• IsCoveringMap.isoClass_monodromyTriple_eq and IsCoveringMap.isoClass_monodromyTriple_eq_of_homeomorph: the isomorphism class of the triple depends only on the cover up to homeomorphism over U.

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, §2.7 (the monodromy of a cover, well defined up to the numbering of the fibre). That text multiplies paths in the opposite order and so inverts the monodromy permutations; with Mathlib's order no inversion is needed, and the resulting triples are the componentwise inverses of the ones there.
• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, §1.3 (the action of the fundamental group on a fibre).

The triple of a representation of the fundamental group

noncomputable def TauCeti.ThricePuncturedSphere.permutationTriple {n : ℕ} (ρ : FundamentalGroup ThricePuncturedSphere basePt →* Equiv.Perm (Fin n)) : PermutationTriple n

The permutation triple of a representation ρ of π₁(ℂ ∖ {0, 1}, 1/2) on Fin n: its values at the peripheral elements periph0 and periph1, the third component being ρ periphInf (permutationTriple_σinf).

Equations

• TauCeti.ThricePuncturedSphere.permutationTriple ρ = TauCeti.PermutationTriple.ofTwo (ρ TauCeti.ThricePuncturedSphere.periph0) (ρ TauCeti.ThricePuncturedSphere.periph1)

@[simp]

theorem TauCeti.ThricePuncturedSphere.permutationTriple_σ0 {n : ℕ} (ρ : FundamentalGroup ThricePuncturedSphere basePt →* Equiv.Perm (Fin n)) : (permutationTriple ρ).σ0 = ρ periph0

@[simp]

theorem TauCeti.ThricePuncturedSphere.permutationTriple_σ1 {n : ℕ} (ρ : FundamentalGroup ThricePuncturedSphere basePt →* Equiv.Perm (Fin n)) : (permutationTriple ρ).σ1 = ρ periph1

@[simp]

theorem TauCeti.ThricePuncturedSphere.permutationTriple_σinf {n : ℕ} (ρ : FundamentalGroup ThricePuncturedSphere basePt →* Equiv.Perm (Fin n)) : (permutationTriple ρ).σinf = ρ periphInf

The third component of the triple of ρ is the value of ρ at the peripheral element at ∞.

@[simp]

theorem TauCeti.ThricePuncturedSphere.monodromyGroup_permutationTriple {n : ℕ} (ρ : FundamentalGroup ThricePuncturedSphere basePt →* Equiv.Perm (Fin n)) : (permutationTriple ρ).monodromyGroup = ρ.range

The monodromy group of the triple of ρ is the image of ρ, because periph0 and periph1 generate the fundamental group.

theorem TauCeti.ThricePuncturedSphere.isConnected_permutationTriple_iff {n : ℕ} (ρ : FundamentalGroup ThricePuncturedSphere basePt →* Equiv.Perm (Fin n)) : (permutationTriple ρ).IsConnected ↔ n ≠ 0 ∧ MulAction.IsPretransitive (↥ρ.range) (Fin n)

The triple of ρ is connected exactly when n ≠ 0 and the image of ρ acts transitively on Fin n.

theorem TauCeti.ThricePuncturedSphere.permutationTriple_conj_comp {n : ℕ} (ρ : FundamentalGroup ThricePuncturedSphere basePt →* Equiv.Perm (Fin n)) (τ : Equiv.Perm (Fin n)) : permutationTriple ((MulEquiv.toMonoidHom (MulAut.conj τ)).comp ρ) = τ • permutationTriple ρ

Conjugating a representation by τ relabels its triple by τ.

theorem TauCeti.ThricePuncturedSphere.permutationTriple_injective {n : ℕ} : Function.Injective permutationTriple

A representation of π₁(ℂ ∖ {0, 1}, 1/2) is determined by its triple.

theorem TauCeti.ThricePuncturedSphere.permutationTriple_surjective {n : ℕ} : Function.Surjective permutationTriple

Every permutation triple is the triple of a representation of π₁(ℂ ∖ {0, 1}, 1/2), because the fundamental group is free on periph0 and periph1.

The monodromy triple of a cover

noncomputable def IsCoveringMap.monodromyTriple {n : ℕ} {E : Type u} [TopologicalSpace E] {p : E → TauCeti.ThricePuncturedSphere} (hp : IsCoveringMap p) (ν : ↑(p ⁻¹' {TauCeti.ThricePuncturedSphere.basePt}) ≃ Fin n) : TauCeti.PermutationTriple n

The monodromy triple of a covering map p : E → ℂ ∖ {0, 1} whose fibre over the basepoint 1/2 is numbered by ν: the monodromy permutations of the numbered fibre along the peripheral elements periph0, periph1 and periphInf.

Equations

• hp.monodromyTriple ν = TauCeti.ThricePuncturedSphere.permutationTriple ν.permutationRepresentation

theorem IsCoveringMap.monodromyTriple_def {n : ℕ} {E : Type u} [TopologicalSpace E] {p : E → TauCeti.ThricePuncturedSphere} (hp : IsCoveringMap p) (ν : ↑(p ⁻¹' {TauCeti.ThricePuncturedSphere.basePt}) ≃ Fin n) : hp.monodromyTriple ν = TauCeti.ThricePuncturedSphere.permutationTriple (ν.permCongrHom.toMonoidHom.comp (hp.monodromyPerm TauCeti.ThricePuncturedSphere.basePt))

The monodromy triple is the triple of the monodromy representation IsCoveringMap.monodromyPerm, transported to Fin n by the numbering ν.

@[simp]

theorem IsCoveringMap.monodromyTriple_σ0 {n : ℕ} {E : Type u} [TopologicalSpace E] {p : E → TauCeti.ThricePuncturedSphere} (hp : IsCoveringMap p) (ν : ↑(p ⁻¹' {TauCeti.ThricePuncturedSphere.basePt}) ≃ Fin n) : (hp.monodromyTriple ν).σ0 = ν.permCongr ((hp.monodromyPerm TauCeti.ThricePuncturedSphere.basePt) TauCeti.ThricePuncturedSphere.periph0)

The first component of the monodromy triple is the monodromy along the peripheral element at 0, read through the numbering.

@[simp]

theorem IsCoveringMap.monodromyTriple_σ1 {n : ℕ} {E : Type u} [TopologicalSpace E] {p : E → TauCeti.ThricePuncturedSphere} (hp : IsCoveringMap p) (ν : ↑(p ⁻¹' {TauCeti.ThricePuncturedSphere.basePt}) ≃ Fin n) : (hp.monodromyTriple ν).σ1 = ν.permCongr ((hp.monodromyPerm TauCeti.ThricePuncturedSphere.basePt) TauCeti.ThricePuncturedSphere.periph1)

The second component of the monodromy triple is the monodromy along the peripheral element at 1, read through the numbering.

@[simp]

theorem IsCoveringMap.monodromyTriple_σinf {n : ℕ} {E : Type u} [TopologicalSpace E] {p : E → TauCeti.ThricePuncturedSphere} (hp : IsCoveringMap p) (ν : ↑(p ⁻¹' {TauCeti.ThricePuncturedSphere.basePt}) ≃ Fin n) : (hp.monodromyTriple ν).σinf = ν.permCongr ((hp.monodromyPerm TauCeti.ThricePuncturedSphere.basePt) TauCeti.ThricePuncturedSphere.periphInf)

The third component of the monodromy triple is the monodromy along the peripheral element at ∞.

@[simp]

theorem IsCoveringMap.monodromyGroup_monodromyTriple {n : ℕ} {E : Type u} [TopologicalSpace E] {p : E → TauCeti.ThricePuncturedSphere} (hp : IsCoveringMap p) (ν : ↑(p ⁻¹' {TauCeti.ThricePuncturedSphere.basePt}) ≃ Fin n) : (hp.monodromyTriple ν).monodromyGroup = Subgroup.map ν.permCongrHom.toMonoidHom (hp.monodromyPerm TauCeti.ThricePuncturedSphere.basePt).range

The monodromy group of the monodromy triple is the image of the monodromy representation, transported to Fin n by the numbering.

theorem IsCoveringMap.isConnected_monodromyTriple_iff {n : ℕ} {E : Type u} [TopologicalSpace E] {p : E → TauCeti.ThricePuncturedSphere} (hp : IsCoveringMap p) (ν : ↑(p ⁻¹' {TauCeti.ThricePuncturedSphere.basePt}) ≃ Fin n) : (hp.monodromyTriple ν).IsConnected ↔ PathConnectedSpace E

The monodromy triple is connected exactly when the total space of the cover is path connected.

theorem IsCoveringMap.isConnected_monodromyTriple {n : ℕ} {E : Type u} [TopologicalSpace E] {p : E → TauCeti.ThricePuncturedSphere} (hp : IsCoveringMap p) (ν : ↑(p ⁻¹' {TauCeti.ThricePuncturedSphere.basePt}) ≃ Fin n) [PathConnectedSpace E] : (hp.monodromyTriple ν).IsConnected

The monodromy triple of a cover with path-connected total space is connected.

theorem IsCoveringMap.monodromyTriple_eq_of_comp_eq {n : ℕ} {E F : Type u} [TopologicalSpace E] [TopologicalSpace F] {p : E → TauCeti.ThricePuncturedSphere} {q : F → TauCeti.ThricePuncturedSphere} (hp : IsCoveringMap p) (ν : ↑(p ⁻¹' {TauCeti.ThricePuncturedSphere.basePt}) ≃ Fin n) (hq : IsCoveringMap q) (ν' : ↑(q ⁻¹' {TauCeti.ThricePuncturedSphere.basePt}) ≃ Fin n) (f : C(E, F)) (hf : q ∘ ⇑f = p) (hν : ∀ (e : ↑(p ⁻¹' {TauCeti.ThricePuncturedSphere.basePt})), ν' (Function.fiberMap (⇑f) hf TauCeti.ThricePuncturedSphere.basePt e) = ν e) : hq.monodromyTriple ν' = hp.monodromyTriple ν

A map of covers over ℂ ∖ {0, 1} carrying the point numbered i of the first fibre to the point numbered i of the second has the same monodromy triple on both sides.

theorem IsCoveringMap.monodromyTriple_trans {n : ℕ} {E : Type u} [TopologicalSpace E] {p : E → TauCeti.ThricePuncturedSphere} (hp : IsCoveringMap p) (ν : ↑(p ⁻¹' {TauCeti.ThricePuncturedSphere.basePt}) ≃ Fin n) (τ : Equiv.Perm (Fin n)) : hp.monodromyTriple (ν.trans τ) = τ • hp.monodromyTriple ν

Renumbering the fibre by a permutation τ of Fin n relabels the monodromy triple by τ.

theorem IsCoveringMap.isoClass_monodromyTriple_eq {n : ℕ} {E : Type u} [TopologicalSpace E] {p : E → TauCeti.ThricePuncturedSphere} (hp : IsCoveringMap p) (ν ν' : ↑(p ⁻¹' {TauCeti.ThricePuncturedSphere.basePt}) ≃ Fin n) : TauCeti.PermutationTriple.IsoClass.mk (hp.monodromyTriple ν') = TauCeti.PermutationTriple.IsoClass.mk (hp.monodromyTriple ν)

The isomorphism class of the monodromy triple does not depend on the numbering of the fibre.

theorem IsCoveringMap.isoClass_monodromyTriple_eq_of_homeomorph {n : ℕ} {E F : Type u} [TopologicalSpace E] [TopologicalSpace F] {p : E → TauCeti.ThricePuncturedSphere} {q : F → TauCeti.ThricePuncturedSphere} (hp : IsCoveringMap p) (ν : ↑(p ⁻¹' {TauCeti.ThricePuncturedSphere.basePt}) ≃ Fin n) (hq : IsCoveringMap q) (ν' : ↑(q ⁻¹' {TauCeti.ThricePuncturedSphere.basePt}) ≃ Fin n) (f : E ≃ₜ F) (hf : q ∘ ⇑f = p) : TauCeti.PermutationTriple.IsoClass.mk (hq.monodromyTriple ν') = TauCeti.PermutationTriple.IsoClass.mk (hp.monodromyTriple ν)

Covers of ℂ ∖ {0, 1} that are homeomorphic over ℂ ∖ {0, 1} have isomorphic monodromy triples, whatever the numberings of their fibres.