Points of the filled cover

For a map to the thrice-punctured sphere, one point is added for each connected component over each of the three standard punctured neighborhoods. For a finite cover, the component-cycle equivalences identify the number of added points with the sum of the three full cycle counts of its monodromy triple.

These are the new points in the compactification of a finite cover. Their puncture labels determine where the extended map sends them. A homeomorphism over the thrice-punctured sphere transports these added points by its induced bijections on connected components, preserving puncture labels and respecting identities, inverses, and composition. The component bijections use Mathlib's Topology.IsCoinducing.connectedComponentsHomeomorph.

References

• E. Girondo and G. González-Diez, Introduction to Compact Riemann Surfaces and Dessins d'Enfants, §1.2.7 (one added point for each component over a puncture).

def TauCeti.FilledPoint {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) : Type u_1

The components above the punctures 0, 1, and ∞, respectively. Each component contributes one point to the filled cover.

noncomputable def TauCeti.FilledPoint.overZero {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodZero) → FilledPoint p

Add a point over the puncture 0 for each component of its punctured preimage.

noncomputable def TauCeti.FilledPoint.overOne {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodOne) → FilledPoint p

Add a point over the puncture 1 for each component of its punctured preimage.

noncomputable def TauCeti.FilledPoint.overInf {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodInf) → FilledPoint p

Add a point over the puncture ∞ for each component of its punctured preimage.

noncomputable def TauCeti.FilledPoint.equivSum {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) : FilledPoint p ≃ ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodZero) ⊕ ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodOne) ⊕ ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodInf)

The three kinds of added point, as an explicit sum for defining maps out of them.

@[simp]

theorem TauCeti.FilledPoint.equivSum_overZero {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) (c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodZero)) : (equivSum p) (overZero p c) = Sum.inl c

@[simp]

theorem TauCeti.FilledPoint.equivSum_overOne {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) (c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodOne)) : (equivSum p) (overOne p c) = Sum.inr (Sum.inl c)

@[simp]

theorem TauCeti.FilledPoint.equivSum_overInf {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) (c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodInf)) : (equivSum p) (overInf p c) = Sum.inr (Sum.inr c)

noncomputable def TauCeti.FilledPoint.sigmaEquiv {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) : FilledPoint p ≃ (q : ThricePuncturedSphere.Puncture) × ConnectedComponents ↑(p ⁻¹' q.neighborhood)

The added points as pairs ⟨q, c⟩ of a puncture q and a connected component c of p ⁻¹' D_q*, so that the three punctures can be handled by one argument.

@[simp]

theorem TauCeti.FilledPoint.sigmaEquiv_overZero {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) (c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodZero)) : (sigmaEquiv p) (overZero p c) = ⟨ThricePuncturedSphere.Puncture.zero, c⟩

@[simp]

theorem TauCeti.FilledPoint.sigmaEquiv_overOne {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) (c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodOne)) : (sigmaEquiv p) (overOne p c) = ⟨ThricePuncturedSphere.Puncture.one, c⟩

@[simp]

theorem TauCeti.FilledPoint.sigmaEquiv_overInf {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) (c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodInf)) : (sigmaEquiv p) (overInf p c) = ⟨ThricePuncturedSphere.Puncture.inf, c⟩

@[simp]

theorem TauCeti.FilledPoint.sigmaEquiv_symm_zero {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) (c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.Puncture.zero.neighborhood)) : (sigmaEquiv p).symm ⟨ThricePuncturedSphere.Puncture.zero, c⟩ = overZero p c

@[simp]

theorem TauCeti.FilledPoint.sigmaEquiv_symm_one {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) (c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.Puncture.one.neighborhood)) : (sigmaEquiv p).symm ⟨ThricePuncturedSphere.Puncture.one, c⟩ = overOne p c

@[simp]

theorem TauCeti.FilledPoint.sigmaEquiv_symm_inf {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) (c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.Puncture.inf.neighborhood)) : (sigmaEquiv p).symm ⟨ThricePuncturedSphere.Puncture.inf, c⟩ = overInf p c

theorem TauCeti.FilledPoint.overZero_injective {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) : Function.Injective (overZero p)

theorem TauCeti.FilledPoint.overOne_injective {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) : Function.Injective (overOne p)

theorem TauCeti.FilledPoint.overInf_injective {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) : Function.Injective (overInf p)

noncomputable def TauCeti.FilledPoint.puncture {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) : FilledPoint p → Fin 3

The puncture over which an added point lies, with 0, 1, and 2 representing 0, 1, and ∞.

@[simp]

theorem TauCeti.FilledPoint.puncture_overZero {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) (c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodZero)) : puncture p (overZero p c) = 0

@[simp]

theorem TauCeti.FilledPoint.puncture_overOne {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) (c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodOne)) : puncture p (overOne p c) = 1

@[simp]

