Curvature under a conformal change of metric

Let g be a Riemannian metric on M and f a positive function, and let ĝ = f g be the conformally rescaled metric Bundle.ContMDiffRiemannianMetric.rescale. The Levi-Civita connections of the two metrics differ by the conformal connection tensor A(Y, X) = (2 f)⁻¹ (df(X) Y + df(Y) X - g(X, Y) grad_g f) (TauCeti.Manifold.conformalConnectionTensor), and this file computes the curvature of ĝ from that of g:

R^ĝ(X, Y) Z = R^g(X, Y) Z + (∇_X A)(Z, Y) - (∇_Y A)(Z, X) + A(A(Z, Y), X) - A(A(Z, X), Y),

where ∇ is the Levi-Civita connection of g and (∇_X A)(Z, Y) = ∇_X (A(Z, Y)) - A(∇_X Z, Y) - A(Z, ∇_X Y). Writing f = e^(2φ), the tensor is A(Y, X) = dφ(X) Y + dφ(Y) X - g(X, Y) grad_g φ, and this is the classical transformation law of the Riemann curvature under the conformal change e^(2φ) g.

The identity holds at a point x for a Cⁿ metric with 1 ≤ n, and with the Levi-Civita connection of g replaced by any connection that is Levi-Civita for g. The conformal factor f is assumed Cⁿ on all of M and the vector field Z differentiable on all of M; the remaining hypotheses are differentiability at x of X, Y, ∇_X Z, ∇_Y Z, A(Z, X) and A(Z, Y). For a smooth metric, a smooth conformal factor and smooth vector fields all the hypotheses hold. As for the conformal change of the Levi-Civita connection (Bundle.ContMDiffRiemannianMetric.leviCivitaConnection_rescale_apply), connections do not depend on a metric, so each metric is installed in turn as the RiemannianBundle instance of the tangent bundle of M and the connections are compared directly on M.

For a smooth metric and a smooth conformal factor f = e^(2φ), the difference of the two curvatures is a tensor built from the Hessian Hess φ, the differential dφ and the gradient grad φ, so it can be evaluated pointwise and contracted. The factor is given as a smooth positive function f together with a function φ satisfying f = e^(2φ); such a φ is automatically smooth. With n the dimension, Δ = div grad the Laplace–Beltrami operator of g and R(u, v) w = ∇_u ∇_v w - ∇_v ∇_u w - ∇_[u,v] w, the contractions are the classical formulas

Ric^ĝ = Ric^g - (n - 2) (Hess φ - dφ ⊗ dφ) + (-Δφ - (n - 2) |dφ|²) g,

Scal^ĝ = e^(-2φ) (Scal^g - 2 (n - 1) Δφ - (n - 1) (n - 2) |dφ|²).

The scalar formula is the input from which the conformal Laplacian of the Yamabe problem arises. In dimension two it becomes Scal^ĝ = e^(-2φ) (Scal^g - 2 Δφ), the curvature equation of conformal metrics on surfaces.

In dimension n ≥ 3 the Ricci and scalar formulas combine into the transformation law of the Schouten tensor P = (Ric - Scal g / (2 (n - 1))) / (n - 2),

P^ĝ = P^g - Hess φ + dφ ⊗ dφ - (|dφ|² / 2) g,

Since the fully covariant curvature tensor of ĝ is e^(2φ) (Rm^g - T ⊙ g), with ⊙ the Kulkarni–Nomizu product and T = Hess φ - dφ ⊗ dφ + (|dφ|² / 2) g the same correction, the Weyl tensor W = Rm - P ⊙ g satisfies W^ĝ = f W^g for ĝ = f g, away from dimension 2. Equivalently, the Weyl tensor of type (1, 3) is a conformal invariant; in particular its vanishing depends only on the conformal class. This is the conformal invariance used in the characterization of local conformal flatness by the Weyl tensor.

