The Lie algebra of a Lie group

Given a Lie group, we define GroupLieAlgebra I G as its tangent space at the identity, and we endow it with a Lie bracket, as follows. Given two vectors v, w : GroupLieAlgebra I G, consider the associated left-invariant vector fields mulInvariantVectorField v (given at a point g by the image of v under the derivative of left-multiplication by g) and mulInvariantVectorField w. Then take their Lie bracket at the identity: this is by definition the bracket of v and w.

Due to general properties of the Lie bracket of vector fields, this gives a Lie algebra structure on GroupLieAlgebra I G.

Note that one can also define a Lie algebra on the space of left-invariant derivations on C^∞ functions (see LeftInvariantDerivation.instLieAlgebra). For finite-dimensional C^∞ real manifolds, this space of derivations can be canonically identified with the tangent space, and we recover the same Lie algebra structure (TODO: prove this). In other smoothness classes or on other fields, this identification is not always true, though, so the derivations point of view does not work in these settings. Therefore, the point of view in the current file is more general, and should be favored when possible.

The standing assumption in this file is that the group is C^n for n = minSmoothness 𝕜 3, i.e., it is C^3 over ℝ or ℂ, and analytic otherwise.

@[reducible, inline]

abbrev GroupLieAlgebra {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (G : Type u_4) [TopologicalSpace G] [ChartedSpace H G] [Group G] : Type u_3

The Lie algebra of a Lie group, i.e., its tangent space at the identity. We use the word GroupLieAlgebra instead of LieAlgebra as the latter is taken as a generic class.

Equations

• GroupLieAlgebra I G = TangentSpace I 1

@[reducible, inline]

abbrev AddGroupLieAlgebra {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (G : Type u_4) [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] : Type u_3

The Lie algebra of an additive Lie group, i.e., its tangent space at zero. We use the word AddGroupLieAlgebra instead of LieAlgebra as the latter is taken as a generic class.

Equations

• AddGroupLieAlgebra I G = TangentSpace I 0

noncomputable def mulInvariantVectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] (v : GroupLieAlgebra I G) (g : G) : TangentSpace I g

The invariant vector field associated to a vector v in the Lie alebra. At a point g, it is given by the image of v under left-multiplication by g.

Equations

• mulInvariantVectorField v g = (mfderiv I I (fun (x : G) => g * x) 1) v

noncomputable def addInvariantVectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] (v : AddGroupLieAlgebra I G) (g : G) : TangentSpace I g

The invariant vector field associated to a vector v in the Lie alebra. At a point g, it is given by the image of v under left-addition by g.

Equations

• addInvariantVectorField v g = (mfderiv I I (fun (x : G) => g + x) 0) v

theorem mulInvariantVectorField_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] (v w : GroupLieAlgebra I G) : mulInvariantVectorField (v + w) = mulInvariantVectorField v + mulInvariantVectorField w

theorem addInvariantVectorField_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] (v w : AddGroupLieAlgebra I G) : addInvariantVectorField (v + w) = addInvariantVectorField v + addInvariantVectorField w

theorem addInvariantVectorField_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] (c : 𝕜) (v : AddGroupLieAlgebra I G) : addInvariantVectorField (c • v) = c • addInvariantVectorField v

theorem mulInvariantVectorField_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] (c : 𝕜) (v : GroupLieAlgebra I G) : mulInvariantVectorField (c • v) = c • mulInvariantVectorField v

noncomputable instance instBracketGroupLieAlgebra {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] : Bracket (GroupLieAlgebra I G) (GroupLieAlgebra I G)

The Lie bracket of two vectors v and w in the Lie algebra of a Lie group is obtained by taking the Lie bracket of the associated invariant vector fields, at the identity.

Equations

• instBracketGroupLieAlgebra = { bracket := fun (v w : GroupLieAlgebra I G) => VectorField.mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1 }

