Covariant derivatives read in a local frame #
Let V → M be a finite-rank smooth vector bundle and let e be a trivialization of V with
b a basis of the model fibre, so that e.localFrame b is a smooth frame of V over
e.baseSet. This file reads a covariant derivative on V in that frame.
Writing σ = ∑ i, σⁱ • eᵢ over e.baseSet, any covariant derivative ∇ satisfies
∇ σ = ∑ i, dσⁱ ⊗ eᵢ + ∑ i, σⁱ • ∇ eᵢ
on e.baseSet. The first summand is itself a covariant derivative over e.baseSet, the flat
one attached to the frame; it is frameCovariantDerivative, and it witnesses that covariant
derivatives always exist locally. The second summand is tensorial in σ, and is the Christoffel
form christoffelForm of ∇ in the frame: ∇ is the flat derivative plus christoffelForm.
For an arbitrary local frame, IsLocalFrameOn.covariantDerivative_eq_sum gives the same product
rule directly in its native coefficients.
Specializing to the tangent bundle and expanding ∇_{eᵢ} eⱼ again in the frame gives the scalar
Christoffel symbols christoffelSymbol; they are C^∞ on e.baseSet for a C^∞ covariant
derivative, and they give the classical coordinate formula for ∇ σ along a frame direction.
Main definitions and results #
TauCeti.Manifold.frameCovariantDerivative: the flat covariant derivative attached to a local frame, andTauCeti.Manifold.isCovariantDerivativeOn_frameCovariantDerivative, the proof that it is a covariant derivative over the trivialization base set, andTauCeti.Manifold.contMDiffCovariantDerivativeOn_frameCovariantDerivative, its regularity there.TauCeti.Manifold.frameCovariantDerivative_eq_symmL_comp: the flat derivative of a section whose frame coefficients are the coordinates of a model-valued map, andTauCeti.Manifold.frameCovariantDerivative_symmL_const, its vanishing on constant coordinates.TauCeti.Manifold.covariantDerivative_eq_frameCovariantDerivative_add_sum: the local frame formula for an arbitrary covariant derivative.TauCeti.Manifold.covariantDerivative_eq_of_localFrame_eq: two covariant derivatives which agree on the frame sections at a point agree at that point on every section differentiable there.TauCeti.Manifold.christoffelForm: the Christoffel form of a covariant derivative in a local frame, withTauCeti.Manifold.christoffelForm_applycomputing it andTauCeti.Manifold.covariantDerivative_eq_add_christoffelFormexpressing the covariant derivative as the flat one plus it.TauCeti.Manifold.covariantDerivative_symm_eq_christoffelFormandTauCeti.Manifold.covariantDerivative_symm_apply_symm: a covariant derivative differentiates a section with constant coordinates in the trivialization by the Christoffel form, and on the tangent bundle by the Christoffel map.TauCeti.Manifold.covariantDerivative_symm_comp_apply_symm: on the tangent bundle, the covariant derivative of the vector field with coordinatesgin the trivialization has coordinatesdg + Γ(g, ·).TauCeti.Manifold.christoffelSymbol: the scalar Christoffel symbols of a covariant derivative on the tangent bundle in a local frame, withTauCeti.Manifold.covariantDerivative_localFrame_eq_sum_christoffelSymbolexpanding∇_{eᵢ} eⱼ,TauCeti.Manifold.contMDiffOn_christoffelSymboltheir smoothness, andTauCeti.Manifold.christoffelForm_localFrame_applyidentifying them with the frame components of the Christoffel form.TauCeti.Manifold.christoffelMap: the Christoffel form transported to a continuous bilinear map on the model space, withTauCeti.Manifold.christoffelMap_applyreading it back as the Christoffel form andTauCeti.Manifold.contMDiffOn_christoffelMapproving its smoothness.TauCeti.Manifold.covariantDerivative_apply_localFrame_eq_sum: the classical coordinate formula(∇_{eᵢ} σ)ᵏ = dσᵏ(eᵢ) + ∑ j, σʲ Γᵏᵢⱼ.
References #
- M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 2, §2.
- J. M. Lee, Introduction to Riemannian Manifolds, GTM 176, 2018, Ch. 4.
theorem
IsLocalFrameOn.covariantDerivative_eq_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]
{ι : Type u_7}
[Fintype ι]
{s : ι → (x : M) → V x}
{u : Set M}
{x : M}
{n : WithTop ℕ∞}
(hs : IsLocalFrameOn I F n s u)
(hn : 1 ≤ n)
(hu : u ∈ nhds x)
{cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x}
(hcov : IsCovariantDerivativeOn F cov u)
{σ : (x : M) → V x}
(hcoeff : ∀ (i : ι), (MDiffAt fun (y : M) => (hs.coeff i y) (σ y)) x)
:
A covariant derivative in a local frame differentiates the coefficients and the frame sections by the product rule. Only differentiability of the coefficient functions at the point is required.
The flat covariant derivative of a local frame #
noncomputable def
TauCeti.Manifold.frameCovariantDerivative
{𝕜 : 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]
[ContMDiffVectorBundle 1 F V I]
{ι : Type u_7}
[Fintype ι]
(b : Module.Basis ι 𝕜 F)
(e : Bundle.Trivialization F Bundle.TotalSpace.proj)
[MemTrivializationAtlas e]
(σ : (x : M) → V x)
(x : M)
:
The flat covariant derivative attached to the local frame induced by a trivialization e of
V and a basis b of the model fibre: it differentiates the coefficient functions of a section
and keeps the frame fixed. It is a covariant derivative over e.baseSet, by
isCovariantDerivativeOn_frameCovariantDerivative; outside that set it carries a junk value.
Instances For
theorem
TauCeti.Manifold.frameCovariantDerivative_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]
{x : M}
{σ : (x : M) → V x}
[ContMDiffVectorBundle 1 F V I]
{ι : Type u_7}
[Fintype ι]
(b : Module.Basis ι 𝕜 F)
{e : Bundle.Trivialization F Bundle.TotalSpace.proj}
[MemTrivializationAtlas e]
(v : TangentSpace I x)
:
(frameCovariantDerivative I b e σ x) v = ∑ i : ι, (d% ((LinearMap.piApply (Bundle.Trivialization.localFrameCoeff I e b i)) σ) x) v • e.localFrame b i x
The flat covariant derivative of the frame, evaluated on a tangent vector.
theorem
TauCeti.Manifold.frameCovariantDerivative_eq_symmL_comp
{𝕜 : 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}
{σ : (x : M) → V x}
[ContMDiffVectorBundle 1 F V I]
{ι : Type u_7}
[Fintype ι]
(b : Module.Basis ι 𝕜 F)
{e : Bundle.Trivialization F Bundle.TotalSpace.proj}
[MemTrivializationAtlas e]
[CompleteSpace 𝕜]
[FiniteDimensional 𝕜 F]
{g : M → F}
{A : TangentSpace I x →L[𝕜] F}
(hg : HasMFDerivAt% g x A)
(hcoeff :
∀ (i : ι),
(fun (z : M) => (Bundle.Trivialization.localFrameCoeff I e b i z) (σ z)) =ᶠ[nhds x] fun (z : M) =>
(b.coord i) (g z))
(hx : x ∈ e.baseSet)
:
If the coefficients of a section in the frame of e agree near x with the coordinates of a
model-valued map g that has derivative A at x, then its flat frame derivative at x is
e.symmL x ∘ A.
@[simp]
theorem
TauCeti.Manifold.frameCovariantDerivative_symmL_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]
[VectorBundle 𝕜 F V]
{x : M}
[ContMDiffVectorBundle 1 F V I]
{ι : Type u_7}
[Fintype ι]
(b : Module.Basis ι 𝕜 F)
{e : Bundle.Trivialization F Bundle.TotalSpace.proj}
[MemTrivializationAtlas e]
[CompleteSpace 𝕜]
[FiniteDimensional 𝕜 F]
(hx : x ∈ e.baseSet)
(v : F)
:
The section z ↦ e.symmL z v has constant coefficients in the frame of e, so its flat frame
derivative at a point of the base set vanishes.
theorem
TauCeti.Manifold.isCovariantDerivativeOn_frameCovariantDerivative
{𝕜 : 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]
[ContMDiffVectorBundle 1 F V I]
{ι : Type u_7}
[Fintype ι]
(b : Module.Basis ι 𝕜 F)
{e : Bundle.Trivialization F Bundle.TotalSpace.proj}
[MemTrivializationAtlas e]
[CompleteSpace 𝕜]
[FiniteDimensional 𝕜 F]
:
IsCovariantDerivativeOn F (frameCovariantDerivative I b e) e.baseSet
The flat frame derivative satisfies the covariant-derivative axioms on the base set of the trivialization defining the frame.
The local frame formula #
theorem
TauCeti.Manifold.covariantDerivative_eq_frameCovariantDerivative_add_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}
{σ : (x : M) → V x}
{cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x}
[ContMDiffVectorBundle 1 F V I]
{ι : Type u_7}
[Fintype ι]
(b : Module.Basis ι 𝕜 F)
{e : Bundle.Trivialization F Bundle.TotalSpace.proj}
[MemTrivializationAtlas e]
[CompleteSpace 𝕜]
[FiniteDimensional 𝕜 F]
(hcov : IsCovariantDerivativeOn F cov e.baseSet)
(hx : x ∈ e.baseSet)
(hσ : (MDiffAt fun (x : M) => ⟨x, σ x⟩) x)
:
cov σ x = frameCovariantDerivative I b e σ x + ∑ i : ι, (Bundle.Trivialization.localFrameCoeff I e b i x) (σ x) • cov (e.localFrame b i) x
The local frame formula: over the base set of a trivialization, a covariant derivative is the flat derivative of the frame coefficients plus the coefficients times the covariant derivatives of the frame sections.
theorem
TauCeti.Manifold.covariantDerivative_eq_of_localFrame_eq
{𝕜 : 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}
{σ : (x : M) → V x}
{cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x}
[ContMDiffVectorBundle 1 F V I]
{ι : Type u_7}
(b : Module.Basis ι 𝕜 F)
{e : Bundle.Trivialization F Bundle.TotalSpace.proj}
[MemTrivializationAtlas e]
[CompleteSpace 𝕜]
[FiniteDimensional 𝕜 F]
[Finite ι]
{cov' : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x}
(hcov : IsCovariantDerivativeOn F cov e.baseSet)
(hcov' : IsCovariantDerivativeOn F cov' e.baseSet)
(hx : x ∈ e.baseSet)
(hframe : ∀ (i : ι), cov (e.localFrame b i) x = cov' (e.localFrame b i) x)
(hσ : (MDiffAt fun (x : M) => ⟨x, σ x⟩) x)
:
Two covariant derivatives over the base set of a trivialization which agree on the frame sections at a point agree there on every section differentiable at that point.
The Christoffel form #
noncomputable def
TauCeti.Manifold.christoffelForm
{𝕜 : 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}
[ContMDiffVectorBundle 1 F V I]
{ι : Type u_7}
[Fintype ι]
(b : Module.Basis ι 𝕜 F)
{e : Bundle.Trivialization F Bundle.TotalSpace.proj}
[MemTrivializationAtlas e]
[CompleteSpace 𝕜]
[FiniteDimensional 𝕜 F]
(hcov : IsCovariantDerivativeOn F cov e.baseSet)
(x : M)
:
The Christoffel form of a covariant derivative in a local frame: the endomorphism-valued
one-form by which the covariant derivative differs from the flat derivative
frameCovariantDerivative of the frame.
Instances For
theorem
TauCeti.Manifold.covariantDerivative_eq_add_christoffelForm
{𝕜 : 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}
{σ : (x : M) → V x}
{cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x}
[ContMDiffVectorBundle 1 F V I]
{ι : Type u_7}
[Fintype ι]
(b : Module.Basis ι 𝕜 F)
{e : Bundle.Trivialization F Bundle.TotalSpace.proj}
[MemTrivializationAtlas e]
[CompleteSpace 𝕜]
[FiniteDimensional 𝕜 F]
(hcov : IsCovariantDerivativeOn F cov e.baseSet)
(hx : x ∈ e.baseSet)
(hσ : (MDiffAt fun (x : M) => ⟨x, σ x⟩) x)
:
A covariant derivative is the flat derivative of its frame plus its Christoffel form.
theorem
TauCeti.Manifold.christoffelForm_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]
{x : M}
{cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x}
[ContMDiffVectorBundle 1 F V I]
{ι : Type u_7}
[Fintype ι]
(b : Module.Basis ι 𝕜 F)
{e : Bundle.Trivialization F Bundle.TotalSpace.proj}
[MemTrivializationAtlas e]
[CompleteSpace 𝕜]
[FiniteDimensional 𝕜 F]
(hcov : IsCovariantDerivativeOn F cov e.baseSet)
(hx : x ∈ e.baseSet)
(v : V x)
:
(christoffelForm b hcov x) v = ∑ i : ι, (Bundle.Trivialization.localFrameCoeff I e b i x) v • cov (e.localFrame b i) x
The Christoffel form is the frame expansion of the covariant derivatives of the frame sections.
theorem
TauCeti.Manifold.covariantDerivative_symm_eq_christoffelForm
{𝕜 : 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}
[ContMDiffVectorBundle 1 F V I]
{ι : Type u_7}
[Fintype ι]
(b : Module.Basis ι 𝕜 F)
{e : Bundle.Trivialization F Bundle.TotalSpace.proj}
[MemTrivializationAtlas e]
[CompleteSpace 𝕜]
[FiniteDimensional 𝕜 F]
(hcov : IsCovariantDerivativeOn F cov e.baseSet)
(hx : x ∈ e.baseSet)
(v : F)
:
A covariant derivative differentiates the section with constant coordinates v in the
trivialization e by its Christoffel form: the flat derivative of such a section vanishes.
Regularity of the flat covariant derivative of a local frame #
theorem
TauCeti.Manifold.contMDiffCovariantDerivativeOn_frameCovariantDerivative
{𝕜 : 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]
[ContMDiffVectorBundle 1 F V I]
{ι : Type u_7}
[Fintype ι]
(b : Module.Basis ι 𝕜 F)
{e : Bundle.Trivialization F Bundle.TotalSpace.proj}
[MemTrivializationAtlas e]
[CompleteSpace 𝕜]
[FiniteDimensional 𝕜 F]
[FiniteDimensional 𝕜 E]
{m k n : WithTop ℕ∞}
[IsManifold I m M]
[ContMDiffVectorBundle k F V I]
(hm : n + 1 ≤ m)
(hk : n + 1 ≤ k)
:
ContMDiffCovariantDerivativeOn F n (frameCovariantDerivative I b e) e.baseSet
The flat covariant derivative of a local frame is C^n on the base set of the trivialization
defining the frame, on a C^m manifold and a C^k bundle with n + 1 ≤ m and n + 1 ≤ k: it
sends a section which is C^(n + 1) there to a C^n section of Hom(TM, V) there.
Christoffel symbols on the tangent bundle #
noncomputable def
TauCeti.Manifold.christoffelSymbol
{𝕜 : 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]
[IsManifold I 1 M]
[ContMDiffVectorBundle 1 E (TangentSpace I) I]
{ι : Type u_5}
(b : Module.Basis ι 𝕜 E)
(e : Bundle.Trivialization E Bundle.TotalSpace.proj)
[MemTrivializationAtlas e]
(cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x)
(i j k : ι)
(x : M)
:
𝕜
The Christoffel symbols of a covariant derivative on the tangent bundle, in the local frame
induced by a trivialization e and a basis b of the model space: christoffelSymbol I b e cov i j k x is the k-th coefficient of ∇_{eᵢ} eⱼ at x. Outside e.baseSet it carries a junk
value.
Instances For
@[simp]
theorem
TauCeti.Manifold.christoffelSymbol_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]
[IsManifold I 1 M]
[ContMDiffVectorBundle 1 E (TangentSpace I) I]
{ι : Type u_5}
(b : Module.Basis ι 𝕜 E)
{e : Bundle.Trivialization E Bundle.TotalSpace.proj}
[MemTrivializationAtlas e]
{x : M}
{cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x}
(i j k : ι)
:
christoffelSymbol I b e cov i j k x = (Bundle.Trivialization.localFrameCoeff I e b k x) ((cov (e.localFrame b j) x) (e.localFrame b i x))
The defining formula for the Christoffel symbols.
theorem
TauCeti.Manifold.covariantDerivative_localFrame_eq_sum_christoffelSymbol
{𝕜 : 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]
[IsManifold I 1 M]
[ContMDiffVectorBundle 1 E (TangentSpace I) I]
{ι : Type u_5}
(b : Module.Basis ι 𝕜 E)
{e : Bundle.Trivialization E Bundle.TotalSpace.proj}
[MemTrivializationAtlas e]
{x : M}
{cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x}
[Fintype ι]
(hx : x ∈ e.baseSet)
(i j : ι)
:
(cov (e.localFrame b j) x) (e.localFrame b i x) = ∑ k : ι, christoffelSymbol I b e cov i j k x • e.localFrame b k x
The Christoffel symbols expand the covariant derivative of a frame section along a frame direction back in the frame.
noncomputable def
TauCeti.Manifold.christoffelMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[FiniteDimensional 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 1 M]
[ContMDiffVectorBundle 1 E (TangentSpace I) I]
{ι : Type u_5}
(b : Module.Basis ι 𝕜 E)
{e : Bundle.Trivialization E Bundle.TotalSpace.proj}
[MemTrivializationAtlas e]
{cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x}
[Fintype ι]
(hcov : IsCovariantDerivativeOn E cov e.baseSet)
(x : M)
:
The Christoffel form transported through the tangent-bundle trivialization to a model-space-valued continuous bilinear map.
Instances For
theorem
TauCeti.Manifold.christoffelMap_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[FiniteDimensional 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 1 M]
[ContMDiffVectorBundle 1 E (TangentSpace I) I]
{ι : Type u_5}
(b : Module.Basis ι 𝕜 E)
{e : Bundle.Trivialization E Bundle.TotalSpace.proj}
[MemTrivializationAtlas e]
{x : M}
{cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x}
[Fintype ι]
(hcov : IsCovariantDerivativeOn E cov e.baseSet)
(hx : x ∈ e.baseSet)
(v w : E)
:
((christoffelMap b hcov x) v) w = (Bundle.Trivialization.continuousLinearMapAt 𝕜 e x)
(((christoffelForm b hcov x) ((Bundle.Trivialization.symmL 𝕜 e x) v)) ((Bundle.Trivialization.symmL 𝕜 e x) w))
The model-space Christoffel map is the Christoffel form read in the trivialization: it acts on the coordinates of a fibre vector and of a tangent direction, and returns the coordinates of the value of the Christoffel form on them.
theorem
TauCeti.Manifold.covariantDerivative_symm_apply_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[FiniteDimensional 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 1 M]
[ContMDiffVectorBundle 1 E (TangentSpace I) I]
{ι : Type u_5}
(b : Module.Basis ι 𝕜 E)
{e : Bundle.Trivialization E Bundle.TotalSpace.proj}
[MemTrivializationAtlas e]
{x : M}
{cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x}
[Fintype ι]
(hcov : IsCovariantDerivativeOn E cov e.baseSet)
(hx : x ∈ e.baseSet)
(v u : E)
:
A covariant derivative on the tangent bundle differentiates the vector field with constant
coordinates v in the trivialization e, in the direction with coordinates u, by the Christoffel
map: the result has coordinates christoffelMap b hcov x v u.
theorem
TauCeti.Manifold.covariantDerivative_symm_comp_apply_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[FiniteDimensional 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 1 M]
[ContMDiffVectorBundle 1 E (TangentSpace I) I]
{ι : Type u_5}
(b : Module.Basis ι 𝕜 E)
{e : Bundle.Trivialization E Bundle.TotalSpace.proj}
[MemTrivializationAtlas e]
{x : M}
{cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x}
[Fintype ι]
(hcov : IsCovariantDerivativeOn E cov e.baseSet)
(hx : x ∈ e.baseSet)
{g : M → E}
(hg : MDiffAt g x)
(u : E)
:
The coordinate formula for a covariant derivative on the tangent bundle. The covariant
derivative of the vector field with coordinates g in the trivialization e, in the direction
with coordinates u, has coordinates dg(u) + Γ(g, u), where Γ is the Christoffel map.
theorem
TauCeti.Manifold.contMDiffOn_christoffelSymbol
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[FiniteDimensional 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 1 M]
[ContMDiffVectorBundle 1 E (TangentSpace I) I]
{ι : Type u_5}
(b : Module.Basis ι 𝕜 E)
{e : Bundle.Trivialization E Bundle.TotalSpace.proj}
[MemTrivializationAtlas e]
{cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x}
{n : WithTop ℕ∞}
[ContMDiffVectorBundle n E (TangentSpace I) I]
[ContMDiffVectorBundle (n + 1) E (TangentSpace I) I]
[ContMDiffCovariantDerivativeOn E n cov e.baseSet]
(i j k : ι)
:
ContMDiffOn I (modelWithCornersSelf 𝕜 𝕜) n (christoffelSymbol I b e cov i j k) e.baseSet
The Christoffel symbols of a C^n covariant derivative are C^n on the base set of the
trivialization defining the frame.
theorem
TauCeti.Manifold.christoffelForm_localFrame_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[FiniteDimensional 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 1 M]
[ContMDiffVectorBundle 1 E (TangentSpace I) I]
{ι : Type u_5}
(b : Module.Basis ι 𝕜 E)
{e : Bundle.Trivialization E Bundle.TotalSpace.proj}
[MemTrivializationAtlas e]
{x : M}
{cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x}
[Fintype ι]
(hcov : IsCovariantDerivativeOn E cov e.baseSet)
(hx : x ∈ e.baseSet)
(i j : ι)
:
((christoffelForm b hcov x) (e.localFrame b j x)) (e.localFrame b i x) = ∑ k : ι, christoffelSymbol I b e cov i j k x • e.localFrame b k x
The frame components of the Christoffel form are the Christoffel symbols.
@[simp]
theorem
TauCeti.Manifold.christoffelMap_apply_basis
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[FiniteDimensional 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 1 M]
[ContMDiffVectorBundle 1 E (TangentSpace I) I]
{ι : Type u_5}
(b : Module.Basis ι 𝕜 E)
{e : Bundle.Trivialization E Bundle.TotalSpace.proj}
[MemTrivializationAtlas e]
{x : M}
{cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x}
[Fintype ι]
(hcov : IsCovariantDerivativeOn E cov e.baseSet)
(hx : x ∈ e.baseSet)
(i j : ι)
:
The basis coefficients of the model-space Christoffel map are the scalar Christoffel symbols.
theorem
TauCeti.Manifold.coord_christoffelMap_apply_basis
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[FiniteDimensional 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 1 M]
[ContMDiffVectorBundle 1 E (TangentSpace I) I]
{ι : Type u_5}
(b : Module.Basis ι 𝕜 E)
{e : Bundle.Trivialization E Bundle.TotalSpace.proj}
[MemTrivializationAtlas e]
{x : M}
{cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x}
[Fintype ι]
(hcov : IsCovariantDerivativeOn E cov e.baseSet)
(hx : x ∈ e.baseSet)
(i j k : ι)
:
The scalar basis coefficients of the model-space Christoffel map are precisely the Christoffel symbols.
theorem
TauCeti.Manifold.contMDiffOn_christoffelMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[FiniteDimensional 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 1 M]
[ContMDiffVectorBundle 1 E (TangentSpace I) I]
{ι : Type u_5}
(b : Module.Basis ι 𝕜 E)
{e : Bundle.Trivialization E Bundle.TotalSpace.proj}
[MemTrivializationAtlas e]
{cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x}
[Fintype ι]
{n : WithTop ℕ∞}
(hcov : IsCovariantDerivativeOn E cov e.baseSet)
[ContMDiffVectorBundle n E (TangentSpace I) I]
[ContMDiffVectorBundle (n + 1) E (TangentSpace I) I]
[ContMDiffCovariantDerivativeOn E n cov e.baseSet]
:
ContMDiffOn I (modelWithCornersSelf 𝕜 (E →L[𝕜] E →L[𝕜] E)) n (christoffelMap b hcov) e.baseSet
The model-space Christoffel map of a C^n covariant derivative is C^n on the base set of
the trivialization defining its coordinates.
theorem
TauCeti.Manifold.covariantDerivative_apply_localFrame_eq_sum
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[FiniteDimensional 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 1 M]
[ContMDiffVectorBundle 1 E (TangentSpace I) I]
{ι : Type u_5}
(b : Module.Basis ι 𝕜 E)
{e : Bundle.Trivialization E Bundle.TotalSpace.proj}
[MemTrivializationAtlas e]
{x : M}
{cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x}
{σ : (x : M) → TangentSpace I x}
[Fintype ι]
(hcov : IsCovariantDerivativeOn E cov e.baseSet)
(hx : x ∈ e.baseSet)
(hσ : (MDiffAt fun (x : M) => ⟨x, σ x⟩) x)
(i : ι)
:
(cov σ x) (e.localFrame b i x) = ∑ k : ι,
((d% ((LinearMap.piApply (Bundle.Trivialization.localFrameCoeff I e b k)) σ) x) (e.localFrame b i x) + ∑ j : ι, (Bundle.Trivialization.localFrameCoeff I e b j x) (σ x) * christoffelSymbol I b e cov i j k x) • e.localFrame b k x
The classical coordinate formula for a covariant derivative on the tangent bundle: along the
frame direction eᵢ, the k-th component of ∇ σ is the derivative of the k-th coefficient of
σ plus the Christoffel contraction ∑ j, σʲ Γᵏᵢⱼ.