Documentation

TauCeti.Geometry.Manifold.Riemannian.Nil.Connection

The Levi-Civita connection of Nil #

This file computes the Levi-Civita connection of the model geometry Nil, the space ℝ³ with coordinates (x, y, z) and the left-invariant metric dx² + dy² + (dz - x dy)². Writing θ(v) = v₃ - x v₂ for the contact form dz - x dy, the Christoffel formula of the first kind shows that at a point with first coordinate x the derivative of the constant field v in the direction u is

Γ(u, v) = ½ (u₂ θ(v) + v₂ θ(u), -(u₁ θ(v) + v₁ θ(u)), -(u₁ v₂ + v₁ u₂) - x (u₁ θ(v) + v₁ θ(u))).

This is also the Christoffel map of Nil in its global chart, the input of the coordinate formula for the curvature tensor.

The left-invariant vector fields X_a = mulInvariantVectorField a of Nil are the left translates X_a(p) = (a₁, a₂, a₃ + x a₂) of the tangent vectors a at the identity. In particular E₁ = ∂_x, E₂ = ∂_y + x ∂_z and E₃ = ∂_z form a left-invariant orthonormal frame, with [E₁, E₂] = E₃ the only nonzero bracket. The Levi-Civita connection preserves left-invariant fields: ∇_{X_a} X_b = X_c with c = ½ (a₂ b₃ + b₂ a₃, -(a₁ b₃ + b₁ a₃), a₁ b₂ - a₂ b₁). This is the classical table ∇_{E₁} E₂ = ½ E₃ = -∇_{E₂} E₁, ∇_{E₁} E₃ = ∇_{E₃} E₁ = -½ E₂, ∇_{E₂} E₃ = ∇_{E₃} E₂ = ½ E₁, with all other entries zero.

Main results #

References #

The Christoffel map #

source
@[simp]
theorem TauCeti.Nil.leviCivitaConnection_const_apply (p : Nil) (u v : ℝ × ℝ × ℝ) :
(tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) ((↑(CovariantDerivative.leviCivitaConnection (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) Nil) (fun (q : Nil) => (tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) q).symm v) p) ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p).symm u)) = ((u.2.1 * (v.2.2 - p.x * v.2.1) + v.2.1 * (u.2.2 - p.x * u.2.1)) / 2, -(u.1 * (v.2.2 - p.x * v.2.1) + v.1 * (u.2.2 - p.x * u.2.1)) / 2, -(u.1 * v.2.1 + v.1 * u.2.1) / 2 - p.x * (u.1 * (v.2.2 - p.x * v.2.1) + v.1 * (u.2.2 - p.x * u.2.1)) / 2)

The Levi-Civita derivative of the constant field v of Nil in the direction u, at a point p with first coordinate x, is ½ (u₂ θ(v) + v₂ θ(u), -(u₁ θ(v) + v₁ θ(u)), -(u₁ v₂ + v₁ u₂) - x (u₁ θ(v) + v₁ θ(u))), where θ(v) = v₃ - x v₂. Tangent vectors are read in the model space ℝ³.

source
@[simp]
theorem TauCeti.Nil.christoffelMap_leviCivitaConnection_apply {ι : Type u_1} [Fintype ι] (b : Module.Basis ι ℝ (ℝ × ℝ × ℝ)) (p : Nil) (u v : ℝ × ℝ × ℝ) :
((Manifold.christoffelMap b ⋯ p) v) u = ((u.2.1 * (v.2.2 - p.x * v.2.1) + v.2.1 * (u.2.2 - p.x * u.2.1)) / 2, -(u.1 * (v.2.2 - p.x * v.2.1) + v.1 * (u.2.2 - p.x * u.2.1)) / 2, -(u.1 * v.2.1 + v.1 * u.2.1) / 2 - p.x * (u.1 * (v.2.2 - p.x * v.2.1) + v.1 * (u.2.2 - p.x * u.2.1)) / 2)

The Christoffel map of Nil in its global chart, for any basis of ℝ³: with the field value v first and the direction u second, it is the derivative of the constant field v computed in leviCivitaConnection_const_apply.

Left-invariant vector fields #

source
@[simp]
theorem TauCeti.Nil.tangentSpaceCastModel_mulInvariantVectorField (a : ℝ × ℝ × ℝ) (p : Nil) :
(tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) (mulInvariantVectorField a p) = (a.1, a.2.1, a.2.2 + p.x * a.2.1)

The left-invariant vector field mulInvariantVectorField a of Nil, the left translate of the tangent vector a at the identity, has value (a₁, a₂, a₃ + x a₂) at a point with first coordinate x, read in the model space ℝ³.

source
theorem TauCeti.Nil.leviCivitaConnection_mulInvariantVectorField (a b : ℝ × ℝ × ℝ) (p : Nil) :
(↑(CovariantDerivative.leviCivitaConnection (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) Nil) (mulInvariantVectorField b) p) (mulInvariantVectorField a p) = mulInvariantVectorField ((a.2.1 * b.2.2 + b.2.1 * a.2.2) / 2, -(a.1 * b.2.2 + b.1 * a.2.2) / 2, (a.1 * b.2.1 - a.2.1 * b.1) / 2) p

The Levi-Civita connection of Nil on left-invariant fields. The Levi-Civita derivative of the left-invariant field X_b along X_a is the left-invariant field X_c with c = ½ (a₂ b₃ + b₂ a₃, -(a₁ b₃ + b₁ a₃), a₁ b₂ - a₂ b₁).