Standard punctured neighborhoods of the three punctures

This file fixes pairwise disjoint standard neighborhoods of the punctures 0, 1, and ∞ in the thrice-punctured sphere. In the affine coordinate they are

• puncturedNeighborhoodZero = {z | ‖z‖ < 1 / 2};
• puncturedNeighborhoodOne = {z | ‖z - 1‖ < 1 / 2};
• puncturedNeighborhoodInf = {z | 2 < ‖z‖}.

The missing center of each finite disc is already excluded from ThricePuncturedSphere. The anharmonic maps z ↦ 1 - z and z ↦ 1 / z identify the neighborhoods at 1 and ∞ with the one at 0. Thus all three are copies of the same punctured disc, expressed in the standard local coordinates at the three punctures.

These neighborhoods are the local geometric input for extending a finite cover across the three punctures: their pairwise disjointness lets the three fillings be performed independently.

Main definitions

• puncturedDiscOneHalf: the punctured complex disc of radius 1 / 2.
• puncturedNeighborhoodZero, puncturedNeighborhoodOne, puncturedNeighborhoodInf: the three standard neighborhoods.
• puncturedNeighborhoodZeroHomeomorphPuncturedDiscOneHalf, puncturedNeighborhoodOneHomeomorphPuncturedDiscOneHalf, and puncturedNeighborhoodInfHomeomorphPuncturedDiscOneHalf: their standard local coordinates.

The three neighborhoods

def TauCeti.ThricePuncturedSphere.puncturedDiscOneHalf : Set ℂ

The complex punctured disc of radius 1 / 2, used as the common coordinate model for the three standard punctured neighborhoods.

Equations

• TauCeti.ThricePuncturedSphere.puncturedDiscOneHalf = {z : ℂ | 0 < ‖z‖ ∧ ‖z‖ < 1 / 2}

def TauCeti.ThricePuncturedSphere.puncturedNeighborhoodZero : Set ThricePuncturedSphere

The standard punctured disc of radius 1 / 2 about 0 in the thrice-punctured sphere. The center is absent because points of ThricePuncturedSphere are nonzero.

Equations

• TauCeti.ThricePuncturedSphere.puncturedNeighborhoodZero = {z : TauCeti.ThricePuncturedSphere | ‖↑z‖ < 1 / 2}

def TauCeti.ThricePuncturedSphere.puncturedNeighborhoodOne : Set ThricePuncturedSphere

The standard punctured disc of radius 1 / 2 about 1 in the thrice-punctured sphere. The center is absent because points of ThricePuncturedSphere are not equal to 1.

Equations

• TauCeti.ThricePuncturedSphere.puncturedNeighborhoodOne = {z : TauCeti.ThricePuncturedSphere | ‖↑z - 1‖ < 1 / 2}

def TauCeti.ThricePuncturedSphere.puncturedNeighborhoodInf : Set ThricePuncturedSphere

The standard punctured neighborhood of ∞, represented in the affine coordinate by the exterior of the closed disc of radius 2.

Equations

• TauCeti.ThricePuncturedSphere.puncturedNeighborhoodInf = {z : TauCeti.ThricePuncturedSphere | 2 < ‖↑z‖}

@[simp]

theorem TauCeti.ThricePuncturedSphere.mem_puncturedNeighborhoodZero {z : ThricePuncturedSphere} : z ∈ puncturedNeighborhoodZero ↔ ‖↑z‖ < 1 / 2

@[simp]

theorem TauCeti.ThricePuncturedSphere.mem_puncturedNeighborhoodOne {z : ThricePuncturedSphere} : z ∈ puncturedNeighborhoodOne ↔ ‖↑z - 1‖ < 1 / 2

@[simp]

theorem TauCeti.ThricePuncturedSphere.mem_puncturedNeighborhoodInf {z : ThricePuncturedSphere} : z ∈ puncturedNeighborhoodInf ↔ 2 < ‖↑z‖

@[simp]

theorem TauCeti.ThricePuncturedSphere.mem_puncturedDiscOneHalf {z : ℂ} : z ∈ puncturedDiscOneHalf ↔ 0 < ‖z‖ ∧ ‖z‖ < 1 / 2

theorem TauCeti.ThricePuncturedSphere.isOpen_puncturedNeighborhoodZero : IsOpen puncturedNeighborhoodZero

The standard punctured neighborhood of 0 is open.

theorem TauCeti.ThricePuncturedSphere.isOpen_puncturedNeighborhoodOne : IsOpen puncturedNeighborhoodOne

