Composing smooth embeddings with diffeomorphisms

Mathlib defines Manifold.IsSmoothEmbedding as an immersion that is also a topological embedding, and lists Diffeomorph.isSmoothEmbedding as a TODO in Mathlib/Geometry/Manifold/SmoothEmbedding.lean, because a general composite of immersions has to combine two complements.

Composing with a diffeomorphism is elementary, and TauCeti/Geometry/Manifold/Immersion.lean settles it at the level of immersions: a diffeomorphism carries charts to charts, so both composites are immersions with the same complement. This file adds the topological half — composing with a diffeomorphism on either side preserves being a topological embedding — and packages the result as operations on the bundled type TauCeti.SmoothEmbedding.

Since the composition is transparent, the bundled operations are just reindexing: a TauCeti.SmoothEmbedding may be reparametrised by a diffeomorphism of its source (TauCeti.SmoothEmbedding.compDiffeomorph) or transported by a diffeomorphism of its target (TauCeti.SmoothEmbedding.transDiffeomorph). Reparametrisation leaves the image alone and transport moves it by the ambient diffeomorphism, and the two assemble into an action of the self-diffeomorphism group TauCeti.Diff of the target and a right action of that of the source; the two actions commute, which is recorded as a SMulCommClass instance.

This is the transport layer that layer 4 of the geometric-topology roadmap (TauCetiRoadmap/GeometricTopology/README.md) needs for its geometric presentations, where a knot presentation is a smooth embedding of the circle into the ambient manifold N: reversing the orientation of such a presentation and rotating its parametrisation are precisely precomposition with a diffeomorphism of the circle, while the ambient Diff(N)-action is postcomposition.

Main results

• TauCeti.isSmoothEmbedding_comp_diffeomorph and TauCeti.isSmoothEmbedding_diffeomorph_comp, with their _iff companions: smooth embeddings are stable under composition with a diffeomorphism on either side.
• TauCeti.isSmoothEmbedding_comp_continuousLinearEquiv: a smooth embedding of a vector space stays one after a linear change of coordinates of the source, which changes its model.
• Diffeomorph.isSmoothEmbedding_comp: from a boundaryless source, a diffeomorphism onto a boundaryless manifold with a different finite-dimensional model transports smooth embeddings.
• TauCeti.isSmoothEmbedding_diffeomorph: a diffeomorphism is a smooth embedding.
• TauCeti.isSmoothEmbedding_continuousLinearEquiv: a continuous linear equivalence between normed spaces is a smooth embedding.

Main definitions

• TauCeti.SmoothEmbedding.ofDiffeomorph: a diffeomorphism as a bundled smooth embedding.
• TauCeti.SmoothEmbedding.ofContinuousLinearEquiv: a continuous linear equivalence as a bundled smooth embedding.
• TauCeti.SmoothEmbedding.compDiffeomorph: reparametrise a bundled smooth embedding by a diffeomorphism of its source.
• TauCeti.SmoothEmbedding.transDiffeomorph: transport a bundled smooth embedding by a diffeomorphism of its target.
• the MulAction (Diff J N n) (SmoothEmbedding I J n M N) given by transport, and the reparametrisation action of (Diff I M n)ᵐᵒᵖ.

References

• M. Hirsch, Differential Topology, Springer GTM 33 (1976), Chapter 1, for immersions and embeddings and their behaviour under composition.

theorem TauCeti.isSmoothEmbedding_comp_diffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M'] {N : Type u_8} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} [IsManifold I n M'] (e : Diffeomorph I I M' M n) (h : Manifold.IsSmoothEmbedding I J n f) : Manifold.IsSmoothEmbedding I J n (f ∘ ⇑e)

Reparametrising a smooth embedding by a diffeomorphism of the source gives a smooth embedding.

theorem TauCeti.isSmoothEmbedding_comp_continuousLinearEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners 𝕜 E' G} {N : Type u_8} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {E₀ : Type u_10} [NormedAddCommGroup E₀] [NormedSpace 𝕜 E₀] {g : E → N} (e : E₀ ≃L[𝕜] E) (h : Manifold.IsSmoothEmbedding (modelWithCornersSelf 𝕜 E) J n g) : Manifold.IsSmoothEmbedding (modelWithCornersSelf 𝕜 E₀) J n (g ∘ ⇑e)

Precomposing a smooth embedding of a vector space with a continuous linear equivalence gives a smooth embedding, for the new source model.

theorem TauCeti.isSmoothEmbedding_diffeomorph_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_8} [TopologicalSpace N] [ChartedSpace G N] {P : Type u_9} [TopologicalSpace P] [ChartedSpace G P] {n : WithTop ℕ∞} {f : M → N} [IsManifold J n P] (h : Manifold.IsSmoothEmbedding I J n f) (e : Diffeomorph J J N P n) : Manifold.IsSmoothEmbedding I J n (⇑e ∘ f)

