Curvature of Riemannian manifolds

DefinitionCurvature expression of a covariant derivative on extensions#✓fully proved

Let \(\nabla\) be a covariant derivative on a vector bundle \(V\) over a manifold \(M\), let \(x \in M\), let \(u, v \in T_x M\) and let \(\sigma \in V_x\). Let \(X\) and \(Y\) be the vector fields on \(M\) whose coordinates in the preferred local trivialization of \(TM\) at \(x\) are constant, equal to those of \(u\) and \(v\), on the base set of that trivialization, with a fixed but unspecified value at each point outside it; let \(S\) be the section of \(V\) obtained in the same way from \(\sigma\) and the preferred local trivialization of \(V\) at \(x\). The curvature expression of \(\nabla\) at \(x\) on \(u\), \(v\), \(\sigma\) is the vector

\[R(u, v)\sigma = \nabla_u (\nabla_Y S) - \nabla_v (\nabla_X S) - \nabla_{[X, Y](x)} S \in V_x,\]

where \(\nabla_Y S\) is the section \(y \mapsto \nabla_{Y(y)} S\) and \([X, Y]\) is the Lie bracket.

When \(\nabla\) sends \(C^2\) sections to \(C^1\) sections (for instance the Levi-Civita connection of a \(C^\infty\) metric), this is the curvature tensor \(R(X, Y) = \nabla_X \nabla_Y - \nabla_Y \nabla_X - \nabla_{[X, Y]}\) applied to \(u\), \(v\), \(\sigma\), and it does not depend on the extensions. For other connections it can depend on values of \(\nabla\) that the axioms of a covariant derivative leave unconstrained.

def extendCurvature (cov : CovariantDerivative I F V) (x : M) (u v : TangentSpace I x) (σ : V x) :
    V x :=
  cov (fun y ↦ cov (extend F σ) y (extend E v y)) x u
    - cov (fun y ↦ cov (extend F σ) y (extend E u y)) x v
    - cov (extend F σ) x (mlieBracket I (extend E u) (extend E v) x)

Used by 4

Used byAntisymmetry of the curvature expression · Ricci contraction of the curvature expression · Euclidean space is Ricci-flat · Riemann curvature endomorphism

TheoremAntisymmetry of the curvature expression#✓fully proved

For every covariant derivative \(\nabla\) on a vector bundle \(V\) over a manifold \(M\), every \(x \in M\), all \(u, v \in T_x M\) and every \(\sigma \in V_x\), the curvature expression \(R\) of \(\nabla\) on extensions satisfies \(R(u, v)\sigma = -R(v, u)\sigma\).

theorem extendCurvature_antisymm (cov : CovariantDerivative I F V) (x : M)
    (u v : TangentSpace I x) (σ : V x) :
    cov.extendCurvature x u v σ = - cov.extendCurvature x v u σ

Uses 1 · Used by 1

Statement usesCurvature expression of a covariant derivative on extensions

Used byAntisymmetry of the Riemann curvature

DefinitionRicci contraction of the curvature expression#✓fully proved

Let \(M\) be a manifold modelled on a finite-dimensional normed space over a nontrivially normed field \(\mathbb{K}\), let \(\nabla\) be a covariant derivative on the tangent bundle of \(M\), let \(R\) be its curvature expression on extensions, let \(x \in M\) and let \(v, w \in T_x M\). With \(e_1, \dots, e_n\) the fixed basis of \(T_x M\) chosen for every finite-dimensional space and \(e_1^*, \dots, e_n^*\) its coordinate functionals, the Ricci contraction is

\[\operatorname{Ric}(v, w) = \sum_{i=1}^n e_i^*(R(e_i, v) w) \in \mathbb{K},\]

the trace of \(z \mapsto R(z, v) w\) computed in that basis (Lang, Lecture Notes on Riemannian Geometry, Def. 2.7). No metric is involved.

When \(z \mapsto R(z, v) w\) is linear, as it is for a connection that sends \(C^2\) sections to \(C^1\) sections, this is its trace and does not depend on the basis.

def extendRicci (cov : CovariantDerivative I E (TangentSpace I : M → Type _)) (x : M)
    (v w : TangentSpace I x) : 𝕜 :=
  ∑ i, (Module.finBasis 𝕜 (TangentSpace I x)).coord i
    (cov.extendCurvature x (Module.finBasis 𝕜 (TangentSpace I x) i) v w)

Uses 1 · Used by 1

