Topological branched covers of the sphere with branch values in {0, 1, ∞}

A topological branched cover of degree n (TauCeti.TopBranchedCover n) is a compact, connected, Hausdorff space Z with a continuous map π : Z → OnePoint ℂ that is a covering map of degree n over the thrice-punctured sphere, the complement of the three marked points 0, 1 and ∞ (TauCeti.ThricePuncturedSphere.marked), and that is locally w ↦ w ^ e, in charts, at every point over a marked point. These are the objects that analytic Riemann existence for three-point covers classifies, by finite covers of the thrice-punctured sphere on the topological side and by Belyi maps on the analytic side.

The local exponent is a topological invariant (TauCeti.IsLocalPowerAt.unique), so every point z has a well-defined local degree TauCeti.TopBranchedCover.localDegree, equal to 1 off the marked fibres. Every fibre of π is finite, and the local degrees over any point add up to the degree: ∑ e = n. Thus the local degrees in each fibre form a partition of the covering degree, the ramification partition TauCeti.TopBranchedCover.ramificationPartition, recording how sheets coalesce over branch values. It is 1ⁿ away from the marked points and is invariant under isomorphism.

Deleting the fibres over the three marked points leaves a connected cover of degree n of the thrice-punctured sphere (TauCeti.TopBranchedCover.connectedCover), compatibly with isomorphisms, so restriction descends to isomorphism classes. Conversely, a branched cover is determined by this unbranched part: every continuous map over the thrice-punctured sphere between unbranched parts extends uniquely to the total spaces (TauCeti.TopBranchedCover.extend), so every isomorphism of unbranched parts extends to a unique isomorphism of branched covers, and restriction is injective on isomorphism classes. This is the uniqueness of the compactification of a finite cover of the thrice-punctured sphere. The extension exists because at a point of a marked fibre the values of the map cluster in a connected subset of a finite fibre, hence at a single point. In particular the deck group of π is the deck group of the unbranched cover (TauCeti.TopBranchedCover.deckMulEquivDeckRestrict).

The data carries no atlas and no surjectivity or countability axiom. The local models at marked points and the covering map elsewhere already provide a chart around every point (TauCeti.TopBranchedCover.exists_mem_source), so Z is a compact topological surface, hence second countable (TauCeti.TopBranchedCover.instSecondCountableTopology); they also make π open, so π is surjective onto the connected sphere (TauCeti.TopBranchedCover.surjective), and properness of π is a consequence of compactness (TauCeti.TopBranchedCover.isProperMap).

Main definitions

• TauCeti.TopBranchedCover n: a topological branched cover of the sphere of degree n with branch values in {0, 1, ∞}.
• TauCeti.TopBranchedCover.Iso: isomorphisms, homeomorphisms commuting with the projections.
• TauCeti.TopBranchedCover.IsoClass n: branched covers of degree n up to isomorphism.
• TauCeti.TopBranchedCover.localDegree: the local degree at a point.
• TauCeti.TopBranchedCover.ramificationPartition: the partition of the degree formed by the local degrees over a point.
• TauCeti.TopBranchedCover.restrict: the projection restricted to the complement of the marked fibres, as a map to the thrice-punctured sphere.
• TauCeti.TopBranchedCover.connectedCover: the connected finite cover of the thrice-punctured sphere obtained by deleting the marked fibres.
• TauCeti.TopBranchedCover.IsoClass.restrict: restriction on isomorphism classes, to isomorphism classes of connected covers of the thrice-punctured sphere.
• TauCeti.TopBranchedCover.extend: the extension of a continuous map over the thrice-punctured sphere between unbranched parts to the total spaces.
• TauCeti.TopBranchedCover.Iso.ofRestrict: the extension of a homeomorphism over the thrice-punctured sphere between unbranched parts to an isomorphism of branched covers.
• TauCeti.TopBranchedCover.Iso.ofConnectedCoverIso: the extension of an isomorphism of the unbranched connected covers to an isomorphism of branched covers, inverse to TauCeti.TopBranchedCover.Iso.connectedCoverIso.
• TauCeti.TopBranchedCover.deckMulEquivDeckRestrict: restriction identifies the deck group of a branched cover with the deck group of its unbranched part.
• TauCeti.TopBranchedCover.sphere: the sphere over itself, of degree 1.

Main results

• TauCeti.TopBranchedCover.localDegree_eq_iff: the local degree is the unique exponent of a local power model.
• TauCeti.TopBranchedCover.localDegree_eq_one: off the marked fibres the local degree is 1.
• TauCeti.TopBranchedCover.finite_preimage_singleton: every fibre is finite.
• TauCeti.TopBranchedCover.finsum_mem_preimage_singleton_localDegree: the local degrees over any point sum to the degree.
• TauCeti.TopBranchedCover.parts_ramificationPartition_of_notMem_marked: off the marked points the ramification partition is 1ⁿ.
• TauCeti.TopBranchedCover.Iso.localDegree_apply, TauCeti.TopBranchedCover.Iso.ramificationPartition_eq: isomorphisms preserve local degrees and ramification partitions.
• TauCeti.TopBranchedCover.isConnected_preimage_range: deleting the marked fibres leaves a connected space, which is moreover path connected (TauCeti.TopBranchedCover.instPathConnectedSpacePreimageRange).
• TauCeti.TopBranchedCover.natCard_restrict_preimage_singleton: the restricted cover has degree n.
• TauCeti.TopBranchedCover.Iso.connectedCoverIso: an isomorphism of branched covers restricts to an isomorphism of their unbranched connected covers.
• TauCeti.TopBranchedCover.dense_preimage_range: the unbranched part is dense.
• TauCeti.TopBranchedCover.eq_extend: the extension of a map of unbranched parts is unique.
• TauCeti.TopBranchedCover.Iso.restrict_injective: an isomorphism of branched covers is determined by its restriction to the unbranched parts.
• TauCeti.TopBranchedCover.IsoClass.restrict_injective: uniqueness of the compactification, a branched cover is determined up to isomorphism by its unbranched connected cover.

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, §1.2 (branched coverings, their local degrees, and the compactification of finite covers of a punctured surface; Lemma 1.80 and Proposition 1.81 for its uniqueness).
• O. Forster, Lectures on Riemann Surfaces, Graduate Texts in Mathematics 81, Springer, 1981, §4 (the multiplicities over every point of a proper map add up to its degree).
• TauCeti.Analysis.Complex.RiemannSurface.Degree, whose analytic fibre-sum argument supplies the proof plan adapted to the topological local-degree setting here.

structure TauCeti.TopBranchedCover (n : ℕ) : Type (u + 1)

A topological branched cover of the sphere of degree n with branch values in {0, 1, ∞}: a compact, connected, Hausdorff space Z with a continuous map π : Z → OnePoint ℂ which is a covering map with fibres of n points over the complement of the marked points, and which is locally w ↦ w ^ e, in a chart at the source and one at the target, at every point over a marked point.

The usual requirements that π be surjective and that Z be second countable are consequences (TauCeti.TopBranchedCover.surjective, TauCeti.TopBranchedCover.instSecondCountableTopology), so they are not part of the data.

The exponent e is not part of the data: it is unique (TauCeti.IsLocalPowerAt.unique), and is recorded as TauCeti.TopBranchedCover.localDegree. The degree hypothesis only concerns unmarked points: over a marked point the fibre has fewer points whenever π is branched there, and it is the local degrees that add up to n instead (TauCeti.TopBranchedCover.finsum_mem_preimage_singleton_localDegree).

• Z : Type u

  The total space.

• instTopologicalSpace : TopologicalSpace self.Z
• instCompactSpace : CompactSpace self.Z
• instConnectedSpace : ConnectedSpace self.Z
• instT2Space : T2Space self.Z
• π : C(self.Z, OnePoint ℂ)

  The branched covering map.

• isCoveringMapOn : IsCoveringMapOn (⇑self.π) ThricePuncturedSphere.markedᶜ

  Off the three marked points, π is a covering map.

• natCard_preimage_singleton (y : OnePoint ℂ) : y ∉ ThricePuncturedSphere.marked → Nat.card ↑(⇑self.π ⁻¹' {y}) = n

  Off the three marked points, the fibres of π have n points.

• exists_isLocalPowerAt_of_mem_marked (z : self.Z) : self.π z ∈ ThricePuncturedSphere.marked → ∃ (e : ℕ), IsLocalPowerAt (⇑self.π) z e

  Over each marked point, π is w ↦ w ^ e in some chart at the source and some chart at the target.

theorem TauCeti.TopBranchedCover.isProperMap {n : ℕ} (X : TopBranchedCover n) : IsProperMap ⇑X.π

The branched covering map is proper, since its source is compact.

theorem TauCeti.TopBranchedCover.isCoveringMap_restrictPreimage {n : ℕ} (X : TopBranchedCover n) : IsCoveringMap (ThricePuncturedSphere.markedᶜ.restrictPreimage ⇑X.π)

Over the complement of the marked points, π restricts to a covering map.

The unbranched cover

noncomputable def TauCeti.TopBranchedCover.restrict {n : ℕ} (X : TopBranchedCover n) : ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint) → ThricePuncturedSphere

The projection π restricted to the complement of the fibres over 0, 1 and ∞, viewed as a map to ThricePuncturedSphere through toOnePoint.

@[simp]

