[Merged by Bors] - feat: local frames in a vector bundle by grunweg · Pull Request #30083 · leanprover-community/mathlib4

grunweg · 2025-09-30T10:04:26Z

We construct local frames on a vector from local trivialisations. The former constructs, given a trivialisation e of the vector bundle and a basis of the model fibre, Basis.localFrame is a local frame on e.baseSet
A future PR will use this 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

depends on: [Merged by Bors] - feat: custom elaborators for differential geometry #27021
depends on: [Merged by Bors] - feat: local frames in a vector bundle #30338
depends on: [Merged by Bors] - feat: add contMDiffOn_empty and friends #31542
depends on: [Merged by Bors] - feat: local frame induced by a vector bundle trivialisation #31788

github-actions · 2025-09-30T10:05:33Z

PR summary 8115783e28

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ contMDiffAt_iff_localFrame_coeff
+ contMDiffAt_localFrame_coeff
+ contMDiffOn_baseSet_iff_localFrame_coeff
+ contMDiffOn_baseSet_localFrame_coeff
+ contMDiffOn_iff_localFrame_coeff
+ contMDiffOn_localFrame_coeff
+ eq_of_coeff_eq
+ eq_sum_localFrame_coeff_smul
+ eventually_eq_localFrame_sum_coeff_smul
+ localFrame_coeff
+ localFrame_coeff_apply_of_mem_baseSet
+ localFrame_coeff_apply_of_notMem_baseSet
+ localFrame_coeff_congr
+ localFrame_coeff_eq_coeff
+ mdifferentiableAt_iff_localFrame_coeff
+ mdifferentiableAt_localFrame_coeff
+ mdifferentiableOn_baseSet_localFrame_coeff
+ mdifferentiableOn_localFrame_coeff
+ piApply
+ piApply_apply
+ piApply_apply_apply
- coeff_apply_zero_at

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 scripts/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).

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

mathlib4-merge-conflict-bot · 2025-10-23T14:14:02Z

This pull request has conflicts, please merge master and resolve them.

ocfnash

Thanks!

I've left a bunch of fairly superficial comments, but I think they're worth addressing. I'll return again once you've had a chance to respond.

Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean

grunweg · 2026-02-22T22:07:49Z

Most lemma statements are not in simp normal form: (LinearMap.piApply (hs.coeff i)) t x simplifies to (hs.coeff i x) (t x). So the next step is to change the lemma statements accordingly...
@michaellee94 If you'd like to help, I wouldn't mind a hand. (Otherwise, I'll get to this myself in due time.)

grunweg · 2026-02-23T22:22:29Z

Ok, I think I caught all obvious such references: the remaining ones are in hypotheses, where I'm not convinced yet that they must be removed.

michaellee94 · 2026-02-23T23:06:59Z

Thanks for doing that, @grunweg! Was out of town, sorry for missing your message.

ocfnash

Thanks!

bors d+

Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean

mathlib-bors · 2026-02-24T11:09:45Z

✌️ 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 · 2026-02-24T18:13:25Z

Thanks for the careful review over the many rounds - I am very happy how this PR turned out, and think it's much nicer as a result.
bors merge

We construct local frames on a vector from local trivialisations. The former constructs, given a trivialisation `e` of the vector bundle and a basis of the model fibre, `Basis.localFrame` is a local frame on `e.baseSet` A future PR will use this 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](mailto:patrickmassot@free.fr) Co-authored-by: michaellee94 <michael.a.rodrigues.lee@gmail.com>

mathlib-bors · 2026-02-24T19:05:41Z

Pull request successfully merged into master.

Build succeeded:

…#31338) As suggested in #30083.

We construct local frames on a vector from local trivialisations. The former constructs, given a trivialisation `e` of the vector bundle and a basis of the model fibre, `Basis.localFrame` is a local frame on `e.baseSet` A future PR will use this 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](mailto:patrickmassot@free.fr) Co-authored-by: michaellee94 <michael.a.rodrigues.lee@gmail.com>