Statement usesCurvature expression of a covariant derivative on extensions

Used byRicci curvature

DefinitionRiemann curvature endomorphism#✓fully proved

For a point \(x\) of a \(C^\infty\) Riemannian manifold \((M, g)\) with Levi-Civita connection \(\nabla\), and tangent vectors \(u, v, w \in T_x M\),

\[R(u, v) w = (\nabla_X \nabla_Y W - \nabla_Y \nabla_X W - \nabla_{[X, Y]} W)(x),\]

where \(X\), \(Y\), \(W\) are the vector fields extending \(u\), \(v\), \(w\) that have constant coordinates in the preferred chart at \(x\). Since the Levi-Civita connection of a \(C^\infty\) metric is \(C^\infty\), this is the textbook curvature endomorphism and does not depend on the extensions.

This is the sign convention of [Lang, Def. 2.1] and [Gud, Def. 8.8]; the opposite sign convention is also common.

def riemannCurvature (x : M) (u v w : TangentSpace I x) : TangentSpace I x :=
  (CovariantDerivative.leviCivitaConnection I M).extendCurvature x u v w

Uses 1 · Used by 6

Statement usesCurvature expression of a covariant derivative on extensions

Used byEuclidean space is Ricci-flat · Antisymmetry of the Riemann curvature · Euclidean space is flat · Sectional curvature · Sectional curvature vanishes on a vector and a multiple of it · Euclidean space has zero sectional curvature

TheoremAntisymmetry of the Riemann curvature#✓fully proved

Let \((M, g)\) be a \(C^\infty\) Riemannian manifold. Its Riemann curvature endomorphism \(R\) is antisymmetric in its first two arguments: \(R(u, v) w = -R(v, u) w\) for every point \(x \in M\) and all tangent vectors \(u, v, w \in T_x M\).

theorem riemannCurvature_antisymm (x : M) (u v w : TangentSpace I x) :
    riemannCurvature I x u v w = - riemannCurvature I x v u w

Uses 2

Statement usesRiemann curvature endomorphism

Proof usesAntisymmetry of the curvature expression

DefinitionSectional curvature#✓fully proved

Let \((M, g)\) be a \(C^\infty\) Riemannian manifold modeled on a finite-dimensional real space (boundary and corners allowed), with Riemann curvature endomorphism \(R\), and let \(x \in M\). The sectional curvature of tangent vectors \(u, v \in T_x M\) is

\[K(u, v) = \frac{\langle R(u, v) v, u \rangle}{\|u\|^2 \|v\|^2 - \langle u, v \rangle^2},\]

the sectional curvature of the plane spanned by \(u\) and \(v\) when they are linearly independent ([Lang, Def. 2.4], [Gud, Def. 8.14]). When \(u\) and \(v\) are linearly dependent the denominator vanishes and \(K(u, v)\) is \(0\) by definition.

With the sign convention used here for \(R\), the round unit sphere has \(K = 1\).

def sectionalCurvature (x : M) (u v : TangentSpace I x) : ℝ :=
  inner ℝ (riemannCurvature I x u v v) u / (‖u‖ ^ 2 * ‖v‖ ^ 2 - inner ℝ u v ^ 2)

Uses 1 · Used by 5

Statement usesRiemann curvature endomorphism

Used bySectional curvature bounded below · Sectional curvature bounded above · Sectional curvature vanishes on equal vectors · Sectional curvature vanishes on a vector and a multiple of it · Euclidean space has zero sectional curvature

TheoremSectional curvature vanishes on a vector and a multiple of it#✓fully proved

Let \((M, g)\) be a \(C^\infty\) Riemannian manifold modeled on a finite-dimensional real space (boundary and corners allowed), and let \(x \in M\), \(u \in T_x M\) and \(c \in \mathbb{R}\). Then the sectional curvature at \(x\) satisfies \(K(u, cu) = 0\): the denominator \(\|u\|^2 \|cu\|^2 - \langle u, cu \rangle^2\) of its defining formula vanishes, and the quotient is then \(0\) by definition.

theorem sectionalCurvature_smul_right (x : M) (u : TangentSpace I x) (c : ℝ) :
    sectionalCurvature I x u (c • u) = 0

Uses 2 · Used by 1

Statement usesSectional curvature

Proof usesRiemann curvature endomorphism

Used bySectional curvature vanishes on equal vectors

TheoremSectional curvature vanishes on equal vectors#✓fully proved

