Regular covers of the thrice-punctured sphere

Let c be a connected cover of the thrice-punctured sphere U = ℂ ∖ {0, 1} whose fibre over the basepoint b = 1/2 is numbered by Fin n, and let t be its monodromy triple. This file proves that the following are equivalent:

• the deck group acts transitively on the fibre over b, or equivalently on every fibre (TauCeti.Deck.IsRegular);
• the triple t is regular (TauCeti.PermutationTriple.IsRegular);
• the subgroup of π₁(U, b) recovered from any point of the fibre over b is normal;
• the monodromy group of the cover, the image of π₁(U, b) in the permutations of the fibre, acts freely on the fibre;
• the deck group has order n, and likewise the monodromy group has order n.

The group π₁(U, b) is free on the peripheral loops (TauCeti.ThricePuncturedSphere.fundamentalGroupMulEquivFreeGroup), so the third condition is normality of the corresponding subgroup of FreeGroup (Fin 2). For a regular cover the deck group is isomorphic to the opposite of the monodromy group of t (TauCeti.ConnectedFiberNumberedCover.deckMulEquivMonodromyGroupMulOpposite).

The correspondence with normal subgroups of triangle groups goes through the quotient map TauCeti.ThricePuncturedSphere.toTriangleGroup a b c : π₁(U, b) →* Δ(a, b, c) sending the peripheral loops at 0 and 1 to the generators x and y. When the components of t have orders dividing a, b, c, the monodromy representation of the cover factors through it and the permutation representation TauCeti.TriangleGroup.toPerm t of Δ(a, b, c), so the subgroup of π₁(U, b) recovered from the point labelled i is the preimage of the stabiliser of i in Δ(a, b, c). For a regular cover this is the preimage of the kernel of toPerm t, which is the normal subgroup that TauCeti.TriangleGroup.regularIsoClassEquiv attaches to the class of t.

Main declarations

• TauCeti.ConnectedFiberNumberedCover.isRegular_proj_iff: a numbered cover of U is regular exactly when its triple is.
• TauCeti.ConnectedFiberNumberedCover.normal_range_mapOfEq_iff: the recovered subgroup is normal exactly when the triple is regular.
• TauCeti.ConnectedFiberNumberedCover.isRegular_iff_isCancelSMul: the triple is regular exactly when the monodromy group acts freely on the fibre.
• TauCeti.ConnectedFiberNumberedCover.isRegular_iff_card_deck, TauCeti.ConnectedFiberNumberedCover.isRegular_iff_card_range_monodromyPerm: the triple is regular exactly when the deck group, respectively the monodromy group, has order the degree.
• TauCeti.ConnectedFiberNumberedCover.deckMulEquivMonodromyGroupMulOpposite: the deck group of a regular cover is the opposite of the monodromy group of its triple.
• TauCeti.ThricePuncturedSphere.toTriangleGroup: the quotient map π₁(U, b) →* Δ(a, b, c).
• TauCeti.ConnectedFiberNumberedCover.range_mapOfEq_eq_comap_regularIsoClassEquiv: the recovered subgroup of a regular cover is the preimage of the normal subgroup of Δ(a, b, c) attached to its triple.

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, Definition 2.64 and Proposition 2.66 (normal coverings, and normality as deg f = |Mon(f)|).
• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, Proposition 1.39 (normal covering spaces and normal subgroups).

The quotient map to a triangle group

noncomputable def TauCeti.ThricePuncturedSphere.toTriangleGroup (a b c : ℕ) : FundamentalGroup ThricePuncturedSphere basePt →* TriangleGroup a b c

The quotient map π₁(ℂ ∖ {0, 1}, 1/2) →* Δ(a, b, c) sending the peripheral loops periph0 and periph1 to the generators x and y. It is defined through the free basis TauCeti.ThricePuncturedSphere.peripheralBasis.

Equations

• TauCeti.ThricePuncturedSphere.toTriangleGroup a b c = TauCeti.ThricePuncturedSphere.peripheralBasis.lift ![TauCeti.TriangleGroup.x a b c, TauCeti.TriangleGroup.y a b c]

@[simp]