Differentiating the Schouten law gives the transformation law of the Cotton tensor C(X, Y, Z) = (∇_Z P)(X, Y) - (∇_Y P)(X, Z): for ĝ = e^(2φ) g, away from dimension 2,

C^ĝ(X, Y, Z) = C^g(X, Y, Z) + W^g(Y, Z, grad φ, X).

The third derivatives of φ cancel by the Ricci identity for the Hessian (TauCeti.Manifold.mvfderiv_hessian_sub_swap), the change of connection contributes the Kulkarni–Nomizu part of the curvature, and only the Weyl tensor survives. In dimension 3 the Weyl tensor vanishes, so the Cotton tensor is a conformal invariant there; this is the conformal invariance used in the three-dimensional characterization of local conformal flatness.

Main results

• Bundle.ContMDiffRiemannianMetric.curvatureOperator_leviCivitaConnection_rescale: the curvature of f g in terms of a Levi-Civita connection of g and the conformal connection tensor of f.
• Bundle.ContMDiffRiemannianMetric.curvatureOperator_leviCivitaConnection_rescale_of_contMDiff: the same identity for a smooth metric, a smooth conformal factor and smooth vector fields.
• Bundle.ContMDiffRiemannianMetric.curvatureTensor_leviCivitaConnection_rescale: the pointwise curvature tensor of e^(2φ) g in terms of that of g, Hess φ, dφ and grad φ.
• Bundle.ContMDiffRiemannianMetric.ricciTensor_leviCivitaConnection_rescale: the Ricci tensor of e^(2φ) g.
• Bundle.ContMDiffRiemannianMetric.scalarCurvature_rescale: the scalar curvature of e^(2φ) g.
• Bundle.ContMDiffRiemannianMetric.scalarCurvature_rescale_of_finrank_eq_two: on a surface, Scal^(e^(2φ) g) = e^(-2φ) (Scal^g - 2 Δφ).
• Bundle.ContMDiffRiemannianMetric.scalarCurvature_rescale_eq_iff_of_finrank_eq_two: on a surface, e^(2φ) g has scalar curvature c exactly when -Δφ + Scal^g / 2 = (c / 2) e^(2φ).
• Bundle.ContMDiffRiemannianMetric.schoutenTensor_leviCivitaConnection_rescale: the Schouten tensor of e^(2φ) g.
• Bundle.ContMDiffRiemannianMetric.weylTensor_leviCivitaConnection_rescale: the Weyl tensor of f g is f times that of g.
• Bundle.ContMDiffRiemannianMetric.weylTensor_leviCivitaConnection_rescale_eq_zero_iff: the Weyl tensor of f g vanishes at a point exactly when that of g does.
• Bundle.ContMDiffRiemannianMetric.cottonTensor_leviCivitaConnection_rescale: the Cotton tensor of e^(2φ) g is that of g plus the Weyl tensor of g contracted with grad φ.
• Bundle.ContMDiffRiemannianMetric.cottonTensor_leviCivitaConnection_rescale_of_finrank_eq_three: in dimension 3 the Cotton tensor of f g equals that of g.

References

• A. L. Besse, Einstein Manifolds, Springer (1987), Sections 1.G and 1.J.
• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 7 (curvature of conformally related metrics).
• J. M. Lee and T. H. Parker, The Yamabe problem, Bull. Amer. Math. Soc. 17 (1987), 37–91, Section 2.

