feat(Manifold/VectorBundle): tensoriality construction by hrmacbeth · Pull Request #36277 · leanprover-community/mathlib4

hrmacbeth · 2026-03-06T15:09:34Z

Given vector bundles V and W over a manifold, one can construct a section of the hom-bundle Π x, V x →L[𝕜] W x from a tensorial operation sending sections of V to sections of W. This PR provides this construction.

Co-authored-by: Michael Rothgang rothgang@math.uni-bonn.de
Co-authored-by: Patrick Massot mailto:patrickmassot@free.fr

depends on: [Merged by Bors] - feat: FiberBundle.extend #36234

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

github-actions · 2026-03-06T15:10:40Z

PR summary ee78550dfd

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Topology.VectorBundle.FiniteDimensional` (new file)	1796
`Mathlib.Geometry.Manifold.VectorBundle.Tensoriality` (new file)	2250

Declarations diff

+ TensorialAt
+ continuousLinearEquivAt
+ finiteDimensional
+ finrank_eq
+ homeomorphAt
+ mkHom
+ mkHom_apply
+ mkHom_apply_eq_extend
+ mkHom₂
+ mkHom₂_apply
+ mkHom₂_apply_eq_extend
+ pointwise
+ pointwise₂
+ sum
+ t0Space
+ t1Space
+ t2Space
+ t3Space
+ zero
+ «local»

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.

No changes to technical debt.

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-dependent-issues · 2026-03-06T17:24:58Z

This PR/issue depends on:

~~[Merged by Bors] - feat: FiberBundle.extend #36234~~
By Dependent Issues (🤖). Happy coding!

Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean

ADedecker

Thanks! I'm not very familiar with this corner of the library, so let's ask for a second look.

maintainer delegate

Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean

Mathlib/Topology/FiberBundle/Basic.lean

ADedecker · 2026-03-08T20:42:22Z

Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean

+  { add_left v₁ v₂ w := by
+      rw [← (hΦ₁ _ (mdifferentiableAt_extend ..)).add (mdifferentiableAt_extend ..)
+        (mdifferentiableAt_extend ..)]
+      apply TensorialAt.pointwise₂ hΦ₁ hΦ₂ (mdifferentiableAt_extend ..) _
+        (mdifferentiableAt_extend ..) (mdifferentiableAt_extend ..) _ rfl
+      · exact mdifferentiableAt_add_section (mdifferentiableAt_extend ..)
+          (mdifferentiableAt_extend ..)
+      · simp
+    smul_left c v w := by
+      rw [← (hΦ₁ _ (mdifferentiableAt_extend ..)).smul (f := fun _ ↦ c) (mdifferentiable_const ..)
+        (mdifferentiableAt_extend ..)]
+      apply TensorialAt.pointwise₂ hΦ₁ hΦ₂ (mdifferentiableAt_extend ..)
+        (mdifferentiableAt_const.smul_section (mdifferentiableAt_extend ..))
+        (mdifferentiableAt_extend ..) (mdifferentiableAt_extend ..)
+      · simp
+      · rfl
+    add_right v w₁ w₂ := by
+      rw [← (hΦ₂ _ (mdifferentiableAt_extend ..)).add (mdifferentiableAt_extend ..)
+        (mdifferentiableAt_extend ..)]
+      apply TensorialAt.pointwise₂ hΦ₁ hΦ₂ (mdifferentiableAt_extend ..)
+        (mdifferentiableAt_extend ..) (mdifferentiableAt_extend ..) <|
+        mdifferentiableAt_add_section (mdifferentiableAt_extend ..) (mdifferentiableAt_extend ..)
+      · rfl
+      · simp
+    smul_right c v w := by
+      rw [← (hΦ₂ _ (mdifferentiableAt_extend ..)).smul (f := fun _ ↦ c) (mdifferentiable_const ..)
+        (mdifferentiableAt_extend ..)]
+      apply TensorialAt.pointwise₂ hΦ₁ hΦ₂ (mdifferentiableAt_extend ..)
+        (mdifferentiableAt_extend ..) (mdifferentiableAt_extend ..) <|
+        mdifferentiableAt_const.smul_section (mdifferentiableAt_extend ..)
+      · rfl
+      · simp }
+  H.toLinearMap.toContinuousBilinearMap


It makes me a bit sad that our API for quotients (e.g LinearMap.liftQ₂) doesn't apply to arbitrary linear surjections... (This is just a remark, I'm not asking for you to do anything)

ocfnash · 2026-03-09T14:07:19Z

Nice: I'm going to review right now.

ocfnash

I thought about this a bit because it's a bit sad that we are avoiding working with modules over germs of functions. I suppose to pursue this we'd need to have some type synonym for A that bound x so that it could also be seen as a module over germs of functions with scalar action f • a = (f x) • a ~~(or equivalently turn A into the trivial vector bundle)~~ and indeed this all does seem likely to be quite awkward.

So far the main cost seems to be that we are forced into proving results like TensorialAt.zero and TensorialAt.sum which is not so expensive.

In summary, I'm a bit dubious but I don't see a better design (except possibly by writing a very large API to support the germ-based approach).

bors d+

Mathlib/Topology/VectorBundle/FiniteDimensional.lean

Mathlib/Topology/FiberBundle/Basic.lean

ocfnash · 2026-03-09T14:27:08Z

Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean

+
+/-- An operation `Φ` on sections of a vector bundle `V` over `M` is *tensorial* at `x : M`, if it
+respects addition and scalar multiplication by germs of diffentiable functions at `f`. -/
+structure TensorialAt (Φ : (Π x : M, V x) → A) (x : M) : Prop where


Any chance I could persuade you of:

Suggested change

structure TensorialAt (Φ : (Π x : M, V x) → A) (x : M) : Prop where

structure IsTensorialAt (Φ : (Π x : M, V x) → A) (x : M) : Prop where

In fact, this very same question came up when Patrick, Heather and I were discussing this in person. Majority was in favour of TensorialAt (which is covered by the naming convention, as tensorial is an adjective.

I'll bring it up again. Why do you prefer the Is version - so I can pass this on?

I'm very late replying but I like the Is version because it is a hint to the user that the definition is Prop-valued.

Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean

ocfnash · 2026-03-09T15:54:23Z

Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean

+  smul : ∀ {f : M → 𝕜} {σ : Π x : M, V x}, MDiffAt f x → MDiffAt (T% σ) x → Φ (f • σ) = f x • Φ σ
+  add : ∀ {σ σ'}, MDiffAt (T% σ) x → MDiffAt (T% σ') x → Φ (σ + σ') = Φ σ + Φ σ'


No action required but just briefly noting that there is the possibility for difficulty in higher differentiability classes because the user might have constructed a Φ that only knows how to interact with smooth (say) sections and thus be unable to discharge these proof obligations.

After thinking a bit I decided it was OK to regard this as "user error" but I do wonder how large a burden we might be putting on people who only want to work in a smooth setting.

You raise a very good point! I think it's not unlikely that this situation will happen and we'll need to change this definition. On the other hand, the current definition has served us well (supporting, e.g., the Levi-Civita connection or most of the work towards Ehresmann connections), so it's not too wrong either.

Let's merge this now, and revisit later if necessary.

mathlib-bors · 2026-03-09T15:54:56Z

✌️ hrmacbeth 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: Anatole Dedecker <anatolededecker@gmail.com> Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>

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

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

grunweg

Thanks for the careful review comments! I have addressed the ones I did not respond to (at #36432; for some reason I cannot push to this branch directly).

grunweg · 2026-03-10T10:28:00Z

Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean

+
+/-- An operation `Φ` on sections of a vector bundle `V` over `M` is *tensorial* at `x : M`, if it
+respects addition and scalar multiplication by germs of diffentiable functions at `f`. -/
+structure TensorialAt (Φ : (Π x : M, V x) → A) (x : M) : Prop where


In fact, this very same question came up when Patrick, Heather and I were discussing this in person. Majority was in favour of TensorialAt (which is covered by the naming convention, as tensorial is an adjective.

I'll bring it up again. Why do you prefer the Is version - so I can pass this on?

grunweg · 2026-03-10T10:29:16Z

Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean

+  smul : ∀ {f : M → 𝕜} {σ : Π x : M, V x}, MDiffAt f x → MDiffAt (T% σ) x → Φ (f • σ) = f x • Φ σ
+  add : ∀ {σ σ'}, MDiffAt (T% σ) x → MDiffAt (T% σ') x → Φ (σ + σ') = Φ σ + Φ σ'


You raise a very good point! I think it's not unlikely that this situation will happen and we'll need to change this definition. On the other hand, the current definition has served us well (supporting, e.g., the Levi-Civita connection or most of the work towards Ehresmann connections), so it's not too wrong either.

Let's merge this now, and revisit later if necessary.

grunweg · 2026-03-10T10:35:16Z

I have made all remaining review comments in #36432, and just borsed that one.
Thanks for the quick reviews!

grunweg · 2026-03-10T12:00:10Z

This PR has been merged in #36432; closing.

…uous linear equivalences (#36435) and use this to remove mathematically superfluous typeclass hypotheses in the tensoriality criterion. Follow-up to #36277/#36432.

…uous linear equivalences (leanprover-community#36435) and use this to remove mathematically superfluous typeclass hypotheses in the tensoriality criterion. Follow-up to leanprover-community#36277/leanprover-community#36432.

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

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 mentioned this pull request Mar 6, 2026

[Merged by Bors] - feat: covariant derivatives on vector bundles #36279

Closed

2 tasks

grunweg changed the title ~~feat(Manifold/VectorBundle): Tensoriality construction~~ feat(Manifold/VectorBundle): tensoriality construction Mar 6, 2026

Merge branch 'master' into tensoriality

8e65e59

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

ADedecker reviewed Mar 6, 2026

View reviewed changes

Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean Outdated Show resolved Hide resolved

ADedecker reviewed Mar 6, 2026

View reviewed changes

Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean Outdated Show resolved Hide resolved

ADedecker reviewed Mar 6, 2026

View reviewed changes

Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean Outdated Show resolved Hide resolved

grunweg mentioned this pull request Mar 7, 2026

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

Open

6 tasks

PatrickMassot added 2 commits March 7, 2026 14:35

Incorporate review comments

74c9c11

Forgotten simplification

589946d

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

ADedecker approved these changes Mar 8, 2026

View reviewed changes

ocfnash self-assigned this Mar 9, 2026

ocfnash approved these changes Mar 9, 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 Mar 9, 2026

Apply suggestions from code review

0e144cf

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

grunweg mentioned this pull request Mar 10, 2026

[Merged by Bors] - feat(Manifold/VectorBundle): tensoriality construction #36432

Closed

grunweg and others added 2 commits March 10, 2026 11:05

Apply suggestions from code review

f9c89ac

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

Apply suggestion from @ADedecker

2f29360

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

grunweg reviewed Mar 10, 2026

View reviewed changes

grunweg mentioned this pull request Mar 10, 2026

[Merged by Bors] - feat: transfer IsTopologicalAddGroup and ContinuousSMul across continuous linear equivalences #36435

Closed

1 task

grunweg closed this Mar 10, 2026

grunweg deleted the tensoriality branch March 10, 2026 12:00

	structure TensorialAt (Φ : (Π x : M, V x) → A) (x : M) : Prop where
	structure IsTensorialAt (Φ : (Π x : M, V x) → A) (x : M) : Prop where

		smul : ∀ {f : M → 𝕜} {σ : Π x : M, V x}, MDiffAt f x → MDiffAt (T% σ) x → Φ (f • σ) = f x • Φ σ
		add : ∀ {σ σ'}, MDiffAt (T% σ) x → MDiffAt (T% σ') x → Φ (σ + σ') = Φ σ + Φ σ'

Conversation

hrmacbeth 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 ee78550dfd

Import changes for modified files

Declarations diff

Uh oh!

mathlib-dependent-issues bot commented Mar 6, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ADedecker left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ADedecker Mar 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ocfnash commented Mar 9, 2026

Uh oh!

ocfnash left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

ocfnash Mar 9, 2026

Choose a reason for hiding this comment

Uh oh!

grunweg Mar 10, 2026

Choose a reason for hiding this comment

Uh oh!

ocfnash Mar 11, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

ocfnash Mar 9, 2026

Choose a reason for hiding this comment

Uh oh!

grunweg Mar 10, 2026

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Mar 9, 2026

Uh oh!

grunweg left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

grunweg Mar 10, 2026

Choose a reason for hiding this comment

Uh oh!

grunweg Mar 10, 2026

Choose a reason for hiding this comment

Uh oh!

grunweg commented Mar 10, 2026

Uh oh!

grunweg commented Mar 10, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

hrmacbeth commented Mar 6, 2026 •

edited by grunweg

Loading

github-actions bot commented Mar 6, 2026 •

edited

Loading

ADedecker Mar 8, 2026 •

edited

Loading

ocfnash left a comment •

edited

Loading

grunweg left a comment •

edited

Loading