theorem TauCeti.TopBranchedCover.coe_restrict_apply {n : ℕ} (X : TopBranchedCover n) (z : ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)) : ↑↑(X.restrict z) = X.π ↑z

The restricted projection agrees with the branched covering map, read in the Riemann sphere.

theorem TauCeti.TopBranchedCover.isCoveringMap_restrict {n : ℕ} (X : TopBranchedCover n) : IsCoveringMap X.restrict

Deleting the fibres over the three marked points leaves a covering of the thrice-punctured sphere.

theorem TauCeti.TopBranchedCover.isLocalPowerAt_one {n : ℕ} (X : TopBranchedCover n) {z : X.Z} (hz : X.π z ∉ ThricePuncturedSphere.marked) : IsLocalPowerAt (⇑X.π) z 1

Off the marked fibres, π is locally the first power map.

theorem TauCeti.TopBranchedCover.exists_isLocalPowerAt {n : ℕ} (X : TopBranchedCover n) (z : X.Z) : ∃ (e : ℕ), IsLocalPowerAt (⇑X.π) z e

At every point, π is locally a power map.

theorem TauCeti.TopBranchedCover.exists_mem_source {n : ℕ} (X : TopBranchedCover n) (z : X.Z) : ∃ (φ : OpenPartialHomeomorph X.Z ℂ), z ∈ φ.source

Every point of the total space lies in the source of a chart to ℂ, so the total space is a topological surface.

instance TauCeti.TopBranchedCover.instSecondCountableTopology {n : ℕ} (X : TopBranchedCover n) : SecondCountableTopology X.Z

The total space is second countable: it is compact and covered by charts to ℂ.

theorem TauCeti.TopBranchedCover.surjective {n : ℕ} (X : TopBranchedCover n) : Function.Surjective ⇑X.π

The branched covering map is surjective: by the local power models it is open at every point, and its image is compact, hence closed, in the connected sphere.

noncomputable def TauCeti.TopBranchedCover.localDegree {n : ℕ} (X : TopBranchedCover n) (z : X.Z) : ℕ

The local degree of a branched cover at a point z: the exponent e for which π is w ↦ w ^ e near z, in charts (TauCeti.TopBranchedCover.localDegree_eq_iff). It is 1 off the marked fibres (TauCeti.TopBranchedCover.localDegree_eq_one).

theorem TauCeti.TopBranchedCover.isLocalPowerAt_localDegree {n : ℕ} (X : TopBranchedCover n) (z : X.Z) : IsLocalPowerAt (⇑X.π) z (X.localDegree z)

The branched covering map is locally w ↦ w ^ e at z, for e the local degree.

theorem TauCeti.TopBranchedCover.localDegree_eq_iff {n : ℕ} (X : TopBranchedCover n) {z : X.Z} {e : ℕ} : X.localDegree z = e ↔ IsLocalPowerAt (⇑X.π) z e

The local degree is the unique exponent for which π is locally a power map.

theorem TauCeti.TopBranchedCover.localDegree_pos {n : ℕ} (X : TopBranchedCover n) (z : X.Z) : 0 < X.localDegree z

Local degrees are positive.

@[simp]

theorem TauCeti.TopBranchedCover.localDegree_eq_one {n : ℕ} (X : TopBranchedCover n) {z : X.Z} (hz : X.π z ∉ ThricePuncturedSphere.marked) : X.localDegree z = 1

Off the marked fibres, the local degree is 1.

