Christoffel symbols of a nondegenerate metric in linear coordinates

Let g : E → E →L[ℝ] E →L[ℝ] ℝ be a field of symmetric nondegenerate bilinear forms on an open subset of a finite-dimensional real normed space E, as a metric reads in a chart. No positivity is assumed, so pseudo-Riemannian metrics are included. Writing Dg(u) for the derivative of the metric coefficients in the direction u, the Christoffel symbols of the first kind are the covectors

Γ₁(u, v)(w) = (Dg(u)(v, w) + Dg(v)(u, w) - Dg(w)(u, v)) / 2,

and the Christoffel symbols of the second kind Γ(u, v) are the vectors obtained by raising the index with the metric: g(Γ(u, v), w) = Γ₁(u, v)(w) for all w. Raising the index is the inverse of the musical map v ↦ g(v, ·), which is invertible by nondegeneracy. The map Γ is bundled as a continuous bilinear map, so that its smoothness in the base point is a statement about a single function.

These are the coefficients of the Levi-Civita connection in a chart, and this file proves the characteristic local facts behind the Koszul construction of that connection:

• Γ is symmetric, which is torsion-freeness in coordinates;
• Dg(u)(v, w) = g(Γ(u, v), w) + g(v, Γ(u, w)), which is metric compatibility in coordinates;
• Γ is the only symmetric bilinear map with this compatibility property, using only nondegeneracy;
• if g is C^(n+1) on an open set, or at a point where it is nondegenerate, then Γ is C^n there, since inversion of the musical map is smooth;
• in a basis, Γ^k_ij = (1/2) Σ_l g^(kl) (∂_i g_jl + ∂_j g_il - ∂_l g_ij) with g^(kl) the inverse of the Gram matrix of the metric.

Main definitions and results

• TauCeti.Manifold.christoffelFirstKind: the Christoffel symbols of the first kind.
• TauCeti.Manifold.christoffelSecondKind: the Christoffel symbols of the second kind.
• TauCeti.Manifold.christoffelSecondKindOfJet: the Christoffel formula on metric first jets.
• ContinuousLinearMap.IsInvertible.contDiffAt_christoffelSecondKindOfJet: smoothness at invertible metric values.
• TauCeti.Manifold.apply_christoffelSecondKind: lowering the index of Γ gives Γ₁.
• TauCeti.Manifold.christoffelSecondKind_comm: Γ is symmetric.
• TauCeti.Manifold.fderiv_apply_eq_christoffelSecondKind_add: metric compatibility of Γ.
• TauCeti.Manifold.eq_christoffelSecondKind_iff: Γ is the unique symmetric compatible bilinear map.
• TauCeti.Manifold.contDiffOn_christoffelSecondKind and TauCeti.Manifold.contDiffAt_christoffelSecondKind: smoothness of Γ.
• TauCeti.Manifold.hasFDerivAt_repr_christoffelSecondKind: differentiability of the coordinates of Γ in a basis.
• TauCeti.Manifold.repr_christoffelSecondKind: the classical index formula.

References

• B. O'Neill, Semi-Riemannian Geometry with Applications to Relativity, Academic Press (1983), Chapter 3: the Levi-Civita connection of a nondegenerate metric and its Christoffel symbols.
• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 5: the Christoffel symbols of a metric in coordinates.

The Christoffel symbols of the first kind

noncomputable def TauCeti.Manifold.christoffelFirstKind {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : E → E →L[ℝ] E →L[ℝ] ℝ) (x u v : E) : E →L[ℝ] ℝ

The Christoffel symbols of the first kind of a field of bilinear forms g at x: the covector Γ₁(u, v) = w ↦ (Dg(u)(v, w) + Dg(v)(u, w) - Dg(w)(u, v)) / 2, where Dg is the derivative of g at x.

@[simp]

theorem TauCeti.Manifold.christoffelFirstKind_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : E → E →L[ℝ] E →L[ℝ] ℝ) (x u v w : E) : (christoffelFirstKind g x u v) w = ((((fderiv ℝ g x) u) v) w + (((fderiv ℝ g x) v) u) w - (((fderiv ℝ g x) w) u) v) / 2

Evaluation of the Christoffel symbols of the first kind.

theorem TauCeti.Manifold.christoffelFirstKind_eq_of_differentiableAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : E → E →L[ℝ] E →L[ℝ] ℝ} {x : E} (hg : DifferentiableAt ℝ g x) (u v : E) : christoffelFirstKind g x u v = 2⁻¹ • (((fderiv ℝ g x) u) v + ((fderiv ℝ g x) v) u - fderiv ℝ (fun (y : E) => ((g y) u) v) x)

