Documentation

TauCeti.Geometry.Diffeomorphism.Cerf

Cerf's theorem: the path components of Diff(S³) #

Cerf proved that every orientation-preserving diffeomorphism of the three-sphere is isotopic to the identity, that is, π₀ Diff⁺(S³) = 0. This file states that theorem against the weak Whitney topology on Diff(S³), as TauCeti.CerfTheorem, and records what follows about the path components of Diff(S³) from the dimension-independent results of TauCeti.Geometry.Diffeomorphism.Sphere.Isotopy.

The statement avoids orientations of diffeomorphisms by comparing with the orthogonal group: TauCeti.CerfTheorem says that every smooth diffeomorphism of S³ is joined, in Diff(S³), to the restriction of an orthogonal transformation of ℝ⁴, so the map π₀ O(4) → π₀ Diff(S³) induced by the reference inclusion TauCeti.orthogonalToDiffSphere is surjective. That map is injective in every dimension (TauCeti.joined_orthogonalToDiffSphere_iff): two orthogonal transformations of ℝⁿ⁺¹ are isotopic as diffeomorphisms of Sⁿ exactly when they have the same determinant. So Diff(Sⁿ) is never path-connected (TauCeti.not_pathConnectedSpace_diff_sphere), and Cerf's theorem is equivalent to Diff(S³) having exactly two path components (TauCeti.cerfTheorem_iff_natCard_zerothHomotopy_eq_two).

The orientation-free form is equivalent to Cerf's: a diffeomorphism isotopic to an orthogonal transformation of determinant -1 reverses orientation, so under TauCeti.CerfTheorem an orientation-preserving diffeomorphism is isotopic to an element of SO(4), hence to the identity; and conversely an orientation-reversing diffeomorphism composed with a reflection preserves orientation. Orientation-preservation of diffeomorphisms is not used here.

Cerf's theorem follows from the Smale conjecture Diff(S³) ≃ O(4) (Hatcher), since a homotopy equivalence is surjective on path components (TauCeti.SmaleConjecture.cerfTheorem). It is not proved here. Cerf's corollary Γ₄ = 0, that every diffeomorphism of S³ extends over the four-ball, is not stated here either.

Main definitions #

Main results #

References #

Cerf's theorem #

source
def TauCeti.CerfTheorem :
Prop

Cerf's theorem, π₀ Diff⁺(S³) = 0, in orientation-free form: every smooth diffeomorphism of the three-sphere is joined, in the weak Whitney topology, to the restriction of an orthogonal transformation of ℝ⁴. Together with TauCeti.joined_orthogonalToDiffSphere_iff this says that Diff(S³) has two path components, the isotopy classes of the identity and of a reflection (TauCeti.cerfTheorem_iff_natCard_zerothHomotopy_eq_two). It is stated, not proved.

Instances For
    source
    theorem TauCeti.SmaleConjecture.cerfTheorem (h : SmaleConjecture) :
    CerfTheorem

    The Smale conjecture implies Cerf's theorem. A homotopy equivalence is surjective on path components: if g is a homotopy inverse of the inclusion O(4) → Diff(S³), then every f is joined to the image of g f by the homotopy from the composite to the identity.

    source
    theorem TauCeti.cerfTheorem_iff_natCard_zerothHomotopy_eq_two :
    CerfTheorem ↔ Nat.card (ZerothHomotopy (Diff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 3))) ↑(Metric.sphere 0 1) ↑⊤)) = 2

    Cerf's theorem as a count of path components. Cerf's theorem holds exactly when the diffeomorphism group of S³ has two path components.