feat: metric connections#36299
Conversation
Extend an element of a fiber at a point to a local section.
We define the torsion tensor of an affine connection, i.e. a covariant derivative on the tangent bundle `TM` of some manifold `M`.
TODO: file is still unreviewed; will need further tweaks
PR summary de8a06c8fdImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
|
This pull request has conflicts, please merge |
|
This PR/issue depends on: |
We never unbundled the normed and algebra hierarchies, and this is causing performance problems in leanprover-community#36299 and friends. Try if lowering the respective instance priorities helps.
|
!bench |
|
Benchmark results for 49bf82d against de8a06c are in. There are no significant changes. @grunweg
Small changes (2🟥)
and 1 hidden |
|
Let's try the effect of the commit I just pushed. (I know locally that it helps, let's see how much.) |
|
!bench |
|
Benchmark results for 2f1bbfe against de8a06c are in. There are no significant changes. @grunweg
Small changes (2🟥)
and 1 hidden |
|
26% faster, not bad! |
|
|
||
| ## Main definitions and results | ||
|
|
||
| * `CovariantDerivative.compatibilityTensor`: the tensor |
There was a problem hiding this comment.
I am not convinced by this name, because nothing says it's about metrics. Compatibility of covariant derivatives and other objects can make sense, so the name should be more specific.
| ## Main definitions and results | ||
|
|
||
| * `CovariantDerivative.compatibilityTensor`: the tensor | ||
| `(X, σ, τ) ↦ X g(σ, τ) - g(∇_X σ, τ) - g(σ, ∇_X τ)` defining when a connection `∇` on a Riemannian |
There was a problem hiding this comment.
Here you're writing the first derivative as X ..., 6 lines above you write it as ∇_X. You could also use L_X to emphasize it's the usual derivative of a genuine function with respect to the vector field, no bundles or connections involved.
|
|
||
| A connection on `V` is compatible with the metric on `V` iff `X ⟨σ, τ⟩ = ⟨∇_X σ, τ⟩ + ⟨σ, ∇_X τ⟩` | ||
| holds for all sufficiently nice vector fields `X` on `M` and sections `σ`, `τ` of `V`. | ||
| The left hand side is the pushforward of the function `⟨σ, τ⟩` along the vector field `X`: |
There was a problem hiding this comment.
pushforward sounds strange to me here.
| -- set_option profiler.threshold 500 | ||
|
|
||
| /-- The scalar product of two sections. -/ | ||
| noncomputable abbrev product (σ τ : Π x : M, V x) : M → ℝ := |
There was a problem hiding this comment.
Do you really want to introduce a new definition, that will then be available throughout Mathlib for everyone? Wouldn't a notation local to the file make more sense?
|
I've just pushed a change with the correct |
|
Thanks a lot! Let's see what the benchmark says, for posterity. |
|
!bench |
|
Benchmark results for a2e9ee1 against de8a06c are in. There are no significant changes. @grunweg
Small changes (3✅, 1🟥)
|
| The left hand side is the pushforward of the function `⟨σ, τ⟩` along the vector field `X`: | ||
| the left hand side at `x` is `df(X x)`, where `f := ⟨σ, τ⟩` (ie. `X` is seen a derivation on | ||
| the algebra of function on the base manifold acting on the function `⟨σ, τ⟩`). | ||
| In our definition, we ask for this identity to at each `x : M`, whenever `X`, `σ` and `τ` are |
There was a problem hiding this comment.
| In our definition, we ask for this identity to at each `x : M`, whenever `X`, `σ` and `τ` are | |
| In our definition, we ask for this identity to hold at each `x : M`, whenever `X`, `σ` and `τ` are |
|
|
This file defines what it means for a connection on a Riemannian vector bundle
(V, g)to be compatible with the metricg. Namely, the differentiated metric tensor∇ g(defined by(X, σ, τ) ↦ X g(σ, τ) - g(∇_X σ, τ) - g(σ, ∇_X τ)) should vanish on all differentiable vector fieldsXand differentiable sectionsσ,τ.From the path towards the the Levi-Civita connection and Riemannian geometry.
Co-authored-by: Heather Macbeth 25316162+hrmacbeth@users.noreply.github.com
Co-authored-by: Patrick Massot patrickmassot@free.fr
WIP: some API issues need to be decided, some slow proofs need to be diagnosed, some documentation needs to be improved, and may adjust variable names/ theorem names/notation.