A machine-checked solution to the Jacobians challenge

19.15. Finiteness.CechModelGeometry🔗

Jacobians.Finiteness.CechModelGeometry — source

isOpen_chartImage_of_subset_source

Chart-image-open atom. The image of an OPEN set s ⊆ (chartAt ℂ y).source under the chart chartAt ℂ y is open in ℂ. (chartAt ℂ y is an OpenPartialHomeomorph, so this is OpenPartialHomeomorph.isOpen_image_of_subset_source.) This is exactly how an overlap chart-image Uov is shown open.

theorem isOpen_chartImage_of_subset_source {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    {y : X} {s : Set X} (hs : IsOpen s)
    (hsub : s ⊆ (chartAt (H := ℂ) y).source) :
    IsOpen ((chartAt (H := ℂ) y) '' s)

isCompact_chartImage_of_subset_source

Compact-image atom. The image of a COMPACT set K ⊆ (chartAt ℂ y).source under the chart chartAt ℂ y is compact in ℂ (the chart is continuous on its source). This is how an overlap chart-image shrinking Kov is shown compact.

theorem isCompact_chartImage_of_subset_source {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    {y : X} {K : Set X} (hK : IsCompact K)
    (hsub : K ⊆ (chartAt (H := ℂ) y).source) :
    IsCompact ((chartAt (H := ℂ) y) '' K)

chartOpen_subset_chartAt_source

For x ∈ chartCover, the outer open shrinkage chartOpen x lies in the chart source (chartOpen x ⊆ shrunkChart x ⊆ (chartAt ℂ x).source). The basic containment behind both the Uov/Kov source-membership obligations.

theorem chartOpen_subset_chartAt_source {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] (x : X) (hx : x ∈ (chartCover : Finset X)) :
    chartOpen (X := X) x ⊆ (chartAt (H := ℂ) x).source

coverCenter

The n-th cover center, where n = #chartCover: enumerate chartCover by Fin #chartCover (Finset.equivFin). Used to give the overlap index J = Fin #chartCover ² a Type 0 carrier (the {x // x ∈ chartCover} subtype lives in X's universe, which DiskOverlapData.J : Type forbids).

noncomputable def coverCenter (a : Fin ((chartCover : Finset X).card)) : X

coverCenter_mem

theorem coverCenter_mem {X : Type*} [TopologicalSpace X] [CompactSpace X]
    [ChartedSpace ℂ X] (a : Fin ((chartCover : Finset X).card)) :
    coverCenter a ∈ (chartCover : Finset X)

chartCoverOverlapData

The chart-cover overlap geometry. From Montel's canonical chart cover of the compact Riemann surface X, the DiskOverlapData whose overlaps are read in the FIRST chart of each ordered pair (coverCenter enumerates the cover charts by Fin #chartCover, keeping the index in Type 0):

  • index J = ordered pairs of cover charts Fin #chartCover ²;

  • Uov (a,b) = chart-a image of the OPEN outer overlap chartOpen a ∩ chartOpen b (open in ℂ);

  • Kov (a,b) = chart-a image of the COMPACT inner overlap innerShrunkChart a ∩ innerShrunkChart b (compact in ℂ, ⊆ Uov by image-monotonicity). The inner shrinkings cover X over chartCover (Montel.iUnion_innerShrunkChart_chartCover_eq, transported through the Fin-enumeration), so this is a genuine *covering* relatively-compact shrinking — the Leray-model geometry, not a placeholder.

noncomputable def chartCoverOverlapData : DiskOverlapData where

iUnion_innerShrunkChart_coverCenter_eq

The inner shrinking covers X. The Kov-overlaps come from innerShrunkChart pieces that cover X over the cover indices: ⋃ a, innerShrunkChart (coverCenter a) = Set.univ. This is the covering property that promotes the geometry from "some compact ⊆ some open" to a genuine *relatively-compact covering shrinking* (the Leray-model geometry). Transports Montel.iUnion_innerShrunkChart_chartCover_eq through the Fin-enumeration coverCenter.

theorem iUnion_innerShrunkChart_coverCenter_eq {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] :
    (⋃ a : Fin ((chartCover : Finset X).card), innerShrunkChart (X := X) (coverCenter a)) =
      Set.univ