Linearity of 3-manifold groups

StructureClosed topological 3-manifold#✓fully proved

A closed topological 3-manifold is a nonempty, compact, connected, Hausdorff, second-countable topological space \(M\) together with an atlas of charts, homeomorphisms from open subsets of \(M\) onto open subsets of \(\mathbb{R}^3\), whose domains cover \(M\). Since the charts land in \(\mathbb{R}^3\) itself rather than in a half-space, \(M\) has no boundary.

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

Used by 1

Used byA closed 3-manifold group with no faithful representation in \(GL_4(\mathbb{R})\)

TheoremA closed 3-manifold group with no faithful representation in \(GL_4(\mathbb{R})\)#●ready to prove

There is a closed connected topological 3-manifold \(M\) with a point \(x\) such that no group homomorphism from the fundamental group \(\pi_1(M, x)\) to \(GL_4(\mathbb{R})\) is injective.

public theorem_wanted nonlinear_three_manifold_group :
    ∃ (M : Closed3Manifold) (x : M.carrier),
      ∀ f : FundamentalGroup M.carrier x →* GL (Fin 4) ℝ, ¬ Function.Injective f

Sources

• J. O. Button, Aspherical 3-manifold groups not in GL(4, k) for any field k, arXiv:1404.4639 (2014). See the discussion of [Kir97, Problem 3.33] in the K3 problem list. Problem nonlinear_three_manifold_group of the lean-eval benchmark.

Uses 1

Statement usesClosed topological 3-manifold

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.