Smooth ambient isotopies

A Diffeotopy J n M is a C^n motion of a real manifold M through self-diffeomorphisms, starting at the identity. It is bundled by its level-preserving total diffeomorphism of I × M: this makes invertibility in the time and space variables part of the data and ensures that no unrelated choices of inverse maps are carried by the structure.

The time interval is Mathlib's unitInterval, with its manifold-with-boundary structure modelled on 𝓡∂ 1. The total diffeomorphism is required to preserve the time coordinate. Its slice at each t : I is therefore a self-diffeomorphism of M; Diffeotopy.timeSlice packages that fact. Diffeotopies coerce to their spatial component, so Φ (t, x) is the point of M reached from x at time t. Diffeotopies compose and invert, and forgetting smoothness gives the existing TauCeti.AmbientIsotopy.

This supplies the smooth ambient-isotopy half of the geometric-topology roadmap's requirement that isotopy notions be defined generally before they are specialized to knots. The non-ambient smooth isotopy of arbitrary maps is separate and is not defined here. The specialization to bundled smooth embeddings, used for geometric knot presentations, is in TauCeti.Geometry.Manifold.SmoothEmbedding.SmoothAmbientIsotopy.Basic.

Main definitions

• TauCeti.Diffeotopy: a level-preserving diffeomorphism of I × M starting at the identity.
• TauCeti.Diffeotopy.timeSlice: the self-diffeomorphism of M at a fixed time.
• TauCeti.Diffeotopy.final: the self-diffeomorphism at time one.
• TauCeti.Diffeotopy.refl, trans, and symm: the constant, composite, and inverse diffeotopies.
• TauCeti.Diffeotopy.toAmbientIsotopy: forget smoothness to obtain a continuous ambient isotopy.

Main results

• TauCeti.Diffeotopy.timeSlice_trans and timeSlice_symm: time slices commute with composition and inversion.
• TauCeti.Diffeotopy.final_trans and final_symm: the corresponding calculus for final diffeomorphisms.
• TauCeti.Diffeotopy.toAmbientIsotopy_final_apply: forgetting smoothness preserves the final action.

References

• G. Burde and H. Zieschang, Knots, 2nd ed., de Gruyter (2003), Chapter 1, for ambient isotopy of knots.
• M. Hirsch, Differential Topology, Springer GTM 33 (1976), Chapter 8, §8.1, for smooth isotopies and diffeotopies.

structure TauCeti.Diffeotopy {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (J : ModelWithCorners ℝ E H) (n : WithTop ℕ∞) (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] : Type u_4

A C^n diffeotopy of a real manifold M: a level-preserving diffeomorphism of I × M which is the identity at time zero.

Bundling the level-preserving total map as a Diffeomorph makes every time slice invertible and makes its inverse canonical.

• toDiffeomorph : Diffeomorph ((modelWithCornersEuclideanHalfSpace 1).prod J) ((modelWithCornersEuclideanHalfSpace 1).prod J) (↑unitInterval × M) (↑unitInterval × M) n

  The level-preserving total diffeomorphism of I × M.

• fst_apply (p : ↑unitInterval × M) : (self.toDiffeomorph p).1 = p.1

  The total diffeomorphism preserves the time coordinate.

• snd_apply_zero' (x : M) : (self.toDiffeomorph (0, x)).2 = x

  The motion starts at the identity.

@[instance_reducible]

instance TauCeti.Diffeotopy.instCoeFun {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} : CoeFun (Diffeotopy J n M) fun (x : Diffeotopy J n M) => ↑unitInterval × M → M

Apply a diffeotopy as Φ (t, x): the spatial component of the total diffeomorphism.

Equations

• TauCeti.Diffeotopy.instCoeFun = { coe := fun (Φ : TauCeti.Diffeotopy J n M) (p : ↑unitInterval × M) => (Φ.toDiffeomorph p).2 }

Ambient coordinate changes

noncomputable def TauCeti.Diffeotopy.transDiffeomorph {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {P : Type u_4} [TopologicalSpace P] [ChartedSpace H P] (f : Diffeomorph J J M P n) (Φ : Diffeotopy J n M) : Diffeotopy J n P

Transport a diffeotopy across an ambient diffeomorphism by conjugation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Diffeotopy.transDiffeomorph_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {P : Type u_4} [TopologicalSpace P] [ChartedSpace H P] (f : Diffeomorph J J M P n) (Φ : Diffeotopy J n M) (p : ↑unitInterval × P) : (fun (p : ↑unitInterval × P) => ((transDiffeomorph f Φ).toDiffeomorph p).2) p = f ((fun (p : ↑unitInterval × M) => (Φ.toDiffeomorph p).2) (p.1, f.symm p.2))

@[simp]

theorem TauCeti.Diffeotopy.coe_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) (p : ↑unitInterval × M) : (fun (p : ↑unitInterval × M) => (Φ.toDiffeomorph p).2) p = (Φ.toDiffeomorph p).2

Applying a diffeotopy returns the spatial component of its total diffeomorphism.

theorem TauCeti.Diffeotopy.toDiffeomorph_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) (p : ↑unitInterval × M) : Φ.toDiffeomorph p = (p.1, (fun (p : ↑unitInterval × M) => (Φ.toDiffeomorph p).2) p)