theorem TauCeti.TopBranchedCover.finite_preimage_singleton {n : ℕ} (X : TopBranchedCover n) (y : OnePoint ℂ) : (⇑X.π ⁻¹' {y}).Finite

Every fibre of a branched cover is finite: it is compact, and its points are isolated in it by the local power models.

theorem TauCeti.TopBranchedCover.finite_preimage_marked {n : ℕ} (X : TopBranchedCover n) : (⇑X.π ⁻¹' ThricePuncturedSphere.marked).Finite

The fibres over the three marked points are finite.

theorem TauCeti.TopBranchedCover.dense_preimage_range {n : ℕ} (X : TopBranchedCover n) : Dense (⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)

The complement of the marked fibres is dense in the total space: the marked fibres are finite, and no point of the total space is isolated, since every point lies in a chart to ℂ.

theorem TauCeti.TopBranchedCover.image_val_restrict_preimage_singleton {n : ℕ} (X : TopBranchedCover n) (z : ThricePuncturedSphere) : Subtype.val '' X.restrict ⁻¹' {z} = ⇑X.π ⁻¹' {z.toOnePoint}

The points over z in the restricted cover are exactly the points over z in the original branched cover.

theorem TauCeti.TopBranchedCover.finite_restrict_preimage_singleton {n : ℕ} (X : TopBranchedCover n) (z : ThricePuncturedSphere) : (X.restrict ⁻¹' {z}).Finite

Every fibre of the restricted cover is finite.

theorem TauCeti.TopBranchedCover.natCard_restrict_preimage_singleton {n : ℕ} (X : TopBranchedCover n) (z : ThricePuncturedSphere) : Nat.card ↑(X.restrict ⁻¹' {z}) = n

Every fibre of the restricted cover has n points.

theorem TauCeti.TopBranchedCover.isConnected_preimage_range {n : ℕ} (X : TopBranchedCover n) : IsConnected (⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)

Removing the fibres over 0, 1 and ∞ from the connected total space leaves a connected space.

instance TauCeti.TopBranchedCover.instPathConnectedSpacePreimageRange {n : ℕ} (X : TopBranchedCover n) : PathConnectedSpace ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)

The total space of the restricted cover is path connected.

theorem TauCeti.TopBranchedCover.nonempty_restrict_preimage_singleton_equiv {n : ℕ} (X : TopBranchedCover n) (z : ThricePuncturedSphere) : Nonempty (↑(X.restrict ⁻¹' {z}) ≃ Fin n)

Every fibre of the restricted cover can be numbered by Fin n.

noncomputable def TauCeti.TopBranchedCover.connectedCover {n : ℕ} (X : TopBranchedCover n) : ConnectedCover ThricePuncturedSphere.basePt n

The connected degree-n cover of the thrice-punctured sphere obtained by deleting the fibres over the three marked points.

noncomputable def TauCeti.TopBranchedCover.connectedCoverHomeomorph {n : ℕ} (X : TopBranchedCover n) : ↑X.connectedCover.cover.obj.left ≃ₜ ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)

The canonical identification of the packaged connected cover's total space with the complement of the marked fibres.

theorem TauCeti.TopBranchedCover.restrict_connectedCoverHomeomorph {n : ℕ} (X : TopBranchedCover n) (z : ↑X.connectedCover.cover.obj.left) : X.restrict (X.connectedCoverHomeomorph z) = (CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj X.connectedCover.cover)) z

Under the canonical identification, the packaged cover's projection is the restricted branched-cover projection.

theorem TauCeti.TopBranchedCover.π_connectedCoverHomeomorph {n : ℕ} (X : TopBranchedCover n) (z : ↑X.connectedCover.cover.obj.left) : X.π ↑(X.connectedCoverHomeomorph z) = ↑↑((CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj X.connectedCover.cover)) z)

Under the canonical identification, the branched-cover projection is the packaged cover's projection, read in the Riemann sphere.

theorem TauCeti.TopBranchedCover.finsum_mem_preimage_singleton_localDegree {n : ℕ} (X : TopBranchedCover n) (y : OnePoint ℂ) : ∑ᶠ (z : X.Z) (_ : z ∈ ⇑X.π ⁻¹' {y}), X.localDegree z = n

The local degrees over any point add up to the degree. Over an unmarked point this is the degree hypothesis; over a marked point q, it says that the multiset of local degrees over q is a partition of n.

theorem TauCeti.TopBranchedCover.ne_zero {n : ℕ} (X : TopBranchedCover n) : n ≠ 0

The degree of a branched cover is positive: an unmarked point has a nonempty finite fibre.

Ramification partitions

noncomputable def TauCeti.TopBranchedCover.ramificationPartition {n : ℕ} (X : TopBranchedCover n) (y : OnePoint ℂ) : n.Partition

The ramification partition of a branched cover over a point y of the sphere: the partition of the degree n whose parts are the local degrees at the points of the fibre over y (TauCeti.TopBranchedCover.parts_ramificationPartition), one part for each point. It is a partition of n because the local degrees over y add up to the degree (TauCeti.TopBranchedCover.finsum_mem_preimage_singleton_localDegree).

theorem TauCeti.TopBranchedCover.parts_ramificationPartition {n : ℕ} (X : TopBranchedCover n) (y : OnePoint ℂ) : (X.ramificationPartition y).parts = Multiset.map X.localDegree ⋯.toFinset.val

The parts of the ramification partition over y are the local degrees at the points of the fibre over y.

@[simp]

theorem TauCeti.TopBranchedCover.mem_parts_ramificationPartition {n : ℕ} (X : TopBranchedCover n) {y : OnePoint ℂ} {e : ℕ} : e ∈ (X.ramificationPartition y).parts ↔ ∃ (z : X.Z), X.π z = y ∧ X.localDegree z = e

A number is a part of the ramification partition over y exactly when it is the local degree at some point over y.

@[simp]

theorem TauCeti.TopBranchedCover.card_parts_ramificationPartition {n : ℕ} (X : TopBranchedCover n) (y : OnePoint ℂ) : (X.ramificationPartition y).parts.card = (⇑X.π ⁻¹' {y}).ncard

The ramification partition over y has one part for each point of the fibre over y.

theorem TauCeti.TopBranchedCover.parts_ramificationPartition_of_notMem_marked {n : ℕ} (X : TopBranchedCover n) {y : OnePoint ℂ} (hy : y ∉ ThricePuncturedSphere.marked) : (X.ramificationPartition y).parts = Multiset.replicate n 1

Away from the marked points the ramification partition is 1ⁿ: the branched cover is unramified there.

Isomorphisms

structure TauCeti.TopBranchedCover.Iso {n : ℕ} (X : TopBranchedCover n) (Y : TopBranchedCover n) : Type (max u_1 u_2)

An isomorphism of topological branched covers: a homeomorphism of the total spaces commuting with the branched covering maps.

• toHomeomorph : X.Z ≃ₜ Y.Z

  The homeomorphism of total spaces.

• π_apply (z : X.Z) : Y.π (self.toHomeomorph z) = X.π z

  The homeomorphism commutes with the branched covering maps.

theorem TauCeti.TopBranchedCover.Iso.ext_iff {n : ℕ} {X : TopBranchedCover n} {Y : TopBranchedCover n} {x y : X.Iso Y} : x = y ↔ x.toHomeomorph = y.toHomeomorph

theorem TauCeti.TopBranchedCover.Iso.ext {n : ℕ} {X : TopBranchedCover n} {Y : TopBranchedCover n} {x y : X.Iso Y} (toHomeomorph : x.toHomeomorph = y.toHomeomorph) : x = y

def TauCeti.TopBranchedCover.Iso.refl {n : ℕ} (X : TopBranchedCover n) : X.Iso X

The identity isomorphism.

@[simp]

theorem TauCeti.TopBranchedCover.Iso.refl_toHomeomorph {n : ℕ} (X : TopBranchedCover n) : (refl X).toHomeomorph = Homeomorph.refl X.Z

def TauCeti.TopBranchedCover.Iso.symm {n : ℕ} {X : TopBranchedCover n} {Y : TopBranchedCover n} (ι : X.Iso Y) : Y.Iso X

The inverse of an isomorphism.

@[simp]

theorem TauCeti.TopBranchedCover.Iso.symm_toHomeomorph {n : ℕ} {X : TopBranchedCover n} {Y : TopBranchedCover n} (ι : X.Iso Y) : ι.symm.toHomeomorph = ι.toHomeomorph.symm

def TauCeti.TopBranchedCover.Iso.trans {n : ℕ} {X : TopBranchedCover n} {Y : TopBranchedCover n} {W : TopBranchedCover n} (ι : X.Iso Y) (κ : Y.Iso W) : X.Iso W

The composite of two isomorphisms.

@[simp]

theorem TauCeti.TopBranchedCover.Iso.trans_toHomeomorph {n : ℕ} {X : TopBranchedCover n} {Y : TopBranchedCover n} {W : TopBranchedCover n} (ι : X.Iso Y) (κ : Y.Iso W) : (ι.trans κ).toHomeomorph = ι.toHomeomorph.trans κ.toHomeomorph

def TauCeti.TopBranchedCover.Iso.restrict {n : ℕ} {X : TopBranchedCover n} {Y : TopBranchedCover n} (ι : X.Iso Y) : ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint) ≃ₜ ↑(⇑Y.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)

The homeomorphism of the restricted total spaces induced by an isomorphism of topological branched covers.

@[simp]

theorem TauCeti.TopBranchedCover.Iso.coe_restrict_apply {n : ℕ} {X : TopBranchedCover n} {Y : TopBranchedCover n} (ι : X.Iso Y) (z : ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)) : ↑(ι.restrict z) = ι.toHomeomorph ↑z

@[simp]

theorem TauCeti.TopBranchedCover.Iso.refl_restrict {n : ℕ} (X : TopBranchedCover n) : (refl X).restrict = Homeomorph.refl ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)

@[simp]

theorem TauCeti.TopBranchedCover.Iso.symm_restrict {n : ℕ} {X : TopBranchedCover n} {Y : TopBranchedCover n} (ι : X.Iso Y) : ι.symm.restrict = ι.restrict.symm

@[simp]

theorem TauCeti.TopBranchedCover.Iso.trans_restrict {n : ℕ} {X : TopBranchedCover n} {Y : TopBranchedCover n} {W : TopBranchedCover n} (ι : X.Iso Y) (κ : Y.Iso W) : (ι.trans κ).restrict = ι.restrict.trans κ.restrict

@[simp]

theorem TauCeti.TopBranchedCover.Iso.restrict_restrict {n : ℕ} {X : TopBranchedCover n} {Y : TopBranchedCover n} (ι : X.Iso Y) (z : ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)) : Y.restrict (ι.restrict z) = X.restrict z

