feat: local frames in a vector bundle #30338

grunweg · 2025-10-08T17:50:09Z

We define a predicate IsLocalFrameOn, for a collection of sections of a vector bundle to be a local frame.
We provide some basic API, such as the coefficients of a section t w.r.t. a local frame, or proving smoothness of t via proving the smoothness of its local frame coefficients.

A future PR will construct actual local frames, and use these to define the local extension of a tangent vector to a vector field near a point.

From the path towards geodesics and the Levi-Civita connection.

Co-authored-by: Patrick Massot patrickmassot@free.fr

This depends on the custom elaborators added in leanprover-community#27021; for some reason, using these fails. To be investigated!

github-actions · 2025-10-08T17:51:18Z

PR summary c7bb7934b2

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Geometry.Manifold.VectorBundle.LocalFrame` (new file)	2101

Declarations diff

+ IsLocalFrameOn
+ congr
+ contMDiffAt
+ contMDiffAt_of_repr
+ contMDiffAt_of_repr_aux
+ contMDiffOn_of_repr
+ eq_iff_repr
+ mdifferentiableAt_of_repr
+ mdifferentiableAt_of_repr_aux
+ mdifferentiableOn_of_repr
+ mono
+ repr
+ repr_apply_of_mem
+ repr_apply_of_notMem
+ repr_apply_zero_at
+ repr_congr
+ repr_eq_of_eq
+ repr_spec
+ repr_sum_eq
+ toBasisAt
+ toBasisAt_coe

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

ocfnash

Thanks, just a bunch of nitpicks!

bors d+

Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean

ocfnash · 2025-10-20T16:35:50Z

Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean

+Outside of `u`, this returns the junk value 0. -/
+-- NB. We don't use simps here, as we prefer to have dedicated `_apply` lemmas for the separate
+-- cases.
+def repr (hs : IsLocalFrameOn I F n s u) (i : ι) : (Π x : M, V x) →ₗ[𝕜] M → 𝕜 where


I have never been a fan of the name repr in Basis and this is also pretty far from Basis.repr (which is an equivalence singling no one coord).

I'd prefer almost anything else here. What do you think of:

Suggested change

def repr (hs : IsLocalFrameOn I F n s u) (i : ι) : (Π x : M, V x) →ₗ[𝕜] M → 𝕜 where

def toLin (hs : IsLocalFrameOn I F n s u) (i : ι) : (Π x : M, V x) →ₗ[𝕜] M → 𝕜 where

(or maybe coeff or coord)

Good point! I went by analogy with Basis.repr, but indeed Basis.coord is a better analogy. So, certainly coord would already be a better name, and perhaps coeff is even better. I'll think about it!

Why did you pick toLin? To me, that seems "type-correct", but carries little semantic information (unlike coeff or coord).

Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean

ocfnash · 2025-10-20T16:37:53Z

Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean

+
+/-- A local frame locally spans the space of sections for `V`: for each local frame `s i` on an open
+set `u` around `x`, we have `t = ∑ i, (hs.repr i t) • (s i x)` near `x`. -/
+lemma repr_spec [Fintype ι] (hs : IsLocalFrameOn I F n s u) (t : Π x : M,  V x) (hu'' : u ∈ 𝓝 x) :


How about:

Suggested change

lemma repr_spec [Fintype ι] (hs : IsLocalFrameOn I F n s u) (t : Π x : M, V x) (hu'' : u ∈ 𝓝 x) :

lemma eventually_eq_sum_repr_smul [Fintype ι] (hs : IsLocalFrameOn I F n s u) (t : Π x : M, V x) (hu'' : u ∈ 𝓝 x) :

(or even better if you agree with my comment above and pick something other than repr)

I'll do both!

ocfnash · 2025-10-20T16:40:42Z

Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean

+basis of `V x` for each `x ∈ e.baseSet`. Any section `s` of `e` can be uniquely written as
+`s = ∑ i, f^i sᵢ` near `x`, and `s` is smooth at `x` iff the functions `f^i` are.
+
+The latter statement holds in many cases, but not for every vector bundle. In this file, we prove


If you're raising explicitly the failure to capture smoothness by smoothness of coefficients (IIUC), then I think you need to add a sentence saying when it can fail.

I guess the key point is that IsLocalFrame is only really useful in finite-dimensions?

Indeed, that's mostly it. The subsequent sentences describe better when this holds. Do you see a way to reword this? (Otherwise, I'll think about it when I'm done with my teaching this week.)

Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean

mathlib-bors · 2025-10-20T16:59:54Z

✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>

grunweg

Thank you for the careful review. I'm still learning something new every time. I have some comments on your comments (and will fully address them once I'm out of my teaching cave for the week).

grunweg · 2025-10-20T20:59:58Z

Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean

+basis of `V x` for each `x ∈ e.baseSet`. Any section `s` of `e` can be uniquely written as
+`s = ∑ i, f^i sᵢ` near `x`, and `s` is smooth at `x` iff the functions `f^i` are.
+
+The latter statement holds in many cases, but not for every vector bundle. In this file, we prove


Indeed, that's mostly it. The subsequent sentences describe better when this holds. Do you see a way to reword this? (Otherwise, I'll think about it when I'm done with my teaching this week.)

grunweg · 2025-10-20T21:01:50Z

Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean

+Outside of `u`, this returns the junk value 0. -/
+-- NB. We don't use simps here, as we prefer to have dedicated `_apply` lemmas for the separate
+-- cases.
+def repr (hs : IsLocalFrameOn I F n s u) (i : ι) : (Π x : M, V x) →ₗ[𝕜] M → 𝕜 where


Good point! I went by analogy with Basis.repr, but indeed Basis.coord is a better analogy. So, certainly coord would already be a better name, and perhaps coeff is even better. I'll think about it!

Why did you pick toLin? To me, that seems "type-correct", but carries little semantic information (unlike coeff or coord).

grunweg · 2025-10-20T21:02:50Z

Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean

+
+/-- A local frame locally spans the space of sections for `V`: for each local frame `s i` on an open
+set `u` around `x`, we have `t = ∑ i, (hs.repr i t) • (s i x)` near `x`. -/
+lemma repr_spec [Fintype ι] (hs : IsLocalFrameOn I F n s u) (t : Π x : M,  V x) (hu'' : u ∈ 𝓝 x) :


I'll do both!

grunweg added 8 commits October 8, 2025 09:29

feat: local frames

f4ec99c

This depends on the custom elaborators added in leanprover-community#27021; for some reason, using these fails. To be investigated!

Update for recent changes (to precedence of T%)

f29606b

Fix the build

45b84fe

Polish

2800eb5

Fix the build

2c3bb2a

Extend doc-string; remove local extension stuff for now

8f523f3

Remove another lemma

cb50043

Just the first half

c962609

github-actions bot added the t-differential-geometry Manifolds etc label Oct 8, 2025

grunweg mentioned this pull request Oct 8, 2025

feat: local frames in a vector bundle #30083

Open

2 tasks

Lint

dc5ebd8

grunweg mentioned this pull request Oct 8, 2025

Mr. Covariant Derivatives #26221

Draft

32 tasks

leanprover-community-bot-assistant assigned hrmacbeth Oct 16, 2025

ocfnash approved these changes Oct 20, 2025

View reviewed changes

leanprover-community-mathlib4-bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Oct 20, 2025

Apply easy review comments

c630841

Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>

grunweg commented Oct 20, 2025

View reviewed changes

	def repr (hs : IsLocalFrameOn I F n s u) (i : ι) : (Π x : M, V x) →ₗ[𝕜] M → 𝕜 where
	def toLin (hs : IsLocalFrameOn I F n s u) (i : ι) : (Π x : M, V x) →ₗ[𝕜] M → 𝕜 where

	lemma repr_spec [Fintype ι] (hs : IsLocalFrameOn I F n s u) (t : Π x : M, V x) (hu'' : u ∈ 𝓝 x) :
	lemma eventually_eq_sum_repr_smul [Fintype ι] (hs : IsLocalFrameOn I F n s u) (t : Π x : M, V x) (hu'' : u ∈ 𝓝 x) :

feat: local frames in a vector bundle #30338

Are you sure you want to change the base?

feat: local frames in a vector bundle #30338

Uh oh!

Conversation

grunweg commented Oct 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Oct 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary c7bb7934b2

Import changes for modified files

Declarations diff

Uh oh!

ocfnash left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mathlib-bors bot commented Oct 20, 2025

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

grunweg commented Oct 8, 2025 •

edited

Loading

github-actions bot commented Oct 8, 2025 •

edited

Loading