I am trying to understand the computation π₁(S¹, 1) ≅ ℤ. Using the covering map p: ℝ → S¹ given by p(t) = e^(2π i t), I can see that each loop γ: [0,1] → S¹ based at 1 lifts uniquely to a path \tildeγ: [0,1] → ℝ with \tildeγ(0) = 0, and the winding number is \tildeγ(1) ∈ ℤ. How do we formally prove that the map Φ: π₁(S¹) → ℤ sending [γ] ↦ \tildeγ(1) is a group isomorphism? In particular, why is it well-defined and why is the concatenation of loops reflected by addition in ℤ?