Quelle  Lie_Algebra.thy

(*  Title:       Lie_Algebra
    Author:      Richard Schmoetten <richard.schmoetten@ed.ac.uk>, 2024
    Maintainer:  Richard Schmoetten <richard.schmoetten@ed.ac.uk>
*)

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 (‹g›)
  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"

― ‹TODO this could be in an instance of 🍋‹diff› going from a manifold to itself,
 rather than 🍋‹diffeomorphism›, i.e. an endomorphism rather than an automorphism.›
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)

― ‹Repeat notation from @{thm c_manifold.vector_field_invariant_under_def}.›
notation vector_field_invariant_under (infix ‹invariant'_under› 80)
abbreviation "L_invariant X ≡ ∀p∈carrier. X invariant_under (L p)"

lemma L_invariantD [dest]: "X (tms p q) f = X q (restrict0 G (f ∘ (L 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 ∘ (L 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] (L 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) ∘ L p) = Z 🍋 (restrict0 G (f ∘ L 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 X_\<L> defines "X_\<L> ≡ {X ∈ SVF. L_invariant X}"
  shows "subspace X_\<L>"
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 ∈ X_\<L>" unfolding assms(1) using SVF.m1.mem_zero by blast

  fix c and x
  assume x: "x ∈ X_\<L>"
  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 ∈ X_\<L>" unfolding assms(1) using SVF.m1.mem_scale x assms by blast

  fix y
  assume y: "y ∈ X_\<L>"
  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 ∈ X_\<L>" unfolding assms(1) using SVF.m1.mem_add assms x y by blast
qed


lemma lie_algebra_of_left_invariant_svf:
  fixes X_\<L> defines "X_\<L> ≡ {X. smooth_vector_field X ∧ L_invariant X}"
  shows "lie_algebra X_\<L> (*_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