[Merged by Bors] - feat(Geometry/Manifold): state generalized Poincaré conjecture

[alreadydone]

---

[github-actions]

PR summary 61f96f8bc4

Import changes

No significant changes to the import graph

---

Declarations diff

+ ContinuousMap.HomotopyEquiv.NonemptyDiffeomorphSphere
++ instance (n : ℕ) :

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[ocfnash]

Ha, lovely!

I think it is probably a good idea to introduce:

class IsHomotopySphere (M : Type*) [TopologicalSpace M] (n : ℕ) : Prop :=
  nonempty_homotopyEquiv : Nonempty (ContinuousMap.HomotopyEquiv M S)

and

class IsTopologicalSphere (M : Type*) [TopologicalSpace M] (n : ℕ) : Prop :=
  nonempty_homoeomorph : Nonempty (Homeomorph M S)

I'll have a proper look this evening when I have some time (and try to remember if there was a reason I used structomorph rather than diffeomorph when I was over in ICERM).

[ocfnash]

What do you think about something like this:

def TopologicalPoincareConjecture (n : ℕ) : Prop :=
    ∀ (M : Type u) [TopologicalSpace M] [T2Space M] [ChartedSpace ℝⁿ M],
    M ≃ₕ 𝕊ⁿ → Nonempty (M ≃ₜ 𝕊ⁿ)

def SmoothPoincareConjecture (n : ℕ) : Prop :=
    ∀ (M : Type u) [TopologicalSpace M] [T2Space M] [ChartedSpace ℝⁿ M]
    [SmoothManifoldWithCorners (𝓡 n) M],
    M ≃ₕ 𝕊ⁿ → Nonempty (M ≃ₘ⟮𝓡 n, 𝓡 n⟯ 𝕊ⁿ)

proof_wanted TopologicalPoincareConjecture.proof : ∀ n, TopologicalPoincareConjecture n

proof_wanted SmoothPoincareConjecture.not_seven : ¬ SmoothPoincareConjecture 7

etc

[kim-em]

bors merge

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style