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
lie_add_group I G: a Lie additive group whereGis a manifold on the model with cornersI.lie_group I G: a Lie multiplicative group whereGis a manifold on the model with cornersI.lie_add_group_morphism I I' G G': morphism of addittive Lie groupslie_group_morphism I I' G G': morphism of Lie groupslie_add_group_core I G: allows to define a Lie additive group without first proving it is a topological additive group.lie_group_core I G: allows to define a Lie group without first proving it is a topological group.reals_lie_group: real numbers are a Lie group
Implementation notes
A priori, a Lie group here is a manifold with corners.
The definition of Lie group cannot require I : model_with_corners ๐ 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 model_prod 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 : model_with_corners ๐ E H.
@[class]
structure
lie_add_group
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space ๐ E]
(I : model_with_corners ๐ E H)
(G : Type u_4)
[add_group G]
[topological_space G]
[topological_add_group G]
[charted_space H G] :
Prop
- to_smooth_manifold_with_corners : smooth_manifold_with_corners I G
- smooth_add : smooth (I.prod I) I (ฮป (p : G ร G), p.fst + p.snd)
- smooth_neg : smooth I I (ฮป (a : G), -a)
A Lie (additive) group is a group and a smooth manifold at the same time in which the addition and negation operations are smooth.
@[class]
structure
lie_group
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space ๐ E]
(I : model_with_corners ๐ E H)
(G : Type u_4)
[group G]
[topological_space G]
[topological_group G]
[charted_space H G] :
Prop
- to_smooth_manifold_with_corners : smooth_manifold_with_corners I G
- smooth_mul : smooth (I.prod I) I (ฮป (p : G ร G), p.fst * p.snd)
- smooth_inv : smooth I I (ฮป (a : G), aโปยน)
A Lie group is a group and a smooth manifold at the same time in which the multiplication and inverse operations are smooth.
Instances
theorem
smooth_add
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space ๐ E]
{I : model_with_corners ๐ E H}
{G : Type u_5}
[topological_space G]
[charted_space H G]
[add_group G]
[topological_add_group G]
[lie_add_group I G] :
theorem
smooth_mul
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space ๐ E]
{I : model_with_corners ๐ E H}
{G : Type u_5}
[topological_space G]
[charted_space H G]
[group G]
[topological_group G]
[lie_group I G] :
theorem
smooth.mul
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space ๐ E]
{I : model_with_corners ๐ E H}
{G : Type u_5}
[topological_space G]
[charted_space H G]
[group G]
[topological_group G]
[lie_group I G]
{E' : Type u_6}
[normed_group E']
[normed_space ๐ E']
{H' : Type u_7}
[topological_space H']
{I' : model_with_corners ๐ E' H'}
{M : Type u_8}
[topological_space M]
[charted_space H' M]
[smooth_manifold_with_corners I' M]
{f g : M โ G} :
theorem
smooth.add
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space ๐ E]
{I : model_with_corners ๐ E H}
{G : Type u_5}
[topological_space G]
[charted_space H G]
[add_group G]
[topological_add_group G]
[lie_add_group I G]
{E' : Type u_6}
[normed_group E']
[normed_space ๐ E']
{H' : Type u_7}
[topological_space H']
{I' : model_with_corners ๐ E' H'}
{M : Type u_8}
[topological_space M]
[charted_space H' M]
[smooth_manifold_with_corners I' M]
{f g : M โ G} :
theorem
smooth_left_mul
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space ๐ E]
{I : model_with_corners ๐ E H}
{G : Type u_5}
[topological_space G]
[charted_space H G]
[group G]
[topological_group G]
[lie_group I G]
{a : G} :
theorem
smooth_left_add
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space ๐ E]
{I : model_with_corners ๐ E H}
{G : Type u_5}
[topological_space G]
[charted_space H G]
[add_group G]
[topological_add_group G]
[lie_add_group I G]
{a : G} :
theorem
smooth_right_add
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space ๐ E]
{I : model_with_corners ๐ E H}
{G : Type u_5}
[topological_space G]
[charted_space H G]
[add_group G]
[topological_add_group G]
[lie_add_group I G]
{a : G} :
theorem
smooth_right_mul
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space ๐ E]
{I : model_with_corners ๐ E H}
{G : Type u_5}
[topological_space G]
[charted_space H G]
[group G]
[topological_group G]
[lie_group I G]
{a : G} :
theorem
smooth_on.add
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space ๐ E]
{I : model_with_corners ๐ E H}
{G : Type u_5}
[topological_space G]
[charted_space H G]
[add_group G]
[topological_add_group G]
[lie_add_group I G]
{E' : Type u_6}
[normed_group E']
[normed_space ๐ E']
{H' : Type u_7}
[topological_space H']
{I' : model_with_corners ๐ E' H'}
{M : Type u_8}
[topological_space M]
[charted_space H' M]
[smooth_manifold_with_corners I' M]
{f g : M โ G}
{s : set M} :
theorem
smooth_on.mul
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space ๐ E]
{I : model_with_corners ๐ E H}
{G : Type u_5}
[topological_space G]
[charted_space H G]
[group G]
[topological_group G]
[lie_group I G]
{E' : Type u_6}
[normed_group E']
[normed_space ๐ E']
{H' : Type u_7}
[topological_space H']
{I' : model_with_corners ๐ E' H'}
{M : Type u_8}
[topological_space M]
[charted_space H' M]
[smooth_manifold_with_corners I' M]
{f g : M โ G}
{s : set M} :
theorem
smooth_pow
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space ๐ E]
{I : model_with_corners ๐ E H}
{G : Type u_5}
[topological_space G]
[charted_space H G]
[group G]
[topological_group G]
[lie_group I G]
(n : โ) :
theorem
smooth_neg
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space ๐ E]
{I : model_with_corners ๐ E H}
{G : Type u_5}
[topological_space G]
[charted_space H G]
[add_group G]
[topological_add_group G]
[lie_add_group I G] :
theorem
smooth_inv
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space ๐ E]
{I : model_with_corners ๐ E H}
{G : Type u_5}
[topological_space G]
[charted_space H G]
[group G]
[topological_group G]
[lie_group I G] :
theorem
smooth.neg
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space ๐ E]
{I : model_with_corners ๐ E H}
{G : Type u_5}
[topological_space G]
[charted_space H G]
[add_group G]
[topological_add_group G]
[lie_add_group I G]
{E' : Type u_6}
[normed_group E']
[normed_space ๐ E']
{H' : Type u_7}
[topological_space H']
{I' : model_with_corners ๐ E' H'}
{M : Type u_8}
[topological_space M]
[charted_space H' M]
[smooth_manifold_with_corners I' M]
{f : M โ G} :
theorem
smooth.inv
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space ๐ E]
{I : model_with_corners ๐ E H}
{G : Type u_5}
[topological_space G]
[charted_space H G]
[group G]
[topological_group G]
[lie_group I G]
{E' : Type u_6}
[normed_group E']
[normed_space ๐ E']
{H' : Type u_7}
[topological_space H']
{I' : model_with_corners ๐ E' H'}
{M : Type u_8}
[topological_space M]
[charted_space H' M]
[smooth_manifold_with_corners I' M]
{f : M โ G} :
theorem
smooth_on.inv
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space ๐ E]
{I : model_with_corners ๐ E H}
{G : Type u_5}
[topological_space G]
[charted_space H G]
[group G]
[topological_group G]
[lie_group I G]
{E' : Type u_6}
[normed_group E']
[normed_space ๐ E']
{H' : Type u_7}
[topological_space H']
{I' : model_with_corners ๐ E' H'}
{M : Type u_8}
[topological_space M]
[charted_space H' M]
[smooth_manifold_with_corners I' M]
{f : M โ G}
{s : set M} :
theorem
smooth_on.neg
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space ๐ E]
{I : model_with_corners ๐ E H}
{G : Type u_5}
[topological_space G]
[charted_space H G]
[add_group G]
[topological_add_group G]
[lie_add_group I G]
{E' : Type u_6}
[normed_group E']
[normed_space ๐ E']
{H' : Type u_7}
[topological_space H']
{I' : model_with_corners ๐ E' H'}
{M : Type u_8}
[topological_space M]
[charted_space H' M]
[smooth_manifold_with_corners I' M]
{f : M โ G}
{s : set M} :
@[instance]
def
prod.lie_group
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space ๐ E]
{I : model_with_corners ๐ E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[group G]
[topological_group G]
[h : lie_group I G]
{E' : Type u_5}
[normed_group E']
[normed_space ๐ E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners ๐ E' H'}
{G' : Type u_7}
[topological_space G']
[charted_space H' G']
[group G']
[topological_group G']
[h' : lie_group I' G'] :
Equations
@[instance]
def
prod.lie_add_group
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space ๐ E]
{I : model_with_corners ๐ E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[add_group G]
[topological_add_group G]
[h : lie_add_group I G]
{E' : Type u_5}
[normed_group E']
[normed_space ๐ E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners ๐ E' H'}
{G' : Type u_7}
[topological_space G']
[charted_space H' G']
[add_group G']
[topological_add_group G']
[h' : lie_add_group I' G'] :
lie_add_group (I.prod I') (G ร G')
structure
lie_add_group_morphism
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{E : Type u_2}
[normed_group E]
[normed_space ๐ E]
{E' : Type u_3}
[normed_group E']
[normed_space ๐ E']
(I : model_with_corners ๐ E E)
(I' : model_with_corners ๐ E' E')
(G : Type u_4)
[topological_space G]
[charted_space E G]
[smooth_manifold_with_corners I G]
[add_group G]
[topological_add_group G]
[lie_add_group I G]
(G' : Type u_5)
[topological_space G']
[charted_space E' G']
[smooth_manifold_with_corners I' G']
[add_group G']
[topological_add_group G']
[lie_add_group I' G'] :
Type (max u_4 u_5)
- to_add_monoid_hom : G โ+ G'
- smooth_to_fun : smooth I I' c.to_add_monoid_hom.to_fun
Morphism of additive Lie groups.
structure
lie_group_morphism
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{E : Type u_2}
[normed_group E]
[normed_space ๐ E]
{E' : Type u_3}
[normed_group E']
[normed_space ๐ E']
(I : model_with_corners ๐ E E)
(I' : model_with_corners ๐ E' E')
(G : Type u_4)
[topological_space G]
[charted_space E G]
[smooth_manifold_with_corners I G]
[group G]
[topological_group G]
[lie_group I G]
(G' : Type u_5)
[topological_space G']
[charted_space E' G']
[smooth_manifold_with_corners I' G']
[group G']
[topological_group G']
[lie_group I' G'] :
Type (max u_4 u_5)
- to_monoid_hom : G โ* G'
- smooth_to_fun : smooth I I' c.to_monoid_hom.to_fun
Morphism of Lie groups.
@[instance]
def
lie_add_group_morphism.has_zero
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{E : Type u_2}
[normed_group E]
[normed_space ๐ E]
{E' : Type u_3}
[normed_group E']
[normed_space ๐ E']
{I : model_with_corners ๐ E E}
{I' : model_with_corners ๐ E' E'}
{G : Type u_4}
[topological_space G]
[charted_space E G]
[smooth_manifold_with_corners I G]
[add_group G]
[topological_add_group G]
[lie_add_group I G]
{G' : Type u_5}
[topological_space G']
[charted_space E' G']
[smooth_manifold_with_corners I' G']
[add_group G']
[topological_add_group G']
[lie_add_group I' G'] :
has_zero (lie_add_group_morphism I I' G G')
@[instance]
def
lie_group_morphism.has_one
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{E : Type u_2}
[normed_group E]
[normed_space ๐ E]
{E' : Type u_3}
[normed_group E']
[normed_space ๐ E']
{I : model_with_corners ๐ E E}
{I' : model_with_corners ๐ E' E'}
{G : Type u_4}
[topological_space G]
[charted_space E G]
[smooth_manifold_with_corners I G]
[group G]
[topological_group G]
[lie_group I G]
{G' : Type u_5}
[topological_space G']
[charted_space E' G']
[smooth_manifold_with_corners I' G']
[group G']
[topological_group G']
[lie_group I' G'] :
has_one (lie_group_morphism I I' G G')
Equations
- lie_group_morphism.has_one = {one := {to_monoid_hom := 1, smooth_to_fun := _}}
@[instance]
def
lie_group_morphism.inhabited
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{E : Type u_2}
[normed_group E]
[normed_space ๐ E]
{E' : Type u_3}
[normed_group E']
[normed_space ๐ E']
{I : model_with_corners ๐ E E}
{I' : model_with_corners ๐ E' E'}
{G : Type u_4}
[topological_space G]
[charted_space E G]
[smooth_manifold_with_corners I G]
[group G]
[topological_group G]
[lie_group I G]
{G' : Type u_5}
[topological_space G']
[charted_space E' G']
[smooth_manifold_with_corners I' G']
[group G']
[topological_group G']
[lie_group I' G'] :
inhabited (lie_group_morphism I I' G G')
Equations
@[instance]
def
lie_add_group_morphism.inhabited
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{E : Type u_2}
[normed_group E]
[normed_space ๐ E]
{E' : Type u_3}
[normed_group E']
[normed_space ๐ E']
{I : model_with_corners ๐ E E}
{I' : model_with_corners ๐ E' E'}
{G : Type u_4}
[topological_space G]
[charted_space E G]
[smooth_manifold_with_corners I G]
[add_group G]
[topological_add_group G]
[lie_add_group I G]
{G' : Type u_5}
[topological_space G']
[charted_space E' G']
[smooth_manifold_with_corners I' G']
[add_group G']
[topological_add_group G']
[lie_add_group I' G'] :
inhabited (lie_add_group_morphism I I' G G')
@[instance]
def
lie_add_group_morphism.has_coe_to_fun
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{E : Type u_2}
[normed_group E]
[normed_space ๐ E]
{E' : Type u_3}
[normed_group E']
[normed_space ๐ E']
{I : model_with_corners ๐ E E}
{I' : model_with_corners ๐ E' E'}
{G : Type u_4}
[topological_space G]
[charted_space E G]
[smooth_manifold_with_corners I G]
[add_group G]
[topological_add_group G]
[lie_add_group I G]
{G' : Type u_5}
[topological_space G']
[charted_space E' G']
[smooth_manifold_with_corners I' G']
[add_group G']
[topological_add_group G']
[lie_add_group I' G'] :
has_coe_to_fun (lie_add_group_morphism I I' G G')
@[instance]
def
lie_group_morphism.has_coe_to_fun
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{E : Type u_2}
[normed_group E]
[normed_space ๐ E]
{E' : Type u_3}
[normed_group E']
[normed_space ๐ E']
{I : model_with_corners ๐ E E}
{I' : model_with_corners ๐ E' E'}
{G : Type u_4}
[topological_space G]
[charted_space E G]
[smooth_manifold_with_corners I G]
[group G]
[topological_group G]
[lie_group I G]
{G' : Type u_5}
[topological_space G']
[charted_space E' G']
[smooth_manifold_with_corners I' G']
[group G']
[topological_group G']
[lie_group I' G'] :
has_coe_to_fun (lie_group_morphism I I' G G')
Equations
- lie_group_morphism.has_coe_to_fun = {F := ฮป (a : lie_group_morphism I I' G G'), G โ G', coe := ฮป (a : lie_group_morphism I I' G G'), a.to_monoid_hom.to_fun}
structure
lie_add_group_core
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{E : Type u_2}
[normed_group E]
[normed_space ๐ E]
(I : model_with_corners ๐ E E)
(G : Type u_3)
[add_group G]
[topological_space G]
[charted_space E G]
[smooth_manifold_with_corners I G] :
Prop
- smooth_add : smooth (I.prod I) I (ฮป (p : G ร G), p.fst + p.snd)
- smooth_neg : smooth I I (ฮป (a : G), -a)
Sometimes one might want to define a Lie additive group G without having proved previously
that G is a topological additive group. In such case it is possible to use lie_add_group_core
that does not require such instance, and then get a Lie group by invoking to_lie_add_group.
structure
lie_group_core
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{E : Type u_2}
[normed_group E]
[normed_space ๐ E]
(I : model_with_corners ๐ E E)
(G : Type u_3)
[group G]
[topological_space G]
[charted_space E G]
[smooth_manifold_with_corners I G] :
Prop
- smooth_mul : smooth (I.prod I) I (ฮป (p : G ร G), p.fst * p.snd)
- smooth_inv : smooth I I (ฮป (a : G), aโปยน)
Sometimes one might want to define a Lie group G without having proved previously that G is
a topological group. In such case it is possible to use lie_group_core that does not require such
instance, and then get a Lie group by invoking to_lie_group defined below.
theorem
lie_add_group_core.to_topological_add_group
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{E : Type u_2}
[normed_group E]
[normed_space ๐ E]
{I : model_with_corners ๐ E E}
{G : Type u_4}
[topological_space G]
[charted_space E G]
[smooth_manifold_with_corners I G]
[add_group G] :
lie_add_group_core I G โ topological_add_group G
theorem
lie_group_core.to_topological_group
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{E : Type u_2}
[normed_group E]
[normed_space ๐ E]
{I : model_with_corners ๐ E E}
{G : Type u_4}
[topological_space G]
[charted_space E G]
[smooth_manifold_with_corners I G]
[group G] :
lie_group_core I G โ topological_group G
theorem
lie_group_core.to_lie_group
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{E : Type u_2}
[normed_group E]
[normed_space ๐ E]
{I : model_with_corners ๐ E E}
{G : Type u_4}
[topological_space G]
[charted_space E G]
[smooth_manifold_with_corners I G]
[group G]
(c : lie_group_core I G) :
lie_group I G
theorem
lie_add_group_core.to_lie_add_group
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{E : Type u_2}
[normed_group E]
[normed_space ๐ E]
{I : model_with_corners ๐ E E}
{G : Type u_4}
[topological_space G]
[charted_space E G]
[smooth_manifold_with_corners I G]
[add_group G]
(c : lie_add_group_core I G) :
lie_add_group I G
Real numbers are a Lie group
@[instance]
def
normed_group_lie_group
{๐ : Type u_1}
[nondiscrete_normed_field ๐]
{E : Type u_2}
[normed_group E]
[normed_space ๐ E] :
lie_add_group (model_with_corners_self ๐ E) E
Equations
@[instance]