theorem TauCeti.ThricePuncturedSphere.toTriangleGroup_periph0 (a b c : ℕ) : (toTriangleGroup a b c) periph0 = TriangleGroup.x a b c

TauCeti.ThricePuncturedSphere.toTriangleGroup sends the loop around 0 to x.

@[simp]

theorem TauCeti.ThricePuncturedSphere.toTriangleGroup_periph1 (a b c : ℕ) : (toTriangleGroup a b c) periph1 = TriangleGroup.y a b c

TauCeti.ThricePuncturedSphere.toTriangleGroup sends the loop around 1 to y.

@[simp]

theorem TauCeti.ThricePuncturedSphere.toTriangleGroup_periphInf (a b c : ℕ) : (toTriangleGroup a b c) periphInf = TriangleGroup.z a b c

TauCeti.ThricePuncturedSphere.toTriangleGroup sends the loop around ∞ to z.

theorem TauCeti.ThricePuncturedSphere.toTriangleGroup_surjective (a b c : ℕ) : Function.Surjective ⇑(toTriangleGroup a b c)

TauCeti.ThricePuncturedSphere.toTriangleGroup is surjective: x and y generate Δ(a, b, c).

theorem TauCeti.ThricePuncturedSphere.toPerm_permutationTriple_comp_toTriangleGroup {n a b c : ℕ} (ρ : FundamentalGroup ThricePuncturedSphere basePt →* Equiv.Perm (Fin n)) (ha : (permutationTriple ρ).σ0 ^ a = 1) (hb : (permutationTriple ρ).σ1 ^ b = 1) (hc : (permutationTriple ρ).σinf ^ c = 1) : (TriangleGroup.toPerm (permutationTriple ρ) ha hb hc).comp (toTriangleGroup a b c) = ρ

A representation of π₁(ℂ ∖ {0, 1}, 1/2) factors through the triangle group Δ(a, b, c) whenever the components of its triple have orders dividing a, b and c: it is the permutation representation of the triple composed with TauCeti.ThricePuncturedSphere.toTriangleGroup.

Regularity of the deck action

theorem TauCeti.ConnectedFiberNumberedCover.isPretransitive_deck_iff_isRegular {n : ℕ} (c : ConnectedFiberNumberedCover ThricePuncturedSphere.basePt n) : MulAction.IsPretransitive ↥(deck ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c.cover))) ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c.cover)) ⁻¹' {ThricePuncturedSphere.basePt}) ↔ (↑c.connectedTriple).IsRegular

The deck group of a numbered cover of ℂ ∖ {0, 1} acts transitively on the fibre over 1/2 exactly when the triple of the cover is regular.

theorem TauCeti.ConnectedFiberNumberedCover.isRegular_proj_iff {n : ℕ} (c : ConnectedFiberNumberedCover ThricePuncturedSphere.basePt n) : Deck.IsRegular ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c.cover)) ↔ (↑c.connectedTriple).IsRegular

A numbered cover of ℂ ∖ {0, 1} is regular exactly when its triple is regular: the deck group acts transitively on every fibre exactly when the triple is regular.

theorem TauCeti.ConnectedFiberNumberedCover.isRegular_iff_card_deck {n : ℕ} (c : ConnectedFiberNumberedCover ThricePuncturedSphere.basePt n) : (↑c.connectedTriple).IsRegular ↔ Nat.card ↥(deck ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c.cover))) = n

A numbered cover of ℂ ∖ {0, 1} is regular exactly when its deck group has order the degree.

theorem TauCeti.ConnectedFiberNumberedCover.isRegular_iff_card_range_monodromyPerm {n : ℕ} (c : ConnectedFiberNumberedCover ThricePuncturedSphere.basePt n) : (↑c.connectedTriple).IsRegular ↔ Nat.card ↥(⋯.monodromyPerm ThricePuncturedSphere.basePt).range = n

A numbered cover of ℂ ∖ {0, 1} is regular exactly when its monodromy group, the image of π₁(ℂ ∖ {0, 1}, 1/2) in the permutations of the fibre over 1/2, has order the degree.

The recovered subgroup and the monodromy action

