[Merged by Bors] - feat: metric connections by grunweg · Pull Request #36299 · leanprover-community/mathlib4

grunweg · 2026-03-06T22:20:36Z

This file defines what it means for a connection on a Riemannian vector bundle (V, g) to be compatible with the metric g. Namely, the differentiated metric tensor ∇ g (defined by (X, σ, τ) ↦ X g(σ, τ) - g(∇_X σ, τ) - g(σ, ∇_X τ)) should vanish on all differentiable vector fields X and differentiable sections σ, τ.

From the path towards 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

depends on: [Merged by Bors] - feat: covariant derivatives on vector bundles #36279
depends on: [Merged by Bors] - feat: mfderiv_smul #34263
depends on: [Merged by Bors] - chore: rename extDerivFun to mvfderiv #39485
depends on: [Merged by Bors] - feat: add and use custom (d)elaborators for mvfderiv, add basic API lemmas #39554

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

github-actions · 2026-03-06T22:21:48Z

PR summary f5d014bf4f

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.Metric` (new file)	2222

Declarations diff (regex)

+ IsMetricCompatible
+ IsMetricCompatible.mvfderiv_inner_eq
+ _root_.VectorBundle.injective_eval_contMDiffAt_sec
+ _root_.VectorBundle.injective_eval_mdifferentiableAt_sec
+ derivMetricTensor
+ derivMetricTensorAux
+ derivMetricTensorAux_apply
+ derivMetricTensor_apply
+ derivMetricTensor_apply_eq_extend
+ isMetricCompatible_iff
+ tensorial_derivMetricTensorAux₁
+ tensorial_derivMetricTensorAux₂

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit f5d014b).

+9 new declarations
−0 removed declarations

+CovariantDerivative.IsMetricCompatible
+CovariantDerivative.IsMetricCompatible.mvfderiv_inner_eq
+CovariantDerivative.derivMetricTensor
+CovariantDerivative.derivMetricTensor.congr_simp
+CovariantDerivative.derivMetricTensor_apply
+CovariantDerivative.derivMetricTensor_apply_eq_extend
+CovariantDerivative.isMetricCompatible_iff
+VectorBundle.injective_eval_contMDiffAt_sec
+VectorBundle.injective_eval_mdifferentiableAt_sec

No changes to strong technical debt.

No changes to weak technical debt.

Current commit f5d014bf4f
Reference commit 96fd0fff3b

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).

grunweg · 2026-06-09T17:37:01Z

Could you write down somewhere why you only treat CovariantDerivative and not IsCovariantDerivativeOn?

Sure: in short, we are not aware of any application of such a notion.

You want covariant derivatives on a set e.g. to construct any covariant derivative by gluing. Heather, Patrick and I are not aware of any application of gluing metric connections. (This is also why we don't have the torsion of a connection on a set.) Do you think this is worth a comment in the implementation notes?

…ric.lean Co-authored-by: Sebastien Gouezel <sebastien.gouezel@univ-rennes1.fr>

grunweg · 2026-06-11T12:14:49Z

Thanks for the review comments, fixed!

grunweg · 2026-06-14T12:31:30Z

-awaiting-author
All comments addressed again.

sgouezel · 2026-06-17T15:58:46Z

bors r+
Thanks!

This file defines what it means for a connection on a Riemannian vector bundle `(V, g)` to be *compatible* with the metric `g`. Namely, the differentiated metric tensor `∇ g` (defined by `(X, σ, τ) ↦ X g(σ, τ) - g(∇_X σ, τ) - g(σ, ∇_X τ)`) should vanish on all differentiable vector fields `X` and differentiable sections `σ`, `τ`. From the path towards the Levi-Civita connection and Riemannian geometry. Co-authored-by: Heather Macbeth [25316162+hrmacbeth@users.noreply.github.com](mailto:25316162+hrmacbeth@users.noreply.github.com) Co-authored-by: Patrick Massot [patrickmassot@free.fr](mailto:patrickmassot@free.fr) Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Patrick Massot <patrickmassot@free.fr>

grunweg · 2026-06-17T16:41:18Z

Thanks a lot for the reviews, and especially through the last stages of nitpicking/bikeshedding!

mathlib-bors · 2026-06-17T17:44:17Z

Pull request successfully merged into master.

Build succeeded:

This file defines what it means for a connection on a Riemannian vector bundle `(V, g)` to be *compatible* with the metric `g`. Namely, the differentiated metric tensor `∇ g` (defined by `(X, σ, τ) ↦ X g(σ, τ) - g(∇_X σ, τ) - g(σ, ∇_X τ)`) should vanish on all differentiable vector fields `X` and differentiable sections `σ`, `τ`. From the path towards the Levi-Civita connection and Riemannian geometry. Co-authored-by: Heather Macbeth [25316162+hrmacbeth@users.noreply.github.com](mailto:25316162+hrmacbeth@users.noreply.github.com) Co-authored-by: Patrick Massot [patrickmassot@free.fr](mailto:patrickmassot@free.fr) Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Patrick Massot <patrickmassot@free.fr>

PatrickMassot and others added 18 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

Merge branch 'master' into covariant-derivatives-torsion

4cc7608

chore: add more bar!

c76b337

feat: torsion of an affine connection

ff0a1bf

We define the torsion tensor of an affine connection, i.e. a covariant derivative on the tangent bundle `TM` of some manifold `M`.

Fix the build

ba399a0

chore: add missing bar; and use mfderiv% and mfderiv[s] slightly more

03cb39f

chore: don't need mfderiv_smul and friends just yet

98bd8bb

chore: cherry-pick leanprover-community#34263

5ef0c9b

chore: transplant improvements from PR

711c141

feat: metric connections

b0a39e7

TODO: file is still unreviewed; will need further tweaks

grunweg added WIP Work in progress t-differential-geometry Manifolds etc labels Mar 6, 2026

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

hrmacbeth added 2 commits March 7, 2026 10:49

generalize to a riemannian bundle

7f7b5d8

update notation after generalisation

3de9043

hrmacbeth changed the title ~~feat: metric connections on the tangent bundle~~ feat: metric connections Mar 7, 2026

grunweg mentioned this pull request Mar 7, 2026

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

Draft

17 of 18 tasks

hrmacbeth added 4 commits March 7, 2026 15:29

adjust after rewrite of mfderiv_sul

4dcac6e

docs

91d1d2a

import new file

dcbeacf

clean up proofs a bit

072c4b8

Merge branch 'master' into covariant-derivatives-metric

71e83a0

sgouezel reviewed Jun 10, 2026

View reviewed changes

Comment thread Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Metric.lean Outdated

Comment thread Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Metric.lean Outdated

Comment thread Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Metric.lean Outdated

sgouezel added the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Jun 10, 2026

grunweg and others added 2 commits June 11, 2026 14:04

Update Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Met…

ba9dfc8

…ric.lean Co-authored-by: Sebastien Gouezel <sebastien.gouezel@univ-rennes1.fr>

Review comments

1aaf63c

grunweg removed the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Jun 11, 2026

grunweg requested a review from sgouezel June 11, 2026 12:36

sgouezel reviewed Jun 11, 2026

View reviewed changes

Comment thread Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Metric.lean Outdated

Comment thread Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Metric.lean Outdated

Comment thread Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Metric.lean Outdated

sgouezel added the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Jun 12, 2026

grunweg added 2 commits June 14, 2026 14:29

Review comments 1: renaming

76ba34f

Second renaming; reword doc-string

f5d014b

github-actions Bot removed the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Jun 14, 2026

mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label Jun 17, 2026

mathlib-bors Bot changed the title ~~feat: metric connections~~ [Merged by Bors] - feat: metric connections Jun 17, 2026

mathlib-bors Bot closed this Jun 17, 2026

grunweg deleted the covariant-derivatives-metric branch June 17, 2026 21:18

kim-em mentioned this pull request Aug 6, 2026

Add roadmap: geodesics, the exponential map, and Hopf-Rinow TauCetiProject/TauCetiRoadmap#94

Merged

Navigation Menu

[Merged by Bors] - feat: metric connections - #36299

[Merged by Bors] - feat: metric connections#36299
grunweg wants to merge 50 commits into
leanprover-community:masterfrom
grunweg:covariant-derivatives-metric

grunweg commented Mar 6, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Mar 6, 2026 •

edited

Loading

Declarations diff (regex)

Uh oh!

grunweg commented Jun 9, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg commented Jun 11, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg commented Jun 14, 2026

Uh oh!

sgouezel commented Jun 17, 2026

Uh oh!

grunweg commented Jun 17, 2026

Uh oh!

mathlib-bors Bot commented Jun 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

Conversation

grunweg commented Mar 6, 2026 • edited 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 f5d014bf4f

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

grunweg commented Jun 9, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg commented Jun 11, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg commented Jun 14, 2026

Uh oh!

sgouezel commented Jun 17, 2026

Uh oh!

grunweg commented Jun 17, 2026

Uh oh!

mathlib-bors Bot commented Jun 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

grunweg commented Mar 6, 2026 •

edited

Loading

github-actions Bot commented Mar 6, 2026 •

edited

Loading