Documentation

FormalConjectures.Millenium.Poincare

The Poincaré Conjecture #

References:

source
def PoincareConjecture.ConjectureFor (n : ℕ) :
Prop

The predicate that the generalized Poincaré conjecture holds in dimension $n$, i.e. that any $n$-dimensional manifold that is homotopy equivalent to the sphere is in fact homeomorphic to the sphere.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem PoincareConjecture.poincare_conjecture :
    ConjectureFor 3

    The Millenium Problem, solved by Grigori Perelman in 2003: the Poincaré Conjecture holds.

    source
    theorem PoincareConjecture.poincare_conjecture.variants.dimension_two :
    ConjectureFor 2

    The Generalized Poincaré Conjecture holds for surfaces.

    source
    theorem PoincareConjecture.poincare_conjecture.variants.dimension_ge_five (n : ℕ) (hn : 5 ≤ n) :
    ConjectureFor n

    The Generalized Poincaré Conjecture holds for dimensions at least 5.

    source
    theorem PoincareConjecture.poincare_conjecture.variants.dimension_four :
    ConjectureFor 4

    The Generalized Poincaré Conjecture holds in dimension 4.

    source
    def PoincareConjecture.SmoothConjectureFor (n : ℕ) :
    Prop

    The predicate that the smooth Poincaré conjecture holds in dimension $n$.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem PoincareConjecture.poincare_conjecture.variants.smooth_for_three :
      SmoothConjectureFor 3

      A reformulation of the Millenium Problem in terms of smooth 3-folds.

      source
      theorem PoincareConjecture.poincare_conjecture.variants.smooth_implication (H : SmoothConjectureFor 3) :
      ConjectureFor 3

      The smooth formulation of the Millenium Problem implies the general case. This follows from the fact that every topological 3-fold admits a smooth structure [mo296171].

      source
      def PoincareConjecture.SmoothTrueValues :
      Set ℕ

      The values at which the smooth version of the conjecture is known to hold.

      Equations
      Instances For
        source
        theorem PoincareConjecture.poincare_conjecture.variants.smooth_known_cases (n : ℕ) (hn : n ∈ SmoothTrueValues) :
        SmoothConjectureFor n

        The smooth version of the Poincaré conjecture is known to hold in dimensions $1, 2, 3, 5, 6, 12, 56, 61$. See [Wang2017].

        source
        theorem PoincareConjecture.poincare_conjecture.variants.smooth_dimension_four :
        SmoothConjectureFor 4

        The four dimensional case of the smooth version of the conjecture is still open. See [Wang2017].

        source
        theorem PoincareConjecture.poincare_conjecture.variants.smooth_other_cases (n : ℕ) (hn : n > 4) (hn' : n ∉ SmoothTrueValues) :
        ¬SmoothConjectureFor n

        It is conjectured that the only values of $n > 4$ for which the smooth version of the conjecture holds are $n = 5, 6, 12, 56, 61$. See Conjecture 1.17 in [Wang2017].