6.24. MappingDegree.FibreCardLocallyConstantFromNormalForm🔗

Jacobians.MappingDegree.FibreCardLocallyConstantFromNormalForm — source

HurwitzPatchingData

Hurwitz patching package for f : X → Y at a target point y₀ : Y.

Bundles the data needed to conclude that f is, in a topological neighbourhood of f ⁻¹' {y₀}, a disjoint union of xs.card homeomorphic sheets onto a common neighbourhood of y₀. From this, the cardinality of f ⁻¹' {y} is constant for y near y₀ (and equals xs.card).

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

fibre_ncard_eq_xs_card_of_mem_W

For y ∈ h.W, the cardinality of the fibre f ⁻¹' {y} equals h.xs.card.

lemma fibre_ncard_eq_xs_card_of_mem_W
    (h : HurwitzPatchingData f y₀)
    {y : Y} (hy : y ∈ h.W) :
    (f ⁻¹' {y}).ncard = h.xs.card

fibreCard_isLocallyConstant_on_subset_of_pointwiseHurwitz

Local-constancy on a regular subset.

Suppose R : Set Y and for *every* y₀ ∈ R we are given a HurwitzPatchingData f y₀. Then the fibre-cardinality function (read from the subtype) is locally constant on R.

theorem fibreCard_isLocallyConstant_on_subset_of_pointwiseHurwitz
    {X : Type u} {Y : Type v}
    [TopologicalSpace X] [TopologicalSpace Y]
    (f : X → Y) (R : Set Y)
    (h : ∀ y₀ ∈ R, HurwitzPatchingData f y₀) :
    IsLocallyConstant
      (fun y : (R : Set Y) => (f ⁻¹' {y.val}).ncard)