IndisputableMonolith.Foundation.CircleFundamentalSimplex

   1import IndisputableMonolith.Foundation.CircleParam
   2
   3/-!
   4# The Fundamental Singular 1-Simplex of the Circle
   5
   6This module constructs the once-around singular 1-simplex in the actual
   7singular simplicial set `TopCat.toSSet.obj (TopCat.sphere 1)` and proves its
   8two faces coincide at the chosen basepoint.
   9-/
  10
  11namespace IndisputableMonolith
  12namespace Foundation
  13namespace CircleFundamentalSimplex
  14
  15open CategoryTheory Opposite
  16open scoped Real
  17
  18noncomputable section
  19
  20open CircleParam
  21
  22/-- The continuous once-around path from the topological standard 1-simplex to
  23the exact `TopCat.sphere 1` object.  The parameter is the second barycentric
  24coordinate, so the endpoints evaluate at angles `0` and `2π`. -/
  25def fundamentalCirclePathMap :
  26    C(stdSimplex ℝ (Fin 2), TopCat.sphere 1) where
  27  toFun x := trigCirclePoint (2 * Real.pi * (x : Fin 2 → ℝ) 1)
  28  continuous_toFun := by
  29    apply continuous_trigCirclePoint.comp
  30    have hcoord : Continuous fun x : stdSimplex ℝ (Fin 2) => (x : Fin 2 → ℝ) 1 :=
  31      (continuous_apply 1).comp continuous_subtype_val
  32    exact continuous_const.mul hcoord
  33
  34/-- The once-around singular 1-simplex in `TopCat.toSSet.obj (TopCat.sphere 1)`.
  35This is the geometric generator candidate for the later H1 computation. -/
  36def fundamentalSphereOneSingularOneSimplex :
  37    (TopCat.toSSet.obj (TopCat.sphere 1)).obj (op (SimplexCategory.mk 1)) :=
  38  (TopCat.toSSetObjEquiv (TopCat.sphere 1) (op (SimplexCategory.mk 1))).symm
  39    fundamentalCirclePathMap
  40
  41/-- The `δ 0` face of the fundamental singular 1-simplex is the chosen
  42basepoint.  In Mathlib's simplex convention this endpoint evaluates the second
  43barycentric coordinate at `1`, hence the angle `2π`. -/
  44theorem fundamentalSphereOneSingularOneSimplex_face_zero :
  45    (TopCat.toSSet.obj (TopCat.sphere 1)).δ (0 : Fin 2)
  46      fundamentalSphereOneSingularOneSimplex =
  47        constantSphereOneSingularZeroSimplex := by
  48  apply (TopCat.toSSetObjEquiv (TopCat.sphere 1) (op (SimplexCategory.mk 0))).injective
  49  ext x
  50  dsimp [TopCat.toSSetObjEquiv, TopCat.toSSet,
  51    CategoryTheory.Presheaf.restrictedULiftYoneda,
  52    CategoryTheory.SimplicialObject.δ,
  53    CategoryTheory.ConcreteCategory.homEquiv,
  54    Homeomorph.continuousMapCongr,
  55    fundamentalSphereOneSingularOneSimplex, fundamentalCirclePathMap,
  56    constantSphereOneSingularZeroSimplex]
  57  change trigCirclePoint
  58      (2 * Real.pi *
  59        ((stdSimplex.map (S := ℝ) ⇑(ConcreteCategory.hom (SimplexCategory.δ (0 : Fin 2))) x :
  60            stdSimplex ℝ (Fin 2)) : Fin 2 → ℝ) 1) =
  61    sphereOneBasepoint
  62  rw [show
  63      ((stdSimplex.map (S := ℝ) ⇑(ConcreteCategory.hom (SimplexCategory.δ (0 : Fin 2))) x :
  64          stdSimplex ℝ (Fin 2)) : Fin 2 → ℝ) 1 = 1 by
  65    rw [stdSimplex.map_coe, FunOnFinite.linearMap_apply_apply]
  66    simp [SimplexCategory.δ]
  67    decide]
  68  simpa using trigCirclePoint_two_pi
  69
  70/-- The `δ 1` face of the fundamental singular 1-simplex is the chosen
  71basepoint.  This endpoint evaluates the second barycentric coordinate at `0`,
  72hence the angle `0`. -/
  73theorem fundamentalSphereOneSingularOneSimplex_face_one :
  74    (TopCat.toSSet.obj (TopCat.sphere 1)).δ (1 : Fin 2)
  75      fundamentalSphereOneSingularOneSimplex =
  76        constantSphereOneSingularZeroSimplex := by
  77  apply (TopCat.toSSetObjEquiv (TopCat.sphere 1) (op (SimplexCategory.mk 0))).injective
  78  ext x
  79  dsimp [TopCat.toSSetObjEquiv, TopCat.toSSet,
  80    CategoryTheory.Presheaf.restrictedULiftYoneda,
  81    CategoryTheory.SimplicialObject.δ,
  82    CategoryTheory.ConcreteCategory.homEquiv,
  83    Homeomorph.continuousMapCongr,
  84    fundamentalSphereOneSingularOneSimplex, fundamentalCirclePathMap,
  85    constantSphereOneSingularZeroSimplex]
  86  change trigCirclePoint
  87      (2 * Real.pi *
  88        ((stdSimplex.map (S := ℝ) ⇑(ConcreteCategory.hom (SimplexCategory.δ (1 : Fin 2))) x :
  89            stdSimplex ℝ (Fin 2)) : Fin 2 → ℝ) 1) =
  90    sphereOneBasepoint
  91  rw [show
  92      ((stdSimplex.map (S := ℝ) ⇑(ConcreteCategory.hom (SimplexCategory.δ (1 : Fin 2))) x :
  93          stdSimplex ℝ (Fin 2)) : Fin 2 → ℝ) 1 = 0 by
  94    rw [stdSimplex.map_coe, FunOnFinite.linearMap_apply_apply]
  95    simp [SimplexCategory.δ]]
  96  simpa using trigCirclePoint_zero
  97
  98/-- The fundamental once-around singular 1-simplex is a loop: its two faces are
  99equal in the actual singular simplicial set of `TopCat.sphere 1`. -/
 100theorem fundamentalSphereOneSingularOneSimplex_faces_eq :
 101    (TopCat.toSSet.obj (TopCat.sphere 1)).δ (0 : Fin 2)
 102      fundamentalSphereOneSingularOneSimplex =
 103        (TopCat.toSSet.obj (TopCat.sphere 1)).δ (1 : Fin 2)
 104          fundamentalSphereOneSingularOneSimplex := by
 105  rw [fundamentalSphereOneSingularOneSimplex_face_zero,
 106    fundamentalSphereOneSingularOneSimplex_face_one]
 107
 108end
 109
 110end CircleFundamentalSimplex
 111end Foundation
 112end IndisputableMonolith
 113