Locally conformally flat metrics

A smooth Riemannian metric g on M is locally conformally flat if every point has a neighbourhood on which some conformal rescaling f g, by a smooth positive function f, is flat. This file defines the notion and proves its first properties: it depends only on the conformal class of g, flat metrics are locally conformally flat, and away from dimension 2 both the Weyl tensor and the Cotton tensor of a locally conformally flat metric vanish identically.

The last statements are one half of the Weyl–Schouten theorem; the converse (vanishing of the Weyl tensor in dimension at least 4, or of the Cotton tensor in dimension 3, implies local conformal flatness) is a Frobenius integrability argument and is not proved here: this file only reduces it to local solvability of the conformal flattening equation (see below). The proof of the forward direction combines two facts: the Weyl tensor of a flat metric vanishes, and the Weyl tensor of f g is f times that of g, so its vanishing at a point is a conformal invariant. For the Cotton tensor, the Cotton tensor of f g vanishes at a point near which f g is flat, and it differs from that of g by a contraction of the Weyl tensor of g, which has just been shown to vanish.

This file reduces the converse to local solvability of a PDE. In dimension at least 3, the metric e^(2φ) g is flat exactly where the Weyl tensor of g vanishes and φ solves the conformal flattening equation Hess φ = P + dφ ⊗ dφ - (|dφ|² / 2) g, since the curvature tensor vanishes exactly when both the Weyl and the Schouten tensor do, the Weyl tensor transforms by a positive factor, and the Schouten tensor of e^(2φ) g vanishes exactly where the equation holds. Hence g is locally conformally flat exactly when its Weyl tensor vanishes and the equation has a smooth solution near every point. In dimension 3 the Weyl condition is automatic (CovariantDerivative.IsMetricCompatible.weylTensor_eq_zero_of_finrank_eq_three).

The conformal factor in the definition is a smooth positive function on all of M, while flatness of f g is only required near the point. Classically the factor is only defined near the point; the two formulations agree because curvature at a point only depends on the metric near that point, and a local positive factor can be extended to a global one by a smooth cutoff without changing it near the point. Requiring a global factor lets the definition use Bundle.ContMDiffRiemannianMetric.rescale directly instead of metrics on open subsets. As for Bundle.ContMDiffRiemannianMetric.weylTensor_leviCivitaConnection_rescale, the metric f g is installed as the RiemannianBundle instance of the tangent bundle of M when its curvature is evaluated.

Dimension 2 is excluded from the Weyl statement because there the Schouten tensor carries the factor 1 / (n - 2), which is 0 by the convention for division by zero, so the Weyl tensor is the full curvature tensor.

Main declarations

• Bundle.ContMDiffRiemannianMetric.IsLocallyConformallyFlat: local conformal flatness of a smooth Riemannian metric on the tangent bundle.
• Bundle.ContMDiffRiemannianMetric.isLocallyConformallyFlat_rescale_iff: local conformal flatness of f g is equivalent to that of g.
• Bundle.ContMDiffRiemannianMetric.IsLocallyConformallyFlat.of_mem_conformalClass: local conformal flatness depends only on the conformal class.
• Bundle.ContMDiffRiemannianMetric.isLocallyConformallyFlat_of_curvatureTensor_eq_zero: flat metrics are locally conformally flat.
• TauCeti.Manifold.isLocallyConformallyFlat_rescale_model_space: every metric conformal to the Euclidean metric is locally conformally flat.
• Bundle.ContMDiffRiemannianMetric.IsLocallyConformallyFlat.weylTensor_eq_zero: away from dimension 2, a locally conformally flat metric has vanishing Weyl tensor.
• Bundle.ContMDiffRiemannianMetric.IsLocallyConformallyFlat.cottonTensor_eq_zero: away from dimension 2, a locally conformally flat metric has vanishing Cotton tensor.
• Bundle.ContMDiffRiemannianMetric.curvatureTensor_leviCivitaConnection_rescale_eq_zero_iff: e^(2φ) g is flat at x exactly when W = 0 and the conformal flattening equation holds at x.
• isLocallyConformallyFlat_iff_forall_weylTensor_eq_zero_and_forall_exists_eventually_hessian_eq (in Bundle.ContMDiffRiemannianMetric): in dimension at least 3, local conformal flatness is equivalent to W = 0 together with local solvability of the conformal flattening equation.

References

• A. L. Besse, Einstein Manifolds, Springer (1987), Section 1.G.
• J. M. Lee and T. H. Parker, The Yamabe problem, Bull. Amer. Math. Soc. 17 (1987), 37–91, Section 2.

def Bundle.ContMDiffRiemannianMetric.IsLocallyConformallyFlat {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) : Prop

A smooth Riemannian metric g is locally conformally flat if every point x has a neighbourhood on which a conformal rescaling f g, by a smooth positive function f, is flat: the curvature tensor of the Levi-Civita connection of f g vanishes at every point near x.

theorem Bundle.ContMDiffRiemannianMetric.isLocallyConformallyFlat_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) : g.IsLocallyConformallyFlat ↔ ∀ (x : M), ∃ (f : M → ℝ) (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hf_pos : ∀ (y : M), 0 < f y), ∀ᶠ (y : M) in nhds x, (CovariantDerivative.leviCivitaConnection I M).curvatureTensor y = 0

Unfolding lemma for Bundle.ContMDiffRiemannianMetric.IsLocallyConformallyFlat.

