IndisputableMonolith.Foundation.CircleCovering

   1import Mathlib.Analysis.SpecialFunctions.Complex.Circle
   2import Mathlib.Analysis.InnerProductSpace.PiL2
   3import Mathlib.Topology.Covering.Basic
   4import IndisputableMonolith.Foundation.CircleParam
   5
   6/-!
   7# The trigonometric parametrization of `TopCat.sphere 1` is a covering map
   8
   9This module supplies the covering-space foundation for the by-hand circle-`H₁`
  10derivation.  Mathlib's singular-homology development (`SingularHomology/Basic`)
  11proves nothing beyond the totally-disconnected case, so every route to
  12`H₁(S¹; ℤ) ≅ ℤ` must build its own degree / winding invariant, and the invariant
  13is defined by lifting singular simplices through a covering map of
  14`TopCat.sphere 1`.
  15
  16The headline result is `isCoveringMap_trigCirclePoint`: the concrete map
  17`t ↦ (cos t, sin t)` already used by `CircleParam` and the fundamental simplex is
  18an honest covering map.  It is obtained by transporting Mathlib's
  19`Circle.isCoveringMap_exp` along
  20
  21* the orthonormal-basis isometry `ℂ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 2)`
  22  (sending `Circle` to the metric unit circle), and
  23* the `ULift` homeomorphism into the exact `TopCat.sphere 1` carrier.
  24
  25No axioms, `sorry`, or project-local replacements for `S¹` are used: the result
  26is about the imported `TopCat.sphere 1` object via real Lean equivalences.
  27-/
  28
  29namespace IndisputableMonolith
  30namespace Foundation
  31namespace CircleCovering
  32
  33open Complex CircleParam
  34
  35noncomputable section
  36
  37/-- The orthonormal-basis isometry `ℂ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 2)`. -/
  38def isoE : ℂ ≃ₗᵢ[ℝ] SphereOneAmbient :=
  39  Complex.orthonormalBasisOneI.repr
  40
  41/-- The induced homeomorphism from Mathlib's `Circle` onto the exact metric
  42unit-circle carrier of `TopCat.sphere 1`. -/
  43def circleHomeoCarrier : Circle ≃ₜ SphereOneCarrier :=
  44  Homeomorph.subtype isoE.toHomeomorph (fun z => by
  45    show z ∈ Metric.sphere (0 : ℂ) 1 ↔
  46        (isoE.toHomeomorph z) ∈ Metric.sphere (0 : SphereOneAmbient) 1
  47    simp only [Metric.mem_sphere, dist_zero_right, LinearIsometryEquiv.coe_toHomeomorph,
  48      LinearIsometryEquiv.norm_map])
  49
  50/-- The covering map `ℝ → SphereOneCarrier`, transported from `Circle.exp`. -/
  51def carrierCovering : ℝ → SphereOneCarrier :=
  52  circleHomeoCarrier ∘ Circle.exp
  53
  54/-- The transported map is a genuine covering map of the metric circle carrier. -/
  55theorem isCoveringMap_carrierCovering : IsCoveringMap carrierCovering :=
  56  Circle.isCoveringMap_exp.homeomorph_comp circleHomeoCarrier
  57
  58/-- The carrier covering agrees with the ambient trigonometric vector
  59`(cos t, sin t)`. -/
  60theorem carrierCovering_val (t : ℝ) :
  61    (carrierCovering t : SphereOneAmbient) = trigCircleVector t := by
  62  show isoE (Circle.exp t : ℂ) = trigCircleVector t
  63  rw [show (Circle.exp t : ℂ) = Complex.exp (t * Complex.I) from Circle.coe_exp t,
  64      show isoE (Complex.exp (t * Complex.I))
  65        = Complex.orthonormalBasisOneI.repr (Complex.exp (t * Complex.I)) from rfl]
  66  ext i
  67  rw [Complex.orthonormalBasisOneI_repr_apply]
  68  fin_cases i
  69  · simp [trigCircleVector, Complex.exp_ofReal_mul_I_re]
  70  · simp [trigCircleVector, Complex.exp_ofReal_mul_I_im]
  71
  72/-- The carrier covering, lifted into the exact `TopCat.sphere 1` object, equals
  73the `CircleParam` trigonometric parametrization pointwise. -/
  74theorem ulift_carrierCovering_eq_trig :
  75    (Homeomorph.ulift (X := SphereOneCarrier)).symm ∘ carrierCovering
  76      = CircleParam.trigCirclePoint := by
  77  funext t
  78  apply ULift.ext
  79  apply Subtype.ext
  80  exact carrierCovering_val t
  81
  82/-- **The trigonometric parametrization `t ↦ (cos t, sin t)` of the imported
  83`TopCat.sphere 1` object is a covering map.**  This is the covering-space
  84foundation for the winding / degree invariant on singular `1`-chains. -/
  85theorem isCoveringMap_trigCirclePoint :
  86    IsCoveringMap CircleParam.trigCirclePoint := by
  87  rw [← ulift_carrierCovering_eq_trig]
  88  exact isCoveringMap_carrierCovering.homeomorph_comp
  89    (Homeomorph.ulift (X := SphereOneCarrier)).symm
  90
  91end
  92
  93end CircleCovering
  94end Foundation
  95end IndisputableMonolith
  96