IndisputableMonolith.Foundation.CircleParam

   1import Mathlib.Topology.Category.TopCat.Sphere
   2import Mathlib.AlgebraicTopology.SingularSet
   3import Mathlib.Analysis.InnerProductSpace.PiL2
   4import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
   5
   6/-!
   7# Circle Parametrization Primitives
   8
   9This module starts the by-hand circle-H1 derivation against the actual imported
  10`TopCat.sphere 1` object.  It establishes the exact carrier, a checked
  11basepoint, and the constant singular 1-simplex face identities in
  12`TopCat.toSSet.obj (TopCat.sphere 1)`.
  13
  14The constant simplex is not the fundamental generator.  It is the first API
  15anchor: all later once-around simplices should live in this same singular
  16simplicial set and use the same face maps.
  17-/
  18
  19namespace IndisputableMonolith
  20namespace Foundation
  21namespace CircleParam
  22
  23open CategoryTheory Opposite
  24
  25noncomputable section
  26
  27/-- The exact ambient Euclidean space for Mathlib's `TopCat.sphere 1`. -/
  28abbrev SphereOneAmbient : Type :=
  29  EuclideanSpace ℝ (Fin 2)
  30
  31/-- The exact metric-sphere carrier under the `ULift` in `TopCat.sphere 1`. -/
  32abbrev SphereOneCarrier : Type :=
  33  Metric.sphere (0 : SphereOneAmbient) 1
  34
  35/-- The first coordinate unit vector in the ambient Euclidean plane. -/
  36def sphereOneBaseVector : SphereOneAmbient :=
  37  EuclideanSpace.single (0 : Fin 2) (1 : ℝ)
  38
  39/-- The first coordinate unit vector lies on Mathlib's unit circle. -/
  40theorem sphereOneBaseVector_mem_sphere :
  41    sphereOneBaseVector ∈ Metric.sphere (0 : SphereOneAmbient) 1 := by
  42  change dist (EuclideanSpace.single (0 : Fin 2) (1 : ℝ) : SphereOneAmbient) 0 = 1
  43  simp
  44
  45/-- Basepoint of the exact `TopCat.sphere 1` object. -/
  46def sphereOneBasepoint : TopCat.sphere 1 :=
  47  ULift.up ⟨sphereOneBaseVector, sphereOneBaseVector_mem_sphere⟩
  48
  49/-- The ambient Euclidean vector `(cos t, sin t)`. -/
  50def trigCircleVector (t : ℝ) : SphereOneAmbient :=
  51  !₂[Real.cos t, Real.sin t]
  52
  53/-- The vector `(cos t, sin t)` lies on the exact metric unit circle used by
  54`TopCat.sphere 1`. -/
  55theorem trigCircleVector_mem_sphere (t : ℝ) :
  56    trigCircleVector t ∈ Metric.sphere (0 : SphereOneAmbient) 1 := by
  57  change dist (trigCircleVector t) 0 = 1
  58  rw [dist_zero_right]
  59  have hsq : ‖trigCircleVector t‖ ^ 2 = 1 := by
  60    rw [EuclideanSpace.norm_sq_eq]
  61    simp [trigCircleVector, Fin.sum_univ_two, Real.cos_sq_add_sin_sq]
  62  have hnonneg : 0 ≤ ‖trigCircleVector t‖ := norm_nonneg _
  63  nlinarith
  64
  65/-- The ambient trigonometric circle parametrization is continuous. -/
  66theorem continuous_trigCircleVector :
  67    Continuous trigCircleVector := by
  68  change Continuous fun t : ℝ =>
  69    (WithLp.toLp 2 (fun i : Fin 2 => ![Real.cos t, Real.sin t] i) : SphereOneAmbient)
  70  exact (PiLp.continuous_toLp (p := 2) (β := fun _ : Fin 2 => ℝ)).comp
  71    (continuous_pi fun i => by
  72      fin_cases i
  73      · simpa using Real.continuous_cos
  74      · simpa using Real.continuous_sin)
  75
  76/-- The once-around trigonometric parametrization as a point of the exact
  77`TopCat.sphere 1` object. -/
  78def trigCirclePoint (t : ℝ) : TopCat.sphere 1 :=
  79  ULift.up ⟨trigCircleVector t, trigCircleVector_mem_sphere t⟩
  80
  81/-- The once-around trigonometric parametrization is continuous as a map into
  82the exact `TopCat.sphere 1` object. -/
  83theorem continuous_trigCirclePoint :
  84    Continuous trigCirclePoint := by
  85  unfold trigCirclePoint
  86  exact continuous_uliftUp.comp (continuous_trigCircleVector.subtype_mk _)
  87
  88/-- The trigonometric parametrization starts at the chosen basepoint. -/
  89theorem trigCirclePoint_zero :
  90    trigCirclePoint 0 = sphereOneBasepoint := by
  91  apply ULift.ext
  92  apply Subtype.ext
  93  ext i
  94  fin_cases i <;>
  95    simp [trigCirclePoint, trigCircleVector, sphereOneBasepoint, sphereOneBaseVector]
  96
  97/-- The trigonometric parametrization returns to the basepoint after one full
  98turn. -/
  99theorem trigCirclePoint_two_pi :
 100    trigCirclePoint (2 * Real.pi) = sphereOneBasepoint := by
 101  apply ULift.ext
 102  apply Subtype.ext
 103  ext i
 104  fin_cases i <;>
 105    simp [trigCirclePoint, trigCircleVector, sphereOneBasepoint, sphereOneBaseVector]
 106
 107/-- The constant singular 1-simplex at `sphereOneBasepoint`, in the actual
 108singular simplicial set of `TopCat.sphere 1`. -/
 109def constantSphereOneSingularOneSimplex :
 110    (TopCat.toSSet.obj (TopCat.sphere 1)).obj (op (SimplexCategory.mk 1)) :=
 111  (TopCat.toSSetObjEquiv (TopCat.sphere 1) (op (SimplexCategory.mk 1))).symm
 112    (ContinuousMap.const _ sphereOneBasepoint)
 113
 114/-- The constant singular 0-simplex at `sphereOneBasepoint`. -/
 115def constantSphereOneSingularZeroSimplex :
 116    (TopCat.toSSet.obj (TopCat.sphere 1)).obj (op (SimplexCategory.mk 0)) :=
 117  (TopCat.toSSetObjEquiv (TopCat.sphere 1) (op (SimplexCategory.mk 0))).symm
 118    (ContinuousMap.const _ sphereOneBasepoint)
 119
 120/-- The left face of the constant singular 1-simplex is the basepoint
 1210-simplex. -/
 122theorem constantSphereOneSingularOneSimplex_face_zero :
 123    (TopCat.toSSet.obj (TopCat.sphere 1)).δ (0 : Fin 2)
 124      constantSphereOneSingularOneSimplex =
 125        constantSphereOneSingularZeroSimplex := by
 126  rfl
 127
 128/-- The right face of the constant singular 1-simplex is the basepoint
 1290-simplex. -/
 130theorem constantSphereOneSingularOneSimplex_face_one :
 131    (TopCat.toSSet.obj (TopCat.sphere 1)).δ (1 : Fin 2)
 132      constantSphereOneSingularOneSimplex =
 133        constantSphereOneSingularZeroSimplex := by
 134  rfl
 135
 136/-- The two faces of the constant singular 1-simplex coincide. -/
 137theorem constantSphereOneSingularOneSimplex_faces_eq :
 138    (TopCat.toSSet.obj (TopCat.sphere 1)).δ (0 : Fin 2)
 139      constantSphereOneSingularOneSimplex =
 140        (TopCat.toSSet.obj (TopCat.sphere 1)).δ (1 : Fin 2)
 141          constantSphereOneSingularOneSimplex := by
 142  rw [constantSphereOneSingularOneSimplex_face_zero,
 143    constantSphereOneSingularOneSimplex_face_one]
 144
 145end
 146
 147end CircleParam
 148end Foundation
 149end IndisputableMonolith
 150