theorem Bundle.ContMDiffRiemannianMetric.curvatureOperator_leviCivitaConnection_rescale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] {n : WithTop ℕ∞} (g : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (hn : 1 ≤ n) {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) n f) (hf_pos : ∀ (x : M), 0 < f x) {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} (hcov : CovariantDerivative.IsLeviCivitaConnection I cov) {X Y Z : (x : M) → TangentSpace I x} {x : M} (hX : (MDiffAt fun (x : M) => ⟨x, X x⟩) x) (hY : (MDiffAt fun (x : M) => ⟨x, Y x⟩) x) (hZ : MDiff fun (x : M) => ⟨x, Z x⟩) (hXZ : (MDiffAt fun (y : M) => ⟨y, (↑cov Z y) (X y)⟩) x) (hYZ : (MDiffAt fun (y : M) => ⟨y, (↑cov Z y) (Y y)⟩) x) (hAX : (MDiffAt fun (y : M) => ⟨y, ((TauCeti.Manifold.conformalConnectionTensor I f y) (Z y)) (X y)⟩) x) (hAY : (MDiffAt fun (y : M) => ⟨y, ((TauCeti.Manifold.conformalConnectionTensor I f y) (Z y)) (Y y)⟩) x) : (CovariantDerivative.leviCivitaConnection I M).curvatureOperator X Y Z x = cov.curvatureOperator X Y Z x + ((↑cov (fun (y : M) => ((TauCeti.Manifold.conformalConnectionTensor I f y) (Z y)) (Y y)) x) (X x) - ((TauCeti.Manifold.conformalConnectionTensor I f x) ((↑cov Z x) (X x))) (Y x) - ((TauCeti.Manifold.conformalConnectionTensor I f x) (Z x)) ((↑cov Y x) (X x))) - ((↑cov (fun (y : M) => ((TauCeti.Manifold.conformalConnectionTensor I f y) (Z y)) (X y)) x) (Y x) - ((TauCeti.Manifold.conformalConnectionTensor I f x) ((↑cov Z x) (Y x))) (X x) - ((TauCeti.Manifold.conformalConnectionTensor I f x) (Z x)) ((↑cov X x) (Y x))) + (((TauCeti.Manifold.conformalConnectionTensor I f x) (((TauCeti.Manifold.conformalConnectionTensor I f x) (Z x)) (Y x))) (X x) - ((TauCeti.Manifold.conformalConnectionTensor I f x) (((TauCeti.Manifold.conformalConnectionTensor I f x) (Z x)) (X x))) (Y x))

Curvature under conformal change. Let ∇ be a Levi-Civita connection of a C¹ metric g and A the conformal connection tensor of a positive function f. Then the curvature of the Levi-Civita connection of f g is

R^(f g)(X, Y) Z = R^∇(X, Y) Z + (∇_X A)(Z, Y) - (∇_Y A)(Z, X) + A(A(Z, Y), X) - A(A(Z, X), Y),

with (∇_X A)(Z, Y) = ∇_X (A(Z, Y)) - A(∇_X Z, Y) - A(Z, ∇_X Y). The metric g and the function f are assumed Cⁿ on all of M for some 1 ≤ n, and Z differentiable on all of M; the remaining hypotheses are differentiability at x of X, Y, ∇_X Z, ∇_Y Z, A(Z, X) and A(Z, Y).

theorem Bundle.ContMDiffRiemannianMetric.curvatureOperator_leviCivitaConnection_rescale_of_contMDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hf_pos : ∀ (x : M), 0 < f x) {X Y Z : (x : M) → TangentSpace I x} (hX : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, X x⟩) (hY : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Y x⟩) (hZ : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Z x⟩) (x : M) : (CovariantDerivative.leviCivitaConnection I M).curvatureOperator X Y Z x = (CovariantDerivative.leviCivitaConnection I M).curvatureOperator X Y Z x + ((↑(CovariantDerivative.leviCivitaConnection I M) (fun (y : M) => ((TauCeti.Manifold.conformalConnectionTensor I f y) (Z y)) (Y y)) x) (X x) - ((TauCeti.Manifold.conformalConnectionTensor I f x) ((↑(CovariantDerivative.leviCivitaConnection I M) Z x) (X x))) (Y x) - ((TauCeti.Manifold.conformalConnectionTensor I f x) (Z x)) ((↑(CovariantDerivative.leviCivitaConnection I M) Y x) (X x))) - ((↑(CovariantDerivative.leviCivitaConnection I M) (fun (y : M) => ((TauCeti.Manifold.conformalConnectionTensor I f y) (Z y)) (X y)) x) (Y x) - ((TauCeti.Manifold.conformalConnectionTensor I f x) ((↑(CovariantDerivative.leviCivitaConnection I M) Z x) (Y x))) (X x) - ((TauCeti.Manifold.conformalConnectionTensor I f x) (Z x)) ((↑(CovariantDerivative.leviCivitaConnection I M) X x) (Y x))) + (((TauCeti.Manifold.conformalConnectionTensor I f x) (((TauCeti.Manifold.conformalConnectionTensor I f x) (Z x)) (Y x))) (X x) - ((TauCeti.Manifold.conformalConnectionTensor I f x) (((TauCeti.Manifold.conformalConnectionTensor I f x) (Z x)) (X x))) (Y x))