For every point \(x\) of a \(C^\infty\) Riemannian manifold \((M, g)\) and every tangent vector \(u \in T_x M\), the sectional curvature formula \(K\) gives \(K(u, u) = 0\): its denominator \(\|u\|^2 \|u\|^2 - \langle u, u \rangle^2\) vanishes, where \(\langle \cdot, \cdot \rangle\) and \(\|\cdot\|\) are the inner product and norm on \(T_x M\) given by \(g\), and a quotient by \(0\) is taken to be \(0\).

@[simp]
theorem sectionalCurvature_self (x : M) (u : TangentSpace I x) :
    sectionalCurvature I x u u = 0

Uses 2

Statement usesSectional curvature

Proof usesSectional curvature vanishes on a vector and a multiple of it

DefinitionRicci curvature#✓fully proved

For a point \(x\) of a \(C^\infty\) Riemannian manifold \((M, g)\) and tangent vectors \(v, w \in T_x M\), the Ricci curvature is \(\operatorname{Ric}_x(v, w) = \sum_i e_i^*(R(e_i, v) w)\), where \(R\) is the Riemann curvature endomorphism of the Levi-Civita connection of \(g\), \((e_i)\) is a fixed basis of \(T_x M\) and \((e_i^*)\) is its dual basis; the contraction itself uses no metric. Since \(z \mapsto R(z, v) w\) is linear, this is its trace and does not depend on the basis ([Lang, Def. 2.7]). The unit \(n\)-sphere has \(\operatorname{Ric} = (n - 1) g\).

def ricci (x : M) (v w : TangentSpace I x) : ℝ :=
  (CovariantDerivative.leviCivitaConnection I M).extendRicci x v w

Uses 1 · Used by 8

Statement usesRicci contraction of the curvature expression

Used byEinstein metric · Ricci curvature bounded below · Euclidean space is Ricci-flat · Scalar curvature · Euclidean space has zero scalar curvature · Gradient Ricci soliton · The Gaussian gradient Ricci soliton · Gaussian potentials that are gradient Ricci solitons

DefinitionScalar curvature#✓fully proved

The scalar curvature of a \(C^\infty\) Riemannian manifold \((M, g)\) at a point \(x\) is \(\sum_i \operatorname{Ric}_x(e_i, e_i)\), the metric trace of the Ricci curvature \(\operatorname{Ric}\), where \((e_i)\) is a fixed orthonormal basis of \(T_x M\) ([Gud, Def. 8.32]). The unit \(n\)-sphere has scalar curvature \(n (n - 1)\).

def scalarCurvature (x : M) : ℝ :=
  ∑ i, ricci I x (stdOrthonormalBasis ℝ (TangentSpace I x) i)
    (stdOrthonormalBasis ℝ (TangentSpace I x) i)

Uses 1 · Used by 3

Statement usesRicci curvature

Used byManifolds admitting a metric of positive scalar curvature · Scalar curvature bounded below · Euclidean space has zero scalar curvature

DefinitionSectional curvature bounded below#✓fully proved

A \(C^\infty\) Riemannian manifold \(M\) has sectional curvature at least \(k \in \mathbb{R}\) when \(K(u, v) \ge k\) for every point \(x \in M\) and all linearly independent tangent vectors \(u, v \in T_x M\), where \(K(u, v)\) is the sectional curvature of the plane spanned by \(u\) and \(v\).

def SectionalCurvatureGE (k : ℝ) : Prop :=
  ∀ (x : M) (u v : TangentSpace I x), LinearIndependent ℝ ![u, v] →
    k ≤ sectionalCurvature I x u v

Uses 1

Statement usesSectional curvature

DefinitionSectional curvature bounded above#✓fully proved

A \(C^\infty\) Riemannian manifold \(M\) has sectional curvature at most \(k \in \mathbb{R}\) when \(K(u, v) \le k\) for every point \(x \in M\) and all linearly independent tangent vectors \(u, v \in T_x M\), where \(K(u, v)\) is the sectional curvature of the plane spanned by \(u\) and \(v\).

def SectionalCurvatureLE (k : ℝ) : Prop :=
  ∀ (x : M) (u v : TangentSpace I x), LinearIndependent ℝ ![u, v] →
    sectionalCurvature I x u v ≤ k

Uses 1

Statement usesSectional curvature

DefinitionRicci curvature bounded below#✓fully proved

