Physicslib4.Geometry.PseudoRiemannian.Flat

The flat connection on a vector space

On a finite-dimensional real vector space E, viewed as a manifold over itself, the tangent bundle is trivial and the ordinary directional derivative ∇_v σ = Dσ(v) is a covariant derivative. For a pseudo-Riemannian metric that is constant (the same bilinear form at every point), it is the Levi-Civita connection. This is the flat case used for Minkowski spacetime.

Main definitions

• Physicslib4.Geometry.flatConnection: σ ↦ (x ↦ fderiv ℝ σ x).

Main results

• PseudoRiemannianMetric.isLeviCivitaFor_flatConnection: for a constant metric, the flat connection is a Levi-Civita connection.
• PseudoRiemannianMetric.leviCivita_apply_eq_fderiv: hence the Levi-Civita connection of a constant metric is the directional derivative on differentiable vector fields.

Blueprint reference: lmm:minkowski-directional-derivative-levi-civita, lmm:minkowski-levi-civita-flat.

theorem Physicslib4.Geometry.isCovariantDerivativeOn_fderiv (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] : IsCovariantDerivativeOn E fun (σ : (x : E) → TangentSpace (modelWithCornersSelf ℝ E) x) (x : E) => fderiv ℝ (fun (y : TangentSpace (modelWithCornersSelf ℝ E) x) => σ y) x

The directional derivative is a covariant derivative on the tangent bundle of E.

Blueprint reference: lmm:minkowski-directional-derivative-levi-civita.

noncomputable def Physicslib4.Geometry.flatConnection (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] : CovariantDerivative (modelWithCornersSelf ℝ E) E (TangentSpace (modelWithCornersSelf ℝ E))

The flat connection on a vector space E: the ordinary directional derivative, ∇_v σ = Dσ(v).

On E viewed as a manifold over itself the tangent bundle is trivial, and differentiating the components of a vector field is a covariant derivative (isCovariantDerivativeOn_fderiv); all its Christoffel symbols vanish. For a metric that is the same bilinear form at every point, such as the Minkowski metric, it is the Levi-Civita connection (isLeviCivitaFor_flatConnection), so the geodesics of Minkowski spacetime are the straight lines traversed at constant velocity.

Blueprint: lmm:minkowski-directional-derivative-levi-civita

Equations

• One or more equations did not get rendered due to their size.

theorem Physicslib4.Geometry.flatConnection_apply (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] (σ : (x : E) → TangentSpace (modelWithCornersSelf ℝ E) x) (x : E) (v : TangentSpace (modelWithCornersSelf ℝ E) x) : (↑(flatConnection E) σ x) v = (fderiv ℝ (fun (y : E) => σ y) x) v

theorem Physicslib4.Geometry.PseudoRiemannianMetric.isLeviCivitaFor_flatConnection {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (g : PseudoRiemannianMetric (modelWithCornersSelf ℝ E) E) (B : E →L[ℝ] E →L[ℝ] ℝ) (hg : ∀ (x : E), g.val x = B) : CovariantDerivative.IsLeviCivitaFor g (flatConnection E)

For a metric that is the same bilinear form B at every point, the flat connection is a Levi-Civita connection.

Blueprint reference: lmm:minkowski-directional-derivative-levi-civita.

theorem Physicslib4.Geometry.PseudoRiemannianMetric.leviCivita_apply_eq_fderiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (g : PseudoRiemannianMetric (modelWithCornersSelf ℝ E) E) (B : E →L[ℝ] E →L[ℝ] ℝ) (hg : ∀ (x : E), g.val x = B) {X : (x : E) → TangentSpace (modelWithCornersSelf ℝ E) x} {x : E} (hX : (MDiffAt fun (x : E) => ⟨x, X x⟩) x) (v : TangentSpace (modelWithCornersSelf ℝ E) x) : (↑g.leviCivita X x) v = (fderiv ℝ (fun (y : E) => X y) x) v

The Levi-Civita connection of a constant metric is flat: on vector fields differentiable at x, it is the directional derivative.

Blueprint reference: lmm:minkowski-levi-civita-flat.