Christoffel symbols of a nondegenerate Levi-Civita connection in a chart

Let g be a smooth symmetric nondegenerate metric on M, of any signature. Read in the chart at x₀, it becomes a field chartMetric g x₀ : E → E →L[ℝ] E →L[ℝ] ℝ of symmetric nondegenerate bilinear forms on the chart target. This file identifies the Christoffel map of a Levi-Civita connection of g, read in the canonical tangent-bundle trivialization at x₀, with the Christoffel symbols of the second kind christoffelSecondKind of the chart metric. In particular the scalar Christoffel symbols of the connection are given on the chart domain by the classical index formula

Γᵏᵢⱼ = (1/2) Σ_l g^(kl) (∂ᵢ g_jl + ∂ⱼ g_il - ∂_l g_ij).

The index formula using derivatives within the chart target holds throughout the chart domain, including boundary and corner points. At interior chart points it also holds with unrestricted Fréchet derivatives, giving the comparison with christoffelSecondKind. Its metric input is the coordinate form Dg(u)(v, w) = g(Γ(u, v), w) + g(v, Γ(u, w)) of metric compatibility, valid for every compatible connection. No extension of the chart metric to an open model domain is assumed in the within-derivative formula.

Main definitions and results

In the namespace TauCeti.Manifold.ContMDiffNondegenerateMetric:

• IsMetricCompatible.fderivWithin_chartMetric_apply: metric compatibility throughout a chart target, using within derivatives; fderiv_chartMetric_apply is its interior form.
• IsLeviCivitaConnection.christoffelMap_apply_eq_christoffelSecondKind: the Christoffel map of a Levi-Civita connection is given by the Christoffel symbols of the second kind of the chart metric.
• IsLeviCivitaConnection.christoffelSymbol_eq_fderivWithin: the inverse-matrix index formula throughout the chart domain; christoffelSymbol_eq is its interior form.
• IsLeviCivitaConnection.christoffelSymbol_eventuallyEq: near a point, the scalar Christoffel symbols are the coordinates of the Christoffel symbols of the second kind of the chart metric.

References

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

Metric compatibility in coordinates

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.IsMetricCompatible.fderivWithin_chartMetric_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {g : ContMDiffNondegenerateMetric} {x₀ y : M} [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] (b : Module.Basis ι ℝ E) {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} (h : g.IsMetricCompatible cov) (hy : y ∈ (extChartAt I x₀).source) (u v w : E) : (((fderivWithin ℝ (g.chartMetric x₀) (extChartAt I x₀).target (↑(extChartAt I x₀) y)) u) v) w = ((g.chartMetric x₀ (↑(extChartAt I x₀) y)) (((christoffelMap b ⋯ y) v) u)) w + ((g.chartMetric x₀ (↑(extChartAt I x₀) y)) v) (((christoffelMap b ⋯ y) w) u)

Metric compatibility in coordinates. Let ∇ be compatible with the nondegenerate metric g, and let y be any point of the chart domain at x₀, including a boundary or corner point. Writing G for the chart metric and Γ(u, v) = christoffelMap b _ y v u for the Christoffel map of ∇ in the trivialization at x₀, applied to the field value v and the direction u, the derivative within the chart target is DG(u)(v, w) = G(Γ(u, v), w) + G(v, Γ(u, w)).

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.IsMetricCompatible.fderiv_chartMetric_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {g : ContMDiffNondegenerateMetric} {x₀ y : M} [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] (b : Module.Basis ι ℝ E) {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} (h : g.IsMetricCompatible cov) (hy : y ∈ (extChartAt I x₀).source) (hint : ↑(extChartAt I x₀) y ∈ interior (Set.range ↑I)) (u v w : E) : (((fderiv ℝ (g.chartMetric x₀) (↑(extChartAt I x₀) y)) u) v) w = ((g.chartMetric x₀ (↑(extChartAt I x₀) y)) (((christoffelMap b ⋯ y) v) u)) w + ((g.chartMetric x₀ (↑(extChartAt I x₀) y)) v) (((christoffelMap b ⋯ y) w) u)

Metric compatibility in coordinates. Let ∇ be compatible with the nondegenerate metric g, and let y be a point of the chart domain at x₀ whose chart image lies in the interior of the model. Writing G for the chart metric and Γ(u, v) = christoffelMap b _ y v u for the Christoffel map of ∇ in the trivialization at x₀, applied to the field value v and the direction u, the derivative of the chart metric is DG(u)(v, w) = G(Γ(u, v), w) + G(v, Γ(u, w)).