A \(C^\infty\) Riemannian manifold \((M, g)\) has Ricci curvature at least \(k \in \mathbb{R}\), written \(\operatorname{Ric} \ge k g\), when \(\operatorname{Ric}_x(v, v) \ge k \|v\|^2\) for every point \(x \in M\) and every tangent vector \(v \in T_x M\), where \(\operatorname{Ric}\) is the Ricci curvature and \(\|v\|\) is the norm of \(v\) given by \(g\).

def RicciGE (k : ℝ) : Prop :=
  ∀ (x : M) (v : TangentSpace I x), k * ‖v‖ ^ 2 ≤ ricci I x v v

Uses 1

Statement usesRicci curvature

DefinitionScalar curvature bounded below#✓fully proved

A \(C^\infty\) Riemannian manifold \(M\) has scalar curvature at least \(k \in \mathbb{R}\) when its scalar curvature at every point \(x \in M\) is at least \(k\).

def ScalarCurvatureGE (k : ℝ) : Prop :=
  ∀ x : M, k ≤ scalarCurvature I x

Uses 1

Statement usesScalar curvature

DefinitionEinstein metric#✓fully proved

A \(C^\infty\) Riemannian manifold \((M, g)\) is Einstein when there is a real constant \(\lambda\) such that \(\operatorname{Ric}_x(v, w) = \lambda \, g_x(v, w)\) for every point \(x \in M\) and all tangent vectors \(v, w \in T_x M\), where \(\operatorname{Ric}\) is the Ricci curvature ([Lang], Einstein manifolds). Ricci-flat is the case \(\lambda = 0\).

def IsEinstein : Prop :=
  ∃ c : ℝ, ∀ (x : M) (v w : TangentSpace I x), ricci I x v w = c * inner ℝ v w

Uses 1

Statement usesRicci curvature

TheoremExtending a tangent vector of a normed space gives a constant vector field#✓fully proved

Let \(F\) be a normed space over a nontrivially normed field, viewed as a manifold modelled on itself, so that each tangent space of \(F\) is \(F\). For every point \(x \in F\), tangent vector \(u \in T_xF\) and point \(y \in F\), the extension of \(u\) to a vector field on \(F\) (built from the trivialization of the tangent bundle at \(x\)) has value \(u\) at \(y\).

theorem FiberBundle.extend_model_space (x : F) (u : TangentSpace 𝓘(𝕜, F) x) (y : F) :
    extend F u y = u

Used by 6

Used byThe Levi-Civita connection of Euclidean space kills constant vector fields · Extensions of tangent vectors of a normed space are differentiable · Lie brackets of extended tangent vectors of a normed space vanish · Geodesic velocity curves in Euclidean space · The Levi-Civita connection of a vector space is the Fréchet derivative · The Hessian on Euclidean space as an iterated directional derivative

TheoremExtensions of tangent vectors of a normed space are differentiable#✓fully proved

Let \(F\) be a normed space over a nontrivially normed field, viewed as a manifold modelled on itself. For every point \(x \in F\), tangent vector \(u \in T_xF\) and point \(y \in F\), the extension of \(u\) to a vector field on \(F\) (built from the trivialization of the tangent bundle at \(x\)), viewed as a map from \(F\) to its tangent bundle, is differentiable at \(y\), not only at the base point \(x\).

theorem FiberBundle.mdifferentiableAt_extend_model_space {x : F} (u : TangentSpace 𝓘(𝕜, F) x)
    (y : F) : MDiffAt (T% (extend F u)) y

Uses 1 · Used by 3

Proof usesExtending a tangent vector of a normed space gives a constant vector field

Used byThe Levi-Civita connection of Euclidean space kills constant vector fields · Geodesic velocity curves in Euclidean space · The Levi-Civita connection of a vector space is the Fréchet derivative

TheoremLie brackets of extended tangent vectors of a normed space vanish#✓fully proved