The total diffeomorphism of a diffeotopy sends (t, x) to (t, Φ (t, x)).

@[simp]

theorem TauCeti.Diffeotopy.apply_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) (x : M) : (fun (p : ↑unitInterval × M) => (Φ.toDiffeomorph p).2) (0, x) = x

A diffeotopy starts at the identity.

theorem TauCeti.Diffeotopy.contMDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) : ContMDiff ((modelWithCornersEuclideanHalfSpace 1).prod J) J n fun (p : ↑unitInterval × M) => (Φ.toDiffeomorph p).2

A diffeotopy is a C^n map of time and space into the ambient manifold.

@[simp]

theorem TauCeti.Diffeotopy.fst_symm_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) (p : ↑unitInterval × M) : (Φ.toDiffeomorph.symm p).1 = p.1

The inverse total diffeomorphism also preserves the time coordinate.

theorem TauCeti.Diffeotopy.toDiffeomorph_symm_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) (p : ↑unitInterval × M) : Φ.toDiffeomorph.symm p = (p.1, (Φ.toDiffeomorph.symm p).2)

The inverse total diffeomorphism sends p to its time coordinate paired with its spatial component.

noncomputable def TauCeti.Diffeotopy.timeSlice {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) (t : ↑unitInterval) : Diffeomorph J J M M n

The time-t slice of a diffeotopy, bundled as a self-diffeomorphism of M.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Diffeotopy.timeSlice_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) (t : ↑unitInterval) (x : M) : (Φ.timeSlice t) x = (fun (p : ↑unitInterval × M) => (Φ.toDiffeomorph p).2) (t, x)

Evaluating the time-t diffeomorphism is evaluating the diffeotopy at (t, x).

@[simp]

theorem TauCeti.Diffeotopy.timeSlice_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) : Φ.timeSlice 0 = Diffeomorph.refl J M n

The time-zero slice of a diffeotopy is the identity diffeomorphism.

noncomputable def TauCeti.Diffeotopy.final {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) : Diffeomorph J J M M n

The time-1 self-diffeomorphism of a diffeotopy.

Equations

• Φ.final = Φ.timeSlice 1

theorem TauCeti.Diffeotopy.final_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) : Φ.final = Φ.timeSlice 1

The final diffeomorphism is the time-one slice.

@[simp]

theorem TauCeti.Diffeotopy.final_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) (x : M) : Φ.final x = (fun (p : ↑unitInterval × M) => (Φ.toDiffeomorph p).2) (1, x)

The final diffeomorphism acts by the time-one slice.

