A manifold carrying a chosen Riemannian metric

The Riemannian API (gradient, volume density, Levi-Civita connection, curvature) is driven by a RiemannianBundle instance on the tangent bundle. Comparing two metrics g and g' on the same manifold M, for instance a metric and a conformal rescaling of it, would require two incompatible instances on the same carrier. Instead, TauCeti.WithMetric g is a copy of M whose RiemannianBundle instance is g; different metrics give different copies, and each copy has exactly one metric instance.

The copy carries the topology, charts and manifold structure of M, transported along the tautological equivalence ofWithMetric : WithMetric g → M, and the Borel σ-algebra of that topology. The map ofWithMetric is a diffeomorphism of every order, its differential is the identity of the model space, and the metric of the copy is the pullback of g along it. Two copies of M are related by the identity diffeomorphism TauCeti.WithMetric.diffeomorphWithMetric.

Main definitions

• TauCeti.WithMetric g: the manifold M with the Riemannian metric g, together with the conversions TauCeti.WithMetric.toWithMetric and TauCeti.WithMetric.ofWithMetric.
• TauCeti.WithMetric.diffeomorph: the diffeomorphism WithMetric g ≃ M.
• TauCeti.WithMetric.diffeomorphWithMetric: the identity diffeomorphism between the copies of M carrying two metrics.
• TauCeti.WithMetric.metric: the metric of the copy, the pullback of g along ofWithMetric, installed as its RiemannianBundle instance.

Main results

• TauCeti.WithMetric.mfderiv_ofWithMetric: the differential of ofWithMetric is the identity.
• TauCeti.WithMetric.mfderiv_comp_ofWithMetric: the chain rule for a function read on the copy, without a differentiability hypothesis.
• TauCeti.WithMetric.inner_def: the inner product of the copy is g evaluated on the transported tangent vectors.
• TauCeti.WithMetric.mfderiv_ofWithMetric_chartLocalFrame: the chart frames of the copy are those of M.

structure TauCeti.WithMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) : Type u_3

The manifold M carrying the Riemannian metric g: a copy of M whose RiemannianBundle instance is g. Distinct metrics on M give distinct copies, so that two metrics can be compared without installing two metric instances on one carrier.

• toWithMetric :: (
• ofWithMetric : M

  The underlying point of M.

• )

theorem TauCeti.WithMetric.ext {E : Type u_1} {inst✝ : NormedAddCommGroup E} {inst✝¹ : NormedSpace ℝ E} {H : Type u_2} {inst✝² : TopologicalSpace H} {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} {inst✝³ : TopologicalSpace M} {inst✝⁴ : ChartedSpace H M} {inst✝⁵ : IsManifold I 1 M} {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} {x y : WithMetric g} (ofWithMetric : x.ofWithMetric = y.ofWithMetric) : x = y

theorem TauCeti.WithMetric.ext_iff {E : Type u_1} {inst✝ : NormedAddCommGroup E} {inst✝¹ : NormedSpace ℝ E} {H : Type u_2} {inst✝² : TopologicalSpace H} {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} {inst✝³ : TopologicalSpace M} {inst✝⁴ : ChartedSpace H M} {inst✝⁵ : IsManifold I 1 M} {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} {x y : WithMetric g} : x = y ↔ x.ofWithMetric = y.ofWithMetric

def TauCeti.WithMetric.equiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) : WithMetric g ≃ M

The tautological equivalence between the copy of M carrying g and M.

@[simp]

theorem TauCeti.WithMetric.equiv_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (x : WithMetric g) : (equiv g) x = x.ofWithMetric

@[simp]

theorem TauCeti.WithMetric.equiv_symm_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (x : M) : (equiv g).symm x = { ofWithMetric := x }

@[simp]

theorem TauCeti.WithMetric.ofWithMetric_toWithMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (x : M) : { ofWithMetric := x }.ofWithMetric = x

@[simp]

theorem TauCeti.WithMetric.toWithMetric_ofWithMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (x : WithMetric g) : { ofWithMetric := x.ofWithMetric } = x

theorem TauCeti.WithMetric.ofWithMetric_injective {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} : Function.Injective ofWithMetric

theorem TauCeti.WithMetric.toWithMetric_injective {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) : Function.Injective (toWithMetric g)

@[simp]