The restriction of an isomorphism of topological branched covers commutes with the projections to the thrice-punctured sphere.

noncomputable def TauCeti.TopBranchedCover.Iso.connectedCoverHomeomorph {n : ℕ} {X Y : TopBranchedCover n} (ι : X.Iso Y) : ↑X.connectedCover.cover.obj.left ≃ₜ ↑Y.connectedCover.cover.obj.left

The homeomorphism between the packaged total spaces induced by restriction of an isomorphism of topological branched covers, expressed through their canonical identifications with the complements of the marked fibres.

noncomputable def TauCeti.TopBranchedCover.Iso.connectedCoverIso {n : ℕ} {X Y : TopBranchedCover n} (ι : X.Iso Y) : X.connectedCover.cover ≅ Y.connectedCover.cover

The restriction of an isomorphism of topological branched covers is an isomorphism of the associated connected covers of the thrice-punctured sphere.

@[simp]

theorem TauCeti.TopBranchedCover.Iso.connectedCoverIso_hom_hom_left {n : ℕ} {X Y : TopBranchedCover n} (ι : X.Iso Y) : CategoryTheory.Over.Hom.left ι.connectedCoverIso.hom.hom = (TopCat.isoOfHomeo ι.connectedCoverHomeomorph).hom

@[simp]