The standard punctured neighborhood of 1 is open.

theorem TauCeti.ThricePuncturedSphere.isOpen_puncturedNeighborhoodInf : IsOpen puncturedNeighborhoodInf

The standard punctured neighborhood of ∞ is open.

Disjointness

theorem TauCeti.ThricePuncturedSphere.disjoint_puncturedNeighborhoodZero_puncturedNeighborhoodOne : Disjoint puncturedNeighborhoodZero puncturedNeighborhoodOne

The standard punctured neighborhoods of 0 and 1 are disjoint.

theorem TauCeti.ThricePuncturedSphere.disjoint_puncturedNeighborhoodZero_puncturedNeighborhoodInf : Disjoint puncturedNeighborhoodZero puncturedNeighborhoodInf

The standard punctured neighborhoods of 0 and ∞ are disjoint.

theorem TauCeti.ThricePuncturedSphere.disjoint_puncturedNeighborhoodOne_puncturedNeighborhoodInf : Disjoint puncturedNeighborhoodOne puncturedNeighborhoodInf

The standard punctured neighborhoods of 1 and ∞ are disjoint.

Standard local coordinates

noncomputable def TauCeti.ThricePuncturedSphere.puncturedNeighborhoodZeroHomeomorphPuncturedDiscOneHalf : ↑puncturedNeighborhoodZero ≃ₜ ↑puncturedDiscOneHalf

The affine coordinate identifies the standard neighborhood of 0 with the complex punctured disc of radius 1 / 2.

Equations

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

@[simp]

theorem TauCeti.ThricePuncturedSphere.coe_puncturedNeighborhoodZeroHomeomorphPuncturedDiscOneHalf (z : ↑puncturedNeighborhoodZero) : ↑(puncturedNeighborhoodZeroHomeomorphPuncturedDiscOneHalf z) = ↑↑z

@[simp]

theorem TauCeti.ThricePuncturedSphere.coe_puncturedNeighborhoodZeroHomeomorphPuncturedDiscOneHalf_symm_apply (w : ↑puncturedDiscOneHalf) : ↑↑(puncturedNeighborhoodZeroHomeomorphPuncturedDiscOneHalf.symm w) = ↑w

The inverse affine coordinate on the punctured disc is w ↦ w.

noncomputable def TauCeti.ThricePuncturedSphere.puncturedNeighborhoodOneHomeomorphPuncturedDiscOneHalf : ↑puncturedNeighborhoodOne ≃ₜ ↑puncturedDiscOneHalf

The coordinate z ↦ 1 - z identifies the standard neighborhood of 1 with the complex punctured disc of radius 1 / 2.

Equations

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

@[simp]

theorem TauCeti.ThricePuncturedSphere.coe_puncturedNeighborhoodOneHomeomorphPuncturedDiscOneHalf (z : ↑puncturedNeighborhoodOne) : ↑(puncturedNeighborhoodOneHomeomorphPuncturedDiscOneHalf z) = 1 - ↑↑z

@[simp]

theorem TauCeti.ThricePuncturedSphere.coe_puncturedNeighborhoodOneHomeomorphPuncturedDiscOneHalf_symm_apply (w : ↑puncturedDiscOneHalf) : ↑↑(puncturedNeighborhoodOneHomeomorphPuncturedDiscOneHalf.symm w) = 1 - ↑w

The inverse coordinate at 1 is w ↦ 1 - w.

noncomputable def TauCeti.ThricePuncturedSphere.puncturedNeighborhoodInfHomeomorphPuncturedDiscOneHalf : ↑puncturedNeighborhoodInf ≃ₜ ↑puncturedDiscOneHalf

The coordinate z ↦ 1 / z identifies the standard neighborhood of ∞ with the complex punctured disc of radius 1 / 2. This is the standard chart at ∞.

Equations

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

@[simp]

theorem TauCeti.ThricePuncturedSphere.coe_puncturedNeighborhoodInfHomeomorphPuncturedDiscOneHalf (z : ↑puncturedNeighborhoodInf) : ↑(puncturedNeighborhoodInfHomeomorphPuncturedDiscOneHalf z) = 1 / ↑↑z

@[simp]

theorem TauCeti.ThricePuncturedSphere.coe_puncturedNeighborhoodInfHomeomorphPuncturedDiscOneHalf_symm_apply (w : ↑puncturedDiscOneHalf) : ↑↑(puncturedNeighborhoodInfHomeomorphPuncturedDiscOneHalf.symm w) = 1 / ↑w

The inverse coordinate at ∞ is w ↦ 1 / w.