theorem TauCeti.ConnectedFiberNumberedCover.normal_range_mapOfEq_iff {n : ℕ} (c : ConnectedFiberNumberedCover ThricePuncturedSphere.basePt n) (e : ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c.cover)) ⁻¹' {ThricePuncturedSphere.basePt})) : (FundamentalGroup.mapOfEq { toFun := ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c.cover)), continuous_toFun := ⋯ } ⋯).range.Normal ↔ (↑c.connectedTriple).IsRegular

The subgroup of π₁(ℂ ∖ {0, 1}, 1/2) recovered from a point of the fibre over 1/2 is normal exactly when the triple of the cover is regular. Through the isomorphism TauCeti.ThricePuncturedSphere.fundamentalGroupMulEquivFreeGroup this is normality of the corresponding subgroup of FreeGroup (Fin 2).

theorem TauCeti.ConnectedFiberNumberedCover.isRegular_iff_isCancelSMul {n : ℕ} (c : ConnectedFiberNumberedCover ThricePuncturedSphere.basePt n) : (↑c.connectedTriple).IsRegular ↔ IsCancelSMul ↥(⋯.monodromyPerm ThricePuncturedSphere.basePt).range ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c.cover)) ⁻¹' {ThricePuncturedSphere.basePt})

A numbered cover of ℂ ∖ {0, 1} is regular exactly when its monodromy group acts freely on the fibre over 1/2.

noncomputable def TauCeti.ConnectedFiberNumberedCover.deckMulEquivMonodromyGroupMulOpposite {n : ℕ} (c : ConnectedFiberNumberedCover ThricePuncturedSphere.basePt n) (h : (↑c.connectedTriple).IsRegular) (i : Fin n) : ↥(deck ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c.cover))) ≃* (↥(↑c.connectedTriple).monodromyGroup)ᵐᵒᵖ

The deck group of a regular numbered cover of ℂ ∖ {0, 1} is the opposite of the monodromy group of its triple. A deck transformation φ goes to the unique element of the monodromy group moving the label i to the label of the image under φ of the point labelled i (unop_deckMulEquivMonodromyGroupMulOpposite_smul).

Equations

• c.deckMulEquivMonodromyGroupMulOpposite h i = c.deckMulEquiv.trans (TauCeti.PermutationTriple.automorphismGroupMulEquivMonodromyGroupMulOpposite h i)

@[simp]

theorem TauCeti.ConnectedFiberNumberedCover.unop_deckMulEquivMonodromyGroupMulOpposite_smul {n : ℕ} (c : ConnectedFiberNumberedCover ThricePuncturedSphere.basePt n) (h : (↑c.connectedTriple).IsRegular) (i : Fin n) (φ : ↥(deck ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c.cover)))) : MulOpposite.unop ((c.deckMulEquivMonodromyGroupMulOpposite h i) φ) • i = (c.deckPerm φ) i

The element of the monodromy group attached to a deck transformation φ moves the label i as φ does.

Comparison with normal subgroups of triangle groups

theorem TauCeti.ConnectedFiberNumberedCover.toPerm_comp_toTriangleGroup {n : ℕ} (c : ConnectedFiberNumberedCover ThricePuncturedSphere.basePt n) {a b k : ℕ} (ha : (↑c.connectedTriple).σ0 ^ a = 1) (hb : (↑c.connectedTriple).σ1 ^ b = 1) (hk : (↑c.connectedTriple).σinf ^ k = 1) : (TriangleGroup.toPerm (↑c.connectedTriple) ha hb hk).comp (ThricePuncturedSphere.toTriangleGroup a b k) = c.ν.permCongrHom.toMonoidHom.comp (⋯.monodromyPerm ThricePuncturedSphere.basePt)

The monodromy representation of a numbered cover of ℂ ∖ {0, 1} factors through the triangle group Δ(a, b, k), whenever the components of its triple have orders dividing a, b and k: it is the permutation representation of the triple composed with the quotient map TauCeti.ThricePuncturedSphere.toTriangleGroup.

