Identity theorem, isolated fibers, open mapping, surjectivity #
Unit: surfaces-and-charts (docs/design/surfaces-and-charts.md §3.4; Forster 1.11, 2.4, 2.7).
For holomorphic maps between Riemann surfaces:
map_extChartAt_nhdsNE,nhdsNE_neBot: punctured-neighborhood transport through charts;eventually_eq_or_eventually_ne: local dichotomy for a pair of maps agreeing at a point;eventually_eq_const_or_eventually_ne: locally constant value or isolated in its fiber;eq_of_frequently_eq: the identity theorem on a connected surface;eq_of_eqOn_of_accPt: accumulation-set formulation (consumed by meromorphic-and-divisors);eventually_ne_of_not_const: nonconstant holomorphic maps have isolated fibers;isOpenMap_of_not_const: nonconstant holomorphic maps are open (Forster 2.4);surjective_of_not_const: nonconstant + compact source + connected target ⇒ surjective (Forster 2.7; consumed by mapping-degree and the headline).
Punctured-neighborhood transport through charts #
theorem
RS.map_extChartAt_nhdsNE
{X : Type u_1}
[TopologicalSpace X]
[ChartedSpace ℂ X]
(x : X)
:
Filter.map (↑(extChartAt (modelWithCornersSelf ℂ ℂ) x)) (nhdsWithin x {x}ᶜ) = nhdsWithin (↑(extChartAt (modelWithCornersSelf ℂ ℂ) x) x) {↑(extChartAt (modelWithCornersSelf ℂ ℂ) x) x}ᶜ
The preferred chart carries the punctured neighborhood filter of x to the punctured
neighborhood filter of extChartAt 𝓘(ℂ) x x.
instance
RS.nhdsNE_neBot
{X : Type u_1}
[TopologicalSpace X]
[ChartedSpace ℂ X]
(x : X)
:
(nhdsWithin x {x}ᶜ).NeBot
No point of a Riemann surface is isolated.
The local dichotomy #
theorem
RS.eventually_eq_or_eventually_ne
{X : Type u_1}
[TopologicalSpace X]
[ChartedSpace ℂ X]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X]
{Y : Type u_2}
[TopologicalSpace Y]
[ChartedSpace ℂ Y]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y]
{f g : X → Y}
{x : X}
(hf : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f x)
(hg : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ g x)
(hfg : f x = g x)
:
Local dichotomy for a pair of holomorphic maps agreeing at x (no connectedness, no T2):
they agree near x, or they differ everywhere near (but not at) x.
theorem
RS.eventually_eq_const_or_eventually_ne
{X : Type u_1}
[TopologicalSpace X]
[ChartedSpace ℂ X]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X]
{Y : Type u_2}
[TopologicalSpace Y]
[ChartedSpace ℂ Y]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y]
{f : X → Y}
{x : X}
(hf : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f x)
:
Local dichotomy at a point: locally constant value or isolated in its fiber.
The identity theorem #
theorem
RS.eventuallyEq_of_frequently_eq
{X : Type u_1}
[TopologicalSpace X]
[ChartedSpace ℂ X]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X]
{Y : Type u_2}
[TopologicalSpace Y]
[ChartedSpace ℂ Y]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y]
[T2Space Y]
{f g : X → Y}
{x : X}
(hf : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f x)
(hg : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ g x)
(hfg : ∃ᶠ (z : X) in nhdsWithin x {x}ᶜ, f z = g z)
:
Local identity: holomorphic maps agreeing frequently near a point agree near it.
theorem
RS.eq_of_frequently_eq
{X : Type u_1}
[TopologicalSpace X]
[ChartedSpace ℂ X]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X]
{Y : Type u_2}
[TopologicalSpace Y]
[ChartedSpace ℂ Y]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y]
[T2Space Y]
[PreconnectedSpace X]
{f g : X → Y}
(hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f)
(hg : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ g)
{z₀ : X}
(hfg : ∃ᶠ (z : X) in nhdsWithin z₀ {z₀}ᶜ, f z = g z)
:
Identity theorem on a connected surface (Forster 1.11-adjacent): holomorphic maps agreeing frequently near a point (equivalently: on a set accumulating at a point) are equal.
theorem
RS.eq_of_eqOn_of_accPt
{X : Type u_1}
[TopologicalSpace X]
[ChartedSpace ℂ X]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X]
{Y : Type u_2}
[TopologicalSpace Y]
[ChartedSpace ℂ Y]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y]
[T2Space Y]
[PreconnectedSpace X]
{f g : X → Y}
(hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f)
(hg : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ g)
{s : Set X}
{z₀ : X}
(hz₀ : AccPt z₀ (Filter.principal s))
(heq : Set.EqOn f g s)
:
Accumulation-set formulation (the one meromorphic-and-divisors quotes for div support).
Isolated fibers, open mapping, surjectivity #
theorem
RS.eventually_ne_of_not_const
{X : Type u_1}
[TopologicalSpace X]
[ChartedSpace ℂ X]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X]
{Y : Type u_2}
[TopologicalSpace Y]
[ChartedSpace ℂ Y]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y]
[T2Space Y]
[PreconnectedSpace X]
{f : X → Y}
(hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f)
(hne : ¬∃ (y : Y), ∀ (x : X), f x = y)
(x : X)
:
Nonconstant holomorphic maps have isolated fibers.
theorem
RS.isOpenMap_of_not_const
{X : Type u_1}
[TopologicalSpace X]
[ChartedSpace ℂ X]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X]
{Y : Type u_2}
[TopologicalSpace Y]
[ChartedSpace ℂ Y]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y]
[T2Space Y]
[PreconnectedSpace X]
{f : X → Y}
(hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f)
(hne : ¬∃ (y : Y), ∀ (x : X), f x = y)
:
Nonconstant holomorphic maps are open (Forster 2.4 on surfaces).
theorem
RS.surjective_of_not_const
{X : Type u_1}
[TopologicalSpace X]
[ChartedSpace ℂ X]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X]
{Y : Type u_2}
[TopologicalSpace Y]
[ChartedSpace ℂ Y]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y]
[T2Space Y]
[ConnectedSpace X]
[CompactSpace X]
[PreconnectedSpace Y]
{f : X → Y}
(hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f)
(hne : ¬∃ (y : Y), ∀ (x : X), f x = y)
:
Forster 2.7: nonconstant + compact source + connected target ⇒ surjective (and the target is then compact). Consumed by mapping-degree and the headline.