Foundation Circle Winding

/-- **Lift independence.**  The displacement computed from the canonical lift
equals the endpoint difference of *any* continuous lift `Γ` of the path.  Two
lifts that agree on the same fiber differ by a constant in the deck group `2πℤ`,
so their endpoint differences coincide. -/
theorem pathDisplacement_eq (γ : C(I, SphereOne)) (Γ : C(I, ℝ))
    (hΓ : trigCirclePoint ∘ (Γ : I → ℝ) = γ) :
    pathDisplacement γ = Γ 1 - Γ 0 := by
  set Γ' := pathLift γ with hΓ'def
  -- The two lift starts lie in the same fiber, hence differ by `k • (2π)`.
  have hfib : trigCirclePoint (Γ 0) = trigCirclePoint (Γ' 0) := by
    have h1 : trigCirclePoint (Γ 0) = γ 0 := congrFun hΓ 0
    have h2 : trigCirclePoint (Γ' 0) = γ 0 := congrFun (pathLift_lifts γ) 0
    rw [h1, h2]
  obtain ⟨k, hk⟩ := (trigCirclePoint_eq_iff (Γ 0) (Γ' 0)).1 hfib
  set c : ℝ := (k : ℝ) * (2 * Real.pi) with hcdef
  -- `Γ' + c` is also a lift, and agrees with `Γ` at `0`.
  have hshift_lifts : trigCirclePoint ∘ (fun t : I => Γ' t + c) = γ := by
    funext t
    have : trigCirclePoint (Γ' t + c) = trigCirclePoint (Γ' t) :=
      trigCirclePoint_add_intMul_period (Γ' t) k
    rw [Function.comp_apply, this]
    exact congrFun (pathLift_lifts γ) t
  have hagree0 : Γ 0 = (fun t : I => Γ' t + c) 0 := by
    simp only [hcdef]; rw [hk]
  -- Lift uniqueness on the connected interval forces equality.
  have huniq : (fun t : I => Γ t) = (fun t : I => Γ' t + c) :=
    isCoveringMap_trig.eq_of_comp_eq Γ.continuous
      (Γ'.continuous.add continuous_const)
      (by rw [hΓ, hshift_lifts]) 0 hagree0
  have hone : Γ 1 = Γ' 1 + c := congrFun huniq 1
  have hzero : Γ 0 = Γ' 0 + c := congrFun huniq 0
  simp only [pathDisplacement, ← hΓ'def]
  rw [hone, hzero]; ring

/-- **Displacement of a reversed path.**  Traversing a path backwards negates its
displacement, because the canonical lift composed with `t ↦ 1 - t` lifts the
reversed path and its endpoint difference flips sign. -/
theorem pathDisplacement_reverse (γ : C(I, SphereOne)) :
    pathDisplacement (reversePath γ) = - pathDisplacement γ := by
  have hlift :
      trigCirclePoint ∘ (((pathLift γ).comp intervalReverse) : I → ℝ) = reversePath γ := by
    funext t
    show trigCirclePoint (pathLift γ (unitInterval.symm t)) = γ (unitInterval.symm t)
    exact congrFun (pathLift_lifts γ) (unitInterval.symm t)
  rw [pathDisplacement_eq (reversePath γ) ((pathLift γ).comp intervalReverse) hlift]
  show pathLift γ (unitInterval.symm 1) - pathLift γ (unitInterval.symm 0) = - pathDisplacement γ
  rw [unitInterval.symm_one, unitInterval.symm_zero]
  rw [pathDisplacement_self]
  ring

/-- **Additivity of the displacement under path concatenation.**  The
displacement of a concatenated path is the sum of the displacements.  Together
with homotopy invariance this is exactly what makes the winding number a homology
invariant: the alternating face sum of a singular `2`-simplex telescopes to `0`. -/
theorem pathDisplacement_trans {x y z : SphereOne} (γ : Path x y) (γ' : Path y z) :
    pathDisplacement ((γ.trans γ' : Path x z) : C(I, SphereOne))
      = pathDisplacement (γ : C(I, SphereOne)) + pathDisplacement (γ' : C(I, SphereOne)) := by
  obtain ⟨e, he⟩ := trigCirclePoint_surjective x
  have hpe : x = trigCirclePoint e := he.symm
  have hγ0 : (γ : C(I, SphereOne)) 0 = trigCirclePoint e := γ.source.trans hpe
  set Lγ := isCoveringMap_trig.liftPath (γ : C(I, SphereOne)) e hγ0 with hLγ
  have hLγlifts : trigCirclePoint ∘ (Lγ : I → ℝ) = (γ : C(I, SphereOne)) :=
    isCoveringMap_trig.liftPath_lifts (γ : C(I, SphereOne)) e hγ0
  have hLγ0 : Lγ 0 = e := isCoveringMap_trig.liftPath_zero (γ : C(I, SphereOne)) e hγ0
  have htrigLγ1 : trigCirclePoint (Lγ 1) = y := by
    have := congrFun hLγlifts 1
    rw [Function.comp_apply] at this
    rw [this]; exact γ.target
  have hγ'0 : (γ' : C(I, SphereOne)) 0 = trigCirclePoint (Lγ 1) := by
    rw [htrigLγ1]; exact γ'.source
  set Lγ' := isCoveringMap_trig.liftPath (γ' : C(I, SphereOne)) (Lγ 1) hγ'0 with hLγ'
  have hLγ'0 : Lγ' 0 = Lγ 1 :=
    isCoveringMap_trig.liftPath_zero (γ' : C(I, SphereOne)) (Lγ 1) hγ'0
  -- displacement of the two pieces
  have hd_γ : pathDisplacement (γ : C(I, SphereOne)) = Lγ 1 - e := by
    rw [pathDisplacement_eq (γ : C(I, SphereOne)) Lγ hLγlifts, hLγ0]
  have hd_γ' : pathDisplacement (γ' : C(I, SphereOne)) = Lγ' 1 - Lγ 1 := by
    rw [pathDisplacement_eq (γ' : C(I, SphereOne)) Lγ'
        (isCoveringMap_trig.liftPath_lifts (γ' : C(I, SphereOne)) (Lγ 1) hγ'0), hLγ'0]
  -- displacement of the concatenation, via the lift-of-concatenation theorem
  have htrans0 : ((γ.trans γ' : Path x z) : C(I, SphereOne)) 0 = trigCirclePoint e :=
    (γ.trans γ').source.trans hpe
  set Lt := isCoveringMap_trig.liftPath ((γ.trans γ' : Path x z) : C(I, SphereOne)) e htrans0
    with hLt
  have hLtlifts : trigCirclePoint ∘ (Lt : I → ℝ) = ((γ.trans γ' : Path x z) : C(I, SphereOne)) :=
    isCoveringMap_trig.liftPath_lifts ((γ.trans γ' : Path x z) : C(I, SphereOne)) e htrans0
  have hLt0 : Lt 0 = e :=
    isCoveringMap_trig.liftPath_zero ((γ.trans γ' : Path x z) : C(I, SphereOne)) e htrans0
  have hLt1 : Lt 1 = Lγ' 1 := by
    have h := DFunLike.congr_fun (isCoveringMap_trig.liftPath_trans hpe γ γ') 1
    simpa using h
  have hd_trans : pathDisplacement ((γ.trans γ' : Path x z) : C(I, SphereOne)) = Lγ' 1 - e := by
    rw [pathDisplacement_eq ((γ.trans γ' : Path x z) : C(I, SphereOne)) Lt hLtlifts, hLt0, hLt1]
  rw [hd_trans, hd_γ, hd_γ']; ring

/-- A closed path has displacement equal to an integer number of full turns. -/
theorem pathDisplacement_loop_intMul (γ : C(I, SphereOne)) (hloop : γ 1 = γ 0) :
    ∃ k : ℤ, pathDisplacement γ = (k : ℝ) * (2 * Real.pi) := by
  have hfib : trigCirclePoint (pathLift γ 1) = trigCirclePoint (pathLift γ 0) := by
    have h1 : trigCirclePoint (pathLift γ 1) = γ 1 := congrFun (pathLift_lifts γ) 1
    have h0 : trigCirclePoint (pathLift γ 0) = γ 0 := congrFun (pathLift_lifts γ) 0
    rw [h1, h0, hloop]
  obtain ⟨k, hk⟩ := (trigCirclePoint_eq_iff (pathLift γ 1) (pathLift γ 0)).1 hfib
  refine ⟨k, ?_⟩
  rw [pathDisplacement_self, hk]
  ring

/-- **The winding number of the fundamental loop is `1`.**  The winding invariant
is therefore a left inverse to the fundamental loop class on the nose: it sends
the canonical generator to `1`. -/
theorem pathWinding_fundamentalLoop : pathWinding fundamentalLoop = 1 := by
  rw [pathWinding, pathDisplacement_fundamentalLoop]
  have hpi : (2 : ℝ) * Real.pi ≠ 0 := by positivity
  field_simp

/-- A closed path in `S¹` with zero winding is homotopic rel endpoints to the
constant path at its basepoint.  The homotopy lifts the path to `ℝ`, uses zero
winding to identify the lift endpoints, and contracts the lifted path linearly
to its initial value before projecting back through the covering map. -/
theorem pathHomotopicRel_const_of_loop_winding_zero (γ : C(I, SphereOne))
    (hloop : γ 1 = γ 0) (hw : pathWinding γ = 0) :
    γ.HomotopicRel (ContinuousMap.const I (γ 0)) {0, 1} := by
  have hlift_end : pathLift γ 1 = pathLift γ 0 := by
    exact pathLift_endpoint_eq_of_winding_zero γ hw
  let Hmap : C(I × I, SphereOne) := {
    toFun p :=
      trigCirclePoint
        ((1 - ((p.1 : I) : ℝ)) * pathLift γ p.2 +
          ((p.1 : I) : ℝ) * pathLift γ 0)
    continuous_toFun := by
      exact continuous_trigCirclePoint.comp (by continuity)
  }
  let H : γ.Homotopy (ContinuousMap.const I (γ 0)) :=
    ContinuousMap.Homotopy.mk Hmap
      (by
        intro x
        change trigCirclePoint
            ((1 - (((0 : I) : I) : ℝ)) * pathLift γ x +
              (((0 : I) : I) : ℝ) * pathLift γ 0) = γ x
        simp
        exact congrFun (pathLift_lifts γ) x)
      (by
        intro x
        change trigCirclePoint
            ((1 - (((1 : I) : I) : ℝ)) * pathLift γ x +
              (((1 : I) : I) : ℝ) * pathLift γ 0) =
            (ContinuousMap.const I (γ 0)) x
        simp
        exact congrFun (pathLift_lifts γ) 0)
  refine ⟨ContinuousMap.HomotopyWith.mk H ?_⟩
  intro t x hx
  rcases hx with hx | hx
  · subst x
    change trigCirclePoint
        ((1 - ((t : I) : ℝ)) * pathLift γ 0 +
          ((t : I) : ℝ) * pathLift γ 0) = γ 0
    rw [← congrFun (pathLift_lifts γ) 0]
    congr 1
    ring
  · subst x
    change trigCirclePoint
        ((1 - ((t : I) : ℝ)) * pathLift γ 1 +
          ((t : I) : ℝ) * pathLift γ 0) = γ 1
    rw [hlift_end]
    rw [hloop]
    rw [← congrFun (pathLift_lifts γ) 0]
    congr 1
    ring