Theory Lie_Algebra
section ‹The Lie algebra of a Lie Group›
theory Lie_Algebra
imports
Lie_Group
Manifold_Lie_Bracket
Smooth_Manifolds.Cotangent_Space
begin
sublocale lie_group ⊆ smooth_manifold by unfold_locales
locale lie_algebra_morphism =
src: lie_algebra S1 scale1 bracket1 +
dest: lie_algebra S2 scale2 bracket2 +
linear_on S1 S2 scale1 scale2 f
for S1 S2
and scale1::"'a::field ⇒ 'b ⇒ 'b::ab_group_add" and scale2::"'a::field ⇒ 'c ⇒ 'c::ab_group_add"
and bracket1 and bracket2
and f +
assumes bracket_hom: "⋀X Y. X ∈ S1 ⟹ Y ∈ S1 ⟹ f (bracket1 X Y) = bracket2 (f X) (f Y)"
text ‹Multiple isomorphic Lie algebras can be referred to as ``the'' Lie algebra $\mathfrak g$
of a given Lie group $G$. One Lie algebra is already guaranteed to exist for any Lie group
by virtue of @{thm smooth_manifold.lie_algebra_of_smooth_vector_fields}. We give an isomorphism
between the subalgebra of \emph{left-invariant} (smooth) vector fields and the tangent space
at identity, and take the latter to be ``the'' Lie algebra $\mathfrak g$.›
context lie_group begin
text ‹Some notation, for simplicity: the Lie group (or here, its carrier) is $G$, and the tangent
space at the identity (the Lie algebra) is $\mathfrak g$.›
notation carrier (‹G›)
definition tangent_space_at_identity (‹𝔤›)
where "tangent_space_at_identity = tangent_space tms_one"
subsection ‹(Left-)invariant vector fields›
text ‹A vector field $X$ is invariant under some $k$-smooth map $F$ if the vector assigned to a
point $F(p)$ by $X$ is the same as the vector assigned by (the push-forward under) $F$ to the
vector $X(p)$. Essentially, $F$ and $X$ ``commute''.›
definition (in c_manifold) vector_field_invariant_under :: "'a vector_field ⇒ ('a⇒'a) ⇒ bool"
(infix ‹invariant'_under› 80)
where "X invariant_under F ≡ ∀p∈carrier. ∀f∈diff_fun_space.
X (F p) f = (diff.push_forward k charts charts F) (X p) f"
definition (in c_automorphism) invariant :: "'a vector_field ⇒ bool"
where "invariant X ≡ ∀p∈carrier. ∀g∈src.diff_fun_space. X (f p) g = push_forward (X p) g"
lemma (in c_automorphism) invariant_simp: "src.vector_field_invariant_under X f = invariant X"
unfolding src.vector_field_invariant_under_def invariant_def by simp
lemma (in c_manifold) vector_field_invariant_underD: "X (F p) f = X p (restrict0 carrier (f ∘ F))"
if "X invariant_under F" "diff k charts charts F" "p∈carrier" "f∈diff_fun_space"
using that by (auto simp: vector_field_invariant_under_def diff.push_forward_def)
lemma (in c_manifold) vector_field_invariant_underI: "X invariant_under F"
if "diff k charts charts F" "⋀p f. p∈carrier ⟹ f∈diff_fun_space ⟹ X (F p) f = X p (restrict0 carrier (f ∘ F))"
by (simp add: vector_field_invariant_under_def diff.push_forward_def that)
notation vector_field_invariant_under (infix ‹invariant'_under› 80)
abbreviation "L_invariant X ≡ ∀p∈carrier. X invariant_under (ℒ p)"
lemma L_invariantD [dest]: "X (tms p q) f = X q (restrict0 G (f ∘ (ℒ p)))"
if "L_invariant X" "p∈G" "q∈G" "f∈diff_fun_space"
using vector_field_invariant_underD diff_tms(1) that by auto
lemma L_invariantI [intro]: "L_invariant X"
if "⋀p q f. p∈carrier ⟹ q∈carrier ⟹ f∈diff_fun_space ⟹ X (tms p q) f = X q (restrict0 carrier (f ∘ (ℒ p)))"
using that vector_field_invariant_underI diff_tms(1) by auto
lemma lie_bracket_left_invariant:
assumes "L_invariant X" "smooth_vector_field X"
and "L_invariant Y" "smooth_vector_field Y"
shows "L_invariant [X;Y]" "smooth_vector_field [X;Y]"
proof
fix p assume p: "p∈G"
show "vector_field_invariant_under [X;Y] (ℒ p)"
proof (intro vector_field_invariant_underI)
fix q f
assume q: "q∈G" and f: "f∈diff_fun_space"
have 1: "restrict0 G ((Z ˝ f) ∘ ℒ p) = Z ˝ (restrict0 G (f ∘ ℒ p))"
if Z: "L_invariant Z" "extensional0 carrier Z" for Z
proof
fix t show "restrict0 G ((Z ˝ f) ∘ tms p) t = Z t (restrict0 G (f ∘ tms p))"
apply (cases "t∈G")
subgoal
using f p Z vector_field_invariant_underD[OF _ _ q smooth_vf_diff_fun_space]
by (auto)
using Z by (simp add: extensional0_outside)
qed
show "[X;Y] (tms p q) f = [X;Y] q (restrict0 G (f ∘ tms p))"
unfolding lie_bracket_def
using assms diff_tms(1) assms
by (auto simp: 1 p f vector_field_invariant_underD[OF _ _ q smooth_vf_diff_fun_space] smooth_vector_fieldE(2))
qed (simp add: p diff_tms(1))
qed (simp_all add: assms(2,4) lie_bracket_closed)
text ‹In fact, left-invariant smooth vector fields form a Lie subalgebra.›
lemma subspace_of_left_invariant_svf:
fixes 𝔛⇩ℒ defines "𝔛⇩ℒ ≡ {X ∈ SVF. L_invariant X}"
shows "subspace 𝔛⇩ℒ"
proof (unfold subspace_def, safe)
interpret SVF: lie_algebra SVF scaleR lie_bracket_of_smooth_vector_fields
using lie_algebra_of_smooth_vector_fields by simp
have "L_invariant 0"
apply (intro ballI vector_field_invariant_underI) by (simp_all add: diff_tms(1))
thus "0 ∈ 𝔛⇩ℒ" unfolding assms(1) using SVF.m1.mem_zero by blast
fix c and x
assume x: "x ∈ 𝔛⇩ℒ"
then have "L_invariant (c *⇩R x)"
apply (intro ballI vector_field_invariant_underI) using assms by (auto simp add: diff_tms(1))
thus "c *⇩R x ∈ 𝔛⇩ℒ" unfolding assms(1) using SVF.m1.mem_scale x assms by blast
fix y
assume y: "y ∈ 𝔛⇩ℒ"
then have "L_invariant (x + y)"
apply (intro ballI vector_field_invariant_underI) using assms vector_field_invariant_underD x by (auto simp: diff_tms(1))
thus "x + y ∈ 𝔛⇩ℒ" unfolding assms(1) using SVF.m1.mem_add assms x y by blast
qed
lemma lie_algebra_of_left_invariant_svf:
fixes 𝔛⇩ℒ defines "𝔛⇩ℒ ≡ {X. smooth_vector_field X ∧ L_invariant X}"
shows "lie_algebra 𝔛⇩ℒ (*⇩R) (λX Y. [X;Y])"
proof -
interpret SVF: lie_algebra SVF scaleR lie_bracket_of_smooth_vector_fields
using lie_algebra_of_smooth_vector_fields by simp
show ?thesis
using assms subspace_of_left_invariant_svf by (auto intro: SVF.lie_subalgebra
simp: SVF.m1.implicit_subspace_with subspace_with lie_bracket_left_invariant SVF_def)
qed
end
end