Theorems · Definition · differential geometry

CovariantDerivative.derivMetricTensor

{E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {H : Type u_2} →
        [inst_2 : TopologicalSpace H] →
          {I : ModelWithCorners ℝ E H} →
            {M : Type u_3} →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : ChartedSpace H M] →
                  {F : Type u_4} →
                    [inst_5 : NormedAddCommGroup F] →
                      [inst_6 : NormedSpace ℝ F] →
                        {V : M → Type u_5} →
                          [inst_7 : TopologicalSpace (Bundle.TotalSpace F V)] →
                            [inst_8 : (x : M) → NormedAddCommGroup (V x)] →
                              [inst_9 : (x : M) → InnerProductSpace ℝ (V x)] →
                                [inst_10 : FiberBundle F V] →
                                  CovariantDerivative I F V →
                                    [inst_11 : VectorBundle ℝ F V] →
                                      [IsContMDiffRiemannianBundle I 1 F V] →
                                        [ContMDiffVectorBundle 1 F V I] →
                                          [FiniteDimensional ℝ F] →
                                            (x : M) → V x →L[ℝ] V x →L[ℝ] TangentSpace I x →L[ℝ] ℝ

The tensor (X, σ, τ) ↦ X g(σ, τ) - g(∇_X σ, τ) - g(σ, ∇_X τ) defining when a connection ∇ on a Riemannian bundle (M, V) is compatible with the metric g.

Defined in

Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric

Cited by

5 results in Mathlib

Foundations

Depth 229 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceNormedAddCommGroupInnerProductSpaceFiberBundleVectorBundleIsContMDiffRiemannianBundleContMDiffVectorBundleFiniteDimensional