Spaces of Riemannian metrics

DefinitionCoordinate expression of a Riemannian metric#✓fully proved

Let \(g\) be a smooth Riemannian metric on the tangent bundle of a smooth manifold \(M\) modeled through a model with corners \(I : H \to E\), and let \(e\) be an open partial homeomorphism from \(M\) to \(H\). Write \(\psi\) for the inverse of the extended chart \(I \circ e\), \(T\) for the target of \(I \circ e\), and \(D\psi(x)\) for the derivative of \(\psi\) at \(x\) within \(T\). The coordinate expression of \(g\) in \(e\) is the field of continuous bilinear forms on \(E\) that assigns to each \(x \in E\) the pullback form \((v, w) \mapsto g_{\psi(x)}(D\psi(x)\,v, D\psi(x)\,w)\).

noncomputable def metricInCoordinates
    (g : ContMDiffRiemannianMetric I ∞ E (fun x : M ↦ TangentSpace I x))
    (e : OpenPartialHomeomorph M H) : E → E →L[ℝ] E →L[ℝ] ℝ :=
  fun x =>
    (show E →L[ℝ] E →L[ℝ] ℝ from g.inner ((e.extend I).symm x)).bilinearComp
      (show E →L[ℝ] E from
        mfderivWithin 𝓘(ℝ, E) I (e.extend I).symm (e.extend I).target x)
      (show E →L[ℝ] E from
        mfderivWithin 𝓘(ℝ, E) I (e.extend I).symm (e.extend I).target x)

Used by 8

Used bySmoothness of a metric in coordinates · The \(C^k\) topology on smooth Riemannian metrics · The \(C^k\) topologies on smooth metrics get finer as \(k\) grows · Pointwise formula for a metric in coordinates · Conformal scaling of a metric in coordinates · Constant rescalings converge in every \(C^k\) topology · Convergence in \(\mathcal{G}^k(M)\) · Convergence in the \(C^k\) topology on smooth metrics

TheoremPointwise formula for a metric in coordinates#✓fully proved

Let \(g\) be a smooth Riemannian metric on the tangent bundle of a smooth manifold \(M\) modeled through a model with corners \(I : H \to E\), and let \(e\) be an open partial homeomorphism from \(M\) to \(H\). Write \(g^e\) for the coordinate expression of \(g\) in \(e\), \(\psi\) for the inverse of the extended chart \(I \circ e\), \(T\) for the target of \(I \circ e\), and \(D\psi(x)\) for the derivative of \(\psi\) at \(x\) within \(T\). Then for all \(x, v, w \in E\) we have \(g^e(x)(v, w) = g_{\psi(x)}(D\psi(x)\,v, D\psi(x)\,w)\).

@[simp]
theorem metricInCoordinates_apply
    (g : ContMDiffRiemannianMetric I ∞ E (fun x : M ↦ TangentSpace I x))
    (e : OpenPartialHomeomorph M H) (x v w : E) :
    metricInCoordinates g e x v w =
      g.inner ((e.extend I).symm x)
        (mfderivWithin 𝓘(ℝ, E) I (e.extend I).symm (e.extend I).target x v)
        (mfderivWithin 𝓘(ℝ, E) I (e.extend I).symm (e.extend I).target x w)

Uses 1 · Used by 2

Statement usesCoordinate expression of a Riemannian metric

Used bySmoothness of a metric in coordinates · Conformal scaling of a metric in coordinates

TheoremConformal scaling of a metric in coordinates#✓fully proved

Let \(g\) be a smooth Riemannian metric on the tangent bundle of a smooth manifold \(M\) modeled through a model with corners \(I : H \to E\), let \(u : M \to \mathbb{R}\) be a smooth function with \(u(p) > 0\) for every \(p \in M\), and let \(e\) be an open partial homeomorphism from \(M\) to \(H\). Write \(g^e\) for the coordinate expression of \(g\) in \(e\) and \(\psi\) for the inverse of the extended chart \(I \circ e\). Then for every \(x \in E\) the coordinate expression of the conformally scaled metric \(u g\) satisfies \((u g)^e(x) = u(\psi(x))\, g^e(x)\).

theorem metricInCoordinates_conformalScale
    (g : ContMDiffRiemannianMetric I ∞ E (fun x : M ↦ TangentSpace I x))
    (u : M → ℝ) (hu : ContMDiff I 𝓘(ℝ) ∞ u) (hpos : ∀ x, 0 < u x)
    (e : OpenPartialHomeomorph M H) (x : E) :
    metricInCoordinates (g.conformalScale u hu hpos) e x =
      u ((e.extend I).symm x) • metricInCoordinates g e x

