IndisputableMonolith.Foundation.CircleLifting

   1import Mathlib.Analysis.Convex.Contractible
   2import Mathlib.Analysis.Convex.StdSimplex
   3import Mathlib.Topology.Homotopy.Lifting
   4import IndisputableMonolith.Foundation.CircleCovering
   5
   6/-!
   7# Lifting prerequisites for the circle winding invariant
   8
   9The winding / degree invariant on singular `1`-chains of `TopCat.sphere 1` is
  10built by lifting singular simplices through the covering map
  11`CircleCovering.isCoveringMap_trigCirclePoint`.  Two ingredients are needed and
  12established here, both about the *exact imported* objects:
  13
  14* **Simplex contractibility.**  The realization domain of an `n`-simplex is the
  15  topological standard simplex `stdSimplex ℝ (Fin (n+1))`, a nonempty convex set,
  16  hence contractible and (therefore) simply connected.  Mathlib's path-lifting
  17  monodromy invariance (`IsCoveringMap.liftPath_apply_one_eq_of_homotopicRel`)
  18  combined with `SimplyConnectedSpace.paths_homotopic` is what makes the winding
  19  number kill boundaries, so we register the contractibility instance once here.
  20
  21* **Fiber structure of the covering.**  `trigCirclePoint a = trigCirclePoint b`
  22  iff `a` and `b` differ by an integer multiple of the period `2π`.  This is the
  23  deck-transformation description of the fiber and is the algebraic heart of both
  24  the well-definedness of the winding number and the value `w(fundamental) = 1`.
  25
  26No axioms, `sorry`, or project-local `S¹` replacements are used.
  27-/
  28
  29namespace IndisputableMonolith
  30namespace Foundation
  31namespace CircleLifting
  32
  33open Complex CircleParam CircleCovering
  34open scoped Real
  35
  36noncomputable section
  37
  38/-- The topological standard `n`-simplex (the realization domain of a singular
  39`(n-1)`-simplex) is contractible: it is a nonempty convex set. -/
  40instance stdSimplex_contractibleSpace (n : ℕ) [NeZero n] :
  41    ContractibleSpace (stdSimplex ℝ (Fin n)) :=
  42  (convex_stdSimplex ℝ (Fin n)).contractibleSpace
  43    ⟨_, single_mem_stdSimplex ℝ (0 : Fin n)⟩
  44
  45/-- Consequently the standard simplex is simply connected; this is the precise
  46hypothesis consumed by the path-lifting monodromy invariance used to show the
  47winding number kills boundaries.  (Stated explicitly for discoverability; it is
  48also available by instance resolution.) -/
  49theorem stdSimplex_simplyConnectedSpace (n : ℕ) [NeZero n] :
  50    SimplyConnectedSpace (stdSimplex ℝ (Fin n)) :=
  51  inferInstance
  52
  53/-- Two real parameters hit the same point of `TopCat.sphere 1` under the
  54trigonometric covering iff they have the same `Circle.exp`. -/
  55theorem trigCirclePoint_eq_iff_exp (a b : ℝ) :
  56    trigCirclePoint a = trigCirclePoint b ↔ Circle.exp a = Circle.exp b := by
  57  rw [← ulift_carrierCovering_eq_trig]
  58  simp only [Function.comp_apply, carrierCovering]
  59  refine ⟨fun h => ?_, fun h => ?_⟩
  60  · exact circleHomeoCarrier.injective (Homeomorph.ulift.symm.injective h)
  61  · rw [h]
  62
  63/-- **Fiber of the trigonometric covering.**  `trigCirclePoint a = trigCirclePoint b`
  64exactly when `a` and `b` differ by an integer number of full turns `2π`.  This is
  65the deck-transformation group `2π ℤ` of the universal cover `ℝ → S¹`. -/
  66theorem trigCirclePoint_eq_iff (a b : ℝ) :
  67    trigCirclePoint a = trigCirclePoint b ↔ ∃ m : ℤ, a = b + (m : ℝ) * (2 * Real.pi) := by
  68  rw [trigCirclePoint_eq_iff_exp, Circle.exp_eq_exp]
  69
  70/-- The covering map of `TopCat.sphere 1`, repackaged as an
  71`IsCoveringMap` term for direct use with the path-lifting API. -/
  72theorem isCoveringMap_trig : IsCoveringMap CircleParam.trigCirclePoint :=
  73  isCoveringMap_trigCirclePoint
  74
  75end
  76
  77end CircleLifting
  78end Foundation
  79end IndisputableMonolith
  80