Lie groups #
A Lie group is a group that is also a smooth manifold, in which the group operations of
multiplication and inversion are smooth maps. Smoothness of the group multiplication means that
multiplication is a smooth mapping of the product manifold G
× G
into G
.
Note that, since a manifold here is not second-countable and Hausdorff a Lie group here is not guaranteed to be second-countable (even though it can be proved it is Hausdorff). Note also that Lie groups here are not necessarily finite dimensional.
Main definitions and statements #
LieAddGroup I G
: a Lie additive group whereG
is a manifold on the model with cornersI
.LieGroup I G
: a Lie multiplicative group whereG
is a manifold on the model with cornersI
.normedSpaceLieAddGroup
: a normed vector space over a nontrivially normed field is an additive Lie group.
Implementation notes #
A priori, a Lie group here is a manifold with corners.
The definition of Lie group cannot require I : ModelWithCorners 𝕜 E E
with the same space as the
model space and as the model vector space, as one might hope, beause in the product situation,
the model space is ModelProd E E'
and the model vector space is E × E'
, which are not the same,
so the definition does not apply. Hence the definition should be more general, allowing
I : ModelWithCorners 𝕜 E H
.
- compatible : ∀ {e e' : LocalHomeomorph G H}, e ∈ atlas H G → e' ∈ atlas H G → LocalHomeomorph.trans (LocalHomeomorph.symm e) e' ∈ contDiffGroupoid ⊤ I
- smooth_add : Smooth (ModelWithCorners.prod I I) I fun p => p.fst + p.snd
Negation is smooth in an additive Lie group.
A Lie (additive) group is a group and a smooth manifold at the same time in which the addition and negation operations are smooth.
Instances
- compatible : ∀ {e e' : LocalHomeomorph G H}, e ∈ atlas H G → e' ∈ atlas H G → LocalHomeomorph.trans (LocalHomeomorph.symm e) e' ∈ contDiffGroupoid ⊤ I
- smooth_mul : Smooth (ModelWithCorners.prod I I) I fun p => p.fst * p.snd
Inversion is smooth in a Lie group.
A Lie group is a group and a smooth manifold at the same time in which the multiplication and inverse operations are smooth.
Instances
An additive Lie group is an additive topological group. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].
A Lie group is a topological group. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].
Normed spaces are Lie groups #
Inversion is smooth away from
0
.
A smooth manifold with 0
and Inv
such that fun x ↦ x⁻¹
is smooth at all nonzero points.
Any complete normed (semi)field has this property.
Instances
In a manifold with smooth inverse away from 0
, the inverse is continuous away from 0
.
This is not an instance for technical reasons, see
note [Design choices about smooth algebraic structures].