pi_1 of the circle is Z

pi1_circle_mulEquiv_int

Submitter: Kim Morrison.

Notes: Computes the fundamental group of the complex unit circle.

Source: Classical theorem in algebraic topology.

Informal solution: Use winding number to identify loops in the circle up to homotopy with the integers.

theorem declaration uses `sorry`pi1_circle_mulEquiv_int :
    Nonempty (HomotopyGroup.Pi 1 Circle (1 : Circle) ≃* Multiplicative ℤ) := by⊢ Nonempty (HomotopyGroup.Pi 1 Circle 1 ≃* Multiplicative ℤ)
  sorryAll goals completed! 🐙

Solved by

Not yet solved.