Curvature of a covariant derivative #
For a covariant derivative ∇ on a vector bundle, this file defines its curvature operator
R(X, Y) σ = ∇ X (∇ Y σ) - ∇ Y (∇ X σ) - ∇ [X, Y] σ.
We use the sign convention of Lee. The arguments to Mathlib's CovariantDerivative are ordered
as cov σ x (X x) = ∇ X σ, so the order in the defining formula is worth making explicit.
The operator is alternating in its vector-field arguments. For a smooth connection it takes
smooth fields and sections to a smooth section and is linear over smooth scalar functions in all
three arguments; this is the tensoriality statement behind the pointwise (1,3)-curvature tensor
of a connection on the tangent bundle.
Main definitions and results #
CovariantDerivative.curvatureOperator: the curvature operator of a connection.CovariantDerivative.curvatureOperator_antisymm: curvature is antisymmetric in its two vector-field arguments.CovariantDerivative.contMDiff_curvatureOperator: a smooth connection has smooth curvature on smooth fields and sections.CovariantDerivative.curvatureOperator_smul_first,CovariantDerivative.curvatureOperator_smul_second, andCovariantDerivative.curvatureOperator_smul_section: curvature is linear over smooth functions in each argument.CovariantDerivative.curvatureOperator_congr: on finite-rank smooth bundles over finite-dimensional Hausdorff manifolds, curvature at a point depends only on the values of its three inputs there.CovariantDerivative.curvatureOperator_congr_of_eventuallyEq: curvature agrees at a point when its smooth inputs agree in a neighborhood of that point;CovariantDerivative.curvatureOperator_congr_of_eventuallyEq_of_mdifferentiableAtonly asks for differentiability near the point.CovariantDerivative.curvatureOperator_congr_covariantDerivative: two connections which agree on differentiable sections have the same curvature on differentiable inputs.
References #
- J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176, 2018, Chapter 7, pp. 196--198.
noncomputable def
CovariantDerivative.curvatureOperator
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[(x : M) → TopologicalSpace (V x)]
[∀ (x : M), IsTopologicalAddGroup (V x)]
[∀ (x : M), ContinuousSMul 𝕜 (V x)]
[FiberBundle F V]
(cov : CovariantDerivative I F V)
(X Y : (x : M) → TangentSpace I x)
(σ : (x : M) → V x)
(x : M)
:
V x
The curvature operator of a covariant derivative, with Lee's sign convention:
R(X, Y) σ = ∇ X (∇ Y σ) - ∇ Y (∇ X σ) - ∇ [X, Y] σ.
The output is left as an unbundled section so that the definition is available without any
regularity assumption on the connection. Smoothness is supplied by
contMDiff_curvatureOperator when the connection and input sections are smooth.
Instances For
theorem
CovariantDerivative.curvatureOperator_def
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[(x : M) → TopologicalSpace (V x)]
[∀ (x : M), IsTopologicalAddGroup (V x)]
[∀ (x : M), ContinuousSMul 𝕜 (V x)]
[FiberBundle F V]
(cov : CovariantDerivative I F V)
(X Y : (x : M) → TangentSpace I x)
(σ : (x : M) → V x)
:
cov.curvatureOperator X Y σ = fun (x : M) =>
(↑cov (fun (y : M) => (↑cov σ y) (Y y)) x) (X x) - (↑cov (fun (y : M) => (↑cov σ y) (X y)) x) (Y x) - (↑cov σ x) (VectorField.mlieBracket I X Y x)
The curvature operator as a section, expressed using covariant derivatives.
theorem
CovariantDerivative.curvatureOperator_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[(x : M) → TopologicalSpace (V x)]
[∀ (x : M), IsTopologicalAddGroup (V x)]
[∀ (x : M), ContinuousSMul 𝕜 (V x)]
[FiberBundle F V]
(cov : CovariantDerivative I F V)
(X Y : (x : M) → TangentSpace I x)
(σ : (x : M) → V x)
(x : M)
:
cov.curvatureOperator X Y σ x = (↑cov (fun (y : M) => (↑cov σ y) (Y y)) x) (X x) - (↑cov (fun (y : M) => (↑cov σ y) (X y)) x) (Y x) - (↑cov σ x) (VectorField.mlieBracket I X Y x)
The defining formula for the curvature operator evaluated at a point.
theorem
CovariantDerivative.curvatureOperator_antisymm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[(x : M) → TopologicalSpace (V x)]
[∀ (x : M), IsTopologicalAddGroup (V x)]
[∀ (x : M), ContinuousSMul 𝕜 (V x)]
[FiberBundle F V]
(cov : CovariantDerivative I F V)
(X Y : (x : M) → TangentSpace I x)
(σ : (x : M) → V x)
:
Curvature is antisymmetric in its two vector-field arguments.
@[simp]
theorem
CovariantDerivative.curvatureOperator_self
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[(x : M) → TopologicalSpace (V x)]
[∀ (x : M), IsTopologicalAddGroup (V x)]
[∀ (x : M), ContinuousSMul 𝕜 (V x)]
[FiberBundle F V]
(cov : CovariantDerivative I F V)
(X : (x : M) → TangentSpace I x)
(σ : (x : M) → V x)
:
Curvature vanishes when its two vector-field arguments coincide.
theorem
CovariantDerivative.curvatureOperator_congr_covariantDerivative
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[(x : M) → TopologicalSpace (V x)]
[∀ (x : M), IsTopologicalAddGroup (V x)]
[∀ (x : M), ContinuousSMul 𝕜 (V x)]
[FiberBundle F V]
(cov : CovariantDerivative I F V)
{cov' : CovariantDerivative I F V}
(h : ∀ ⦃σ : (x : M) → V x⦄ ⦃y : M⦄, (MDiffAt fun (x : M) => ⟨x, σ x⟩) y → ↑cov σ y = ↑cov' σ y)
{X Y : (x : M) → TangentSpace I x}
{σ : (x : M) → V x}
{x : M}
(hσ : MDiff fun (x : M) => ⟨x, σ x⟩)
(hXσ : (MDiffAt fun (y : M) => ⟨y, (↑cov' σ y) (X y)⟩) x)
(hYσ : (MDiffAt fun (y : M) => ⟨y, (↑cov' σ y) (Y y)⟩) x)
:
Two connections which agree on every section differentiable at the point of evaluation have the same curvature on a section which is differentiable everywhere, at every point where the covariant derivatives of that section along the two vector fields are differentiable. A connection is unconstrained on sections which are not differentiable, so this is the form in which a connection determined by other data, such as a Levi-Civita connection, is compared with an explicit one.
@[simp]
theorem
CovariantDerivative.curvatureOperator_zero_first
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[(x : M) → TopologicalSpace (V x)]
[∀ (x : M), IsTopologicalAddGroup (V x)]
[∀ (x : M), ContinuousSMul 𝕜 (V x)]
[FiberBundle F V]
(cov : CovariantDerivative I F V)
[VectorBundle 𝕜 F V]
(Y : (x : M) → TangentSpace I x)
(σ : (x : M) → V x)
:
Curvature vanishes when its first vector-field argument is zero.
@[simp]
theorem
CovariantDerivative.curvatureOperator_zero_second
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[(x : M) → TopologicalSpace (V x)]
[∀ (x : M), IsTopologicalAddGroup (V x)]
[∀ (x : M), ContinuousSMul 𝕜 (V x)]
[FiberBundle F V]
(cov : CovariantDerivative I F V)
[VectorBundle 𝕜 F V]
(X : (x : M) → TangentSpace I x)
(σ : (x : M) → V x)
:
Curvature vanishes when its second vector-field argument is zero.
@[simp]
theorem
CovariantDerivative.curvatureOperator_zero_section
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[(x : M) → TopologicalSpace (V x)]
[∀ (x : M), IsTopologicalAddGroup (V x)]
[∀ (x : M), ContinuousSMul 𝕜 (V x)]
[FiberBundle F V]
(cov : CovariantDerivative I F V)
[VectorBundle 𝕜 F V]
(X Y : (x : M) → TangentSpace I x)
:
Curvature vanishes on the zero section.
theorem
CovariantDerivative.contMDiff_curvatureOperator
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{V : M → Type u_5}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module ℝ (V x)]
[(x : M) → TopologicalSpace (V x)]
[∀ (x : M), IsTopologicalAddGroup (V x)]
[∀ (x : M), ContinuousSMul ℝ (V x)]
[FiberBundle F V]
(cov : CovariantDerivative I F V)
[CompleteSpace E]
[IsManifold I (↑⊤) M]
[VectorBundle ℝ F V]
[cov.ContMDiffCovariantDerivative ↑⊤]
{X Y : (x : M) → TangentSpace I x}
{σ : (x : M) → V x}
(hX : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, X x⟩)
(hY : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Y x⟩)
(hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (x : M) => ⟨x, σ x⟩)
:
ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (x : M) => ⟨x, cov.curvatureOperator X Y σ x⟩
The curvature operator of a smooth connection sends smooth vector fields and smooth sections to a smooth section.
@[simp]
theorem
CovariantDerivative.curvatureOperator_add_first
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{V : M → Type u_5}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module ℝ (V x)]
[(x : M) → TopologicalSpace (V x)]
[∀ (x : M), IsTopologicalAddGroup (V x)]
[∀ (x : M), ContinuousSMul ℝ (V x)]
[FiberBundle F V]
{cov : CovariantDerivative I F V}
[CompleteSpace E]
[IsManifold I (↑⊤) M]
[VectorBundle ℝ F V]
[cov.ContMDiffCovariantDerivative ↑⊤]
{X X' Y : (x : M) → TangentSpace I x}
{σ : (x : M) → V x}
(hX : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, X x⟩)
(hX' : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, X' x⟩)
(hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (x : M) => ⟨x, σ x⟩)
:
Curvature is additive in its first vector-field argument.
@[simp]
theorem
CovariantDerivative.curvatureOperator_add_second
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{V : M → Type u_5}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module ℝ (V x)]
[(x : M) → TopologicalSpace (V x)]
[∀ (x : M), IsTopologicalAddGroup (V x)]
[∀ (x : M), ContinuousSMul ℝ (V x)]
[FiberBundle F V]
{cov : CovariantDerivative I F V}
[CompleteSpace E]
[IsManifold I (↑⊤) M]
[VectorBundle ℝ F V]
[cov.ContMDiffCovariantDerivative ↑⊤]
{X Y Y' : (x : M) → TangentSpace I x}
{σ : (x : M) → V x}
(hY : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Y x⟩)
(hY' : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Y' x⟩)
(hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (x : M) => ⟨x, σ x⟩)
:
Curvature is additive in its second vector-field argument.
@[simp]
theorem
CovariantDerivative.curvatureOperator_add_section
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{V : M → Type u_5}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module ℝ (V x)]
[(x : M) → TopologicalSpace (V x)]
[∀ (x : M), IsTopologicalAddGroup (V x)]
[∀ (x : M), ContinuousSMul ℝ (V x)]
[FiberBundle F V]
{cov : CovariantDerivative I F V}
[IsManifold I (↑⊤) M]
[VectorBundle ℝ F V]
[cov.ContMDiffCovariantDerivative ↑⊤]
{X Y : (x : M) → TangentSpace I x}
{σ τ : (x : M) → V x}
(hX : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, X x⟩)
(hY : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Y x⟩)
(hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (x : M) => ⟨x, σ x⟩)
(hτ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (x : M) => ⟨x, τ x⟩)
:
Curvature is additive in its section argument.
@[simp]
theorem
CovariantDerivative.curvatureOperator_neg_first
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{V : M → Type u_5}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module ℝ (V x)]
[(x : M) → TopologicalSpace (V x)]
[∀ (x : M), IsTopologicalAddGroup (V x)]
[∀ (x : M), ContinuousSMul ℝ (V x)]
[FiberBundle F V]
{cov : CovariantDerivative I F V}
[IsManifold I (↑⊤) M]
[VectorBundle ℝ F V]
[cov.ContMDiffCovariantDerivative ↑⊤]
{X Y : (x : M) → TangentSpace I x}
{σ : (x : M) → V x}
(hX : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, X x⟩)
(hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (x : M) => ⟨x, σ x⟩)
:
Curvature changes sign when its first vector-field argument is negated.
@[simp]
theorem
CovariantDerivative.curvatureOperator_neg_second
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{V : M → Type u_5}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module ℝ (V x)]
[(x : M) → TopologicalSpace (V x)]
[∀ (x : M), IsTopologicalAddGroup (V x)]
[∀ (x : M), ContinuousSMul ℝ (V x)]
[FiberBundle F V]
{cov : CovariantDerivative I F V}
[IsManifold I (↑⊤) M]
[VectorBundle ℝ F V]
[cov.ContMDiffCovariantDerivative ↑⊤]
{X Y : (x : M) → TangentSpace I x}
{σ : (x : M) → V x}
(hY : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Y x⟩)
(hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (x : M) => ⟨x, σ x⟩)
:
Curvature changes sign when its second vector-field argument is negated.
@[simp]
theorem
CovariantDerivative.curvatureOperator_neg_section
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{V : M → Type u_5}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module ℝ (V x)]
[(x : M) → TopologicalSpace (V x)]
[∀ (x : M), IsTopologicalAddGroup (V x)]
[∀ (x : M), ContinuousSMul ℝ (V x)]
[FiberBundle F V]
{cov : CovariantDerivative I F V}
[IsManifold I (↑⊤) M]
[VectorBundle ℝ F V]
[cov.ContMDiffCovariantDerivative ↑⊤]
{X Y : (x : M) → TangentSpace I x}
{σ : (x : M) → V x}
(hX : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, X x⟩)
(hY : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Y x⟩)
(hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (x : M) => ⟨x, σ x⟩)
:
Curvature changes sign when its section argument is negated.
@[simp]
theorem
CovariantDerivative.curvatureOperator_smul_first
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{V : M → Type u_5}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module ℝ (V x)]
[(x : M) → TopologicalSpace (V x)]
[∀ (x : M), IsTopologicalAddGroup (V x)]
[∀ (x : M), ContinuousSMul ℝ (V x)]
[FiberBundle F V]
{cov : CovariantDerivative I F V}
[CompleteSpace E]
[IsManifold I (↑⊤) M]
[VectorBundle ℝ F V]
[cov.ContMDiffCovariantDerivative ↑⊤]
{X Y : (x : M) → TangentSpace I x}
{σ : (x : M) → V x}
{f : M → ℝ}
(hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f)
(hX : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, X x⟩)
(hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (x : M) => ⟨x, σ x⟩)
:
Curvature is linear over smooth functions in its first vector-field argument.
@[simp]
theorem
CovariantDerivative.curvatureOperator_smul_second
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{V : M → Type u_5}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module ℝ (V x)]
[(x : M) → TopologicalSpace (V x)]
[∀ (x : M), IsTopologicalAddGroup (V x)]
[∀ (x : M), ContinuousSMul ℝ (V x)]
[FiberBundle F V]
{cov : CovariantDerivative I F V}
[CompleteSpace E]
[IsManifold I (↑⊤) M]
[VectorBundle ℝ F V]
[cov.ContMDiffCovariantDerivative ↑⊤]
{X Y : (x : M) → TangentSpace I x}
{σ : (x : M) → V x}
{f : M → ℝ}
(hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f)
(hY : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Y x⟩)
(hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (x : M) => ⟨x, σ x⟩)
:
Curvature is linear over smooth functions in its second vector-field argument.
@[simp]
theorem
CovariantDerivative.curvatureOperator_smul_section
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{V : M → Type u_5}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module ℝ (V x)]
[(x : M) → TopologicalSpace (V x)]
[∀ (x : M), IsTopologicalAddGroup (V x)]
[∀ (x : M), ContinuousSMul ℝ (V x)]
[FiberBundle F V]
{cov : CovariantDerivative I F V}
[CompleteSpace E]
[IsManifold I (↑⊤) M]
[VectorBundle ℝ F V]
[cov.ContMDiffCovariantDerivative ↑⊤]
{X Y : (x : M) → TangentSpace I x}
{σ : (x : M) → V x}
{f : M → ℝ}
(hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f)
(hX : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, X x⟩)
(hY : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Y x⟩)
(hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (x : M) => ⟨x, σ x⟩)
:
Curvature is linear over smooth functions in its section argument.
theorem
CovariantDerivative.curvatureOperator_congr_of_eventuallyEq_of_mdifferentiableAt
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{V : M → Type u_5}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module ℝ (V x)]
[(x : M) → TopologicalSpace (V x)]
[∀ (x : M), IsTopologicalAddGroup (V x)]
[∀ (x : M), ContinuousSMul ℝ (V x)]
[FiberBundle F V]
{cov : CovariantDerivative I F V}
{X X' Y Y' : (x : M) → TangentSpace I x}
{σ σ' : (x : M) → V x}
{x : M}
(hσ' : ∀ᶠ (y : M) in nhds x, (MDiffAt fun (x : M) => ⟨x, σ' x⟩) y)
(hY'σ' : (MDiffAt fun (y : M) => ⟨y, (↑cov σ' y) (Y' y)⟩) x)
(hX'σ' : (MDiffAt fun (y : M) => ⟨y, (↑cov σ' y) (X' y)⟩) x)
(hXX' : X =ᶠ[nhds x] X')
(hYY' : Y =ᶠ[nhds x] Y')
(hσσ' : ∀ᶠ (y : M) in nhds x, σ y = σ' y)
:
Curvature at a point is unchanged when its inputs agree in a neighborhood of that point, provided the second section is differentiable near the point and the covariant derivatives of it entering the curvature are differentiable at the point. Nothing is asked of the first inputs, and no global smoothness is required, so this applies to local frames.
theorem
CovariantDerivative.curvatureOperator_congr_of_eventuallyEq
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{V : M → Type u_5}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module ℝ (V x)]
[(x : M) → TopologicalSpace (V x)]
[∀ (x : M), IsTopologicalAddGroup (V x)]
[∀ (x : M), ContinuousSMul ℝ (V x)]
[FiberBundle F V]
{cov : CovariantDerivative I F V}
[IsManifold I (↑⊤) M]
[VectorBundle ℝ F V]
[cov.ContMDiffCovariantDerivative ↑⊤]
{X X' Y Y' : (x : M) → TangentSpace I x}
{σ σ' : (x : M) → V x}
{x : M}
(hX' : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, X' x⟩)
(hY' : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Y' x⟩)
(hσ' : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (x : M) => ⟨x, σ' x⟩)
(hXX' : X =ᶠ[nhds x] X')
(hYY' : Y =ᶠ[nhds x] Y')
(hσσ' : ∀ᶠ (y : M) in nhds x, σ y = σ' y)
:
Curvature at a point is unchanged when its inputs agree in a neighborhood of that point with smooth inputs.
theorem
CovariantDerivative.curvatureOperator_congr
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{V : M → Type u_5}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module ℝ (V x)]
[(x : M) → TopologicalSpace (V x)]
[∀ (x : M), IsTopologicalAddGroup (V x)]
[∀ (x : M), ContinuousSMul ℝ (V x)]
[FiberBundle F V]
{cov : CovariantDerivative I F V}
[IsManifold I (↑⊤) M]
[VectorBundle ℝ F V]
[cov.ContMDiffCovariantDerivative ↑⊤]
[FiniteDimensional ℝ E]
[T2Space M]
[FiniteDimensional ℝ F]
[ContMDiffVectorBundle (↑⊤) F V I]
{X X' Y Y' : (x : M) → TangentSpace I x}
{σ σ' : (x : M) → V x}
{x : M}
(hX : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, X x⟩)
(hX' : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, X' x⟩)
(hY : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Y x⟩)
(hY' : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Y' x⟩)
(hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (x : M) => ⟨x, σ x⟩)
(hσ' : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (x : M) => ⟨x, σ' x⟩)
(hXX' : X x = X' x)
(hYY' : Y x = Y' x)
(hσσ' : σ x = σ' x)
:
On a finite-dimensional Hausdorff manifold and a finite-rank smooth vector bundle, the value of curvature on smooth inputs depends only on their values at the given point.