Covariant derivatives of sections and evaluation of connection operations

Mathlib's IsCovariantDerivativeOn is additive on pairs of sections differentiable at a point of the set it is a covariant derivative on. This file derives the corresponding statements for negatives and differences, and iterates additivity to finite sums of sections. It also evaluates Mathlib's CovariantDerivative.addOneForm on sections and CovariantDerivative.difference on section values and fibre vectors.

Main results

• IsCovariantDerivativeOn.neg and IsCovariantDerivativeOn.sub: a covariant derivative over u commutes with negation and subtraction of sections differentiable at a point of u.
• TauCeti.Manifold.covariantDerivative_sum: a covariant derivative over u commutes with finite sums of sections differentiable at a point of u.
• CovariantDerivative.covariantDerivative_smul_section_apply and CovariantDerivative.covariantDerivative_smul_section_vectorField: the Leibniz rule for the covariant derivative of a function multiple of a section at a tangent vector and along a vector field.
• CovariantDerivative.addOneForm_apply: evaluate a connection perturbed by an endomorphism-valued one-form on a section.
• CovariantDerivative.difference_apply: evaluate the difference of two connections on the value of a section differentiable at the base point.
• CovariantDerivative.difference_apply_eq_extend: evaluate the difference of two connections on a fibre vector using a local extension.

theorem TauCeti.Manifold.covariantDerivative_sum {𝕜 : 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] [VectorBundle 𝕜 F V] {x : M} {cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x} {κ : Type u_7} {u : Set M} {s : Finset κ} {τ : κ → (x : M) → V x} (hcov : IsCovariantDerivativeOn F cov u) (hx : x ∈ u) (hτ : ∀ i ∈ s, (MDiffAt fun (x : M) => ⟨x, τ i x⟩) x) : cov (∑ i ∈ s, τ i) x = ∑ i ∈ s, cov (τ i) x

A covariant derivative over u commutes with finite sums of sections differentiable at a point of u.

theorem IsCovariantDerivativeOn.neg {𝕜 : 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] [VectorBundle 𝕜 F V] {cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x} {u : Set M} {σ : (x : M) → V x} {x : M} (hcov : IsCovariantDerivativeOn F cov u) (hσ : (MDiffAt fun (x : M) => ⟨x, σ x⟩) x) (hx : x ∈ u := by trivial) : cov (-σ) x = -cov σ x

A covariant derivative over u sends the negative of a section differentiable at a point of u to the negative of its covariant derivative there.

theorem IsCovariantDerivativeOn.sub {𝕜 : 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] [VectorBundle 𝕜 F V] {cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x} {u : Set M} {σ σ' : (x : M) → V x} {x : M} (hcov : IsCovariantDerivativeOn F cov u) (hσ : (MDiffAt fun (x : M) => ⟨x, σ x⟩) x) (hσ' : (MDiffAt fun (x : M) => ⟨x, σ' x⟩) x) (hx : x ∈ u := by trivial) : cov (σ - σ') x = cov σ x - cov σ' x

A covariant derivative over u sends the difference of two sections differentiable at a point of u to the difference of their covariant derivatives there.

@[simp]

theorem CovariantDerivative.addOneForm_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) (A : (x : M) → V x →L[𝕜] TangentSpace I x →L[𝕜] V x) (σ : (x : M) → V x) (x : M) : ↑(cov.addOneForm A) σ x = ↑cov σ x + (A x) (σ x)

Adding an endomorphism-valued one-form, evaluated on a section.

theorem CovariantDerivative.covariantDerivative_smul_section_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) {f : M → 𝕜} {σ : (x : M) → V x} {x : M} (hf : MDiffAt f x) (hσ : (MDiffAt fun (x : M) => ⟨x, σ x⟩) x) (v : TangentSpace I x) : (↑cov (f • σ) x) v = f x • (↑cov σ x) v + (d% f x) v • σ x

Leibniz rule at a tangent vector. The covariant derivative of f • σ at x along v is f x • ∇_v σ + df_x(v) • σ x, for f and σ differentiable at x.

theorem CovariantDerivative.covariantDerivative_smul_section_vectorField {𝕜 : 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) {f : M → 𝕜} {σ : (x : M) → V x} {Z : (x : M) → TangentSpace I x} (hf : MDiff f) (hσ : MDiff fun (x : M) => ⟨x, σ x⟩) : (fun (y : M) => (↑cov (f • σ) y) (Z y)) = (f • fun (y : M) => (↑cov σ y) (Z y)) + (fun (y : M) => (d% f y) (Z y)) • σ

Leibniz rule along a vector field. The covariant derivative of f • σ along a vector field Z is f times the covariant derivative of σ along Z, plus the derivative of f along Z times σ, for a differentiable function f and a differentiable section σ.

theorem CovariantDerivative.difference_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] [VectorBundle 𝕜 F V] [CompleteSpace 𝕜] [FiniteDimensional 𝕜 F] [ContMDiffVectorBundle 1 F V I] (cov cov' : CovariantDerivative I F V) {σ : (x : M) → V x} {x : M} (hσ : (MDiffAt fun (x : M) => ⟨x, σ x⟩) x) : (cov.difference cov' x) (σ x) = ↑cov σ x - ↑cov' σ x

The difference of two connections evaluated on a section differentiable at the base point.

theorem CovariantDerivative.difference_apply_eq_extend {𝕜 : 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] [VectorBundle 𝕜 F V] [CompleteSpace 𝕜] [FiniteDimensional 𝕜 F] [ContMDiffVectorBundle 1 F V I] (cov cov' : CovariantDerivative I F V) (x : M) (w : V x) : (cov.difference cov' x) w = ↑cov (FiberBundle.extend F w) x - ↑cov' (FiberBundle.extend F w) x

Evaluate the difference of two connections through a local extension of a fibre vector.