Lie groups and Lie algebras

Stream: maths

[Kevin Buzzard]

Anthony Bordg was asking me about Lie algebras and Lie groups. I see we have Lie algebras now. Do we have the tangent vector space of a smooth manifold at a point? I would imagine that the abstract definition of Lie group waswould be easy. Is the structure of a Lie algebra on the tangent space of a Lie group within reach?

[Kevin Buzzard]

@Anthony Bordg

[Scott Morrison]

I think you have at least the tense wrong in "the abstract definition of Lie group was easy"...

[Oliver Nash]

I briefly looked at this back in January or so. I view the Lie algebra structure on the tangent space to a Lie group at the identity arising because the invariant vector fields are a Lie subalgebra of the Lie algebra of all vector fields on the group.

[Oliver Nash]

If we go that route, then we first need the Lie algebra structure on vector fields so I looked into defining that and when I last looked, we didn't even have the vector space structure on sections of a vector bundle.

[Oliver Nash]

Things may have changed but it looked like there was still a bit of work to do till we had this. Not huge, but not quite trivial.

[Scott Morrison]

Presumably we need Yury's work on the implicit function theorem before we even unlock the Lie group level, as one of the very first theorems should be that you don't need to check smoothness of the inverse.

[Oliver Nash]

There might be a case to be made for developing some theory for closed subgroups of the general linear group. If we had the exponential map for matrices then we could probably get quite far.

[Scott Morrison]

Is the right route to the exponential map for matrices just a functional calculus? I was thinking about attempting Stone-Weierstrauss in any case.

[Sebastien Gouezel]

Oliver Nash said:

If we go that route, then we first need the Lie algebra structure on vector fields so I looked into defining that and when I last looked, we didn't even have the vector space structure on sections of a vector bundle.

That's correct. There are several design questions here, the main one being: how does one register a vector bundle? Possible definitions would be:

