Mapping-degree basics

• RS.fiberMultSum F y — the total multiplicity of F over y (a finsum; junk 0 for constant or non-holomorphic F by CC4's junk conventions) with its Finset bridge fiberMultSum_eq_finset_sum and junk lemma fiberMultSum_of_forall_eq.
• RS.not_eventuallyConst — globally nonconstant holomorphic maps on connected surfaces are nowhere locally constant (identity theorem); THE bridge to every local-multiplicity hypothesis. RS.one_le_multiplicity_of_not_const is its multiplicity corollary.
• Fibers of nonconstant holomorphic maps on compact surfaces are closed, discrete and finite: RS.isDiscrete_fiber, RS.fiber_finite.
• Re-exports (one-import convenience for downstream): RS.isOpenMap_of_not_const', RS.surjective_of_not_const'; bounds RS.multiplicity_le_fiberMultSum, RS.one_le_fiberMultSum.

Surface perfectness ((𝓝[≠] x).NeBot) is NOT re-proved here: surfaces-and-charts already provides the instance RS.nhdsNE_neBot for any ChartedSpace ℂ space.

fiberMultSum (minimal instances)

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

Total multiplicity of F over y (the fiber-sum). Junk-free by convention: for holomorphic nonconstant F on compact X the fiber is finite and every summand is ≥ 1; for constant F all summands are junk 0 (CC4), so the value is 0.

Equations

• RS.fiberMultSum F y = ∑ᶠ (x : X) (_ : x ∈ F ⁻¹' {y}), RS.multiplicity F x

theorem RS.fiberMultSum_def {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (F : X → Y) (y : Y) : fiberMultSum F y = ∑ᶠ (x : X) (_ : x ∈ F ⁻¹' {y}), multiplicity F x

theorem RS.fiberMultSum_eq_finset_sum {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {y : Y} (hfin : (F ⁻¹' {y}).Finite) : fiberMultSum F y = ∑ x ∈ hfin.toFinset, multiplicity F x

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

Junk convention: constant maps have fiberMultSum ≡ 0 (every summand is junk 0).

Nonconstancy bridges and fibers (standing surface hypotheses)

theorem RS.not_eventuallyConst {X : Type u_1} [TopologicalSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) (x : X) : ¬Filter.EventuallyConst F (nhds x)

Globally nonconstant holomorphic maps on connected surfaces are nowhere locally constant (identity theorem). THE bridge to every local-multiplicity hypothesis.

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

Pointwise multiplicity is ≥ 1 under the global hypotheses.

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

Fibers of nonconstant holomorphic maps are discrete.

theorem RS.fiber_finite {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} (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) (y : Y) : (F ⁻¹' {y}).Finite

Fibers of nonconstant holomorphic maps on a compact surface are finite.

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

Re-export of surfaces-and-charts' open mapping theorem (one-import convenience).

theorem RS.surjective_of_not_const' {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} [PreconnectedSpace Y] (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) : Function.Surjective F

Re-export of surfaces-and-charts' surjectivity theorem (one-import convenience).

theorem RS.multiplicity_le_fiberMultSum {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} (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) {x : X} : multiplicity F x ≤ fiberMultSum F (F x)

Each local multiplicity is bounded by the fiber-sum over its own value.

theorem RS.one_le_fiberMultSum {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} [PreconnectedSpace Y] (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) (y : Y) : 1 ≤ fiberMultSum F y

Fiber-sums of nonconstant maps are positive (fibers are nonempty by surjectivity and every summand is ≥ 1).