theorem TauCeti.FilledPoint.puncture_overInf {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) (c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodInf)) : puncture p (overInf p c) = 2

theorem TauCeti.FilledPoint.cases {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) (y : FilledPoint p) : (∃ (c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodZero)), y = overZero p c) ∨ (∃ (c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodOne)), y = overOne p c) ∨ ∃ (c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodInf)), y = overInf p c

Every added point lies over exactly one of the three punctures.

theorem TauCeti.FilledPoint.puncture_eq_zero_iff {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) (y : FilledPoint p) : puncture p y = 0 ↔ ∃ (c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodZero)), y = overZero p c

The points labelled 0 are exactly those constructed over 0.

theorem TauCeti.FilledPoint.puncture_eq_one_iff {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) (y : FilledPoint p) : puncture p y = 1 ↔ ∃ (c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodOne)), y = overOne p c

The points labelled 1 are exactly those constructed over 1.

theorem TauCeti.FilledPoint.puncture_eq_two_iff {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) (y : FilledPoint p) : puncture p y = 2 ↔ ∃ (c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodInf)), y = overInf p c

The points labelled 2 (the puncture ∞) are exactly those constructed over ∞.

def TauCeti.FilledPoint.neighborhoodCongr {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} {F : Type u_2} [TopologicalSpace F] {p' : F → ThricePuncturedSphere} (h : E ≃ₜ F) (hh : p' ∘ ⇑h = p) (q : ThricePuncturedSphere.Puncture) : ↑(p ⁻¹' q.neighborhood) ≃ₜ ↑(p' ⁻¹' q.neighborhood)

Restrict an isomorphism over the sphere to the preimage of a standard punctured neighbourhood.

@[simp]

theorem TauCeti.FilledPoint.coe_neighborhoodCongr_apply {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} {F : Type u_2} [TopologicalSpace F] {p' : F → ThricePuncturedSphere} (h : E ≃ₜ F) (hh : p' ∘ ⇑h = p) (q : ThricePuncturedSphere.Puncture) (x : ↑(p ⁻¹' q.neighborhood)) : ↑((neighborhoodCongr h hh q) x) = h ↑x

@[simp]

theorem TauCeti.FilledPoint.coe_neighborhoodCongr_symm_apply {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} {F : Type u_2} [TopologicalSpace F] {p' : F → ThricePuncturedSphere} (h : E ≃ₜ F) (hh : p' ∘ ⇑h = p) (q : ThricePuncturedSphere.Puncture) (y : ↑(p' ⁻¹' q.neighborhood)) : ↑((neighborhoodCongr h hh q).symm y) = h.symm ↑y

noncomputable def TauCeti.FilledPoint.congr {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} {F : Type u_2} [TopologicalSpace F] {p' : F → ThricePuncturedSphere} (h : E ≃ₜ F) (hh : p' ∘ ⇑h = p) : FilledPoint p ≃ FilledPoint p'

An isomorphism over the sphere transports added points by its induced bijection on components over each puncture.

@[simp]

theorem TauCeti.FilledPoint.sigmaEquiv_congr {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} {F : Type u_2} [TopologicalSpace F] {p' : F → ThricePuncturedSphere} (h : E ≃ₜ F) (hh : p' ∘ ⇑h = p) (i : FilledPoint p) : (sigmaEquiv p') ((congr h hh) i) = ⟨((sigmaEquiv p) i).fst, ⋯.connectedComponentsMap ((sigmaEquiv p) i).snd⟩

The puncture and component of a transported point.

@[simp]

theorem TauCeti.FilledPoint.congr_sigmaEquiv_symm_mk {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} {F : Type u_2} [TopologicalSpace F] {p' : F → ThricePuncturedSphere} (h : E ≃ₜ F) (hh : p' ∘ ⇑h = p) (q : ThricePuncturedSphere.Puncture) (x : ↑(p ⁻¹' q.neighborhood)) : (congr h hh) ((sigmaEquiv p).symm ⟨q, ConnectedComponents.mk x⟩) = (sigmaEquiv p').symm ⟨q, ConnectedComponents.mk ((neighborhoodCongr h hh q) x)⟩

On a component represented by a point, transport is represented by the image point.

@[simp]

theorem TauCeti.FilledPoint.puncture_congr {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} {F : Type u_2} [TopologicalSpace F] {p' : F → ThricePuncturedSphere} (h : E ≃ₜ F) (hh : p' ∘ ⇑h = p) (i : FilledPoint p) : puncture p' ((congr h hh) i) = puncture p i

Transport does not change the puncture label.

@[simp]

theorem TauCeti.FilledPoint.congr_refl {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} : congr (Homeomorph.refl E) ⋯ = Equiv.refl (FilledPoint p)

Identity isomorphisms fix every added point.

theorem TauCeti.FilledPoint.congr_trans {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} {F : Type u_2} {G : Type u_3} [TopologicalSpace F] [TopologicalSpace G] {p' : F → ThricePuncturedSphere} {p'' : G → ThricePuncturedSphere} (h : E ≃ₜ F) (hh : p' ∘ ⇑h = p) (k : F ≃ₜ G) (hk : p'' ∘ ⇑k = p') : congr (h.trans k) ⋯ = (congr h hh).trans (congr k hk)

Transport along a composite is the composite of the two transports.

@[simp]

theorem TauCeti.FilledPoint.symm_congr {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} {F : Type u_2} [TopologicalSpace F] {p' : F → ThricePuncturedSphere} (h : E ≃ₜ F) (hh : p' ∘ ⇑h = p) : (congr h hh).symm = congr h.symm ⋯

Transport along the inverse isomorphism reverses transport.

theorem TauCeti.FilledPoint.finite {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) {n : ℕ} (hp : IsCoveringMap p) (ν : ↑(p ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) : Finite (FilledPoint p)

A numbered finite cover has only finitely many added points.

theorem TauCeti.FilledPoint.natCard_eq_cycleCounts {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) {n : ℕ} (hp : IsCoveringMap p) (ν : ↑(p ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) : Nat.card (FilledPoint p) = (hp.monodromyTriple ν).cycleCounts.1 + (hp.monodromyTriple ν).cycleCounts.2.1 + (hp.monodromyTriple ν).cycleCounts.2.2

The number of points added to a numbered finite cover is the sum of the cycle counts of its three monodromy permutations. Fixed points count as cycles of length one.

noncomputable def TauCeti.FilledCover.indexEquiv {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {n : ℕ} (ν : ↑(p ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) : FilledPoint p ≃ Quotient (Equiv.Perm.SameCycle.setoid (hp.monodromyTriple ν).σ0) ⊕ Quotient (Equiv.Perm.SameCycle.setoid (hp.monodromyTriple ν).σ1) ⊕ Quotient (Equiv.Perm.SameCycle.setoid (hp.monodromyTriple ν).σinf)

The added points are the cycles of the monodromy. For a cover whose fibre over 1/2 is numbered by ν, the components of p ⁻¹' D_q* over the punctures 0, 1 and ∞, which are the points added in FilledCover p, are the cycles of σ0, σ1 and σinf respectively (IsCoveringMap.sameCycleQuotientσ0EquivConnectedComponents and its analogues).

@[simp]

theorem TauCeti.FilledCover.indexEquiv_overZero {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {n : ℕ} (ν : ↑(p ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) (c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodZero)) : (indexEquiv hp ν) (FilledPoint.overZero p c) = Sum.inl ((hp.sameCycleQuotientσ0EquivConnectedComponents ν).symm c)

@[simp]

theorem TauCeti.FilledCover.indexEquiv_overOne {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {n : ℕ} (ν : ↑(p ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) (c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodOne)) : (indexEquiv hp ν) (FilledPoint.overOne p c) = Sum.inr (Sum.inl ((hp.sameCycleQuotientσ1EquivConnectedComponents ν).symm c))

@[simp]

theorem TauCeti.FilledCover.indexEquiv_overInf {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {n : ℕ} (ν : ↑(p ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) (c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodInf)) : (indexEquiv hp ν) (FilledPoint.overInf p c) = Sum.inr (Sum.inr ((hp.sameCycleQuotientσinfEquivConnectedComponents ν).symm c))

@[simp]

theorem TauCeti.FilledCover.indexEquiv_symm_inl {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {n : ℕ} (ν : ↑(p ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) (a : Quotient (Equiv.Perm.SameCycle.setoid (hp.monodromyTriple ν).σ0)) : (indexEquiv hp ν).symm (Sum.inl a) = FilledPoint.overZero p ((hp.sameCycleQuotientσ0EquivConnectedComponents ν) a)

@[simp]

theorem TauCeti.FilledCover.indexEquiv_symm_inr_inl {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {n : ℕ} (ν : ↑(p ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) (a : Quotient (Equiv.Perm.SameCycle.setoid (hp.monodromyTriple ν).σ1)) : (indexEquiv hp ν).symm (Sum.inr (Sum.inl a)) = FilledPoint.overOne p ((hp.sameCycleQuotientσ1EquivConnectedComponents ν) a)

@[simp]

theorem TauCeti.FilledCover.indexEquiv_symm_inr_inr {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {n : ℕ} (ν : ↑(p ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) (a : Quotient (Equiv.Perm.SameCycle.setoid (hp.monodromyTriple ν).σinf)) : (indexEquiv hp ν).symm (Sum.inr (Sum.inr a)) = FilledPoint.overInf p ((hp.sameCycleQuotientσinfEquivConnectedComponents ν) a)

theorem TauCeti.FilledCover.finite_filledPoint {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) : Finite (FilledPoint p)

A finite cover has finitely many added points. This is FilledPoint.finite, applied to a numbering of the fibre over 1/2, which is finite as soon as one fibre is.