6.31. MappingDegree.HurwitzPatchingDataConstruction🔗

Jacobians.MappingDegree.HurwitzPatchingDataConstruction — source

LocalSheetData

Per-point local-sheet datum. At a fibre point x of f over y₀, the local-biholomorphism content packages into:

• an open neighbourhood U of x,

• an open neighbourhood V of y₀,

• a continuous local inverse g : Y → X with g '' V ⊆ U, LeftInvOn g f U, RightInvOn g f V.

In particular f is injective on U and surjective from U onto V.

structure LocalSheetData {X : Type u} {Y : Type v}
    [TopologicalSpace X] [TopologicalSpace Y]
    (f : X → Y) (y₀ : Y) (x : X) where

injOn

f is injective on U.

lemma injOn (s : LocalSheetData f y₀ x) : InjOn f s.U

exists_pairwiseDisjoint_open_of_finset

Pairwise-disjoint open neighbourhoods of a finite set in a T2 space.

For any Finset X in a T2 space, there is a function W : X → Set X such that for every x ∈ s, W x is open and contains x, and W x and W x' are disjoint for distinct x, x' ∈ s.

lemma exists_pairwiseDisjoint_open_of_finset
    {X : Type u} [TopologicalSpace X] [T2Space X] (s : Finset X) :
    ∃ W : X → Set X,
      (∀ x ∈ s, IsOpen (W x)) ∧
      (∀ x ∈ s, x ∈ W x) ∧
      (∀ x ∈ s, ∀ x' ∈ s, x ≠ x' → Disjoint (W x) (W x'))

ofLocalSheets

Construction of HurwitzPatchingData from per-point local-sheet data.

Given:

• f : X → Y continuous,

• X compact T2, Y T2,

• y₀ : Y and a *finite* fibre f ⁻¹' {y₀},

• a LocalSheetData f y₀ x for every x ∈ f ⁻¹' {y₀},

construct a HurwitzPatchingData f y₀.

noncomputable def ofLocalSheets
    [T2Space X] [CompactSpace X] [T2Space Y]
    {f : X → Y} (hf : Continuous f) {y₀ : Y}
    (h_fib : (f ⁻¹' {y₀}).Finite)
    (sheets : ∀ x ∈ f ⁻¹' {y₀}, LocalSheetData f y₀ x) :
    HurwitzPatchingData f y₀