feat: extend a tangent vector for a locally smooth vector field#30339
feat: extend a tangent vector for a locally smooth vector field#30339grunweg wants to merge 12 commits intoleanprover-community:masterfrom
Conversation
PR summary 0b5d4bb20cImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
|
This pull request has conflicts, please merge |
47e04b3 to
4f981df
Compare
10104f6 to
ca31502
Compare
ca31502 to
b373e3c
Compare
|
This pull request has conflicts, please merge |
0d5e415 to
42a27cb
Compare
64e3089 to
88bfdc2
Compare
|
This PR/issue depends on:
|
|
This pull request has conflicts, please merge |
88bfdc2 to
c8081dc
Compare
|
@ocfnash Would you also like to take a look at the next piece in the local frames saga? |
|
@grunweg Yes of course happy to review: should I wait for the WIP label to disappear or look already tomorrow? |
|
Oh, I wasn't aware that label was still present. I do have three higher-level questions (which are also in the PR description) --- depending on their answer, this PR will become WIP again --- but otherwise, this is ready for a look. |
| The details of this extension are unspecified (and could be subject to change). | ||
| Currently, we construct this extension using a local frame induced by a choose of basis of the | ||
| fibre `F` and a compatible trivialisation `e` of `V` around `x`. | ||
| (Allowing any local frame near `x` would be easy to implement.) | ||
| Our construction has constant coefficients on `e.baseSet` w.r.t. this local frame, and is zero | ||
| otherwise. In particular, it is smooth on `e.baseSet`, and (globally) linear in `v`. |
There was a problem hiding this comment.
Given this, I tend to think we should make this an existential lemma rather than a definition. E.g., something like:
lemma exists_foo [CompleteSpace 𝕜] [FiniteDimensional 𝕜 F] [ContMDiffVectorBundle ∞ F V I]
(e : Trivialization F (TotalSpace.proj : TotalSpace F V → M)) [MemTrivializationAtlas e]
{x : M} (hx : x ∈ e.baseSet) :
∃ s : V x →ₗ[𝕜] ((x' : M) → V x'), ∀ v, s v x = v ∧ CMDiff[e.baseSet] ∞ (T% (s v)) := by
sorryThere was a problem hiding this comment.
This would be really really inconvenient. We want to use this definition as input to other definitions. Your proposal would result in lots of letI on top of definition bodies. A typical use is https://github.com/leanprover-community/mathlib4/pull/36128/changes#diff-3f270ece139d7bb1abd8287dd1aed17f07e2434ca37578061c60fecca1db925bR416
| -- XXX: we could generalise this definition to any local frame on `U ∋ x`, with smoothness on `U`. | ||
| -- Would this be useful? Should do this? |
There was a problem hiding this comment.
This does sound like it would be worth having. If there is a very good API for passing from a local frame to a trivialization then probably that is what we should do here instead. OTOH if not (and if there cannot be such API), we might just want both (and the local frame version could happen later).
There was a problem hiding this comment.
I don’t think it’s worth having this. Using local frame here was already a mistake we made because we didn’t know enough about existing stuff. The extension using another frame would have no extra property at all.
|
-awaiting-author |
|
Closing in favor of #36234 |
Given a vector bundle
VoverMand a vectorXin the fibreE xsome pointx,construct a section of
Vwhich is smooth nearxand has valueXatx.This will be used to prove the tensoriality of covariant derivatives.
From the path towards geodesics and the Levi-Civita connection.
Co-authored-by: Patrick Massot patrickmassot@free.fr
Open questions I'd like a second opinion on:
should this definition be generalised to any local frame (on some setseems not necessaryU ∋ x)? this would be easy; at the moment, I don't see how we would need thatshould the new definition be namespaced, e.g. in the Trivialization namespace?
order of the explicit arguments: first e then b, or the other way around? might be resolved by the previous point
depends on: [Merged by Bors] - feat: local frames in a vector bundle #30083