The second fundamental form of a map into an inner product space

Let i : V → E be a map from a finite-dimensional normed space over 𝕜 = ℝ or ℂ into an inner product space over 𝕜. Its tangent space at x is the range of the derivative Di(x), and its normal space is the orthogonal complement (Di(x)).rangeᗮ. The second fundamental form TauCeti.secondFundamentalForm 𝕜 i x is the normal component of the second derivative,

B(v, w) = P_N (D²i(x)(v, w)),

where P_N is the orthogonal projection onto the normal space. When i is an immersion parametrising a submanifold of E, this is the second fundamental form of the submanifold, evaluated on the tangent vectors Di(x) v and Di(x) w (the Gauss formula). It is symmetric, and it is unchanged by a reparametrisation of the source, up to the derivative of the reparametrisation: the second derivative of a change of coordinates contributes only a tangent term, which the projection removes.

For a holomorphic map into a complex inner product space, the real and complex constructions are compared. Equip E with the real inner product re ⟪x, y⟫. The real tangent space and the real normal space are then complex subspaces, so multiplication by I (the complex structure J) preserves both. The real second fundamental form secondFundamentalForm ℝ i x agrees with the complex-bilinear, normal-valued form secondFundamentalForm ℂ i x, which gives the identities

B(Jv, w) = J B(v, w) = B(v, Jw) and B(Jv, Jw) = -B(v, w).

These identities are what make the shape operators of a complex submanifold anticommute with J, so that their eigenvalues come in pairs ±λ.

Main definitions

• TauCeti.secondFundamentalForm 𝕜 i x: the normal component of the second derivative of i.

Main results

• TauCeti.secondFundamentalForm_apply_mem_orthogonal: the second fundamental form is normal-valued.
• TauCeti.inner_secondFundamentalForm_apply_of_mem_orthogonal: against a normal vector, the second fundamental form pairs like the second derivative.
• ContDiffAt.secondFundamentalForm_apply_comm: symmetry.
• ContDiffAt.secondFundamentalForm_comp: invariance under reparametrisation of the source.
• DifferentiableAt.orthogonal_range_fderiv_restrictScalars: the real normal space of a holomorphic map is its complex normal space.
• ContDiffAt.secondFundamentalForm_restrictScalars_apply: the real second fundamental form of a holomorphic map is its complex second fundamental form.
• ContDiffAt.secondFundamentalForm_I_smul_left, ContDiffAt.secondFundamentalForm_I_smul_right, ContDiffAt.secondFundamentalForm_I_smul_I_smul: the identities displayed above.

References

• J. Milnor, Morse Theory, Princeton University Press, 1963, Section 7.
• S. Kobayashi and K. Nomizu, Foundations of Differential Geometry, Vol. II, Chapter IX.
• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer, 2018, Chapter 8.

noncomputable def TauCeti.secondFundamentalForm (𝕜 : Type u_1) {V : Type u_2} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (i : V → E) (x : V) : V →L[𝕜] V →L[𝕜] E

The second fundamental form of i : V → E at x: the component of the second derivative D²i(x)(v, w) orthogonal to the tangent space (Di(x)).range. For an immersion this is the second fundamental form of the parametrised submanifold, evaluated on Di(x) v and Di(x) w.

theorem TauCeti.secondFundamentalForm_apply {𝕜 : Type u_1} {V : Type u_2} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (i : V → E) (x v w : V) : ((secondFundamentalForm 𝕜 i x) v) w = (↑(fderiv 𝕜 i x)).rangeᗮ.starProjection (((fderiv 𝕜 (fderiv 𝕜 i) x) v) w)

The second fundamental form is the normal projection of the second derivative.

@[simp]

theorem TauCeti.secondFundamentalForm_apply_mem_orthogonal {𝕜 : Type u_1} {V : Type u_2} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (i : V → E) (x v w : V) : ((secondFundamentalForm 𝕜 i x) v) w ∈ (↑(fderiv 𝕜 i x)).rangeᗮ

The second fundamental form takes values in the normal space.

theorem TauCeti.inner_secondFundamentalForm_apply_of_mem_orthogonal {𝕜 : Type u_1} {V : Type u_2} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {i : V → E} {x : V} {ν : E} (hν : ν ∈ (↑(fderiv 𝕜 i x)).rangeᗮ) (v w : V) : inner 𝕜 ν (((secondFundamentalForm 𝕜 i x) v) w) = inner 𝕜 ν (((fderiv 𝕜 (fderiv 𝕜 i) x) v) w)

