IndisputableMonolith.Foundation.LinkingVanishingLowDim

   1import Mathlib.AlgebraicTopology.SingularHomology.Basic
   2import Mathlib.Algebra.Category.ModuleCat.Colimits
   3import Mathlib.Algebra.Homology.ShortComplex.ModuleCat
   4import Mathlib.Topology.Category.TopCat.Sphere
   5import Mathlib.Geometry.Manifold.Instances.Sphere
   6
   7/-!
   8# Linking vanishes in low dimension (D = 0, 1)
   9
  10Mathlib-only leaf module. It restates (verbatim) the content-typed linking
  11object `linkingComplementH1` and detector `DetectsNontrivialLinking` from
  12`IndisputableMonolith.Foundation.PublicSpine`, and proves that the detector
  13fails in dimensions `0` and `1`:
  14
  15* `not_detects_zero`: the `0`-sphere is a finite (two-point) space, hence
  16  totally disconnected, hence so is every subspace; singular homology in
  17  degree `1` of a totally disconnected space vanishes
  18  (`AlgebraicTopology.isZero_singularHomologyFunctor_of_totallyDisconnectedSpace`).
  19* `not_detects_one`: a continuous injection `S¹ → S¹` is surjective (if it
  20  missed a point, stereographic projection would give a continuous injection
  21  `S¹ → ℝ`, impossible since removing the preimage of a middle value keeps
  22  `S¹` connected while disconnecting the image interval); the complement of
  23  an embedded circle in `S¹` is therefore empty, and homology of the empty
  24  space vanishes in degree `1`.
  25
  26The two definitions are restated with the same implicit arguments and
  27universes as the parent module, so the parent can glue by `exact`.
  28-/
  29
  30namespace IndisputableMonolith
  31namespace Foundation
  32namespace LinkingVanishingLowDim
  33
  34/-- Verbatim restatement of `PublicSpine.linkingComplementH1`. -/
  35noncomputable def linkingComplementH1 (D : ℕ)
  36    (f : C(TopCat.sphere.{0} 1, TopCat.sphere.{0} D)) : ModuleCat ℤ :=
  37  ((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) 1).obj
  38    (ModuleCat.of ℤ ℤ)).obj
  39    (TopCat.of {x : TopCat.sphere.{0} D // x ∉ Set.range f})
  40
  41/-- Verbatim restatement of `PublicSpine.DetectsNontrivialLinking`. -/
  42def DetectsNontrivialLinking (D : ℕ) : Prop :=
  43  ∃ f : C(TopCat.sphere.{0} 1, TopCat.sphere.{0} D),
  44    Topology.IsEmbedding f ∧
  45      ¬ CategoryTheory.Limits.IsZero (linkingComplementH1 D f)
  46
  47/-! ## Dimension 0: the 0-sphere is a two-point space -/
  48
  49/-- The unit sphere in `ℝ¹` is contained in the two-point set `{e, -e}`. -/
  50lemma sphere_fin_one_finite :
  51    (Metric.sphere (0 : EuclideanSpace ℝ (Fin 1)) 1).Finite := by
  52  have hsub : Metric.sphere (0 : EuclideanSpace ℝ (Fin 1)) 1 ⊆
  53      {EuclideanSpace.single (0 : Fin 1) (1 : ℝ),
  54        EuclideanSpace.single (0 : Fin 1) (-1 : ℝ)} := by
  55    intro x hx
  56    rw [EuclideanSpace.sphere_zero_eq _ zero_le_one, Set.mem_setOf_eq,
  57      Fin.sum_univ_one] at hx
  58    have h0 : (x 0 - 1) * (x 0 + 1) = 0 := by nlinarith
  59    rcases mul_eq_zero.mp h0 with h | h
  60    · left
  61      ext i
  62      obtain rfl : i = (0 : Fin 1) := Subsingleton.elim _ _
  63      rw [EuclideanSpace.single_apply, if_pos rfl]
  64      linarith
  65    · right
  66      ext i
  67      obtain rfl : i = (0 : Fin 1) := Subsingleton.elim _ _
  68      rw [EuclideanSpace.single_apply, if_pos rfl]
  69      linarith
  70  exact ((Set.finite_singleton _).insert _).subset hsub
  71
  72instance : Finite ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 1)) 1) :=
  73  sphere_fin_one_finite.to_subtype
  74
  75/-- No embedded circle in the 0-sphere has homologically nontrivial
  76complement: every subspace of the two-point space `S⁰` is totally
  77disconnected, so its first singular homology vanishes. -/
  78theorem not_detects_zero : ¬ DetectsNontrivialLinking 0 := by
  79  rintro ⟨f, -, hH⟩
  80  apply hH
  81  haveI hTD : TotallyDisconnectedSpace ↥(TopCat.sphere.{0} 0) := by
  82    show TotallyDisconnectedSpace
  83      (ULift.{0} ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 1)) 1))
  84    infer_instance
  85  haveI : TotallyDisconnectedSpace
  86      ↥(TopCat.of {x : TopCat.sphere.{0} 0 // x ∉ Set.range f}) :=
  87    (inferInstance :
  88      TotallyDisconnectedSpace {x : TopCat.sphere.{0} 0 // x ∉ Set.range f})
  89  exact AlgebraicTopology.isZero_singularHomologyFunctor_of_totallyDisconnectedSpace
  90    (ModuleCat ℤ) 1 (ModuleCat.of ℤ ℤ)
  91    (TopCat.of {x : TopCat.sphere.{0} 0 // x ∉ Set.range f}) one_ne_zero
  92
  93/-! ## Dimension 1: an embedded circle fills the whole 1-sphere -/
  94
  95/-- There is no continuous injection from the metric circle into `ℝ`:
  96removing the preimage of a strictly-middle value leaves the circle connected
  97(stereographic projection identifies it with `ℝ¹`), while the image must be
  98an order-connected set that omits a middle point between two attained
  99values. -/
 100theorem no_continuous_injective_circle_to_real
 101    (g : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) → ℝ)
 102    (hgc : Continuous g) (hginj : Function.Injective g) : False := by
 103  -- three distinct points on the circle
 104  have mem1 : EuclideanSpace.single (0 : Fin 2) (1 : ℝ) ∈
 105      Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 := by
 106    rw [mem_sphere_zero_iff_norm, EuclideanSpace.norm_single]; norm_num
 107  have mem2 : EuclideanSpace.single (1 : Fin 2) (1 : ℝ) ∈
 108      Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 := by
 109    rw [mem_sphere_zero_iff_norm, EuclideanSpace.norm_single]; norm_num
 110  have mem3 : EuclideanSpace.single (0 : Fin 2) (-1 : ℝ) ∈
 111      Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 := by
 112    rw [mem_sphere_zero_iff_norm, EuclideanSpace.norm_single]; norm_num
 113  set a : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) := ⟨_, mem1⟩ with ha
 114  set b : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) := ⟨_, mem2⟩ with hb
 115  set c : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) := ⟨_, mem3⟩ with hc
 116  have hab : a ≠ b := by
 117    intro h
 118    have h0 := congrArg (fun v : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) =>
 119      (v : EuclideanSpace ℝ (Fin 2)) 0) h
 120    simp only [ha, hb, EuclideanSpace.single_apply] at h0
 121    norm_num at h0
 122  have hac : a ≠ c := by
 123    intro h
 124    have h0 := congrArg (fun v : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) =>
 125      (v : EuclideanSpace ℝ (Fin 2)) 0) h
 126    simp only [ha, hc, EuclideanSpace.single_apply] at h0
 127    norm_num at h0
 128  have hbc : b ≠ c := by
 129    intro h
 130    have h0 := congrArg (fun v : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) =>
 131      (v : EuclideanSpace ℝ (Fin 2)) 0) h
 132    simp only [hb, hc, EuclideanSpace.single_apply] at h0
 133    norm_num at h0
 134  -- among the three (distinct) values pick the strictly-middle one
 135  have hgab : g a ≠ g b := fun h => hab (hginj h)
 136  have hgac : g a ≠ g c := fun h => hac (hginj h)
 137  have hgbc : g b ≠ g c := fun h => hbc (hginj h)
 138  obtain ⟨x0, y1, y2, hy1, hy2, hlt1, hlt2⟩ :
 139      ∃ x0 y1 y2 : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1),
 140        y1 ≠ x0 ∧ y2 ≠ x0 ∧ g y1 < g x0 ∧ g x0 < g y2 := by
 141    rcases hgab.lt_or_gt with h1 | h1
 142    · rcases hgbc.lt_or_gt with h2 | h2
 143      · exact ⟨b, a, c, hab, hbc.symm, h1, h2⟩
 144      · rcases hgac.lt_or_gt with h3 | h3
 145        · exact ⟨c, a, b, hac, hbc, h3, h2⟩
 146        · exact ⟨a, c, b, hac.symm, hab.symm, h3, h1⟩
 147    · rcases hgac.lt_or_gt with h3 | h3
 148      · exact ⟨a, b, c, hab.symm, hac.symm, h1, h3⟩
 149      · rcases hgbc.lt_or_gt with h2 | h2
 150        · exact ⟨c, b, a, hbc, hac, h2, h3⟩
 151        · exact ⟨b, c, a, hbc.symm, hab, h2, h1⟩
 152  -- the circle minus the middle point is connected (stereographic projection)
 153  haveI fact2 : Fact (Module.finrank ℝ (EuclideanSpace ℝ (Fin 2)) = 1 + 1) :=
 154    ⟨by norm_num [finrank_euclideanSpace_fin]⟩
 155  have hconn :
 156      IsConnected ({x0}ᶜ : Set ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1)) := by
 157    haveI hct : ConnectedSpace ((stereographic' (1 : ℕ) x0).target) := by
 158      rw [stereographic'_target]
 159      exact (Homeomorph.Set.univ (EuclideanSpace ℝ (Fin 1))).symm.surjective.connectedSpace
 160        (Homeomorph.Set.univ (EuclideanSpace ℝ (Fin 1))).symm.continuous
 161    haveI hcs : ConnectedSpace ((stereographic' (1 : ℕ) x0).source) :=
 162      (stereographic' (1 : ℕ) x0).toHomeomorphSourceTarget.symm.surjective.connectedSpace
 163        (stereographic' (1 : ℕ) x0).toHomeomorphSourceTarget.symm.continuous
 164    rw [← stereographic'_source (n := 1) x0]
 165    exact isConnected_iff_connectedSpace.mpr hcs
 166  -- its image omits the middle value, contradicting order-connectedness
 167  have hy1m : y1 ∈ ({x0}ᶜ : Set ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1)) :=
 168    Set.mem_compl_singleton_iff.mpr hy1
 169  have hy2m : y2 ∈ ({x0}ᶜ : Set ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1)) :=
 170    Set.mem_compl_singleton_iff.mpr hy2
 171  have himg : IsPreconnected (g '' ({x0}ᶜ)) :=
 172    hconn.isPreconnected.image g hgc.continuousOn
 173  have hmid : g x0 ∈ g '' ({x0}ᶜ) :=
 174    himg.Icc_subset ⟨y1, hy1m, rfl⟩ ⟨y2, hy2m, rfl⟩ ⟨hlt1.le, hlt2.le⟩
 175  obtain ⟨z, hz, hzeq⟩ := hmid
 176  exact Set.mem_compl_singleton_iff.mp hz (hginj hzeq)
 177
 178/-- A continuous injection of the metric circle into itself is surjective:
 179if it missed a point, composing with the stereographic projection from that
 180point would give a continuous injection of the circle into `ℝ¹`. -/
 181theorem continuous_injective_circle_self_surjective
 182    (f₀ : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) →
 183      ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1))
 184    (hc : Continuous f₀) (hinj : Function.Injective f₀) :
 185    Function.Surjective f₀ := by
 186  intro p
 187  by_contra hp
 188  push_neg at hp
 189  haveI fact2 : Fact (Module.finrank ℝ (EuclideanSpace ℝ (Fin 2)) = 1 + 1) :=
 190    ⟨by norm_num [finrank_euclideanSpace_fin]⟩
 191  set φ := stereographic' (1 : ℕ) p with hφ
 192  have hmem : ∀ x, f₀ x ∈ φ.source := by
 193    intro x
 194    rw [hφ, stereographic'_source]
 195    exact Set.mem_compl_singleton_iff.mpr (hp x)
 196  have hφc : Continuous fun x => φ (f₀ x) :=
 197    φ.continuousOn.comp_continuous hc hmem
 198  set g : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) → ℝ :=
 199    fun x => (φ (f₀ x)) 0 with hg
 200  have hgc : Continuous g :=
 201    (EuclideanSpace.proj (0 : Fin 1)).continuous.comp hφc
 202  have hginj : Function.Injective g := by
 203    intro x y hxy
 204    apply hinj
 205    apply φ.injOn (hmem x) (hmem y)
 206    ext i
 207    obtain rfl : i = (0 : Fin 1) := Subsingleton.elim _ _
 208    exact hxy
 209  exact (no_continuous_injective_circle_to_real g hgc hginj).elim
 210
 211/-- No embedded circle in the 1-sphere has homologically nontrivial
 212complement: the embedding is surjective, so the complement is empty, and
 213singular homology of the empty space vanishes in degree `1`. -/
 214theorem not_detects_one : ¬ DetectsNontrivialLinking 1 := by
 215  rintro ⟨f, hemb, hH⟩
 216  apply hH
 217  -- the underlying self-map of the metric circle
 218  set f₀ : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) →
 219      ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) :=
 220    fun x =>
 221      (show ULift.{0} ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) from
 222        f (show ↥(TopCat.sphere.{0} 1) from ULift.up x)).down with hf₀
 223  have hc : Continuous f₀ := by
 224    exact continuous_uliftDown.comp (f.continuous.comp continuous_uliftUp)
 225  have hinj : Function.Injective f₀ := by
 226    intro x y h
 227    have h2 : f (ULift.up x) = f (ULift.up y) := ULift.down_injective h
 228    have h3 := hemb.injective h2
 229    exact congrArg ULift.down h3
 230  have hsurj := continuous_injective_circle_self_surjective f₀ hc hinj
 231  haveI hE : IsEmpty {x : TopCat.sphere.{0} 1 // x ∉ Set.range f} := by
 232    constructor
 233    rintro ⟨x, hx⟩
 234    obtain ⟨y, hy⟩ := hsurj
 235      (show ULift.{0} ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) from x).down
 236    exact hx ⟨ULift.up y, ULift.down_injective hy⟩
 237  haveI hTD : TotallyDisconnectedSpace {x : TopCat.sphere.{0} 1 // x ∉ Set.range f} := by
 238    constructor
 239    intro t _ _ x hx
 240    exact (hE.false x).elim
 241  haveI : TotallyDisconnectedSpace
 242      ↥(TopCat.of {x : TopCat.sphere.{0} 1 // x ∉ Set.range f}) := hTD
 243  exact AlgebraicTopology.isZero_singularHomologyFunctor_of_totallyDisconnectedSpace
 244    (ModuleCat ℤ) 1 (ModuleCat.of ℤ ℤ)
 245    (TopCat.of {x : TopCat.sphere.{0} 1 // x ∉ Set.range f}) one_ne_zero
 246
 247end LinkingVanishingLowDim
 248end Foundation
 249end IndisputableMonolith
 250