The Christoffel symbols of a Levi-Civita connection

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.IsLeviCivitaConnection.christoffelMap_apply_eq_christoffelSecondKind {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {g : ContMDiffNondegenerateMetric} {x₀ y : M} [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] (b : Module.Basis ι ℝ E) {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} (h : g.IsLeviCivitaConnection cov) (hy : y ∈ (extChartAt I x₀).source) (hint : ↑(extChartAt I x₀) y ∈ interior (Set.range ↑I)) (v u : E) : ((christoffelMap b ⋯ y) v) u = ((christoffelSecondKind (g.chartMetric x₀) (↑(extChartAt I x₀) y)) u) v

The Christoffel map of a Levi-Civita connection in a chart. Let ∇ be a Levi-Civita connection of the nondegenerate metric g, and let y be a point of the chart domain at x₀ whose chart image lies in the interior of the model. The Christoffel map of ∇ in the trivialization at x₀, applied to the field value v and the direction u, is the Christoffel symbol of the second kind christoffelSecondKind of the chart metric at the chart image of y, applied to u and v.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.IsLeviCivitaConnection.christoffelSymbol_eq_fderivWithin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {g : ContMDiffNondegenerateMetric} {x₀ y : M} [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] (b : Module.Basis ι ℝ E) {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} [DecidableEq ι] (h : g.IsLeviCivitaConnection cov) (hy : y ∈ (extChartAt I x₀).source) (i j k : ι) : christoffelSymbol I b (trivializationAt E (TangentSpace I) x₀) (↑cov) i j k y = 2⁻¹ * ∑ l : ι, ((LinearMap.toMatrix₂ b b) (g.chartMetric x₀ (↑(extChartAt I x₀) y)).toBilinForm)⁻¹ k l * ((((fderivWithin ℝ (g.chartMetric x₀) (extChartAt I x₀).target (↑(extChartAt I x₀) y)) (b i)) (b j)) (b l) + (((fderivWithin ℝ (g.chartMetric x₀) (extChartAt I x₀).target (↑(extChartAt I x₀) y)) (b j)) (b i)) (b l) - (((fderivWithin ℝ (g.chartMetric x₀) (extChartAt I x₀).target (↑(extChartAt I x₀) y)) (b l)) (b i)) (b j))

The index formula on the whole chart domain. The coordinate partial derivatives are Fréchet derivatives within the chart target, so the formula includes boundary and corner points and requires no extension of the metric to an open subset of the model space.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.IsLeviCivitaConnection.christoffelSymbol_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {g : ContMDiffNondegenerateMetric} {x₀ y : M} [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] (b : Module.Basis ι ℝ E) {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} [DecidableEq ι] (h : g.IsLeviCivitaConnection cov) (hy : y ∈ (extChartAt I x₀).source) (hint : ↑(extChartAt I x₀) y ∈ interior (Set.range ↑I)) (i j k : ι) : christoffelSymbol I b (trivializationAt E (TangentSpace I) x₀) (↑cov) i j k y = 2⁻¹ * ∑ l : ι, ((LinearMap.toMatrix₂ b b) (g.chartMetric x₀ (↑(extChartAt I x₀) y)).toBilinForm)⁻¹ k l * ((((fderiv ℝ (g.chartMetric x₀) (↑(extChartAt I x₀) y)) (b i)) (b j)) (b l) + (((fderiv ℝ (g.chartMetric x₀) (↑(extChartAt I x₀) y)) (b j)) (b i)) (b l) - (((fderiv ℝ (g.chartMetric x₀) (↑(extChartAt I x₀) y)) (b l)) (b i)) (b j))

The index formula for the Christoffel symbols of a Levi-Civita connection. Let ∇ be a Levi-Civita connection of the nondegenerate metric g, and b a basis of the model space. At a point y of the chart domain at x₀ whose chart image lies in the interior of the model, the Christoffel symbols of ∇ in the coordinate frame of b are Γᵏᵢⱼ = (1/2) Σ_l g^(kl) (∂ᵢ g_jl + ∂ⱼ g_il - ∂_l g_ij), where g_ij is the Gram matrix of the chart metric in the basis b, g^(kl) its inverse, and ∂ᵢ the derivative in the direction b i.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.IsLeviCivitaConnection.christoffelSymbol_eventuallyEq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {g : ContMDiffNondegenerateMetric} {x₀ y : M} [FiniteDimensional ℝ E] {ι : Type u_4} (b : Module.Basis ι ℝ E) {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} [Finite ι] (h : g.IsLeviCivitaConnection cov) (hy : y ∈ (extChartAt I x₀).source) (hint : ↑(extChartAt I x₀) y ∈ interior (Set.range ↑I)) (i j k : ι) : christoffelSymbol I b (trivializationAt E (TangentSpace I) x₀) (↑cov) i j k =ᶠ[nhds y] fun (y' : M) => (b.repr (((christoffelSecondKind (g.chartMetric x₀) (↑(extChartAt I x₀) y')) (b i)) (b j))) k

Near a point of the chart domain at x₀ whose chart image is interior, the Christoffel symbols of a Levi-Civita connection of g, in the frame of b, are the coordinates of the Christoffel symbols of the second kind of the chart metric.