Manifold structure on Moebius strip

Stream: mathlib4

[Dominic Steinitz]

There was a question about where the IsManifold instance came from. I hope this makes it a bit clearer. Maybe the instance instance (m n : ℕ) : ChartedSpace ((EuclideanSpace ℝ (Fin (n + m)))) (EuclideanSpace ℝ (Fin n) × (EuclideanSpace ℝ (Fin m)) should be added somewhere.

cc @Michael Rothgang

/-
Copyright (c) 2025 Dominic Steinitz. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Dominic Steinitz
-/
import Mathlib.Geometry.Manifold.Instances.Sphere
import Mathlib.Topology.FiberBundle.Basic
import Mathlib.Geometry.Manifold.VectorBundle.Basic

set_option linter.style.longLine false

open Function Set
open scoped Manifold
open Bundle

noncomputable
def Mobius : FiberBundleCore (Fin 2) (Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) (EuclideanSpace ℝ (Fin 1)) where
  baseSet i := sorry
  isOpen_baseSet i := sorry
  indexAt x := if (x.val 0) > 0 then 0 else 1
  mem_baseSet_at := sorry
  coordChange := sorry
  coordChange_self := sorry
  continuousOn_coordChange := sorry
  coordChange_comp := sorry

  /-
  Once we have a `FiberBundleCore` then we are given that the total space is a
  `ChartedSpace` by `FiberBundle.chartedSpace'`.
  -/

#synth ChartedSpace ((Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) × (EuclideanSpace ℝ (Fin 1)))
                    (TotalSpace (EuclideanSpace ℝ (Fin 1)) Mobius.Fiber)

#check FiberBundle.chartedSpace'

/-
But we want the model space to be 𝓡 2. We can compose `ChartedSpace`:
-/
noncomputable
instance : ChartedSpace ((EuclideanSpace ℝ (Fin 1)) × (EuclideanSpace ℝ (Fin 1)))
                       (TotalSpace (EuclideanSpace ℝ (Fin 1)) Mobius.Fiber)
 := ChartedSpace.comp
  (ModelProd (EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin 1)))
  ((Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) × (EuclideanSpace ℝ (Fin 1)))
  (TotalSpace (EuclideanSpace ℝ (Fin 1)) Mobius.Fiber)

