Smooth concordance of smooth embeddings #
This file defines a globally collared smooth concordance between two smooth embeddings
f g : M → N. To avoid manifolds with boundary, a concordance is a C^n embedding
F : M × ℝ → N × ℝ which is a collared track from f to g (TauCeti.IsCollaredTrack): the
product f × id and g × id on uniform positive-width neighborhoods of the initial and final
ends, mapping M × (0, 1) into N × (0, 1).
Its restriction to M × [0, 1] is an ordinary smooth concordance which is a product near both
ends. The uniform collar widths are part of the data here, so this is stronger than merely requiring
an ordinary smooth concordance; no converse is asserted for noncompact M. The product ends make
globally collared concordances stack smoothly. For knots, M is the circle and the track is an
annulus in N × [0, 1]; this is the relation underlying the knot concordance group.
The relation is defined here for arbitrary smooth embeddings, in line with defining isotopy once
for general maps; smooth knot concordance is the case of TauCeti.SmoothCircleEmbedding, whose
source is the circle.
Main definitions #
TauCeti.SmoothEmbedding.Concordance f g: aC^nconcordance fromftog, in collared form.TauCeti.SmoothEmbedding.conjTime: a smooth embedding ofM × ℝintoN × ℝconjugated by an affine change of time, as a smooth embedding.TauCeti.SmoothEmbedding.Concordance.refl,symm,trans: the constant concordance, the reversed concordance, and the stacked concordance.TauCeti.SmoothEmbedding.Concordance.ofDiffeotopy: the trace of a diffeotopy, a concordance from an embedding to its image under the final diffeomorphism.TauCeti.SmoothEmbedding.Concordance.ofSmoothIsotopy: the collared trace of a compact-source smooth isotopy, as a concordance.TauCeti.SmoothEmbedding.Concordance.ofSourceDiffeotopy: the trace of a diffeotopy of the source, a concordance from an embedding to its reparametrization by the final diffeomorphism.TauCeti.SmoothEmbedding.Concordance.ofDiffeotopies: the trace of a diffeotopy of the target and one of the source run together, a concordance fromftoΦ.final ∘ f ∘ Ψ.final.TauCeti.SmoothEmbedding.Concordance.collaredSmoothTransitionUnit: the time reparametrization of these traces, a smooth transition from0to1constant near both ends.TauCeti.SmoothEmbedding.Concordant: the concordance relation.
Main results #
TauCeti.SmoothEmbedding.Concordant.equivalence: for a finite-dimensional ambient model, concordance is an equivalence relation.TauCeti.SmoothEmbedding.SmoothAmbientIsotopic.concordant: smoothly ambient isotopic embeddings are concordant.TauCeti.SmoothEmbedding.Concordant.of_smoothIsotopic: smoothly isotopic embeddings of a compact boundaryless source into a finite-dimensional Hausdorff boundaryless target are concordant.
Implementation notes #
Everything about a concordance that does not depend on the smoothness of its track — the time-level
lemmas, the reversed track TauCeti.reverseTime and the stacked track TauCeti.stack with its
embedding property — is inherited from TauCeti.IsCollaredTrack; this file only supplies the
smoothness of the reversed and stacked tracks. Stacking two concordances glues two immersions along
an open cover. Mathlib's Manifold.IsImmersion requires a single complement for all points, so the
glued map is shown to be an immersion with TauCeti.isImmersion_iff_forall_isImmersionAt, which
needs the model of N to be finite-dimensional. The same criterion for the isotopy track
requires that assumption in ofSmoothIsotopy as well as trans and statements depending on them.
The traces of diffeotopies and smooth isotopies are reparametrized by Real.smoothTransition,
which is C^∞ but not analytic; ofDiffeotopy, ofSourceDiffeotopy, ofDiffeotopies and
ofSmoothIsotopy therefore assume n ≤ ∞.
References #
- J. F. P. Hudson, Concordance, isotopy, and diffeotopy, Ann. of Math. 91 (1970), 425–448, for concordance of embeddings.
- C. Livingston, A survey of classical knot concordance, in Handbook of Knot Theory (2005), Section 2, for knot concordance.
structure
TauCeti.SmoothEmbedding.Concordance
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
(f g : SmoothEmbedding I J n M N)
:
Type (max u_5 u_6)
A C^n concordance from the smooth embedding f to the smooth embedding g, in collared
form: a C^n embedding of M × ℝ into N × ℝ which is f × id and g × id on neighborhoods
of the initial and final ends, and maps M × (0, 1) into N × (0, 1).
- toSmoothEmbedding : SmoothEmbedding (I.prod (modelWithCornersSelf ℝ ℝ)) (J.prod (modelWithCornersSelf ℝ ℝ)) n (M × ℝ) (N × ℝ)
The track of the concordance, a smooth embedding of
M × ℝintoN × ℝ. - isCollaredTrack_toSmoothEmbedding : IsCollaredTrack ⇑f ⇑g ⇑self.toSmoothEmbedding
Instances For
def
TauCeti.SmoothEmbedding.Concordant
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
(f g : SmoothEmbedding I J n M N)
:
Two smooth embeddings are concordant when there is a concordance from one to the other.
Instances For
theorem
TauCeti.SmoothEmbedding.concordant_iff_nonempty
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
:
Two smooth embeddings are concordant exactly when their concordance type is nonempty.
Affine changes of time #
noncomputable def
TauCeti.SmoothEmbedding.conjTime
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
[IsManifold I n M]
[IsManifold J n N]
(T : SmoothEmbedding (I.prod (modelWithCornersSelf ℝ ℝ)) (J.prod (modelWithCornersSelf ℝ ℝ)) n (M × ℝ) (N × ℝ))
(a b : ℝ)
(ha : a ≠ 0)
:
SmoothEmbedding (I.prod (modelWithCornersSelf ℝ ℝ)) (J.prod (modelWithCornersSelf ℝ ℝ)) n (M × ℝ) (N × ℝ)
The conjugate TauCeti.conjTime T a b of a smooth embedding T of M × ℝ into N × ℝ by the
affine change of time t ↦ a * t + b, a ≠ 0, as a smooth embedding.
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.coe_conjTime
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
[IsManifold I n M]
[IsManifold J n N]
(T : SmoothEmbedding (I.prod (modelWithCornersSelf ℝ ℝ)) (J.prod (modelWithCornersSelf ℝ ℝ)) n (M × ℝ) (N × ℝ))
(a b : ℝ)
(ha : a ≠ 0)
:
The underlying map of the conjugate smooth embedding is the conjugate map.
@[instance_reducible]
noncomputable instance
TauCeti.SmoothEmbedding.Concordance.instFunLike
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
:
@[simp]
theorem
TauCeti.SmoothEmbedding.Concordance.coe_toSmoothEmbedding
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
(F : f.Concordance g)
:
The underlying map of a concordance is that of its track.
theorem
TauCeti.SmoothEmbedding.Concordance.ext
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
{F G : f.Concordance g}
(hFG : ∀ (p : M × ℝ), F p = G p)
:
Two concordances with the same track are equal.
theorem
TauCeti.SmoothEmbedding.Concordance.ext_iff
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
{F G : f.Concordance g}
:
theorem
TauCeti.SmoothEmbedding.Concordance.isCollaredTrack
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
(F : f.Concordance g)
:
IsCollaredTrack ⇑f ⇑g ⇑F
The track of a concordance is a collared track from f to g.
@[simp]
theorem
TauCeti.SmoothEmbedding.Concordance.apply_zero
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
(F : f.Concordance g)
(x : M)
:
At time 0 a concordance is its initial embedding.
@[simp]
theorem
TauCeti.SmoothEmbedding.Concordance.apply_one
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
(F : f.Concordance g)
(x : M)
:
At time 1 a concordance is its final embedding.
Diffeomorphisms #
noncomputable def
TauCeti.SmoothEmbedding.Concordance.transDiffeomorph
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
{P : Type u_8}
[TopologicalSpace P]
[ChartedSpace H' P]
[IsManifold J n P]
(F : f.Concordance g)
(e : Diffeomorph J J N P n)
:
(f.transDiffeomorph e).Concordance (g.transDiffeomorph e)
An ambient diffeomorphism carries a concordance from f to g to one between the
transported embeddings.
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.Concordance.transDiffeomorph_apply
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
{P : Type u_8}
[TopologicalSpace P]
[ChartedSpace H' P]
[IsManifold J n P]
(F : f.Concordance g)
(e : Diffeomorph J J N P n)
(p : M × ℝ)
:
noncomputable def
TauCeti.SmoothEmbedding.Concordance.compDiffeomorph
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M']
[IsManifold I n M']
(F : f.Concordance g)
(e : Diffeomorph I I M' M n)
:
(f.compDiffeomorph e).Concordance (g.compDiffeomorph e)
A diffeomorphism of the source reparametrizes a concordance from f to g into one between
the reparametrized embeddings.
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.Concordance.compDiffeomorph_apply
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M']
[IsManifold I n M']
(F : f.Concordance g)
(e : Diffeomorph I I M' M n)
(p : M' × ℝ)
:
The constant and the reversed concordance #
noncomputable def
TauCeti.SmoothEmbedding.Concordance.refl
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
[IsManifold I n M]
[IsManifold J n N]
(f : SmoothEmbedding I J n M N)
:
f.Concordance f
The constant concordance from f to itself, whose track is f × id.
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.Concordance.refl_apply
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
[IsManifold I n M]
[IsManifold J n N]
(f : SmoothEmbedding I J n M N)
(p : M × ℝ)
:
noncomputable def
TauCeti.SmoothEmbedding.Concordance.symm
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
[IsManifold I n M]
[IsManifold J n N]
(F : f.Concordance g)
:
g.Concordance f
The reversed concordance from g to f, obtained by reflecting time in 1 / 2.
Instances For
theorem
TauCeti.SmoothEmbedding.Concordance.coe_symm
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
[IsManifold I n M]
[IsManifold J n N]
(F : f.Concordance g)
:
The track of the reversed concordance is the reversed track.
@[simp]
theorem
TauCeti.SmoothEmbedding.Concordance.symm_apply
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
[IsManifold I n M]
[IsManifold J n N]
(F : f.Concordance g)
(x : M)
(t : ℝ)
:
@[simp]
theorem
TauCeti.SmoothEmbedding.Concordance.symm_symm
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
[IsManifold I n M]
[IsManifold J n N]
(F : f.Concordance g)
:
Reversing a concordance twice gives it back.
Stacking concordances #
noncomputable def
TauCeti.SmoothEmbedding.Concordance.trans
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g h : SmoothEmbedding I J n M N}
[IsManifold I n M]
[IsManifold J n N]
[FiniteDimensional ℝ E']
(F : f.Concordance g)
(G : g.Concordance h)
:
f.Concordance h
The stacked concordance from f to h: the concordance F from f to g at triple speed
during [0, 1/3], then the constant concordance at g, then the concordance G from g to h
at triple speed during [2/3, 1].
Instances For
theorem
TauCeti.SmoothEmbedding.Concordance.coe_trans
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g h : SmoothEmbedding I J n M N}
[IsManifold I n M]
[IsManifold J n N]
[FiniteDimensional ℝ E']
(F : f.Concordance g)
(G : g.Concordance h)
:
The track of the stacked concordance is the stacked track.
theorem
TauCeti.SmoothEmbedding.Concordance.trans_apply_of_le
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g h : SmoothEmbedding I J n M N}
[IsManifold I n M]
[IsManifold J n N]
[FiniteDimensional ℝ E']
(F : f.Concordance g)
(G : g.Concordance h)
(x : M)
{t : ℝ}
(ht : t ≤ 1 / 2)
:
Before time 1 / 2 the stacked concordance runs the first concordance at triple speed.
theorem
TauCeti.SmoothEmbedding.Concordance.trans_apply_of_lt
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g h : SmoothEmbedding I J n M N}
[IsManifold I n M]
[IsManifold J n N]
[FiniteDimensional ℝ E']
(F : f.Concordance g)
(G : g.Concordance h)
(x : M)
{t : ℝ}
(ht : 1 / 2 < t)
:
After time 1 / 2 the stacked concordance runs the second concordance at triple speed.
Diffeotopies #
The time reparametrization t ↦ Real.smoothTransition (2 * t - 1 / 2) of the traces of
diffeotopies, as a map into the unit interval: a smooth transition from 0 to 1 which is
constant on neighborhoods of both ends of the unit interval.
Instances For
@[simp]
The collared smooth transition at t is Real.smoothTransition (2 * t - 1 / 2).
theorem
TauCeti.SmoothEmbedding.Concordance.contMDiff_collaredSmoothTransitionUnit
{n : WithTop ℕ∞}
(hn : n ≤ ↑⊤)
:
The collared smooth transition is C^n for every n ≤ ∞.
The collared smooth transition is continuous.
theorem
TauCeti.SmoothEmbedding.Concordance.collaredSmoothTransitionUnit_eq_zero_of_le
{t : ℝ}
(ht : t ≤ 1 / 4)
:
The collared smooth transition is 0 up to time 1 / 4.
theorem
TauCeti.SmoothEmbedding.Concordance.collaredSmoothTransitionUnit_eq_one_of_ge
{t : ℝ}
(ht : 3 / 4 ≤ t)
:
The collared smooth transition is 1 from time 3 / 4 on.
noncomputable def
TauCeti.SmoothEmbedding.Concordance.ofDiffeotopy
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
[IsManifold I n M]
[IsManifold J n N]
(hn : n ≤ ↑⊤)
(Φ : Diffeotopy J n N)
(f : SmoothEmbedding I J n M N)
:
f.Concordance (f.transDiffeomorph Φ.final)
The trace of a diffeotopy Φ of N: the concordance (x, t) ↦ (Φ (ρ t, f x), t) from f
to its image under the final diffeomorphism of Φ, where
ρ(t) = Real.smoothTransition (2 * t - 1 / 2).
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.Concordance.ofDiffeotopy_apply
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
[IsManifold I n M]
[IsManifold J n N]
(hn : n ≤ ↑⊤)
(Φ : Diffeotopy J n N)
(f : SmoothEmbedding I J n M N)
(p : M × ℝ)
:
(ofDiffeotopy hn Φ f) p = ((fun (p : ↑unitInterval × N) => (Φ.toDiffeomorph p).2) (collaredSmoothTransitionUnit p.2, f p.1), p.2)
noncomputable def
TauCeti.SmoothEmbedding.Concordance.ofSmoothIsotopy
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
[IsManifold I n M]
[IsManifold J n N]
[FiniteDimensional ℝ E']
[I.Boundaryless]
[J.Boundaryless]
[CompactSpace M]
[T2Space N]
(F : SmoothIsotopy f.toContMDiffMap g.toContMDiffMap)
(hn : 1 ≤ n)
(hn' : n ≤ ↑⊤)
:
f.Concordance g
The collared trace of a smooth isotopy of a compact boundaryless source is a concordance. The time coordinate is retained, so intersections between different time slices cause no problem. The target is finite-dimensional, Hausdorff and boundaryless.
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.Concordance.ofSmoothIsotopy_apply
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
[IsManifold I n M]
[IsManifold J n N]
[FiniteDimensional ℝ E']
[I.Boundaryless]
[J.Boundaryless]
[CompactSpace M]
[T2Space N]
(F : SmoothIsotopy f.toContMDiffMap g.toContMDiffMap)
(hn : 1 ≤ n)
(hn' : n ≤ ↑⊤)
(p : M × ℝ)
:
The trace evaluates the isotopy at a smooth time transition constant near both ends.
noncomputable def
TauCeti.SmoothEmbedding.Concordance.ofSourceDiffeotopy
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
[IsManifold I n M]
[IsManifold J n N]
(hn : n ≤ ↑⊤)
(Ψ : Diffeotopy I n M)
(f : SmoothEmbedding I J n M N)
:
f.Concordance (f.compDiffeomorph Ψ.final)
The trace of a source diffeotopy Ψ of M: the concordance (x, t) ↦ (f (Ψ (ρ t, x)), t)
from f to its reparametrization by the final diffeomorphism of Ψ, where
ρ(t) = Real.smoothTransition (2 * t - 1 / 2).
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.Concordance.ofSourceDiffeotopy_apply
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
[IsManifold I n M]
[IsManifold J n N]
(hn : n ≤ ↑⊤)
(Ψ : Diffeotopy I n M)
(f : SmoothEmbedding I J n M N)
(p : M × ℝ)
:
(ofSourceDiffeotopy hn Ψ f) p = (f ((fun (p : ↑unitInterval × M) => (Ψ.toDiffeomorph p).2) (collaredSmoothTransitionUnit p.2, p.1)), p.2)
The trace of a source diffeotopy at (x, t) is f applied to the motion of x at the
reparametrized time Real.smoothTransition (2 * t - 1 / 2).
noncomputable def
TauCeti.SmoothEmbedding.Concordance.ofDiffeotopies
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
[IsManifold I n M]
[IsManifold J n N]
(hn : n ≤ ↑⊤)
(Φ : Diffeotopy J n N)
(Ψ : Diffeotopy I n M)
(f : SmoothEmbedding I J n M N)
:
f.Concordance ((f.transDiffeomorph Φ.final).compDiffeomorph Ψ.final)
The trace of an ambient and a source diffeotopy run together: for diffeotopies Φ of N
and Ψ of M, the concordance (x, t) ↦ (Φ (ρ t, f (Ψ (ρ t, x))), t) from f to
Φ.final ∘ f ∘ Ψ.final, where ρ(t) = Real.smoothTransition (2 * t - 1 / 2). Unlike the stacked
traces of Φ and of Ψ, every time slice is Φₛ ∘ f ∘ Ψₛ for a single time s, so a property
of f preserved by all such conjugations holds along the whole concordance.
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.Concordance.ofDiffeotopies_apply
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
[IsManifold I n M]
[IsManifold J n N]
(hn : n ≤ ↑⊤)
(Φ : Diffeotopy J n N)
(Ψ : Diffeotopy I n M)
(f : SmoothEmbedding I J n M N)
(p : M × ℝ)
:
(ofDiffeotopies hn Φ Ψ f) p = ((fun (p : ↑unitInterval × N) => (Φ.toDiffeomorph p).2)
(collaredSmoothTransitionUnit p.2, f ((fun (p : ↑unitInterval × M) => (Ψ.toDiffeomorph p).2) (collaredSmoothTransitionUnit p.2, p.1))), p.2)
The joint trace of an ambient and a source diffeotopy at (x, t) applies Ψ, then f, then
Φ, all at the reparametrized time collaredSmoothTransitionUnit t.
The concordance relation #
theorem
TauCeti.SmoothEmbedding.Concordant.of_concordance
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
(F : f.Concordance g)
:
f.Concordant g
A concordance witnesses concordance.
theorem
TauCeti.SmoothEmbedding.Concordant.of_smoothIsotopic
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
[FiniteDimensional ℝ E']
[I.Boundaryless]
[J.Boundaryless]
[IsManifold I n M]
[IsManifold J n N]
[CompactSpace M]
[T2Space N]
(hfg : SmoothIsotopic f.toContMDiffMap g.toContMDiffMap)
(hn : 1 ≤ n)
(hn' : n ≤ ↑⊤)
:
f.Concordant g
Smoothly isotopic embeddings of a compact boundaryless source into a finite-dimensional Hausdorff boundaryless target are concordant.
theorem
TauCeti.SmoothEmbedding.Concordant.transDiffeomorph
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
{P : Type u_8}
[TopologicalSpace P]
[ChartedSpace H' P]
[IsManifold J n P]
(hfg : f.Concordant g)
(e : Diffeomorph J J N P n)
:
(f.transDiffeomorph e).Concordant (g.transDiffeomorph e)
An ambient diffeomorphism preserves concordance.
theorem
TauCeti.SmoothEmbedding.Concordant.compDiffeomorph
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M']
[IsManifold I n M']
(hfg : f.Concordant g)
(e : Diffeomorph I I M' M n)
:
(f.compDiffeomorph e).Concordant (g.compDiffeomorph e)
Reparametrizing the source by a diffeomorphism preserves concordance.
theorem
TauCeti.SmoothEmbedding.Concordant.refl
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
[IsManifold I n M]
[IsManifold J n N]
(f : SmoothEmbedding I J n M N)
:
f.Concordant f
Concordance is reflexive.
theorem
TauCeti.SmoothEmbedding.Concordant.symm
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
[IsManifold I n M]
[IsManifold J n N]
(hfg : f.Concordant g)
:
g.Concordant f
Concordance is symmetric.
theorem
TauCeti.SmoothEmbedding.Concordant.trans
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g h : SmoothEmbedding I J n M N}
[IsManifold I n M]
[IsManifold J n N]
[FiniteDimensional ℝ E']
(hfg : f.Concordant g)
(hgh : g.Concordant h)
:
f.Concordant h
Concordance is transitive, for a finite-dimensional ambient model.
theorem
TauCeti.SmoothEmbedding.Concordant.equivalence
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
[IsManifold I n M]
[IsManifold J n N]
[FiniteDimensional ℝ E']
:
For a finite-dimensional ambient model, concordance is an equivalence relation on smooth embeddings.
def
TauCeti.SmoothEmbedding.Concordant.setoid
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
[FiniteDimensional ℝ E']
(I : ModelWithCorners ℝ E H)
(J : ModelWithCorners ℝ E' H')
(n : WithTop ℕ∞)
(M : Type u_7)
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I n M]
(N : Type u_8)
[TopologicalSpace N]
[ChartedSpace H' N]
[IsManifold J n N]
:
Setoid (SmoothEmbedding I J n M N)
Concordance of smooth embeddings, packaged as a setoid.
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.Concordant.setoid_r_iff
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
[IsManifold I n M]
[IsManifold J n N]
[FiniteDimensional ℝ E']
:
The relation of the concordance setoid is concordance.
theorem
TauCeti.SmoothEmbedding.SmoothAmbientIsotopic.concordant
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H : Type u_3}
[TopologicalSpace H]
{H' : Type u_4}
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ E' H'}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
[IsManifold I n M]
[IsManifold J n N]
(hn : n ≤ ↑⊤)
{f g : SmoothEmbedding I J n M N}
(hfg : f.SmoothAmbientIsotopic g)
:
f.Concordant g
Smoothly ambient isotopic embeddings are concordant, through the trace of the diffeotopy.