Killing vector fields on a Riemannian manifold

StructureKilling vector field#✓fully proved

Let \(M\) be a finite-dimensional smooth manifold, possibly with boundary or corners, with a smooth Riemannian metric \(g = \langle \cdot, \cdot \rangle\) and its Levi-Civita connection \(\nabla\). A vector field \(X\) on \(M\) is a Killing vector field if \(X\) is smooth and satisfies Killing's equation: for every point \(x \in M\) and all tangent vectors \(u, v \in T_x M\),

\[\langle \nabla_u X, v \rangle + \langle u, \nabla_v X \rangle = 0.\]

In index notation this is \(\nabla_i X_j + \nabla_j X_i = 0\), and it is equivalent to the vanishing of the Lie derivative \(L_X g\) of the metric. Smoothness is part of the definition, as in the textbook definition.

structure IsKillingVectorField (X : (x : M) → TangentSpace I x) : Prop where
  contMDiff : CMDiff ∞ (T% X)
  inner_leviCivitaConnection_add : ∀ (x : M) (u v : TangentSpace I x),
    inner ℝ (leviCivitaConnection I M X x u) v +
      inner ℝ u (leviCivitaConnection I M X x v) = 0

Sources

• Burns and Matveev (2021), §10.2, for motivation: a Killing field \(V\) gives the linear first integral \(\xi \mapsto g(V, \xi)\) of geodesic flow.

Used by 11

Used bySum of Killing fields · Real multiples of Killing fields · Killing's equation on the diagonal · Killing fields via the diagonal of Killing's equation · Killing fields are those with vanishing Lie derivative of the metric · The zero field is Killing · Space of Killing vector fields · Membership in the space of Killing fields · Translations are Killing · Linear Killing fields on Euclidean space · Killing fields on Euclidean space

TheoremKilling's equation on the diagonal#✓fully proved

Let \(X\) be a Killing vector field on a smooth Riemannian manifold \(M\) with Levi-Civita connection \(\nabla\). Then \(\langle \nabla_u X, u \rangle = 0\) for every point \(x \in M\) and every tangent vector \(u \in T_x M\): a Killing field preserves lengths infinitesimally.

theorem IsKillingVectorField.inner_leviCivitaConnection_self
    {X : (x : M) → TangentSpace I x} (hX : IsKillingVectorField I X)
    (x : M) (u : TangentSpace I x) :
    inner ℝ (leviCivitaConnection I M X x u) u = 0

Uses 1 · Used by 1

Statement usesKilling vector field

Used byKilling fields via the diagonal of Killing's equation

TheoremKilling fields via the diagonal of Killing's equation#✓fully proved

Let \(M\) be a smooth Riemannian manifold with Levi-Civita connection \(\nabla\). A vector field \(X\) on \(M\) is a Killing vector field if and only if \(X\) is smooth and \(\langle \nabla_u X, u \rangle = 0\) for every point \(x \in M\) and every tangent vector \(u \in T_x M\).

The converse direction is a polarization argument.

theorem isKillingVectorField_iff_inner_leviCivitaConnection_self
    {X : (x : M) → TangentSpace I x} :
    IsKillingVectorField I X ↔ CMDiff ∞ (T% X) ∧
      ∀ (x : M) (u : TangentSpace I x),
        inner ℝ (leviCivitaConnection I M X x u) u = 0

Uses 2

Statement usesKilling vector field

Proof usesKilling's equation on the diagonal

TheoremThe Lie derivative of the metric via the Levi-Civita connection#✓fully proved

Let \(M\) be a smooth manifold modeled on a finite-dimensional real normed space (possibly with corners), with a smooth Riemannian metric \(g = \langle \cdot, \cdot \rangle\) and Levi-Civita connection \(\nabla\), and let \(X\), \(Y\), \(Z\) be vector fields on \(M\) that are differentiable at a point \(x\). Write \([\cdot, \cdot]\) for the Lie bracket of vector fields and \(X_x \langle Y, Z \rangle\) for the derivative at \(x\) of the function \(y \mapsto \langle Y_y, Z_y \rangle\) in the direction \(X_x\). Then

\[ X_x \langle Y, Z \rangle - \langle [X, Y]_x, Z_x \rangle - \langle Y_x, [X, Z]_x \rangle = \langle \nabla_{Y_x} X, Z_x \rangle + \langle Y_x, \nabla_{Z_x} X \rangle. \]

The left-hand side is \((\mathcal{L}_X g)(Y, Z)\) at \(x\).

theorem mvfderiv_inner_sub_inner_mlieBracket
    {X Y Z : (x : M) → TangentSpace I x} {x : M}
    (hX : MDiffAt (T% X) x) (hY : MDiffAt (T% Y) x) (hZ : MDiffAt (T% Z) x) :
    ((d% (fun y ↦ inner ℝ (Y y) (Z y)) x) (X x)) -
        inner ℝ (VectorField.mlieBracket I X Y x) (Z x) -
        inner ℝ (Y x) (VectorField.mlieBracket I X Z x) =
      inner ℝ (leviCivitaConnection I M X x (Y x)) (Z x) +
        inner ℝ (Y x) (leviCivitaConnection I M X x (Z x))