Curvature under conformal change, for a smooth metric g, a smooth positive function f and smooth vector fields. With ∇ the Levi-Civita connection of g and A the conformal connection tensor of f, the curvature of the Levi-Civita connection of f g is

R^(f g)(X, Y) Z = R^g(X, Y) Z + (∇_X A)(Z, Y) - (∇_Y A)(Z, X) + A(A(Z, Y), X) - A(A(Z, X), Y),

with (∇_X A)(Z, Y) = ∇_X (A(Z, Y)) - A(∇_X Z, Y) - A(Z, ∇_X Y).

theorem Bundle.ContMDiffRiemannianMetric.curvatureTensor_leviCivitaConnection_rescale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hf_pos : ∀ (x : M), 0 < f x) {φ : M → ℝ} (hfφ : ∀ (x : M), f x = Real.exp (2 * φ x)) (x : M) (u v w : TangentSpace I x) : ((((CovariantDerivative.leviCivitaConnection I M).curvatureTensor x) u) v) w = ((((CovariantDerivative.leviCivitaConnection I M).curvatureTensor x) u) v) w + TauCeti.Manifold.hessian I φ x u w • v - TauCeti.Manifold.hessian I φ x v w • u + Inner.inner ℝ u w • (↑(CovariantDerivative.leviCivitaConnection I M) (TauCeti.Manifold.mgradient I φ) x) v - Inner.inner ℝ v w • (↑(CovariantDerivative.leviCivitaConnection I M) (TauCeti.Manifold.mgradient I φ) x) u + ((d% φ x) v * (d% φ x) w) • u - ((d% φ x) u * (d% φ x) w) • v + ((d% φ x) u * Inner.inner ℝ v w - (d% φ x) v * Inner.inner ℝ u w) • TauCeti.Manifold.mgradient I φ x - ‖TauCeti.Manifold.mgradient I φ x‖ ^ 2 • (Inner.inner ℝ v w • u - Inner.inner ℝ u w • v)

Curvature tensor under conformal change. Let g be a smooth metric and f = e^(2φ) a smooth positive function. With Hess φ, ∇ and grad φ taken for g, the curvature tensor of f g at x is

R^(f g)(u, v) w = R^g(u, v) w + Hess φ(u, w) v - Hess φ(v, w) u + g(u, w) ∇_v grad φ - g(v, w) ∇_u grad φ + dφ(v) dφ(w) u - dφ(u) dφ(w) v + (dφ(u) g(v, w) - dφ(v) g(u, w)) grad φ - |dφ|² (g(v, w) u - g(u, w) v).

theorem Bundle.ContMDiffRiemannianMetric.ricciTensor_leviCivitaConnection_rescale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hf_pos : ∀ (x : M), 0 < f x) {φ : M → ℝ} (hfφ : ∀ (x : M), f x = Real.exp (2 * φ x)) (x : M) (u v : TangentSpace I x) : (((CovariantDerivative.leviCivitaConnection I M).ricciTensor x) u) v = (((CovariantDerivative.leviCivitaConnection I M).ricciTensor x) u) v - (↑(Module.finrank ℝ E) - 2) * (TauCeti.Manifold.hessian I φ x u v - (d% φ x) u * (d% φ x) v) + (-TauCeti.Manifold.laplaceBeltrami I φ x - (↑(Module.finrank ℝ E) - 2) * ‖TauCeti.Manifold.mgradient I φ x‖ ^ 2) * Inner.inner ℝ u v

