Documentation

TauCeti.AlgebraicTopology.ThricePuncturedSphere.CompactCore

The compact cores of the thrice-punctured sphere #

For ρ > 0, the compact core compactCore ρ of ℂ ∖ {0, 1} is the set of points at distance at least ρ from each of the three punctures, measured in the standard local coordinate z, 1 - z or 1 / z at 0, 1 or ∞:

compactCore ρ = {z | ρ ≤ ‖z‖ ∧ ρ ≤ ‖z - 1‖ ∧ ‖z‖ ≤ ρ⁻¹}.

It is compact, and every compact subset of ℂ ∖ {0, 1} lies in one of them, so the complements of the compact cores form a basis of the cocompact filter: going to infinity in ℂ ∖ {0, 1} means approaching one of the three punctures. The core of radius 1 / 2 is the complement of the three standard punctured neighbourhoods.

A finite cover of ℂ ∖ {0, 1} is a proper map, so the preimage of every compact core is compact. This is the compactness input for filling in the punctures of a finite cover: for small ρ > 0, the cover is the union of the compact preimage of compactCore ρ and of its parts over the closed punctured discs 0 < ‖w‖ ≤ ρ in the coordinates w at 0, 1 and ∞. In the filling charts, each of these parts becomes a finite union of closed discs, hence compact, once its centres are added.

Main definitions #

Main results #

References #

source
def TauCeti.ThricePuncturedSphere.compactCore (ρ : ℝ) :
Set ThricePuncturedSphere

The compact core of radius ρ of the thrice-punctured sphere: the points at distance at least ρ from 0 and from 1, and at distance at most ρ⁻¹ from 0. In the standard local coordinates z, 1 - z and 1 / z at the three punctures, for ρ > 0 these are the points whose coordinate has norm at least ρ. For ρ ≤ 0, the compact core is empty.

Instances For
    source
    @[simp]
    theorem TauCeti.ThricePuncturedSphere.mem_compactCore {ρ : ℝ} {z : ThricePuncturedSphere} :
    z ∈ compactCore ρ ↔ ρ ≤ ‖↑z‖ ∧ ρ ≤ ‖↑z - 1‖ ∧ ‖↑z‖ ≤ ρ⁻¹
    source
    theorem TauCeti.ThricePuncturedSphere.isCompact_compactCore (ρ : ℝ) :
    IsCompact (compactCore ρ)

    The compact core is compact: for ρ > 0 its image in ℂ is closed and bounded and avoids the two finite punctures, and for ρ ≤ 0 it is empty.

    source
    theorem TauCeti.ThricePuncturedSphere.exists_subset_compactCore {K : Set ThricePuncturedSphere} (hK : IsCompact K) :
    ∃ (ρ : ℝ), 0 < ρ ∧ K ⊆ compactCore ρ

    Every compact subset of the thrice-punctured sphere lies in a compact core: on a compact set, the distances to the three punctures in their local coordinates are bounded below by a positive constant.

    source
    theorem TauCeti.ThricePuncturedSphere.hasBasis_cocompact :
    (Filter.cocompact ThricePuncturedSphere).HasBasis (fun (ρ : ℝ) => 0 < ρ) fun (ρ : ℝ) => (compactCore ρ)ᶜ

    The complements of the compact cores of positive radius form a basis of the cocompact filter on the thrice-punctured sphere.

    source
    theorem TauCeti.ThricePuncturedSphere.Puncture.mem_compactCore_iff (q : Puncture) {ρ : ℝ} (hρ : 0 < ρ) {z : ThricePuncturedSphere} (hz : z ∈ q.neighborhood) :
    z ∈ compactCore ρ ↔ 2 * ρ ≤ ‖↑(q.coord ⟨z, hz⟩)‖

    On the standard punctured neighbourhood of a puncture, the compact core of radius ρ > 0 consists of the points whose standard coordinate has norm at least 2 * ρ: the cores are the complements of the punctured discs of radius 2 * ρ about the three punctures in these coordinates.

    source
    theorem TauCeti.ThricePuncturedSphere.compactCore_one_half :
    compactCore (1 / 2) = (puncturedNeighborhoodZero ∪ puncturedNeighborhoodOne ∪ puncturedNeighborhoodInf)ᶜ

    The compact core of radius 1 / 2 is the complement of the three standard punctured neighbourhoods of 0, 1 and ∞.

    source
    theorem IsCoveringMap.isCompact_preimage_compactCore {E : Type u_1} [TopologicalSpace E] {p : E → TauCeti.ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : TauCeti.ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) (ρ : ℝ) :
    IsCompact (p ⁻¹' TauCeti.ThricePuncturedSphere.compactCore ρ)

    The compact core of a finite cover. A covering map of the thrice-punctured sphere with one finite fibre has finite fibres everywhere, so it is proper and the preimage of every compact core is compact.