The stack of adapted charts over a fiber (heart, part 1)

• RS.FiberStack F y₀ — the (finite) fiber over y₀ enumerated as pt : Fin n → X, pairwise-disjoint adapted charts at each fiber point, and an open V ∋ y₀ contained in every target-chart source, whose target-chart images lie in the normal-form balls and whose F-preimage is trapped in the chart sources. This is the multiplicity-aware local model of F over an arbitrary point of Y (branch value or not); Forster's 4.24-proof mechanism.
• RS.exists_fiberStack — existence over every y₀ : Y (compactness of X traps the fiber via the closed-map filter inequality IsClosedMap.comap_nhds_le; no sequences).
• Basic API: mem_fiber_pt, maps_pt_eq, mem_source_pt, radius_pos, mult_ne_zero, fiber_eq_iUnion.

LocalConstancy.lean combines this with the planar count (RootCounting.lean) to prove that fiberMultSum is locally constant.

structure RS.FiberStack {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (F : X → Y) (y₀ : Y) : Type (max u_1 u_2)

A stack of adapted charts over y₀: the (finite) fiber enumerated as pt : Fin n → X, pairwise-disjoint adapted charts at each fiber point, and an open V ∋ y₀ that is contained in every target-chart source, whose target-chart images lie in the normal-form balls, and whose F-preimage is trapped in the chart sources.

• n : ℕ

  The number of points in the fiber.

• pt : Fin self.n → X

  An enumeration of the fiber.

• pt_injective : Function.Injective self.pt
• range_pt : Set.range self.pt = F ⁻¹' {y₀}
• one_le_mult (i : Fin self.n) : 1 ≤ multiplicity F (self.pt i)
• A (i : Fin self.n) : AdaptedChartsAt F (self.pt i) (multiplicity F (self.pt i))

  Adapted charts (local normal form z ↦ z ^ k) at each fiber point.

• disjoint_sources : Pairwise (Function.onFun Disjoint fun (i : Fin self.n) => (self.A i).e.source)
• V : Set Y

  The distinguished open neighborhood of y₀.

• isOpen_V : IsOpen self.V
• mem_V : y₀ ∈ self.V
• V_subset (i : Fin self.n) : self.V ⊆ (self.A i).e'.source
• map_V_mem_ball (i : Fin self.n) (y : Y) : y ∈ self.V → ↑(self.A i).e' y ∈ Metric.ball 0 ((self.A i).radius ^ multiplicity F (self.pt i))
• preimage_V_subset : F ⁻¹' self.V ⊆ ⋃ (i : Fin self.n), (self.A i).e.source

theorem RS.FiberStack.mem_fiber_pt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {y₀ : Y} (S : FiberStack F y₀) (i : Fin S.n) : S.pt i ∈ F ⁻¹' {y₀}

theorem RS.FiberStack.maps_pt_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {y₀ : Y} (S : FiberStack F y₀) (i : Fin S.n) : F (S.pt i) = y₀

theorem RS.FiberStack.mem_source_pt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {y₀ : Y} (S : FiberStack F y₀) (i : Fin S.n) : S.pt i ∈ (S.A i).e.source

theorem RS.FiberStack.radius_pos {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {y₀ : Y} (S : FiberStack F y₀) (i : Fin S.n) : 0 < (S.A i).radius

theorem RS.FiberStack.mult_ne_zero {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {y₀ : Y} (S : FiberStack F y₀) (i : Fin S.n) : multiplicity F (S.pt i) ≠ 0

theorem RS.FiberStack.fiber_eq_iUnion {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {y₀ : Y} (S : FiberStack F y₀) {y : Y} (hy : y ∈ S.V) : F ⁻¹' {y} = ⋃ (i : Fin S.n), F ⁻¹' {y} ∩ (S.A i).e.source

The fiber over any y ∈ V decomposes along the chart sources (disjointly, by disjoint_sources).

Existence (standing surface hypotheses)

theorem RS.exists_fiberStack {X : Type u_1} [TopologicalSpace X] [T2Space 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) : Nonempty (FiberStack F y₀)

Existence of a stack of adapted charts over every point (heart, part 1; Forster 4.24-proof mechanism). Does NOT need F surjective, Y connected, nor the fiber nonempty (n = 0 is allowed).