Uses 4 · Used by 1

Statement usesConformal scaling of a Riemannian metric · Coordinate expression of a Riemannian metric

Proof usesInner product of a conformally scaled metric · Pointwise formula for a metric in coordinates

Used byConstant rescalings converge in every \(C^k\) topology

TheoremSmoothness of a metric in coordinates#✓fully proved

Let \(E\) be a finite-dimensional real normed space, let \(M\) be a smooth manifold modeled through a model with corners \(I : H \to E\), and let \(g\) be a smooth Riemannian metric on the tangent bundle of \(M\). For every chart \(e\) in the maximal smooth atlas of \(M\), the coordinate expression of \(g\) in \(e\), viewed as a map from \(E\) to the continuous bilinear forms on \(E\), is \(C^\infty\) on the target of the extended chart \(I \circ e\).

theorem contDiffOn_metricInCoordinates [FiniteDimensional ℝ E]
    (g : ContMDiffRiemannianMetric I ∞ E (fun x : M ↦ TangentSpace I x))
    {e : OpenPartialHomeomorph M H} (he : e ∈ IsManifold.maximalAtlas I ∞ M) :
    ContDiffOn ℝ ∞ (metricInCoordinates g e) (e.extend I).target

Uses 2 · Used by 1

Statement usesCoordinate expression of a Riemannian metric

Proof usesPointwise formula for a metric in coordinates

Used byConstant rescalings converge in every \(C^k\) topology

DefinitionThe \(C^k\) topology on smooth Riemannian metrics#✓fully proved

Let \(M\) be a smooth manifold modelled on a real normed space \(E\) through a model with corners \(I\), and let \(k \in \mathbb{N} \cup \{\infty\}\). For a chart \(\varphi\) of the maximal smooth atlas of \(M\), write \(T_\varphi \subseteq E\) for the target of the extended chart \(I \circ \varphi\). The (weak, compact-open) \(C^k\) topology on the space of smooth Riemannian metrics on \(M\) is the coarsest topology for which, for every chart \(\varphi\) of the maximal atlas and every natural number \(i \le k\), the map sending a metric \(g\) to the \(i\)-th iterated derivative within \(T_\varphi\) of the coordinate expression of \(g\) in \(\varphi\) is continuous, where these derivatives carry the topology of uniform convergence on compact subsets of \(T_\varphi\).

For \(k = \infty\) this is the \(C^\infty\) topology. Every element of the space is a smooth metric, whatever \(k\) is; \(k\) only indexes the topology.

@[instance_reducible]
def metricCkTopology (I : ModelWithCorners ℝ E H) (M : Type*) [TopologicalSpace M]
    [ChartedSpace H M] [IsManifold I ∞ M] (k : ℕ∞) :
    TopologicalSpace (Bundle.ContMDiffRiemannianMetric I ∞ E
      (fun x : M ↦ TangentSpace I x)) :=
  ⨅ (e : ↥(IsManifold.maximalAtlas I ∞ M)) (i : ℕ) (_hh : (i : ℕ∞) ≤ k),
    TopologicalSpace.induced
      (fun g =>
        UniformOnFun.ofFun {K : Set E | IsCompact K ∧ K ⊆ (e.val.extend I).target}
          (iteratedFDerivWithin ℝ i (metricInCoordinates g e.val)
            (e.val.extend I).target))
      inferInstance

Sources

• Burns-Matveev v2 §8.4 finite-atlas ε-balls, v3 §8.3 weak C^k topology after Hirsch Ch. II. k = ⊤ is the C^∞ topology (smooth, not analytic). The space carries smooth metrics for every k, and no chart is chosen. Equality with the finite-atlas ε-ball topology on a closed manifold follows by the standard argument (relatively compact chart domains and chain rule).

Uses 1 · Used by 4

Statement usesCoordinate expression of a Riemannian metric

Used byThe \(C^k\) topologies on smooth metrics get finer as \(k\) grows · Constant rescalings converge in every \(C^k\) topology · Convergence in \(\mathcal{G}^k(M)\) · Convergence in the \(C^k\) topology on smooth metrics

DefinitionThe space \(\mathcal{G}^k(M)\) of smooth metrics with the \(C^k\) topology#✓fully proved

For a smooth manifold \(M\) and \(k \in \mathbb{N} \cup \{\infty\}\), \(\mathcal{G}^k(M)\) is the space of all smooth Riemannian metrics on \(M\), equipped with the \(C^k\) topology. It is not the space of \(C^k\) metrics: every element is smooth, and \(k\) only indexes the topology.