At a point where g is differentiable, the Christoffel symbols of the first kind of g, with the last term written as the derivative of the scalar function y ↦ g y u v.

theorem TauCeti.Manifold.christoffelFirstKind_comm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : E → E →L[ℝ] E →L[ℝ] ℝ} {x : E} (hsymm : ∀ᶠ (y : E) in nhds x, (g y).toBilinForm.IsSymm) (u v : E) : christoffelFirstKind g x u v = christoffelFirstKind g x v u

The Christoffel symbols of the first kind of a metric are symmetric in their first two arguments.

theorem TauCeti.Manifold.christoffelFirstKind_add_christoffelFirstKind {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : E → E →L[ℝ] E →L[ℝ] ℝ} {x : E} (hsymm : ∀ᶠ (y : E) in nhds x, (g y).toBilinForm.IsSymm) (u v w : E) : (christoffelFirstKind g x u v) w + (christoffelFirstKind g x u w) v = (((fderiv ℝ g x) u) v) w

The Christoffel symbols of the first kind of a metric, summed over the two orders of their last two arguments, give the derivative of the metric.

The Christoffel symbols of the second kind

noncomputable def TauCeti.Manifold.christoffelSecondKindOfJet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (j : (E →L[ℝ] E →L[ℝ] ℝ) × (E →L[ℝ] E →L[ℝ] E →L[ℝ] ℝ)) : E →L[ℝ] E →L[ℝ] E

The Christoffel symbols determined by a metric value and its first derivative. The first component of the jet is the musical map, and the second is the derivative of the metric.

@[simp]

theorem TauCeti.Manifold.christoffelSecondKindOfJet_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (j : (E →L[ℝ] E →L[ℝ] ℝ) × (E →L[ℝ] E →L[ℝ] E →L[ℝ] ℝ)) (u v : E) : ((christoffelSecondKindOfJet j) u) v = j.1.inverse (2⁻¹ • ((j.2 u) v + (j.2 v) u - (j.2.flip u).flip v))

Evaluation of the Christoffel formula on a metric first jet.

noncomputable def TauCeti.Manifold.christoffelSecondKind {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : E → E →L[ℝ] E →L[ℝ] ℝ) (x : E) : E →L[ℝ] E →L[ℝ] E

The Christoffel symbols of the second kind of a field of bilinear forms g at x: the bilinear map Γ with g(Γ(u, v), w) = Γ₁(u, v)(w), obtained from the Christoffel symbols of the first kind Γ₁ by inverting the musical map g x : E →L[ℝ] E →L[ℝ] ℝ. When g x is not invertible this inverse, and hence Γ, is zero.

theorem TauCeti.Manifold.christoffelSecondKind_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : E → E →L[ℝ] E →L[ℝ] ℝ) (x : E) : christoffelSecondKind g x = christoffelSecondKindOfJet (g x, fderiv ℝ g x)

The Christoffel symbols at a point depend only on the metric value and its derivative.

@[instance_reducible]

noncomputable def TauCeti.Manifold.christoffelBilinearNormedAddCommGroup {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] : NormedAddCommGroup (E →L[ℝ] E →L[ℝ] ℝ)

The canonical normed additive group on metric bilinear forms, cached for jet regularity.

@[instance_reducible]

noncomputable def TauCeti.Manifold.christoffelBilinearNormedSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] : NormedSpace ℝ (E →L[ℝ] E →L[ℝ] ℝ)

The canonical real normed space on metric bilinear forms, cached for jet regularity.

theorem ContinuousLinearMap.IsInvertible.contDiffAt_christoffelSecondKindOfJet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {n : WithTop ℕ∞} {j : (E →L[ℝ] E →L[ℝ] ℝ) × (E →L[ℝ] E →L[ℝ] E →L[ℝ] ℝ)} (hj : j.1.IsInvertible) : ContDiffAt ℝ n TauCeti.Manifold.christoffelSecondKindOfJet j

The Christoffel formula depends smoothly on the metric value and its first derivative wherever the musical map is invertible.

theorem TauCeti.Manifold.christoffelSecondKind_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : E → E →L[ℝ] E →L[ℝ] ℝ) (x u v : E) : ((christoffelSecondKind g x) u) v = (g x).inverse (christoffelFirstKind g x u v)

The Christoffel symbols of the second kind are the Christoffel symbols of the first kind with the index raised by the inverse musical map.