Used by 1

Used byKilling fields are those with vanishing Lie derivative of the metric

TheoremKilling fields are those with vanishing Lie derivative of the metric#✓fully proved

Let \(M\) be a smooth Riemannian manifold with metric \(g = \langle \cdot, \cdot \rangle\). A vector field \(X\) on \(M\) is a Killing vector field if and only if \(X\) is smooth and, for every point \(x \in M\) and all vector fields \(Y\) and \(Z\) on \(M\) that are differentiable at \(x\),

\[X_x \langle Y, Z \rangle - \langle [X, Y]_x, Z_x \rangle - \langle Y_x, [X, Z]_x \rangle = 0,\]

where \(X_x \langle Y, Z \rangle\) is the derivative at \(x\) of the function \(y \mapsto \langle Y_y, Z_y \rangle\) in the direction \(X_x\), and \([X, Y]\) is the Lie bracket. The left-hand side is \((L_X g)(Y, Z)\) at \(x\), where \(L_X g\) is the Lie derivative of \(g\) along \(X\).

theorem isKillingVectorField_iff_mvfderiv_inner
    {X : (x : M) → TangentSpace I x} :
    IsKillingVectorField I X ↔ CMDiff ∞ (T% X) ∧
      ∀ (x : M) (Y Z : (x : M) → TangentSpace I x), MDiffAt (T% Y) x →
        MDiffAt (T% Z) x → ((d% (fun y ↦ inner ℝ (Y y) (Z y)) x) (X x)) -
          inner ℝ (VectorField.mlieBracket I X Y x) (Z x) -
          inner ℝ (Y x) (VectorField.mlieBracket I X Z x) = 0

Uses 2

Statement usesKilling vector field

Proof usesThe Lie derivative of the metric via the Levi-Civita connection

TheoremThe zero field is Killing#✓fully proved

On a smooth Riemannian manifold, the zero vector field is a Killing vector field.

theorem isKillingVectorField_zero :
    IsKillingVectorField I (0 : (x : M) → TangentSpace I x)

Uses 1 · Used by 1

Statement usesKilling vector field

Used bySpace of Killing vector fields

TheoremSum of Killing fields#✓fully proved

On a smooth Riemannian manifold, the sum \(X + Y\) of two Killing vector fields \(X\) and \(Y\) is a Killing vector field.

theorem IsKillingVectorField.add {X Y : (x : M) → TangentSpace I x}
    (hX : IsKillingVectorField I X) (hY : IsKillingVectorField I Y) :
    IsKillingVectorField I (X + Y)

Uses 1 · Used by 1

Statement usesKilling vector field

Used bySpace of Killing vector fields

TheoremReal multiples of Killing fields#✓fully proved

On a smooth Riemannian manifold, if \(X\) is a Killing vector field and \(c\) is a real number, then \(c X\) is a Killing vector field.

theorem IsKillingVectorField.const_smul {X : (x : M) → TangentSpace I x}
    (hX : IsKillingVectorField I X) (c : ℝ) : IsKillingVectorField I (c • X)

Uses 1 · Used by 1

Statement usesKilling vector field

Used bySpace of Killing vector fields

DefinitionSpace of Killing vector fields#✓fully proved

For a smooth Riemannian manifold \(M\), the Killing vector fields on \(M\) form a real linear subspace of the real vector space of all (not necessarily continuous) vector fields on \(M\).

def killingVectorFields : Submodule ℝ (Π x : M, TangentSpace I x) where
  carrier := {X | IsKillingVectorField I X}
  zero_mem' := isKillingVectorField_zero I
  add_mem' := fun hX hY ↦ IsKillingVectorField.add I hX hY
  smul_mem' := fun c _X hX ↦ IsKillingVectorField.const_smul I hX c

Uses 4 · Used by 2

Statement usesKilling vector field · Sum of Killing fields · Real multiples of Killing fields · The zero field is Killing

Used byExtensionality for Killing fields · Membership in the space of Killing fields

TheoremMembership in the space of Killing fields#✓fully proved

A vector field \(X\) on a smooth Riemannian manifold \(M\) lies in the space of Killing vector fields on \(M\) if and only if \(X\) is a Killing vector field.

@[simp]
theorem mem_killingVectorFields {X : (x : M) → TangentSpace I x} :
    X ∈ killingVectorFields I M ↔ IsKillingVectorField I X

Uses 2

Statement usesKilling vector field · Space of Killing vector fields

TheoremExtensionality for Killing fields#✓fully proved

Two elements \(a\) and \(b\) of the space of Killing vector fields on a smooth Riemannian manifold \(M\) that agree at every point \(x \in M\) are equal.

@[ext]
theorem killingVectorFields.ext {a b : killingVectorFields I M}
    (h : ∀ x : M, (a : Π x : M, TangentSpace I x) x = (b : Π x : M, TangentSpace I x) x) :
    a = b

Uses 1

Statement usesSpace of Killing vector fields

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.