theorem TauCeti.WithMetric.ofWithMetric_inj {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} {x y : WithMetric g} : x.ofWithMetric = y.ofWithMetric ↔ x = y

theorem TauCeti.WithMetric.toWithMetric_inj {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) {x y : M} : { ofWithMetric := x } = { ofWithMetric := y } ↔ x = y

Two points of M give the same point of the copy only if they are equal. Not tagged @[simp]: simp already proves it with the constructor lemma TauCeti.WithMetric.toWithMetric.injEq.

@[instance_reducible]

instance TauCeti.WithMetric.instTopologicalSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) : TopologicalSpace (WithMetric g)

The copy of M carrying g has the topology of M.

def TauCeti.WithMetric.homeomorph {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) : WithMetric g ≃ₜ M

The tautological homeomorphism between the copy of M carrying g and M.

@[simp]

theorem TauCeti.WithMetric.coe_homeomorph {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) : ⇑(homeomorph g) = ofWithMetric

@[simp]

theorem TauCeti.WithMetric.coe_homeomorph_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) : ⇑(homeomorph g).symm = toWithMetric g

instance TauCeti.WithMetric.instCompactSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) [CompactSpace M] : CompactSpace (WithMetric g)

The copy of a compact manifold is compact.

instance TauCeti.WithMetric.instLindelofSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) [LindelofSpace M] : LindelofSpace (WithMetric g)

The copy of a Lindelöf manifold is Lindelöf.

@[instance_reducible]

instance TauCeti.WithMetric.instMeasurableSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) : MeasurableSpace (WithMetric g)

The copy of M carrying g is measured on its Borel σ-algebra.

instance TauCeti.WithMetric.instBorelSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) : BorelSpace (WithMetric g)

@[instance_reducible]

instance TauCeti.WithMetric.instChartedSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) : ChartedSpace H (WithMetric g)

The copy of M carrying g has the charts of M, precomposed with ofWithMetric.

theorem TauCeti.WithMetric.chartAt_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (x : WithMetric g) : chartAt H x = (homeomorph g).transOpenPartialHomeomorph (chartAt H x.ofWithMetric)

instance TauCeti.WithMetric.instIsManifoldReal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) {k : WithTop ℕ∞} [IsManifold I k M] : IsManifold I k (WithMetric g)

The chart transitions of the copy are those of M, so it is a manifold of the same smoothness.

theorem TauCeti.WithMetric.mem_chartAt_source_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} (α x : WithMetric g) : x ∈ (chartAt H α).source ↔ x.ofWithMetric ∈ (chartAt H α.ofWithMetric).source

theorem TauCeti.WithMetric.extChartAt_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} (α x : WithMetric g) : ↑(extChartAt I α) x = ↑(extChartAt I α.ofWithMetric) x.ofWithMetric

theorem TauCeti.WithMetric.extChartAt_symm_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} (α : WithMetric g) (z : E) : ↑(extChartAt I α).symm z = { ofWithMetric := ↑(extChartAt I α.ofWithMetric).symm z }

theorem TauCeti.WithMetric.trivializationAt_apply_snd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} (α x : WithMetric g) (v : TangentSpace I x) : (↑(trivializationAt E (TangentSpace I) α) ⟨x, v⟩).2 = (↑(trivializationAt E (TangentSpace I) α.ofWithMetric) ⟨x.ofWithMetric, v⟩).2

The tangent trivializations of the copy read a tangent vector in the same coordinates as those of M.

theorem TauCeti.WithMetric.trivializationAt_linearEquivAt_symm_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} (α x : WithMetric g) (hx : x ∈ (trivializationAt E (TangentSpace I) α).baseSet) (hx' : x.ofWithMetric ∈ (trivializationAt E (TangentSpace I) α.ofWithMetric).baseSet) (z : E) : (Bundle.Trivialization.linearEquivAt ℝ (trivializationAt E (TangentSpace I) α) x hx).symm z = (Bundle.Trivialization.linearEquivAt ℝ (trivializationAt E (TangentSpace I) α.ofWithMetric) x.ofWithMetric hx').symm z

The tangent trivializations of the copy and of M have the same inverse on fibres.

