Orthogonal representatives of normal classes #
For a smooth embedding into a manifold whose tangent spaces carry a Riemannian metric, every
intrinsic normal class has a unique representative orthogonal to the tangent space of the
embedded submanifold. This identifies the intrinsic normal space with the orthogonal complement
of the embedded tangent space, using Mathlib's Submodule.quotientEquivOfIsTopCompl.
References #
- J. M. Lee, Introduction to Smooth Manifolds, second edition, Theorem 6.24.
noncomputable def
TauCeti.SmoothEmbedding.normalSpaceOrthogonalComplementEquiv
{E : Type u_1}
{V : Type u_2}
{H : Type u_3}
{G : Type u_4}
{M : Type u_5}
{N : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ V G}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
:
Orthogonal representatives identify an intrinsic normal space with the orthogonal complement of the embedded tangent space in the ambient tangent space.
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.normalSpaceOrthogonalComplementEquiv_symm_apply
{E : Type u_1}
{V : Type u_2}
{H : Type u_3}
{G : Type u_4}
{M : Type u_5}
{N : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ V G}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
(v : ↥(f.tangentRange x hn)ᗮ)
:
The inverse orthogonal-representative equivalence takes the normal class of the given orthogonal vector.
@[simp]
theorem
TauCeti.SmoothEmbedding.normalSpaceOrthogonalComplementEquiv_normalClass
{E : Type u_1}
{V : Type u_2}
{H : Type u_3}
{G : Type u_4}
{M : Type u_5}
{N : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ V G}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
(v : TangentSpace J (f x))
:
(f.normalSpaceOrthogonalComplementEquiv x hn) ((f.normalClass x hn) v) = (f.tangentRange x hn)ᗮ.orthogonalProjectionOnto v
The orthogonal representative of the class of an ambient tangent vector is its projection onto the orthogonal complement of the embedded tangent space.
noncomputable def
TauCeti.SmoothEmbedding.normalRepresentative
{E : Type u_1}
{V : Type u_2}
{H : Type u_3}
{G : Type u_4}
{M : Type u_5}
{N : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ V G}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
:
The unique tangent vector orthogonal to the embedded tangent space which represents an intrinsic normal class.
Instances For
theorem
TauCeti.SmoothEmbedding.normalRepresentative_apply
{E : Type u_1}
{V : Type u_2}
{H : Type u_3}
{G : Type u_4}
{M : Type u_5}
{N : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ V G}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
(v : f.NormalSpace x hn)
:
The normal representative is the orthogonal vector given by the orthogonal-representative equivalence.
@[simp]
theorem
TauCeti.SmoothEmbedding.normalRepresentative_normalClass
{E : Type u_1}
{V : Type u_2}
{H : Type u_3}
{G : Type u_4}
{M : Type u_5}
{N : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ V G}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
(v : TangentSpace J (f x))
:
The representative of an ambient tangent class is its orthogonal projection to the normal directions.
@[simp]
theorem
TauCeti.SmoothEmbedding.normalClass_normalRepresentative
{E : Type u_1}
{V : Type u_2}
{H : Type u_3}
{G : Type u_4}
{M : Type u_5}
{N : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ V G}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
(v : f.NormalSpace x hn)
:
Taking the normal class of its orthogonal representative recovers the original class.
theorem
TauCeti.SmoothEmbedding.normalRepresentative_mem_orthogonal
{E : Type u_1}
{V : Type u_2}
{H : Type u_3}
{G : Type u_4}
{M : Type u_5}
{N : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ V G}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
(v : f.NormalSpace x hn)
:
Normal representatives are orthogonal to every tangent vector of the embedded submanifold.
theorem
TauCeti.SmoothEmbedding.normalRepresentative_eq_iff
{E : Type u_1}
{V : Type u_2}
{H : Type u_3}
{G : Type u_4}
{M : Type u_5}
{N : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ V G}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
(v : f.NormalSpace x hn)
(w : TangentSpace J (f x))
:
The normal representative is the unique orthogonal ambient tangent vector in its normal class.
theorem
TauCeti.SmoothEmbedding.inner_normalRepresentative_mfderiv
{E : Type u_1}
{V : Type u_2}
{H : Type u_3}
{G : Type u_4}
{M : Type u_5}
{N : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ V G}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
(v : f.NormalSpace x hn)
(w : TangentSpace I x)
:
The normal representative is perpendicular to the differential of every tangent vector.
theorem
TauCeti.SmoothEmbedding.normalRepresentative_normalClass_eq_sub_mfderiv_inverse
{E : Type u_1}
{V : Type u_2}
{H : Type u_3}
{G : Type u_4}
{M : Type u_5}
{N : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ V G}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
[FiniteDimensional ℝ E]
(f : SmoothEmbedding I J n M N)
(x : M)
(hn : n ≠ 0)
(v : TangentSpace J (f x))
:
have d := mfderiv% ⇑f x;
have φ := (Bundle.RiemannianBundle.g.inner (f x)) v ∘SL d;
have a := ContinuousLinearMap.precomp ℝ d ∘SL Bundle.RiemannianBundle.g.inner (f x) ∘SL d;
(f.normalRepresentative x hn) ((f.normalClass x hn) v) = v - d (a.inverse φ)
The orthogonal representative is obtained by subtracting the tangential component. The inverse of the induced metric recovers that component from the ambient metric covector. This pointwise identity needs no regularity assumption on the ambient metric.