@[nolint unusedArguments]
def RiemannianMetricWithCk (I : ModelWithCorners ℝ E H) (M : Type*) [TopologicalSpace M]
    [ChartedSpace H M] [IsManifold I ∞ M] (k : ℕ∞) : Type _ :=
  Bundle.ContMDiffRiemannianMetric I ∞ E (fun x : M ↦ TangentSpace I x)

Used by 2

Used bySmooth metrics as elements of \(\mathcal{G}^k(M)\) · Convergence in \(\mathcal{G}^k(M)\)

DefinitionSmooth metrics as elements of \(\mathcal{G}^k(M)\)#✓fully proved

For a smooth manifold \(M\) and \(k \in \mathbb{N} \cup \{\infty\}\), the identity map is a bijection from the space of smooth Riemannian metrics on \(M\) to \(\mathcal{G}^k(M)\), the same space of metrics equipped with the \(C^k\) topology.

def RiemannianMetricWithCk.ofMetric {I : ModelWithCorners ℝ E H} {M : Type*}
    [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M] (k : ℕ∞) :
    Bundle.ContMDiffRiemannianMetric I ∞ E (fun x : M ↦ TangentSpace I x) ≃
      RiemannianMetricWithCk I M k :=
  Equiv.refl _

Uses 1 · Used by 1

Statement usesThe space \(\mathcal{G}^k(M)\) of smooth metrics with the \(C^k\) topology

Used byConvergence in \(\mathcal{G}^k(M)\)

TheoremConvergence in the \(C^k\) topology on smooth metrics#✓fully proved

Let \(M\) be a smooth manifold modelled on a real normed space \(E\) through a model with corners \(I\), let \(k \in \mathbb{N} \cup \{\infty\}\), let \(l\) be a filter on a type \(\alpha\), and let \(g_a\) (\(a \in \alpha\)) and \(g_0\) be smooth Riemannian metrics on \(M\). For a chart \(\varphi\) of the maximal smooth atlas of \(M\), write \(T_\varphi \subseteq E\) for the target of the extended chart \(I \circ \varphi\). Then \(g_a\) tends to \(g_0\) along \(l\) in the \(C^k\) topology if and only if, for every chart \(\varphi\) of the maximal atlas, every natural number \(i \le k\) and every compact set \(K \subseteq T_\varphi\), the \(i\)-th iterated derivatives within \(T_\varphi\) of the coordinate expressions of \(g_a\) in \(\varphi\) converge uniformly on \(K\) along \(l\) to the \(i\)-th iterated derivative within \(T_\varphi\) of the coordinate expression of \(g_0\) in \(\varphi\).

theorem tendsto_metricCkTopology_iff {I : ModelWithCorners ℝ E H} {M : Type*}
    [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M] {k : ℕ∞}
    {α : Type*} {l : Filter α}
    {g : α → Bundle.ContMDiffRiemannianMetric I ∞ E (fun x : M ↦ TangentSpace I x)}
    {g₀ : Bundle.ContMDiffRiemannianMetric I ∞ E (fun x : M ↦ TangentSpace I x)} :
    Tendsto g l (@nhds _ (metricCkTopology I M k) g₀) ↔
      ∀ e ∈ IsManifold.maximalAtlas I ∞ M, ∀ i : ℕ, (i : ℕ∞) ≤ k →
        ∀ K : Set E, IsCompact K → K ⊆ (e.extend I).target →
          TendstoUniformlyOn
            (fun a => iteratedFDerivWithin ℝ i (metricInCoordinates (g a) e)
              (e.extend I).target)
            (iteratedFDerivWithin ℝ i (metricInCoordinates g₀ e) (e.extend I).target)
            l K

Sources

• Burns-Matveev v3 §8.3.

Uses 2 · Used by 2

Statement usesThe \(C^k\) topology on smooth Riemannian metrics · Coordinate expression of a Riemannian metric

Used byConstant rescalings converge in every \(C^k\) topology · Convergence in \(\mathcal{G}^k(M)\)

TheoremConvergence in \(\mathcal{G}^k(M)\)#✓fully proved

Let \(M\) be a smooth manifold modelled on a real normed space \(E\) through a model with corners \(I\), let \(k \in \mathbb{N} \cup \{\infty\}\), let \(l\) be a filter on a type \(\alpha\), and let \(g_a\) (\(a \in \alpha\)) and \(g_0\) be smooth Riemannian metrics on \(M\). For a chart \(\varphi\) of the maximal smooth atlas of \(M\), write \(T_\varphi \subseteq E\) for the target of the extended chart \(I \circ \varphi\). Then \(g_a\), regarded as elements of the space \(\mathcal{G}^k(M)\) of smooth metrics with the \(C^k\) topology, tend to \(g_0\) along \(l\) if and only if, for every chart \(\varphi\) of the maximal atlas, every natural number \(i \le k\) and every compact set \(K \subseteq T_\varphi\), the \(i\)-th iterated derivatives within \(T_\varphi\) of the coordinate expressions of \(g_a\) in \(\varphi\) converge uniformly on \(K\) along \(l\) to the \(i\)-th iterated derivative within \(T_\varphi\) of the coordinate expression of \(g_0\) in \(\varphi\).