Let \(F\) be a normed space over a nontrivially normed field, viewed as a manifold modelled on itself. For points \(x, x' \in F\) and tangent vectors \(a \in T_xF\) and \(b \in T_{x'}F\), let \(X\) and \(Y\) be the extensions of \(a\) and \(b\) to vector fields on \(F\) (built from the trivializations of the tangent bundle at \(x\) and at \(x'\)). Then the Lie bracket \([X, Y]\) vanishes at every point \(y \in F\).

theorem VectorField.mlieBracket_extend_model_space {x x' : F} (a : TangentSpace 𝓘(𝕜, F) x)
    (b : TangentSpace 𝓘(𝕜, F) x') (y : F) :
    mlieBracket 𝓘(𝕜, F) (extend F a) (extend F b) y = 0

Uses 1 · Used by 1

Proof usesExtending a tangent vector of a normed space gives a constant vector field

Used byThe Levi-Civita connection of Euclidean space kills constant vector fields

TheoremThe Levi-Civita connection of Euclidean space kills constant vector fields#✓fully proved

Let \(F\) be a finite-dimensional real inner product space with the Riemannian metric given by its inner product on every tangent space, and let \(\nabla\) be its Levi-Civita connection. For every point \(x \in F\) and tangent vector \(w \in T_xF\), let \(W\) be the extension of \(w\) to a vector field on \(F\) (built from the trivialization of the tangent bundle at \(x\); it is the constant vector field with value \(w\)). Then the covariant derivative \(\nabla W\) at every point \(y \in F\) is the zero map.

theorem CovariantDerivative.leviCivitaConnection_extend_vectorSpace {x : F}
    (w : TangentSpace 𝓘(ℝ, F) x) (y : F) :
    leviCivitaConnection 𝓘(ℝ, F) F (extend F w) y = 0

Uses 3 · Used by 4

Proof usesExtending a tangent vector of a normed space gives a constant vector field · Extensions of tangent vectors of a normed space are differentiable · Lie brackets of extended tangent vectors of a normed space vanish

Used byEuclidean space is flat · Geodesic velocity curves in Euclidean space · The Levi-Civita connection of a vector space is the Fréchet derivative · The Hessian on Euclidean space as an iterated directional derivative

TheoremEuclidean space is flat#✓fully proved

Let \(F\) be a finite-dimensional real inner product space with the Riemannian metric given by its inner product on every tangent space. For every point \(x \in F\) and all tangent vectors \(u, v, w \in T_xF\), the Riemann curvature endomorphism \(R\) of \(F\) at \(x\) satisfies \(R(u, v)w = 0\).

theorem riemannCurvature_vectorSpace (x : F) (u v w : TangentSpace 𝓘(ℝ, F) x) :
    riemannCurvature 𝓘(ℝ, F) x u v w = 0

Uses 2 · Used by 2

Statement usesRiemann curvature endomorphism

Proof usesThe Levi-Civita connection of Euclidean space kills constant vector fields

Used byEuclidean space is Ricci-flat · Euclidean space has zero sectional curvature

TheoremEuclidean space has zero sectional curvature#✓fully proved

Let \(F\) be a finite-dimensional real inner product space with the Riemannian metric given by its inner product on every tangent space. For every point \(x \in F\) and all tangent vectors \(u, v \in T_xF\), the sectional curvature \(K(u, v)\) of \(F\) at \(x\) is \(0\).

theorem sectionalCurvature_vectorSpace (x : F) (u v : TangentSpace 𝓘(ℝ, F) x) :
    sectionalCurvature 𝓘(ℝ, F) x u v = 0

Uses 3

Statement usesSectional curvature

Proof usesRiemann curvature endomorphism · Euclidean space is flat

TheoremEuclidean space is Ricci-flat#✓fully proved

Let \(F\) be a finite-dimensional real inner product space with the Riemannian metric given by its inner product on every tangent space. For every point \(x \in F\) and all tangent vectors \(v, w \in T_xF\), the Ricci curvature \(\mathrm{Ric}(v, w)\) of \(F\) at \(x\) is \(0\).

theorem ricci_vectorSpace (x : F) (v w : TangentSpace 𝓘(ℝ, F) x) :
    ricci 𝓘(ℝ, F) x v w = 0

Uses 4 · Used by 3

Statement usesRicci curvature

Proof usesCurvature expression of a covariant derivative on extensions · Riemann curvature endomorphism · Euclidean space is flat

Used byEuclidean space has zero scalar curvature · The Gaussian gradient Ricci soliton · Gaussian potentials that are gradient Ricci solitons

TheoremEuclidean space has zero scalar curvature#✓fully proved

Let \(F\) be a finite-dimensional real inner product space with the Riemannian metric given by its inner product on every tangent space. For every point \(x \in F\), the scalar curvature of \(F\) at \(x\) is \(0\).

theorem scalarCurvature_vectorSpace (x : F) : scalarCurvature 𝓘(ℝ, F) x = 0

Uses 3

Statement usesScalar curvature

Proof usesRicci curvature · Euclidean space is Ricci-flat

23 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.