noncomputable def TauCeti.WithMetric.diffeomorph {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (k : WithTop ℕ∞) : Diffeomorph I I (WithMetric g) M k

The tautological diffeomorphism, of every order, between the copy of M carrying g and M.

@[simp]

theorem TauCeti.WithMetric.coe_diffeomorph {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} (k : WithTop ℕ∞) : ⇑(diffeomorph g k) = ofWithMetric

@[simp]

theorem TauCeti.WithMetric.coe_diffeomorph_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} (k : WithTop ℕ∞) : ⇑(diffeomorph g k).symm = toWithMetric g

theorem TauCeti.WithMetric.continuous_ofWithMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} : Continuous ofWithMetric

theorem TauCeti.WithMetric.continuous_toWithMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} : Continuous (toWithMetric g)

theorem TauCeti.WithMetric.contMDiff_ofWithMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} {k : WithTop ℕ∞} : ContMDiff I I k ofWithMetric

ofWithMetric is a diffeomorphism, hence smooth of every order.

theorem TauCeti.WithMetric.contMDiff_toWithMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} {k : WithTop ℕ∞} : ContMDiff I I k (toWithMetric g)

toWithMetric g is a diffeomorphism, hence smooth of every order.

theorem TauCeti.WithMetric.hasMFDerivAt_ofWithMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} (x : WithMetric g) : HasMFDerivAt% ofWithMetric x (ContinuousLinearMap.id ℝ (TangentSpace I x))

The differential of ofWithMetric is the identity of the model space.

theorem TauCeti.WithMetric.hasMFDerivAt_toWithMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} (x : M) : HasMFDerivAt% (toWithMetric g) x (ContinuousLinearMap.id ℝ (TangentSpace I x))

The differential of toWithMetric g is the identity of the model space.

The tangent spaces TangentSpace I x of a point x of the copy and TangentSpace I x.ofWithMetric of the underlying point of M are both, by definition, the model space E. The following lemmas state that the differentials of ofWithMetric and toWithMetric g are the identity under this identification; later statements comparing tangent vectors of the copy with tangent vectors of M go through these lemmas rather than through the identification.

theorem TauCeti.WithMetric.mfderiv_ofWithMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} (x : WithMetric g) : mfderiv% ofWithMetric x = ContinuousLinearMap.id ℝ (TangentSpace I x)

The differential of ofWithMetric is the identity of the model space.

theorem TauCeti.WithMetric.mfderiv_toWithMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} (x : M) : mfderiv% (toWithMetric g) x = ContinuousLinearMap.id ℝ (TangentSpace I x)

The differential of toWithMetric g is the identity of the model space.

theorem TauCeti.WithMetric.mfderiv_ofWithMetric_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} (x : WithMetric g) (v : TangentSpace I x) : (mfderiv% ofWithMetric x) v = v

The differential of ofWithMetric maps a tangent vector to itself.

theorem TauCeti.WithMetric.mfderiv_toWithMetric_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} (x : M) (v : TangentSpace I x) : (mfderiv% (toWithMetric g) x) v = v

The differential of toWithMetric g maps a tangent vector to itself.

@[simp]

theorem TauCeti.WithMetric.mfderiv_ofWithMetric_mfderiv_toWithMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} (x : M) (v : TangentSpace I x) : (mfderiv% ofWithMetric { ofWithMetric := x }) ((mfderiv% (toWithMetric g) x) v) = v

Transporting a tangent vector of M to the copy and back gives the vector itself.

@[simp]

theorem TauCeti.WithMetric.mfderiv_toWithMetric_mfderiv_ofWithMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} (x : WithMetric g) (v : TangentSpace I x) : (mfderiv% (toWithMetric g) x.ofWithMetric) ((mfderiv% ofWithMetric x) v) = v

Transporting a tangent vector of the copy to M and back gives the vector itself.

theorem TauCeti.WithMetric.mdifferentiableAt_comp_ofWithMetric_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u_6} [TopologicalSpace M'] [ChartedSpace H' M'] {u : M → M'} {x : WithMetric g} : MDiffAt (u ∘ ofWithMetric) x ↔ MDiffAt u x.ofWithMetric

A map out of M is differentiable at a point exactly when it is differentiable as a map out of the copy of M.

theorem TauCeti.WithMetric.mfderiv_comp_ofWithMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u_6} [TopologicalSpace M'] [ChartedSpace H' M'] (u : M → M') (x : WithMetric g) : mfderiv% (u ∘ ofWithMetric) x = mfderiv% u x.ofWithMetric ∘SL mfderiv% ofWithMetric x