theorem TauCeti.Manifold.christoffelSecondKind_comm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : E → E →L[ℝ] E →L[ℝ] ℝ} {x : E} (hsymm : ∀ᶠ (y : E) in nhds x, (g y).toBilinForm.IsSymm) (u v : E) : ((christoffelSecondKind g x) u) v = ((christoffelSecondKind g x) v) u

The Christoffel symbols of the second kind of a metric are symmetric. In coordinates this is torsion-freeness of the Levi-Civita connection.

@[simp]

theorem TauCeti.Manifold.apply_christoffelSecondKind {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : E → E →L[ℝ] E →L[ℝ] ℝ} {x : E} [FiniteDimensional ℝ E] (hnd : (g x).toBilinForm.Nondegenerate) (u v w : E) : ((g x) (((christoffelSecondKind g x) u) v)) w = (christoffelFirstKind g x u v) w

Lowering the index of the Christoffel symbols of the second kind of a nondegenerate metric gives the Christoffel symbols of the first kind: g(Γ(u, v), w) = Γ₁(u, v)(w).

theorem TauCeti.Manifold.fderiv_apply_eq_christoffelSecondKind_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : E → E →L[ℝ] E →L[ℝ] ℝ} {x : E} [FiniteDimensional ℝ E] (hsymm : ∀ᶠ (y : E) in nhds x, (g y).toBilinForm.IsSymm) (hnd : (g x).toBilinForm.Nondegenerate) (u v w : E) : (((fderiv ℝ g x) u) v) w = ((g x) (((christoffelSecondKind g x) u) v)) w + ((g x) v) (((christoffelSecondKind g x) u) w)

Metric compatibility in coordinates. The derivative of a symmetric nondegenerate metric is Dg(u)(v, w) = g(Γ(u, v), w) + g(v, Γ(u, w)).

theorem TauCeti.Manifold.eq_christoffelSecondKind_of_fderiv_apply_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : E → E →L[ℝ] E →L[ℝ] ℝ} {x : E} [FiniteDimensional ℝ E] (hsymm : (g x).toBilinForm.IsSymm) (hnd : (g x).toBilinForm.Nondegenerate) {A : E →L[ℝ] E →L[ℝ] E} (hA : ∀ (u v : E), (A u) v = (A v) u) (hcomp : ∀ (u v w : E), (((fderiv ℝ g x) u) v) w = ((g x) ((A u) v)) w + ((g x) v) ((A u) w)) : A = christoffelSecondKind g x

Uniqueness of the Christoffel symbols. At a point where the metric is symmetric and nondegenerate, a symmetric bilinear map A with Dg(u)(v, w) = g(A(u, v), w) + g(v, A(u, w)) is the map of Christoffel symbols of the second kind.

theorem TauCeti.Manifold.eq_christoffelSecondKind_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : E → E →L[ℝ] E →L[ℝ] ℝ} {x : E} [FiniteDimensional ℝ E] (hsymm : ∀ᶠ (y : E) in nhds x, (g y).toBilinForm.IsSymm) (hnd : (g x).toBilinForm.Nondegenerate) {A : E →L[ℝ] E →L[ℝ] E} : A = christoffelSecondKind g x ↔ (∀ (u v : E), (A u) v = (A v) u) ∧ ∀ (u v w : E), (((fderiv ℝ g x) u) v) w = ((g x) ((A u) v)) w + ((g x) v) ((A u) w)

Characterization of the Christoffel symbols. Near a point where the metric is symmetric, and at which it is nondegenerate, the Christoffel symbols of the second kind are the unique symmetric bilinear map A with Dg(u)(v, w) = g(A(u, v), w) + g(v, A(u, w)).

Smoothness

theorem TauCeti.Manifold.contDiffAt_christoffelFirstKind {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : E → E →L[ℝ] E →L[ℝ] ℝ} {x : E} [FiniteDimensional ℝ E] {m n : WithTop ℕ∞} (hg : ContDiffAt ℝ m g x) (hnm : n + 1 ≤ m) (u v : E) : ContDiffAt ℝ n (fun (y : E) => christoffelFirstKind g y u v) x

Pointwise smoothness of the Christoffel symbols of the first kind. If a field of bilinear forms is C^m at x, then its Christoffel symbols of the first kind are C^n at x, for n + 1 ≤ m.

theorem TauCeti.Manifold.contDiffOn_christoffelFirstKind {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : E → E →L[ℝ] E →L[ℝ] ℝ} [FiniteDimensional ℝ E] {m n : WithTop ℕ∞} {U : Set E} (hU : IsOpen U) (hg : ContDiffOn ℝ m g U) (hnm : n + 1 ≤ m) (u v : E) : ContDiffOn ℝ n (fun (y : E) => christoffelFirstKind g y u v) U

