[Merged by Bors] - feat: covariant derivatives on vector bundles by PatrickMassot · Pull Request #36279 · leanprover-community/mathlib4

PatrickMassot · 2026-03-06T16:23:26Z

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: Michael Rothgang rothgang@math.uni-bonn.de

depends on: [Merged by Bors] - feat: FiberBundle.extend #36234
depends on: [Merged by Bors] - feat(Manifold/VectorBundle): tensoriality construction #36432

Extend an element of a fiber at a point to a local section.

github-actions · 2026-03-06T16:24:36Z

PR summary 151b5c4ae6

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic` (new file)	2253

Declarations diff

+ ContMDiffCovariantDerivative
+ ContMDiffCovariantDerivative.affine_combination
+ ContMDiffCovariantDerivative.finite_affine_combination
+ ContMDiffCovariantDerivativeOn
+ CovariantDerivative
+ IsCovariantDerivativeOn
+ _root_.ContMDiffCovariantDerivativeOn.affine_combination
+ _root_.ContMDiffCovariantDerivativeOn.finite_affine_combination
+ addOneForm
+ add_one_form
+ congr_of_eqOn
+ congr_of_eventuallyEq
+ contMDiffCovariantDerivativeOn_univ_iff
+ differenceAux
+ differenceAux_tensorial
+ difference_apply
+ extDerivFun
+ extDerivFun_add
+ extDerivFun_zero
+ iUnion
+ instance : CoeFun (CovariantDerivative I F V)
+ isCovariantDerivativeOn
+ mono
+ of_isCovariantDerivativeOn_of_open_cover
+ of_isCovariantDerivativeOn_of_open_cover_coe
+ smulRight_zero
+ smul_const
+ zero_smulRight
++ affine_combination
++ difference
++ finite_affine_combination
++ zero

You can run this locally as follows

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

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

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

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
10169	1	backward.isDefEq

Current commit 412906b87e
Reference commit 151b5c4ae6

You can run this locally as

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

Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Basic.lean

sgouezel · 2026-03-07T09:28:51Z

Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Basic.lean

+/--
+A covariant derivative ∇ is called of class `C^k` iff, whenever `X` is a `C^k` section and `σ` a
+`C^{k+1}` section, the result `∇_X σ` is a `C^k` section. This is a class so typeclass inference can
+deduce this automatically.


Could you insist that there is no a priori monotonicity wrt k in this definition, if I understand correctly the definition? Or is there in fact such a monotonicity, although this is not obvious from the definition, thanks to a local description in coordinates?

I added a comment. That stuff about differentiability is kind of a stub in this file, but we wanted to show we have in mind that the condition without differentiability assumption is a weird mathematical object. A later PR will develop the theory of covariant derivatives seen in a trivialization, including that you always get D + A where D is mfderic and A is an End(V)-valued 1-form.

mathlib-dependent-issues · 2026-03-10T12:09:50Z

This PR/issue depends on:

~~[Merged by Bors] - feat: FiberBundle.extend #36234~~
~~[Merged by Bors] - feat(Manifold/VectorBundle): tensoriality construction #36432~~
By Dependent Issues (🤖). Happy coding!

grunweg · 2026-03-10T14:40:04Z

@sgouezel Would you like to take another look at this PR, now that its dependency has been merged?
This would be very helpful - as Heather, Patrick and I were all involved with writing it, we better not merge it ourselves. Thanks!

Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Basic.lean

This is actually not used, but shows the definition can be worked with

grunweg · 2026-03-12T14:57:28Z

Thanks for your comments. I have responded to them all; this PR is ready for review again.

ocfnash

Thanks, a few last comments but LGTM.

bors d+

Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Basic.lean

Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean

Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Basic.lean

mathlib-bors · 2026-03-12T16:16:52Z

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

ocfnash · 2026-03-12T16:18:05Z

Also

bors d=@grunweg

mathlib-bors · 2026-03-12T16:18:08Z

✌️ 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.

mathlib-auto-merge · 2026-03-12T18:46:58Z

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

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: Michael Rothgang <rothgang@math.uni-bonn.de> Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>

mathlib-bors · 2026-03-12T19:50:54Z

Pull request successfully merged into master.

Build succeeded:

PatrickMassot and others added 9 commits March 6, 2026 00:02

feat: FiberBundle.extend

4dc88fe

Extend an element of a fiber at a point to a local section.

Lint

419199f

Some cleanup suggested by Michael

9cc0d58

lint

a412b42

Golfs and docs

54895ba

Merge branch 'master' into tensoriality

403efac

tensoriality

9c8186d

fix imports

72147d5

feat: Covariant derivatives on a vector bundle

efdc73f

mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 6, 2026

grunweg changed the title ~~feat: Covariant derivatives on vector bundles~~ feat: covariant derivatives on vector bundles Mar 6, 2026

grunweg mentioned this pull request Mar 6, 2026

[Merged by Bors] - feat: torsion of an affine connection #36285

Closed

1 task

grunweg added the t-differential-geometry Manifolds etc label Mar 6, 2026

grunweg and others added 2 commits March 6, 2026 18:58

chore: don't need mfderiv_smul and friends just yet

e31fd12

Merge branch 'master' into pm_covariant_derivative_basic

550df2d

grunweg mentioned this pull request Mar 6, 2026

[Merged by Bors] - feat: mfderiv_smul #34263

Closed

hrmacbeth mentioned this pull request Mar 6, 2026

feat: metric connections #36299

Open

2 tasks

sgouezel reviewed Mar 7, 2026

View reviewed changes

grunweg mentioned this pull request Mar 7, 2026

[placeholder PR uniting ongoing work on connections and geodesics] #36036

Open

6 tasks

PatrickMassot and others added 3 commits March 7, 2026 21:21

Review comment

3312cba

docs typo

1cb261e

Merge branch 'master' into pm_covariant_derivative_basic

78209a1

grunweg removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 10, 2026

grunweg requested a review from sgouezel March 10, 2026 14:40

grunweg added 2 commits March 10, 2026 17:53

Merge branch 'master' into pm_covariant_derivative_basic

064c9a6

chore: use elaborators twice more

341dfd5

ocfnash reviewed Mar 11, 2026

View reviewed changes

ocfnash added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 11, 2026

grunweg added 6 commits March 12, 2026 12:14

Generalise congr_of_eqOn to congr_of_eventuallyEq

ec5202d

refactor: add and use extDerivFun --- TODO, add more API!

ed04242

chore: add ContinuousLinearMap.smulRight_zero,zero_smulRight

24d4f4a

Use smulRight also: makes things even nicer

c74e179

Merge branch 'master' into pm_covariant_derivative_basic

9b282f4

chore: some API for extDerivFun_add

aa1b892

This is actually not used, but shows the definition can be worked with

ocfnash approved these changes Mar 12, 2026

View reviewed changes

mathlib-triage bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Mar 12, 2026

grunweg added 2 commits March 12, 2026 19:25

Review comments, part 1

b9880cc

chore: move extDerivFun and add it to the module doc-string

412906b

grunweg added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Mar 12, 2026

mathlib-bors bot changed the title ~~feat: covariant derivatives on vector bundles~~ [Merged by Bors] - feat: covariant derivatives on vector bundles Mar 12, 2026

mathlib-bors bot closed this Mar 12, 2026

TheDarkchip mentioned this pull request Mar 13, 2026

feat(Geometry/Manifold): existence of covariant derivatives #36620

Closed

Conversation

PatrickMassot commented Mar 6, 2026 • edited by grunweg Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Mar 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 151b5c4ae6

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

sgouezel Mar 7, 2026

Choose a reason for hiding this comment

Uh oh!

PatrickMassot Mar 7, 2026

Choose a reason for hiding this comment

Uh oh!

mathlib-dependent-issues bot commented Mar 10, 2026

Uh oh!

grunweg commented Mar 10, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg commented Mar 12, 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!

mathlib-bors bot commented Mar 12, 2026

Uh oh!

ocfnash commented Mar 12, 2026

Uh oh!

mathlib-bors bot commented Mar 12, 2026

Uh oh!

mathlib-auto-merge bot commented Mar 12, 2026

Uh oh!

mathlib-bors bot commented Mar 12, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

PatrickMassot commented Mar 6, 2026 •

edited by grunweg

Loading

github-actions bot commented Mar 6, 2026 •

edited

Loading