6.25. MappingDegree.FibreCardOnRegularSubset🔗

Jacobians.MappingDegree.FibreCardOnRegularSubset — source

fibre_card_well_defined_on_regular_subset_holds_of_locallyConstant

Top-level reduction (regular-form). The fibre_card_well_defined_at_regular_statement conclusion follows from the existence, for every non-constant analytic f, of a regular-value subset R ⊆ Y together with a fibre-cardinality function locally constant on R, preconnected R, and the support witness ∀ w : RegularValueWitnessReg f, w.value ∈ R.

lemma fibre_card_well_defined_on_regular_subset_holds_of_locallyConstant
    {X : Type u} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    {Y : Type v} [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y]
    (h_lc : ∀ (f : X → Y), ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f →
      ¬ Jacobians.Discharge.IsConstantMap f →
      ∃ (R : Set Y) (card_of : Y → ℕ),
        (∀ w : RegularValueWitness f, card_of w.value = w.card) ∧
        (∀ w : RegularValueWitnessReg f, w.toWitness.value ∈ R) ∧
        IsLocallyConstant (fun y : R => card_of y.val) ∧
        IsPreconnected (Set.univ : Set R)) :
    ∀ (f : X → Y), ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f → ¬ Jacobians.Discharge.IsConstantMap f →
      ∀ (w₁ w₂ : RegularValueWitnessReg f), w₁.card = w₂.card