Ramification locus, branch locus, regular values

• RS.ramificationLocus F (points with multiplicity ≥ 2), RS.branchLocus F (their images), RS.IsRegularValue F y (no ramification point in the fiber).
• Finiteness (Forster 4.23-adjacent): RS.isClosed_ramificationLocus, RS.isDiscrete_ramificationLocus, RS.ramificationLocus_finite, RS.branchLocus_finite.
• Regular values: RS.isRegularValue_iff_notMem_branchLocus, RS.multiplicity_eq_one_of_isRegularValue, cofiniteness RS.setOf_isRegularValue_mem_cofinite, density RS.dense_setOf_isRegularValue, and existence RS.exists_isRegularValue.

Definitions (minimal instances)

def RS.ramificationLocus {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (F : X → Y) : Set X

Points where F is ramified (local multiplicity ≥ 2, CC4's IsRamifiedAt).

Equations

• RS.ramificationLocus F = {x : X | RS.IsRamifiedAt F x}

def RS.branchLocus {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (F : X → Y) : Set Y

Branch values (critical values): images of ramification points.

Equations

• RS.branchLocus F = F '' RS.ramificationLocus F

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

y is a regular value iff every point of its fiber is unramified. (For holomorphic nonconstant F this is equivalent to y ∉ branchLocus F, and then every fiber point has multiplicity exactly 1.) Values NOT attained are regular (empty fiber) — harmless, since for nonconstant F every value is attained.

Equations

• RS.IsRegularValue F y = ∀ x ∈ F ⁻¹' {y}, ¬RS.IsRamifiedAt F x

theorem RS.mem_ramificationLocus_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {x : X} : x ∈ ramificationLocus F ↔ 2 ≤ multiplicity F x

theorem RS.isRegularValue_iff_notMem_branchLocus {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (F : X → Y) (y : Y) : IsRegularValue F y ↔ y ∉ branchLocus F

Pure set algebra: regular values are exactly the non-branch values.

Finiteness (standing surface hypotheses)

theorem RS.eventually_notMem_ramificationLocus {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) : ∀ᶠ (z : X) in nhdsWithin x {x}ᶜ, z ∉ ramificationLocus F

Ramification is isolated: near any point (off the point itself) F is unramified.

theorem RS.isClosed_ramificationLocus {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) : IsClosed (ramificationLocus F)

theorem RS.isDiscrete_ramificationLocus {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) : IsDiscrete (ramificationLocus F)

theorem RS.ramificationLocus_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) : (ramificationLocus F).Finite

theorem RS.branchLocus_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) : (branchLocus F).Finite

theorem RS.multiplicity_eq_one_of_isRegularValue {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} (hy : IsRegularValue F y) {x : X} (hx : F x = y) : multiplicity F x = 1

Over a regular value every fiber point has multiplicity exactly 1.

theorem RS.setOf_isRegularValue_mem_cofinite {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 | IsRegularValue F y} ∈ Filter.cofinite

Regular values are cofinite.

theorem RS.dense_setOf_isRegularValue {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) : Dense {y : Y | IsRegularValue F y}

Regular values are dense (Y is perfect and T1, so finite sets have empty interior).

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