The Christoffel symbols of the first kind of a C^m field of bilinear forms are C^n on an open set, for n + 1 ≤ m.

theorem TauCeti.Manifold.contDiffAt_christoffelSecondKind {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : E → E →L[ℝ] E →L[ℝ] ℝ} {x : E} [FiniteDimensional ℝ E] {m n : WithTop ℕ∞} (hg : ContDiffAt ℝ m g x) (hnm : n + 1 ≤ m) (hnd : (g x).toBilinForm.Nondegenerate) : ContDiffAt ℝ n (christoffelSecondKind g) x

Pointwise smoothness of the Christoffel symbols. If a field of bilinear forms is C^m at x and nondegenerate at x, then its Christoffel symbols of the second kind are C^n at x, for n + 1 ≤ m.

theorem TauCeti.Manifold.contDiffOn_christoffelSecondKind {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : E → E →L[ℝ] E →L[ℝ] ℝ} [FiniteDimensional ℝ E] {m n : WithTop ℕ∞} {U : Set E} (hU : IsOpen U) (hg : ContDiffOn ℝ m g U) (hnm : n + 1 ≤ m) (hnd : ∀ y ∈ U, (g y).toBilinForm.Nondegenerate) : ContDiffOn ℝ n (christoffelSecondKind g) U

Smoothness of the Christoffel symbols. If a field of nondegenerate bilinear forms is C^m on an open set, then its Christoffel symbols of the second kind are C^n there, for n + 1 ≤ m.

theorem TauCeti.Manifold.hasFDerivAt_repr_christoffelSecondKind {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : E → E →L[ℝ] E →L[ℝ] ℝ} {x : E} [FiniteDimensional ℝ E] {ι : Type u_2} (b : Module.Basis ι ℝ E) (hg : ContDiffAt ℝ 2 g x) (hnd : (g x).toBilinForm.Nondegenerate) (i j k : ι) : HasFDerivAt (fun (y : E) => (b.repr (((christoffelSecondKind g y) (b i)) (b j))) k) (LinearMap.toContinuousLinearMap (b.coord k) ∘SL fderiv ℝ (fun (y : E) => ((christoffelSecondKind g y) (b i)) (b j)) x) x

The coordinates of the Christoffel symbols of the second kind of a C² field g of bilinear forms, nondegenerate at x, are differentiable at x, with derivative the coordinates of the derivative of the Christoffel symbols.

theorem TauCeti.Manifold.eventuallyEq_apply_christoffelSecondKind {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : E → E →L[ℝ] E →L[ℝ] ℝ} {x : E} [FiniteDimensional ℝ E] (hg : ∀ᶠ (y : E) in nhds x, DifferentiableAt ℝ g y) (hnd : (g x).toBilinForm.Nondegenerate) (u v w : E) : (fun (y : E) => ((g y) (((christoffelSecondKind g y) u) v)) w) =ᶠ[nhds x] fun (y : E) => 2⁻¹ * ((fderiv ℝ (fun (y' : E) => ((g y') v) w) y) u + (fderiv ℝ (fun (y' : E) => ((g y') u) w) y) v - (fderiv ℝ (fun (y' : E) => ((g y') u) v) y) w)

Near a point where a field g of bilinear forms is differentiable on a neighbourhood and nondegenerate, lowering the index of the Christoffel symbols of the second kind gives the first-kind formula in terms of the derivatives of the scalar functions y ↦ g y u v.

The index formula

theorem TauCeti.Manifold.repr_christoffelSecondKind {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : E → E →L[ℝ] E →L[ℝ] ℝ} {x : E} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (hsymm : (g x).toBilinForm.IsSymm) (hnd : (g x).toBilinForm.Nondegenerate) (b : Module.Basis ι ℝ E) (i j k : ι) : (b.repr (((christoffelSecondKind g x) (b i)) (b j))) k = 2⁻¹ * ∑ l : ι, ((LinearMap.toMatrix₂ b b) (g x).toBilinForm)⁻¹ k l * ((((fderiv ℝ g x) (b i)) (b j)) (b l) + (((fderiv ℝ g x) (b j)) (b i)) (b l) - (((fderiv ℝ g x) (b l)) (b i)) (b j))

The index formula for the Christoffel symbols. For a basis b of E, the k-th coordinate of Γ(b i, b j) is (1/2) Σ_l g^(kl) (∂_i g_jl + ∂_j g_il - ∂_l g_ij), where g^(kl) is the inverse of the Gram matrix g_ij = g(b i, b j) of the symmetric nondegenerate metric at x, and ∂_i g_jl = Dg(b i)(b j, b l).