Composition law and multiplicity-one criteria

• RS.multiplicityENat_comp / RS.multiplicity_comp — multiplicities multiply under composition: mult (G ∘ F) x = mult G (F x) * mult F x (the ℕ version is junk-robust thanks to ENat.toNat_mul).
• RS.multiplicityENat_comp_chart_symm (+ ℕ version) — precomposition with an admissible chart does not change the multiplicity.
• RS.multiplicity_eq_one_iff_injOn — mult = 1 iff F is injective near x; RS.exists_openPartialHomeomorph_of_multiplicity_eq_one — mult = 1 gives a local homeomorphism agreeing with F (Forster 2.5 germ); RS.isRamifiedAt_iff_not_injOn.
• RS.eventually_multiplicity_eq_one — ramification is isolated: near x (off x), mult F y = 1 (mapping-degree's "critical values are discrete" seed).

theorem RS.multiplicityENat_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [TopologicalSpace Z] [ChartedSpace ℂ Z] {G : Y → Z} {F : X → Y} {x : X} (hG : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ G (F x)) (hF : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F x) : multiplicityENat (G ∘ F) x = multiplicityENat G (F x) * multiplicityENat F x

Multiplicities multiply under composition (ℕ∞ version; honest, no junk interference).

theorem RS.multiplicity_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [TopologicalSpace Z] [ChartedSpace ℂ Z] {G : Y → Z} {F : X → Y} {x : X} (hG : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ G (F x)) (hF : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F x) : multiplicity (G ∘ F) x = multiplicity G (F x) * multiplicity F x

Multiplicities multiply under composition (ℕ version; junk-robust thanks to ENat.toNat_mul).

theorem RS.multiplicityENat_comp_chart_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {z : ℂ} (hz : z ∈ e.target) (hF : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F (↑e.symm z)) : multiplicityENat (F ∘ ↑e.symm) z = multiplicityENat F (↑e.symm z)

Behavior under precomposition with charts: reading a map through any admissible chart does not change the multiplicity. (F ∘ e.symm : ℂ → Y, multiplicity at a planar point.)

theorem RS.multiplicity_comp_chart_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {z : ℂ} (hz : z ∈ e.target) (hF : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F (↑e.symm z)) : multiplicity (F ∘ ↑e.symm) z = multiplicity F (↑e.symm z)

ℕ version of multiplicityENat_comp_chart_symm.

theorem RS.multiplicity_eq_one_iff_injOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} {x : X} (hF : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F x) (hnc : ¬Filter.EventuallyConst F (nhds x)) : multiplicity F x = 1 ↔ ∃ U ∈ nhds x, Set.InjOn F U

multiplicity = 1 ↔ local injectivity (Forster 2.5 direction of the normal form).

theorem RS.exists_openPartialHomeomorph_of_multiplicity_eq_one {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} {x : X} (hF : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F x) (hnc : ¬Filter.EventuallyConst F (nhds x)) (h1 : multiplicity F x = 1) : ∃ (h : OpenPartialHomeomorph X Y), x ∈ h.source ∧ ∀ z ∈ h.source, ↑h z = F z

multiplicity = 1 gives a local homeomorphism agreeing with F (Forster 2.5 germ).

theorem RS.isRamifiedAt_iff_not_injOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} {x : X} (hF : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F x) (hnc : ¬Filter.EventuallyConst F (nhds x)) : IsRamifiedAt F x ↔ ¬∃ U ∈ nhds x, Set.InjOn F U

theorem RS.eventually_multiplicity_eq_one {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} {x : X} (hF : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F x) (hnc : ¬Filter.EventuallyConst F (nhds x)) : ∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, multiplicity F y = 1

Ramification is isolated: nearby points are unramified (mapping-degree's "critical values are discrete" seed).