Ricci tensor under conformal change. Let g be a smooth metric on a manifold of dimension n and f = e^(2φ) a smooth positive function. Then Ric^(f g) = Ric^g - (n - 2) (Hess φ - dφ ⊗ dφ) + (-Δφ - (n - 2) |dφ|²) g, where Hess φ, Δφ = div grad φ and |dφ| are taken for g.

theorem Bundle.ContMDiffRiemannianMetric.scalarCurvature_rescale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hf_pos : ∀ (x : M), 0 < f x) {φ : M → ℝ} (hfφ : ∀ (x : M), f x = Real.exp (2 * φ x)) (x : M) : (g.rescale f hf hf_pos).scalarCurvature x = (f x)⁻¹ * (g.scalarCurvature x - 2 * (↑(Module.finrank ℝ E) - 1) * TauCeti.Manifold.laplaceBeltrami I φ x - (↑(Module.finrank ℝ E) - 1) * (↑(Module.finrank ℝ E) - 2) * ‖TauCeti.Manifold.mgradient I φ x‖ ^ 2)

Scalar curvature under conformal change. Let g be a smooth metric on a manifold of dimension n and f = e^(2φ) a smooth positive function. Then Scal^(f g) = f⁻¹ (Scal^g - 2 (n - 1) Δφ - (n - 1) (n - 2) |dφ|²), where Δφ = div grad φ and |dφ| are taken for g.

theorem Bundle.ContMDiffRiemannianMetric.scalarCurvature_rescale_of_finrank_eq_two {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (hE : Module.finrank ℝ E = 2) {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hf_pos : ∀ (x : M), 0 < f x) {φ : M → ℝ} (hfφ : ∀ (x : M), f x = Real.exp (2 * φ x)) (x : M) : (g.rescale f hf hf_pos).scalarCurvature x = (f x)⁻¹ * (g.scalarCurvature x - 2 * TauCeti.Manifold.laplaceBeltrami I φ x)

Scalar curvature under conformal change on a surface. Let g be a smooth metric on a surface and f = e^(2φ) a smooth positive function. Then Scal^(f g) = f⁻¹ (Scal^g - 2 Δφ), where Δφ = div grad φ is taken for g.

theorem Bundle.ContMDiffRiemannianMetric.scalarCurvature_rescale_eq_iff_of_finrank_eq_two {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (hE : Module.finrank ℝ E = 2) {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hf_pos : ∀ (x : M), 0 < f x) {φ : M → ℝ} (hfφ : ∀ (x : M), f x = Real.exp (2 * φ x)) (c : ℝ) (x : M) : (g.rescale f hf hf_pos).scalarCurvature x = c ↔ -TauCeti.Manifold.laplaceBeltrami I φ x + g.scalarCurvature x / 2 = c / 2 * Real.exp (2 * φ x)

The prescribed curvature equation on a surface. Let g be a smooth metric on a surface and f = e^(2φ) a smooth positive function. Then e^(2φ) g has scalar curvature c at x exactly when -Δφ + Scal^g / 2 = (c / 2) e^(2φ) there, where Δφ = div grad φ is taken for g. Since the scalar curvature of a surface is twice its Gaussian curvature, for c = -2 this is the equation Δ⁺φ + K + e^(2φ) = 0 for a metric of Gaussian curvature -1, where Δ⁺ = -div grad and K = Scal^g / 2.

theorem Bundle.ContMDiffRiemannianMetric.schoutenTensor_leviCivitaConnection_rescale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hf_pos : ∀ (x : M), 0 < f x) {φ : M → ℝ} (hfφ : ∀ (x : M), f x = Real.exp (2 * φ x)) (hn : 3 ≤ Module.finrank ℝ E) (x : M) (u v : TangentSpace I x) : (((CovariantDerivative.leviCivitaConnection I M).schoutenTensor x) u) v = (((CovariantDerivative.leviCivitaConnection I M).schoutenTensor x) u) v - TauCeti.Manifold.hessian I φ x u v + (d% φ x) u * (d% φ x) v - ‖TauCeti.Manifold.mgradient I φ x‖ ^ 2 / 2 * Inner.inner ℝ u v

Schouten tensor under conformal change. Let g be a smooth metric on a manifold of dimension n ≥ 3 and f = e^(2φ) a smooth positive function. Then the Schouten tensor of f g is P^(f g) = P^g - Hess φ + dφ ⊗ dφ - (|dφ|² / 2) g, where Hess φ and |dφ| are taken for g.

theorem Bundle.ContMDiffRiemannianMetric.weylTensor_leviCivitaConnection_rescale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hf_pos : ∀ (x : M), 0 < f x) (hn : Module.finrank ℝ E ≠ 2) (x : M) (u v w z : TangentSpace I x) : (((((CovariantDerivative.leviCivitaConnection I M).weylTensor x) u) v) w) z = f x * (((((CovariantDerivative.leviCivitaConnection I M).weylTensor x) u) v) w) z

