Foundation Circle Winding Path Winding Fundamental Loop

/-- **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

/-- **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

/-- 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

/-- 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