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}
(hf : smooth I' I f)
(hg : smooth I' I 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}
(hf : smooth I' I f)
(hg : smooth I' I 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.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}
(hf : smooth_on I' I f s)
(hg : smooth_on I' I g s) :
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}
(hf : smooth_on I' I f s)
(hg : smooth_on I' I g s) :
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_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] :
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}
(hf : smooth I' I f) :
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}
(hf : smooth I' I f) :
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}
(hf : smooth_on I' I f s) :
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}
(hf : smooth_on I' I f s) :
@[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')
@[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'] :
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_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_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.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]
(c : lie_add_group_core I 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]
(c : lie_group_core I 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 π(π, E) E