Aspherical homology 4-spheres

StructureClosed topological 4-manifold#✓fully proved

A closed topological 4-manifold is a nonempty, compact, connected, Hausdorff, second-countable topological space \(M\) together with an atlas of charts covering \(M\), each a homeomorphism from an open subset of \(M\) onto an open subset of \(\mathbb{R}^4\) (charts are modelled on all of \(\mathbb{R}^4\), not on a half-space, so \(M\) has no boundary).

No smoothness or compatibility between charts is required, so this is a topological, not necessarily smooth, manifold.

structure Closed4Manifold where
  /-- The underlying point set. -/
  carrier : Type
  [topology : TopologicalSpace carrier]
  [t2 : T2Space carrier]
  [secondCountable : SecondCountableTopology carrier]
  [charted : ChartedSpace (EuclideanSpace ℝ (Fin 4)) carrier]
  [compact : CompactSpace carrier]
  [connected : ConnectedSpace carrier]
  /-- The carrier is nonempty: a closed manifold has points. -/
  [nonempty : Nonempty carrier]

Used by 3

Used byExistence of an aspherical integer homology 4-sphere · Aspherical closed 4-manifold · Integer homology 4-sphere

DefinitionIntegral singular homology as a \(\mathbb{Z}\)-module#✓fully proved

For a natural number \(k\) and a topological space \(X\), \(H_k(X; \mathbb{Z})\) is the \(k\)-th singular homology of \(X\) with coefficients in \(\mathbb{Z}\), viewed as a \(\mathbb{Z}\)-module.

noncomputable def intHomology (k : ℕ) (X : TopCat) : ModuleCat ℤ :=
  ((singularHomologyFunctor (ModuleCat.{0} ℤ) k).obj (ModuleCat.of ℤ ℤ)).obj X

Used by 1

Used byInteger homology 4-sphere

DefinitionAspherical closed 4-manifold#✓fully proved

A closed topological 4-manifold \(M\) is aspherical if for every \(k \ge 2\) and every point \(x \in M\) the homotopy group \(\pi_k(M, x)\) is trivial.

def Closed4Manifold.IsAspherical (M : Closed4Manifold) : Prop :=
  ∀ k : ℕ, 2 ≤ k → ∀ x : M.carrier, Subsingleton (HomotopyGroup (Fin k) M.carrier x)

Uses 1 · Used by 1

Statement usesClosed topological 4-manifold

Used byExistence of an aspherical integer homology 4-sphere

DefinitionInteger homology 4-sphere#✓fully proved

A closed topological 4-manifold \(M\) is an integer homology 4-sphere if for every \(k \ge 0\) the integral singular homology \(H_k(M; \mathbb{Z})\) is isomorphic, as a \(\mathbb{Z}\)-module, to \(H_k(S^4; \mathbb{Z})\), where \(S^4\) is the unit sphere in \(\mathbb{R}^5\).

def Closed4Manifold.IsIntegerHomologySphere (M : Closed4Manifold) : Prop :=
  ∀ k : ℕ, Nonempty (intHomology k (TopCat.of M.carrier) ≅
    intHomology k (TopCat.of (sphere (0 : EuclideanSpace ℝ (Fin 5)) 1)))

Uses 2 · Used by 1

Statement usesClosed topological 4-manifold · Integral singular homology as a \(\mathbb{Z}\)-module

Used byExistence of an aspherical integer homology 4-sphere

TheoremExistence of an aspherical integer homology 4-sphere#●ready to prove

There is a closed connected topological 4-manifold \(M\) that is aspherical, meaning that for every \(k \ge 2\) and every point \(x \in M\) the homotopy group \(\pi_k(M, x)\) is trivial, and that is an integer homology 4-sphere, meaning that for every \(k \ge 0\) the integral singular homology \(H_k(M; \mathbb{Z})\) is isomorphic to \(H_k(S^4; \mathbb{Z})\), where \(S^4\) is the unit sphere in \(\mathbb{R}^5\).

public theorem_wanted aspherical_integer_homology_four_sphere :
    ∃ M : Closed4Manifold, M.IsAspherical ∧ M.IsIntegerHomologySphere

Sources

• J. G. Ratcliffe and S. T. Tschantz, Some examples of aspherical 4-manifolds that are homology 4-spheres, arXiv:math/0312436 (2003), solving [Kir97, Problem 4.17]. Earlier, F. Luo constructed an aspherical rational homology 4-sphere (1988). Problem aspherical_integer_homology_four_sphere of the lean-eval benchmark.

Uses 3

Statement usesClosed topological 4-manifold · Aspherical closed 4-manifold · Integer homology 4-sphere

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.