IndisputableMonolith.Foundation.CircleWinding

   1import Mathlib.Topology.Homotopy.Lifting
   2import IndisputableMonolith.Foundation.CircleLifting
   3
   4/-!
   5# The local winding (displacement) invariant on paths in `TopCat.sphere 1`
   6
   7This module defines the winding / displacement of a path in the exact
   8`TopCat.sphere 1` object by lifting it through the covering map
   9`CircleCovering.isCoveringMap_trigCirclePoint` and measuring how far the lift
  10travels in `ℝ`.
  11
  12The central technical result is `pathDisplacement_eq`: the displacement computed
  13from the canonical (choice-based) lift agrees with the endpoint difference of
  14*any* continuous lift.  This is what makes the displacement a usable invariant:
  15it lets every later computation pick whatever explicit lift is convenient.  The
  16proof is the deck-transformation argument: two lifts of one path that start in
  17the same fiber differ by a constant element of the deck group `2πℤ`, by the
  18covering's lift-uniqueness theorem (`IsCoveringMap.eq_of_comp_eq`) and the period
  19invariance of `trigCirclePoint`.
  20
  21No axioms, `sorry`, or project-local `S¹` replacements are used.
  22-/
  23
  24namespace IndisputableMonolith
  25namespace Foundation
  26namespace CircleWinding
  27
  28open CircleParam CircleCovering CircleLifting
  29open scoped Real Topology unitInterval
  30
  31noncomputable section
  32
  33/-- Abbreviation for the carrier of the exact `TopCat.sphere 1` object. -/
  34abbrev SphereOne : Type := TopCat.sphere 1
  35
  36/-- The trigonometric covering is surjective: every point of `TopCat.sphere 1`
  37is `trigCirclePoint` of some real angle. -/
  38theorem trigCirclePoint_surjective : Function.Surjective trigCirclePoint := by
  39  intro y
  40  rw [← ulift_carrierCovering_eq_trig]
  41  obtain ⟨c, hc⟩ := (Homeomorph.ulift (X := SphereOneCarrier)).symm.surjective y
  42  obtain ⟨z, hz⟩ := circleHomeoCarrier.surjective c
  43  refine ⟨Complex.arg (z : ℂ), ?_⟩
  44  simp only [Function.comp_apply, carrierCovering]
  45  rw [Circle.exp_arg, hz, hc]
  46
  47/-- Period invariance of the covering: shifting the angle by an integer number of
  48full turns `2π` does not change the point. -/
  49theorem trigCirclePoint_add_intMul_period (x : ℝ) (k : ℤ) :
  50    trigCirclePoint (x + (k : ℝ) * (2 * Real.pi)) = trigCirclePoint x := by
  51  rw [trigCirclePoint_eq_iff]
  52  exact ⟨k, rfl⟩
  53
  54/-- A chosen real lift of the initial point of a path. -/
  55def pathLiftStart (γ : C(I, SphereOne)) : ℝ :=
  56  (trigCirclePoint_surjective (γ 0)).choose
  57
  58theorem pathLiftStart_spec (γ : C(I, SphereOne)) :
  59    trigCirclePoint (pathLiftStart γ) = γ 0 :=
  60  (trigCirclePoint_surjective (γ 0)).choose_spec
  61
  62/-- The canonical continuous lift of a path, starting at `pathLiftStart`. -/
  63def pathLift (γ : C(I, SphereOne)) : C(I, ℝ) :=
  64  isCoveringMap_trig.liftPath γ (pathLiftStart γ) (pathLiftStart_spec γ).symm
  65
  66theorem pathLift_lifts (γ : C(I, SphereOne)) :
  67    trigCirclePoint ∘ (pathLift γ) = γ :=
  68  isCoveringMap_trig.liftPath_lifts γ (pathLiftStart γ) (pathLiftStart_spec γ).symm
  69
  70theorem pathLift_zero (γ : C(I, SphereOne)) :
  71    pathLift γ 0 = pathLiftStart γ :=
  72  isCoveringMap_trig.liftPath_zero γ (pathLiftStart γ) (pathLiftStart_spec γ).symm
  73
  74/-- The displacement of a path: how far its canonical lift travels in `ℝ`. -/
  75def pathDisplacement (γ : C(I, SphereOne)) : ℝ :=
  76  pathLift γ 1 - pathLift γ 0
  77
  78/-- **Lift independence.**  The displacement computed from the canonical lift
  79equals the endpoint difference of *any* continuous lift `Γ` of the path.  Two
  80lifts that agree on the same fiber differ by a constant in the deck group `2πℤ`,
  81so their endpoint differences coincide. -/
  82theorem pathDisplacement_eq (γ : C(I, SphereOne)) (Γ : C(I, ℝ))
  83    (hΓ : trigCirclePoint ∘ (Γ : I → ℝ) = γ) :
  84    pathDisplacement γ = Γ 1 - Γ 0 := by
  85  set Γ' := pathLift γ with hΓ'def
  86  -- The two lift starts lie in the same fiber, hence differ by `k • (2π)`.
  87  have hfib : trigCirclePoint (Γ 0) = trigCirclePoint (Γ' 0) := by
  88    have h1 : trigCirclePoint (Γ 0) = γ 0 := congrFun hΓ 0
  89    have h2 : trigCirclePoint (Γ' 0) = γ 0 := congrFun (pathLift_lifts γ) 0
  90    rw [h1, h2]
  91  obtain ⟨k, hk⟩ := (trigCirclePoint_eq_iff (Γ 0) (Γ' 0)).1 hfib
  92  set c : ℝ := (k : ℝ) * (2 * Real.pi) with hcdef
  93  -- `Γ' + c` is also a lift, and agrees with `Γ` at `0`.
  94  have hshift_lifts : trigCirclePoint ∘ (fun t : I => Γ' t + c) = γ := by
  95    funext t
  96    have : trigCirclePoint (Γ' t + c) = trigCirclePoint (Γ' t) :=
  97      trigCirclePoint_add_intMul_period (Γ' t) k
  98    rw [Function.comp_apply, this]
  99    exact congrFun (pathLift_lifts γ) t
 100  have hagree0 : Γ 0 = (fun t : I => Γ' t + c) 0 := by
 101    simp only [hcdef]; rw [hk]
 102  -- Lift uniqueness on the connected interval forces equality.
 103  have huniq : (fun t : I => Γ t) = (fun t : I => Γ' t + c) :=
 104    isCoveringMap_trig.eq_of_comp_eq Γ.continuous
 105      (Γ'.continuous.add continuous_const)
 106      (by rw [hΓ, hshift_lifts]) 0 hagree0
 107  have hone : Γ 1 = Γ' 1 + c := congrFun huniq 1
 108  have hzero : Γ 0 = Γ' 0 + c := congrFun huniq 0
 109  simp only [pathDisplacement, ← hΓ'def]
 110  rw [hone, hzero]; ring
 111
 112/-- The displacement of the canonical lift is exactly its own endpoint
 113difference (the defining special case of `pathDisplacement_eq`). -/
 114theorem pathDisplacement_self (γ : C(I, SphereOne)) :
 115    pathDisplacement γ = pathLift γ 1 - pathLift γ 0 := rfl
 116
 117/-- The unit-interval reversal `t ↦ 1 - t` as a continuous self-map. -/
 118def intervalReverse : C(I, I) := ⟨unitInterval.symm, unitInterval.continuous_symm⟩
 119
 120/-- The reverse of a path in `S¹`, reparameterised by `t ↦ 1 - t`. -/
 121def reversePath (γ : C(I, SphereOne)) : C(I, SphereOne) := γ.comp intervalReverse
 122
 123@[simp] theorem reversePath_apply (γ : C(I, SphereOne)) (t : I) :
 124    reversePath γ t = γ (unitInterval.symm t) := rfl
 125
 126/-- **Displacement of a reversed path.**  Traversing a path backwards negates its
 127displacement, because the canonical lift composed with `t ↦ 1 - t` lifts the
 128reversed path and its endpoint difference flips sign. -/
 129theorem pathDisplacement_reverse (γ : C(I, SphereOne)) :
 130    pathDisplacement (reversePath γ) = - pathDisplacement γ := by
 131  have hlift :
 132      trigCirclePoint ∘ (((pathLift γ).comp intervalReverse) : I → ℝ) = reversePath γ := by
 133    funext t
 134    show trigCirclePoint (pathLift γ (unitInterval.symm t)) = γ (unitInterval.symm t)
 135    exact congrFun (pathLift_lifts γ) (unitInterval.symm t)
 136  rw [pathDisplacement_eq (reversePath γ) ((pathLift γ).comp intervalReverse) hlift]
 137  show pathLift γ (unitInterval.symm 1) - pathLift γ (unitInterval.symm 0) = - pathDisplacement γ
 138  rw [unitInterval.symm_one, unitInterval.symm_zero]
 139  rw [pathDisplacement_self]
 140  ring
 141
 142/-- Paths homotopic relative to their endpoints share their initial point. -/
 143theorem homotopicRel_apply_zero {γ δ : C(I, SphereOne)}
 144    (h : γ.HomotopicRel δ {0, 1}) : γ 0 = δ 0 := by
 145  obtain ⟨H⟩ := h
 146  have hmem : (0 : I) ∈ ({0, 1} : Set I) := by left; rfl
 147  rw [← H.eq_fst 1 hmem, H.apply_one 0]
 148
 149/-- **Homotopy invariance of the displacement.**  If two paths are homotopic
 150relative to their endpoints, they have the same displacement.  This is the core
 151mechanism by which the winding invariant kills boundaries: the boundary loop of a
 152singular `2`-simplex is null-homotopic in the contractible standard simplex, so
 153its displacement vanishes. -/
 154theorem pathDisplacement_homotopic {γ δ : C(I, SphereOne)}
 155    (h : γ.HomotopicRel δ {0, 1}) : pathDisplacement γ = pathDisplacement δ := by
 156  have hend : γ 0 = δ 0 := homotopicRel_apply_zero h
 157  have he_γ : γ 0 = trigCirclePoint (pathLiftStart γ) := (pathLiftStart_spec γ).symm
 158  have he_δ : δ 0 = trigCirclePoint (pathLiftStart γ) := by rw [← hend]; exact he_γ
 159  have key : isCoveringMap_trig.liftPath γ (pathLiftStart γ) he_γ 1
 160      = isCoveringMap_trig.liftPath δ (pathLiftStart γ) he_δ 1 :=
 161    isCoveringMap_trig.liftPath_apply_one_eq_of_homotopicRel h (pathLiftStart γ) he_γ he_δ
 162  have dγ : pathDisplacement γ
 163      = isCoveringMap_trig.liftPath γ (pathLiftStart γ) he_γ 1 - pathLiftStart γ := by
 164    rw [pathDisplacement_eq γ (isCoveringMap_trig.liftPath γ (pathLiftStart γ) he_γ)
 165        (isCoveringMap_trig.liftPath_lifts γ (pathLiftStart γ) he_γ),
 166      isCoveringMap_trig.liftPath_zero γ (pathLiftStart γ) he_γ]
 167  have dδ : pathDisplacement δ
 168      = isCoveringMap_trig.liftPath δ (pathLiftStart γ) he_δ 1 - pathLiftStart γ := by
 169    rw [pathDisplacement_eq δ (isCoveringMap_trig.liftPath δ (pathLiftStart γ) he_δ)
 170        (isCoveringMap_trig.liftPath_lifts δ (pathLiftStart γ) he_δ),
 171      isCoveringMap_trig.liftPath_zero δ (pathLiftStart γ) he_δ]
 172  rw [dγ, dδ, key]
 173
 174/-- **Additivity of the displacement under path concatenation.**  The
 175displacement of a concatenated path is the sum of the displacements.  Together
 176with homotopy invariance this is exactly what makes the winding number a homology
 177invariant: the alternating face sum of a singular `2`-simplex telescopes to `0`. -/
 178theorem pathDisplacement_trans {x y z : SphereOne} (γ : Path x y) (γ' : Path y z) :
 179    pathDisplacement ((γ.trans γ' : Path x z) : C(I, SphereOne))
 180      = pathDisplacement (γ : C(I, SphereOne)) + pathDisplacement (γ' : C(I, SphereOne)) := by
 181  obtain ⟨e, he⟩ := trigCirclePoint_surjective x
 182  have hpe : x = trigCirclePoint e := he.symm
 183  have hγ0 : (γ : C(I, SphereOne)) 0 = trigCirclePoint e := γ.source.trans hpe
 184  set Lγ := isCoveringMap_trig.liftPath (γ : C(I, SphereOne)) e hγ0 with hLγ
 185  have hLγlifts : trigCirclePoint ∘ (Lγ : I → ℝ) = (γ : C(I, SphereOne)) :=
 186    isCoveringMap_trig.liftPath_lifts (γ : C(I, SphereOne)) e hγ0
 187  have hLγ0 : Lγ 0 = e := isCoveringMap_trig.liftPath_zero (γ : C(I, SphereOne)) e hγ0
 188  have htrigLγ1 : trigCirclePoint (Lγ 1) = y := by
 189    have := congrFun hLγlifts 1
 190    rw [Function.comp_apply] at this
 191    rw [this]; exact γ.target
 192  have hγ'0 : (γ' : C(I, SphereOne)) 0 = trigCirclePoint (Lγ 1) := by
 193    rw [htrigLγ1]; exact γ'.source
 194  set Lγ' := isCoveringMap_trig.liftPath (γ' : C(I, SphereOne)) (Lγ 1) hγ'0 with hLγ'
 195  have hLγ'0 : Lγ' 0 = Lγ 1 :=
 196    isCoveringMap_trig.liftPath_zero (γ' : C(I, SphereOne)) (Lγ 1) hγ'0
 197  -- displacement of the two pieces
 198  have hd_γ : pathDisplacement (γ : C(I, SphereOne)) = Lγ 1 - e := by
 199    rw [pathDisplacement_eq (γ : C(I, SphereOne)) Lγ hLγlifts, hLγ0]
 200  have hd_γ' : pathDisplacement (γ' : C(I, SphereOne)) = Lγ' 1 - Lγ 1 := by
 201    rw [pathDisplacement_eq (γ' : C(I, SphereOne)) Lγ'
 202        (isCoveringMap_trig.liftPath_lifts (γ' : C(I, SphereOne)) (Lγ 1) hγ'0), hLγ'0]
 203  -- displacement of the concatenation, via the lift-of-concatenation theorem
 204  have htrans0 : ((γ.trans γ' : Path x z) : C(I, SphereOne)) 0 = trigCirclePoint e :=
 205    (γ.trans γ').source.trans hpe
 206  set Lt := isCoveringMap_trig.liftPath ((γ.trans γ' : Path x z) : C(I, SphereOne)) e htrans0
 207    with hLt
 208  have hLtlifts : trigCirclePoint ∘ (Lt : I → ℝ) = ((γ.trans γ' : Path x z) : C(I, SphereOne)) :=
 209    isCoveringMap_trig.liftPath_lifts ((γ.trans γ' : Path x z) : C(I, SphereOne)) e htrans0
 210  have hLt0 : Lt 0 = e :=
 211    isCoveringMap_trig.liftPath_zero ((γ.trans γ' : Path x z) : C(I, SphereOne)) e htrans0
 212  have hLt1 : Lt 1 = Lγ' 1 := by
 213    have h := DFunLike.congr_fun (isCoveringMap_trig.liftPath_trans hpe γ γ') 1
 214    simpa using h
 215  have hd_trans : pathDisplacement ((γ.trans γ' : Path x z) : C(I, SphereOne)) = Lγ' 1 - e := by
 216    rw [pathDisplacement_eq ((γ.trans γ' : Path x z) : C(I, SphereOne)) Lt hLtlifts, hLt0, hLt1]
 217  rw [hd_trans, hd_γ, hd_γ']; ring
 218
 219/-- The winding number of a path: displacement normalized by one full turn. -/
 220def pathWinding (γ : C(I, SphereOne)) : ℝ :=
 221  pathDisplacement γ / (2 * Real.pi)
 222
 223/-- A closed path has displacement equal to an integer number of full turns. -/
 224theorem pathDisplacement_loop_intMul (γ : C(I, SphereOne)) (hloop : γ 1 = γ 0) :
 225    ∃ k : ℤ, pathDisplacement γ = (k : ℝ) * (2 * Real.pi) := by
 226  have hfib : trigCirclePoint (pathLift γ 1) = trigCirclePoint (pathLift γ 0) := by
 227    have h1 : trigCirclePoint (pathLift γ 1) = γ 1 := congrFun (pathLift_lifts γ) 1
 228    have h0 : trigCirclePoint (pathLift γ 0) = γ 0 := congrFun (pathLift_lifts γ) 0
 229    rw [h1, h0, hloop]
 230  obtain ⟨k, hk⟩ := (trigCirclePoint_eq_iff (pathLift γ 1) (pathLift γ 0)).1 hfib
 231  refine ⟨k, ?_⟩
 232  rw [pathDisplacement_self, hk]
 233  ring
 234
 235/-- A closed path has integer winding. -/
 236theorem pathWinding_loop_integral (γ : C(I, SphereOne)) (hloop : γ 1 = γ 0) :
 237    ∃ k : ℤ, pathWinding γ = (k : ℝ) := by
 238  obtain ⟨k, hk⟩ := pathDisplacement_loop_intMul γ hloop
 239  refine ⟨k, ?_⟩
 240  rw [pathWinding, hk]
 241  have hpi : (2 : ℝ) * Real.pi ≠ 0 := by positivity
 242  field_simp [hpi]
 243
 244/-- The fundamental once-around loop, as a path `I → TopCat.sphere 1`. -/
 245def fundamentalLoop : C(I, SphereOne) where
 246  toFun t := trigCirclePoint (2 * Real.pi * (t : ℝ))
 247  continuous_toFun :=
 248    continuous_trigCirclePoint.comp (continuous_const.mul continuous_subtype_val)
 249
 250/-- The explicit linear lift `t ↦ 2π t` of the fundamental loop. -/
 251def fundamentalLift : C(I, ℝ) where
 252  toFun t := 2 * Real.pi * (t : ℝ)
 253  continuous_toFun := continuous_const.mul continuous_subtype_val
 254
 255theorem fundamentalLift_lifts :
 256    trigCirclePoint ∘ (fundamentalLift : I → ℝ) = fundamentalLoop := rfl
 257
 258/-- **The displacement of the fundamental loop is one full turn `2π`.**  This is
 259the surjectivity witness for the winding invariant: the canonical generator maps
 260to a nonzero value. -/
 261theorem pathDisplacement_fundamentalLoop :
 262    pathDisplacement fundamentalLoop = 2 * Real.pi := by
 263  rw [pathDisplacement_eq fundamentalLoop fundamentalLift fundamentalLift_lifts]
 264  show 2 * Real.pi * ((1 : I) : ℝ) - 2 * Real.pi * ((0 : I) : ℝ) = 2 * Real.pi
 265  simp
 266
 267/-- **The winding number of the fundamental loop is `1`.**  The winding invariant
 268is therefore a left inverse to the fundamental loop class on the nose: it sends
 269the canonical generator to `1`. -/
 270theorem pathWinding_fundamentalLoop : pathWinding fundamentalLoop = 1 := by
 271  rw [pathWinding, pathDisplacement_fundamentalLoop]
 272  have hpi : (2 : ℝ) * Real.pi ≠ 0 := by positivity
 273  field_simp
 274
 275/-- Zero winding forces the canonical lift endpoints to agree.  This is the
 276lift-level form consumed by the singular cone construction in
 277`CircleWindingChain`. -/
 278theorem pathLift_endpoint_eq_of_winding_zero (γ : C(I, SphereOne))
 279    (hw : pathWinding γ = 0) :
 280    pathLift γ 1 = pathLift γ 0 := by
 281  have hdisp : pathDisplacement γ = 0 := by
 282    unfold pathWinding at hw
 283    have hpi : (2 : ℝ) * Real.pi ≠ 0 := by positivity
 284    rcases (div_eq_zero_iff).mp hw with hzero | hden
 285    · exact hzero
 286    · exact False.elim (hpi hden)
 287  rw [pathDisplacement_self] at hdisp
 288  linarith
 289
 290/-- The canonical lift of any interval path is uniformly bounded.  This compactness
 291fact is the analytic input needed for the apex continuity of the singular cone. -/
 292theorem pathLift_exists_norm_bound (γ : C(I, SphereOne)) :
 293    ∃ C : ℝ, ∀ t : I, ‖pathLift γ t‖ ≤ C := by
 294  obtain ⟨C, hC⟩ := isCompact_univ.exists_bound_of_continuousOn
 295    (s := (Set.univ : Set I)) (f := fun t : I => pathLift γ t)
 296    (by exact (pathLift γ).continuous.continuousOn)
 297  refine ⟨C, ?_⟩
 298  intro t
 299  exact hC t (by simp)
 300
 301/-- The canonical lift, shifted by its initial value, is uniformly bounded.  This
 302is the exact bound consumed by the cone formula
 303`L₀ + (1 - x₂) * (L(coneBaseParam x) - L₀)`. -/
 304theorem pathLift_shifted_exists_norm_bound (γ : C(I, SphereOne)) :
 305    ∃ C : ℝ, ∀ t : I, ‖pathLift γ t - pathLift γ 0‖ ≤ C := by
 306  obtain ⟨C, hC⟩ := isCompact_univ.exists_bound_of_continuousOn
 307    (s := (Set.univ : Set I)) (f := fun t : I => pathLift γ t - pathLift γ 0)
 308    (by exact ((pathLift γ).continuous.sub continuous_const).continuousOn)
 309  refine ⟨C, ?_⟩
 310  intro t
 311  exact hC t (by simp)
 312
 313/-- A closed path in `S¹` with zero winding is homotopic rel endpoints to the
 314constant path at its basepoint.  The homotopy lifts the path to `ℝ`, uses zero
 315winding to identify the lift endpoints, and contracts the lifted path linearly
 316to its initial value before projecting back through the covering map. -/
 317theorem pathHomotopicRel_const_of_loop_winding_zero (γ : C(I, SphereOne))
 318    (hloop : γ 1 = γ 0) (hw : pathWinding γ = 0) :
 319    γ.HomotopicRel (ContinuousMap.const I (γ 0)) {0, 1} := by
 320  have hlift_end : pathLift γ 1 = pathLift γ 0 := by
 321    exact pathLift_endpoint_eq_of_winding_zero γ hw
 322  let Hmap : C(I × I, SphereOne) := {
 323    toFun p :=
 324      trigCirclePoint
 325        ((1 - ((p.1 : I) : ℝ)) * pathLift γ p.2 +
 326          ((p.1 : I) : ℝ) * pathLift γ 0)
 327    continuous_toFun := by
 328      exact continuous_trigCirclePoint.comp (by continuity)
 329  }
 330  let H : γ.Homotopy (ContinuousMap.const I (γ 0)) :=
 331    ContinuousMap.Homotopy.mk Hmap
 332      (by
 333        intro x
 334        change trigCirclePoint
 335            ((1 - (((0 : I) : I) : ℝ)) * pathLift γ x +
 336              (((0 : I) : I) : ℝ) * pathLift γ 0) = γ x
 337        simp
 338        exact congrFun (pathLift_lifts γ) x)
 339      (by
 340        intro x
 341        change trigCirclePoint
 342            ((1 - (((1 : I) : I) : ℝ)) * pathLift γ x +
 343              (((1 : I) : I) : ℝ) * pathLift γ 0) =
 344            (ContinuousMap.const I (γ 0)) x
 345        simp
 346        exact congrFun (pathLift_lifts γ) 0)
 347  refine ⟨ContinuousMap.HomotopyWith.mk H ?_⟩
 348  intro t x hx
 349  rcases hx with hx | hx
 350  · subst x
 351    change trigCirclePoint
 352        ((1 - ((t : I) : ℝ)) * pathLift γ 0 +
 353          ((t : I) : ℝ) * pathLift γ 0) = γ 0
 354    rw [← congrFun (pathLift_lifts γ) 0]
 355    congr 1
 356    ring
 357  · subst x
 358    change trigCirclePoint
 359        ((1 - ((t : I) : ℝ)) * pathLift γ 1 +
 360          ((t : I) : ℝ) * pathLift γ 0) = γ 1
 361    rw [hlift_end]
 362    rw [hloop]
 363    rw [← congrFun (pathLift_lifts γ) 0]
 364    congr 1
 365    ring
 366
 367end
 368
 369end CircleWinding
 370end Foundation
 371end IndisputableMonolith
 372