The chain rule along ofWithMetric. Since ofWithMetric is a diffeomorphism, it holds without a differentiability hypothesis on u.

theorem TauCeti.WithMetric.mvfderiv_comp_ofWithMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℝ F] (u : M → F) (x : WithMetric g) : d% (u ∘ ofWithMetric) x = d% u x.ofWithMetric ∘SL mfderiv% ofWithMetric x

The differential of a vector-valued function pulls back along ofWithMetric, without any differentiability hypothesis on the function.

theorem TauCeti.WithMetric.mvfderiv_comp_ofWithMetric_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℝ F] (u : M → F) (x : WithMetric g) (v : TangentSpace I x) : (d% (u ∘ ofWithMetric) x) v = (d% u x.ofWithMetric) ((mfderiv% ofWithMetric x) v)

The differential of a vector-valued function read on the copy of M.

noncomputable def TauCeti.WithMetric.diffeomorphWithMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g g' : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (k : WithTop ℕ∞) : Diffeomorph I I (WithMetric g) (WithMetric g') k

The identity diffeomorphism from the copy of M carrying g to the copy carrying g'.

@[simp]

theorem TauCeti.WithMetric.diffeomorphWithMetric_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} (g' : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (k : WithTop ℕ∞) (x : WithMetric g) : (diffeomorphWithMetric g g' k) x = { ofWithMetric := x.ofWithMetric }

@[simp]

theorem TauCeti.WithMetric.diffeomorphWithMetric_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} (g' : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (k : WithTop ℕ∞) : (diffeomorphWithMetric g g' k).symm = diffeomorphWithMetric g' g k

@[simp]

theorem TauCeti.WithMetric.diffeomorphWithMetric_trans {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} (g' g'' : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (k : WithTop ℕ∞) : (diffeomorphWithMetric g g' k).trans (diffeomorphWithMetric g' g'' k) = diffeomorphWithMetric g g'' k

theorem TauCeti.WithMetric.mfderiv_diffeomorphWithMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} (g' : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (k : WithTop ℕ∞) (x : WithMetric g) : mfderiv% ⇑(diffeomorphWithMetric g g' k) x = ContinuousLinearMap.id ℝ (TangentSpace I x)

The differential of the identity diffeomorphism between two copies of M is the identity of the model space.

noncomputable def TauCeti.WithMetric.metric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) [FiniteDimensional ℝ E] : Bundle.ContMDiffRiemannianMetric I n E fun (x : WithMetric g) => TangentSpace I x

The metric of the copy of M carrying g: the pullback of g along ofWithMetric.

@[instance_reducible]

noncomputable instance TauCeti.WithMetric.instRiemannianBundleTangentSpaceReal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} [FiniteDimensional ℝ E] : Bundle.RiemannianBundle fun (x : WithMetric g) => TangentSpace I x

The copy of M carrying g has the metric g.

instance TauCeti.WithMetric.instIsContMDiffRiemannianBundleTangentSpaceReal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} [FiniteDimensional ℝ E] : IsContMDiffRiemannianBundle I n E fun (x : WithMetric g) => TangentSpace I x

The metric of the copy of M carrying a C^n metric is C^n.

instance TauCeti.WithMetric.instIsContinuousRiemannianBundleTangentSpaceReal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} [FiniteDimensional ℝ E] : IsContinuousRiemannianBundle E fun (x : WithMetric g) => TangentSpace I x

The metric of the copy of M carrying g is continuous.

theorem TauCeti.WithMetric.inner_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} [FiniteDimensional ℝ E] (x : WithMetric g) (v w : TangentSpace I x) : inner ℝ v w = ((g.inner x.ofWithMetric) ((mfderiv% ofWithMetric x) v)) ((mfderiv% ofWithMetric x) w)

The inner product of two tangent vectors of the copy of M carrying g is g evaluated on the corresponding tangent vectors of M.

theorem TauCeti.WithMetric.mfderiv_ofWithMetric_chartLocalFrame {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} [FiniteDimensional ℝ E] (α x : WithMetric g) (i : Fin (Module.finrank ℝ E)) : (mfderiv% ofWithMetric x) (Riemannian.Tensor.chartLocalFrame α i x) = Riemannian.Tensor.chartLocalFrame α.ofWithMetric i x.ofWithMetric

The chart frames of the copy of M are those of M.