monodromy: the open pole/zero-free locus as a Riemann surface

Unit: monodromy (docs/design/monodromy.md §4.1). Relativizes Jacobian/Path/'s per-path machinery (IsPrimitiveAlongMap, chain continuation, homotopy invariance) to an open subset s : Opens X of a Riemann surface X, at zero proof cost: mathlib gives an open submanifold of a charted space / IsManifold the same instances for free (TopologicalSpace.Opens.instChartedSpace, and the derived IsManifold instance for opens), so Path's declarations — stated for a fully generic X satisfying only [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X], no T2Space/CompactSpace/ConnectedSpace — apply to s by direct instantiation, term for term (spike-verified, scratch_mono.lean, project root).

Main declarations:

• RS.Monodromy.openLocus/openLocusOfFinite — the open locus determined by a closed/finite "bad set" (in practice a divisor support).
• RS.Monodromy.Path.liftOpenLocus — lift a path of X whose range avoids the bad set to a path in the open locus; RS.Monodromy.Path.liftOpenLocus_extend recovers γ.extend pointwise.

def RS.Monodromy.openLocus {X : Type u_1} [TopologicalSpace X] {S : Set X} (hS : IsClosed S) : TopologicalSpace.Opens X

The open locus determined by a closed "bad set" (in practice a divisor support).

Equations

• RS.Monodromy.openLocus hS = { carrier := Sᶜ, is_open' := ⋯ }

def RS.Monodromy.openLocusOfFinite {X : Type u_1} [TopologicalSpace X] [T2Space X] {S : Set X} (hS : S.Finite) : TopologicalSpace.Opens X

Finite bad sets are closed in a T2Space (Set.Finite.isClosed), hence give an open locus. The standing surface is compact, so this is the case actually used in LogContinuation.lean ((divisor f).support is finite by finite_support_divisor).

Equations

• RS.Monodromy.openLocusOfFinite hS = RS.Monodromy.openLocus ⋯

@[simp]

theorem RS.Monodromy.mem_openLocus {X : Type u_1} [TopologicalSpace X] {S : Set X} (hS : IsClosed S) {x : X} : x ∈ openLocus hS ↔ x ∉ S

@[simp]

theorem RS.Monodromy.mem_openLocusOfFinite {X : Type u_1} [TopologicalSpace X] [T2Space X] {S : Set X} (hS : S.Finite) {x : X} : x ∈ openLocusOfFinite hS ↔ x ∉ S

def RS.Monodromy.Path.liftOpenLocus {X : Type u_1} [TopologicalSpace X] {S : Set X} (hS : IsClosed S) {x y : X} (γ : Path x y) (hγ : ∀ (t : ↑unitInterval), γ t ∉ S) : Path ⟨x, ⋯⟩ ⟨y, ⋯⟩

Lift a path of X whose whole range avoids S to a path in the open locus.

Equations

• RS.Monodromy.Path.liftOpenLocus hS γ hγ = { toFun := fun (t : ↑unitInterval) => ⟨γ t, ⋯⟩, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

theorem RS.Monodromy.Path.liftOpenLocus_extend {X : Type u_1} [TopologicalSpace X] {S : Set X} (hS : IsClosed S) {x y : X} (γ : Path x y) (hγ : ∀ (t : ↑unitInterval), γ t ∉ S) (t : ℝ) : ↑((liftOpenLocus hS γ hγ).extend t) = γ.extend t

The lift's extend recovers γ.extend pointwise (needed to translate IsPrimitiveAlong facts about the lift back into statements about γ.extend, f.holoRepr, etc.).

NB: called with the fully-qualified name Path.liftOpenLocus, not dot notation — Path is a mathlib root-namespace type, so a declaration named Path.foo nested inside RS.Monodromy is not found by the dot-notation mechanism (only by ordinary name resolution, which does see it since we are inside the RS.Monodromy namespace).