The mapping degree

• RS.degree F : ℕ — total multiplicity of F over an arbitrary basepoint of Y; well-defined (basepoint-independent) by RS.fiberMultSum_eq_degree; 0 for constant maps (RS.degree_of_forall_eq).
• Positivity/bounds: RS.one_le_degree, RS.degree_pos_iff, RS.multiplicity_le_degree.
• Regular-fiber cardinality: RS.ncard_fiber_of_isRegularValue, RS.ncard_fiber_le_degree.
• Degree-1 ⇒ bijective ⇒ homeomorphism (genus-zero-headline / Abel bank): RS.bijective_of_degree_eq_one, RS.homeomorphOfDegreeEqOne, RS.coe_homeomorphOfDegreeEqOne, RS.isHomeomorph_of_degree_eq_one.
• RS.degree_comp — degree of a composition is multiplicative (needs the extra instance [CompactSpace Y], the only statement in the unit that does).

noncomputable def RS.degree {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] [Nonempty Y] (F : X → Y) : ℕ

The mapping degree: total multiplicity of F over an arbitrary basepoint of Y. Well-defined (basepoint-independent) by fiberMultSum_eq_degree; 0 for constant maps (degree_of_forall_eq).

Equations

• RS.degree F = RS.fiberMultSum F (Classical.arbitrary Y)

theorem RS.degree_def {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] [Nonempty Y] (F : X → Y) : degree F = fiberMultSum F (Classical.arbitrary Y)

theorem RS.degree_of_forall_eq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] [Nonempty Y] (c : Y) : (degree fun (x : X) => c) = 0

Junk convention: constant maps have degree ≡ 0.

theorem RS.fiberMultSum_eq_degree {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} [ConnectedSpace Y] (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) (y : Y) : fiberMultSum F y = degree F

THE well-definedness statement in degree form: the fiber-sum over any y is the degree.

theorem RS.degree_eq_fiberMultSum {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} [ConnectedSpace Y] (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) (y : Y) : degree F = ∑ᶠ (x : X) (_ : x ∈ F ⁻¹' {y}), multiplicity F x

theorem RS.one_le_degree {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} [ConnectedSpace Y] (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) : 1 ≤ degree F

theorem RS.degree_pos_iff {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} [ConnectedSpace Y] (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) : 0 < degree F ↔ ¬∃ (c : Y), ∀ (x : X), F x = c

degree F is positive exactly when F is nonconstant.

theorem RS.multiplicity_le_degree {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} [ConnectedSpace Y] (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) (x : X) : multiplicity F x ≤ degree F

theorem RS.ncard_fiber_of_isRegularValue {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} [ConnectedSpace Y] (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) {y : Y} (hy : IsRegularValue F y) : (F ⁻¹' {y}).ncard = degree F

Fiber cardinality equals the degree over regular values (every fiber point has multiplicity exactly 1).

theorem RS.ncard_fiber_le_degree {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} [ConnectedSpace Y] (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) (y : Y) : (F ⁻¹' {y}).ncard ≤ degree F

In general (branch values included), fiber cardinality is at most the degree.

Degree 1 ⇒ bijective ⇒ homeomorphism (genus-zero-headline / Abel bank)

theorem RS.bijective_of_degree_eq_one {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} [ConnectedSpace Y] (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) (h1 : degree F = 1) : Function.Bijective F

Degree 1 forces bijectivity: surjectivity is automatic (nonconstant on connected X); injectivity fails only if some fiber has ≥ 2 points, forcing fiberMultSum ≥ 2 > 1.

noncomputable def RS.homeomorphOfDegreeEqOne {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} [ConnectedSpace Y] (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) (h1 : degree F = 1) : X ≃ₜ Y

The homeomorphism witnessed by a degree-1 map (compact source, T2 target, continuous bijection).

Equations

• RS.homeomorphOfDegreeEqOne hF hne h1 = ⋯.homeoOfEquivCompactToT2

theorem RS.coe_homeomorphOfDegreeEqOne {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} [ConnectedSpace Y] (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) (h1 : degree F = 1) : ⇑(homeomorphOfDegreeEqOne hF hne h1) = F

theorem RS.isHomeomorph_of_degree_eq_one {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} [ConnectedSpace Y] (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) (h1 : degree F = 1) : IsHomeomorph F

degree_comp (statement bank; no critical downstream consumer)

theorem RS.degree_comp {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} [ConnectedSpace Y] {Z : Type u_3} [TopologicalSpace Z] [T2Space Z] [ConnectedSpace Z] [ChartedSpace ℂ Z] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Z] [CompactSpace Y] {G : Y → Z} (hG : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ G) (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hneG : ¬∃ (c : Z), ∀ (y : Y), G y = c) (hneF : ¬∃ (c : Y), ∀ (x : X), F x = c) : degree (G ∘ F) = degree G * degree F

Degree is multiplicative under composition. The only statement in the unit needing the extra instance [CompactSpace Y] (finiteness of G's fibers).