Lie algebra of a Lie group

Stream: Is there code for X?

[Kevin Buzzard]

I'm asking it on "is there code for X" but I'm pretty sure there isn't. So what I'm really asking for is whether the community has some kind of strategy for the construction of the Lie algebra structure on the tangent space at the identity of a Lie group. I have never used the manifold side of the library but my understanding is that we have Lie groups and we have the tangent space at the identity, but as far as I know we're missing the structure of the bracket.

The entire construction can be done algebraically; if H is a commutative Hopf algebra over a commutative ring R then Spec(H) is an affine algebraic group scheme over Spec(R) and hence an analogue of a Lie group in the algebro-geometric category (especially if you imagine R is a field, for example the real numbers, so Spec(R) is just one point). The identity section Spec(R) -> Spec(H) corresponds to the counit map H -> R, and if m is its kernel then Hom_{R-mod}(m/m^2,R) (at least if R is a field) will have a Lie algebra structure on it which looks like a project I would be much clearer about how to tackle. NB The algebraic construction raises the issue of proving that the construction commutes with the analytification functor, something which I suspect will not be treated in the literature because "how could it be any other way".

For the definition of an automorphic representation, something I plan on working on this week, we will need the analytic (Lie group) version of everything, and also the definition of the action of the Lie algebra on C^infty functions on the Lie group via first order differential operators. I am very unclear about how much work this project is in practice.

Could someone even suggest a roadmap to this basic construction?

[Sébastien Gouëzel]

All this should be pretty direct:

• First, define the adjoint representation: for fixed g, consider h -> g h g^{-1}. It's a smooth map, stabilizing the identity, so its derivative ad h is a linear map of the Lie algebra (aka the tangent space at the identity).
• Check that, given v in the Lie algebra, then h -> ad h v is smooth. Therefore, its derivative at the identity is a linear map from the Lie algebra to the tangent space of the Lie algebra, which is canonically identified with the Lie algebra. This is the Lie bracket.
• Check that it satisfies all the axioms of a Lie algebra. This will probably be a little bit cumbersome, but that's the way it has to be, I think. For the Jacobi identity, you probably need to know that the second derivative is symmetric, but this is true for analytic manifolds over any field (not sure we have that, but since we have explicit formulas for the iterated derivative of analytic maps it shouldn't be hard).
• To let the Lie algebra act on smooth functions, just let L_v f (g) be the derivative of the function f at the point g applied to the vector g v (well, the derivative at the identity of left multiplication by g, applied to the vector v).

[Florent Schaffhauser]

It's just notation, but maybe write Ad g for the derivative at 1_G of h -> g h g ^ {-1} and then ad : Lie(G) -> End(Lie (G)) for the derivative at 1_G of Ad : G -> GL(Lie(G)) ? One can also see tangent vectors at 1_G as left-invariant vector fields / derivations of the coordinate ring, depending on your point of view, and then define the bracket as a commutator of those. The upshot is that this gives Jacobi for free.

[Johan Commelin]

Wasn't there a mathlib3 PR that did left-invariant differential forms derivation?

[Winston Yin (尹維晨)]

docs#LeftInvariantDerivation

[Winston Yin (尹維晨)]

@Sébastien Gouëzel Care has to be taken re: infinite dimensional manifolds, where the Lie algebra at the identity (consisting of differential operators) cannot in general be identified with the tangent vectors (members of the model vector space, or equivalence classes of smooth curves through the identity).

[Winston Yin (尹維晨)]

In the current mathlib, the latter kind of tangent vectors do not form a Lie algebra.

[Winston Yin (尹維晨)]

There was a thread some months ago about properly developing infinite dimensional manifolds, but I have neither the time nor the expertise at the moment to envision a road map.

[Kevin Buzzard]

I only need Lie algebras for real reductive groups which are by definition finite-dimensional

[Kevin Buzzard]

@Floris van Doorn can you tell your students that any of them who are coming to my course and want to work on the Lie algebra of a Lie group should DM me on Zulip and ask for access to the private course channel?

[Floris van Doorn]

I did, but I think that the students that are planning to come are already part of that channel.

[Kevin Buzzard]

Winston Yin (尹維晨) said:

docs#LeftInvariantDerivation

Sorry for taking so long to reply @Winston Yin (尹維晨) . This is exactly what I want! And thank you to Patrick Massot for making this clear to me :-)

The final step is to write down the Lie algebra morphism from the real Lie algebra of $G$ to the $\mathbb{C}$-endomorphisms of the smooth complex-valued functions on $G$ (which has a complex Lie algebra structure $[a,b]=ab-ba$ where multiplication is function composition). I can't formalise the statement unfortunately, because I don't know my way around the manifold library, but I know I can definitely take it from there.