6.23. MappingDegree.DegreeWellDefined🔗

Jacobians.MappingDegree.DegreeWellDefined — source

degreeFiber_eq_card_of_regular_witness

Witness independence of degreeFiber. For any RegularValueWitnessReg f, the chosen witness's card equals degreeFiber f hf.

theorem degreeFiber_eq_card_of_regular_witness
    {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]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnc : ¬ Jacobians.Discharge.IsConstantMap f)
    (w : Jacobians.Discharge.ContMDiff.RegularValueWitnessReg f) :
    Jacobians.Discharge.ContMDiff.degreeFiber f hf = w.card