Documentation

Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic

Covariant derivatives #

This file defines covariant derivatives (aka Koszul connections) on vector bundles over manifolds.

There are versions of the story: a local unbundled one and a global bundled one. The local version is used by the global version but also (in other files) when seeing a global object in a local trivialization.

In the whole file M is a manifold over any nontrivially normed field π•œ and V is a vector bundle over M with model fiber F.

Main definitions and constructions #

Implementation notes #

On paper there are several equivalent ways to define covariant derivatives on a vector bundle V β†’ M. The most common one starts with a function βˆ‡ taking as input a global smooth vector field X and a global smooth section Οƒ and giving as output a global smooth section βˆ‡_X Οƒ, before proving the result that (βˆ‡_X Οƒ) x at a point x only depends on the value of the vector field at that point and the 1-jet of the section at that point.

Here we ask for a map sending a global section Οƒ of V to a global section βˆ‡ Οƒ of Hom(TM, V). So the fact that (βˆ‡_X Οƒ) x depends only on X x is baked into the definition. Note also that we don’t put any differentiability restriction on Οƒ and X, the type of the covariant derivative map is simply (Ξ  x : M, V x) β†’ (Ξ  x : M, TangentSpace I x β†’L[π•œ] V x)). But the conditions on this map involve differentiability, see the definition of IsCovariantDerivativeOn.

This file proves that (βˆ‡_X Οƒ) x depends only on the germ of Οƒ at x, but not the stronger statement that it depends only the 1-jet of Οƒ at x. This will be proved in a later file.

Local unbundled theory #

source
structure IsCovariantDerivativeOn {π•œ : 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 : ((x : M) β†’ V x) β†’ (x : M) β†’ TangentSpace I x β†’L[π•œ] V x) (s : Set M := Set.univ) :
Prop

A function from sections of a vector bundle V on a manifold M to sections of $Hom(TM, E)$ is a covariant derivative over a set s in M if it is additive and satisfies the Leibniz rule when applied to sections that are differentiable at a point of s.

