6.29. MappingDegree.HLcUnconditional🔗

Jacobians.MappingDegree.HLcUnconditional — source

fibreCard_isLocallyConstant_on_subset_of_localSheets

Local-constancy of fibre cardinality on a subset, from a per-fibre local-sheet supplier.

Given f : X → Y continuous with X compact T2 and Y T2, a subset R : Set Y, finiteness of the fibre over every y ∈ R, and a LocalSheetData f y x for every y ∈ R and every x ∈ f ⁻¹' {y}, the fibre-cardinality function fun y : R => (f ⁻¹' {y.val}).ncard is locally constant.

This is HurwitzPatchingData.ofLocalSheets chained into fibreCard_isLocallyConstant_on_subset_of_pointwiseHurwitz.

theorem fibreCard_isLocallyConstant_on_subset_of_localSheets
    {X : Type u} {Y : Type v}
    [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [TopologicalSpace Y] [T2Space Y]
    {f : X → Y} (hf : Continuous f) (R : Set Y)
    (h_fib : ∀ y ∈ R, (f ⁻¹' {y}).Finite)
    (h_sheets : ∀ y ∈ R, ∀ x ∈ f ⁻¹' {y}, LocalSheetData f y x) :
    IsLocallyConstant
      (fun y : (R : Set Y) => (f ⁻¹' {y.val}).ncard)

fibreCard_isLocallyConstant_on_compl_of_localSheets

Locally-constant fibre cardinality on Cᶜ, from a LocalSheetData supplier on Cᶜ.

When C is large enough that the local-biholomorphism witnesses (LocalSheetData) are available at every point of Cᶜ, the fibre cardinality is locally constant on the regular subtype Cᶜ.

The supplier hypothesis h_sheets is satisfied when C ⊇ critical_values f (where critical values are the f-images of points where the local multiplicity exceeds 1): on the complement, the analytic local normal form is z ↦ z (multiplicity 1), and AnalyticAt.exists_local_biholomorphism yields the open partial homeomorphism that is exactly a LocalSheetData. The transport from chart-flat ℂ → ℂ to f : X → Y is supplied by LocalSheetDataFromContMDiff.lean.

theorem fibreCard_isLocallyConstant_on_compl_of_localSheets
    {X : Type u} {Y : Type v}
    [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [TopologicalSpace Y] [T2Space Y]
    {f : X → Y} (hf : Continuous f) (C : Set Y)
    (h_fib : ∀ y ∈ (Cᶜ : Set Y), (f ⁻¹' {y}).Finite)
    (h_sheets : ∀ y ∈ (Cᶜ : Set Y), ∀ x ∈ f ⁻¹' {y},
      LocalSheetData f y x) :
    IsLocallyConstant
      (fun y : (Cᶜ : Set Y) => (f ⁻¹' {y.val}).ncard)