feat(Geometry): add Freedman's non-smoothability theorem - #523
Conversation
|
Having just opened this, it occurs to me that a better challenge might be to demand a proof that all topological manifolds of dimension 3 can be smoothed. |
After witnessing CI error in parallel PR I suspect this will be necessary.
alreadydone
left a comment
alreadydone
left a comment
There was a problem hiding this comment.
Having just opened this, it occurs to me that a better challenge might be to demand a proof that all topological manifolds of dimension 3 can be smoothed.
I think this is also a good eval problem, and we could add uniqueness too:
local notation "𝔼" => EuclideanSpace ℝ (Fin 3)
theorem three_manifold_smoothable (M : Type*) [TopologicalSpace M] [Nonempty (ChartedSpace 𝔼 M)] :
-- is SecondCountableSpace and T2Space necessary?
∃ _ : ChartedSpace 𝔼 M, IsManifold (𝓡 3) ∞ M := by
sorry
theorem three_manifold_unique_smooth (M N : Type*) [TopologicalSpace M] [TopologicalSpace N]
[ChartedSpace 𝔼 M] [ChartedSpace 𝔼 N] [IsManifold (𝓡 3) ∞ M] [IsManifold (𝓡 3) ∞ N]
(homeo : M ≃ₜ N) :
-- I think this should be true but don't have an exact reference
-- also for Homeomorph.Isotopic (not yet in mathlib) instead of ContinuousMap.Homotopic
∃ diffeo : M ≃ₘ⟮𝓡 3, 𝓡 3⟯ N, ContinuousMap.Homotopic (X := M) (Y := N) diffeo homeo := by
sorry
| In 1982, Freedman proved that every symmetric unimodular bilinear form over `ℤ` arises as the | ||
| intersection form of a closed, oriented, simply-connected topological 4-manifold. In particular | ||
| there exists such a manifold with the `E₈` form as intersection form (moreover because `E₈` is | ||
| even, this is the unique such manifold with this intersection form). However by Rokhlin's theorem | ||
| (or Donaldson's theorem) there is no (closed, oriented, simply-connected) smooth four-manifold with | ||
| this intersection form. |
There was a problem hiding this comment.
Using Casson invariant it's known that the E8 manifold isn't even triangulable, though to state this you'll have to define the geometric realization of an AbstractSimplicialComplex (should be easy, just take a disjoint union of stdSimplexes and quotient by an appropriate relation).
I've been wanting to state some results about PL manifolds too, but defining the PL/PDiff groupoids and proving results about them is probably a project suitable for TauCeti instead.
|
I really should write this elsewhere but as I only have a moment I'll note that it also occurred to me that Newlander-Nierenburg might make a great eval problem! |
2 participants
No description provided.