Maps between intrinsic normal spaces #
A commuting square of differentiable maps between two smooth embeddings induces a continuous linear map between their normal spaces. The ambient differential carries tangent vectors to tangent vectors, so it descends to the quotient. The induced map is an equivalence when the base differential is surjective and the ambient map is a local diffeomorphism. In particular, these equivalences identify intrinsic normal fibres in different submanifold coordinates, without choosing a metric or a complement.
The square need only commute near the chosen base point. This local formulation allows the construction to be applied to coordinate maps and to their restrictions.
A globally commuting square of differentiable maps also induces a map of intrinsic normal total spaces, acting on each fibre by the normal map; these maps respect identities and composition.
References #
- M. Hirsch, Differential Topology, Springer GTM 33 (1976), Chapter 4, ยงยง5โ6, for the normal-bundle and tubular-neighbourhood setting.
- Tau Ceti's
ContinuousLinearEquiv.quotientEquivtopologically bundles Mathlib'sSubmodule.Quotient.equiv.
theorem
TauCeti.SmoothEmbedding.tangentRange_le_comap_mfderiv
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{E : Type u_2}
{F : Type u_3}
{E' : Type u_4}
{F' : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
[NormedAddCommGroup F]
[NormedSpace ๐ F]
[NormedAddCommGroup E']
[NormedSpace ๐ E']
[NormedAddCommGroup F']
[NormedSpace ๐ F']
{H : Type u_6}
{G : Type u_7}
{H' : Type u_8}
{G' : Type u_9}
[TopologicalSpace H]
[TopologicalSpace G]
[TopologicalSpace H']
[TopologicalSpace G']
{I : ModelWithCorners ๐ E H}
{J : ModelWithCorners ๐ F G}
{I' : ModelWithCorners ๐ E' H'}
{J' : ModelWithCorners ๐ F' G'}
{M : Type u_10}
{N : Type u_11}
{M' : Type u_12}
{N' : Type u_13}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
[TopologicalSpace M']
[ChartedSpace H' M']
[TopologicalSpace N']
[ChartedSpace G' N']
{n m : WithTop โโ}
(f : SmoothEmbedding I J n M N)
(g : SmoothEmbedding I' J' m M' N')
{u : M โ M'}
{v : N โ N'}
{x : M}
(hn : n โ 0)
(hm : m โ 0)
(hu : MDiffAt u x)
(hv : MDiffAt v (f x))
(h : v โ โf =แถ [nhds x] โg โ u)
:
f.tangentRange x hn โค Submodule.comap (โ(โ(tangentSpaceCast J' (v (f x)) (g (u x))) โSL mfderiv% v (f x))) (g.tangentRange (u x) hm)
The ambient differential in a locally commuting square carries tangent vectors to tangent vectors.
noncomputable def
TauCeti.SmoothEmbedding.normalMap
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{E : Type u_2}
{F : Type u_3}
{E' : Type u_4}
{F' : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
[NormedAddCommGroup F]
[NormedSpace ๐ F]
[NormedAddCommGroup E']
[NormedSpace ๐ E']
[NormedAddCommGroup F']
[NormedSpace ๐ F']
{H : Type u_6}
{G : Type u_7}
{H' : Type u_8}
{G' : Type u_9}
[TopologicalSpace H]
[TopologicalSpace G]
[TopologicalSpace H']
[TopologicalSpace G']
{I : ModelWithCorners ๐ E H}
{J : ModelWithCorners ๐ F G}
{I' : ModelWithCorners ๐ E' H'}
{J' : ModelWithCorners ๐ F' G'}
{M : Type u_10}
{N : Type u_11}
{M' : Type u_12}
{N' : Type u_13}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
[TopologicalSpace M']
[ChartedSpace H' M']
[TopologicalSpace N']
[ChartedSpace G' N']
{n m : WithTop โโ}
(f : SmoothEmbedding I J n M N)
(g : SmoothEmbedding I' J' m M' N')
{u : M โ M'}
{v : N โ N'}
{x : M}
(hn : n โ 0)
(hm : m โ 0)
(hu : MDiffAt u x)
(hv : MDiffAt v (f x))
(h : v โ โf =แถ [nhds x] โg โ u)
:
The normal map induced by a square commuting near x. On an ambient tangent class,
it is given by the differential of v.
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.normalMap_comp_normalClassL
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{E : Type u_2}
{F : Type u_3}
{E' : Type u_4}
{F' : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
[NormedAddCommGroup F]
[NormedSpace ๐ F]
[NormedAddCommGroup E']
[NormedSpace ๐ E']
[NormedAddCommGroup F']
[NormedSpace ๐ F']
{H : Type u_6}
{G : Type u_7}
{H' : Type u_8}
{G' : Type u_9}
[TopologicalSpace H]
[TopologicalSpace G]
[TopologicalSpace H']
[TopologicalSpace G']
{I : ModelWithCorners ๐ E H}
{J : ModelWithCorners ๐ F G}
{I' : ModelWithCorners ๐ E' H'}
{J' : ModelWithCorners ๐ F' G'}
{M : Type u_10}
{N : Type u_11}
{M' : Type u_12}
{N' : Type u_13}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
[TopologicalSpace M']
[ChartedSpace H' M']
[TopologicalSpace N']
[ChartedSpace G' N']
{n m : WithTop โโ}
(f : SmoothEmbedding I J n M N)
(g : SmoothEmbedding I' J' m M' N')
{u : M โ M'}
{v : N โ N'}
{x : M}
(hn : n โ 0)
(hm : m โ 0)
(hu : MDiffAt u x)
(hv : MDiffAt v (f x))
(h : v โ โf =แถ [nhds x] โg โ u)
:
f.normalMap g hn hm hu hv h โSL f.normalClassL x hn = g.normalClassL (u x) hm โSL โ(tangentSpaceCast J' (v (f x)) (g (u x))) โSL mfderiv% v (f x)
The induced normal map commutes with the continuous quotient maps.
@[simp]
theorem
TauCeti.SmoothEmbedding.normalMap_normalClass
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{E : Type u_2}
{F : Type u_3}
{E' : Type u_4}
{F' : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
[NormedAddCommGroup F]
[NormedSpace ๐ F]
[NormedAddCommGroup E']
[NormedSpace ๐ E']
[NormedAddCommGroup F']
[NormedSpace ๐ F']
{H : Type u_6}
{G : Type u_7}
{H' : Type u_8}
{G' : Type u_9}
[TopologicalSpace H]
[TopologicalSpace G]
[TopologicalSpace H']
[TopologicalSpace G']
{I : ModelWithCorners ๐ E H}
{J : ModelWithCorners ๐ F G}
{I' : ModelWithCorners ๐ E' H'}
{J' : ModelWithCorners ๐ F' G'}
{M : Type u_10}
{N : Type u_11}
{M' : Type u_12}
{N' : Type u_13}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
[TopologicalSpace M']
[ChartedSpace H' M']
[TopologicalSpace N']
[ChartedSpace G' N']
{n m : WithTop โโ}
(f : SmoothEmbedding I J n M N)
(g : SmoothEmbedding I' J' m M' N')
{u : M โ M'}
{v : N โ N'}
{x : M}
(hn : n โ 0)
(hm : m โ 0)
(hu : MDiffAt u x)
(hv : MDiffAt v (f x))
(h : v โ โf =แถ [nhds x] โg โ u)
(w : TangentSpace J (f x))
:
(f.normalMap g hn hm hu hv h) ((f.normalClass x hn) w) = (g.normalClass (u x) hm) ((tangentSpaceCast J' (v (f x)) (g (u x))) ((mfderiv% v (f x)) w))
The induced normal map sends the class of w to the class of dv(w).
@[simp]
theorem
TauCeti.SmoothEmbedding.normalMap_id
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
[NormedAddCommGroup F]
[NormedSpace ๐ F]
{H : Type u_6}
{G : Type u_7}
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ๐ E H}
{J : ModelWithCorners ๐ F G}
{M : Type u_10}
{N : Type u_11}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop โโ}
(f : SmoothEmbedding I J n M N)
(hn : n โ 0)
(x : M)
:
The identity square induces the identity on the normal space.
noncomputable def
TauCeti.SmoothEmbedding.normalBundleMap
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{E : Type u_2}
{F : Type u_3}
{E' : Type u_4}
{F' : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
[NormedAddCommGroup F]
[NormedSpace ๐ F]
[NormedAddCommGroup E']
[NormedSpace ๐ E']
[NormedAddCommGroup F']
[NormedSpace ๐ F']
{H : Type u_6}
{G : Type u_7}
{H' : Type u_8}
{G' : Type u_9}
[TopologicalSpace H]
[TopologicalSpace G]
[TopologicalSpace H']
[TopologicalSpace G']
{I : ModelWithCorners ๐ E H}
{J : ModelWithCorners ๐ F G}
{I' : ModelWithCorners ๐ E' H'}
{J' : ModelWithCorners ๐ F' G'}
{M : Type u_10}
{N : Type u_11}
{M' : Type u_12}
{N' : Type u_13}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
[TopologicalSpace M']
[ChartedSpace H' M']
[TopologicalSpace N']
[ChartedSpace G' N']
{n m : WithTop โโ}
(f : SmoothEmbedding I J n M N)
(g : SmoothEmbedding I' J' m M' N')
{u : M โ M'}
{v : N โ N'}
{K : Type u_14}
{K' : Type u_15}
(hn : n โ 0)
(hm : m โ 0)
(hu : MDiff u)
(hv : MDiff v)
(h : v โ โf = โg โ u)
(p : Bundle.TotalSpace K fun (x : M) => f.NormalSpace x hn)
:
Bundle.TotalSpace K' fun (x : M') => g.NormalSpace x hm
A differentiable commuting square induces a map of intrinsic normal total spaces. On each fibre it is the normal map induced by the ambient differential.
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.normalBundleMap_apply
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{E : Type u_2}
{F : Type u_3}
{E' : Type u_4}
{F' : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
[NormedAddCommGroup F]
[NormedSpace ๐ F]
[NormedAddCommGroup E']
[NormedSpace ๐ E']
[NormedAddCommGroup F']
[NormedSpace ๐ F']
{H : Type u_6}
{G : Type u_7}
{H' : Type u_8}
{G' : Type u_9}
[TopologicalSpace H]
[TopologicalSpace G]
[TopologicalSpace H']
[TopologicalSpace G']
{I : ModelWithCorners ๐ E H}
{J : ModelWithCorners ๐ F G}
{I' : ModelWithCorners ๐ E' H'}
{J' : ModelWithCorners ๐ F' G'}
{M : Type u_10}
{N : Type u_11}
{M' : Type u_12}
{N' : Type u_13}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
[TopologicalSpace M']
[ChartedSpace H' M']
[TopologicalSpace N']
[ChartedSpace G' N']
{n m : WithTop โโ}
(f : SmoothEmbedding I J n M N)
(g : SmoothEmbedding I' J' m M' N')
{u : M โ M'}
{v : N โ N'}
{K : Type u_14}
{K' : Type u_15}
(hn : n โ 0)
(hm : m โ 0)
(hu : MDiff u)
(hv : MDiff v)
(h : v โ โf = โg โ u)
(p : Bundle.TotalSpace K fun (x : M) => f.NormalSpace x hn)
:
The induced total map applies the normal map in each fibre.
@[simp]
theorem
TauCeti.SmoothEmbedding.normalBundleMap_id
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
[NormedAddCommGroup F]
[NormedSpace ๐ F]
{H : Type u_6}
{G : Type u_7}
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ๐ E H}
{J : ModelWithCorners ๐ F G}
{M : Type u_10}
{N : Type u_11}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop โโ}
(f : SmoothEmbedding I J n M N)
{K : Type u_14}
(hn : n โ 0)
:
The identity square induces the identity of the normal bundle.
theorem
TauCeti.SmoothEmbedding.normalMap_comp
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{E : Type u_2}
{F : Type u_3}
{E' : Type u_4}
{F' : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
[NormedAddCommGroup F]
[NormedSpace ๐ F]
[NormedAddCommGroup E']
[NormedSpace ๐ E']
[NormedAddCommGroup F']
[NormedSpace ๐ F']
{H : Type u_6}
{G : Type u_7}
{H' : Type u_8}
{G' : Type u_9}
[TopologicalSpace H]
[TopologicalSpace G]
[TopologicalSpace H']
[TopologicalSpace G']
{I : ModelWithCorners ๐ E H}
{J : ModelWithCorners ๐ F G}
{I' : ModelWithCorners ๐ E' H'}
{J' : ModelWithCorners ๐ F' G'}
{M : Type u_10}
{N : Type u_11}
{M' : Type u_12}
{N' : Type u_13}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
[TopologicalSpace M']
[ChartedSpace H' M']
[TopologicalSpace N']
[ChartedSpace G' N']
{n m : WithTop โโ}
(f : SmoothEmbedding I J n M N)
(g : SmoothEmbedding I' J' m M' N')
{u : M โ M'}
{v : N โ N'}
{x : M}
{E'' : Type u_16}
{F'' : Type u_17}
{H'' : Type u_18}
{G'' : Type u_19}
{M'' : Type u_20}
{N'' : Type u_21}
[NormedAddCommGroup E'']
[NormedSpace ๐ E'']
[NormedAddCommGroup F'']
[NormedSpace ๐ F'']
[TopologicalSpace H'']
[TopologicalSpace G'']
{I'' : ModelWithCorners ๐ E'' H''}
{J'' : ModelWithCorners ๐ F'' G''}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
[TopologicalSpace N'']
[ChartedSpace G'' N'']
{r : WithTop โโ}
(q : SmoothEmbedding I'' J'' r M'' N'')
{u' : M' โ M''}
{v' : N' โ N''}
(hn : n โ 0)
(hm : m โ 0)
(hr : r โ 0)
(hu : MDiffAt u x)
(hv : MDiffAt v (f x))
(hu' : MDiffAt u' (u x))
(hv' : MDiffAt v' (g (u x)))
(h : v โ โf =แถ [nhds x] โg โ u)
(h' : v' โ โg =แถ [nhds (u x)] โq โ u')
:
Composing locally commuting squares composes their induced normal maps. The composite square is obtained from the two given germs.
theorem
TauCeti.SmoothEmbedding.normalBundleMap_comp
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{E : Type u_2}
{F : Type u_3}
{E' : Type u_4}
{F' : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
[NormedAddCommGroup F]
[NormedSpace ๐ F]
[NormedAddCommGroup E']
[NormedSpace ๐ E']
[NormedAddCommGroup F']
[NormedSpace ๐ F']
{H : Type u_6}
{G : Type u_7}
{H' : Type u_8}
{G' : Type u_9}
[TopologicalSpace H]
[TopologicalSpace G]
[TopologicalSpace H']
[TopologicalSpace G']
{I : ModelWithCorners ๐ E H}
{J : ModelWithCorners ๐ F G}
{I' : ModelWithCorners ๐ E' H'}
{J' : ModelWithCorners ๐ F' G'}
{M : Type u_10}
{N : Type u_11}
{M' : Type u_12}
{N' : Type u_13}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
[TopologicalSpace M']
[ChartedSpace H' M']
[TopologicalSpace N']
[ChartedSpace G' N']
{n m : WithTop โโ}
(f : SmoothEmbedding I J n M N)
(g : SmoothEmbedding I' J' m M' N')
{u : M โ M'}
{v : N โ N'}
{K : Type u_14}
{K' : Type u_15}
{E'' : Type u_16}
{F'' : Type u_17}
{H'' : Type u_18}
{G'' : Type u_19}
{M'' : Type u_20}
{N'' : Type u_21}
[NormedAddCommGroup E'']
[NormedSpace ๐ E'']
[NormedAddCommGroup F'']
[NormedSpace ๐ F'']
[TopologicalSpace H'']
[TopologicalSpace G'']
{I'' : ModelWithCorners ๐ E'' H''}
{J'' : ModelWithCorners ๐ F'' G''}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
[TopologicalSpace N'']
[ChartedSpace G'' N'']
{r : WithTop โโ}
(q : SmoothEmbedding I'' J'' r M'' N'')
{u' : M' โ M''}
{v' : N' โ N''}
{K'' : Type u_22}
(hn : n โ 0)
(hm : m โ 0)
(hr : r โ 0)
(hu : MDiff u)
(hv : MDiff v)
(hu' : MDiff u')
(hv' : MDiff v')
(h : v โ โf = โg โ u)
(h' : v' โ โg = โq โ u')
:
f.normalBundleMap q hn hr โฏ โฏ โฏ = g.normalBundleMap q hm hr hu' hv' h' โ f.normalBundleMap g hn hm hu hv h
Composing commuting squares composes their induced maps on normal total spaces.
theorem
TauCeti.SmoothEmbedding.map_tangentRange_mfderiv
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{E : Type u_2}
{F : Type u_3}
{E' : Type u_4}
{F' : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
[NormedAddCommGroup F]
[NormedSpace ๐ F]
[NormedAddCommGroup E']
[NormedSpace ๐ E']
[NormedAddCommGroup F']
[NormedSpace ๐ F']
{H : Type u_6}
{G : Type u_7}
{H' : Type u_8}
{G' : Type u_9}
[TopologicalSpace H]
[TopologicalSpace G]
[TopologicalSpace H']
[TopologicalSpace G']
{I : ModelWithCorners ๐ E H}
{J : ModelWithCorners ๐ F G}
{I' : ModelWithCorners ๐ E' H'}
{J' : ModelWithCorners ๐ F' G'}
{M : Type u_10}
{N : Type u_11}
{M' : Type u_12}
{N' : Type u_13}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
[TopologicalSpace M']
[ChartedSpace H' M']
[TopologicalSpace N']
[ChartedSpace G' N']
{n m : WithTop โโ}
(f : SmoothEmbedding I J n M N)
(g : SmoothEmbedding I' J' m M' N')
{u : M โ M'}
{v : N โ N'}
{x : M}
(hn : n โ 0)
(hm : m โ 0)
(hu : MDiffAt u x)
(hv : MDiffAt v (f x))
(h : v โ โf =แถ [nhds x] โg โ u)
(hsurj : Function.Surjective โ(mfderiv% u x))
:
Submodule.map (โ(โ(tangentSpaceCast J' (v (f x)) (g (u x))) โSL mfderiv% v (f x))) (f.tangentRange x hn) = g.tangentRange (u x) hm
If the base differential is surjective, the ambient differential carries the tangent range onto the target tangent range.
noncomputable def
TauCeti.SmoothEmbedding.normalSpaceEquiv
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{E : Type u_2}
{F : Type u_3}
{E' : Type u_4}
{F' : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
[NormedAddCommGroup F]
[NormedSpace ๐ F]
[NormedAddCommGroup E']
[NormedSpace ๐ E']
[NormedAddCommGroup F']
[NormedSpace ๐ F']
{H : Type u_6}
{G : Type u_7}
{H' : Type u_8}
{G' : Type u_9}
[TopologicalSpace H]
[TopologicalSpace G]
[TopologicalSpace H']
[TopologicalSpace G']
{I : ModelWithCorners ๐ E H}
{J : ModelWithCorners ๐ F G}
{I' : ModelWithCorners ๐ E' H'}
{J' : ModelWithCorners ๐ F' G'}
{M : Type u_10}
{N : Type u_11}
{M' : Type u_12}
{N' : Type u_13}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
[TopologicalSpace M']
[ChartedSpace H' M']
[TopologicalSpace N']
[ChartedSpace G' N']
{n m : WithTop โโ}
(f : SmoothEmbedding I J n M N)
(g : SmoothEmbedding I' J' m M' N')
{u : M โ M'}
{v : N โ N'}
{x : M}
{l : WithTop โโ}
(hn : n โ 0)
(hm : m โ 0)
(hu : MDiffAt u x)
(hv : IsLocalDiffeomorphAt J J' l v (f x))
(hsurj : Function.Surjective โ(mfderiv% u x))
(hl : l โ 0)
(h : v โ โf =แถ [nhds x] โg โ u)
:
A commuting square identifies the intrinsic normal fibres when the base differential is surjective and the ambient map is a local diffeomorphism at the chosen point.
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.normalSpaceEquiv_toContinuousLinearMap
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{E : Type u_2}
{F : Type u_3}
{E' : Type u_4}
{F' : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
[NormedAddCommGroup F]
[NormedSpace ๐ F]
[NormedAddCommGroup E']
[NormedSpace ๐ E']
[NormedAddCommGroup F']
[NormedSpace ๐ F']
{H : Type u_6}
{G : Type u_7}
{H' : Type u_8}
{G' : Type u_9}
[TopologicalSpace H]
[TopologicalSpace G]
[TopologicalSpace H']
[TopologicalSpace G']
{I : ModelWithCorners ๐ E H}
{J : ModelWithCorners ๐ F G}
{I' : ModelWithCorners ๐ E' H'}
{J' : ModelWithCorners ๐ F' G'}
{M : Type u_10}
{N : Type u_11}
{M' : Type u_12}
{N' : Type u_13}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
[TopologicalSpace M']
[ChartedSpace H' M']
[TopologicalSpace N']
[ChartedSpace G' N']
{n m : WithTop โโ}
(f : SmoothEmbedding I J n M N)
(g : SmoothEmbedding I' J' m M' N')
{u : M โ M'}
{v : N โ N'}
{x : M}
{l : WithTop โโ}
(hn : n โ 0)
(hm : m โ 0)
(hu : MDiffAt u x)
(hv : IsLocalDiffeomorphAt J J' l v (f x))
(hsurj : Function.Surjective โ(mfderiv% u x))
(hl : l โ 0)
(h : v โ โf =แถ [nhds x] โg โ u)
:
The normal-fibre equivalence has the normal map as its underlying continuous linear map.
@[simp]
theorem
TauCeti.SmoothEmbedding.normalSpaceEquiv_normalClass
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{E : Type u_2}
{F : Type u_3}
{E' : Type u_4}
{F' : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
[NormedAddCommGroup F]
[NormedSpace ๐ F]
[NormedAddCommGroup E']
[NormedSpace ๐ E']
[NormedAddCommGroup F']
[NormedSpace ๐ F']
{H : Type u_6}
{G : Type u_7}
{H' : Type u_8}
{G' : Type u_9}
[TopologicalSpace H]
[TopologicalSpace G]
[TopologicalSpace H']
[TopologicalSpace G']
{I : ModelWithCorners ๐ E H}
{J : ModelWithCorners ๐ F G}
{I' : ModelWithCorners ๐ E' H'}
{J' : ModelWithCorners ๐ F' G'}
{M : Type u_10}
{N : Type u_11}
{M' : Type u_12}
{N' : Type u_13}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
[TopologicalSpace M']
[ChartedSpace H' M']
[TopologicalSpace N']
[ChartedSpace G' N']
{n m : WithTop โโ}
(f : SmoothEmbedding I J n M N)
(g : SmoothEmbedding I' J' m M' N')
{u : M โ M'}
{v : N โ N'}
{x : M}
{l : WithTop โโ}
(hn : n โ 0)
(hm : m โ 0)
(hu : MDiffAt u x)
(hv : IsLocalDiffeomorphAt J J' l v (f x))
(hsurj : Function.Surjective โ(mfderiv% u x))
(hl : l โ 0)
(h : v โ โf =แถ [nhds x] โg โ u)
(w : TangentSpace J (f x))
:
(f.normalSpaceEquiv g hn hm hu hv hsurj hl h) ((f.normalClass x hn) w) = (g.normalClass (u x) hm) ((tangentSpaceCast J' (v (f x)) (g (u x))) ((mfderiv% v (f x)) w))
On representatives, the normal-fibre equivalence applies the ambient differential.
@[simp]
theorem
TauCeti.SmoothEmbedding.normalSpaceEquiv_symm_normalClass
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{E : Type u_2}
{F : Type u_3}
{E' : Type u_4}
{F' : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
[NormedAddCommGroup F]
[NormedSpace ๐ F]
[NormedAddCommGroup E']
[NormedSpace ๐ E']
[NormedAddCommGroup F']
[NormedSpace ๐ F']
{H : Type u_6}
{G : Type u_7}
{H' : Type u_8}
{G' : Type u_9}
[TopologicalSpace H]
[TopologicalSpace G]
[TopologicalSpace H']
[TopologicalSpace G']
{I : ModelWithCorners ๐ E H}
{J : ModelWithCorners ๐ F G}
{I' : ModelWithCorners ๐ E' H'}
{J' : ModelWithCorners ๐ F' G'}
{M : Type u_10}
{N : Type u_11}
{M' : Type u_12}
{N' : Type u_13}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
[TopologicalSpace M']
[ChartedSpace H' M']
[TopologicalSpace N']
[ChartedSpace G' N']
{n m : WithTop โโ}
(f : SmoothEmbedding I J n M N)
(g : SmoothEmbedding I' J' m M' N')
{u : M โ M'}
{v : N โ N'}
{x : M}
{l : WithTop โโ}
(hn : n โ 0)
(hm : m โ 0)
(hu : MDiffAt u x)
(hv : IsLocalDiffeomorphAt J J' l v (f x))
(hsurj : Function.Surjective โ(mfderiv% u x))
(hl : l โ 0)
(h : v โ โf =แถ [nhds x] โg โ u)
(w : TangentSpace J' (g (u x)))
:
(f.normalSpaceEquiv g hn hm hu hv hsurj hl h).symm ((g.normalClass (u x) hm) w) = (f.normalClass x hn) (((hv.mfderivToContinuousLinearEquiv hl).trans (tangentSpaceCast J' (v (f x)) (g (u x)))).symm w)
On representatives, the inverse normal-fibre equivalence applies the inverse ambient differential, after identifying the equal ambient base points.