theorem RiemannianMetricWithCk.tendsto_iff {I : ModelWithCorners ℝ E H} {M : Type*}
    [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M] {k : ℕ∞}
    {α : Type*} {l : Filter α}
    {g : α → Bundle.ContMDiffRiemannianMetric I ∞ E (fun x : M ↦ TangentSpace I x)}
    {g₀ : Bundle.ContMDiffRiemannianMetric I ∞ E (fun x : M ↦ TangentSpace I x)} :
    Tendsto (fun a => RiemannianMetricWithCk.ofMetric k (g a)) l
        (𝓝 (RiemannianMetricWithCk.ofMetric k g₀)) ↔
      ∀ e ∈ IsManifold.maximalAtlas I ∞ M, ∀ i : ℕ, (i : ℕ∞) ≤ k →
        ∀ K : Set E, IsCompact K → K ⊆ (e.extend I).target →
          TendstoUniformlyOn
            (fun a => iteratedFDerivWithin ℝ i (metricInCoordinates (g a) e)
              (e.extend I).target)
            (iteratedFDerivWithin ℝ i (metricInCoordinates g₀ e) (e.extend I).target)
            l K

Uses 5

Statement usesThe space \(\mathcal{G}^k(M)\) of smooth metrics with the \(C^k\) topology · Smooth metrics as elements of \(\mathcal{G}^k(M)\) · The \(C^k\) topology on smooth Riemannian metrics · Coordinate expression of a Riemannian metric

Proof usesConvergence in the \(C^k\) topology on smooth metrics

TheoremThe \(C^k\) topologies on smooth metrics get finer as \(k\) grows#✓fully proved

Let \(M\) be a smooth manifold and let \(k \le k'\) be elements of \(\mathbb{N} \cup \{\infty\}\). On the space of smooth Riemannian metrics on \(M\), the \(C^{k'}\) topology is finer than the \(C^k\) topology.

theorem metricCkTopology_anti {I : ModelWithCorners ℝ E H} {M : Type*}
    [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M] {k k' : ℕ∞}
    (h : k ≤ k') :
    metricCkTopology I M k' ≤ metricCkTopology I M k

Uses 2

Statement usesThe \(C^k\) topology on smooth Riemannian metrics

Proof usesCoordinate expression of a Riemannian metric

TheoremConstant rescalings converge in every \(C^k\) topology#✓fully proved

Let \(M\) be a smooth manifold modelled on a finite-dimensional real normed space, let \(g\) be a smooth Riemannian metric on \(M\), and let \(k \in \mathbb{N} \cup \{\infty\}\). Let \(l\) be a filter on a type \(\alpha\) and let \(c_a > 0\) (\(a \in \alpha\)) be positive reals with \(c_a \to 1\) along \(l\). Then the rescaled metrics \(c_a g\) tend to \(g\) along \(l\) in the \(C^k\) topology.

In every chart the coordinate expression of \(c_a g\) is \(c_a\) times that of \(g\), hence so is each iterated derivative within the chart target, while those derivatives of \(g\) are bounded on each compact subset of the target.

theorem tendsto_conformalScale_const_metricCkTopology {I : ModelWithCorners ℝ E H}
    {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
    [FiniteDimensional ℝ E]
    (g : Bundle.ContMDiffRiemannianMetric I ∞ E (fun x : M ↦ TangentSpace I x))
    {α : Type*} {l : Filter α} (c : α → ℝ) (hc : ∀ a, 0 < c a)
    (hlim : Tendsto c l (𝓝 1)) (k : ℕ∞) :
    Tendsto
      (fun a => g.conformalScale (fun _ => c a) contMDiff_const (fun _ => hc a)) l
      (@nhds _ (metricCkTopology I M k) g)

Uses 6

Statement usesConformal scaling of a Riemannian metric · The \(C^k\) topology on smooth Riemannian metrics

Proof usesSmoothness of a metric in coordinates · Coordinate expression of a Riemannian metric · Conformal scaling of a metric in coordinates · Convergence in the \(C^k\) topology on smooth metrics

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.