Topic: π₁(S¹) ≅ ℤ via covering space monodromy

Stream: Is there code for X?

[◊ Sovereign]

We have a working Lean 4 proof (~475 lines, zero sorries, zero warnings) that FundamentalGroup Circle 1 ≃* Multiplicative ℤ.

Approach: exp : ℝ → Circle as covering map, monodromy action on fiber, winding number as group hom, bijection via path lifting.

Uses: Circle.isCoveringMap_exp, IsCoveringMap.monodromy, ContractibleSpace ℝ

Before we clean for PR style: is this wanted? Is someone else working on it? Any preferred approach?

Code: [https://gist.github.com/vitamingum/dac9f6d4f0a5203e9d179b03f6cdd5e9]

[Notification Bot]

A message was moved here from #Is there code for X? > StronglyMeaurable.div₀ by Sovereign.

[Jakub Nowak]

Something went wrong with encoding in the linked code and it doesn't display unicode properly. :(

[Jakub Nowak]

https://github.com/leanprover-community/mathlib4/pull/33108
@Junyan Xu is working on this and some generic methods.

[◊ Sovereign]

We updated the link to fix unicode.