From dd27675af6e651f862df939c524f4a07ae21f687 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 25 Sep 2026 17:14:48 +1000 Subject: [PATCH 1/2] chore: bump to Lean v4.35.0-rc3 and current mathlib MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Mathlib's bundle of continuous linear maps now asks for `IsTopologicalAddGroup` and `ContinuousSMul` on the fibers of the target bundle. Supply those for pullback bundles, and restate the existing pullback instances with `inferInstanceAs` so that they agree with mathlib's `AddCommMonoid ((f *įµ– E) x)`. Co-Authored-By: Claude Opus 5 (1M context) --- SphereEversion/Global/OneJetBundle.lean | 5 ++- .../Geometry/Manifold/VectorBundle/Misc.lean | 32 +++++++++++++++++-- lake-manifest.json | 22 ++++++------- lean-toolchain | 2 +- 4 files changed, 45 insertions(+), 16 deletions(-) diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean index 8f1053dd..e1b627c0 100644 --- a/SphereEversion/Global/OneJetBundle.lean +++ b/SphereEversion/Global/OneJetBundle.lean @@ -179,7 +179,10 @@ instance : ContMDiffVectorBundle āˆž (E ā†’L[š•œ] E') set_option backward.isDefEq.respectTransparency false in instance : ChartedSpace HJ JĀ¹MM' := by delta OneJetSpace OneJetBundle - infer_instance + -- `infer_instance` does not close this goal: lining it up with `FiberBundle.chartedSpace` means + -- unfolding the `TopologicalSpace JĀ¹MM'` instance above, which unification during instance + -- synthesis will not do. Naming the instance elaborates at default transparency instead. + exact FiberBundle.chartedSpace .. set_option backward.isDefEq.respectTransparency false in instance : IsManifold ((I.prod I').prod š“˜(š•œ, E ā†’L[š•œ] E')) āˆž JĀ¹MM' := by diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean b/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean index 08cea64e..6bd3950b 100644 --- a/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean +++ b/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean @@ -121,12 +121,38 @@ end Hom section Pullback +/- `Bundle.ContinuousLinearMap.{fiberBundle, vectorBundle}` and +`ContMDiffVectorBundle.continuousLinearMap` ask for `IsTopologicalAddGroup` and `ContinuousSMul` on +the fibers of the target bundle, so the pullback bundle needs those too; `Bundle.Pullback` is not +reducible, so they do not come for free. + +All the instances below are stated with `inferInstanceAs`, matching the pullback instances in +`Mathlib.Topology.VectorBundle.Constructions`. That is load-bearing rather than cosmetic: the +`AddCommGroup` instance has to agree with mathlib's `AddCommMonoid ((f *įµ– E) x)` up to instance +transparency, or the two disagree wherever both are in play, for instance in +`Module R ((f *įµ– E) x)` and hence in `AddCommGroup ((f *įµ– Eā‚) x ā†’L[š•œ] (f *įµ– Eā‚‚) x)`. -/ + /-- We need some instances like this to work with negation on pullbacks -/ instance {B B'} {E : B ā†’ Type*} {f : B' ā†’ B} {x : B'} [āˆ€ x', AddCommGroup (E x')] : - AddCommGroup ((f *įµ– E) x) := by delta Bundle.Pullback; infer_instance + AddCommGroup ((f *įµ– E) x) := + inferInstanceAs <| AddCommGroup (E (f x)) + +instance {B B'} {E : B ā†’ Type*} {f : B' ā†’ B} {x : B'} [āˆ€ x', Zero (E x')] : Zero ((f *įµ– E) x) := + inferInstanceAs <| Zero (E (f x)) + +instance {B B'} {E : B ā†’ Type*} {f : B' ā†’ B} {x : B'} [āˆ€ x', TopologicalSpace (E x')] + [āˆ€ x', AddCommMonoid (E x')] [āˆ€ x', ContinuousAdd (E x')] : ContinuousAdd ((f *įµ– E) x) := + inferInstanceAs <| ContinuousAdd (E (f x)) + +instance {B B'} {E : B ā†’ Type*} {f : B' ā†’ B} {x : B'} [āˆ€ x', TopologicalSpace (E x')] + [āˆ€ x', AddCommGroup (E x')] [āˆ€ x', IsTopologicalAddGroup (E x')] : + IsTopologicalAddGroup ((f *įµ– E) x) := + inferInstanceAs <| IsTopologicalAddGroup (E (f x)) -instance {B B'} {E : B ā†’ Type*} {f : B' ā†’ B} {x : B'} [āˆ€ x', Zero (E x')] : Zero ((f *įµ– E) x) := by - delta Bundle.Pullback; infer_instance +instance {R B B'} [Semiring R] [TopologicalSpace R] {E : B ā†’ Type*} {f : B' ā†’ B} {x : B'} + [āˆ€ x', TopologicalSpace (E x')] [āˆ€ x', AddCommMonoid (E x')] [āˆ€ x', Module R (E x')] + [āˆ€ x', ContinuousSMul R (E x')] : ContinuousSMul R ((f *įµ– E) x) := + inferInstanceAs <| ContinuousSMul R (E (f x)) variable {B F B' K : Type*} {E : B ā†’ Type*} {f : K} [TopologicalSpace B'] [TopologicalSpace (TotalSpace F E)] [TopologicalSpace F] [TopologicalSpace B] [āˆ€ b, Zero (E b)] diff --git a/lake-manifest.json b/lake-manifest.json index bf0b8b86..ffa681f5 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,4 +1,4 @@ -{"version": "1.2.0", +{"version": "1.3.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/PatrickMassot/checkdecls.git", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2631d1cc8c2ace6c6a900425d6e5d2b5963966e9", + "rev": "5e0c4e5239cb0a2d86d68a884bf52cfd963fce22", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d9598f07b1bc701f1e3aae163d2681c1fd978793", + "rev": "fb13df72ecefd8ddbf9291021d7f33a8673eb57b", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ba67e212be1197b84c1f1f6299488a10a3002713", + "rev": "29ff470276c725ae01505d55b17148c18fc7dfd3", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1681d78dd6e65e38b143f9740d829c826673807c", + "rev": "7e81a29bda33a6b257bd37557a6aa6aebe175d96", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a8acbfd87375ff4abe14ce09db5b7664d383bc7f", + "rev": "c643bbb3c24f8a25f9c14e3a6b1ceb13d01f3de1", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "18889deb9e83ea7420ef51c160d6f88552e744e3", + "rev": "a90fbf7b02ff06a0deebf74088dff9e5fe02c9ea", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "507746ab8f4b643ccdacb2ec4cdb5853fa9f8ab3", + "rev": "37b0ba0b26109cf9f9c541f0f9557e50cfa1a3b9", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4cac2177c37f5530c4da76aa8e4307f3fc9e4dcb", + "rev": "33131f4fb10067cb3009bf4db615d9680c1ccd6b", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,10 +95,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "ab3a82db9fea14cf0fd7f5a2de650f4b534640af", + "rev": "843844fa601dd56767b1eb22b7ada5b64d5e567a", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.34.0-rc2", + "inputRev": "v4.35.0-rc3", "inherited": true, "configFile": "lakefile.toml"}], "name": "SphereEversion", diff --git a/lean-toolchain b/lean-toolchain index d5ae4e31..f0e00b33 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.34.0-rc2 \ No newline at end of file +leanprover/lean4:v4.35.0-rc3 From 4e8f1ec0703f8860d984430f9458006a15dd0fc3 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Fri, 25 Sep 2026 12:30:23 +0200 Subject: [PATCH 2/2] Tweak comments --- SphereEversion/Global/OneJetBundle.lean | 11 +++++------ .../Geometry/Manifold/VectorBundle/Misc.lean | 12 ------------ 2 files changed, 5 insertions(+), 18 deletions(-) diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean index 9e453b19..64b37d89 100644 --- a/SphereEversion/Global/OneJetBundle.lean +++ b/SphereEversion/Global/OneJetBundle.lean @@ -155,8 +155,6 @@ instance (x : M Ɨ M') : Module š•œ (FJĀ¹MM' x) := end -set_option backward.isDefEq.respectTransparency false in -set_option backward.isDefEq.respectTransparency.instanceSearchTypes false in instance : TopologicalSpace JĀ¹MM' := by delta OneJetSpace OneJetBundle infer_instance @@ -181,10 +179,11 @@ set_option backward.isDefEq.respectTransparency false in set_option backward.isDefEq.respectTransparency.instanceSearchTypes false in instance : ChartedSpace HJ JĀ¹MM' := by delta OneJetSpace OneJetBundle - -- `infer_instance` does not close this goal: lining it up with `FiberBundle.chartedSpace` means - -- unfolding the `TopologicalSpace JĀ¹MM'` instance above, which unification during instance - -- synthesis will not do. Naming the instance elaborates at default transparency instead. - exact FiberBundle.chartedSpace .. + -- Making `FiberBundle.chartedSpace` apply here means unfolding the `TopologicalSpace JĀ¹MM'` + -- instance above, which unification during instance synthesis will not do. + -- One potential fix is naming the instance: + -- exact FiberBundle.chartedSpace .. + infer_instance set_option backward.isDefEq.respectTransparency false in instance : IsManifold ((I.prod I').prod š“˜(š•œ, E ā†’L[š•œ] E')) āˆž JĀ¹MM' := by diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean b/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean index 6bd3950b..26a8887b 100644 --- a/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean +++ b/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean @@ -121,18 +121,6 @@ end Hom section Pullback -/- `Bundle.ContinuousLinearMap.{fiberBundle, vectorBundle}` and -`ContMDiffVectorBundle.continuousLinearMap` ask for `IsTopologicalAddGroup` and `ContinuousSMul` on -the fibers of the target bundle, so the pullback bundle needs those too; `Bundle.Pullback` is not -reducible, so they do not come for free. - -All the instances below are stated with `inferInstanceAs`, matching the pullback instances in -`Mathlib.Topology.VectorBundle.Constructions`. That is load-bearing rather than cosmetic: the -`AddCommGroup` instance has to agree with mathlib's `AddCommMonoid ((f *įµ– E) x)` up to instance -transparency, or the two disagree wherever both are in play, for instance in -`Module R ((f *įµ– E) x)` and hence in `AddCommGroup ((f *įµ– Eā‚) x ā†’L[š•œ] (f *įµ– Eā‚‚) x)`. -/ - -/-- We need some instances like this to work with negation on pullbacks -/ instance {B B'} {E : B ā†’ Type*} {f : B' ā†’ B} {x : B'} [āˆ€ x', AddCommGroup (E x')] : AddCommGroup ((f *įµ– E) x) := inferInstanceAs <| AddCommGroup (E (f x))