Foundation Circle Covering Is Covering Map Trig Circle Point

The winding foundation

The unit circle in the plane is the set of points at distance 1 from the origin. The trigonometric parametrization sends each real number t to the point (cos t, sin t). As t runs from 0 to 2π, the point traces the circle once; as t runs on, the point keeps circling. This map is a covering map: every point on the circle has a small neighborhood whose preimage under the map is a disjoint union of open intervals, each mapped homeomorphically onto that neighborhood. Intuitively, the real line winds around the circle like thread on a spool, and locally the winding looks like a simple one-to-one correspondence.

Covering maps matter because they let topologists count winding. A loop in the circle, a path that starts and ends at the same point, can be lifted to a path in the real line. The lift's endpoint differs from its start by an integer, the winding number, which records how many times the loop went around. This integer is the basis of the first homology group of the circle, written H₁(S¹; ℤ), which is isomorphic to the integers. Without a covering map, there is no clean way to define this invariant.

The framework's machine-checked library of formal theorems proves that the trigonometric parametrization is indeed a covering map. The result, named isCoveringMap_trigCirclePoint, is a theorem in the framework's library. It is derived by transporting a known covering map, the exponential map from the real line to the circle, along a sequence of explicit equivalences: an isometry from the complex plane to the Euclidean plane, a homeomorphism onto the unit circle, and a lift into the exact topological space object. The proof uses no axioms beyond the standard logical ones and no replacements for the circle; it concerns the imported topological sphere object directly.

This theorem does not itself prove that the homology group of the circle is the integers. It provides the covering-space foundation on which that derivation rests, the invariant being defined by lifting singular simplices through this covering map. The theorem also does not claim anything about circles in other dimensions or about the trigonometric parametrization being the only covering map of the circle; it establishes that this specific map is one.

/-- **The trigonometric parametrization `t ↦ (cos t, sin t)` of the imported
`TopCat.sphere 1` object is a covering map.**  This is the covering-space
foundation for the winding / degree invariant on singular `1`-chains. -/
theorem isCoveringMap_trigCirclePoint :
    IsCoveringMap CircleParam.trigCirclePoint := by
  rw [← ulift_carrierCovering_eq_trig]
  exact isCoveringMap_carrierCovering.homeomorph_comp
    (Homeomorph.ulift (X := SphereOneCarrier)).symm

/-- The transported map is a genuine covering map of the metric circle carrier. -/
theorem isCoveringMap_carrierCovering : IsCoveringMap carrierCovering :=
  Circle.isCoveringMap_exp.homeomorph_comp circleHomeoCarrier

/-- The carrier covering, lifted into the exact `TopCat.sphere 1` object, equals
the `CircleParam` trigonometric parametrization pointwise. -/
theorem ulift_carrierCovering_eq_trig :
    (Homeomorph.ulift (X := SphereOneCarrier)).symm ∘ carrierCovering
      = CircleParam.trigCirclePoint := by
  funext t
  apply ULift.ext
  apply Subtype.ext
  exact carrierCovering_val t

/-- **The trigonometric parametrization `t ↦ (cos t, sin t)` of the imported
`TopCat.sphere 1` object is a covering map.**  This is the covering-space
foundation for the winding / degree invariant on singular `1`-chains. -/
theorem isCoveringMap_trigCirclePoint :
    IsCoveringMap CircleParam.trigCirclePoint := by
  rw [← ulift_carrierCovering_eq_trig]
  exact isCoveringMap_carrierCovering.homeomorph_comp
    (Homeomorph.ulift (X := SphereOneCarrier)).symm

What this page does not claim

This theorem does not prove that the first homology group of the circle is the integers. This theorem does not claim that the trigonometric parametrization is the only covering map of the circle. This theorem does not establish covering map properties for circles in other dimensions.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/CircleCovering.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: