17.10. DolbeaultComparison.LerayCoverExists🔗

Jacobians.DolbeaultComparison.LerayCoverExists — source

simplyConnectedSpace_chartBallPreimage

A chart-preimage of a coordinate ball is simply connected. Let e : OpenPartialHomeomorph X ℂ be a chart and ball cc r ⊆ e.target a coordinate ball inside its target. Then the open set e.source ∩ e ⁻¹' (ball cc r) (the chart-preimage of the ball — a coordinate disk in X) is a SimplyConnectedSpace.

The chart restricted to this set is a homeomorphism onto ball cc r ⊆ ℂ (e.restr has source the set and target ball cc r, by e.right_inv on the target; OpenPartialHomeomorph.toHomeomorphSourceTarget). The ball is contractible (Metric.contractibleSpace_ball), contractibility transports across the homeomorphism (Homeomorph.contractibleSpace), and a contractible space is simply connected (SimplyConnectedSpace.ofContractible, an instance).

theorem simplyConnectedSpace_chartBallPreimage {X : Type*} [TopologicalSpace X]
    (e : OpenPartialHomeomorph X ℂ) (cc : ℂ) (r : ℝ)
    (hr : 0 < r) (hB : Metric.ball cc r ⊆ e.target) :
    SimplyConnectedSpace ↥(e.source ∩ e ⁻¹' Metric.ball cc r)

chartBallRadius

The radius of a coordinate ball around (chartAt ℂ x) x that fits inside the chart target. Exists because (chartAt ℂ x) x ∈ (chartAt ℂ x).target and the target is open (Metric.isOpen_iff).

noncomputable def chartBallRadius (x : X) : ℝ

chartBallRadius_spec

theorem chartBallRadius_spec {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (x : X) :
    0 < chartBallRadius x ∧
      Metric.ball ((chartAt ℂ x) x) (chartBallRadius x) ⊆ (chartAt ℂ x).target

chartBallRadius_pos

theorem chartBallRadius_pos {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (x : X) :
    0 < chartBallRadius x

ball_chartBallRadius_subset_target

theorem ball_chartBallRadius_subset_target {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (x : X) :
    Metric.ball ((chartAt ℂ x) x) (chartBallRadius x) ⊆ (chartAt ℂ x).target

chartDiskRadius

The radius of a smaller chart disk around x, chosen as half of chartBallRadius x.

noncomputable def chartDiskRadius (x : X) : ℝ

chartDiskRadius_pos

theorem chartDiskRadius_pos {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (x : X) :
    0 < chartDiskRadius (X := X) x

closedBall_chartDiskRadius_subset_target

theorem closedBall_chartDiskRadius_subset_target {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] (x : X) :
    Metric.closedBall ((chartAt ℂ x) x) (chartDiskRadius (X := X) x) ⊆
      (chartAt ℂ x).target

chartDiskNbhd

The smaller chart-disk neighborhood of x. This is the cover set that feeds the ChartDiskCover API.

def chartDiskNbhd (x : X) : Set X

chartDiskNbhd_isOpen

theorem chartDiskNbhd_isOpen {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (x : X) :
    IsOpen (chartDiskNbhd (X := X) x)

mem_chartDiskNbhd

theorem mem_chartDiskNbhd {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (x : X) :
    x ∈ chartDiskNbhd (X := X) x

simplyConnectedSpace_chartDiskNbhd

theorem simplyConnectedSpace_chartDiskNbhd {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (x : X) :
    SimplyConnectedSpace ↥(chartDiskNbhd (X := X) x)

exists_finite_chartDiskNbhd_cover

theorem exists_finite_chartDiskNbhd_cover {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [CompactSpace X] :
    ∃ s : Finset X, (⋃ x ∈ s, chartDiskNbhd (X := X) x) = Set.univ

chartDiskCenters

The finite set of centres of the canonical chart-disk cover.

noncomputable def chartDiskCenters : Finset X

chartDiskCenters_cover

theorem chartDiskCenters_cover {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [CompactSpace X] :
    (⋃ x ∈ (chartDiskCenters : Finset X), chartDiskNbhd (X := X) x) = Set.univ

chartDiskCenter

The element of X indexed by Fin (chartDiskCenters.card).

noncomputable def chartDiskCenter (i : Fin (chartDiskCenters (X := X)).card) : X

chartDiskCover

The canonical finite chart-disk cover of a compact Riemann surface.

noncomputable def chartDiskCover : ChartDiskCover X where

chartDiskCover_simplyConnected

Every set of the canonical chart-disk cover is simply connected.

theorem chartDiskCover_simplyConnected (i : (chartDiskCover (X := X)).ι) :
    SimplyConnectedSpace ↥((chartDiskCover (X := X)).U i)