WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Covariant derivative

Revision #1132 → #2456 · back to history

modifiedCovariant derivative (lead)f68b76a0ef43
FieldFrom #1132To #2456
mathlib.decl—CovariantDerivative
mathlib.match_kind—generalization
mathlib.module—Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
note—Mathlib's `CovariantDerivative` structure defines a bundled Koszul connection on an arbitrary vector bundle, generalizing the tangent-bundle case in the lead.
status—formalized
modifiedCovariant transformation law0a65faf04e40
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib's covariant derivative is coordinate-free; there is no lemma stating the transformation law of Christoffel symbols under coordinate changes.
status—not_formalized
modifiedCovariant derivative as a rule on vectors and vector fields1ea0ee677eed
FieldFrom #1132To #2456
mathlib.decl—IsCovariantDerivativeOn
mathlib.match_kind—exact
mathlib.module—Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
note—`IsCovariantDerivativeOn` axiomatizes the rule assigning to a section `σ` and vector `X x` the vector `∇_X σ x`, matching the informal rule-based definition.
status—formalized
modifiedParticle in polar coordinates8cbd812bd5ac
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—This motivating physics example (acceleration in polar coordinates) is not formalized in Mathlib.
status—not_formalized
modifiedParallel transport on a globefcd36349edb8
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Parallel transport itself is absent from Mathlib, so this expository example on the sphere is not formalized.
status—not_formalized
addedInfinitesimal parallel transport measures curvature4c69947049aa
modifiedExistence of Levi-Civita connectionba8068f1ec35
FieldFrom #1132To #2456
mathlib.decl—CovariantDerivative.IsMetricCompatible
mathlib.match_kind——
mathlib.module—Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric
note—Mathlib has `IsMetricCompatible` and `CovariantDerivative.torsion`, but the existence/uniqueness theorem for the Levi-Civita connection itself is not yet proved.
status—partial
modifiedLocality of covariant derivative7356b0a115fa
FieldFrom #1132To #2456
mathlib.decl—IsCovariantDerivativeOn.congr_of_eventuallyEq
mathlib.match_kind—exact
mathlib.module—Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
note—`congr_of_eventuallyEq` proves `cov σ x = cov σ' x` when `σ` and `σ'` agree on a neighborhood of `x`, i.e. `∇σ` depends only on the germ.
status—formalized
modifiedEmbedding setup for covariant derivative5caf4129eff3
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib takes an intrinsic vector-bundle approach; the concrete embedded-submanifold-in-ℝⁿ setup used here is not developed.
status—not_formalized
modifiedDecomposition via Christoffel symbols0a34316c3b78
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Christoffel symbols are not defined in Mathlib.
status—not_formalized
modifiedLevi-Civita covariant derivative as orthogonal projection6614c893c4ab
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The extrinsic tangential-projection construction of the Levi-Civita connection is not in Mathlib.
status—not_formalized
modifiedChristoffel symbols in terms of the metricd3b1f0fcb0cf
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Koszul-type formula expressing Christoffel symbols via metric derivatives is not formalized.
status—not_formalized
modifiedCircle rolled into a cylinder37a18a5a4693
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—This illustrative example is not in Mathlib.
status—not_formalized
modifiedCovariant derivative as a Koszul connectioneac834db4f90
FieldFrom #1132To #2456
mathlib.decl—CovariantDerivative
mathlib.match_kind—generalization
mathlib.module—Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
note—The docstring of `CovariantDerivative` explicitly calls it a Koszul connection, defined on any vector bundle (thus generalizing the tangent-bundle case).
status—formalized
addedCompatibility with tensor product and trace5170549004cb
modifiedCovariant derivative of a functione0aeb7a63ad9
FieldFrom #1132To #2456
mathlib.decl—mfderiv
mathlib.match_kind——
mathlib.module—Mathlib.Geometry.Manifold.MFDeriv.Basic
note—Mathlib's `mfderiv` gives the differential of a function on a manifold, which coincides with the covariant derivative on functions, but is not packaged under that name.
status—partial
modifiedCovariant derivative of f along a vector fielda84a815e6416
FieldFrom #1132To #2456
mathlib.decl—mfderiv
mathlib.match_kind——
mathlib.module—Mathlib.Geometry.Manifold.MFDeriv.Basic
note—This is `x ↦ mfderiv I 𝓘(𝕜) f x (X x)` in Mathlib, but there is no dedicated declaration for the pointwise-along-a-vector-field construction.
status—partial
modifiedEquality with Lie and exterior derivative on functionsc5ce29ddd98e
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib lacks a defined Lie derivative on scalar functions and any statement equating it with the covariant/exterior derivative on functions.
status—not_formalized
modifiedCovariant derivative of a vector field9709a091e040
FieldFrom #1132To #2456
mathlib.decl—CovariantDerivative
mathlib.match_kind—special_case
mathlib.module—Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
note—Taking `V = TangentSpace I` in `CovariantDerivative I E V` gives the covariant derivative of a vector field along another; `cov σ x (X x)` corresponds to `∇_X σ x`.
status—formalized
addedLeibniz (product) rule for covariant derivative8377e153d5d1
modifiedDependence on a neighborhood1b97a4fa0e9c
FieldFrom #1132To #2456
mathlib.decl—IsCovariantDerivativeOn.congr_of_eventuallyEq
mathlib.match_kind—exact
mathlib.module—Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
note—The proved germ-locality lemma `congr_of_eventuallyEq` captures dependence only on a neighborhood of the point.
status—formalized
modifiedCovariant derivative of a vector field on a domain3ae0f4edb9f4
FieldFrom #1132To #2456
mathlib.decl—IsCovariantDerivativeOn
mathlib.match_kind—exact
mathlib.module—Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
note—`IsCovariantDerivativeOn` takes a set parameter `s : Set M`, giving a covariant-derivative rule restricted to a domain.
status—formalized
modifiedCovariant derivative of a covector field6fe3a9c32585
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib does not define the induced covariant derivative on the cotangent bundle.
status—not_formalized
modifiedCovariant derivative of covector is covector8d6af362e6e7
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No covector-field covariant derivative is defined, so its type-preserving property is not stated.
status—not_formalized
modifiedCovariant derivative of a tensor field523e3f0d0a08
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The extension of the covariant derivative to general tensor fields via tensor-product and trace compatibility is not in Mathlib.
status—not_formalized
modifiedExplicit formula for covariant derivative of tensor1ead24c92896
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No such coordinate formula exists in Mathlib.
status—not_formalized
modifiedConnection coefficients (Christoffel symbols)2842d021f586
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Christoffel symbols / connection coefficients are not defined in Mathlib.
status—not_formalized
modifiedCoordinate formula for covariant derivative of vector field464b684e2229
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No index-formula `(∇_j v)^i = ∂_j v^i + Γ^i_{jk} v^k` is present in Mathlib.
status—not_formalized
modifiedCoordinate formula for covectors3b055885bb68
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No coordinate formula for covariant derivatives of covector fields is in Mathlib.
status—not_formalized
modifiedCoordinate formula for tensor fieldse54e09ce4a4e
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No general (r,s)-tensor coordinate formula is present in Mathlib.
status—not_formalized
modifiedTensor density correction term45af55ccb801
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Tensor densities are not treated in Mathlib.
status—not_formalized
modifiedDeterminant of metric as scalar density7237b480a76f
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The weight-1 scalar density from `det g` is not formalized.
status—not_formalized
modifiedSemicolon/comma notationaf2f93915dbd
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The classical `T^i_{;j}` / `T^i_{,j}` index notation is not adopted in Mathlib.
status—not_formalized
modifiedMultiple semicolon indices350c0c6c6f0e
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Iterated-semicolon notation is a syntactic convention absent from Mathlib.
status—not_formalized
modifiedDouble pipe notation (Adler, Bazin & Schiffer)964e30aa20c3
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Alternative double-pipe notation is not adopted.
status—not_formalized
modifiedCovariant derivative of a scalar field6442b00d9108
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has `mfderiv` for functions but no statement identifying the covariant derivative of a scalar with partial differentiation in coordinates.
status—not_formalized
modifiedCovariant derivative of a contravariant vector field0a32f0026175
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No coordinate-index expansion of `∇_μ T^ν` is available.
status—not_formalized
modifiedCovariant derivative of a covariant vector field23fe8b0faaa8
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No coordinate expression for `∇_μ T_ν` in Mathlib.
status—not_formalized
modifiedCovariant derivative of a (2,0) tensor field3416a05c7328
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Coordinate formula for `∇_μ T^{αβ}` is not formalized.
status—not_formalized
modifiedCovariant derivative of a (0,2) tensor field84273168669e
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Coordinate formula for `∇_μ T_{αβ}` is not formalized.
status—not_formalized
modifiedCovariant derivative of a (1,1) tensor field242abefad399
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Coordinate formula for `∇_μ T^α_β` is not formalized.
status—not_formalized
modifiedRiemann tensor via commutator of covariant derivativesb2742fc6b57d
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Riemann curvature tensor is not defined in Mathlib.
status—not_formalized
modifiedCommutator on (2,0)-tensor field4567372ff3c4
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Without a Riemann tensor, the Ricci identity for (2,0) tensor commutators is absent.
status—not_formalized
modifiedCovariant derivative along a smooth curve5ed9235452f4
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib does not define the covariant derivative operator `D/dt` acting on curves' vector fields.
status—not_formalized
modifiedGeodesic of the covariant derivative95c26211ef49
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Geodesics of a connection are not defined in Mathlib.
status—not_formalized
modifiedGeodesics of Levi-Civita are metric geodesics4340bf109e09
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Neither Levi-Civita geodesics nor Riemannian metric geodesics are available in Mathlib's manifold library.
status—not_formalized
modifiedAbsolute/intrinsic derivatived1fe1cdced05
FieldFrom #1132To #2456
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—An alternate name for the (unformalized) covariant derivative along a curve.
status—not_formalized
modifiedAntisymmetrized covariant derivative vs Lie derivative637225fa5198
FieldFrom #1132To #2456
mathlib.decl—CovariantDerivative.torsion_eq_zero_iff
mathlib.match_kind——
mathlib.module—Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
note—`torsion_eq_zero_iff` states `∇_X Y − ∇_Y X = [X,Y]` iff torsion vanishes, which is the torsion-free case of the antisymmetrized-covariant-vs-Lie identity, but the general formula with a torsion term is not stated.
status—partial