noncomputable instance instBracketAddGroupLieAlgebra {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] : Bracket (AddGroupLieAlgebra I G) (AddGroupLieAlgebra I G)

The Lie bracket of two vectors v and w in the Lie algebra of an additive Lie group is obtained by taking the Lie bracket of the associated invariant vector fields, at zero.

Equations

• instBracketAddGroupLieAlgebra = { bracket := fun (v w : AddGroupLieAlgebra I G) => VectorField.mlieBracket I (addInvariantVectorField v) (addInvariantVectorField w) 0 }

theorem GroupLieAlgebra.bracket_def {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] (v w : GroupLieAlgebra I G) : ⁅v, w⁆ = VectorField.mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1

theorem AddGroupLieAlgebra.bracket_def {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] (v w : AddGroupLieAlgebra I G) : ⁅v, w⁆ = VectorField.mlieBracket I (addInvariantVectorField v) (addInvariantVectorField w) 0

@[simp]

theorem inverse_mfderiv_mul_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I (minSmoothness 𝕜 3) G] {g h : G} : (mfderiv I I (fun (b : G) => g * b) h).inverse = mfderiv I I (fun (b : G) => g⁻¹ * b) (g * h)

@[simp]

theorem inverse_mfderiv_add_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I (minSmoothness 𝕜 3) G] {g h : G} : (mfderiv I I (fun (b : G) => g + b) h).inverse = mfderiv I I (fun (b : G) => -g + b) (g + h)

theorem mpullback_mulInvariantVectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I (minSmoothness 𝕜 3) G] (g : G) (v : GroupLieAlgebra I G) : VectorField.mpullback I I (fun (x : G) => g * x) (mulInvariantVectorField v) = mulInvariantVectorField v

Invariant vector fields are invariant under pullbacks.

theorem mpullback_addInvariantVectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I (minSmoothness 𝕜 3) G] (g : G) (v : AddGroupLieAlgebra I G) : VectorField.mpullback I I (fun (x : G) => g + x) (addInvariantVectorField v) = addInvariantVectorField v

Invariant vector fields are invariant under pullbacks.

theorem mulInvariantVectorField_eq_mpullback {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I (minSmoothness 𝕜 3) G] (g : G) (V : (g : G) → TangentSpace I g) : mulInvariantVectorField (V 1) g = VectorField.mpullback I I (fun (x : G) => g⁻¹ * x) V g

theorem addInvariantVectorField_eq_mpullback {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I (minSmoothness 𝕜 3) G] (g : G) (V : (g : G) → TangentSpace I g) : addInvariantVectorField (V 0) g = VectorField.mpullback I I (fun (x : G) => -g + x) V g

theorem contMDiff_mulInvariantVectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I (minSmoothness 𝕜 3) G] (v : GroupLieAlgebra I G) : ContMDiff I I.tangent (minSmoothness 𝕜 2) fun (g : G) => { proj := g, snd := mulInvariantVectorField v g }

theorem contMDiff_addInvariantVectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I (minSmoothness 𝕜 3) G] (v : AddGroupLieAlgebra I G) : ContMDiff I I.tangent (minSmoothness 𝕜 2) fun (g : G) => { proj := g, snd := addInvariantVectorField v g }

theorem contMDiffAt_mulInvariantVectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I (minSmoothness 𝕜 3) G] (v : GroupLieAlgebra I G) {g : G} : ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun (g : G) => { proj := g, snd := mulInvariantVectorField v g }) g

theorem contMDiffAt_addInvariantVectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I (minSmoothness 𝕜 3) G] (v : AddGroupLieAlgebra I G) {g : G} : ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun (g : G) => { proj := g, snd := addInvariantVectorField v g }) g

theorem mdifferentiable_mulInvariantVectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I (minSmoothness 𝕜 3) G] (v : GroupLieAlgebra I G) : MDifferentiable I I.tangent fun (g : G) => { proj := g, snd := mulInvariantVectorField v g }

