Gluing Riemannian metrics along an open cover

Let U and V be open subsets covering the base of a vector bundle, and let g₁ and g₂ be C^n Riemannian metrics on the bundle which agree over U ∩ V. Then there is a C^n Riemannian metric equal to g₁ over U and to g₂ over V. Positivity and boundedness of the unit ball are fibrewise conditions, and smoothness is local: near a point of U the glued metric is g₁, and near a point of V it is g₂.

This is how metrics built separately on overlapping regions, for instance on the two ends of a cylinder that agree with a common product metric on the overlap, are assembled into one metric.

Main definitions and results

• Bundle.ContMDiffRiemannianMetric.piecewise: the metric equal to g₁ over U and to g₂ over V.
• Bundle.ContMDiffRiemannianMetric.piecewise_inner_of_mem_left and Bundle.ContMDiffRiemannianMetric.piecewise_inner_of_mem_right: its inner products over U and over V.

noncomputable def Bundle.ContMDiffRiemannianMetric.piecewise {EB : Type u_1} [NormedAddCommGroup EB] [NormedSpace ℝ EB] {HB : Type u_2} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_5} [TopologicalSpace (TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [(b : B) → AddCommGroup (E b)] [(b : B) → Module ℝ (E b)] [FiberBundle F E] [VectorBundle ℝ F E] {U V : Set B} (g₁ g₂ : ContMDiffRiemannianMetric IB n F E) (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) (h : ∀ b ∈ U ∩ V, g₁.inner b = g₂.inner b) : ContMDiffRiemannianMetric IB n F E

Glue two C^n Riemannian metrics g₁ and g₂ which agree over the overlap of two open sets U and V covering the base: the result is g₁ over U and g₂ over V.

theorem Bundle.ContMDiffRiemannianMetric.piecewise_inner_of_mem_left {EB : Type u_1} [NormedAddCommGroup EB] [NormedSpace ℝ EB] {HB : Type u_2} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_5} [TopologicalSpace (TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [(b : B) → AddCommGroup (E b)] [(b : B) → Module ℝ (E b)] [FiberBundle F E] [VectorBundle ℝ F E] {U V : Set B} {g₁ g₂ : ContMDiffRiemannianMetric IB n F E} {hU : IsOpen U} {hV : IsOpen V} {hUV : U ∪ V = Set.univ} {h : ∀ b ∈ U ∩ V, g₁.inner b = g₂.inner b} {b : B} (hb : b ∈ U) : (g₁.piecewise g₂ hU hV hUV h).inner b = g₁.inner b

Over U, the glued metric is g₁.

theorem Bundle.ContMDiffRiemannianMetric.piecewise_inner_of_mem_right {EB : Type u_1} [NormedAddCommGroup EB] [NormedSpace ℝ EB] {HB : Type u_2} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_5} [TopologicalSpace (TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [(b : B) → AddCommGroup (E b)] [(b : B) → Module ℝ (E b)] [FiberBundle F E] [VectorBundle ℝ F E] {U V : Set B} {g₁ g₂ : ContMDiffRiemannianMetric IB n F E} {hU : IsOpen U} {hV : IsOpen V} {hUV : U ∪ V = Set.univ} {h : ∀ b ∈ U ∩ V, g₁.inner b = g₂.inner b} {b : B} (hb : b ∈ V) : (g₁.piecewise g₂ hU hV hUV h).inner b = g₂.inner b

Over V, the glued metric is g₂.