theorem TauCeti.TopBranchedCover.Iso.connectedCoverIso_inv_hom_left {n : ℕ} {X Y : TopBranchedCover n} (ι : X.Iso Y) : CategoryTheory.Over.Hom.left ι.connectedCoverIso.inv.hom = (TopCat.isoOfHomeo ι.connectedCoverHomeomorph).inv

@[simp]

theorem TauCeti.TopBranchedCover.Iso.localDegree_apply {n : ℕ} {X : TopBranchedCover n} {Y : TopBranchedCover n} (ι : X.Iso Y) (z : X.Z) : Y.localDegree (ι.toHomeomorph z) = X.localDegree z

Isomorphisms of branched covers preserve local degrees.

theorem TauCeti.TopBranchedCover.Iso.ramificationPartition_eq {n : ℕ} {X : TopBranchedCover n} {Y : TopBranchedCover n} (ι : X.Iso Y) (y : OnePoint ℂ) : Y.ramificationPartition y = X.ramificationPartition y

Isomorphic branched covers have the same ramification partition over every point.

@[instance_reducible]

instance TauCeti.TopBranchedCover.isoSetoid (n : ℕ) : Setoid (TopBranchedCover n)

Branched covers related by isomorphism.

def TauCeti.TopBranchedCover.IsoClass (n : ℕ) : Type (u + 1)

Topological branched covers of the sphere of degree n with branch values in {0, 1, ∞}, up to isomorphism.

def TauCeti.TopBranchedCover.IsoClass.mk {n : ℕ} (X : TopBranchedCover n) : IsoClass n

The isomorphism class of a branched cover.

@[simp]

theorem TauCeti.TopBranchedCover.IsoClass.mk_eq_mk_iff {n : ℕ} {X Y : TopBranchedCover n} : mk X = mk Y ↔ Nonempty (X.Iso Y)

Two branched covers have the same isomorphism class exactly when they are isomorphic.

noncomputable def TauCeti.TopBranchedCover.IsoClass.restrict {n : ℕ} : IsoClass n → ConnectedCoverClass ThricePuncturedSphere.basePt n

Restricting over the thrice-punctured sphere sends an isomorphism class of topological branched covers to an isomorphism class of connected covers.

@[simp]

theorem TauCeti.TopBranchedCover.IsoClass.restrict_mk {n : ℕ} (X : TopBranchedCover n) : (mk X).restrict = ConnectedCoverClass.mk X.connectedCover

Restriction on isomorphism classes is represented by restriction of branched covers.

theorem TauCeti.TopBranchedCover.IsoClass.mk_surjective {n : ℕ} : Function.Surjective mk

Every isomorphism class is the class of a branched cover.

Uniqueness of the compactification

A branched cover is determined by its unbranched part: every continuous map over the thrice-punctured sphere between the unbranched parts of two branched covers extends uniquely to their total spaces. At a point x over a marked point q, the punctured neighbourhoods of x are connected, so the cluster set of the map at x is a connected subset of the finite fibre over q: a single point, which is the limit.

noncomputable def TauCeti.TopBranchedCover.extend {n : ℕ} {X : TopBranchedCover n} {m : ℕ} {Y : TopBranchedCover m} (f : C(↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint), ↑(⇑Y.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint))) (hπ : ∀ (z : ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)), Y.π ↑(f z) = X.π ↑z) : C(X.Z, Y.Z)

