A First Stab at a Principal Fibre Bundle

Stream: Is there code for X?

[Dominic Steinitz]

I have this so far. I'd like to prove that the frame bundle is a principal bundle for example. I am starting on the right lines?

import Mathlib

open Manifold

open SmoothManifoldWithCorners

open MulAction

open Bundle

example {G B : Type*} {E : B → Type*} (k n : ℕ)
[TopologicalSpace B]
[ChartedSpace (EuclideanSpace ℝ (Fin n)) B]
[TopologicalSpace G]
[ChartedSpace (EuclideanSpace ℝ (Fin k)) G]
[Group G]
[MulAction G P]
[TopologicalGroup G]
[TopologicalSpace (TotalSpace G E)]
[(b : B) → TopologicalSpace (E b)]
[LieGroup (𝓡 k) G]
[FiberBundle G E] (g g': G) (p : P)
(h_free : stabilizer G p = ⊥) :
  true := by
    -- Just things we know to be true for an action
    have h1 : g • (g' • p) = (g * g') • p := by apply (mul_smul g g' p).symm
    have h2 : (1 : G) • p = p := by apply one_smul
    sorry

[Winston Yin (尹維晨)]

Hi Dominic, a formalisation of the principal bundle would be a significant addition to mathlib, in my opinion, and I'll be excited to see it. Have you had a look at the design of FiberBundle and VectorBundle? I would imagine that you should first define PrincipalBundle in a similar way to FiberBundle and VectorBundle, perhaps with an associated PrincipalBundleCore. I cannot claim to understand the existing structures fully.

Once you have PrincipalBundle, you can construct frameBundle as a term of it. This is analogous to the tangentBundleCore and tangentBundle construction as a vector bundle. I'm afraid this is not as simple as a single theorem. I assume there are people here (e.g. @Heather Macbeth) who may be interested in this and have some ideas.

[Winston Yin (尹維晨)]

Looking at your code, I would also suggest generalising beyond Euclidean spaces when working in mathlib. While it may be more convenient in informal mathematics, in mathlib you will be constantly applying more general theorems, such as those for NormedAddCommGroup. Carrying EuclideanSpace ℝ (Fin n) around then becomes a distraction rather than a simplification. In the same spirit, we try to state manifold results for general 𝕜 manifolds, where 𝕜 is a NontriviallyNormedField, such as the real or complex numbers. You can glean these from e.g. docs#VectorBundleCore.

Another comment is that I am confused by the : true in your code. A theorem is stated with hypotheses before : and the intended goal after :. When we write a proof of a theorem, we try to manipulate the goal until it essentially turns into true in the very last step. Starting with true as the goal is very much backwards.

One more comment. This is something I learnt over time. In informal mathematics, "these things with this binary operation form a group" is stated as a theorem. In mathlib, a lot of these statements are stated not as theorems (using the keyword theorem or lemma) but as constructions of terms of a type (using the keyword def or instance). If you already have a type called MyThings, then showing it is a group involves constructing a term of type Group MyThings, where you provide the binary relation in the mul field of Group and prove that it satisfies all the axioms in the other fields of Group.

I found #tpil very helpful for this kind of thing.

[Winston Yin (尹維晨)]

Oh, and people are probably slow to respond this week due to the Lean Together conference.

[Michael Rothgang]

I can confirm: I was excited to see that you want to formalise principal fibre bundles, but didn't have time so far to respond. Everything Winston says sounds reasonable to me.

[Dominic Steinitz]

I will respond to your points but it is going to take me a few days. But a quick question first: I looked at the links you gave and get the impression that a vector bundle is a stand alone definition whereas I would have expected a vector bundle to be a fibre bundle where the fibres are vector spaces.

[Dominic Steinitz]

I have probably misunderstood as I am new to lean and to Mathlib in particular.

[Michael Rothgang]

A vector bundle is a fibre bundle - both mathematically and in mathlib. If you look at docs#VectorBundle, you'll see [FiberBundle F E], showing that a vector bundle is a fibre bundleF with additional properties (such as its fibres being vector spaces, and the existence of a system of linear trivialisations).

[Winston Yin (尹維晨)]

I haven't thought much about the design space there, but one can imagine VectorBundle extending FiberBundle with additional fields, rather than requiring FiberBundle as an assumption as in mathlib now.

[Winston Yin (尹維晨)]

I suspect this choice might have something to do with docs#MemTrivializationAtlas, which is used in the definition of VectorBundle and whose own definition requires FiberBundle as an assumption. But then I don't understand why we need MemTrivializationAtlas to begin with. If VectorBundle directly extended FiberBundle, then it would be easy to say e ∈ trivializationAtlas' directly without invoking typeclass inference.

[Dominic Steinitz]

Winston Yin (尹維晨) said:

Another comment is that I am confused by the : true in your code. A theorem is stated with hypotheses before : and the intended goal after :. When we write a proof of a theorem, we try to manipulate the goal until it essentially turns into true in the very last step. Starting with true as the goal is very much backwards.

I quite often work backwards (and also forwards). Here I was trying to show that

$p \sim q: \Leftrightarrow \exists g \in G: q=g \triangleright p$

is an equivalence relation but I didn't know how to express that something is an equivalence relation in Lean so I just put true for the theorem and I was going to fill it in later.

It turns out that I don't need this anyway as Lean has already defined orbits (the equivalence classes of the relation).

So up to now I have an example

import Mathlib

open MulAction

instance : MulAction Circle (Fin 2 -> ℝ) where
  mul_smul _ _ _ := sorry
  smul := sorry
  one_smul _ := sorry

example (x : Fin 2 → ℝ) (ξ : Fin 2 → ℝ) :
  x ∈ orbit Circle ξ → (x 0)^2 + (x 1)^2 = (ξ 0)^2 + (ξ 1)^2 := sorry

example (h : Circle) (x : Fin 2 → ℝ) : x ≠ 0 → h ∈ stabilizer Circle x → h = 1 := sorry

I have proofs but I think posting them would obscure rather than enlighten. Of course, I haven't yet proved that $\mathbb{R}^2 \ (0,0)$ is a bundle or that the action is smooth or that it satisfies the requirements to be a principal bundle (which I haven't yet defined).

[Dominic Steinitz]

Winston Yin (尹維晨) said:

Looking at your code, I would also suggest generalising beyond Euclidean spaces when working in mathlib. While it may be more convenient in informal mathematics, in mathlib you will be constantly applying more general theorems, such as those for NormedAddCommGroup. Carrying EuclideanSpace ℝ (Fin n) around then becomes a distraction rather than a simplification. In the same spirit, we try to state manifold results for general 𝕜 manifolds, where 𝕜 is a NontriviallyNormedField, such as the real or complex numbers. You can glean these from e.g. docs#VectorBundleCore.

I was going to generalise after I had managed to work things out for manifolds which are locally Euclidean. I think you are saying it is going to be easier to not think that but that manifolds are locally $\mathbb{k}$ (with some constraint on the $\mathbb{k}$)?

[Dominic Steinitz]

Michael Rothgang said:

A vector bundle is a fibre bundle - both mathematically and in mathlib. If you look at docs#VectorBundle, you'll see [FiberBundle F E], showing that a vector bundle is a fibre bundleF with additional properties (such as its fibres being vector spaces, and the existence of a system of linear trivialisations).

Yes of course - somehow I missed the Mathlib definition of a vector bundle which I then found and yes as you point out it captures the fact that a vector bundle is a fibre bundle (what else could it be).

I looked at this https://github.com/leanprover-community/mathlib4/blob/68ea7d25dcbdd9f46072adf8927a684d4194abbb/Mathlib/Topology/VectorBundle/Basic.lean#L354. I expected to see something like below but didn't look at the declarations above (my bad). So I should look at the docs not just the code.

class VectorBundle(R : Type u_1) {B : Type u_2} (F : Type u_3) (E : B → Type u_4) [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] :
Prop

But now I have another question: there is no explicit vector space but instead a module [(x : B) → Module R (E x)] with a non-trivially normed field [NontriviallyNormedField R] (and thus a vector space). What is the advantage of defining the vector space implicitly?

[Michael Rothgang]

Well, if k is a field, then a k-vector space is precisely a k-module, right? Mathlib doesn't have a concept of "vector space", it only has "modules over a ring". So, instead of saying "\R-vector space", mathlib theorems say "\R-module" (which is the same thing).

[Michael Rothgang]

Granted: this (vector spaces = k-modules) might take getting used to.

[Winston Yin (尹維晨)]

And mathlib's manifolds are locally 𝕜-module. This generalises "locally Euclidean" (finite-dimensional real manifolds) to accommodate complex manifolds, infinite-dimensional real/complex manifolds, and even manifolds where the field 𝕜 is the p-adic numbers. Many proofs for locally Euclidean manifolds can be trivially generalised to these other cases. Where they cannot (such as when a finite coordinate system is needed), we have not developed much specialised theory in mathlib yet.

[Winston Yin (尹維晨)]

I think the Wikipedia article on the principal bundle actually gives a definition corresponding to VectorBundle, namely a FiberBundle with some extra properties. The definition of PrincipalBundleCore (corresponding to VectorBundleCore) would be some gluing procedure compatible with the group action. Then, the frame bundle can be constructed using what becomes of PrincipalBundleCore.

[Dominic Steinitz]

I'd prefer to use the definition that $\pi : P \rightarrow M$ is isomorphic as a bundle to $\rho : P \rightarrow P/G$ where $\rho$ is the quotient map and then derive the properties in the Wikipedia article but let's see how we go.

[Winston Yin (尹維晨)]

I think that's a good exercise to see how one makes design choices when formalising. My suggestion is based on the following considerations. FiberBundle(Core) and VectorBundle(Core) are complex objects that already exist on mathlib and can be modelled after. If your goal is to define the frame bundle as a fibre bundle, you have to put a topology on the total space, which probably involves gluing between patches. This already is the procedure for obtaining PrincipalBundleCore, which leads to the kind of PrincipalBundle that is analogous to VectorBundle. It makes things easier especially if you're learning the API while making design choices in your formalisation.

If you do pursue your preferred approach, you will first need to define bundle morphisms and quotient manifolds, both of which are not in mathlib and probably involve their own design choices.

By the way, in mathlib, you don't have to show that a relation is an equivalence relation to define a quotient type. If you use a non-equivalence relation r, the quotient is simply taken with respect to the equivalence relation generated by r, namely collapsing each disjoint orbit of r into a point.

[Dominic Steinitz]

Thanks very much. I was just about to and look for bundle morphisms and quotient manifolds. I don't think Wikipedia is the last word on what is a principal bundle. There are at least two approaches that I know of that allow the definition without using bundle morphisms and quotient manifolds. I will follow your suggestion and thanks again for saving me work :sweat_smile:

[Michael Rothgang]

I think mathlib should learn about quotient manifolds. I would be surprised, though, if doing entails not learning surprising new things about how to design things. (Unless you're a Lean expert on everything, which I think neither you or me are.) In the short term, avoiding them seems certainly less a more pleasant strategy.

[Winston Yin (尹維晨)]

Thanks for asking these questions, Dominic. I've learnt a few things myself having to look through the library.

[Dominic Steinitz]

Does this look I am headed in the right direction?

structure GBundleCore (ι : Type*) (B : Type*) [TopologicalSpace B] (F : Type*)
    [TopologicalSpace F] [Group G] [MulAction G F] where
  baseSet : ι → Set B
  isOpen_baseSet : ∀ i, IsOpen (baseSet i)
  indexAt : B → ι
  mem_baseSet_at : ∀ x, x ∈ baseSet (indexAt x)
  coordChange : ι → ι → B → F → F
  coordChange_self : ∀ i, ∀ x ∈ baseSet i, ∀ v, coordChange i i x v = v
  continuousOn_coordChange : ∀ i j,
    ContinuousOn (fun p : B × F => coordChange i j p.1 p.2) ((baseSet i ∩ baseSet j) ×ˢ univ)
  coordChange_comp : ∀ i j k, ∀ x ∈ baseSet i ∩ baseSet j ∩ baseSet k, ∀ v,
    (coordChange j k x) (coordChange i j x v) = coordChange i k x v
  coordChange_strucuture_group : ∀ i j, ∀ x ∈ baseSet i ∩ baseSet j, ∀ v, ∃ g : ι → ι → B → F → G, coordChange i j x v = g i j x v • v

I think with this I should be able to define the Möbius band as a G-bundle with structure group $\{1, -1\}$.

[Michael Rothgang]

So a G-bundle is a principal fibre bundle with structure group G? (If so, I would use the latter term. But this is nit-picking: first get the definitions right; names are easy to change.)

[Michael Rothgang]

(I'll try to take a closer look soon; it's late over here now.)

[Scott Carnahan]

Do you mean to say that the Möbius band is the base space of a {1,-1}-bundle with total space S^1 x [0,1] (i.e. its orientation double cover)?

[Dominic Steinitz]

Scott Carnahan said:

Do you mean to say that the Möbius band is the base space of a {1,-1}-bundle with total space S^1 x [0,1] (i.e. its orientation double cover)?

I am saying that the Möbius band has a base space $S^1$ with fiber $\mathbb{R}$ and a structure group the two element group $\{e, a\}$ with $a * a = e$ (aka $\mathbb{Z}/2\mathbb{Z}$). This is not a principal bundle (I don't think you said that but I wanted to note it). I have yet to define a principal bundle (the group action is free and transitive).

[Dominic Steinitz]

Michael Rothgang said:

So a G-bundle is a principal fibre bundle with structure group G? (If so, I would use the latter term. But this is nit-picking: first get the definitions right; names are easy to change.)

I meant the other way round: a principal g-bundle is a g-bundle with conditions (the action is free and transitive).

[Winston Yin (尹維晨)]

I see that you're trying to say that the coordChange function is a G-action on the fibre F. What you probably meant to write is

coordChange_structure_group : ∀ i j, ∀ x ∈ baseSet i ∩ baseSet j,
  ∃ g : G, ∀ v : F, coordChange i j x v = g • v

That is, at each point x : B the transition function from F to F is the action by a group element g. What you wrote seems to mean that at the same base point x, each element of the fibre v : F can be mapped by a different g, which would make the transition map not a group action by G on F in general.

[Winston Yin (尹維晨)]

Then I think we are making some progress. It'll allow us to interpret the same vector bundle as a G-bundle for different groups G, for example subgroups of a larger group, or groups with shared representations such as SO(3) and SU(2).

[Winston Yin (尹維晨)]

For defining PrincipalBundleCore, you first have to add [TopologicalGroup G]. You can add an additional field for another right-action by G on the fibres that is continuous on B × F, and that this right-action is free and transitive and induces homeomorphisms between F and G.

[Dominic Steinitz]

Suppose we have two local trivialisations $\phi_i : \pi^{-1}(U_i) \longrightarrow U_i \times F$ and $\phi_j : \pi^{-1}(U_j) \longrightarrow U_i \times F$ then $p \mapsto (\pi(p),f_i(p))$ for some $f_i : \pi^{-1}(x) \longrightarrow F$ and correspondingly for $j$.

We have for a fibre $\pi^{-1}(x)$, $f_j \circ f_i^{-1} : F \longrightarrow F$ and we suppose that this homeomorphism (or diffeo) is the left action of an element $g_{ij}(x)$, that is, $f_i(p) = g_{ij}(x) \bullet f_j(x)$ then the bundle is a $G$-bundle.

So I think we need

coordChange_structure_group : ∀ i j, ∀ x ∈ baseSet i ∩ baseSet j,
  ∃ g : ι → ι → B → G, ∀ v : F, coordChange i j x v = g i j x • v

[Winston Yin (尹維晨)]

This would be right if you pull the “exists g” before “forall i j”

[Winston Yin (尹維晨)]

Which would be equivalent to what I suggested, up to usage of axiom of choice

[Winston Yin (尹維晨)]

Among these equivalent statements, I recommend the one where the existence proof obligation is the simplest. Showing the existence of a single g is easier than constructing a function from loads of different g.

[Dominic Steinitz]

Winston Yin (尹維晨) said:

Among these equivalent statements, I recommend the one where the existence proof obligation is the simplest. Showing the existence of a single g is easier than constructing a function from loads of different g.

Ok now I am convinced :thumbs_up:

[Dominic Steinitz]

I think the möbius strip as an example means expressing it as a quotient manifold and they do not yet exist in Mathlib. This example typechecks so when I get time I will try filling in the methods (not sure what the Lean term for these are).

structure GBundleCore (ι : Type*) (B : Type*) [TopologicalSpace B] (F : Type*)
    [TopologicalSpace F] [Group G] [MulAction G F] where
  baseSet : ι → Set B
  isOpen_baseSet : ∀ i, IsOpen (baseSet i)
  indexAt : B → ι
  mem_baseSet_at : ∀ x, x ∈ baseSet (indexAt x)
  coordChange : ι → ι → B → F → F
  coordChange_self : ∀ i, ∀ x ∈ baseSet i, ∀ v, coordChange i i x v = v
  continuousOn_coordChange : ∀ i j,
    ContinuousOn (fun p : B × F => coordChange i j p.1 p.2) ((baseSet i ∩ baseSet j) ×ˢ univ)
  coordChange_comp : ∀ i j k, ∀ x ∈ baseSet i ∩ baseSet j ∩ baseSet k, ∀ v,
    (coordChange j k x) (coordChange i j x v) = coordChange i k x v
  coordChange_structure_group : ∀ i j, ∀ x ∈ baseSet i ∩ baseSet j, ∃ g : G, ∀ v : F, coordChange i j x v = g • v

instance : MulAction (⊥ : Subgroup Circle) ℝ where
  smul _ x := x
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

#check GBundleCore (⊥ : Subgroup Circle) (atlas (EuclideanSpace ℝ (Fin 1)) Circle) Circle ℝ

[Winston Yin (尹維晨)]

Could you please describe in words what structure your #check is meant to describe? What's the base space, fibre, and so on.

[Dominic Steinitz]

The base space is the circle, the fibre is the real line and the group is the trivial group just containing the identity. Here's what I have so far:

import Mathlib

open Bundle Topology MulAction Set

variable (R : Type*) {B : Type*} (F : Type*) (E : B → Type*) (G : Type*)

variable [NontriviallyNormedField R] [∀ x, AddCommMonoid (E x)] [∀ x, Module R (E x)]
  [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [TopologicalSpace (TotalSpace F E)]
  [∀ x, TopologicalSpace (E x)] [FiberBundle F E] [Group G] [MulAction G P]

structure GBundleCore (ι : Type*) (B : Type*) [TopologicalSpace B] (F : Type*)
    [TopologicalSpace F] [Group G] [MulAction G F] where
  baseSet : ι → Set B
  isOpen_baseSet : ∀ i, IsOpen (baseSet i)
  indexAt : B → ι
  mem_baseSet_at : ∀ x, x ∈ baseSet (indexAt x)
  coordChange : ι → ι → B → F → F
  coordChange_self : ∀ i, ∀ x ∈ baseSet i, ∀ v, coordChange i i x v = v
  continuousOn_coordChange : ∀ i j,
    ContinuousOn (fun p : B × F => coordChange i j p.1 p.2) ((baseSet i ∩ baseSet j) ×ˢ univ)
  coordChange_comp : ∀ i j k, ∀ x ∈ baseSet i ∩ baseSet j ∩ baseSet k, ∀ v,
    (coordChange j k x) (coordChange i j x v) = coordChange i k x v
  coordChange_structure_group : ∀ i j, ∀ x ∈ baseSet i ∩ baseSet j, ∃ g : G, ∀ v : F, coordChange i j x v = g • v

instance : MulAction (⊥ : Subgroup Circle) ℝ where
  smul _ x := x
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

instance : HSMul (⊥ : Subgroup Circle) ℝ ℝ where
  hSMul g x := g • x

#synth HSMul (⊥ : Subgroup Circle) ℝ ℝ

/- Let's try this out with the circle as the base space, the real line as the fibre and the trivial group
(the only element is the identity) which btw shows that this is a trivial bundle. With the möbius bundle,
when we are able to specify it, the structure group would have to contain 2 elements to capture the twist.
 -/

#check GBundleCore
#check GBundleCore (⊥ : Subgroup Circle)
#check GBundleCore (⊥ : Subgroup Circle) (atlas (EuclideanSpace ℝ (Fin 1)) Circle)
#check GBundleCore (⊥ : Subgroup Circle) (atlas (EuclideanSpace ℝ (Fin 1)) Circle) Circle
#check GBundleCore (⊥ : Subgroup Circle) (atlas (EuclideanSpace ℝ (Fin 1)) Circle) Circle ℝ

-- Currently I am stuck. I have given an instance of HSMul but Lean seems to be ignoring it
theorem bar : ∀ (b : GBundleCore (⊥ : Subgroup Circle) (atlas (EuclideanSpace ℝ (Fin 1)) Circle) Circle ℝ),
              ∀ (i j : ↑(atlas (EuclideanSpace ℝ (Fin 1)) Circle)),
  ∀ x ∈ univ, ∃ (g : Circle), ∀ (v : ℝ), GBundleCore.coordChange b i j x v = g • v := by
    sorry

noncomputable
def foo : GBundleCore (⊥ : Subgroup Circle) (atlas (EuclideanSpace ℝ (Fin 1)) Circle) Circle ℝ :=
  { baseSet := λ _ => univ
    isOpen_baseSet := λ _ => isOpen_univ
    indexAt := sorry
    mem_baseSet_at := λ x => mem_univ x
    coordChange := λ _ _ _ => ContinuousLinearMap.id ℝ ℝ
    coordChange_self := λ _ _ _ _ => rfl
    continuousOn_coordChange := sorry
    coordChange_comp := λ _ _ _ _ _ _ => rfl
    coordChange_structure_group := sorry
    }

#lint

[Winston Yin (尹維晨)]

I might be missing something but whey does your #check have four arguments when GBundleCore has 3?

[Winston Yin (尹維晨)]

iota, B, and F

[Winston Yin (尹維晨)]

(I’m on mobile. Sorry about the formatting)

[Dominic Steinitz]

Is G an implicit variable? We use it in the definition but it is not defined in the definition itself but further up the file.

variable (R : Type*) {B : Type*} (F : Type*) (E : B → Type*) (G : Type*)

[Dominic Steinitz]

I think my example is wrong - it should not have ContinuousLinearMap as that pertains to vector bundles and we want fiber bundles. I am still trying to work out how to write the simple example of the base space being a circle and the fibres being the real line (with no twists).

[Winston Yin (尹維晨)]

I see! I missed the variable declaration earlier. This is why, for structures in mathlib, we tend to write the full list of arguments inside the structure declaration itself, even if they’ve already been declared earlier in the file.

[Winston Yin (尹維晨)]

Could you rewrite it in that form? The code you shared above is a bit confusing, in that B and F are repeated in the structure declaration but R and G are not

[Dominic Steinitz]

I hadn't fully internalised Lean's "implicit variables" (if that is what they are called) but they seem to be a common idiom. I agree having all variables bound is much easier to understand. Here's the "no free variables" version:

import Mathlib

open Bundle Topology MulAction Set

structure GBundleCore (ι : Type*) (B : Type*) [TopologicalSpace B] (F : Type*)
    [TopologicalSpace F] (G : Type*) [Group G] [MulAction G F] where
  baseSet : ι → Set B
  isOpen_baseSet : ∀ i, IsOpen (baseSet i)
  indexAt : B → ι
  mem_baseSet_at : ∀ x, x ∈ baseSet (indexAt x)
  coordChange : ι → ι → B → F → F
  coordChange_self : ∀ i, ∀ x ∈ baseSet i, ∀ v, coordChange i i x v = v
  continuousOn_coordChange : ∀ i j,
    ContinuousOn (fun p : B × F => coordChange i j p.1 p.2) ((baseSet i ∩ baseSet j) ×ˢ univ)
  coordChange_comp : ∀ i j k, ∀ x ∈ baseSet i ∩ baseSet j ∩ baseSet k, ∀ v,
    (coordChange j k x) (coordChange i j x v) = coordChange i k x v
  coordChange_structure_group : ∀ i j, ∀ x ∈ baseSet i ∩ baseSet j, ∃ g : G, ∀ v : F, coordChange i j x v = g • v

/- Let's try this out with the circle as the base space, the real line as the fibre and the trivial group
(the only element is the identity) which btw shows that this is a trivial bundle. With the möbius bundle,
when we are able to specify it, the structure group would have to contain 2 elements to capture the twist.
 -/

instance trivialMulAction : MulAction (⊥ : Subgroup Circle) ℝ where
  smul _ x := x
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

instance : MulAction Circle ℝ where
  mul_smul _ _ _ := sorry
  smul := sorry
  one_smul _ := sorry

instance baz : HSMul (⊥ : Subgroup Circle) ℝ ℝ where
  hSMul g x := g • x

#synth HSMul (⊥ : Subgroup Circle) ℝ ℝ
#check @HSMul.hSMul (⊥ : Subgroup Circle) ℝ ℝ

#check GBundleCore
#check GBundleCore (atlas (EuclideanSpace ℝ (Fin 1)) Circle) Circle ℝ (⊥ : Subgroup Circle)

-- Currently I am stuck. I have given an instance of HSMul but Lean seems to be ignoring it.
--  Well this `@HSMul.hSMul (⊥ : Subgroup Circle) ℝ ℝ self g v` compiles but `g • v` does not.
theorem bar : ∀ (b : GBundleCore (atlas (EuclideanSpace ℝ (Fin 1)) Circle) Circle ℝ  (⊥ : Subgroup Circle)),
              ∀ (i j : ↑(atlas (EuclideanSpace ℝ (Fin 1)) Circle)),
              ∀ x ∈ (fun x => univ) i ∩ (fun x => univ) j,
              ∃ (g : (⊥ : Subgroup Circle)), ∀ (v : ℝ), GBundleCore.coordChange b i j x v = @HSMul.hSMul (⊥ : Subgroup Circle) ℝ ℝ self g v := by
    sorry

-- Surely altases are empty Lean seems not to think so.
instance : Nonempty (↑(atlas (EuclideanSpace ℝ (Fin 1)) Circle)) := sorry

noncomputable
def foo : GBundleCore (atlas (EuclideanSpace ℝ (Fin 1)) Circle) Circle ℝ (⊥ : Subgroup Circle) where
  baseSet _ := univ
  isOpen_baseSet _ := isOpen_univ
  indexAt := λ x => Classical.choose (Set.exists_mem_of_nonempty (atlas (EuclideanSpace ℝ (Fin 1)) Circle))
  mem_baseSet_at := mem_univ
  coordChange _ _ _ := sorry
  coordChange_self _ _ _ _ := sorry
  continuousOn_coordChange i j := sorry
  coordChange_comp _ _ _ _ _ _ := sorry
  coordChange_structure_group := sorry

[Dominic Steinitz]

When I get back later today, I will put the code in a repo then it will be easier for us both to work with.

[Dominic Steinitz]

@Winston Yin (尹維晨) At the moment I am baffled as to what to put into coordChange_structure_group. I feel it ought to be

∀ i j, ∀ x ∈ baseSet i ∩ baseSet j, ∃ g : G, ∀ v : F, coordChange i j x v = g • v

But Lean seems to think it should be

sorry : ∀ (i j : ↑(atlas (EuclideanSpace ℝ (Fin 1)) Circle)),
  ∀ x ∈ (fun x => univ) i ∩ (fun x => univ) j, ∃ g, ∀ (v : ℝ), (fun x x x => id) i j x v = g • v

fun x x x I don't understand.

Anyway here is a working (or rather not working) full example.

import Mathlib

open Bundle Topology MulAction Set

structure GBundleCore (ι : Type*) (B : Type*) [TopologicalSpace B] (F : Type*)
    [TopologicalSpace F] (G : Type*) [Group G] [MulAction G F] where
  baseSet : ι → Set B
  isOpen_baseSet : ∀ i, IsOpen (baseSet i)
  indexAt : B → ι
  mem_baseSet_at : ∀ x, x ∈ baseSet (indexAt x)
  coordChange : ι → ι → B → F → F
  coordChange_self : ∀ i, ∀ x ∈ baseSet i, ∀ v, coordChange i i x v = v
  continuousOn_coordChange : ∀ i j,
    ContinuousOn (fun p : B × F => coordChange i j p.1 p.2) ((baseSet i ∩ baseSet j) ×ˢ univ)
  coordChange_comp : ∀ i j k, ∀ x ∈ baseSet i ∩ baseSet j ∩ baseSet k, ∀ v,
    (coordChange j k x) (coordChange i j x v) = coordChange i k x v
  coordChange_structure_group : ∀ i j, ∀ x ∈ baseSet i ∩ baseSet j, ∃ g : G, ∀ v : F, coordChange i j x v = g • v

/- Let's try this out with the circle as the base space, the real line as the fibre and the trivial group
(the only element is the identity) which btw shows that this is a trivial bundle. With the möbius bundle,
when we are able to specify it, the structure group would have to contain 2 elements to capture the twist.
 -/

instance trivialMulAction : MulAction (⊥ : Subgroup Circle) ℝ where
  smul _ x := x
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

instance : MulAction Circle ℝ where
  mul_smul _ _ _ := sorry
  smul := sorry
  one_smul _ := sorry

instance baz : HSMul (⊥ : Subgroup Circle) ℝ ℝ where
  hSMul g x := g • x

#synth HSMul (⊥ : Subgroup Circle) ℝ ℝ
#check @HSMul.hSMul (⊥ : Subgroup Circle) ℝ ℝ

#check GBundleCore
#check GBundleCore (atlas (EuclideanSpace ℝ (Fin 1)) Circle) Circle ℝ (⊥ : Subgroup Circle)

-- Surely altases are empty Lean seems not to think so.
instance : Nonempty (↑(atlas (EuclideanSpace ℝ (Fin 1)) Circle)) := sorry

noncomputable
def foo : FiberBundleCore (atlas (EuclideanSpace ℝ (Fin 1)) Circle) Circle ℝ where
  baseSet _ := univ
  isOpen_baseSet _ := isOpen_univ
  indexAt := λ x => Classical.choose (Set.exists_mem_of_nonempty (atlas (EuclideanSpace ℝ (Fin 1)) Circle))
  mem_baseSet_at := mem_univ
  coordChange _ _ _ := id
  coordChange_self _ _ _ _ := rfl
  continuousOn_coordChange i j := continuous_snd.continuousOn
  coordChange_comp _ _ _ _ _ _ := rfl

noncomputable
def hoo : GBundleCore (atlas (EuclideanSpace ℝ (Fin 1)) Circle) Circle ℝ (⊥ : Subgroup Circle) where
  baseSet _ := univ
  isOpen_baseSet _ := isOpen_univ
  indexAt := λ x => Classical.choose (Set.exists_mem_of_nonempty (atlas (EuclideanSpace ℝ (Fin 1)) Circle))
  mem_baseSet_at := mem_univ
  coordChange _ _ _ := id
  coordChange_self _ _ _ _ := rfl
  continuousOn_coordChange i j := continuous_snd.continuousOn
  coordChange_comp _ _ _ _ _ _ := rfl
  coordChange_structure_group := sorry

[Ruben Van de Velde]

Can you dsimp only to get rid of the funs?

[Winston Yin (尹維晨)]

I'm sorry that I may not be able to answer all your questions or dive into the details, but I can point out various things as I see them, so you can be on the right track, both in terms of the goal at hand and generally getting used to Lean/mathlib.

[Winston Yin (尹維晨)]

variable (a : ...) (b : ...) (c : ...)

def myDefinition (d : ...) (e : ...) : ... := ...

is equivalent to

def myDefinition (a : ...) (b : ...) (c : ...) (d : ...) (e : ...) : ... := ...

where everything declared by variable comes first. If the variables repeat, then the later ones supersede the earlier ones:

variable (a : ...) (b : ...) (c : ...)

def myDefinition (a : ...) (d : ...) : ... := ...

is equivalent to

def myDefinition (b : ...) (c : ...) (a : ...) (d : ...) : ... := ...

Suppose the definition doesn't refer to c at all, then Lean automatically omits it from the type ascription of myDefinition, so you get instead

def myDefinition (b : ...) (a : ...) (d : ...) : ... := ...

[Winston Yin (尹維晨)]

By explicit/implicit variables, we don't mean whether they're declared using variable. We mean whether they're declared (in either places) using (a : ...) or {a : ...} or [a : ...]. The round brackets are explicit variables that must be provided whenever the function/theorem is used. The curly brackets are implicit variables that can be inferred from other explicit/implicit variables, so they don't need to be provided when you use the function/theorem. The square brackets are typceclass implicit, meaning that they are inferred (synthesised) automatically through the typeclass system; they can also be simplified to [...] directly without a variable name.

[Winston Yin (尹維晨)]

Now onto the maths.

GBundleCore (atlas (EuclideanSpace ℝ (Fin 1)) Circle) Circle ℝ (⊥ : Subgroup Circle)

seems a little confused to me. The last argument G is meant to be the group that acts on the fibre F. In this case, you want it to be the trivial group acting on the reals. Why did you choose the trivial subgroup of the circle for this? The group that acts on the fibre has little to do with the underlying base space. This confusion is why you had to define an instance for trivialMulAction. The MulAction Circle ℝ is also confused mathematically.

What you should've done is to find an existing group that has a MulAction on the reals. For example, the group of non-zero reals acting by multiplication. The structure group could be the whole group, or any of its subgroups including the trivial subgroup. The way mathlib spells this is ℝˣ, or equivalently, Units ℝ. When you end up defining the Möbius strip, you can then use the subgroup of ℝˣ generated by -1.

My intuition tells me that it's not good design to define the trivial circular band or the Möbius strip by explicitly stating the structure subgroup in the type ascription. Instead, use the full group ℝˣ along with another predicate that states that all the transition functions belong to a certain subgroup of ℝˣ.

[Winston Yin (尹維晨)]

In the definition foo, you are trying to construct a fibre bundle on Circle with fibre ℝ. Since this is trivial, you only need one baseSet, which of course is the whole circle univ. The way this works is that indexAt tells us which point maps to which index, and baseSet tells us which index maps to which subset of the circle. The index set/type is specified as part of the type ascription, and you wrote atlas (EuclideanSpace ℝ (Fin 1)) Circle there. Recall that the atlas on the circle consists of two charts, each omitting a single point. This is mathematically at odds with your simple one-base-space definition of the fibre bundle, which is probably why you resorted to Classical.choose. There are two remedies.

The first is to stick to the one-base-set definition but stop using atlas ... Circle as your index set. You need the index set to have exactly one element. Just use for example Fin 1. Then, indexAt will just be fun _ => 0.

The second is to have the base sets align with the underlying atlas. You get to keep atlas ... Circle as the index set, but the baseSet will now directly refer to the source of the individual charts in the atlas. See the source code of docs#tangentBundleCore for this pattern.

Since your goal is to move to non-trivial examples where there are multiple base sets, I recommend the second approach.

[Winston Yin (尹維晨)]

Now onto fun x x x. This is just a quirk of Lean, which requires an explicit step to go from id a to a. If you instead say coordChange _ _ _ x := x, I'm guessing this'll go away (please verify).

[Winston Yin (尹維晨)]

Perhaps I should give a general piece of advice that passing type checks doesn't mean the statement is mathematically correct, and one should think about what each type in your formalised object actually refers to mathematically.

[Winston Yin (尹維晨)]

One more piece of advice relating to type theory. When we say "the trivial group" in informal mathematics, we mean "any single-element group". That is, we don't care what this element really is, as long as there's a group structure on it. In type theory, you need to specify what type this element is, and you usually want to choose a type that already works well with the type it is acting on. Choosing the trivial subgroup of Circle to act on the reals is not mathematically wrong per se, but it looks jarring in type theory because there is no natural action of the full Circle group on the reals.

[Dominic Steinitz]

Thanks very much for such a comprehensive reply. This type checks but as you noted in one of your replies that is no indication that the maths is correct (I am too used to type checkers preventing any infelicities). I will reply to your points later this week when I have some more time. Thanks once again.

import Mathlib

open Bundle Topology MulAction Set

structure GBundleCore (ι : Type*) (B : Type*) [TopologicalSpace B] (F : Type*)
    [TopologicalSpace F] (G : Type*) [Group G] [MulAction G F] where
  baseSet : ι → Set B
  isOpen_baseSet : ∀ i, IsOpen (baseSet i)
  indexAt : B → ι
  mem_baseSet_at : ∀ x, x ∈ baseSet (indexAt x)
  coordChange : ι → ι → B → F → F
  coordChange_self : ∀ i, ∀ x ∈ baseSet i, ∀ v, coordChange i i x v = v
  continuousOn_coordChange : ∀ i j,
    ContinuousOn (fun p : B × F => coordChange i j p.1 p.2) ((baseSet i ∩ baseSet j) ×ˢ univ)
  coordChange_comp : ∀ i j k, ∀ x ∈ baseSet i ∩ baseSet j ∩ baseSet k, ∀ v,
    (coordChange j k x) (coordChange i j x v) = coordChange i k x v
  coordChange_structure_group : ∀ i j, ∀ x ∈ baseSet i ∩ baseSet j, ∃ g : G, ∀ v : F, coordChange i j x v = g • v

/- Let's try this out with the circle as the base space, the real line as the fibre and the trivial group
(the only element is the identity) which btw shows that this is a trivial bundle. With the möbius bundle,
when we are able to specify it, the structure group would have to contain 2 elements to capture the twist.

But first we start with ℝˣ as the structure group!
 -/

noncomputable
def ioo : GBundleCore (atlas (EuclideanSpace ℝ (Fin 1)) Circle) Circle ℝ ℝˣ where
  baseSet i := i.1.source
  isOpen_baseSet i := i.1.open_source
  indexAt := achart (EuclideanSpace ℝ (Fin 1))
  mem_baseSet_at := mem_chart_source (EuclideanSpace ℝ (Fin 1))
  coordChange i j x v := v
  coordChange_self _ _ _ _ := rfl
  continuousOn_coordChange i j := continuous_snd.continuousOn
  coordChange_comp _ _ _ _ _ _ := rfl
  coordChange_structure_group := by
    intro i j x hx
    have h1 : ∃ g : ℝˣ, ∀ v : ℝ, v = g • v := by
      existsi 1
      intro v
      have h2 : (1 : ℝ) • v = v := one_smul ℝ v
      exact h2.symm
    exact h1

[Winston Yin (尹維晨)]

That looks correct to me. Now try the Möbius strip!

[Dominic Steinitz]

Winston Yin (尹維晨) said:

That looks correct to me. Now try the Möbius strip!

Just coming up with an atlas is turning out to be more work than I imagined (unless you know of some quick way of doing this). I will carry on but don't hold your breath.

[Kevin Buzzard]

Dominic I see you're currently at the "wow, formalization is much harder work than I expected" stage :-) I would be interested to hear about the problems you're facing. My naive (because I've never worked with manifolds) idea would be: cover S^1 with two covers S^1-{1} and S^1-{-1}, define constant sheaves there, prove S^1-{1,-1} is in two pieces, glue with +1 on one piece and -1 on the other, and then see what Lean says you have to do next.

Is there a slicker way? Am I completely off here?

[Dominic Steinitz]

Kevin Buzzard said:

Dominic I see you're currently at the "wow, formalization is much harder work than I expected" stage :-) I would be interested to hear about the problems you're facing. My naive (because I've never worked with manifolds) idea would be: cover S^1 with two covers S^1-{1} and S^1-{-1}, define constant sheaves there, prove S^1-{1,-1} is in two pieces, glue with +1 on one piece and -1 on the other, and then see what Lean says you have to do next.

Is there a slicker way? Am I completely off here?

That is exactly what I am trying to do but there seems to be a lot to fill in e.g.

noncomputable
def chart_at_S1_excluding_minus_1 : PartialHomeomorph S1 ℝ :=
{
  toFun := λ z => arg z.val,
  invFun := λ r => ⟨exp (r * Complex.I), exp_mem_unitSphere r⟩,
  source := {z : S1 | arg z.val ∈ Ioo (-Real.pi) (Real.pi)},
  target := Ioo (-Real.pi) (Real.pi),
  map_source' := λ z hz => hz,
  map_target' := λ r hr => ⟨(sorry : (-Real.pi) < (exp (r * I)).arg), (sorry : (exp (r * I)).arg < (Real.pi))⟩,
  left_inv' := λ z hz => sorry
  right_inv' := λ r hr => sorry,
  open_source := sorry,
  open_target := isOpen_Ioo,
  continuousOn_toFun := sorry,
  continuousOn_invFun := sorry
}

Although I am more fluent than I was a few months ago, it still takes me time to fill in sorry in map_target'. But I am getting there.

[Damiano Testa]

Maybe excluding any one point, rather than $\pm 1$ directly, might be more recyclable?

[Dominic Steinitz]

Damiano Testa said:

Maybe excluding any one point, rather than $\pm 1$ directly, might be more recyclable?

That possibility did cross my mind since AFAICS the charts on the sphere (in Lean) are defined like that but I wanted to stick with the approach that everyone learns (with proof by hand waving).

[Dominic Steinitz]

Here's what I have so far

import Mathlib

open Bundle Topology MulAction Set
open Complex

def S1 : Type := Submonoid.unitSphere ℂ
deriving TopologicalSpace

theorem exp_mem_unitSphere (r : ℝ) : exp (r * I) ∈ Submonoid.unitSphere ℂ := by
  have h1 : abs (exp (r * I)) = 1 := abs_exp_ofReal_mul_I r
  have h2 : exp (r * I) ∈ Metric.sphere 0 1 ↔ ‖exp (r * I)‖ = 1 := mem_sphere_zero_iff_norm
  have h3 : ‖exp (r * I)‖ = abs (exp (r * I)) := rfl
  have h5 : ‖exp (r * I)‖ = 1 := by
    rw [h3, h1]
  have h6 : exp (r * I) ∈ Metric.sphere 0 1 := h2.2 h5
  have h7 : exp (r * I) ∈ Submonoid.unitSphere ℂ := h6
  exact h7

theorem arg_exp_within_Ioo (θ : ℝ) (hθ : -Real.pi < θ ∧ θ < Real.pi) :
  arg (exp (θ * I)) = θ := by
  have θ_in_Ioo : θ ∈ Ioo (-Real.pi) Real.pi := hθ
  have θ_in_Ioc : θ ∈ Ioc (-Real.pi) Real.pi := by
    exact Ioo_subset_Ioc_self θ_in_Ioo

  have arg_exp_formula : arg (exp (θ * I)) = toIocMod (mul_pos two_pos Real.pi_pos) (-Real.pi) θ :=
    Complex.arg_exp_mul_I θ

  have toIocMod_eq_theta : toIocMod (mul_pos two_pos Real.pi_pos) (-Real.pi) θ = θ ↔
      θ ∈ Ioc (-Real.pi) ((-Real.pi) + (2 * Real.pi)) :=
    toIocMod_eq_self (mul_pos two_pos Real.pi_pos)

  have interval_simplification : -Real.pi + 2 * Real.pi = Real.pi := by ring

  have toIocMod_eq_theta' : toIocMod (mul_pos two_pos Real.pi_pos) (-Real.pi) θ = θ ↔
      θ ∈ Ioc (-Real.pi) Real.pi := by rwa [interval_simplification] at toIocMod_eq_theta

  have toIocMod_simplifies : toIocMod (mul_pos two_pos Real.pi_pos) (-Real.pi) θ = θ :=
    toIocMod_eq_theta'.mpr θ_in_Ioc

  exact arg_exp_formula.trans toIocMod_simplifies


noncomputable
def chart_at_S1_excluding_minus_1 : PartialHomeomorph S1 ℝ :=
{
  toFun := λ z => arg z.val,
  invFun := λ r => ⟨exp (r * Complex.I), exp_mem_unitSphere r⟩,
  source := {z : S1 | arg z.val ∈ Ioo (-Real.pi) (Real.pi)},
  target := Ioo (-Real.pi) (Real.pi),
  map_source' := λ z hz => hz,
  map_target' := λ r hr => by
    have h1 : (exp (r * I)).arg = r := arg_exp_within_Ioo r hr
    have h2a : (-Real.pi) < r := hr.1
    have h2b : r < Real.pi := hr.2
    have h3a : (-Real.pi) < (exp (r * I)).arg := by
      rw [h1]
      exact h2a
    have h3b : (exp (r * I)).arg < (Real.pi) := by
      rw [h1]
      exact h2b
    exact ⟨(h3a : (-Real.pi) < (exp (r * I)).arg), (h3b : (exp (r * I)).arg < (Real.pi))⟩,
  left_inv' := λ z hz => by
    have h0 : (Complex.abs z.val) * exp ((z.val).arg * I) = z.val := by exact abs_mul_exp_arg_mul_I z.val
    have h4 : z.val ∈ Submonoid.unitSphere ℂ := by exact z.prop
    have h5 : z.val ∈ Metric.sphere 0 1 ↔ ‖z.val‖ = 1 := mem_sphere_zero_iff_norm
    have h7 : z.val ∈ Metric.sphere 0 1 := h4
    have h6 : ‖z.val‖ = 1 := by rwa [h5] at h7
    have h8 : ‖z.val‖ * exp ((z.val).arg * I) = z.val := by exact abs_mul_exp_arg_mul_I z.val
    have h9 : z.val = exp ((z.val).arg * I) := by
      calc z.val = ‖z.val‖ * exp ((z.val).arg * I) := by rw [h8]
                _ = (1 : ℝ) *  exp ((z.val).arg * I) := by rw [h6]
                _ = (1 : ℂ) * exp ((z.val).arg * I) := by norm_cast
                _ = exp ((z.val).arg * I) := by rw [one_mul]
    have h3 : (fun r => ⟨exp (r * I), by exact exp_mem_unitSphere r⟩) (z.val).arg = z := by
      apply Subtype.ext
      exact h9.symm
    exact h3
  right_inv' := λ r hr => by
   have h1 : arg (exp (r * I)) = r := arg_exp_within_Ioo r hr
   exact h1
  open_source := by
    exact sorry,
  open_target := isOpen_Ioo,
  continuousOn_toFun  := (sorry : (ContinuousOn (λ z => arg z.val)) {z : S1 | arg z.val ∈ Ioo (-Real.pi) (Real.pi)}),
  continuousOn_invFun := sorry
}

[Winston Yin (尹維晨)]

Dominic, when you post your code, could you also briefly describe what you did and what issue you’re seeking help on? This makes it more likely that somebody (including me) will look through the long code block.

[Dominic Steinitz]

Fair point. I was trying to respond to the suggestions from @Kevin Buzzard and @Damiano Testa about creating an atlas.

Let $\sim$ be the equivalence relation on $[0,1] \times \mathbb{R}$ defined by $(0, y) \sim(1, -y)$ and the Mobius strip be as usual be $M=[0,1] \times \mathbb{R} /\sim$.
Let $\pi(x, y) = x$ be the projection map $\pi : M \rightarrow \mathbb{S}^1$.

We can define a local trivialization $\phi_V$ on $\pi^{-1}(V)=\pi^{-1}(S^1 \backslash\{\pi\})$:

$\phi_V: \pi^{-1}(V) \rightarrow V \times \mathbb{R} \text { by }(x, y) \mapsto \begin{cases}(x, y) & 0 \leq x<\frac{1}{2} \\ (x-1,-y) & \frac{1}{2}<x \leq 1\end{cases}$

We only need check that this map is well defined on $[(0,y)]$ as all other equivalence classes are just a single element. For $(0,y), (1, -) \in [(0,y)]$:

$\phi_V(0,y) = (0,y) = \phi_V(1, -y)$

To expreess that this is a G-bundle in Lean, we previously invented:

structure GBundleCore (ι : Type*) (B : Type*) [TopologicalSpace B] (F : Type*)
    [TopologicalSpace F] (G : Type*) [Group G] [MulAction G F] where
  baseSet : ι → Set B
  isOpen_baseSet : ∀ i, IsOpen (baseSet i)
  indexAt : B → ι
  mem_baseSet_at : ∀ x, x ∈ baseSet (indexAt x)
  coordChange : ι → ι → B → F → F
  coordChange_self : ∀ i, ∀ x ∈ baseSet i, ∀ v, coordChange i i x v = v
  continuousOn_coordChange : ∀ i j,
    ContinuousOn (fun p : B × F => coordChange i j p.1 p.2) ((baseSet i ∩ baseSet j) ×ˢ univ)
  coordChange_comp : ∀ i j k, ∀ x ∈ baseSet i ∩ baseSet j ∩ baseSet k, ∀ v,
    (coordChange j k x) (coordChange i j x v) = coordChange i k x v
  coordChange_structure_group : ∀ i j, ∀ x ∈ baseSet i ∩ baseSet j, ∃ g : G, ∀ v : F, coordChange i j x v = g • v

In particular we have indexAt which gives a chart at a point in the base space of the bundle. Thus I started creating an atlas for the circle with two charts (as has been suggested). This proved trickier than anticipated and I was showing what I had so far for just one of the (two) charts. And I wondered if I was going in the right direction or was completely off the rails.

If anyone had any suggestions on how to approach this, I would be very grateful.

[Dominic Steinitz]

Damiano Testa said:

Maybe excluding any one point, rather than $\pm 1$ directly, might be more recyclable?

Kevin Buzzard said:

Dominic I see you're currently at the "wow, formalization is much harder work than I expected" stage :-) I would be interested to hear about the problems you're facing. My naive (because I've never worked with manifolds) idea would be: cover S^1 with two covers S^1-{1} and S^1-{-1}, define constant sheaves there, prove S^1-{1,-1} is in two pieces, glue with +1 on one piece and -1 on the other, and then see what Lean says you have to do next.

Is there a slicker way? Am I completely off here?

Both great suggestions and I could have saved myself a lot of work. I now have two charts and I hope I can now move forward to defining local trivialisations.

import Mathlib

open Bundle Topology MulAction Set
open Complex

def S1 : Type := Submonoid.unitSphere ℂ
deriving TopologicalSpace

noncomputable def U := chartAt (EuclideanSpace ℝ (Fin 1)) (Circle.exp 0 : Circle)
noncomputable def V := chartAt (EuclideanSpace ℝ (Fin 1)) (Circle.exp Real.pi : Circle)

noncomputable
def chart_at_S1_excluding_1 : PartialHomeomorph S1 (EuclideanSpace ℝ (Fin 1)) := U
noncomputable
def chart_at_S1_excluding_minus_1 : PartialHomeomorph S1 (EuclideanSpace ℝ (Fin 1)) := V

[Dominic Steinitz]

Perhaps I should first prove that they cover S1.

[Winston Yin (尹維晨)]

Sorry I’ve been slow to look at these. Having charts of the base manifold that don’t align with the trivialisation base sets is mathematically ok, but you’re better off defining the Möbius strip explicitly as the total space of a bundle with a suitable gluing between charts. This way, the base space will be a circle with two charts, each missing a point (as Kevin suggested), and the fibres are glued such that the transition function is 1 on one overlapping patch and -1 on the other.

[Winston Yin (尹維晨)]

This is what FiberBundleCore or in this case VectorBundleCore is for.

[Winston Yin (尹維晨)]

I would also recommend using the existing manifold structure on the sphere: docs#EuclideanSpace.instChartedSpaceSphere which uses the stereographic projection to define two charts that each miss one point.

[Winston Yin (尹維晨)]

@Dominic Steinitz How's our circular bundle doing?

[Dominic Steinitz]

It's coming along very slowly - I have been down many rabbit holes

[Dominic Steinitz]

Finally I have a Mobius strip that type checks - it is not yet a G-bundle but it is at least a fibre bundle. I have only given the co-ordinate change functions below as the rest of the proofs occupy an embarrassingly large 500 LoC. The full code is here.

Copying in @Nicolò Cavalleri

def MyCoordChange : Fin 2 → Fin 2 → (Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) → EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1)
      | 0, 0, _, α => α
      | 0, 1, x, α => if (x.val 1) > 0 then α else -α
      | 1, 0, x, α => if (x.val 1) > 0 then α else -α
      | 1, 1, _, α => α

def Mobius : FiberBundleCore (Fin 2) (Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) (EuclideanSpace ℝ (Fin 1)) :=
{
  baseSet := λ i => if i = 0 then chart_excluding_minus_1.source
                             else chart_excluding_1.source,

  isOpen_baseSet := by
    intro i
    dsimp only
    split
    · exact chart_excluding_minus_1.open_source
    · exact chart_excluding_1.open_source

  indexAt := λ x => if (x.val 0) > 0 then 0 else 1,

  mem_baseSet_at := my_mem_baseSet_at,

  coordChange := MyCoordChange,

  coordChange_self := MyCoordChange_self,

  continuousOn_coordChange := by
    intro i j
    exact MyContinuousOn_coordChange i j

  coordChange_comp := MyCoordChange_comp
}

[Dominic Steinitz]

Kevin Buzzard said:

Dominic I see you're currently at the "wow, formalization is much harder work than I expected" stage :-) I would be interested to hear about the problems you're facing. My naive (because I've never worked with manifolds) idea would be: cover S^1 with two covers S^1-{1} and S^1-{-1}, define constant sheaves there, prove S^1-{1,-1} is in two pieces, glue with +1 on one piece and -1 on the other, and then see what Lean says you have to do next.

Is there a slicker way? Am I completely off here?

I think this is what I have now done.

[Michael Rothgang]

On the aspect of "my code is long": taking a quick look, I think your code can be compressed/golfed quite a bit. (This is completely normal, by the way! I've learned a lot about code golfing by submitting my code for review, seeing it shortened drastically.) I'll be happy to give some advice, if you want.

[Dominic Steinitz]

Michael Rothgang said:

On the aspect of "my code is long": taking a quick look, I think your code can be compressed/golfed quite a bit. (This is completely normal, by the way! I've learned a lot about code golfing by submitting my code for review, seeing it shortened drastically.) I'll be happy to give some advice, if you want.

I was rather hoping someone would take a look and give some advice so yes please. I know I used the tried and tested software engineering technique of cut'n'paste so I was hopeful something could be done at least about that.

[Dominic Steinitz]

I moved the code here: https://github.com/idontgetoutmuch/DifferentialGeometry/blob/master/my_project/MyProject/Mobius.lean

[Michael Rothgang]

Sure. I might only get to this on Friday (I have to finish preparing a talk, due on Thursday). Do you have mathlib write permissions already? If so and you create a mathlib branch, I can also push changes directly. Either way is totally fine for me.

[Dominic Steinitz]

Michael Rothgang said:

Sure. I might only get to this on Friday (I have to finish preparing a talk, due on Thursday). Do you have mathlib write permissions already? If so and you create a mathlib branch, I can also push changes directly. Either way is totally fine for me.

I do not have Mathlib write permissions. Should I ask for them? I guess we could make this example part of Mathlib. The code is currently in my own stand-alone repo. I could fork Mathlib and then give you write permissions to my clone if that works better for you. Let me try doing that.

[Dominic Steinitz]

@Michael Rothgang I invited you and will now transfer my work to my fork of Mathlib

[Dominic Steinitz]

All code is now here: https://github.com/idontgetoutmuch/mathlib4/commit/fa2bdfda8d43d6f409a92c48f7a28bf73ac2956b

[Michael Rothgang]

I pushed some simplifications to that branch. These are only "local" clean-ups, i.e. no changes to high-level structure whatsoever. Feel free to DM me and I can explain the motivation behind any particular change.

[Patrick Massot]

I missed that discussion because I’m not subscribed to this channel. But I’m really puzzled to see charts for the Möbius strip mentioned here. This sounds really masochistic. Why don’t you define it as a quotient of the plane by the obvious ℤ action?

[Patrick Massot]

I didn’t read the whole thread, so please ignore my message if it’s not relevant. I only want to say that defining the Möbius strip (with any extra structure you wish) is much simpler as a quotient, and if Mathlib doesn’t know enough about quotients then we need to fix that instead of putting in painful ad-hoc chart constructions.

[Patrick Massot]

Maybe I should read the entire thread because I’m confused by the fact that the Möbius strip appears in a principal fiber bundle thread. Do you mean $ℤ/2$--bundle at the “boundary”?

[Patrick Massot]

As a general fact, I think we should have no atlas construction in Mathlib for any concrete manifold. There is always a nicer way to put manifold structures on interesting spaces. The case of spheres is special. It was meant as an experiment in computing in Mathlib (and it was partially reverted because it was too slow). But outside of this experiment it is a very bad example. Defining charts on spheres is the worst way to put a manifold structure on them.

[Michael Rothgang]

Patrick Massot said:

As a general fact, I think we should have no atlas construction in Mathlib for any concrete manifold. There is always a nicer way to put manifold structures on interesting spaces. The case of spheres is special. It was meant as an experiment in computing in Mathlib (and it was partially reverted because it was too slow). But outside of this experiment it is a very bad example. Defining charts on spheres is the worst way to put a manifold structure on them.

Let me emphasize this is a medium- to long-term goal. For instance, for spheres one should rather use the regular value theorem; for e.g. real projective space, one should use a general result about quotients of actions. Both of these are not in mathlib.

[Michael Rothgang]

I have some ideas towards the regular value theorem, but that's some path ahead. Some next milestones/related work in-flight is

• prove the inverse function theorem for manifolds,
• prove the constant rank theorem,
• deduce the regular value theorem,
• (optional) prove Sard's theorem and rejoice that in finite dimension almost every value is a regular value.
• The implicit function theorem (for vector bundles) would also be nice to have, but might not be needed for this application.

I have in-progress code for 1 and 4, which in many cases is quite dusty/could certainly use help.

[Dominic Steinitz]

Patrick Massot said:

I missed that discussion because I’m not subscribed to this channel. But I’m really puzzled to see charts for the Möbius strip mentioned here. This sounds really masochistic. Why don’t you define it as a quotient of the plane by the obvious ℤ action?

Great question:

1. AFAICT quotient manifolds do not exist in Mathlib
2. The way bundles are set up in Mathlib means you define a (fibre) bundle via its co-ordinate transform maps so you never end up defining the total space. To get the total space you do then need quotienting and this may be done somewhere in Mathlib but I didn't find it.
3. It wasn't meant to be masochistic but I wanted to do it the way it is given in many presentations. The masochism is probably related in part to my inexperience.

[Dominic Steinitz]

Patrick Massot said:

Maybe I should read the entire thread because I’m confused by the fact that the Möbius strip appears in a principal fiber bundle thread. Do you mean $ℤ/2$--bundle at the “boundary”?

I started with G-bundles and the Möbius strip is an example of a non-trivial G-bundle. I didn't give my Möbius strip a boundary but I am not sure what to call such a structure so I kept the word strip.

[Dominic Steinitz]

Patrick Massot said:

I didn’t read the whole thread, so please ignore my message if it’s not relevant. I only want to say that defining the Möbius strip (with any extra structure you wish) is much simpler as a quotient, and if Mathlib doesn’t know enough about quotients then we need to fix that instead of putting in painful ad-hoc chart constructions.

I look forward to the delivery of quotient manifolds :smiling_face:

[Dominic Steinitz]

Patrick Massot said:

As a general fact, I think we should have no atlas construction in Mathlib for any concrete manifold. There is always a nicer way to put manifold structures on interesting spaces. The case of spheres is special. It was meant as an experiment in computing in Mathlib (and it was partially reverted because it was too slow). But outside of this experiment it is a very bad example. Defining charts on spheres is the worst way to put a manifold structure on them.

And yet this is the first example many folk encounter. I assumed that this is "the Mathlib way" - did I miss something saying don't use this as a template? I am sure I saw someone doing some work on producing more examples of manifolds: projective space? affine space? Grassmanians? I thought to add to the examples :sad:

[Patrick Massot]

Dominic Steinitz said:

Patrick Massot said:

Maybe I should read the entire thread because I’m confused by the fact that the Möbius strip appears in a principal fiber bundle thread. Do you mean $ℤ/2$--bundle at the “boundary”?

I started with G-bundles and the Möbius strip is an example of a non-trivial G-bundle. I didn't give my Möbius strip a boundary but I am not sure what to call such a structure so I kept the word strip.

Oh, do you mean non-principal G-bundle? Then I understand what you mean, and I was misled by the title of the thread.

[Patrick Massot]

Dominic Steinitz said:

Patrick Massot said:

As a general fact, I think we should have no atlas construction in Mathlib for any concrete manifold. There is always a nicer way to put manifold structures on interesting spaces. The case of spheres is special. It was meant as an experiment in computing in Mathlib (and it was partially reverted because it was too slow). But outside of this experiment it is a very bad example. Defining charts on spheres is the worst way to put a manifold structure on them.

And yet this is the first example many folk encounter. I assumed that this is "the Mathlib way" - did I miss something saying don't use this as a template? I am sure I saw someone doing some work on producing more examples of manifolds: projective space? affine space? Grassmanians? I thought to add to the examples :sad:

Of course you are free to work on whatever you want. But, if you want to be maximally useful to the community, then you should work on building the right tool for the job instead of bypassing those tools using ad hoc elementary constructions. Putting a manifold structure on Grassmanians by hand is really painful on paper already. The natural way to proceed is to work on Lie groups and homogeneous spaces. Then you get the manifold structure and the smooth action of the general linear groups of free. And you don’t have to restart from scratch the day you want to do more general flag manifolds.

[Winston Yin (尹維晨)]

To put this thread in context, @Dominic Steinitz is in the process of learning the manifold / fibre bundle part of mathlib, as well as Lean and formalisation generally. With defining principle G-bundles as a goal, he is trying to define (non-principle) G-bundles and a couple elementary constructions of such.

It took me about 1 year of playing with Lean / mathlib to be useful (a small PR being merged), but the process is itself loads of fun, even if the approaches I experimented with were nowhere near the the generality mathlib demands.

@Michael Rothgang I would like to see implicit function theorem (on Banach spaces), which is on the path to something else I'm hoping to work on soon ish.

[Michael Rothgang]

Did you mean the implicit function theorem on Banach manifolds (or perhaps Banach space vector bundles)? Because I think mathlib has the implicit function theorem already --- doesn't it?

[Michael Rothgang]

I would also like to see that. And the inverse function theorem, and the regular value theorem. But somebody has to do it, and I'm currently busy with Carleson, a paper, immersions/embeddings and submanifolds (as well as polishing the inverse function theorem). I can't do everything at once, even if I'd like to :-)
(And, last but not least: I'd like to finally take an afternoon to review your PR about local flows. I haven't forgotten about it.)

[Winston Yin (尹維晨)]

Ah sorry I meant the smoothness statement for implicit function theorem on Banach spaces.

[Winston Yin (尹維晨)]

And then for Banach manifolds

[Winston Yin (尹維晨)]

I'm aware of all the cool things you're doing! (esp. from convos with Floris at the Berkeley conference) Feel free to reach out about the PRs when you find the time.

[Matteo Cipollina]

I have read this thread with interest and out of curiosity have tried to implement the suggestion made by @Patrick Massot . I've started to try to prove that MobiusStrip admits a smooth manifold structure compatible with the quotient topology, and has the desired bundle structure, though I had no time to complete it yet. Hope this could be useful!

import Mathlib

open Manifold Set Function FiniteDimensional Filter Topology

noncomputable section

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
variable {I : ModelWithCorners ℝ E E}

def mobius_action (n : ℤ) (p : ℝ × ℝ) : ℝ × ℝ :=
  (p.1 + n, if 2 ∣ n then p.2 else -p.2)

def mobius_equiv (p q : ℝ × ℝ) : Prop :=
  ∃ n : ℤ, mobius_action n p = q

lemma Int.dvd_iff_exists_eq_mul_left {a b : ℤ} : a ∣ b ↔ ∃ c, b = a * c := by
  rfl

lemma mobius_equiv_refl (p : ℝ × ℝ) : mobius_equiv p p :=
  ⟨0, by simp [mobius_action]⟩

lemma mobius_action_neg {p q : ℝ × ℝ} {n : ℤ} (h : mobius_action n p = q) :
  mobius_action (-n) q = p := by
  simp [mobius_action] at h ⊢
  have h1 : q.1 = p.1 + n := by
    have h_fst := (Prod.ext_iff.1 h).1
    simp [mobius_action] at h_fst
    exact id (Eq.symm h_fst)
  have h2 : q.2 = if 2 ∣ n then p.2 else -p.2 := by
    have h_snd := (Prod.ext_iff.1 h).2
    simp [mobius_action] at h_snd
    exact id (Eq.symm h_snd)
  ext
  · simp [h1, add_neg_cancel_right]
  · by_cases hn : 2 ∣ n
    · have h_neg : 2 ∣ -n := by rw [dvd_neg]; exact hn
      simp [h_neg, h2, hn]
    · have h_neg : ¬(2 ∣ -n) := by
        intro h; apply hn; rw [dvd_neg] at h; exact h
      simp [h_neg, h2, hn]

lemma mobius_equiv_symm {p q : ℝ × ℝ} (h : mobius_equiv p q) : mobius_equiv q p :=
  let ⟨n, hn⟩ := h
  ⟨-n, mobius_action_neg hn⟩

lemma mobius_action_comp_fst {p q r : ℝ × ℝ} {n m : ℤ}
  (hn : mobius_action n p = q) (hm : mobius_action m q = r) :
  (mobius_action (n + m) p).1 = r.1 := by
  simp [mobius_action] at hn hm ⊢
  have h1 : q.1 = p.1 + n := Eq.symm ((Prod.ext_iff.1 hn).1)
  have h3 : r.1 = q.1 + m := Eq.symm ((Prod.ext_iff.1 hm).1)
  simp [h1, h3]
  ring

lemma mobius_action_comp_snd_even_even {p q r : ℝ × ℝ} {n m : ℤ}
  (hn : mobius_action n p = q) (hm : mobius_action m q = r)
  (hn2 : 2 ∣ n) (hm2 : 2 ∣ m) :
  (mobius_action (n + m) p).2 = r.2 := by
  simp [mobius_action] at hn hm ⊢
  have h2 : q.2 = if 2 ∣ n then p.2 else -p.2 := Eq.symm ((Prod.ext_iff.1 hn).2)
  have h4 : r.2 = if 2 ∣ m then q.2 else -q.2 := Eq.symm ((Prod.ext_iff.1 hm).2)
  have h : 2 ∣ (n + m) := dvd_add hn2 hm2
  simp [h, hn2, hm2, h2, h4]

lemma mobius_action_comp_snd_even_odd {p q r : ℝ × ℝ} {n m : ℤ}
  (hn : mobius_action n p = q) (hm : mobius_action m q = r)
  (hn2 : 2 ∣ n) (hm2 : ¬(2 ∣ m)) :
  (mobius_action (n + m) p).2 = r.2 := by
  simp [mobius_action] at hn hm ⊢
  have h2 : q.2 = if 2 ∣ n then p.2 else -p.2 := Eq.symm ((Prod.ext_iff.1 hn).2)
  have h4 : r.2 = if 2 ∣ m then q.2 else -q.2 := Eq.symm ((Prod.ext_iff.1 hm).2)
  have h : ¬(2 ∣ (n + m)) := by
    simp [Int.even_add]; omega
  simp [h, hn2, hm2, h2, h4]

lemma mobius_action_comp_snd_odd_even {p q r : ℝ × ℝ} {n m : ℤ}
  (hn : mobius_action n p = q) (hm : mobius_action m q = r)
  (hn2 : ¬(2 ∣ n)) (hm2 : 2 ∣ m) :
  (mobius_action (n + m) p).2 = r.2 := by
  simp [mobius_action] at hn hm ⊢
  have h2 : q.2 = if 2 ∣ n then p.2 else -p.2 := Eq.symm ((Prod.ext_iff.1 hn).2)
  have h4 : r.2 = if 2 ∣ m then q.2 else -q.2 := Eq.symm ((Prod.ext_iff.1 hm).2)
  have h : ¬(2 ∣ (n + m)) := by
    simp [Int.even_add]; omega
  simp [h, hn2, hm2, h2, h4]

lemma mobius_action_comp_snd_odd_odd {p q r : ℝ × ℝ} {n m : ℤ}
  (hn : mobius_action n p = q) (hm : mobius_action m q = r)
  (hn2 : ¬(2 ∣ n)) (hm2 : ¬(2 ∣ m)) :
  (mobius_action (n + m) p).2 = r.2 := by
  simp [mobius_action] at hn hm ⊢
  have h2 : q.2 = if 2 ∣ n then p.2 else -p.2 := Eq.symm ((Prod.ext_iff.1 hn).2)
  have h4 : r.2 = if 2 ∣ m then q.2 else -q.2 := Eq.symm ((Prod.ext_iff.1 hm).2)
  have h : 2 ∣ (n + m) := by
    have n_eq : ∃ j, n = 2 * j + 1 := by
        cases Int.even_or_odd n with
        | inl h_even =>
          have : 2 ∣ n := by
            cases h_even with
            | intro j hj =>
              use j
              rw [← mul_two j, mul_comm] at hj
              exact hj
          contradiction
        | inr h_odd =>
          exact h_odd
    have m_eq : ∃ j, m = 2 * j + 1 := by
      cases Int.even_or_odd m with
      | inl h_even =>
        have : 2 ∣ m := by
          cases h_even with
          | intro j hj => use j; omega
        contradiction
      | inr h_odd =>
        exact h_odd
    obtain ⟨j₁, h₁⟩ := n_eq
    obtain ⟨j₂, h₂⟩ := m_eq
    use j₁ + j₂ + 1
    calc n + m = (2 * j₁ + 1) + (2 * j₂ + 1) := by rw [h₁, h₂]
             _ = 2 * (j₁ + j₂ + 1) := by ring
  simp [h, hn2, hm2, h2, h4]

lemma mobius_action_comp {p q r : ℝ × ℝ} {n m : ℤ}
  (hn : mobius_action n p = q) (hm : mobius_action m q = r) :
  mobius_action (n + m) p = r := by
  ext
  · -- First coordinate
    exact mobius_action_comp_fst hn hm
  · -- Second coordinate
    by_cases hn2 : 2 ∣ n
    · by_cases hm2 : 2 ∣ m
      · -- Both even
        exact mobius_action_comp_snd_even_even hn hm hn2 hm2
      · -- n even, m odd
        exact mobius_action_comp_snd_even_odd hn hm hn2 hm2
    · by_cases hm2 : 2 ∣ m
      · -- n odd, m even
        exact mobius_action_comp_snd_odd_even hn hm hn2 hm2
      · -- Both odd
        exact mobius_action_comp_snd_odd_odd hn hm hn2 hm2

lemma mobius_equiv_trans {p q r : ℝ × ℝ} (hpq : mobius_equiv p q) (hqr : mobius_equiv q r) :
  mobius_equiv p r :=
  let ⟨n, hn⟩ := hpq
  let ⟨m, hm⟩ := hqr
  ⟨n + m, mobius_action_comp hn hm⟩

instance mobius_setoid : Setoid (ℝ × ℝ) :=
  { r := mobius_equiv,
    iseqv := ⟨mobius_equiv_refl, mobius_equiv_symm, mobius_equiv_trans⟩ }

def MobiusStrip := Quotient mobius_setoid

def mob_mk : ℝ × ℝ → MobiusStrip := Quotient.mk mobius_setoid

def circle_equiv (x y : ℝ) : Prop :=
  ∃ n : ℤ, y = x + n

instance circle_setoid : Setoid ℝ :=
  { r := circle_equiv,
    iseqv := ⟨
      -- Reflexivity
      fun x => ⟨0, by simp⟩,
      -- Symmetry
      fun {x y} ⟨n, h⟩ => ⟨-n, by rw [h]; simp;⟩,
      -- Transitivity
      fun {x y z} ⟨n, hn⟩ ⟨m, hm⟩ => ⟨n + m, by rw [hm, hn]; simp; ring⟩
    ⟩ }

[Patrick Massot]

May I suggest that you could use mobius_action n p = (p.1 + n, (-1)^n*p.2) instead? This is of course equivalent to your definition, but I think it will make things easier.

[Dominic Steinitz]

Winston Yin (尹維晨) said:

To put this thread in context, Dominic Steinitz is in the process of learning the manifold / fibre bundle part of mathlib, as well as Lean and formalisation generally. With defining principle G-bundles as a goal, he is trying to define (non-principle) G-bundles and a couple elementary constructions of such.

It took me about 1 year of playing with Lean / mathlib to be useful (a small PR being merged), but the process is itself loads of fun, even if the approaches I experimented with were nowhere near the the generality mathlib demands.

Michael Rothgang I would like to see implicit function theorem (on Banach spaces), which is on the path to something else I'm hoping to work on soon ish.

To give even more context: I want to reproduce my article on what I call the Mercator connection in which I constructed a connection which is compatible with the usual metric on the 2-sphere but in which parallel means parallel on the Mercator projection (and so it must have torsion).

This led me to want to define a connection in Lean (I couldn't find one) and I think the best way to do this is go via the Ehresmann definition for which one needs principal G-bundles (something that does not exist in SageManifolds, the tool I originally used and there was no way I could modify SageManifolds as it is written in Python).

This was meant to be a prelude to doing some work on gravitational waves without the "débauche d'indices" :laughter_tears:. Maybe in 10 years time I will reach my goal.

@Winston Yin (尹維晨) I am relieved to know that learning how Lean treats differential geometry is not something one picks up overnight (but SageManifolds also required some time to learn and the lack of types led me often to pound my desk).

[Patrick Massot]

I think this is understated. Differential geometry is very probably the most difficult part of Mathlib to learn.

[Winston Yin (尹維晨)]

And also why it's the most fun :)