Homotopy invariance: the 2D grid argument (CC6)

Unit: paths-and-integrals (docs/design/paths-and-integrals.md §5). A primitive of η along a continuous homotopy square exists (hand-rolled grid via mathlib's 2D Lebesgue-number lemma exists_monotone_Icc_subset_open_cover_unitInterval_prod_self), subsuming both rel-endpoint and free-loop homotopy invariance of pathIntegral.

Main declarations:

• RS.gridK H — the clamped map ℝ × ℝ → X associated to H : C(I × I, X).
• RS.GridChain H, RS.exists_gridChain — the 2D chart-ball subdivision.
• RS.exists_primitive_along_square — existence of a primitive along the (clamped) square.
• RS.pathIntegral_congr_homotopic, RS.pathIntegralQ, RS.pathIntegral_congr_freeHomotopic, RS.pathIntegral_eq_of_simplyConnected, RS.period_eq_zero_of_homotopic_refl.

The clamped map of a homotopy square

noncomputable def RS.gridK {X : Type u_1} [TopologicalSpace X] (H : C(↑unitInterval × ↑unitInterval, X)) (p : ℝ × ℝ) : X

The map ℝ × ℝ → X obtained by clamping both coordinates of H : C(I × I, X) into [0,1].

Equations

• RS.gridK H p = H (Set.projIcc 0 1 RS.gridK._proof_1 p.1, Set.projIcc 0 1 RS.gridK._proof_1 p.2)

theorem RS.continuous_gridK {X : Type u_1} [TopologicalSpace X] (H : C(↑unitInterval × ↑unitInterval, X)) : Continuous (gridK H)

The 2D chart-ball subdivision

structure RS.GridChain {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (H : C(↑unitInterval × ↑unitInterval, X)) : Type u_1

A grid subdivision of [0,1]² with chart-and-ball data adapted to H: on each cell Icc (t j) (t (j+1)) ×ˢ Icc (t k) (t (k+1)), gridK H stays inside a single chart-ball.

• m : ℕ

  The number of subdivisions in the homotopy direction.

• t : ℕ → ℝ

  The subdivision times.

• ht0 : self.t 0 = 0
• ht1 (k : ℕ) : self.m ≤ k → self.t k = 1
• mono : Monotone self.t
• e : ℕ → ℕ → OpenPartialHomeomorph X ℂ

  The chart used on each square of the grid.

• he (j k : ℕ) : self.e j k ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X
• c : ℕ → ℕ → ℂ

  The centre of each square's disc.

• r : ℕ → ℕ → ℝ

  The radius of each square's disc.

• hr (j k : ℕ) : 0 < self.r j k
• ball_subset (j k : ℕ) : Metric.ball (self.c j k) (self.r j k) ⊆ (self.e j k).target
• maps (j k : ℕ) (p : ℝ × ℝ) : p ∈ Set.Icc (self.t j) (self.t (j + 1)) ×ˢ Set.Icc (self.t k) (self.t (k + 1)) → gridK H p ∈ (self.e j k).source ∧ ↑(self.e j k) (gridK H p) ∈ Metric.ball (self.c j k) (self.r j k)

theorem RS.exists_gridChain {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (H : C(↑unitInterval × ↑unitInterval, X)) : Nonempty (GridChain H)

Product hcov/preconnectedness helpers (the only genuinely new bookkeeping vs 1D)

Row assembly (inner induction)

Column stacking (outer induction) and the square theorem

theorem RS.exists_primitive_along_square {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {H : C(↑unitInterval × ↑unitInterval, X)} (η : Form1 X) : ∃ (F : ℝ × ℝ → ℂ), IsPrimitiveAlongMap (gridK H) η F Set.univ

A primitive of η along a continuous square H : C(I × I, X) exists (along the clamped map on all of ℝ × ℝ).

Consequences: homotopy invariance of pathIntegral

theorem RS.pathIntegral_congr_homotopic {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x y : X} {γ₀ γ₁ : Path x y} (h : γ₀.Homotopic γ₁) (η : Form1 X) : pathIntegral γ₀ η = pathIntegral γ₁ η

noncomputable def RS.pathIntegralQ {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x y : X} (η : Form1 X) (q : Path.Homotopic.Quotient x y) : ℂ

Descent of the integral to homotopy classes.

Equations

• RS.pathIntegralQ η q = Quotient.liftOn q (fun (x_1 : Path x y) => RS.pathIntegral x_1 η) ⋯

@[simp]

theorem RS.pathIntegralQ_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x y : X} (γ : Path x y) (η : Form1 X) : pathIntegralQ η (Path.Homotopic.Quotient.mk γ) = pathIntegral γ η

theorem RS.pathIntegralQ_trans {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x y z : X} (p : Path.Homotopic.Quotient x y) (q : Path.Homotopic.Quotient y z) (η : Form1 X) : pathIntegralQ η (p.trans q) = pathIntegralQ η p + pathIntegralQ η q

theorem RS.pathIntegral_congr_freeHomotopic {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x₀ x₁ : X} {γ₀ : Path x₀ x₀} {γ₁ : Path x₁ x₁} (H : γ₀.Homotopy γ₁.toContinuousMap) (hloop : ∀ (s : ↑unitInterval), H (s, 0) = H (s, 1)) (η : Form1 X) : pathIntegral γ₀ η = pathIntegral γ₁ η

Free homotopy of loops (moving basepoint) preserves periods.

theorem RS.pathIntegral_eq_of_simplyConnected {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x y : X} [SimplyConnectedSpace X] (γ₀ γ₁ : Path x y) (η : Form1 X) : pathIntegral γ₀ η = pathIntegral γ₁ η

theorem RS.period_eq_zero_of_homotopic_refl {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x : X} {γ : Path x x} (h : γ.Homotopic (Path.refl x)) (η : Form1 X) : pathIntegral γ η = 0