Killing vector fields on Euclidean space

TheoremKilling fields on Euclidean space#✓fully proved

Let \(F\) be a finite-dimensional real inner product space, viewed as a Riemannian manifold with the metric given by its inner product. A vector field \(V\) on \(F\) is Killing if and only if \(V\) is \(C^\infty\) and its derivative is skew-adjoint at every point: for all \(x, u, w \in F\), \(\langle DV(x)\,u, w \rangle + \langle u, DV(x)\,w \rangle = 0\).

theorem Manifold.isKillingVectorField_vectorSpace_iff
    {V : Π y : F, TangentSpace 𝓘(ℝ, F) y} :
    Manifold.IsKillingVectorField 𝓘(ℝ, F) V ↔ ContDiff ℝ ∞ V ∧
      ∀ (x : F) (u w : TangentSpace 𝓘(ℝ, F) x),
        inner ℝ (fderiv ℝ V x u) w + inner ℝ u (fderiv ℝ V x w) = 0

Uses 2 · Used by 2

Statement usesKilling vector field

Proof usesThe Levi-Civita connection of a vector space is the Fréchet derivative

Used byTranslations are Killing · Linear Killing fields on Euclidean space

TheoremTranslations are Killing#✓fully proved

Let \(F\) be a finite-dimensional real inner product space, viewed as a Riemannian manifold with the metric given by its inner product. For every \(c \in F\), the constant vector field \(y \mapsto c\) on \(F\) is Killing.

theorem Manifold.isKillingVectorField_const (c : F) :
    Manifold.IsKillingVectorField 𝓘(ℝ, F)
      (fun y : F => show TangentSpace 𝓘(ℝ, F) y from c)

Uses 2

Statement usesKilling vector field

Proof usesKilling fields on Euclidean space

TheoremLinear Killing fields on Euclidean space#✓fully proved

Let \(F\) be a finite-dimensional real inner product space, viewed as a Riemannian manifold with the metric given by its inner product, and let \(A \colon F \to F\) be a continuous linear map. The linear vector field \(y \mapsto A y\) is Killing if and only if \(A\) is skew-adjoint: \(\langle A u, w \rangle + \langle u, A w \rangle = 0\) for all \(u, w \in F\).

theorem Manifold.isKillingVectorField_continuousLinearMap_iff (A : F →L[ℝ] F) :
    Manifold.IsKillingVectorField 𝓘(ℝ, F)
      (fun y : F => show TangentSpace 𝓘(ℝ, F) y from A y) ↔
      ∀ u w : F, inner ℝ (A u) w + inner ℝ u (A w) = 0

Uses 2

Statement usesKilling vector field

Proof usesKilling fields on Euclidean space

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.