noncomputable def TauCeti.Diffeotopy.refl {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (J : ModelWithCorners ℝ E H) (n : WithTop ℕ∞) (M : Type u_5) [TopologicalSpace M] [ChartedSpace H M] : Diffeotopy J n M

The constant diffeotopy at the identity.

Equations

• TauCeti.Diffeotopy.refl J n M = { toDiffeomorph := Diffeomorph.refl ((modelWithCornersEuclideanHalfSpace 1).prod J) (↑unitInterval × M) n, fst_apply := ⋯, snd_apply_zero' := ⋯ }

@[simp]

theorem TauCeti.Diffeotopy.refl_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (p : ↑unitInterval × M) : (fun (p : ↑unitInterval × M) => ((refl J n M).toDiffeomorph p).2) p = p.2

The constant diffeotopy fixes every point at every time.

@[simp]

theorem TauCeti.Diffeotopy.timeSlice_refl {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (t : ↑unitInterval) : (refl J n M).timeSlice t = Diffeomorph.refl J M n

The time slice of the constant diffeotopy is the identity.

@[simp]

theorem TauCeti.Diffeotopy.final_refl {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} : (refl J n M).final = Diffeomorph.refl J M n

The final diffeomorphism of the constant diffeotopy is the identity.

noncomputable def TauCeti.Diffeotopy.trans {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ Ψ : Diffeotopy J n M) : Diffeotopy J n M

Compose two diffeotopies pointwise, first Φ and then Ψ.

Equations

• Φ.trans Ψ = { toDiffeomorph := Φ.toDiffeomorph.trans Ψ.toDiffeomorph, fst_apply := ⋯, snd_apply_zero' := ⋯ }

@[simp]

theorem TauCeti.Diffeotopy.trans_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ Ψ : Diffeotopy J n M) (p : ↑unitInterval × M) : (fun (p : ↑unitInterval × M) => ((Φ.trans Ψ).toDiffeomorph p).2) p = (fun (p : ↑unitInterval × M) => (Ψ.toDiffeomorph p).2) (p.1, (fun (p : ↑unitInterval × M) => (Φ.toDiffeomorph p).2) p)

Evaluating a composite diffeotopy applies Φ and then Ψ at the same time.

@[simp]

theorem TauCeti.Diffeotopy.timeSlice_trans {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ Ψ : Diffeotopy J n M) (t : ↑unitInterval) : (Φ.trans Ψ).timeSlice t = (Φ.timeSlice t).trans (Ψ.timeSlice t)

The time slice of a composite diffeotopy is the composite of its time slices.

@[simp]

theorem TauCeti.Diffeotopy.final_trans {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ Ψ : Diffeotopy J n M) : (Φ.trans Ψ).final = Φ.final.trans Ψ.final

The final diffeomorphism of a composite diffeotopy is the composite of the final diffeomorphisms.

noncomputable def TauCeti.Diffeotopy.symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) : Diffeotopy J n M

Reverse a diffeotopy by taking the inverse of its level-preserving total diffeomorphism.

Equations

• Φ.symm = { toDiffeomorph := Φ.toDiffeomorph.symm, fst_apply := ⋯, snd_apply_zero' := ⋯ }

@[simp]

theorem TauCeti.Diffeotopy.symm_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) (p : ↑unitInterval × M) : (fun (p : ↑unitInterval × M) => (Φ.symm.toDiffeomorph p).2) p = (Φ.toDiffeomorph.symm p).2

Evaluating the inverse diffeotopy uses the spatial component of the inverse total diffeomorphism.

@[simp]

theorem TauCeti.Diffeotopy.symm_timeSlice_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) (t : ↑unitInterval) (x : M) : (Φ.timeSlice t).symm x = (fun (p : ↑unitInterval × M) => (Φ.symm.toDiffeomorph p).2) (t, x)

The inverse of the time-t slice acts by the inverse diffeotopy at time t.

@[simp]

theorem TauCeti.Diffeotopy.timeSlice_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) (t : ↑unitInterval) : Φ.symm.timeSlice t = (Φ.timeSlice t).symm

The time slice of the inverse diffeotopy is the inverse time slice.

@[simp]

theorem TauCeti.Diffeotopy.symm_apply_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) (p : ↑unitInterval × M) : (Φ.toDiffeomorph.symm (p.1, (Φ.toDiffeomorph p).2)).2 = p.2