theorem mdifferentiable_addInvariantVectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I (minSmoothness 𝕜 3) G] (v : AddGroupLieAlgebra I G) : MDifferentiable I I.tangent fun (g : G) => { proj := g, snd := addInvariantVectorField v g }

theorem mdifferentiableAt_mulInvariantVectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I (minSmoothness 𝕜 3) G] (v : GroupLieAlgebra I G) {g : G} : MDifferentiableAt I I.tangent (fun (g : G) => { proj := g, snd := mulInvariantVectorField v g }) g

theorem mdifferentiableAt_addInvariantVectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I (minSmoothness 𝕜 3) G] (v : AddGroupLieAlgebra I G) {g : G} : MDifferentiableAt I I.tangent (fun (g : G) => { proj := g, snd := addInvariantVectorField v g }) g

theorem mulInvariantVector_mlieBracket {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I (minSmoothness 𝕜 3) G] [CompleteSpace E] (v w : GroupLieAlgebra I G) : mulInvariantVectorField (VectorField.mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1) = VectorField.mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w)

The invariant vector field associated to the value at the identity of the Lie bracket of two invariant vector fields, is everywhere the Lie bracket of the invariant vector fields.

theorem addInvariantVector_mlieBracket {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I (minSmoothness 𝕜 3) G] [CompleteSpace E] (v w : AddGroupLieAlgebra I G) : addInvariantVectorField (VectorField.mlieBracket I (addInvariantVectorField v) (addInvariantVectorField w) 0) = VectorField.mlieBracket I (addInvariantVectorField v) (addInvariantVectorField w)

The invariant vector field associated to the value at zero of the Lie bracket of two invariant vector fields, is everywhere the Lie bracket of the invariant vector fields.

noncomputable instance instLieRingGroupLieAlgebra {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I (minSmoothness 𝕜 3) G] [CompleteSpace E] : LieRing (GroupLieAlgebra I G)

The tangent space at the identity of a Lie group is a Lie ring, for the bracket given by the Lie bracket of invariant vector fields.

Equations

• instLieRingGroupLieAlgebra = { toAddCommGroup := instAddCommGroupTangentSpace I, toBracket := instBracketGroupLieAlgebra, add_lie := ⋯, lie_add := ⋯, lie_self := ⋯, leibniz_lie := ⋯ }

noncomputable instance instLieRingAddGroupLieAlgebra {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I (minSmoothness 𝕜 3) G] [CompleteSpace E] : LieRing (AddGroupLieAlgebra I G)

The tangent space at the identity of an additive Lie group is a Lie ring, for the bracket given by the Lie bracket of invariant vector fields.

Equations

• instLieRingAddGroupLieAlgebra = { toAddCommGroup := instAddCommGroupTangentSpace I, toBracket := instBracketAddGroupLieAlgebra, add_lie := ⋯, lie_add := ⋯, lie_self := ⋯, leibniz_lie := ⋯ }

noncomputable instance instLieAlgebraAddGroupLieAlgebra {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} [CompleteSpace E] {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I (minSmoothness 𝕜 3) G] : LieAlgebra 𝕜 (AddGroupLieAlgebra I G)

The tangent space at the identity of an additive Lie group is a Lie algebra, for the bracket given by the Lie bracket of invariant vector fields.

Equations

• instLieAlgebraAddGroupLieAlgebra = { toModule := instModuleTangentSpace I, lie_smul := ⋯ }

noncomputable instance instLieAlgebraGroupLieAlgebra {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I (minSmoothness 𝕜 3) G] [CompleteSpace E] : LieAlgebra 𝕜 (GroupLieAlgebra I G)

The tangent space at the identity of a Lie group is a Lie algebra, for the bracket given by the Lie bracket of invariant vector fields.

Equations

• instLieAlgebraGroupLieAlgebra = { toModule := instModuleTangentSpace I, lie_smul := ⋯ }