…leanprover-community#31338) As suggested in leanprover-community#30083.

grunweg added t-differential-geometry Manifolds etc blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Sep 30, 2025

grunweg force-pushed the localframes branch 2 times, most recently from 617c74b to df44a30 Compare September 30, 2025 18:38

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 8, 2025

grunweg added 4 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

grunweg force-pushed the localframes branch from df44a30 to 2800eb5 Compare October 8, 2025 16:29

grunweg changed the title ~~feat: local frames~~ feat: local frames in a vector bundle Oct 8, 2025

grunweg added 3 commits October 8, 2025 09:34

Fix the build

2c3bb2a

Extend doc-string; remove local extension stuff for now

8f523f3

Remove another lemma

cb50043

grunweg added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 8, 2025

This was referenced Oct 8, 2025

Mr. Covariant Derivatives #26221

Draft

feat: extend a tangent vector for a locally smooth vector field #30339

Closed

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 23, 2025

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 23, 2025

grunweg added 4 commits October 23, 2025 18:05

Merge master

6b1d56f

repr -> coeff

cbaacd5

Last rename, line length and variable management

e0696f8

Comment

b05c562

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 23, 2025

Tweak

9f602c3

grunweg mentioned this pull request Oct 23, 2025

wip: another smoothness lemma for local frames #30824

Open

ocfnash reviewed Oct 31, 2025

View reviewed changes

ocfnash self-assigned this Oct 31, 2025

grunweg removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 22, 2026

Simplify and fix

64ec95a

grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 22, 2026

grunweg added 2 commits February 22, 2026 23:10

A few more; not exhaustive

5dd306c

A few more

29d2b42

Last ones

82ed3ee

grunweg removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 23, 2026

ocfnash approved these changes Feb 24, 2026

View reviewed changes

mathlib-triage bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Feb 24, 2026

grunweg and others added 6 commits February 24, 2026 18:57

Some review comments

40ca609

More

455aee9

Update Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean

f703211

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

Update Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean

3a337fa

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

Tweak

1fee45f

Last parentheses

744962a

mathlib-triage bot added the ready-to-merge This PR has been sent to bors. label Feb 24, 2026

mathlib-bors bot changed the title ~~feat: local frames in a vector bundle~~ [Merged by Bors] - feat: local frames in a vector bundle Feb 24, 2026

mathlib-bors bot closed this Feb 24, 2026

mathlib-bors bot pushed a commit that referenced this pull request Feb 27, 2026

chore: move Pretrivialization, Trivialization to the Bundle namespace (…

fd11b7a

…#31338) As suggested in #30083.

pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Mar 2, 2026

chore: move Pretrivialization, Trivialization to the Bundle namespace (…

1270b0d

…leanprover-community#31338) As suggested in leanprover-community#30083.

xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Mar 10, 2026

chore: move Pretrivialization, Trivialization to the Bundle namespace (…

0000340

…leanprover-community#31338) As suggested in leanprover-community#30083.

pevogam pushed a commit to pevogam/mathlib4 that referenced this pull request Mar 19, 2026

chore: move Pretrivialization, Trivialization to the Bundle namespace (…

7b80cb6

…leanprover-community#31338) As suggested in leanprover-community#30083.

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary 8115783e28

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-merge-conflict-bot commented Oct 23, 2025

Uh oh!

ocfnash left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg commented Feb 22, 2026

Uh oh!

grunweg commented Feb 23, 2026

Uh oh!

michaellee94 commented Feb 23, 2026

Uh oh!

ocfnash left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-bors bot commented Feb 24, 2026

Uh oh!

grunweg commented Feb 24, 2026

Uh oh!

mathlib-bors bot commented Feb 24, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

grunweg commented Sep 30, 2025 •

edited

Loading

github-actions bot commented Sep 30, 2025 •

edited

Loading