theorem Bundle.ContMDiffRiemannianMetric.isLocallyConformallyFlat_of_curvatureTensor_eq_zero {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) (h : ∀ (x : M), (CovariantDerivative.leviCivitaConnection I M).curvatureTensor x = 0) : g.IsLocallyConformallyFlat

A flat metric is locally conformally flat, with the constant conformal factor 1.

theorem Bundle.ContMDiffRiemannianMetric.IsLocallyConformallyFlat.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} (hg : g.IsLocallyConformallyFlat) {h : M → ℝ} (hh : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) h) (hh_pos : ∀ (x : M), 0 < h x) : (g.rescale h hh hh_pos).IsLocallyConformallyFlat

If g is locally conformally flat, then so is every conformal rescaling h g of g: a conformal factor f flattening g near a point gives the factor f / h flattening h g.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.isLocallyConformallyFlat_rescale_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) {h : M → ℝ} (hh : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) h) (hh_pos : ∀ (x : M), 0 < h x) : (g.rescale h hh hh_pos).IsLocallyConformallyFlat ↔ g.IsLocallyConformallyFlat

A conformal rescaling h g of a metric g is locally conformally flat exactly when g is.

theorem Bundle.ContMDiffRiemannianMetric.IsLocallyConformallyFlat.of_mem_conformalClass {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 g' : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} (hg : g.IsLocallyConformallyFlat) (hg' : g' ∈ g.conformalClass) : g'.IsLocallyConformallyFlat

Local conformal flatness depends only on the conformal class: every metric conformal to a locally conformally flat metric is locally conformally flat.

theorem Bundle.ContMDiffRiemannianMetric.IsLocallyConformallyFlat.weylTensor_eq_zero {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} (hg : g.IsLocallyConformallyFlat) (hn : Module.finrank ℝ E ≠ 2) (x : M) : (CovariantDerivative.leviCivitaConnection I M).weylTensor x = 0

Local conformal flatness forces the Weyl tensor to vanish. Away from dimension 2, the Weyl tensor of a locally conformally flat metric vanishes at every point. This is the easy half of the Weyl–Schouten theorem.

theorem Bundle.ContMDiffRiemannianMetric.IsLocallyConformallyFlat.cottonTensor_eq_zero {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} (hg : g.IsLocallyConformallyFlat) (hn : Module.finrank ℝ E ≠ 2) (x : M) : (CovariantDerivative.leviCivitaConnection I M).cottonTensor x = 0

Local conformal flatness forces the Cotton tensor to vanish. Away from dimension 2, the Cotton tensor of a locally conformally flat metric vanishes at every point. In dimension 3 this is the easy half of the characterization of local conformal flatness by the Cotton tensor.

theorem Bundle.ContMDiffRiemannianMetric.curvatureTensor_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) {φ : M → ℝ} (hfφ : ∀ (x : M), f x = Real.exp (2 * φ x)) (hn : 3 ≤ Module.finrank ℝ E) (x : M) : (CovariantDerivative.leviCivitaConnection I M).curvatureTensor x = 0 ↔ (CovariantDerivative.leviCivitaConnection I M).weylTensor x = 0 ∧ ∀ (u v : TangentSpace I x), TauCeti.Manifold.hessian I φ x u v = (((CovariantDerivative.leviCivitaConnection I M).conformalFlatteningForm x (TauCeti.Manifold.mgradient I φ x)) u) v

When e^(2φ) g is flat. In dimension at least 3, the metric f g with f = e^(2φ) has vanishing curvature tensor at x exactly when the Weyl tensor of g vanishes at x and φ solves the conformal flattening equation Hess φ = P + dφ ⊗ dφ - (|dφ|² / 2) g at x, where the Hessian, the gradient and the Schouten tensor P are those of g.

theorem Bundle.ContMDiffRiemannianMetric.isLocallyConformallyFlat_iff_forall_weylTensor_eq_zero_and_forall_exists_eventually_hessian_eq {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) (hn : 3 ≤ Module.finrank ℝ E) : g.IsLocallyConformallyFlat ↔ (∀ (x : M), (CovariantDerivative.leviCivitaConnection I M).weylTensor x = 0) ∧ ∀ (x : M), ∃ (φ : M → ℝ), ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) φ ∧ ∀ᶠ (y : M) in nhds x, ∀ (u v : TangentSpace I y), TauCeti.Manifold.hessian I φ y u v = (((CovariantDerivative.leviCivitaConnection I M).conformalFlatteningForm y (TauCeti.Manifold.mgradient I φ y)) u) v

Local conformal flatness and the conformal flattening equation. In dimension at least 3, a smooth metric g is locally conformally flat exactly when its Weyl tensor vanishes and every point has a neighbourhood on which a smooth function φ solves the conformal flattening equation Hess φ = P + dφ ⊗ dφ - (|dφ|² / 2) g. A solution φ near x gives the conformal factor e^(2φ) flattening g near x, and conversely φ = (log f) / 2 for a flattening factor f.

theorem TauCeti.Manifold.isLocallyConformallyFlat_rescale_model_space {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {f : F → ℝ} (hf : ContMDiff (modelWithCornersSelf ℝ F) (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hf_pos : ∀ (x : F), 0 < f x) : (((riemannianMetricVectorSpace F).ofLE ⋯).rescale f hf hf_pos).IsLocallyConformallyFlat

Conformally Euclidean metrics are locally conformally flat. On a finite-dimensional real inner-product space F, every conformal rescaling f g of the Euclidean metric g by a smooth positive function f is locally conformally flat.