mathlib documentation

geometry.manifold.algebra.lie_group

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

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

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
@[instance]
def lie_add_group.to_has_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_4) [add_group G] [topological_space G] [topological_add_group G] [charted_space H G] [s : lie_add_group I G] :

@[instance]
def lie_group.to_has_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_4) [group G] [topological_space G] [topological_group G] [charted_space H G] [s : lie_group I G] :

@[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

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_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 : β„•) :
smooth I I (Ξ» (a : G), a ^ 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] :
smooth I I (λ (x : G), x⁻¹)

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] :
smooth I I (Ξ» (x : G), -x)

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) :
smooth I' I (λ (x : M), (f x)⁻¹)

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) :
smooth I' I (Ξ» (x : M), -f x)

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) :
smooth_on I' I (Ξ» (x : M), -f x) 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) :
smooth_on I' I (λ (x : M), (f x)⁻¹) 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] [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'] [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] [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'] [lie_group I' G'] :
lie_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] [add_group G] [topological_add_group G] [lie_add_group I G] (G' : Type u_5) [topological_space G'] [charted_space E' G'] [add_group G'] [topological_add_group G'] [lie_add_group I' G'] :
Type (max u_4 u_5)

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] [group G] [topological_group G] [lie_group I G] (G' : Type u_5) [topological_space G'] [charted_space E' G'] [group G'] [topological_group G'] [lie_group I' G'] :
Type (max u_4 u_5)

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] [group G] [topological_group G] [lie_group I G] {G' : Type u_5} [topological_space G'] [charted_space E' G'] [group G'] [topological_group G'] [lie_group I' G'] :

Equations
@[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] [add_group G] [topological_add_group G] [lie_add_group I G] {G' : Type u_5} [topological_space G'] [charted_space E' G'] [add_group G'] [topological_add_group G'] [lie_add_group I' 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] [group G] [topological_group G] [lie_group I G] {G' : Type u_5} [topological_space G'] [charted_space E' G'] [group G'] [topological_group G'] [lie_group I' 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] [add_group G] [topological_add_group G] [lie_add_group I G] {G' : Type u_5} [topological_space G'] [charted_space E' G'] [add_group G'] [topological_add_group G'] [lie_add_group I' 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] [add_group G] [topological_add_group G] [lie_add_group I G] {G' : Type u_5} [topological_space G'] [charted_space E' G'] [add_group G'] [topological_add_group G'] [lie_add_group I' 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] [group G] [topological_group G] [lie_group I G] {G' : Type u_5} [topological_space G'] [charted_space E' G'] [group G'] [topological_group G'] [lie_group I' G'] :

Equations
@[nolint]
def lie_add_group_core.to_smooth_manifold_with_corners {π•œ : 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] (s : lie_add_group_core I G) :

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] :
Prop

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.

@[nolint]
def lie_group_core.to_smooth_manifold_with_corners {π•œ : 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] (s : lie_group_core I G) :

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] :
Prop

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] [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] [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] [group G] (c : lie_group_core 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] [add_group G] (c : lie_add_group_core I G) :

Normed spaces are Lie groups

@[instance]
def normed_space_lie_group {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {E : Type u_2} [normed_group E] [normed_space π•œ E] :