theorem TauCeti.ConnectedFiberNumberedCover.range_mapOfEq_eq_comap_comap_stabilizer {n : ℕ} (c : ConnectedFiberNumberedCover ThricePuncturedSphere.basePt n) {a b k : ℕ} (ha : (↑c.connectedTriple).σ0 ^ a = 1) (hb : (↑c.connectedTriple).σ1 ^ b = 1) (hk : (↑c.connectedTriple).σinf ^ k = 1) (i : Fin n) : (FundamentalGroup.mapOfEq { toFun := ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c.cover)), continuous_toFun := ⋯ } ⋯).range = Subgroup.comap (ThricePuncturedSphere.toTriangleGroup a b k) (Subgroup.comap (TriangleGroup.toPerm (↑c.connectedTriple) ha hb hk) (MulAction.stabilizer (Equiv.Perm (Fin n)) i))

The subgroup recovered from the point labelled i is the preimage of the stabiliser of i under the action of the triangle group Δ(a, b, k) on the labels.

theorem TauCeti.ConnectedFiberNumberedCover.range_mapOfEq_eq_comap_ker {n : ℕ} (c : ConnectedFiberNumberedCover ThricePuncturedSphere.basePt n) {a b k : ℕ} (ha : (↑c.connectedTriple).σ0 ^ a = 1) (hb : (↑c.connectedTriple).σ1 ^ b = 1) (hk : (↑c.connectedTriple).σinf ^ k = 1) (h : (↑c.connectedTriple).IsRegular) (e : ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c.cover)) ⁻¹' {ThricePuncturedSphere.basePt})) : (FundamentalGroup.mapOfEq { toFun := ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c.cover)), continuous_toFun := ⋯ } ⋯).range = Subgroup.comap (ThricePuncturedSphere.toTriangleGroup a b k) (TriangleGroup.toPerm (↑c.connectedTriple) ha hb hk).ker

The subgroup recovered from any point of the fibre of a regular cover is the preimage of the kernel of the action of the triangle group Δ(a, b, k) on the labels.

theorem TauCeti.ConnectedFiberNumberedCover.range_mapOfEq_eq_comap_regularIsoClassEquiv {n : ℕ} (c : ConnectedFiberNumberedCover ThricePuncturedSphere.basePt n) {a b k : ℕ} (ha : (↑c.connectedTriple).σ0 ^ a = 1) (hb : (↑c.connectedTriple).σ1 ^ b = 1) (hk : (↑c.connectedTriple).σinf ^ k = 1) [NeZero n] (h : (↑c.connectedTriple).IsRegular) (e : ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c.cover)) ⁻¹' {ThricePuncturedSphere.basePt})) : (FundamentalGroup.mapOfEq { toFun := ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c.cover)), continuous_toFun := ⋯ } ⋯).range = Subgroup.comap (ThricePuncturedSphere.toTriangleGroup a b k) ↑(TriangleGroup.regularIsoClassEquiv ⟨PermutationTriple.IsoClass.mk ↑c.connectedTriple, ⋯⟩)

A regular cover of ℂ ∖ {0, 1} matches the normal subgroup of the triangle group attached to its triple. The subgroup recovered from any point of the fibre is the preimage under TauCeti.ThricePuncturedSphere.toTriangleGroup of the normal subgroup of index n of Δ(a, b, k) that TauCeti.TriangleGroup.regularIsoClassEquiv attaches to the class of the triple.

The threaded examples

theorem TauCeti.ConnectedFiberNumberedCover.isRegular_proj_of_connectedTriple_eq_cyclicTriple {n : ℕ} (c : ConnectedFiberNumberedCover ThricePuncturedSphere.basePt n) (hc : ↑c.connectedTriple = PermutationTriple.cyclicTriple n) : Deck.IsRegular ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c.cover))

The cover of ℂ ∖ {0, 1} with the triple of z ↦ zⁿ is regular.

theorem TauCeti.ConnectedFiberNumberedCover.isRegular_proj_of_connectedTriple_eq_torusTriple (c : ConnectedFiberNumberedCover ThricePuncturedSphere.basePt 4) (hc : ↑c.connectedTriple = PermutationTriple.torusTriple) : Deck.IsRegular ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c.cover))

The degree-four cover of ℂ ∖ {0, 1} with the torus triple is regular.