Documentation

TauCeti.Geometry.Diffeomorphism.Diffeotopy.Homogeneity

Homogeneity of connected manifolds #

For any two points x and y of a connected open subset U of a finite-dimensional boundaryless manifold M, some diffeotopy of M which fixes every point outside a compact subset of U carries x to y. In particular the diffeomorphisms of a connected manifold isotopic to the identity act transitively on it.

Near a point x, take a bump function ρ in a chart around x and, for a nearby point y, the vector field ρ • (y - x) read in that chart (TauCeti.bumpChartField). Extended by zero, it is a compactly supported vector field on M whose flow line through x is the straight segment from x to y in the chart, so its compactly supported flow diffeotopy moves x to y. Diffeotopies compose and invert, and the points reachable in this way from a given point form an open and closed subset of U.

This is the first step in comparing two ball embeddings in a connected manifold (the disc theorem): it moves the centre of one ball to the centre of the other.

Main results #

References #

Homogeneity #

theorem TauCeti.eventually_exists_diffeotopy_final_apply_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [T2Space M] [BoundarylessManifold I M] {n : WithTop ℕ∞} [IsManifold I n M] {m : ℕ∞} (hm : 1 ≤ m) (hmn : ↑m + 1 ≤ n) {U : Set M} (hU : IsOpen U) {x : M} (hx : x ∈ U) :
∀ᶠ (y : M) in nhds x, ∃ (Φ : Diffeotopy I (↑m) M) (K : Set M), IsCompact K ∧ K ⊆ U ∧ (∀ (t : ↑unitInterval), Set.EqOn (fun (z : M) => (fun (p : ↑unitInterval × M) => (Φ.toDiffeomorph p).2) (t, z)) id Kᶜ) ∧ Φ.final x = y

Every point near x is reached from x by a diffeotopy fixing everything outside a compact subset of a given open neighbourhood U of x.

theorem TauCeti.exists_diffeotopy_final_apply_eq_of_isPreconnected {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [T2Space M] [BoundarylessManifold I M] {n : WithTop ℕ∞} [IsManifold I n M] {m : ℕ∞} (hm : 1 ≤ m) (hmn : ↑m + 1 ≤ n) {U : Set M} (hU : IsOpen U) (hUc : IsPreconnected U) {x y : M} (hx : x ∈ U) (hy : y ∈ U) :
∃ (Φ : Diffeotopy I (↑m) M) (K : Set M), IsCompact K ∧ K ⊆ U ∧ (∀ (t : ↑unitInterval), Set.EqOn (fun (z : M) => (fun (p : ↑unitInterval × M) => (Φ.toDiffeomorph p).2) (t, z)) id Kᶜ) ∧ Φ.final x = y

Homogeneity lemma. For two points x and y of a preconnected open subset U of a finite-dimensional boundaryless manifold, some diffeotopy fixing everything outside a compact subset of U has final map sending x to y. For a C^n manifold the diffeotopy is C^m for every m with 1 ≤ m and m + 1 ≤ n; in particular it is smooth on a smooth manifold.

theorem TauCeti.exists_diffeotopy_final_apply_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [T2Space M] [BoundarylessManifold I M] {n : WithTop ℕ∞} [IsManifold I n M] {m : ℕ∞} [PreconnectedSpace M] (hm : 1 ≤ m) (hmn : ↑m + 1 ≤ n) (x y : M) :
∃ (Φ : Diffeotopy I (↑m) M) (K : Set M), IsCompact K ∧ (∀ (t : ↑unitInterval), Set.EqOn (fun (z : M) => (fun (p : ↑unitInterval × M) => (Φ.toDiffeomorph p).2) (t, z)) id Kᶜ) ∧ Φ.final x = y

Homogeneity lemma. For two points x and y of a connected finite-dimensional boundaryless manifold, some compactly supported diffeotopy has final map sending x to y. For a C^n manifold the diffeotopy is C^m for every m with 1 ≤ m and m + 1 ≤ n.