Ricci solitons

StructureGradient Ricci soliton#✓fully proved

Let \(M\) be a smooth manifold (possibly with boundary or corners) modelled on a finite-dimensional real normed space, with a smooth Riemannian metric \(g\). A function \(f : M \to \mathbb{R}\) and a constant \(c \in \mathbb{R}\) form a gradient Ricci soliton if \(f\) is smooth and, for every point \(x \in M\) and all tangent vectors \(u, v \in T_x M\), \(\operatorname{Ric}_x(u, v) + (\operatorname{Hess} f)_x(u, v) = c \, g_x(u, v)\), where \(\operatorname{Ric}\) is the Ricci curvature of \(g\) and \(\operatorname{Hess} f\) is the covariant Hessian of \(f\).

Completeness and connectedness of \(M\) are not part of this predicate; they are separate hypotheses on \(M\).

structure IsGradientRicciSoliton (f : M → ℝ) (c : ℝ) : Prop where
  /-- The potential is smooth. -/
  contMDiff : ContMDiff I 𝓘(ℝ, ℝ) ∞ f
  /-- The soliton equation `Ric + Hess f = c • g`. -/
  ricci_add_hessian : ∀ (x : M) (u v : TangentSpace I x),
    ricci I x u v + hessian I f x u v = c * inner ℝ u v

Sources

• Oberwolfach Report 27/2012 (Geometrie): T. Yokota, p. 1651, defines a gradient shrinking Ricci soliton by Ric(g) + Hess f = g / (2 * λ) with λ > 0 and f smooth, and R. Haslhofer (with R. Müller), p. 1669, eq. (1), uses Rc + Hess f equal to g / 2.

Uses 2 · Used by 5

Statement usesCovariant Hessian · Ricci curvature

Used byThe Gaussian gradient Ricci soliton · Gaussian potentials that are gradient Ricci solitons · Gradient shrinking Ricci soliton · The Gaussian shrinking soliton · Gaussian potentials that are gradient shrinking Ricci solitons

StructureGradient shrinking Ricci soliton#✓fully proved

On a Riemannian manifold \((M, g)\), a function \(f : M \to \mathbb{R}\) and a constant \(c \in \mathbb{R}\) form a gradient shrinking Ricci soliton if they form a gradient Ricci soliton and \(c > 0\).

Completeness and connectedness of \(M\) are not part of this predicate.

structure IsGradientShrinkingRicciSoliton (f : M → ℝ) (c : ℝ) : Prop
    extends IsGradientRicciSoliton I f c where
  /-- The constant is positive (shrinking). -/
  pos : 0 < c

Sources

• Oberwolfach Report 27/2012 (Geometrie). In Yokota's notation (p. 1651) this is c = 1 / (2 * λ) with λ > 0; Haslhofer's normalization (p. 1669, eq. (1)) is c = 1 / 2.

Uses 1 · Used by 2

Statement usesGradient Ricci soliton

Used byThe Gaussian shrinking soliton · Gaussian potentials that are gradient shrinking Ricci solitons

TheoremThe Gaussian gradient Ricci soliton#✓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 \in \mathbb{R}\). The function \(f(x) = \frac{a}{2} \|x\|^2\) on \(F\) is a gradient Ricci soliton with constant \(a\).

For \(a < 0\) this is the expanding Gaussian soliton.

theorem isGradientRicciSoliton_gaussian {F : Type*} [NormedAddCommGroup F]
    [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (a : ℝ) :
    IsGradientRicciSoliton 𝓘(ℝ, F) (fun x : F => (a / 2) * ‖x‖ ^ 2) a

Uses 6 · Used by 2

Statement usesGradient Ricci soliton

Proof usesCovariant Hessian · The Hessian on Euclidean space is the second derivative · Ricci curvature · Euclidean space is Ricci-flat · Second derivative of the squared norm

Used byGaussian potentials that are gradient Ricci solitons · The Gaussian shrinking soliton

TheoremThe Gaussian shrinking soliton#✓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 > 0\). The function \(f(x) = \frac{a}{2} \|x\|^2\) on \(F\) is a gradient shrinking Ricci soliton with constant \(a\).

theorem isGradientShrinkingRicciSoliton_gaussian {F : Type*} [NormedAddCommGroup F]
    [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (a : ℝ) (ha : 0 < a) :
    IsGradientShrinkingRicciSoliton 𝓘(ℝ, F)
      (fun x : F => (a / 2) * ‖x‖ ^ 2) a

Sources

• Oberwolfach Report 27/2012 (Geometrie), T. Yokota, p. 1652; for a = 1 / 2 this is the Gaussian shrinker (ℝⁿ, g_E, ‖x‖ ^ 2 / 4).

Uses 3 · Used by 1

Statement usesGradient shrinking Ricci soliton

Proof usesGradient Ricci soliton · The Gaussian gradient Ricci soliton

Used byGaussian potentials that are gradient shrinking Ricci solitons

TheoremGaussian potentials that are gradient Ricci solitons#✓fully proved

Let \(F\) be a real inner product space of positive finite dimension, viewed as a Riemannian manifold with the metric given by its inner product, and let \(a, c \in \mathbb{R}\). The function \(f(x) = \frac{a}{2} \|x\|^2\) on \(F\) is a gradient Ricci soliton with constant \(c\) if and only if \(a = c\).

theorem isGradientRicciSoliton_gaussian_iff {F : Type*} [NormedAddCommGroup F]
    [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] [Nontrivial F] (a c : ℝ) :
    IsGradientRicciSoliton 𝓘(ℝ, F) (fun x : F => (a / 2) * ‖x‖ ^ 2) c ↔
      a = c

Uses 7 · Used by 1

Statement usesGradient Ricci soliton

Proof usesCovariant Hessian · The Hessian on Euclidean space is the second derivative · The Gaussian gradient Ricci soliton · Ricci curvature · Euclidean space is Ricci-flat · Second derivative of the squared norm

Used byGaussian potentials that are gradient shrinking Ricci solitons

TheoremGaussian potentials that are gradient shrinking Ricci solitons#✓fully proved

Let \(F\) be a real inner product space of positive finite dimension, viewed as a Riemannian manifold with the metric given by its inner product, and let \(a, c \in \mathbb{R}\). The function \(f(x) = \frac{a}{2} \|x\|^2\) on \(F\) is a gradient shrinking Ricci soliton with constant \(c\) if and only if \(a = c\) and \(c > 0\).

theorem isGradientShrinkingRicciSoliton_gaussian_iff {F : Type*}
    [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F]
    [Nontrivial F] (a c : ℝ) :
    IsGradientShrinkingRicciSoliton 𝓘(ℝ, F)
      (fun x : F => (a / 2) * ‖x‖ ^ 2) c ↔ (a = c ∧ 0 < c)

Uses 4

Statement usesGradient shrinking Ricci soliton

Proof usesGradient Ricci soliton · Gaussian potentials that are gradient Ricci solitons · The Gaussian shrinking soliton

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.