LinkingForcesD3

formal source

  75topological linking (knots/links). The simplest non-trivial link
  76is between circles. Circles link non-trivially only in D = 3. -/
  77
  78structure LinkingForcesD3 where
  79  smallest_linker : ℕ := 1  -- S^1 (circle)
  80  linking_requires : linking_dimension 1 = 3
  81  no_linking_in_2D : ∀ D, D ≤ 2 → ¬(∃ p, linking_dimension p = D ∧ p ≥ 1)
  82  linking_in_3D : linking_dimension 1 = 3
  83
  84theorem linking_forces_d3_cert : LinkingForcesD3 where
  85  linking_requires := circle_links_in_three
  86  no_linking_in_2D := by
  87    intro D hD ⟨p, hp, hp1⟩
  88    unfold linking_dimension at hp
  89    omega
  90  linking_in_3D := circle_links_in_three
  91
  92/-! ## Certificate -/
  93
  94structure AlexanderDualityCert where
  95  circle_degree : circle_cohomology.reduced_cohomology_rank 1 = 1
  96  circle_only_degree : ∀ k, k ≠ 1 → circle_cohomology.reduced_cohomology_rank k = 0
  97  d3_from_linking : linking_dimension 1 = 3
  98
  99theorem alexander_duality_cert_exists : Nonempty AlexanderDualityCert :=
 100  ⟨{ circle_degree := circle_nontrivial_in_degree_one
 101     circle_only_degree := circle_trivial_elsewhere
 102     d3_from_linking := circle_links_in_three }⟩
 103
 104end IndisputableMonolith.Foundation.AlexanderDualityProof