Manifolds and geometric topology

Topological and smooth manifolds in low and high dimensions: surfaces, 3- and 4-manifolds, the Poincaré conjecture, exotic spheres, triangulations, diffeomorphism groups and transformation groups.

TheoremBudney–Gabai knotted three-spheres in \(S^1 \times S^3\)#●ready to prove

Let \(S^1 \subset \mathbb{R}^2\) and \(S^3 \subset \mathbb{R}^4\) be the unit spheres, and fix a point \(x_0 \in S^1\). There is a sequence \(e_0, e_1, e_2, \dots\) of smooth embeddings \(S^3 \to S^1 \times S^3\) such that the complement of the image of each \(e_n\) is connected, each \(e_n\) is homotopic to the standard cross-section \(p \mapsto (x_0, p)\), and for \(i \ne j\) the images of \(e_i\) and \(e_j\) are not smoothly isotopic: there is no smooth map \(H : [0, 1] \times S^3 \to S^1 \times S^3\) such that every slice \(H(t, \cdot)\) is a smooth embedding, \(H(0, \cdot)\) has the same image as \(e_i\), and \(H(1, \cdot)\) has the same image as \(e_j\).

MathlibExt.Topology.BudneyGabaiWanted.Topology.budney_gabai_knotted_three_spheres · 26 lines 
public theorem_wanted budney_gabai_knotted_three_spheres
    (x₀ : sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) :
    ∃ e : ℕ → sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
        sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 ×
          sphere (0 : EuclideanSpace ℝ (Fin 4)) 1,
      (∀ n,
        Manifold.IsSmoothEmbedding
            (𝓡 3) ((𝓡 1).prod (𝓡 3)) ∞ (e n) ∧
          IsConnected (Set.range (e n))ᶜ ∧
          ∃ K : unitInterval × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
              sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 ×
                sphere (0 : EuclideanSpace ℝ (Fin 4)) 1,
            Continuous K ∧
              (∀ p, K (0, p) = e n p) ∧
              ∀ p, K (1, p) = (x₀, p)) ∧
        ∀ i j, i ≠ j →
          ¬ ∃ H : unitInterval × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
              sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 ×
                sphere (0 : EuclideanSpace ℝ (Fin 4)) 1,
            ContMDiff
                ((𝓡∂ 1).prod (𝓡 3)) ((𝓡 1).prod (𝓡 3)) ∞ H ∧
              (∀ t,
                Manifold.IsSmoothEmbedding
                  (𝓡 3) ((𝓡 1).prod (𝓡 3)) ∞ (fun p ↦ H (t, p))) ∧
              Set.range (fun p ↦ H (0, p)) = Set.range (e i) ∧
              Set.range (fun p ↦ H (1, p)) = Set.range (e j)
Sources
  • R. Budney and D. Gabai, 'Knotted 3-balls in S⁴', Corollary 8.6, arXiv:1912.09029v3 (2021), https://arxiv.org/abs/1912.09029. Problem budney_gabai_knotted_three_spheres of the lean-eval benchmark.

TheoremMilnor's exotic 7-sphere#●ready to prove

There is a smooth manifold \(M\) modelled on \(\mathbb{R}^7\) (a topological space with a \(C^\infty\) atlas of charts into \(\mathbb{R}^7\)) that is homeomorphic to the unit sphere \(S^7 \subset \mathbb{R}^8\) but is not diffeomorphic to \(S^7\) with its standard smooth structure.

public theorem_wanted milnor_exotic_sphere_seven :
    ∃ (M : Type) (_ : TopologicalSpace M)
      (_ : ChartedSpace (EuclideanSpace ℝ (Fin 7)) M)
      (_ : IsManifold (𝓡 7) ∞ M)
      (_homeo : M ≃ₜ sphere (0 : EuclideanSpace ℝ (Fin 8)) 1),
      IsEmpty (M ≃ₘ⟮𝓡 7, 𝓡 7⟯ sphere (0 : EuclideanSpace ℝ (Fin 8)) 1)
Sources
  • J. Milnor, On manifolds homeomorphic to the 7-sphere, Ann. of Math. 64 (1956), 399-405. Problem milnor_exotic_sphere_seven of the lean-eval benchmark.

TheoremPardon's theorem: the p-adic integers cannot act faithfully and continuously on a connected 3-manifold#●ready to prove

Pardon's theorem: the p-adic integers cannot act faithfully and continuously on a connected 3-manifold. Let \(p\) be a prime and \(M\) a connected, Hausdorff, second-countable topological space with an atlas of charts modelled on \(\mathbb{R}^3\), that is, a connected topological 3-manifold without boundary. Then there is no faithful action of the additive group \(\mathbb{Z}_p\) of \(p\)-adic integers on \(M\) that is jointly continuous as a map \(\mathbb{Z}_p \times M \to M\).

This is the \(p\)-adic case of the Hilbert–Smith conjecture in dimension three; deducing that every locally compact group acting faithfully on a connected 3-manifold is a Lie group also needs the classical reduction to \(\mathbb{Z}_p\)-actions, which is not part of this statement.

public theorem_wanted hilbert_smith_padic_dimension_three
    (p : ℕ) [Fact p.Prime]
    (M : Type*) [TopologicalSpace M] [T2Space M] [SecondCountableTopology M]
    [ConnectedSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 3)) M]
    [AddAction (PadicInt p) M] [ContinuousVAdd (PadicInt p) M]
    [FaithfulVAdd (PadicInt p) M] :
    False
Sources
  • John Pardon, 'The Hilbert-Smith conjecture for three-manifolds', Journal of the American Mathematical Society 26 (2013), no. 3, 879-899, Theorem 1.5. https://doi.org/10.1090/S0894-0347-2013-00766-3. Problem hilbert_smith_padic_dimension_three of the lean-eval benchmark.
3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.