The extension of a continuous map over the thrice-punctured sphere from the unbranched part of X to that of Y to a continuous map of total spaces. It agrees with f on the unbranched part (TauCeti.TopBranchedCover.extend_apply_val), commutes with the projections (TauCeti.TopBranchedCover.π_extend_apply), and is the only continuous map with the first property (TauCeti.TopBranchedCover.eq_extend).

@[simp]

theorem TauCeti.TopBranchedCover.extend_apply_val {n : ℕ} {X : TopBranchedCover n} {m : ℕ} {Y : TopBranchedCover m} (f : C(↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint), ↑(⇑Y.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint))) (hπ : ∀ (z : ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)), Y.π ↑(f z) = X.π ↑z) (z : ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)) : (extend f hπ) ↑z = ↑(f z)

On the unbranched part, the extension of f is f.

theorem TauCeti.TopBranchedCover.eq_extend {n : ℕ} {X : TopBranchedCover n} {m : ℕ} {Y : TopBranchedCover m} (f : C(↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint), ↑(⇑Y.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint))) (hπ : ∀ (z : ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)), Y.π ↑(f z) = X.π ↑z) {g : C(X.Z, Y.Z)} (hg : ∀ (z : ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)), g ↑z = ↑(f z)) : g = extend f hπ

A continuous map of total spaces agreeing with f on the unbranched part is the extension of f.

@[simp]

theorem TauCeti.TopBranchedCover.π_extend_apply {n : ℕ} {X : TopBranchedCover n} {m : ℕ} {Y : TopBranchedCover m} (f : C(↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint), ↑(⇑Y.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint))) (hπ : ∀ (z : ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)), Y.π ↑(f z) = X.π ↑z) (x : X.Z) : Y.π ((extend f hπ) x) = X.π x

The extension of f commutes with the projections.

theorem TauCeti.TopBranchedCover.extend_apply_extend_apply {n : ℕ} {X : TopBranchedCover n} {m : ℕ} {Y : TopBranchedCover m} (f : C(↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint), ↑(⇑Y.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint))) (hπ : ∀ (z : ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)), Y.π ↑(f z) = X.π ↑z) (g : C(↑(⇑Y.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint), ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint))) (hg : ∀ (z : ↑(⇑Y.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)), X.π ↑(g z) = Y.π ↑z) (hgf : ∀ (z : ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)), g (f z) = z) (x : X.Z) : (extend g hg) ((extend f hπ) x) = x

If g is a left inverse of f on the unbranched parts, the extension of g is a left inverse of the extension of f.

noncomputable def TauCeti.TopBranchedCover.Iso.ofRestrict {n : ℕ} {X : TopBranchedCover n} {Y : TopBranchedCover n} (h : ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint) ≃ₜ ↑(⇑Y.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)) (hπ : ∀ (z : ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)), Y.π ↑(h z) = X.π ↑z) : X.Iso Y

Uniqueness of the compactification. A homeomorphism over the thrice-punctured sphere between the unbranched parts of two branched covers extends to an isomorphism of the branched covers. Its restriction is the given homeomorphism (TauCeti.TopBranchedCover.Iso.restrict_ofRestrict), and it is the only isomorphism with this property (TauCeti.TopBranchedCover.Iso.restrict_injective).

@[simp]

theorem TauCeti.TopBranchedCover.Iso.ofRestrict_toHomeomorph_apply_val {n : ℕ} {X : TopBranchedCover n} {Y : TopBranchedCover n} (h : ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint) ≃ₜ ↑(⇑Y.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)) (hπ : ∀ (z : ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)), Y.π ↑(h z) = X.π ↑z) (z : ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)) : (ofRestrict h hπ).toHomeomorph ↑z = ↑(h z)

On the unbranched part, the homeomorphism underlying TauCeti.TopBranchedCover.Iso.ofRestrict h hπ is h.

@[simp]

theorem TauCeti.TopBranchedCover.Iso.ofRestrict_toHomeomorph_symm_apply_val {n : ℕ} {X : TopBranchedCover n} {Y : TopBranchedCover n} (h : ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint) ≃ₜ ↑(⇑Y.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)) (hπ : ∀ (z : ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)), Y.π ↑(h z) = X.π ↑z) (z : ↑(⇑Y.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)) : (ofRestrict h hπ).toHomeomorph.symm ↑z = ↑(h.symm z)

On the unbranched part, the inverse of the homeomorphism underlying TauCeti.TopBranchedCover.Iso.ofRestrict h hπ is h.symm.

@[simp]

theorem TauCeti.TopBranchedCover.Iso.restrict_ofRestrict {n : ℕ} {X : TopBranchedCover n} {Y : TopBranchedCover n} (h : ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint) ≃ₜ ↑(⇑Y.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)) (hπ : ∀ (z : ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)), Y.π ↑(h z) = X.π ↑z) : (ofRestrict h hπ).restrict = h

