Normal spaces of smooth embeddings #
At a point of a smoothly embedded submanifold, the normal space is the ambient tangent space modulo the image of the differential of the embedding. This quotient is intrinsic: it needs no metric or choice of complementary subspace. It is the fibrewise linear object from which a normal bundle, and eventually a tubular neighbourhood, must be constructed.
The differential is injective for an immersion of positive smoothness. Consequently the normal space has the expected codimension in finite dimensions. The quotient map also characterizes exactly which ambient tangent vectors represent zero normal vectors.
For the tubular-neighbourhood application of normal bundles, see M. Hirsch, Differential Topology, Theorem 6.3.
noncomputable def
TauCeti.SmoothEmbedding.tangentRange
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(_hn : n ≠ 0)
:
Submodule 𝕜 (TangentSpace J (f x))
The tangent subspace of the ambient manifold determined by a positive-regularity embedding
at x. It is the range of the differential, regarded as a linear map of tangent spaces.
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.mem_tangentRange_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
(v : TangentSpace J (f x))
:
An ambient tangent vector is tangent to the embedding precisely when it is a differential image.
noncomputable def
TauCeti.SmoothEmbedding.NormalSpace
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
:
Type u_3
The normal space of a smooth embedding at x: ambient tangent vectors modulo vectors
tangent to the embedded submanifold.
Instances For
theorem
TauCeti.SmoothEmbedding.isClosed_tangentRange
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
:
IsClosed ↑(f.tangentRange x hn)
The tangent range is closed because the differential of an immersion has a continuous left inverse.
@[instance_reducible]
noncomputable instance
TauCeti.SmoothEmbedding.instAddCommGroupNormalSpace
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
:
AddCommGroup (f.NormalSpace x hn)
@[instance_reducible]
noncomputable instance
TauCeti.SmoothEmbedding.instModuleNormalSpace
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
:
Module 𝕜 (f.NormalSpace x hn)
@[instance_reducible]
noncomputable instance
TauCeti.SmoothEmbedding.instTopologicalSpaceNormalSpace
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
:
TopologicalSpace (f.NormalSpace x hn)
instance
TauCeti.SmoothEmbedding.instT3SpaceNormalSpace
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
:
T3Space (f.NormalSpace x hn)
instance
TauCeti.SmoothEmbedding.instIsTopologicalAddGroupNormalSpace
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
:
IsTopologicalAddGroup (f.NormalSpace x hn)
instance
TauCeti.SmoothEmbedding.instContinuousSMulNormalSpace
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
:
ContinuousSMul 𝕜 (f.NormalSpace x hn)
instance
TauCeti.SmoothEmbedding.instFiniteDimensionalNormalSpace
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[FiniteDimensional 𝕜 F]
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
:
FiniteDimensional 𝕜 (f.NormalSpace x hn)
A normal space into a finite-dimensional model is finite-dimensional.
noncomputable def
TauCeti.SmoothEmbedding.normalClass
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
:
Project an ambient tangent vector to its normal class.
Instances For
theorem
TauCeti.SmoothEmbedding.normalClass_def
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
:
The normal-class map is the linear quotient map by the tangent range.
@[simp]
theorem
TauCeti.SmoothEmbedding.normalClass_ker
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
:
The kernel of the normal-class map is exactly the tangent range.
noncomputable def
TauCeti.SmoothEmbedding.normalClassL
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
:
The continuous quotient map from ambient tangent vectors to normal classes.
Instances For
theorem
TauCeti.SmoothEmbedding.isQuotientMap_normalClassL
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
:
Topology.IsQuotientMap ⇑(f.normalClassL x hn)
The continuous normal-class map gives the normal space its quotient topology.
theorem
TauCeti.SmoothEmbedding.isOpenQuotientMap_normalClassL
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
:
IsOpenQuotientMap ⇑(f.normalClassL x hn)
The continuous normal-class map is an open quotient map.
@[simp]
theorem
TauCeti.SmoothEmbedding.normalClassL_toLinearMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
:
The continuous normal-class map has normalClass as its underlying linear map.
@[simp]
theorem
TauCeti.SmoothEmbedding.normalClassL_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
(v : TangentSpace J (f x))
:
The continuous normal-class map agrees pointwise with the linear normal-class map.
noncomputable def
TauCeti.SmoothEmbedding.normalLiftL
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
{V : Type u_8}
[TopologicalSpace V]
[AddCommGroup V]
[Module 𝕜 V]
(g : TangentSpace J (f x) →L[𝕜] V)
(hg : ∀ v ∈ f.tangentRange x hn, g v = 0)
:
A continuous linear map vanishing on tangent vectors descends continuously to normal classes.
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.normalLiftL_comp_normalClassL
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
{V : Type u_8}
[TopologicalSpace V]
[AddCommGroup V]
[Module 𝕜 V]
(g : TangentSpace J (f x) →L[𝕜] V)
(hg : ∀ v ∈ f.tangentRange x hn, g v = 0)
:
The continuous quotient lift recovers the original map after composition with the continuous normal-class map.
theorem
TauCeti.SmoothEmbedding.normalClass_surjective
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
:
Function.Surjective ⇑(f.normalClass x hn)
Every normal vector has an ambient tangent representative.
noncomputable def
TauCeti.SmoothEmbedding.normalSpaceEquivOfMapTangentRange
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{E' : Type u_8}
{F' : Type u_9}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{H' : Type u_10}
{G' : Type u_11}
[TopologicalSpace H']
[TopologicalSpace G']
{I' : ModelWithCorners 𝕜 E' H'}
{J' : ModelWithCorners 𝕜 F' G'}
{M' : Type u_12}
{N' : Type u_13}
[TopologicalSpace M']
[ChartedSpace H' M']
[TopologicalSpace N']
[ChartedSpace G' N']
{m : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(g : SmoothEmbedding I' J' m M' N')
(x : M)
(y : M')
(hn : n ≠ 0)
(hm : m ≠ 0)
(e : TangentSpace J (f x) ≃L[𝕜] TangentSpace J' (g y))
(h : Submodule.map (↑↑e) (f.tangentRange x hn) = g.tangentRange y hm)
:
An ambient tangent equivalence carrying one embedding's tangent range onto the other's induces an equivalence of their intrinsic normal spaces.
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.normalSpaceEquivOfMapTangentRange_normalClass
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{E' : Type u_8}
{F' : Type u_9}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{H' : Type u_10}
{G' : Type u_11}
[TopologicalSpace H']
[TopologicalSpace G']
{I' : ModelWithCorners 𝕜 E' H'}
{J' : ModelWithCorners 𝕜 F' G'}
{M' : Type u_12}
{N' : Type u_13}
[TopologicalSpace M']
[ChartedSpace H' M']
[TopologicalSpace N']
[ChartedSpace G' N']
{m : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(g : SmoothEmbedding I' J' m M' N')
(x : M)
(y : M')
(hn : n ≠ 0)
(hm : m ≠ 0)
(e : TangentSpace J (f x) ≃L[𝕜] TangentSpace J' (g y))
(h : Submodule.map (↑↑e) (f.tangentRange x hn) = g.tangentRange y hm)
(w : TangentSpace J (f x))
:
(f.normalSpaceEquivOfMapTangentRange g x y hn hm e h) ((f.normalClass x hn) w) = (g.normalClass y hm) (e w)
The normal-space equivalence induced by an ambient tangent equivalence applies it to representatives.
@[simp]
theorem
TauCeti.SmoothEmbedding.normalClass_eq_zero_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
(v : TangentSpace J (f x))
:
An ambient tangent vector has zero normal class precisely when it is tangent to the image.
@[simp]
theorem
TauCeti.SmoothEmbedding.normalClass_mfderiv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
(v : TangentSpace I x)
:
The differential of the embedding has zero normal class.
@[simp]
theorem
TauCeti.SmoothEmbedding.normalClass_eq_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
(v w : TangentSpace J (f x))
:
Two ambient tangent vectors represent the same normal vector exactly when their difference is tangent to the embedded submanifold.
noncomputable def
TauCeti.SmoothEmbedding.normalLift
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
{V : Type u_8}
[AddCommGroup V]
[Module 𝕜 V]
(g : TangentSpace J (f x) →ₗ[𝕜] V)
(hg : ∀ v ∈ f.tangentRange x hn, g v = 0)
:
A linear map vanishing on tangent vectors descends to the normal space.
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.normalLiftL_toLinearMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
{V : Type u_8}
[TopologicalSpace V]
[AddCommGroup V]
[Module 𝕜 V]
(g : TangentSpace J (f x) →L[𝕜] V)
(hg : ∀ v ∈ f.tangentRange x hn, g v = 0)
:
The underlying linear map of the continuous normal lift is the linear normal lift.
@[simp]
theorem
TauCeti.SmoothEmbedding.normalLiftL_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
{V : Type u_8}
[TopologicalSpace V]
[AddCommGroup V]
[Module 𝕜 V]
(g : TangentSpace J (f x) →L[𝕜] V)
(hg : ∀ v ∈ f.tangentRange x hn, g v = 0)
(v : f.NormalSpace x hn)
:
The continuous normal lift agrees pointwise with the linear normal lift.
@[simp]
theorem
TauCeti.SmoothEmbedding.normalLift_comp_normalClass
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
{V : Type u_8}
[AddCommGroup V]
[Module 𝕜 V]
(g : TangentSpace J (f x) →ₗ[𝕜] V)
(hg : ∀ v ∈ f.tangentRange x hn, g v = 0)
:
Composing the quotient lift with the normal-class map recovers the original linear map.
theorem
TauCeti.SmoothEmbedding.normalLift_unique
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
{V : Type u_8}
[AddCommGroup V]
[Module 𝕜 V]
(g : TangentSpace J (f x) →ₗ[𝕜] V)
(hg : ∀ v ∈ f.tangentRange x hn, g v = 0)
(h : f.NormalSpace x hn →ₗ[𝕜] V)
(hh : h ∘ₗ f.normalClass x hn = g)
:
A map out of the normal space is determined by its values on ambient tangent classes.
theorem
TauCeti.SmoothEmbedding.normalLiftL_unique
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
{V : Type u_8}
[TopologicalSpace V]
[AddCommGroup V]
[Module 𝕜 V]
(g : TangentSpace J (f x) →L[𝕜] V)
(hg : ∀ v ∈ f.tangentRange x hn, g v = 0)
(h : f.NormalSpace x hn →L[𝕜] V)
(hh : h ∘SL f.normalClassL x hn = g)
:
A continuous linear map out of the normal space is determined by its composition with the continuous normal-class map.
theorem
TauCeti.SmoothEmbedding.finrank_normalSpace_add_finrank
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
[FiniteDimensional 𝕜 F]
:
Module.finrank 𝕜 (f.NormalSpace x hn) + Module.finrank 𝕜 (TangentSpace I x) = Module.finrank 𝕜 (TangentSpace J (f x))
The normal dimension plus the tangent dimension equals the ambient dimension for a finite-dimensional smooth embedding.
theorem
TauCeti.SmoothEmbedding.finrank_normalSpace
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
[FiniteDimensional 𝕜 F]
:
Module.finrank 𝕜 (f.NormalSpace x hn) = Module.finrank 𝕜 (TangentSpace J (f x)) - Module.finrank 𝕜 (TangentSpace I x)
The dimension of the normal space is the codimension of the embedded manifold.