Paired with a normal vector ν, the second fundamental form agrees with the second derivative: ⟪ν, B(v, w)⟫ = ⟪ν, D²i(x)(v, w)⟫.

theorem ContDiffAt.secondFundamentalForm_apply_comm {𝕜 : Type u_1} {V : Type u_2} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {i : V → E} {x : V} (hi : ContDiffAt 𝕜 2 i x) (v w : V) : ((TauCeti.secondFundamentalForm 𝕜 i x) v) w = ((TauCeti.secondFundamentalForm 𝕜 i x) w) v

The second fundamental form of a C² map is symmetric.

theorem ContDiffAt.secondFundamentalForm_comp {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup W] [NormedSpace 𝕜 W] [FiniteDimensional 𝕜 W] {i : V → E} {φ : W → V} {y : W} (hi : ContDiffAt 𝕜 2 i (φ y)) (hφ : ContDiffAt 𝕜 2 φ y) (hsurj : Function.Surjective ⇑(fderiv 𝕜 φ y)) (v w : W) : ((TauCeti.secondFundamentalForm 𝕜 (i ∘ φ) y) v) w = ((TauCeti.secondFundamentalForm 𝕜 i (φ y)) ((fderiv 𝕜 φ y) v)) ((fderiv 𝕜 φ y) w)

Invariance under reparametrisation. If φ : W → V is C² at y with surjective derivative, then the second fundamental form of i ∘ φ at y is that of i at φ y, evaluated on the images under Dφ(y). The term Di(D²φ(v, w)) of the second-order chain rule is tangent, and the normal projection removes it.

Holomorphic maps

The real inner product re ⟪x, y⟫ on a complex inner product space is enabled locally; the real second fundamental form below is taken with respect to it.

theorem DifferentiableAt.orthogonal_range_fderiv_restrictScalars {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [InnerProductSpace ℂ E] {i : V → E} {x : V} (hi : DifferentiableAt ℂ i x) : (↑(fderiv ℝ i x)).rangeᗮ = Submodule.restrictScalars ℝ (↑(fderiv ℂ i x)).rangeᗮ

The real normal space of a complex-differentiable map, for the real inner product re ⟪x, y⟫, is its complex normal space; in particular it is stable under multiplication by I.

theorem ContDiffAt.secondFundamentalForm_restrictScalars_apply {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [InnerProductSpace ℂ E] {i : V → E} {x : V} [FiniteDimensional ℂ V] (hi : ContDiffAt ℂ 2 i x) (v w : V) : ((TauCeti.secondFundamentalForm ℝ i x) v) w = ((TauCeti.secondFundamentalForm ℂ i x) v) w

The real second fundamental form of a holomorphic map is its complex second fundamental form. In particular it is complex bilinear.

@[simp]

theorem ContDiffAt.secondFundamentalForm_I_smul_left {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [InnerProductSpace ℂ E] {i : V → E} {x : V} [FiniteDimensional ℂ V] (hi : ContDiffAt ℂ 2 i x) (v w : V) : ((TauCeti.secondFundamentalForm ℝ i x) (Complex.I • v)) w = Complex.I • ((TauCeti.secondFundamentalForm ℝ i x) v) w

The real second fundamental form of a holomorphic map satisfies B(Jv, w) = J B(v, w).

@[simp]

theorem ContDiffAt.secondFundamentalForm_I_smul_right {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [InnerProductSpace ℂ E] {i : V → E} {x : V} [FiniteDimensional ℂ V] (hi : ContDiffAt ℂ 2 i x) (v w : V) : ((TauCeti.secondFundamentalForm ℝ i x) v) (Complex.I • w) = Complex.I • ((TauCeti.secondFundamentalForm ℝ i x) v) w

The real second fundamental form of a holomorphic map satisfies B(v, Jw) = J B(v, w).

theorem ContDiffAt.secondFundamentalForm_I_smul_I_smul {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [InnerProductSpace ℂ E] {i : V → E} {x : V} [FiniteDimensional ℂ V] (hi : ContDiffAt ℂ 2 i x) (v w : V) : ((TauCeti.secondFundamentalForm ℝ i x) (Complex.I • v)) (Complex.I • w) = -((TauCeti.secondFundamentalForm ℝ i x) v) w

The real second fundamental form of a holomorphic map satisfies B(Jv, Jw) = -B(v, w).