Weyl tensor under conformal change. Away from dimension 2, the fully covariant Weyl tensor of a conformally rescaled smooth metric f g is f times that of g: W^(f g)(u, v, w, z) = f W^g(u, v, w, z). Equivalently, the Weyl tensor of type (1, 3) is conformally invariant.

theorem Bundle.ContMDiffRiemannianMetric.weylTensor_leviCivitaConnection_rescale_eq_zero_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hf_pos : ∀ (x : M), 0 < f x) (hn : Module.finrank ℝ E ≠ 2) (x : M) : (CovariantDerivative.leviCivitaConnection I M).weylTensor x = 0 ↔ (CovariantDerivative.leviCivitaConnection I M).weylTensor x = 0

Away from dimension 2, the Weyl tensor of a conformally rescaled smooth metric f g vanishes at a point exactly when that of g does.

theorem Bundle.ContMDiffRiemannianMetric.cottonTensor_leviCivitaConnection_rescale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hf_pos : ∀ (x : M), 0 < f x) {φ : M → ℝ} (hfφ : ∀ (x : M), f x = Real.exp (2 * φ x)) (hn : Module.finrank ℝ E ≠ 2) (x : M) (u v w : TangentSpace I x) : ((((CovariantDerivative.leviCivitaConnection I M).cottonTensor x) u) v) w = ((((CovariantDerivative.leviCivitaConnection I M).cottonTensor x) u) v) w + (((((CovariantDerivative.leviCivitaConnection I M).weylTensor x) v) w) (TauCeti.Manifold.mgradient I φ x)) u

Cotton tensor under conformal change. Let g be a smooth metric on a manifold of dimension n ≠ 2 and f = e^(2φ) a smooth positive function. Then the Cotton tensor of f g is C^(f g)(u, v, w) = C^g(u, v, w) + W^g(v, w, grad φ, u), where W^g is the Weyl tensor of g and grad φ is taken for g.

theorem Bundle.ContMDiffRiemannianMetric.cottonTensor_leviCivitaConnection_rescale_of_finrank_eq_three {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hf_pos : ∀ (x : M), 0 < f x) (hn : Module.finrank ℝ E = 3) (x : M) : (CovariantDerivative.leviCivitaConnection I M).cottonTensor x = (CovariantDerivative.leviCivitaConnection I M).cottonTensor x

The Cotton tensor is conformally invariant in dimension 3. On a manifold of dimension 3, where the Weyl tensor vanishes, the Cotton tensor of a conformally rescaled smooth metric f g equals that of g.