Theorems · Definition · differential geometry

CovariantDerivative.IsMetricCompatible

{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] → Prop

Predicate saying that a connection ∇ on a Riemannian bundle (V, g) is compatible with the ambient metric, i.e. for all differentiable vector fields X on M and sections σ and τ of V, we have X ⟨σ, τ⟩ = ⟨∇_X σ, τ⟩ + ⟨σ, ∇_X τ⟩.

Defined in

Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceNormedAddCommGroupInnerProductSpaceFiberBundleVectorBundleIsContMDiffRiemannianBundleContMDiffVectorBundleFiniteDimensional