Caution, the argument order is nonstandard: cov Οƒ x (X x) corresponds to βˆ‡_X Οƒ x on paper.

  • add {Οƒ Οƒ' : (x : M) β†’ V x} {x : M} (hΟƒ : MDiffAt (T% Οƒ) x) (hΟƒ' : MDiffAt (T% Οƒ') x) (hx : x ∈ s := by trivial) : cov (Οƒ + Οƒ') x = cov Οƒ x + cov Οƒ' x
  • leibniz {Οƒ : (x : M) β†’ V x} {g : M β†’ π•œ} {x : M} (hΟƒ : MDiffAt (T% Οƒ) x) (hg : MDiffAt g x) (hx : x ∈ s := by trivial) : cov (g β€’ Οƒ) x = g x β€’ cov Οƒ x + (extDerivFun g x).smulRight (Οƒ x)
Instances For
    source
    class ContMDiffCovariantDerivativeOn {π•œ : 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] [IsManifold I 1 M] [VectorBundle π•œ F V] (k : WithTop β„•βˆž) (cov : ((x : M) β†’ V x) β†’ (x : M) β†’ TangentSpace I x β†’L[π•œ] V x) (u : Set M) :
    Prop

    A covariant derivative βˆ‡ is called of class C^k iff, whenever X is a C^k section and Οƒ a C^{k+1} section, the result βˆ‡_X Οƒ is a C^k section. This is a class so typeclass inference can deduce this automatically. We will prove in a later file that any C^(k+1) covariant derivative is C^k.

    Instances

      Changing set #

      In this section, we change s in IsCovariantDerivativeOn F cov s, proving the condition is monotone and local.

      source
      theorem IsCovariantDerivativeOn.mono {π•œ : 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 : ((x : M) β†’ V x) β†’ (x : M) β†’ TangentSpace I x β†’L[π•œ] V x} {s t : Set M} (hcov : IsCovariantDerivativeOn F cov t) (hst : s βŠ† t) :
      IsCovariantDerivativeOn F cov s
      source
      theorem IsCovariantDerivativeOn.iUnion {π•œ : 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] {ΞΉ : Type u_7} {cov : ((x : M) β†’ V x) β†’ (x : M) β†’ TangentSpace I x β†’L[π•œ] V x} {s : ΞΉ β†’ Set M} (hcov : βˆ€ (i : ΞΉ), IsCovariantDerivativeOn F cov (s i)) :
      IsCovariantDerivativeOn F cov (⋃ (i : ΞΉ), s i)
      source
      theorem IsCovariantDerivativeOn.congr_of_eqOn {π•œ : 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 : ((x : M) β†’ V x) β†’ (x : M) β†’ TangentSpace I x β†’L[π•œ] V x} {s : Set M} (hcov : IsCovariantDerivativeOn F cov s) {Οƒ Οƒ' : (x : M) β†’ V x} {x : M} (hΟƒ : MDiffAt (T% Οƒ) x) (hΟƒ' : MDiffAt (T% Οƒ') x) (hxs : s ∈ nhds x) (hσσ' : βˆ€ x ∈ s, Οƒ x = Οƒ' x) :
      cov Οƒ x = cov Οƒ' x

      Given a covariant derivative cov on a neighborhood s of a point x, if sections Οƒ and Οƒ' agree on s and are differentiable at x, then cov Οƒ x = cov Οƒ x'.

      source
      theorem IsCovariantDerivativeOn.congr_of_eventuallyEq {π•œ : 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 : ((x : M) β†’ V x) β†’ (x : M) β†’ TangentSpace I x β†’L[π•œ] V x} {s : Set M} (hcov : IsCovariantDerivativeOn F cov s) {Οƒ Οƒ' : (x : M) β†’ V x} {x : M} (hΟƒ : MDiffAt (T% Οƒ) x) (hΟƒ' : MDiffAt (T% Οƒ') x) (hxs : s ∈ nhds x) (hσσ' : βˆ€αΆ  (x : M) in nhds x, Οƒ x = Οƒ' x) :
      cov Οƒ x = cov Οƒ' x

      Given a covariant derivative cov on a neighborhood s of a point x, if sections Οƒ and Οƒ' agree near x and are differentiable at x, then cov Οƒ x = cov Οƒ x'.

      Computational properties #

      source
      theorem IsCovariantDerivativeOn.zero {π•œ : 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 : ((x : M) β†’ V x) β†’ (x : M) β†’ TangentSpace I x β†’L[π•œ] V x} {s : Set M} [VectorBundle π•œ F V] (hcov : IsCovariantDerivativeOn F cov s) {x : M} (hx : x ∈ s := by trivial) :
      cov 0 x = 0
      source
      theorem IsCovariantDerivativeOn.smul_const {π•œ : 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 : ((x : M) β†’ V x) β†’ (x : M) β†’ TangentSpace I x β†’L[π•œ] V x} {s : Set M} (hcov : IsCovariantDerivativeOn F cov s) {Οƒ : (x : M) β†’ V x} {x : M} (a : π•œ) (hΟƒ : MDiffAt (T% Οƒ) x) (hx : x ∈ s := by trivial) :
      cov (a β€’ Οƒ) x = a β€’ cov Οƒ x

      Operations #

      In this section we prove that:

      Note: morally this means covariant derivatives form an affine space over the vector space of one-forms taking values in the endomorphisms of the bundle, but we don’t package it that way yet.

      source
      theorem IsCovariantDerivativeOn.affine_combination {π•œ : 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] {s : Set M} {cov : ((x : M) β†’ V x) β†’ (x : M) β†’ TangentSpace I x β†’L[π•œ] V x} (hcov : IsCovariantDerivativeOn F cov s) {cov' : ((x : M) β†’ V x) β†’ (x : M) β†’ TangentSpace I x β†’L[π•œ] V x} (hcov' : IsCovariantDerivativeOn F cov' s) (g : M β†’ π•œ) :
      IsCovariantDerivativeOn F (fun (Οƒ : (x : M) β†’ V x) => g β€’ cov Οƒ + (1 - g) β€’ cov' Οƒ) s

      An affine combination of covariant derivatives is a covariant derivative.

      source
      theorem ContMDiffCovariantDerivativeOn.affine_combination {π•œ : 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] [IsManifold I 1 M] [VectorBundle π•œ F V] {cov cov' : ((x : M) β†’ V x) β†’ (x : M) β†’ TangentSpace I x β†’L[π•œ] V x} {u : Set M} {f : M β†’ π•œ} {n : WithTop β„•βˆž} (hf : ContMDiffOn I (modelWithCornersSelf π•œ π•œ) n f u) (Hcov : ContMDiffCovariantDerivativeOn F n cov u) (Hcov' : ContMDiffCovariantDerivativeOn F n cov' u) :
      ContMDiffCovariantDerivativeOn F n (fun (Οƒ : (x : M) β†’ V x) => f β€’ cov Οƒ + (1 - f) β€’ cov' Οƒ) u

      An affine combination of two C^k connections is a C^k connection.

      source
      theorem IsCovariantDerivativeOn.finite_affine_combination {π•œ : 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] {ΞΉ : Type u_7} {s : Finset ΞΉ} {u : Set M} {cov : ΞΉ β†’ ((x : M) β†’ V x) β†’ (x : M) β†’ TangentSpace I x β†’L[π•œ] V x} (h : βˆ€ (i : ΞΉ), IsCovariantDerivativeOn F (cov i) u) {f : ΞΉ β†’ M β†’ π•œ} (hf : βˆ‘ i ∈ s, f i = 1) :
      IsCovariantDerivativeOn F (fun (Οƒ : (x : M) β†’ V x) (x : M) => βˆ‘ i ∈ s, f i x β€’ cov i Οƒ x) u

      A finite affine combination of covariant derivatives is a covariant derivative.

      source
      theorem ContMDiffCovariantDerivativeOn.finite_affine_combination {π•œ : 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] [IsManifold I 1 M] {n : WithTop β„•βˆž} [VectorBundle π•œ F V] {ΞΉ : Type u_7} {s : Finset ΞΉ} {u : Set M} {cov : ΞΉ β†’ ((x : M) β†’ V x) β†’ (x : M) β†’ TangentSpace I x β†’L[π•œ] V x} (hcov : βˆ€ i ∈ s, ContMDiffCovariantDerivativeOn F n (cov i) u) {f : ΞΉ β†’ M β†’ π•œ} (hf : βˆ€ i ∈ s, ContMDiffOn I (modelWithCornersSelf π•œ π•œ) n (f i) u) :
      ContMDiffCovariantDerivativeOn F n (fun (Οƒ : (x : M) β†’ V x) (x : M) => βˆ‘ i ∈ s, f i x β€’ cov i Οƒ x) u

      An affine combination of finitely many C^k connections on u is a C^k connection on u.

      source
      theorem IsCovariantDerivativeOn.add_one_form {π•œ : 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] {s : Set M} {cov : ((x : M) β†’ V x) β†’ (x : M) β†’ TangentSpace I x β†’L[π•œ] V x} (hcov : IsCovariantDerivativeOn F cov s) (A : (x : M) β†’ V x β†’L[π•œ] TangentSpace I x β†’L[π•œ] V x) :
      IsCovariantDerivativeOn F (fun (Οƒ : (x : M) β†’ V x) (x : M) => cov Οƒ x + (A x) (Οƒ x)) s

      Adding a one-form taking values in the endomorphisms of the vector bundle to a covariant derivative gives a covariant derivative.

      source
      noncomputable def IsCovariantDerivativeOn.difference {π•œ : 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 cov' : ((x : M) β†’ V x) β†’ (x : M) β†’ TangentSpace I x β†’L[π•œ] V x} {s : Set M} (hcov : IsCovariantDerivativeOn F cov s) (hcov' : IsCovariantDerivativeOn F cov' s) [CompleteSpace π•œ] [FiniteDimensional π•œ F] [VectorBundle π•œ F V] [ContMDiffVectorBundle 1 F V I] (x : M) :
      V x β†’L[π•œ] TangentSpace I x β†’L[π•œ] V x

      The difference of two covariant derivatives, as a one-form taking values in the endomorphisms of V.

      Equations
      Instances For
        source
        @[simp]
        theorem IsCovariantDerivativeOn.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] {cov cov' : ((x : M) β†’ V x) β†’ (x : M) β†’ TangentSpace I x β†’L[π•œ] V x} {s : Set M} (hcov : IsCovariantDerivativeOn F cov s) (hcov' : IsCovariantDerivativeOn F cov' s) [CompleteSpace π•œ] [FiniteDimensional π•œ F] [VectorBundle π•œ F V] [ContMDiffVectorBundle 1 F V I] {x : M} (hx : x ∈ s := by trivial) {Οƒ : (x : M) β†’ V x} (hΟƒ : MDiffAt (T% Οƒ) x) :
        (hcov.difference hcov' x) (Οƒ x) = cov Οƒ x - cov' Οƒ x

        Bundled global covariant derivatives #

        source
        structure 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] :
        Type (max (max u_2 u_4) u_6)

        Bundled global covariant derivative on a vector bundle. Caution, the argument order is nonstandard: cov Οƒ x (X x) corresponds to βˆ‡_X Οƒ x on paper.

        Instances For
          source
          theorem CovariantDerivative.ext_iff {π•œ : Type u_1} {inst✝ : NontriviallyNormedField π•œ} {E : Type u_2} {inst✝¹ : NormedAddCommGroup E} {inst✝² : NormedSpace π•œ E} {H : Type u_3} {inst✝³ : TopologicalSpace H} {I : ModelWithCorners π•œ E H} {M : Type u_4} {inst✝⁴ : TopologicalSpace M} {inst✝⁡ : ChartedSpace H M} {F : Type u_5} {inst✝⁢ : NormedAddCommGroup F} {inst✝⁷ : NormedSpace π•œ F} {V : M β†’ Type u_6} {inst✝⁸ : TopologicalSpace (Bundle.TotalSpace F V)} {inst✝⁹ : (x : M) β†’ AddCommGroup (V x)} {inst✝¹⁰ : (x : M) β†’ Module π•œ (V x)} {inst✝¹¹ : (x : M) β†’ TopologicalSpace (V x)} {inst✝¹² : βˆ€ (x : M), IsTopologicalAddGroup (V x)} {inst✝¹³ : βˆ€ (x : M), ContinuousSMul π•œ (V x)} {inst✝¹⁴ : FiberBundle F V} {x y : CovariantDerivative I F V} :
          x = y ↔ ↑x = ↑y
          source
          theorem CovariantDerivative.ext {π•œ : Type u_1} {inst✝ : NontriviallyNormedField π•œ} {E : Type u_2} {inst✝¹ : NormedAddCommGroup E} {inst✝² : NormedSpace π•œ E} {H : Type u_3} {inst✝³ : TopologicalSpace H} {I : ModelWithCorners π•œ E H} {M : Type u_4} {inst✝⁴ : TopologicalSpace M} {inst✝⁡ : ChartedSpace H M} {F : Type u_5} {inst✝⁢ : NormedAddCommGroup F} {inst✝⁷ : NormedSpace π•œ F} {V : M β†’ Type u_6} {inst✝⁸ : TopologicalSpace (Bundle.TotalSpace F V)} {inst✝⁹ : (x : M) β†’ AddCommGroup (V x)} {inst✝¹⁰ : (x : M) β†’ Module π•œ (V x)} {inst✝¹¹ : (x : M) β†’ TopologicalSpace (V x)} {inst✝¹² : βˆ€ (x : M), IsTopologicalAddGroup (V x)} {inst✝¹³ : βˆ€ (x : M), ContinuousSMul π•œ (V x)} {inst✝¹⁴ : FiberBundle F V} {x y : CovariantDerivative I F V} (toFun : ↑x = ↑y) :
          x = y
          source
          @[implicit_reducible]
          instance CovariantDerivative.instCoeFunForallForallForallContinuousLinearMapIdTangentSpace {π•œ : 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] :
          CoeFun (CovariantDerivative I F V) fun (x : CovariantDerivative I F V) => ((x : M) β†’ V x) β†’ (x : M) β†’ TangentSpace I x β†’L[π•œ] V x

          Coercion of a CovariantDerivative to function

          Equations
          source
          theorem CovariantDerivative.isCovariantDerivativeOn {π•œ : 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) {s : Set M} :
          IsCovariantDerivativeOn F (↑cov) s
          source
          @[simp]
          theorem CovariantDerivative.zero {π•œ : 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 : CovariantDerivative I F V) :
          ↑cov 0 = 0
          source
          def CovariantDerivative.of_isCovariantDerivativeOn_of_open_cover {π•œ : 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] {ΞΉ : Type u_7} {s : ΞΉ β†’ Set M} {cov : ((x : M) β†’ V x) β†’ (x : M) β†’ TangentSpace I x β†’L[π•œ] V x} (hcov : βˆ€ (i : ΞΉ), IsCovariantDerivativeOn F cov (s i)) (hs : ⋃ (i : ΞΉ), s i = Set.univ) :
          CovariantDerivative I F V

          If cov is a covariant derivative on each set in an open cover, it is a covariant derivative.

          Equations
          Instances For
            source
            @[simp]
            theorem CovariantDerivative.of_isCovariantDerivativeOn_of_open_cover_coe {π•œ : 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] {ΞΉ : Type u_7} {s : ΞΉ β†’ Set M} {cov : ((x : M) β†’ V x) β†’ (x : M) β†’ TangentSpace I x β†’L[π•œ] V x} (hcov : βˆ€ (i : ΞΉ), IsCovariantDerivativeOn F cov (s i)) (hs : ⋃ (i : ΞΉ), s i = Set.univ) :
            ↑(of_isCovariantDerivativeOn_of_open_cover hcov hs) = cov
            source
            class CovariantDerivative.ContMDiffCovariantDerivative {π•œ : 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] [IsManifold I 1 M] [VectorBundle π•œ F V] (cov : CovariantDerivative I F V) (k : WithTop β„•βˆž) :
            Prop

            A covariant derivative βˆ‡ is called of class C^k iff, whenever X is a C^k section and Οƒ a C^{k+1} section, the result βˆ‡_X Οƒ is a C^k section. This is a class so typeclass inference can deduce this automatically. We will prove in a later file that any C^(k+1) covariant derivative is C^k.

            Instances
              source
              @[simp]
              theorem CovariantDerivative.contMDiffCovariantDerivativeOn_univ_iff {π•œ : 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] [IsManifold I 1 M] [VectorBundle π•œ F V] {cov : CovariantDerivative I F V} {k : WithTop β„•βˆž} :
              ContMDiffCovariantDerivativeOn F k (↑cov) Set.univ ↔ cov.ContMDiffCovariantDerivative k

              Operations #

              In this section we prove that:

              Note: morally this means covariant derivatives form an affine space over the vector space of one-forms taking values in the endomorphisms of the bundle, but we don’t package it that way yet.

              source
              def CovariantDerivative.affine_combination {π•œ : 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 cov' : CovariantDerivative I F V) (g : M β†’ π•œ) :
              CovariantDerivative I F V

              An affine combination of covariant derivatives as a covariant derivative.

              Equations
              Instances For
                source
                @[simp]
                theorem CovariantDerivative.affine_combination_toFun {π•œ : 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 cov' : CovariantDerivative I F V) (g : M β†’ π•œ) (Οƒ : (x : M) β†’ V x) (x : M) :
                ↑(cov.affine_combination cov' g) Οƒ x = (g β€’ ↑cov Οƒ + (1 - g) β€’ ↑cov' Οƒ) x
                source
                def CovariantDerivative.finite_affine_combination {π•œ : 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] {ΞΉ : Type u_7} {s : Finset ΞΉ} (cov : ΞΉ β†’ CovariantDerivative I F V) {f : ΞΉ β†’ M β†’ π•œ} (hf : βˆ‘ i ∈ s, f i = 1) :
                CovariantDerivative I F V

                A finite affine combination of covariant derivatives as a covariant derivative.

                Equations
                Instances For
                  source
                  theorem CovariantDerivative.ContMDiffCovariantDerivative.affine_combination {π•œ : 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] [IsManifold I 1 M] [VectorBundle π•œ F V] (cov cov' : CovariantDerivative I F V) {f : M β†’ π•œ} {n : WithTop β„•βˆž} (hf : ContMDiff I (modelWithCornersSelf π•œ π•œ) n f) (hcov : cov.ContMDiffCovariantDerivative n) (hcov' : cov'.ContMDiffCovariantDerivative n) :
                  (cov.affine_combination cov' f).ContMDiffCovariantDerivative n

                  An affine combination of two C^k connections is a C^k connection.

                  source
                  theorem CovariantDerivative.ContMDiffCovariantDerivative.finite_affine_combination {π•œ : 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] [IsManifold I 1 M] [VectorBundle π•œ F V] {ΞΉ : Type u_7} {s : Finset ΞΉ} (cov : ΞΉ β†’ CovariantDerivative I F V) {f : ΞΉ β†’ M β†’ π•œ} (hf : βˆ‘ i ∈ s, f i = 1) {n : WithTop β„•βˆž} (hf' : βˆ€ i ∈ s, ContMDiff I (modelWithCornersSelf π•œ π•œ) n (f i)) (hcov : βˆ€ i ∈ s, (cov i).ContMDiffCovariantDerivative n) :
                  (CovariantDerivative.finite_affine_combination cov hf).ContMDiffCovariantDerivative n

                  An affine combination of finitely many C^k connections is a C^k connection.

                  source
                  def CovariantDerivative.addOneForm {π•œ : 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) :
                  CovariantDerivative I F V

                  Adding a one-form taking values in the endomorphisms of the vector bundle to a covariant derivative gives a covariant derivative.

                  Equations
                  • cov.addOneForm A = { toFun := fun (Οƒ : (x : M) β†’ V x) (x : M) => ↑cov Οƒ x + (A x) (Οƒ x), isCovariantDerivativeOnUniv := β‹― }
                  Instances For
                    source
                    noncomputable def CovariantDerivative.difference {π•œ : 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] [CompleteSpace π•œ] [FiniteDimensional π•œ F] [VectorBundle π•œ F V] [ContMDiffVectorBundle 1 F V I] (cov cov' : CovariantDerivative I F V) (x : M) :
                    V x β†’L[π•œ] TangentSpace I x β†’L[π•œ] V x

                    The difference of two covariant derivatives, as a one-form taking values in the endomorphisms of V.

                    Equations
                    Instances For