26.5. ProperDegree.Degree🔗

Jacobians.ProperDegree.Degree — source

IsConstantMap

Jacobians.IsConstantMap is the discharge's IsConstantMap.

abbrev IsConstantMap {X : Type _} {Y : Type _} (f : X → Y) : Prop

RegularValueWitness

Jacobians.RegularValueWitness is the discharge's structure.

abbrev RegularValueWitness {X : Type _} {Y : Type _} (f : X → Y) : Type _

RegularValueWitnessReg

Jacobians.RegularValueWitnessReg is the discharge's regularity- certified witness.

abbrev RegularValueWitnessReg
    {X : Type _} [TopologicalSpace X] [ChartedSpace ℂ X]
    {Y : Type _} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    (f : X → Y) : Type _

degreeFiber

Jacobians.degreeFiber is the discharge's fibre-cardinality degree.

noncomputable abbrev degreeFiber

regularValueWitnessReg_nonempty_of_nonConstantMap

Unconditional existence of a regular witness for non-constant analytic maps between compact connected complex 1-manifolds.

theorem regularValueWitnessReg_nonempty_of_nonConstantMap
    {X : Type _} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ, ℂ) ω X]
    {Y : Type _} [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ, ℂ) ω Y]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ, ℂ) 𝓘(ℂ) ω f)
    (hnc : ¬ IsConstantMap f) :
    Nonempty (RegularValueWitnessReg f)

degreeFiber_eq_card_of_regularWitness

Degree well-definedness. For non-constant analytic f, the fibre-cardinality degree degreeFiber f hf equals the card of *any* regularity-certified regular-value witness.

theorem degreeFiber_eq_card_of_regularWitness
    {X : Type _} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ, ℂ) ω X]
    {Y : Type _} [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ, ℂ) ω Y]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ, ℂ) 𝓘(ℂ) ω f)
    (hnc : ¬ IsConstantMap f) (w : RegularValueWitnessReg f) :
    degreeFiber f hf = w.card