Transporting a smooth embedding by a diffeomorphism of the target gives a smooth embedding.

theorem TauCeti.isSmoothEmbedding_comp_diffeomorph_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M'] {N : Type u_8} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} [IsManifold I n M] [IsManifold I n M'] (e : Diffeomorph I I M' M n) : Manifold.IsSmoothEmbedding I J n (f ∘ ⇑e) ↔ Manifold.IsSmoothEmbedding I J n f

Precomposition with a diffeomorphism of the source neither creates nor destroys a smooth embedding.

theorem TauCeti.isSmoothEmbedding_diffeomorph_comp_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_8} [TopologicalSpace N] [ChartedSpace G N] {P : Type u_9} [TopologicalSpace P] [ChartedSpace G P] {n : WithTop ℕ∞} {f : M → N} [IsManifold J n N] [IsManifold J n P] (e : Diffeomorph J J N P n) : Manifold.IsSmoothEmbedding I J n (⇑e ∘ f) ↔ Manifold.IsSmoothEmbedding I J n f

Postcomposition with a diffeomorphism of the target neither creates nor destroys a smooth embedding.

theorem TauCeti.isSmoothEmbedding_diffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M'] {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold I n M'] (e : Diffeomorph I I M M' n) : Manifold.IsSmoothEmbedding I I n ⇑e

A diffeomorphism is a smooth embedding.

This is the statement Mathlib lists as the TODO Diffeomorph.isSmoothEmbedding in Mathlib/Geometry/Manifold/SmoothEmbedding.lean; the name is flat here because a Diffeomorph namespace nested in TauCeti would break dot notation on Mathlib's type.

theorem TauCeti.isSmoothEmbedding_continuousLinearEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {n : WithTop ℕ∞} (e : E ≃L[𝕜] E') : Manifold.IsSmoothEmbedding (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n ⇑e

A continuous linear equivalence between normed spaces is a smooth embedding.

theorem Diffeomorph.isSmoothEmbedding_comp {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} {E' : Type u_3} {E'' : Type u_4} {H : Type u_5} {G : Type u_6} {G' : Type u_7} {M : Type u_8} {N : Type u_9} {P : Type u_10} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [FiniteDimensional 𝕜 E''] [TopologicalSpace H] [TopologicalSpace G] [TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {K : ModelWithCorners 𝕜 E'' G'} [I.Boundaryless] [K.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] [TopologicalSpace P] [ChartedSpace G' P] {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold K n P] {f : M → N} (Φ : Diffeomorph J K N P n) (hn : 1 ≤ n) (h : Manifold.IsSmoothEmbedding I J n f) : Manifold.IsSmoothEmbedding I K n (⇑Φ ∘ f)

Transporting a smooth embedding from a boundaryless manifold by a diffeomorphism of the target onto a boundaryless manifold gives a smooth embedding, also when the new target has a different finite-dimensional model.

def TauCeti.SmoothEmbedding.ofDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M'] {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold I n M'] (e : Diffeomorph I I M M' n) : SmoothEmbedding I I n M M'

A diffeomorphism, as a bundled smooth embedding.

@[simp]

theorem TauCeti.SmoothEmbedding.ofDiffeomorph_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M'] {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold I n M'] (e : Diffeomorph I I M M' n) (x : M) : (ofDiffeomorph e) x = e x

@[simp]

theorem TauCeti.SmoothEmbedding.coe_ofDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M'] {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold I n M'] (e : Diffeomorph I I M M' n) : ⇑(ofDiffeomorph e) = ⇑e

def TauCeti.SmoothEmbedding.ofContinuousLinearEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {n : WithTop ℕ∞} (e : E ≃L[𝕜] E') : SmoothEmbedding (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n E E'

A continuous linear equivalence between normed spaces, as a bundled smooth embedding.

@[simp]

theorem TauCeti.SmoothEmbedding.ofContinuousLinearEquiv_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {n : WithTop ℕ∞} (e : E ≃L[𝕜] E') (x : E) : (ofContinuousLinearEquiv e) x = e x

@[simp]

theorem TauCeti.SmoothEmbedding.coe_ofContinuousLinearEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {n : WithTop ℕ∞} (e : E ≃L[𝕜] E') : ⇑(ofContinuousLinearEquiv e) = ⇑e

theorem TauCeti.SmoothEmbedding.range_ofDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M'] {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold I n M'] (e : Diffeomorph I I M M' n) : Set.range ⇑(ofDiffeomorph e) = Set.univ

A diffeomorphism is onto, so as a smooth embedding it has full image.

Not a simp lemma: coe_ofDiffeomorph already rewrites the left-hand side, so this form is never in normal form.

def TauCeti.SmoothEmbedding.compDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M'] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [IsManifold I n M'] (f : SmoothEmbedding I J n M N) (e : Diffeomorph I I M' M n) : SmoothEmbedding I J n M' N

Reparametrisation. A diffeomorphism e : M' ≃ₘ M of the source turns a bundled smooth embedding f : M → N into the bundled smooth embedding f ∘ e : M' → N. For a geometric knot presentation, an embedding of the circle into the ambient manifold N, this is the change of parametrisation of the knot, orientation reversal included.

@[simp]

theorem TauCeti.SmoothEmbedding.compDiffeomorph_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M'] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [IsManifold I n M'] (f : SmoothEmbedding I J n M N) (e : Diffeomorph I I M' M n) (x : M') : (f.compDiffeomorph e) x = f (e x)

@[simp]

theorem TauCeti.SmoothEmbedding.coe_compDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M'] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [IsManifold I n M'] (f : SmoothEmbedding I J n M N) (e : Diffeomorph I I M' M n) : ⇑(f.compDiffeomorph e) = ⇑f ∘ ⇑e

@[simp]

theorem TauCeti.SmoothEmbedding.compDiffeomorph_refl {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [IsManifold I n M] (f : SmoothEmbedding I J n M N) : f.compDiffeomorph (Diffeomorph.refl I M n) = f

Reparametrising by the identity diffeomorphism changes nothing.

@[simp]

theorem TauCeti.SmoothEmbedding.compDiffeomorph_compDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M'] {M'' : Type u_8} [TopologicalSpace M''] [ChartedSpace H M''] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [IsManifold I n M'] [IsManifold I n M''] (f : SmoothEmbedding I J n M N) (e : Diffeomorph I I M' M n) (e' : Diffeomorph I I M'' M' n) : (f.compDiffeomorph e).compDiffeomorph e' = f.compDiffeomorph (e'.trans e)

Reparametrising twice is reparametrising by the composite diffeomorphism.

theorem TauCeti.SmoothEmbedding.range_compDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M'] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [IsManifold I n M'] (f : SmoothEmbedding I J n M N) (e : Diffeomorph I I M' M n) : Set.range ⇑(f.compDiffeomorph e) = Set.range ⇑f

Reparametrisation does not move the image of an embedding.

Not a simp lemma: coe_compDiffeomorph already rewrites the left-hand side, so this form is never in normal form.

def TauCeti.SmoothEmbedding.transDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {P : Type u_10} [TopologicalSpace P] [ChartedSpace G P] {n : WithTop ℕ∞} [IsManifold J n P] (f : SmoothEmbedding I J n M N) (e : Diffeomorph J J N P n) : SmoothEmbedding I J n M P

Ambient transport. A diffeomorphism e : N ≃ₘ P of the target turns a bundled smooth embedding f : M → N into the bundled smooth embedding e ∘ f : M → P. For a geometric knot presentation this is the action of the ambient diffeomorphism group on knots.

@[simp]

theorem TauCeti.SmoothEmbedding.transDiffeomorph_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {P : Type u_10} [TopologicalSpace P] [ChartedSpace G P] {n : WithTop ℕ∞} [IsManifold J n P] (f : SmoothEmbedding I J n M N) (e : Diffeomorph J J N P n) (x : M) : (f.transDiffeomorph e) x = e (f x)

@[simp]

theorem TauCeti.SmoothEmbedding.coe_transDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {P : Type u_10} [TopologicalSpace P] [ChartedSpace G P] {n : WithTop ℕ∞} [IsManifold J n P] (f : SmoothEmbedding I J n M N) (e : Diffeomorph J J N P n) : ⇑(f.transDiffeomorph e) = ⇑e ∘ ⇑f

@[simp]

theorem TauCeti.SmoothEmbedding.transDiffeomorph_refl {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [IsManifold J n N] (f : SmoothEmbedding I J n M N) : f.transDiffeomorph (Diffeomorph.refl J N n) = f

Transporting by the identity diffeomorphism changes nothing.

@[simp]

theorem TauCeti.SmoothEmbedding.transDiffeomorph_transDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {P : Type u_10} [TopologicalSpace P] [ChartedSpace G P] {n : WithTop ℕ∞} {Q : Type u_11} [TopologicalSpace Q] [ChartedSpace G Q] [IsManifold J n P] [IsManifold J n Q] (f : SmoothEmbedding I J n M N) (e : Diffeomorph J J N P n) (e' : Diffeomorph J J P Q n) : (f.transDiffeomorph e).transDiffeomorph e' = f.transDiffeomorph (e.trans e')

Transporting twice is transporting by the composite diffeomorphism.

theorem TauCeti.SmoothEmbedding.range_transDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {P : Type u_10} [TopologicalSpace P] [ChartedSpace G P] {n : WithTop ℕ∞} [IsManifold J n P] (f : SmoothEmbedding I J n M N) (e : Diffeomorph J J N P n) : Set.range ⇑(f.transDiffeomorph e) = ⇑e '' Set.range ⇑f

Ambient transport moves the image of an embedding by the ambient diffeomorphism.

Not a simp lemma: coe_transDiffeomorph already rewrites the left-hand side, so this form is never in normal form.

@[simp]

theorem TauCeti.SmoothEmbedding.transDiffeomorph_compDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M'] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {P : Type u_10} [TopologicalSpace P] [ChartedSpace G P] {n : WithTop ℕ∞} [IsManifold I n M'] [IsManifold J n P] (f : SmoothEmbedding I J n M N) (e : Diffeomorph I I M' M n) (e' : Diffeomorph J J N P n) : (f.compDiffeomorph e).transDiffeomorph e' = (f.transDiffeomorph e').compDiffeomorph e

Reparametrising and transporting commute: they act on opposite sides of the embedding. This is the normal form for a mixed reparametrisation-and-transport, with the transport innermost.

@[instance_reducible]

instance TauCeti.SmoothEmbedding.instMulActionDiff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [IsManifold J n N] : MulAction (Diff J N n) (SmoothEmbedding I J n M N)

The self-diffeomorphism group of the target acts on the smooth embeddings into it, by ambient transport. This is the action of Diff(N) on geometric knot presentations in N.

@[simp]

theorem TauCeti.SmoothEmbedding.smul_def {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [IsManifold J n N] (e : Diff J N n) (f : SmoothEmbedding I J n M N) : e • f = f.transDiffeomorph e

@[instance_reducible]

instance TauCeti.SmoothEmbedding.instMulActionMulOppositeDiff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [IsManifold I n M] : MulAction (Diff I M n)ᵐᵒᵖ (SmoothEmbedding I J n M N)

The self-diffeomorphism group of the source acts on the smooth embeddings out of it on the right, by reparametrisation; the action is recorded on the opposite group.

@[simp]

theorem TauCeti.SmoothEmbedding.unop_smul_def {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [IsManifold I n M] (a : (Diff I M n)ᵐᵒᵖ) (f : SmoothEmbedding I J n M N) : a • f = f.compDiffeomorph (MulOpposite.unop a)

instance TauCeti.SmoothEmbedding.instSMulCommClassDiff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold J n N] : SMulCommClass (Diff J N n) (Diff I M n)ᵐᵒᵖ (SmoothEmbedding I J n M N)

Ambient transport and reparametrisation commute, so the two actions are compatible.