• a manifold $N$ with charts taking values in $E \times F$, and the changes of coordinates send fibers of the projection on $E$ to fibers in a linear way (i.e., prescribing the groupoid as the one of linear maps in the second coordinate). Then you have a quotient manifold, and a vector bundle. This is probably a bad choice to use a quotient manifold like that, because for instance in the tangent bundle the manifold is not defeq to the quotient manifold obtained by quotienting the tangent bundle by its fibers
• more data: a manifold $N$ as above, but also a manifold $M$ and a projection $\pi$ from $N$ to $M$ that behaves nicely. Then the fibers of the projection can be endowed with a vector space structure in a canonical way. But there is the difficulty that, in the tangent bundle case, the fibers of the projection (written as {y // pi y = x}) are not defeq to the tangent space.
• Even more data: $N$, $M$ and $\pi$, but also a family of vector spaces $F_x$ indexed by $x \in M$ and isomorphisms between the fiber above $x$ and $F_x$?
• Or just a manifold structure on a Pi type of the form Π (x : M), F x, with the right groupoid.
• Or, even simpler, a manifold structure on $M \times F$. This may seem crazy, but this is the underlying type of the tangent bundle for now, and it works pretty well.

[Sebastien Gouezel]

My guess is that it will be more flexible to have some kind of predicate, instead of sticking to one specific type-theoretic construction.

[Sebastien Gouezel]

Also, once you have vector bundles you will quickly ask for more general types of bundles, so should category theory be involved already, one way or another?

[Sebastien Gouezel]

And should one define (locally trivial) vector bundles first over a general topological space, and then specialize to manifolds, or do only the manifold case?

[Kevin Buzzard]

I don't know how one should answer this sort of question. There are e.g. undergraduates who want to think about Lie groups and Lie algebras, and then there are Bochner integral people who say that the best way is the most general way.

[Sebastien Gouezel]

I think these are difficult and important questions, that should be discussed throughly here on Zulip.

[Sebastien Gouezel]

It's the same kind of questions as for schemes. Which are not yet in mathlib for the same kind of reason, but at some point we will have to make a choice and move forward.

[Kevin Buzzard]

We made some design decisions about presheaves in the repo, and then mathlib made some different design decisions, but the reason they're not in mathlib is just because nobody is trying to put them in there. I am hoping to get back to this in August or September

[Reid Barton]

We definitely want vector bundles over topological spaces. @Jesse Michael Han and I started thinking about how to represent these at some point, but we didn't go very far with them. Some but not all of the approaches listed above work there. There are also other sorts of fiber bundles of course.

On the other hand, I don't know whether it matters if a smooth vector bundle on a manifold is a topological vector bundle plus some extra stuff. It's probably good enough just to have a way to convert back and forth between the two representations.

[Reid Barton]

Also, :+1: for Stone-Weierstrass. I remember thinking it should be easy.

[Reid Barton]

Sebastien Gouezel said:

My guess is that it will be more flexible to have some kind of predicate, instead of sticking to one specific type-theoretic construction.

Do you have an idea of what this would look like? Do you mean a characteristic predicate for "being a vector bundle over a manifold", or for "being the type of vector bundles over a manifold"? In the first case, you first have to write down the data somehow and then you're already committing to one of your list of representations. In the second case, I would be very interested to hear what you have in mind!

[Sebastien Gouezel]

I mean the former, i.e., you have a type, a projection, and you want to express the fact that this projection corresponds to a vector bundle. So you want to express that you have a vector space structure on the fibers, continuous and locally trivial. How to write this data? What I want to avoid is requiring that the underlying type is $E \times F$, or $\Sigma (x : E), F_x$ with some topology: the setup should cover both situations (and other natural situations), just like the predicate for topological fiber bundles does. For instance, the two following definitions would work.

import topology.topological_fiber_bundle
import analysis.normed_space.basic

namespace vector_bundle1

variables (𝕜 : Type*) {B : Type*} (F : Type*) {Z : Type*}
  [topological_space B] [topological_space Z] [normed_field 𝕜]
  [topological_space F] [add_comm_group F] [module 𝕜 F] [topological_module 𝕜 F] (proj : Z → B)
  [∀ (x : B), add_comm_group {y // proj y = x}] [∀ (x : B), module 𝕜 {y // proj y = x}]
  [∀ (x : B), topological_module 𝕜 {y // proj y = x}]

structure vector_bundle_trivialization extends bundle_trivialization F proj :=
(linear : ∀ x ∈ base_set, is_linear_map 𝕜 (λ (y : {y // proj y = x}), (to_fun y).2))

def is_topological_vector_bundle : Prop :=
∀ x : Z, ∃e : vector_bundle_trivialization 𝕜 F proj, x ∈ e.source

end vector_bundle1

namespace vector_bundle2

variables (𝕜 : Type*) {B : Type*} (F : Type*) {Z : Type*}
  [topological_space B] [topological_space Z] [normed_field 𝕜]
  [topological_space F] [add_comm_group F] [module 𝕜 F] [topological_module 𝕜 F] (proj : Z → B)
  (fiber_triv : Π (x : B), F ≃ {y // proj y = x})

structure vector_bundle_trivialization extends bundle_trivialization F proj :=
(linear : ∀ x ∈ base_set, is_linear_map 𝕜 (λ (y : F), (to_fun (fiber_triv x y)).2))

def is_topological_vector_bundle : Prop :=
∀ x : Z, ∃e : vector_bundle_trivialization 𝕜 F proj fiber_triv, x ∈ e.source

end vector_bundle2

In the first one, I require that typeclass inference knows about the topological vector space structure on the fibers of the projection, written as {y // proj y = x} (which is not defeq to proj ⁻¹' {x}, so one should choose a representation and use it constantly). In the second one, instead I choose for each fiber a bijection with the model vector space F, and I require that the trivialization is linear when seen through this (non-canonical) bijection.

The first one is arguably more natural, but when you work with $E \times F$ note that the fibers are not $F$, they are some other type which has a priori no vector space structure, so you need to register a whole bunch of typeclasses on these fibers, which is not very nice. With the second definition, you just use the canonical identification between $F$ and $\{x\} \times F$ and you're done. So I feel the second definition would be easier to work with.

@Reid Barton , do you remember what you had tried with @Jesse Michael Han ?

[Mario Carneiro]

What if rather than having projections, you had a sigma type as data? That is, a vector bundle is a topological space $Z$ equipped with a homeomorphism to $\Sigma(x:E),F_x$

[Mario Carneiro]

I have always thought that the approach of defining Sigma types via sections of a projection is backwards and unnatural; and in type theory it is much worse since you get these weird noncanonical types

[Sebastien Gouezel]

In the data, you would also need to put a topology on $\Sigma(x : E), F_x$ and a vector space structure on each $F_x$ and so on. The gain compared to using $\{y \mid proj(y) =x\}$ is not obious to me yet.

[Mario Carneiro]

Where is the topology on $\Sigma(x : E), F_x$ required? I guess the natural one doesn't always make sense in this context, but there is a topology induced by the one on Z and you can use that to state any required continuity assumptions between this topology and the ones on E and F_x. But the whole point here is that E, F_x, and Z all need to be specifiable independently of each other, and everything else is constraints

[Mario Carneiro]

Of course in specific cases you might be able to simplify this, e.g. by saying that $Z =\Sigma(x : E), F_x$ in one case or $F_x=\{y\mid proj(y)=x\}$ in another; but having three types means that you have the flexibility to make this choice

[Mario Carneiro]

Oh, I see you provided code. Here's an implementation of my suggestion:

import topology.topological_fiber_bundle
import analysis.normed_space.basic

namespace vector_bundle3

variables (𝕜 : Type*) (Z : Type*) {B : Type*} (E : B → Type*) (F : Type*)
  [normed_field 𝕜] [topological_space Z] [topological_space B] [∀ x, topological_space (E x)]

structure as_sigma :=
(to_sigma : Z ≃ Σ x, E x)
(cont : ∀ x, continuous (λ y : E x, to_sigma.symm ⟨x, y⟩))
(cont_inv : ∀ x, continuous (λ y : {y : Z // (to_sigma y).1 = x},
  (by rw ← y.2; exact (to_sigma y.1).2 : E x)))

variables {Z E}

def as_sigma.proj (s : as_sigma Z E) (z : Z) : B := (s.to_sigma z).1
def as_sigma.slice (s : as_sigma Z E) (x) (y : E x) : Z := s.to_sigma.symm ⟨x, y⟩

variables
  [topological_space F] [add_comm_group F] [module 𝕜 F] [topological_module 𝕜 F]
  [∀ x, add_comm_group (E x)] [∀ x, module 𝕜 (E x)] [∀ (x : B), topological_module 𝕜 (E x)]
  (s : as_sigma Z E)

structure bundle_trivialization extends local_homeomorph Z (B × F) :=
(base_set      : set B)
(open_base_set : is_open base_set)
(source_eq     : source = s.proj ⁻¹' base_set)
(target_eq     : target = set.prod base_set set.univ)
(proj_to_fun   : ∀ p ∈ source, (to_fun p).1 = s.proj p)

structure vector_bundle_trivialization extends bundle_trivialization F s :=
(linear : ∀ x ∈ base_set, is_linear_map 𝕜 (λ (y : E x), (to_fun (s.slice x y)).2))

def is_topological_vector_bundle : Prop :=
∀ x : Z, ∃e : vector_bundle_trivialization 𝕜 F s, x ∈ e.source

end vector_bundle3

[Mario Carneiro]

There are some messy casts in as_sigma.cont_inv, but these can be avoided if you unfold the definition of continuity. Together cont and cont_inv are asserting that to_sigma induces a homeomorphism between E x and {y // (to_sigma y).1 = x}

[Mario Carneiro]

I don't know the maths of bundle_trivialization so I haven't done much with it except make it typecheck

[Nicolò Cavalleri]

I remember someone saying somewhere that there could be a problem in using a normed vector space as a fiber for a smooth vector bundle as this norm creates a conflict in the definition of a Riemannian vector bundle (or maybe I dreamed it? I can't find this message back). I was wondering if someone has a solution to propose in case this is actually a problem. I understand this is a quite abstract question as there is no agreement yet on how the definition of vector bundle could be given, but maybe this problem can be solved abstractly no matter what the actual definition will be? On a finite dimensional vector space there is a unique manifold structure (same for all norms), so in this case could there be a way of creating an instance of manifold on the vector space without mentioning any norm?

[Sebastien Gouezel]

You just need to use a topological vector space for the fiber, instead of a normed vector space.

[Nicolò Cavalleri]

Sorry if this is a stupid question but isn't there only one topology on a vector space that agrees with the manifold structure? Can there be a canonical instance of a topological space as a smooth manifold? In order to make it into a smooth bundle I need the vector space to be a manifold don't I?

[Sebastien Gouezel]

On a given finite-dimensional real vector space, there is a single topological vector space structure, and a unique norm up to equivalence. However, this is in the mathematical sense of unique: give me two vector spaces topologies on this vector space, I can prove they are unique. But, from the point of view of Lean's kernel, they may not coincide, and so a lot of care is required to get things right. This is the difference between equality and definitional equality. https://xenaproject.wordpress.com/2020/07/03/equality-specifications-and-implementations/ may be enlightening about this.

[Nicolò Cavalleri]

But I am still unsure how this helps me to make a generic topological vector space into a manifold.

[Sebastien Gouezel]

Rather, if you start from a normed vector space, it is a manifold over itself. Then a copy of this normed vector space, in which you will only register the topology but not the norm, can be endowed with a manifold structure over the initial normed vector space.

This doesn't really answer your question: if you just start from a topological vector space, I don't think we have means currently to construct a norm creating the topology. (And this is impossible in general, unless your space is finite-dimensional and your field is complete).

[Nicolò Cavalleri]

Yes what you wrote in the first paragraph is what I was trying to say in my first message, even if wasn't thinking about making a copy of the normed space but recreating the topology and the manifold structure in some other way (for example by choosing a basis and using an isomorphism with K^n), but in any case I am not really sure about what is a good way to implement this so I might start with trying to do things with normed spaces and then change it later in case I manage to get somethings done

[Nicolò Cavalleri]

Sebastien Gouezel said:

I mean the former, i.e., you have a type, a projection, and you want to express the fact that this projection corresponds to a vector bundle. So you want to express that you have a vector space structure on the fibers, continuous and locally trivial. How to write this data? What I want to avoid is requiring that the underlying type is $E \times F$, or $\Sigma (x : E), F_x$ with some topology: the setup should cover both situations (and other natural situations), just like the predicate for topological fiber bundles does. For instance, the two following definitions would work.

import topology.topological_fiber_bundle
import analysis.normed_space.basic

namespace vector_bundle1

variables (𝕜 : Type*) {B : Type*} (F : Type*) {Z : Type*}
  [topological_space B] [topological_space Z] [normed_field 𝕜]
  [topological_space F] [add_comm_group F] [module 𝕜 F] [topological_module 𝕜 F] (proj : Z → B)
  [∀ (x : B), add_comm_group {y // proj y = x}] [∀ (x : B), module 𝕜 {y // proj y = x}]
  [∀ (x : B), topological_module 𝕜 {y // proj y = x}]

structure vector_bundle_trivialization extends bundle_trivialization F proj :=
(linear : ∀ x ∈ base_set, is_linear_map 𝕜 (λ (y : {y // proj y = x}), (to_fun y).2))

def is_topological_vector_bundle : Prop :=
∀ x : Z, ∃e : vector_bundle_trivialization 𝕜 F proj, x ∈ e.source

end vector_bundle1

namespace vector_bundle2

variables (𝕜 : Type*) {B : Type*} (F : Type*) {Z : Type*}
  [topological_space B] [topological_space Z] [normed_field 𝕜]
  [topological_space F] [add_comm_group F] [module 𝕜 F] [topological_module 𝕜 F] (proj : Z → B)
  (fiber_triv : Π (x : B), F ≃ {y // proj y = x})

structure vector_bundle_trivialization extends bundle_trivialization F proj :=
(linear : ∀ x ∈ base_set, is_linear_map 𝕜 (λ (y : F), (to_fun (fiber_triv x y)).2))

def is_topological_vector_bundle : Prop :=
∀ x : Z, ∃e : vector_bundle_trivialization 𝕜 F proj fiber_triv, x ∈ e.source

end vector_bundle2

In the first one, I require that typeclass inference knows about the topological vector space structure on the fibers of the projection, written as {y // proj y = x} (which is defeq to proj ⁻¹' {x}, but synctactically different so one should choose a representation and use it constantly if one wants typeclass inference to succeed). In the second one, instead I choose for each fiber a bijection with the model vector space F, and I require that the trivialization is linear when seen through this (non-canonical) bijection.

The first one is arguably more natural, but when you work with $E \times F$ note that the fibers are not $F$, they are some other type which has a priori no vector space structure, so you need to register a whole bunch of typeclasses on these fibers, which is not very nice. With the second definition, you just use the canonical identification between $F$ and $\{x\} \times F$ and you're done. So I feel the second definition would be easier to work with.

Reid Barton , do you remember what you had tried with Jesse Michael Han ?

In this message I am not really sure I unerstand the sentence "one should choose a representation and use it constantly if one wants typeclass inference to succeed": in particular I do not know what the word "representation" refers to. Is there somewhere I can read that could make things clearer?

[Nicolò Cavalleri]

In the past month I played both with Sébastien's definition with fibers {y // proj y = x} and with Mario's definition. I still do not know what exactly Sébastien meant with representation (and I would still be curious) but I defined canonical equivalences between the two fibers and defined a way to lift structures for equivalences, so in the end it's not that much of a pain to work with it (you literally have to write two more lines) and things get smooth by defining enough canonical instances. All the same I must say that to me Mario's definition results very natural since the beginning and in particular it is very easy to define naturally the cotangent bundle and exterior bundles and to work with them. Its only defect is that I do not see how it can be easily used with the current tangent bundle, which should still be the main "goal": I used it only for bundles defined directly with sigma types: that is how I imagine most vector bundles would be defined. For this reason I would be interested to hear @Sebastien Gouezel 's opinion on the possibility of using that definition for the tangent bundle, before discarding it, also after having seen Mario's code. I'd be interested to hear if there were a possibility to make Lean recognize the current tangent bundle as a sigma type, since the total space is, below, a product, which is in turn a constant sigma type, or if, because another name is used for such product, this is impossible.

[Sebastien Gouezel]

I agree that a Sigma type is more natural than a product for the tangent bundle. I have initially defined the tangent bundle as a product to get something nice for vector spaces, but this is only an implementation detail. I will try toredefine it to be a Sigma type, as this should be more handy for Riemannian spaces.

[Nicolò Cavalleri]

Sebastien Gouezel said:

I agree that a Sigma type is more natural than a product for the tangent bundle. I have initially defined the tangent bundle as a product to get something nice for vector spaces, but this is only an implementation detail. I will try toredefine it to be a Sigma type, as this should be more handy for Riemannian spaces.

I think it is perfect as it is if we could make Lean recognize a product as a Sigma type. If this is not possible are you planning to change the base type from product to constant sigma type? That would probably be enough I guess, or are you thinking of changing more?

[Sebastien Gouezel]

I am planning to redefine the total space of a topological fiber bundle core as Σ (x : B), Z.fiber x (where Z is the bundled topological fiber bundle core). Since all the fibers are the same type F, this is indeed a constant sigma type, but from the point of view of typeclass inference this is a little bit better, as one might register additional structures on Z.fiber x, for instance a euclidean space structure that might depend on x, and Lean shouldn't get confused.

And no, making Lean recognize a product as a Sigma type doesn't seem reasonable, they are really different things from the point of view of type theory.

[Nicolò Cavalleri]

Ok cool as soon as you have a working definition let me know (I mean even if it just a branch and not yet ready for PR) so that I can try to adapt and test the second vector bundle experiment to it!

[Sebastien Gouezel]

#3966

[Patrick Massot]

Does it mean we now have dependent type hell when comparing two vectors at two propositionaly equal points?

[Sebastien Gouezel]

No, if you just take the vector, it belongs to the tangent space at x, which is just a copy of the model vector space, so comparing two vectors at two propositionally equal points (or even at different points!) is not a problem for Lean. The difference is only how these tangent spaces are put together to form the tangent bundle.

[Patrick Massot]

Ok, good.