On the unbranched part, the extension TauCeti.TopBranchedCover.Iso.ofRestrict h hπ is h.

theorem TauCeti.TopBranchedCover.Iso.restrict_injective {n : ℕ} {X : TopBranchedCover n} {Y : TopBranchedCover n} : Function.Injective restrict

An isomorphism of branched covers is determined by its restriction to the unbranched parts, which are dense.

noncomputable def TauCeti.TopBranchedCover.Iso.ofConnectedCoverIso {n : ℕ} {X Y : TopBranchedCover n} (e : X.connectedCover.cover ≅ Y.connectedCover.cover) : X.Iso Y

An isomorphism of the connected covers obtained by deleting the marked fibres extends to an isomorphism of the branched covers.

@[simp]

theorem TauCeti.TopBranchedCover.Iso.restrict_ofConnectedCoverIso_connectedCoverHomeomorph {n : ℕ} {X Y : TopBranchedCover n} (e : X.connectedCover.cover ≅ Y.connectedCover.cover) (x : ↑X.connectedCover.cover.obj.left) : (ofConnectedCoverIso e).restrict (X.connectedCoverHomeomorph x) = Y.connectedCoverHomeomorph ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Over.Hom.left e.hom.hom)) x)

On the unbranched parts, TauCeti.TopBranchedCover.Iso.ofConnectedCoverIso e is the map of total spaces underlying e.

@[simp]

theorem TauCeti.TopBranchedCover.Iso.connectedCoverIso_ofConnectedCoverIso {n : ℕ} {X Y : TopBranchedCover n} (e : X.connectedCover.cover ≅ Y.connectedCover.cover) : (ofConnectedCoverIso e).connectedCoverIso = e

Restricting the extension of an isomorphism of connected covers recovers it.

@[simp]

theorem TauCeti.TopBranchedCover.Iso.ofConnectedCoverIso_connectedCoverIso {n : ℕ} {X Y : TopBranchedCover n} (ι : X.Iso Y) : ofConnectedCoverIso ι.connectedCoverIso = ι

An isomorphism of branched covers is the extension of its restriction to the connected covers.

theorem TauCeti.TopBranchedCover.IsoClass.restrict_injective {n : ℕ} : Function.Injective restrict

Uniqueness of the compactification, on isomorphism classes: a topological branched cover is determined up to isomorphism by the connected cover of the thrice-punctured sphere obtained by deleting its marked fibres.

Deck transformations

noncomputable def TauCeti.TopBranchedCover.deckMulEquivDeckRestrict {n : ℕ} (X : TopBranchedCover n) : ↥(deck ⇑X.π) ≃* ↥(deck X.restrict)

The deck group of a branched cover is the deck group of its unbranched part. A deck transformation of π restricts to one of the unbranched cover TauCeti.TopBranchedCover.restrict, and every deck transformation of the unbranched cover extends uniquely across the marked fibres (TauCeti.TopBranchedCover.Iso.ofRestrict).

@[simp]

theorem TauCeti.TopBranchedCover.coe_deckMulEquivDeckRestrict_apply {n : ℕ} (X : TopBranchedCover n) (φ : ↥(deck ⇑X.π)) (z : ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)) : ↑(↑(X.deckMulEquivDeckRestrict φ) z) = ↑φ ↑z

On the unbranched part, the restriction of a deck transformation is the deck transformation.

@[simp]

theorem TauCeti.TopBranchedCover.coe_deckMulEquivDeckRestrict_symm_apply {n : ℕ} (X : TopBranchedCover n) (ψ : ↥(deck X.restrict)) (z : ↑(⇑X.π ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)) : ↑(X.deckMulEquivDeckRestrict.symm ψ) ↑z = ↑(↑ψ z)

On the unbranched part, the extension of a deck transformation of the unbranched cover is that deck transformation.

The sphere over itself

noncomputable def TauCeti.TopBranchedCover.sphere : TopBranchedCover 1

The sphere OnePoint ℂ over itself by the identity: the topological branched cover of degree 1, unbranched everywhere.

noncomputable def TauCeti.TopBranchedCover.sphereHomeomorph : sphere.Z ≃ₜ OnePoint ℂ

The canonical homeomorphism from the total space of sphere to the Riemann sphere.

@[simp]

theorem TauCeti.TopBranchedCover.sphere_π_apply (z : sphere.Z) : sphere.π z = sphereHomeomorph z

The projection of sphere is its canonical homeomorphism to the Riemann sphere.

@[simp]

theorem TauCeti.TopBranchedCover.sphere_localDegree (z : sphere.Z) : sphere.localDegree z = 1

The sphere over itself is unbranched: all its local degrees are 1.