A diffeotopy followed by its inverse fixes every point.

@[simp]

theorem TauCeti.Diffeotopy.apply_symm_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) (p : ↑unitInterval × M) : (Φ.toDiffeomorph (p.1, (Φ.toDiffeomorph.symm p).2)).2 = p.2

The inverse diffeotopy followed by the original fixes every point.

@[simp]

theorem TauCeti.Diffeotopy.final_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) : Φ.symm.final = Φ.final.symm

The final diffeomorphism of the inverse diffeotopy is the inverse final diffeomorphism.

def TauCeti.Diffeotopy.toAmbientIsotopy {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) : AmbientIsotopy M

Forgetting smoothness turns a diffeotopy into a continuous ambient isotopy.

Equations

• Φ.toAmbientIsotopy = { toFun := fun (p : ↑unitInterval × M) => (Φ.toDiffeomorph p).2, continuous_toFun := ⋯, isHomeomorph_total' := ⋯, map_zero_left' := ⋯ }

@[simp]

theorem TauCeti.Diffeotopy.toAmbientIsotopy_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) (p : ↑unitInterval × M) : Φ.toAmbientIsotopy.toContinuousMap p = (fun (p : ↑unitInterval × M) => (Φ.toDiffeomorph p).2) p

Forgetting smoothness does not change the ambient motion.

@[simp]

theorem TauCeti.Diffeotopy.toAmbientIsotopy_final_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) (x : M) : Φ.toAmbientIsotopy.final x = Φ.final x

Forgetting smoothness commutes with taking the final map.

@[simp]

theorem TauCeti.Diffeotopy.toAmbientIsotopy_trans {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ Ψ : Diffeotopy J n M) : (Φ.trans Ψ).toAmbientIsotopy = Φ.toAmbientIsotopy.trans Ψ.toAmbientIsotopy

Forgetting smoothness commutes with composition of diffeotopies.

@[simp]

theorem TauCeti.Diffeotopy.toAmbientIsotopy_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) : Φ.symm.toAmbientIsotopy = Φ.toAmbientIsotopy.symm

Forgetting smoothness commutes with inversion of diffeotopies.

theorem TauCeti.Diffeotopy.ext {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {Φ Ψ : Diffeotopy J n M} (h : ∀ (p : ↑unitInterval × M), (fun (p : ↑unitInterval × M) => (Φ.toDiffeomorph p).2) p = (fun (p : ↑unitInterval × M) => (Ψ.toDiffeomorph p).2) p) : Φ = Ψ

Two diffeotopies are equal when their ambient motions agree pointwise.

theorem TauCeti.Diffeotopy.ext_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {Φ Ψ : Diffeotopy J n M} : Φ = Ψ ↔ ∀ (p : ↑unitInterval × M), (fun (p : ↑unitInterval × M) => (Φ.toDiffeomorph p).2) p = (fun (p : ↑unitInterval × M) => (Ψ.toDiffeomorph p).2) p

@[simp]

theorem TauCeti.Diffeotopy.refl_trans {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) : (refl J n M).trans Φ = Φ

The constant diffeotopy is a left identity for composition.

@[simp]

theorem TauCeti.Diffeotopy.trans_refl {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) : Φ.trans (refl J n M) = Φ

The constant diffeotopy is a right identity for composition.

theorem TauCeti.Diffeotopy.trans_assoc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ Ψ Θ : Diffeotopy J n M) : (Φ.trans Ψ).trans Θ = Φ.trans (Ψ.trans Θ)

Composition of diffeotopies is associative.

@[simp]

theorem TauCeti.Diffeotopy.symm_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) : Φ.symm.symm = Φ

Inverting a diffeotopy twice recovers the original diffeotopy.

@[simp]

theorem TauCeti.Diffeotopy.self_trans_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) : Φ.trans Φ.symm = refl J n M

A diffeotopy followed by its inverse is the constant diffeotopy.

@[simp]

theorem TauCeti.Diffeotopy.symm_trans_self {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) : Φ.symm.trans Φ = refl J n M

A diffeotopy inverse followed by the original is the constant diffeotopy.