IsPrimitiveAlongMap: primitives of a 1-form along a continuous map (CC6)

Unit: paths-and-integrals (docs/design/paths-and-integrals.md §2.1–2.2). One generic predicate serves paths, homotopy squares, and restrictions to subintervals/edges (via comp).

Main declarations:

• RS.IsPrimitiveAlongMap K η F s — near every a ∈ s (within s), F factors as g ∘ e ∘ K for a maximal-atlas chart e at K a and a planar local primitive g of coeffIn e η.
• Basic API: .mono, .add_const, .congr, .congr_map, .continuousOn, .comp.
• .rechart — the chart in the local-primitive data can be re-chosen to any maximal-atlas chart containing the image point (the workhorse for uniqueness/gluing/linearity/bridge).
• .sub_eq_sub — uniqueness up to a constant: two primitives along the same (continuous) map on a preconnected set differ by a constant.
• .glue — the junction argument: primitives on s₁, s₂ agreeing at a point of the (preconnected) overlap glue to a primitive on s₁ ∪ s₂, provided s₁/s₂ cover 𝓝[s₁∪s₂]-neighborhoods of every point (hcov).
• isPrimitiveAlongMap_of_ball — the constant-chart primitive g ∘ e ∘ K on a set mapped by K into a single chart-ball; the reusable "cell primitive" atom for the 1D chain induction (Continuation.lean) and the 2D grid (HomotopySquare.lean).

def RS.IsPrimitiveAlongMap {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {α : Type u_2} [TopologicalSpace α] (K : α → X) (η : Form1 X) (F : α → ℂ) (s : Set α) : Prop

F is a primitive of the 1-form η along the map K on s: near every a ∈ s (within s), F factors as g ∘ e ∘ K for a chart e at K a and a planar local primitive g of the chart coefficient of η.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.IsPrimitiveAlongMap.mono {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {α : Type u_2} [TopologicalSpace α] {K : α → X} {η : Form1 X} {F : α → ℂ} {s t : Set α} (h : IsPrimitiveAlongMap K η F s) (hts : t ⊆ s) : IsPrimitiveAlongMap K η F t

theorem RS.IsPrimitiveAlongMap.add_const {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {α : Type u_2} [TopologicalSpace α] {K : α → X} {η : Form1 X} {F : α → ℂ} {s : Set α} (h : IsPrimitiveAlongMap K η F s) (c : ℂ) : IsPrimitiveAlongMap K η (fun (a : α) => F a + c) s

theorem RS.IsPrimitiveAlongMap.congr {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {α : Type u_2} [TopologicalSpace α] {K : α → X} {η : Form1 X} {F F₁ : α → ℂ} {s : Set α} (h : IsPrimitiveAlongMap K η F s) (hFF' : Set.EqOn F F₁ s) : IsPrimitiveAlongMap K η F₁ s

theorem RS.IsPrimitiveAlongMap.congr_map {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {α : Type u_2} [TopologicalSpace α] {K : α → X} {η : Form1 X} {F : α → ℂ} {s : Set α} {K' : α → X} (h : IsPrimitiveAlongMap K η F s) (hKK' : Set.EqOn K K' s) : IsPrimitiveAlongMap K' η F s

theorem RS.IsPrimitiveAlongMap.continuousOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {α : Type u_2} [TopologicalSpace α] {K : α → X} {η : Form1 X} {F : α → ℂ} {s : Set α} (h : IsPrimitiveAlongMap K η F s) (hK : ContinuousOn K s) : ContinuousOn F s

theorem RS.IsPrimitiveAlongMap.comp {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {α : Type u_2} [TopologicalSpace α] {K : α → X} {η : Form1 X} {F : α → ℂ} {s : Set α} {β : Type u_3} [TopologicalSpace β] (h : IsPrimitiveAlongMap K η F s) {φ : β → α} {t : Set β} (hφ : ContinuousOn φ t) (hm : Set.MapsTo φ t s) : IsPrimitiveAlongMap (K ∘ φ) η (F ∘ φ) t

Composition / restriction along a continuous map of parameter spaces.

theorem RS.IsPrimitiveAlongMap.rechart {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {α : Type u_2} [TopologicalSpace α] {K : α → X} {η : Form1 X} {F : α → ℂ} {s : Set α} {a : α} (h : IsPrimitiveAlongMap K η F s) (ha : a ∈ s) (hK : ContinuousWithinAt K s a) {e' : OpenPartialHomeomorph X ℂ} (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (hKa : K a ∈ e'.source) : ∃ (g' : ℂ → ℂ), (∀ᶠ (z : ℂ) in nhds (↑e' (K a)), HasDerivAt g' (coeffIn e' η z) z) ∧ ∀ᶠ (b : α) in nhdsWithin a s, K b ∈ e'.source ∧ F b = g' (↑e' (K b))

The chart in the local-primitive data can be re-chosen to be any maximal-atlas chart containing the image point.

theorem RS.IsPrimitiveAlongMap.sub_eq_sub {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {α : Type u_2} [TopologicalSpace α] {K : α → X} {η : Form1 X} {F₁ F₂ : α → ℂ} {s : Set α} (hs : IsPreconnected s) (hK : ContinuousOn K s) (h₁ : IsPrimitiveAlongMap K η F₁ s) (h₂ : IsPrimitiveAlongMap K η F₂ s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : F₁ b - F₂ b = F₁ a - F₂ a

Uniqueness up to a constant. Chart overlaps need not be connected; primitives are only ever compared along the parameter space (never across an overlap directly).

theorem RS.IsPrimitiveAlongMap.glue {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {α : Type u_2} [TopologicalSpace α] {K : α → X} {η : Form1 X} {F₁ F₂ : α → ℂ} {s t : Set α} [(a : α) → Decidable (a ∈ s)] (hK : ContinuousOn K (s ∪ t)) (h₁ : IsPrimitiveAlongMap K η F₁ s) (h₂ : IsPrimitiveAlongMap K η F₂ t) (hL : IsPreconnected (s ∩ t)) {a₀ : α} (ha₀ : a₀ ∈ s ∩ t) (hval : F₁ a₀ = F₂ a₀) (hcov : ∀ a ∈ s ∪ t, s ∈ nhdsWithin a (s ∪ t) ∨ t ∈ nhdsWithin a (s ∪ t) ∨ a ∈ s ∩ t) : IsPrimitiveAlongMap K η (s.piecewise F₁ F₂) (s ∪ t)

The junction argument: primitives on s₁, s₂ agreeing at a point of the (preconnected) overlap glue to a primitive on s₁ ∪ s₂.

theorem RS.isPrimitiveAlongMap_of_ball {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {α : Type u_2} [TopologicalSpace α] {K : α → X} {η : Form1 X} {s : Set α} {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {c : ℂ} {r : ℝ} {g : ℂ → ℂ} (hg : ∀ z ∈ Metric.ball c r, HasDerivAt g (coeffIn e η z) z) (hmaps : ∀ a ∈ s, K a ∈ e.source ∧ ↑e (K a) ∈ Metric.ball c r) : IsPrimitiveAlongMap K η (fun (a : α) => g (↑e (K a))) s

Constant-chart primitive: if K maps all of s into a single chart e, with image inside a ball ball c r ⊆ e.target on which g is a planar primitive of coeffIn e η, then g ∘ e ∘ K is a primitive of η along K on s. Used by the 1D chain-continuation induction and the 2D grid (cell primitives).