/-
We'd like
  `instance (m n : ℕ) :
    ChartedSpace ((EuclideanSpace ℝ (Fin (n + m))))
                 (EuclideanSpace ℝ (Fin n) × (EuclideanSpace ℝ (Fin m)))

Luckily Michael Rothgang pointed this out to me:
https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Product.20of.20Euclidean.20spaces/near/515976964
-/

def EuclideanSpace.sumEquivProd (𝕜 : Type*) [RCLike 𝕜] (ι κ : Type*) [Fintype ι] [Fintype κ] :
    EuclideanSpace 𝕜 (ι ⊕ κ) ≃L[𝕜] EuclideanSpace 𝕜 ι × EuclideanSpace 𝕜 κ :=
  (PiLp.sumPiLpEquivProdLpPiLp 2 _).toContinuousLinearEquiv.trans <|
    WithLp.prodContinuousLinearEquiv _ _ _ _

def EuclideanSpace.finAddEquivProd {𝕜 : Type*} [RCLike 𝕜] {n m : ℕ} :
    EuclideanSpace 𝕜 (Fin (n + m)) ≃L[𝕜] EuclideanSpace 𝕜 (Fin n) × EuclideanSpace 𝕜 (Fin m) :=
  (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 finSumFinEquiv.symm).toContinuousLinearEquiv.trans <|
    sumEquivProd 𝕜 _ _

/-
And now we have the required instance.
-/
noncomputable
instance (m n : ℕ) : ChartedSpace ((EuclideanSpace ℝ (Fin (n + m)))) (EuclideanSpace ℝ (Fin n) × (EuclideanSpace ℝ (Fin m))) := by
  have h1 : EuclideanSpace ℝ (Fin (n + m)) ≃L[ℝ] EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin m) := EuclideanSpace.finAddEquivProd
  have h2 : EuclideanSpace ℝ (Fin (n + m)) ≃ₜ EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin m) :=  ContinuousLinearEquiv.toHomeomorph h1
  let x := (EuclideanSpace.finAddEquivProd : EuclideanSpace ℝ (Fin (n + m)) ≃L[ℝ] EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin m))
  let y := ContinuousLinearEquiv.toHomeomorph x
  let z := Homeomorph.toPartialHomeomorph y
  have hz : z.symm.source = univ := rfl
  exact PartialHomeomorph.singletonChartedSpace z.symm hz

/-
And now we can again compose `ChartedSpace` to get the instance we want.
-/
noncomputable
instance : ChartedSpace (EuclideanSpace ℝ (Fin 2)) (Bundle.TotalSpace (EuclideanSpace ℝ (Fin 1)) Mobius.Fiber) := by
  exact ChartedSpace.comp
    (EuclideanSpace ℝ (Fin (1 + 1)))
    ((EuclideanSpace ℝ (Fin 1)) × (EuclideanSpace ℝ (Fin 1)))
    (Bundle.TotalSpace (EuclideanSpace ℝ (Fin 1)) Mobius.Fiber)

#synth IsManifold (𝓡 2) 0 (TotalSpace (EuclideanSpace ℝ (Fin 1)) Mobius.Fiber)

[Michael Rothgang]

Thanks for the ping! I think an equivalence between Euclidean space could be worth PRing to mathlib. Would you like to make a PR? The hardest part of getting it merged may be the "argue why this is worth adding": let me say a few things about that below.

[Michael Rothgang]

First off: I agree that in general, one should be careful with such equivalences. If you need those, you may be proving the wrong thing. (One example: if I only considered manifolds modeled on EuclideanSpace R (Fin n), then taking product manifolds suddenly means I need to identify R^n times R^m with R^{m+n} --- whereas the "correct abstract" way is to speak about ModelProd and product types.)

That said: this is the third application I've seen of this isomorphism.

1. You need such an equivalence to define the ring structure on the bordism groups (of a point): the product of an n and an m-bordism class is an n+m-bordism class --- hence, a 5-bordism class can be a 1-class times a 4-class, or a 2-class times a 3-class, etc. To even say what these bordism classes are, you need to fix a preferred model with corners for each dimension, such as the standard model with corners on Euclidean space. But then, you need to identity R^n times R^m with R^{n+m} to make this palatable.
   (I have not formalised this in detail, but #23138 comes close: if pressed, I could certainly state this in Lean and show where this comes in.)

2. You need such an equivalence to say "if n \leq m, R^n is a submanifold of R^m". (See #24549 for some work in progress). To say "N is a submanifold of M" entails a condition on the respective models with corners (them being a SliceModel, cf. #24550) plus further conditions on how N is embedded into M. Constructing a slice model instance (for the standard model with corners on R^n and R^m) boils down to an equivalence of R^n \times R^{m-n} and R^m.

3. (by Ben Eltschig, see below)
   To define the site on which e.g. diffeological spcaes and smooth sets are defined, one would like to define a category whose objects are the spaces EuclideanSpace ℝ (Fin n). The easiest way to prove that it has all finite products is to work with a continuous linear equivalence between the actual product and EuclideanSpace ℝ (Fin (n + m).
   3'. The above code uses this, to argue the Möbius bundle is a charted space over R². (Here, a good question is whether this is strictly required.)

[Michael Rothgang]

@Dominic Steinitz Thinking about the third application --- do you actually need that instance? Or could you just prove that the total space is a manifold modelled on EuclideanSpace R 1 \times EuclideanSpace R 1?

[Michael Rothgang]

@Ben Eltschig You also mentioned you were interested in such an equivalence of charted spaces. Do you remember why you wanted them? It certainly helps to collect use cases here.

[Ben Eltschig]

I defined a category with objects the spaces EuclideanSpace ℝ (Fin n) here and wanted to show that it has all finite products - the easiest way I found to do that was to work with a continuous linear equivalence between the actual product and EuclideanSpace ℝ (Fin (n + m)). You can still find that equivalence at line 126 there in fact.

[Ben Eltschig]

The broader context is that that category is the site on which e.g. diffeological spaces and smooth sets are defined, and showing that it has all finite products is one of the things needed to prove that it is cohesive

[Michael Rothgang]

Thanks, that helps! I've edited my post to include your application.

[Ben Eltschig]

Also worth noting that counterarguments like "just work with all finite-dimensional normed spaces instead" don't apply here because the site needs to be small to prevent an unnecessary universe bump

[Eric Wieser]

Does Fin (n + m) vs Fin n ⊕ Fin m matter here? Does Fin n versus an arbitrary Fintype I matter?

[Michael Rothgang]

My first two applications certainly need Fin n, Fin m and Fin (n+m). (I'm not 100% sure what you question is, but does this answer it?)

[Ben Eltschig]

My application also needs the types Fin n as index types specifically, because if my objects were Fintype ℝ I for general fintypes I it would again be a large site (unless type theory works different than set theory here? I don't know).

[Notification Bot]

12 messages were moved here from #Geographic locality > London, England by Kevin Buzzard.

[Kevin Buzzard]

(@Dominic Steinitz I moved the discussion to somewhere which will be far more findable in future)

[Dominic Steinitz]

Kevin Buzzard said:

(Dominic Steinitz I moved the discussion to somewhere which will be far more findable in future)

Thank you :thank_you:

[Eric Wieser]

Every fintype is (noncanonically) isomorphic to Fin n for some n, so there should be no universe bump either way

[Ben Eltschig]

The site would still be essentially small, yes. But does that really mean we can consider sheaves on it instead of the small skeleton? I thought there were still some size issues then

[Ben Eltschig]

My understanding is that equivalent sites yield equivalent sheaf topoi, not isomorphic ones - and in the case of a large site that is equivalent to a small site, the sheaf topos on the large site would still be one universe up from the equivalent sheaf topos on the small site

[Ben Eltschig]

looking at the universe levels in CategoryTheory.Sheaf though, you're right that there would be no universe bump there. I haven't thought through whether there are other reasons to work with the small site instead of the large one, but at least isn't one.

[Ben Eltschig]

Sorry for derailing the discussion a bit with this, but I don't think we even have e.g. completeness of sheaves on essentially small sites yet? See here. I assume that can be solved with just a bit more API, but it's at least one reason to work with small sites for now.

[Ben Eltschig]

Actually, apparently we do have it as docs#CategoryTheory.hasLimitsEssentiallySmallSite, but it isn't found in the above example?

[Ben Eltschig]

... and now I see that that's again on me for having asked for HasLimits instead of HasLimitsOfSize.{0,0} in that example. Sorry for all the confusion, I guess this really only shows that I haven't thought about the precise size constraints surrounding sheaves enough.

[Michael Rothgang]

Michael Rothgang said:

Thanks for the ping! I think an equivalence between Euclidean space could be worth PRing to mathlib. Would you like to make a PR? The hardest part of getting it merged may be the "argue why this is worth adding": let me say a few things about that below.

I made such a PR in #25524

[Dominic Steinitz]

Thanks for doing this. It was on my action list and didn't seem that urgent but now I can cross it off :-)

With respect to your question: #mathlib4 > Manifold structure on Moebius strip @ 💬 : it depends what you mean by need. I think saying the Möbius strip is locally $\mathbb{R}^2$ is how most people would think of it rather than locally it is the product $\mathbb{R} \times \mathbb{R}$ although they are the "same" thing.

[Michael Rothgang]

Sure: I was wondering "is there a Lean reason you absolute need R² here" (as opposed to "looks more familiar to humans" --- though I would argue that on paper, R² and $\mathbb{R}\times\mathbb{R}$ are really considered the same, so I wouldn't worry about this detail). I gather the answer is no --- which seems different than for my use case above.

[Dominic Steinitz]

As a little coda, I managed to prove the Möbius strip is a smooth vector bundle:

#synth IsManifold ((𝓡 1).prod (𝓡 1)) ⊤ (TotalSpace (EuclideanSpace ℝ (Fin 1)) MobiusAsVectorBundle.Fiber)

But

#synth IsManifold (𝓡 2) ⊤ (TotalSpace (EuclideanSpace ℝ (Fin 1)) MobiusAsVectorBundle.Fiber)

fails even though

#synth IsManifold (𝓡 2) 0 (TotalSpace (EuclideanSpace ℝ (Fin 1)) MobiusAsVectorBundle.Fiber)

succeeds.