Quelle  Lie_Group.thy

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

theory Lie_Group

imports
  "HOL-Analysis.Analysis"
  "HOL-Eisbach.Eisbach"
  More_Manifolds
begin


section ‹Definition of Lie Groups (as Locales)›

text ‹Some abbreviations for easier reading first. A binary operation is colloquially said
 continuous/smooth/differentiable on a manifold $M$ if it is so on the product manifold $M^2$.
 We fix the types of the binary operations in two of the definitions below, as the target space
 is made explicit only in the third (the one using term‹diff ∞›).›

abbreviation (input) "continuous_on_product_manifold charts (binop::'a==>'a==>'a::{second_countable_topology,t2_space}) ≡
  continuous_on (c_manifold_prod.carrier charts charts) (λ(a,b). binop a b)"
abbreviation (input) "smooth_on_product_manifold charts (binop::'a==>'a==>'a::{second_countable_topology,real_normed_vector}) ≡
  smooth_on (c_manifold_prod.carrier charts charts) (λ(a,b). binop a b)"
abbreviation (input) "diff_on_product_manifold charts binop ≡
  diff ∞ (c_manifold_prod.prod_charts charts charts) charts (λ(a,b). binop a b)"


subsection ‹Topological groups›

text ‹A group with a topology, such that the group operations are continuous.›

locale topological_group =
  manifold charts + group_on_with carrier tms tms_one dvsn invs
  for charts::"('a::{t2_space,second_countable_topology}, 'e::euclidean_space) chart set"
    and tms tms_one dvsn invs +
  assumes cts_mult: "continuous_on_product_manifold charts tms"
    and cts_inv: "continuous_on carrier invs"


subsection ‹Lie groups›

text ‹
 A Lie group is a group on a set, but instead of a carrier set, we specify
 a set of charts, which imply the carrier set as a (smooth) manifold $M$.
 Internally, we consider the product manifold, to define smoothness of multiplication $M \times M \to M$.
 It may be overkill to keep inverse and division separate, considering 🍋‹group_on_with› includes an axiom
 to relate the two, but this is how it's done in other Isabelle theories, so I'll keep it.
 It gives some extra flexibility, and an intro lemma using the more traditional group parameters
 (an operation, and an identity) and axioms is already provided in @{thm group_on_with_alt_intro}.
 ›
locale lie_group =
  c_manifold charts ∞ + group_on_with carrier tms tms_one dvsn invs
  for charts::"('a::{t2_space,second_countable_topology}, 'e::euclidean_space) chart set"
    and tms tms_one dvsn invs +
  assumes smooth_mult: "diff_on_product_manifold charts tms"
    and smooth_inv: "diff ∞ charts charts invs"

text ‹
 We can make a shortened locale for Lie groups where the inversion and division are implied.
 This does \emph{not} say anything about the implementation of inversion or division outside
 the carrier set. See also 🍋‹Groups_On_With.grp_on›.
 ›
locale lie_grp =
  c_manifold charts ∞ + grp_on carrier tms one
  for charts::"('a::{t2_space,second_countable_topology}, 'e::euclidean_space) chart set"
    and tms one +
  ― ‹multiplication and inversion are smooth›
  assumes smooth_mult: "diff_on_product_manifold charts tms"
    and smooth_inv: "diff ∞ charts charts invs"
begin

lemma is_lie_group: "lie_group charts tms one mns invs"
  unfolding lie_group_def lie_group_axioms_def
  by (auto simp: c_manifold_axioms smooth_mult is_group_on_with smooth_inv)

sublocale lie_group charts tms one mns invs
  using is_lie_group .

end

lemma lie_group_imp_lie_grp:
  assumes "lie_group charts pls one any_mns any_invs"
  shows "lie_grp charts pls one"
  unfolding lie_grp_def lie_grp_axioms_def apply (intro conjI)
  subgoal using assms lie_group_def by blast
  subgoal
    using assms unfolding grp_on_def grp_on_axioms_def lie_group_def group_on_with_def group_on_with_axioms_def
    by (meson assms group_on_with.right_minus lie_group.axioms(2))
  subgoal using assms unfolding lie_group_def lie_group_axioms_def by simp
  subgoal using assms unfolding lie_group_def lie_group_axioms_def
    by (smt (verit, ccfv_threshold) ‹grp_on (manifold.carrier charts) pls one› diff.diff_cong
      group_on_with.inv_is_unique group_on_with.right_minus group_on_with.uminus_mem grp_on.is_group_on_with)
  done

text ‹
 We give a few intro rules for the ‹lie_group› predicate, as well as an Eisbach method for further
 breaking down the proof of smoothness of the multiplication and inversion maps. This should
 lead to fairly organised proofs that some structure is a 🍋‹lie_group›.
 In general, I would prefer ‹group_manifold_imp_lie_group2› to ‹group_manifold_imp_lie_group›.
 ›

― ‹This lemma is mostly here to be reproved with restrictions to the allowed manifold,
 which would simplify the applicable definition of smoothness.
 E.g. if the manifold is a Euclidean space,
 ‹diff ∞› is just the standard analysis notion of "infinitely differentiable", i.e. ‹smooth_on›.›
lemma group_manifold_imp_lie_group [intro]:
  assumes is_manifold: "c_manifold c ∞"
    and is_group: "group_on_with (∪(domain ` c)) tms tms_1 dvsn invs"
    and smooth_mult: "diff ∞ (c_manifold_prod.prod_charts c c) c (λ(a,b). tms a b)"
    and smooth_inv: "diff ∞ c c invs"
  shows "lie_group c tms tms_1 dvsn invs"
  unfolding lie_group_def manifold.carrier_def lie_group_axioms_def
  by (simp_all add: c_manifold_prod_def is_manifold is_group smooth_inv smooth_mult)

lemma group_manifold_imp_lie_group2 [intro]:
  assumes is_manifold: "c_manifold c ∞"
    and is_group: "group_on_with (∪(domain ` c)) tms tms_1 dvsn invs"
    and smooth_mult: "diff_axioms ∞ (c_manifold_prod.prod_charts c c) c (λ(a,b). tms a b)"
    and smooth_inv: "diff_axioms ∞ c c invs"
  shows "lie_group c tms tms_1 dvsn invs"
  by (auto intro!: c_manifolds.intro diff.intro simp: assms c_manifold_prod.c_manifold_atlas_product c_manifold_prod_def)

lemma lie_grpI [intro]:
  fixes tms tms_1 c
  defines "invs ≡ grp_on.invs (∪(domain ` c)) tms tms_1"
  assumes is_manifold: "c_manifold c ∞"
    and is_group: "grp_on (∪(domain ` c)) tms tms_1"
    and smooth_mult: "diff_axioms ∞ (c_manifold_prod.prod_charts c c) c (λ(a,b). tms a b)"
    and smooth_inv: "diff_axioms ∞ c c invs"
  shows "lie_grp c tms tms_1"
  by (metis group_manifold_imp_lie_group2 grp_on.is_group_on_with invs_def is_group is_manifold
    lie_group_imp_lie_grp smooth_inv smooth_mult)

text ‹A small method to unfold the axioms of differentiability of group operations.
 Allows for succinct goals to be stated while quickly unfolding to a useful level of technicality.›
method unfold_diff_axioms = (
  unfold diff_axioms_def,
  rule allI,
  rule impI,
  (rule bexI)+,
  (rule conjI),
  rule_tac[2] conjI
)


subsection ‹Some lemmas about Lie groups (and other needed results).›
context lie_group begin

lemma obtain_chart_cover:
  assumes "S ⊆ carrier"
  obtains C where "∀c∈C. c∈atlas" "∀s∈S. ∃c∈C. s ∈ domain c"
  by (metis assms carrierE in_charts_in_atlas subset_iff)

lemma open_covered_by_charts:
  assumes "S ⊆ carrier" "open S"
  obtains C where "∀c∈C. c∈atlas" "S = ∪{domain c | c. c∈C}"
proof -
  obtain C where C: "∀c∈C. c∈atlas" "∀s∈S. ∃c∈C. s ∈ domain c"
    using obtain_chart_cover assms by blast
  let ?restr_chart = "λc. if domain c ⊆ S then c else restrict_chart S c"
  let ?C = "{?restr_chart c | c. c∈C}"
  have "∀c∈?C. c∈atlas"
    using C(1) restrict_chart_in_atlas by auto
  moreover have "S = ∪{domain c | c. c∈?C}"
    using assms(2) domain_restrict_chart by (auto, metis C(2) Int_iff, fastforce)
  ultimately show ?thesis using that by presburger
qed

lemma lie_prod: "c_manifold_prod ∞ charts charts"
  by unfold_locales

interpretation lie_prod: c_manifold_prod ∞ charts charts
  by unfold_locales

lemma continuous_on_tms: 
  assumes "x ∈ carrier"
  shows "continuous_on carrier (λy. tms x y)"
    and "continuous_on carrier (λy. tms y x)"
proof -
  have cts_tms: "continuous_on lie_prod.carrier (λ(a, b). tms a b)"
    using lie_group_axioms diff.continuous_on unfolding lie_group_def lie_group_axioms_def by blast
  have tms_is_comp: "(tms x) = (λ(a, b). tms a b) ∘ (λy. (x,y))"
    by (simp add: comp_def)
  show "continuous_on carrier (λy. tms x y)"
  proof -
    have cts_R: "continuous_on carrier (λy. (x,y))"
      using continuous_on_Pair[OF continuous_on_const[of carrier x] continuous_on_id] .
    have pair_carrier: "Pair x ` carrier ⊆ lie_prod.carrier"
      unfolding image_def using lie_prod.prod_carrier assms by blast
    thus ?thesis
      using continuous_on_compose[OF cts_R] cts_tms tms_is_comp continuous_on_subset[OF _ pair_carrier]
      by metis
  qed
  show "continuous_on carrier (λy. tms y x)"
  proof -
    have cts_L: "continuous_on carrier (λy. (y,x))"
      using continuous_on_Pair[OF continuous_on_id continuous_on_const[of carrier x]] .
    have pair_carrier': "(λy. (y,x)) ` carrier ⊆ lie_prod.carrier"
      unfolding image_def using lie_prod.prod_carrier assms by blast
    thus ?thesis
      using continuous_on_compose[OF cts_L] cts_tms tms_is_comp continuous_on_subset[OF _ pair_carrier']
      by force
  qed
qed

lemma diff_tms:
  assumes "x ∈ carrier"
  shows "diff ∞ charts charts (λy. tms x y)"
    and "diff ∞ charts charts (λy. tms y x)"
  subgoal
    using diff_compose[OF lie_prod.diff_left_Pair[OF assms] smooth_mult] diff.diff_cong by fastforce
  subgoal
    using diff_compose[OF lie_prod.diff_right_Pair[OF assms] smooth_mult] diff.diff_cong by fastforce
  done

lemma diff_tms_invs:
  assumes "x ∈ carrier"
  shows "diff ∞ charts charts (λy. tms (invs x) y)"
    and "diff ∞ charts charts (λy. tms y (invs x))"
  using diff_tms[of "invs x"] assms uminus_mem by blast+

lemma diff_tms_invs':
  assumes "x ∈ carrier"
  shows "diff ∞ charts charts (λy. tms x (invs y))"
    and "diff ∞ charts charts (λy. tms (invs y) x)"
  using diff_compose[OF smooth_inv diff_tms(1)[OF assms]] apply (simp add: diff.diff_cong)
  using diff_compose[OF smooth_inv diff_tms(2)[OF assms]] by (simp add: diff.diff_cong)

end


section ‹Morphisms of Lie groups, actions and representations›

subsection ‹Morphism of Lie groups.›
locale lie_group_pair =
  L1: lie_group c1 t1 i1 d1 m1 +
  L2: lie_group c2 t2 i2 d2 m2
  for c1 :: "('a::{second_countable_topology,t2_space}, 'b::euclidean_space) chart set"
    and c2 :: "('c::{second_countable_topology,t2_space}, 'd::euclidean_space) chart set"
    and t1 t2 and i1 i2 and d1 d2 and m1 m2


locale lie_group_morphism_with =
  lie_group_pair c1 c2 t1 t2 i1 i2 d1 d2 m1 m2 +
  diff ∞ c1 c2 f +
  group_hom_betw L1.carrier L2.carrier t1 t2 i1 i2 d1 d2 m1 m2 f
  for c1 :: "('a::{second_countable_topology,t2_space}, 'b::euclidean_space) chart set"
    and c2 :: "('c::{second_countable_topology,t2_space}, 'd::euclidean_space) chart set"
    and t1 t2 and i1 i2 and d1 d2 and m1 m2 and f

lemma (in lie_group_pair) lie_group_morphismI:
  assumes "diff ∞ c1 c2 f"
    and group_hom: "∀x∈L1.carrier. ∀y∈L1.carrier. f (t1 x y) = t2 (f x) (f y)"
    and closure: "∀x∈L1.carrier. f x ∈ L2.carrier"
  shows "lie_group_morphism_with c1 c2 t1 t2 i1 i2 d1 d2 m1 m2 f"
proof -
  have 1: "group_on_with_pair L1.carrier L2.carrier t1 t2 i1 i2 d1 d2 m1 m2"
    using lie_group_pair_axioms unfolding lie_group_pair_def lie_group_def group_on_with_pair_def by presburger
  show ?thesis
    unfolding lie_group_morphism_with_def group_hom_betw_def group_hom_betw_axioms_def
    by (simp add: assms lie_group_pair_axioms 1)
qed

lemma (in lie_group) lie_group_morphismI:
  assumes "lie_group c2 t2 i2 d2 m2"
    and "diff ∞ charts c2 f"
    and group_hom: "∀x∈carrier. ∀y∈carrier. f (tms x y) = t2 (f x) (f y)"
    and closure: "∀x∈carrier. f x ∈ (manifold.carrier c2)"
  shows "lie_group_morphism_with charts c2 tms t2 tms_one i2 dvsn d2 invs m2 f"
  by (auto intro: lie_group_pair.lie_group_morphismI simp: lie_group_pair_def lie_group_axioms assms)

locale lie_group_isomorphism =
  lie_group_pair c1 c2 t1 t2 i1 i2 d1 d2 m1 m2 +
  diffeomorphism ∞ c1 c2 f f' +
  group_hom_betw L1.carrier L2.carrier t1 t2 i1 i2 d1 d2 m1 m2 f
  for c1 :: "('a::{second_countable_topology,t2_space}, 'b::euclidean_space) chart set"
    and c2 :: "('c::{second_countable_topology,t2_space}, 'd::euclidean_space) chart set"
    and t1 t2 and i1 i2 and d1 d2 and m1 m2 and f f'



subsection ‹Action of a Lie group on a manifold.›

abbreviation (input) "diff_action_map g_charts m_charts action ≡
  diff ∞ (c_manifold_prod.prod_charts g_charts m_charts) m_charts action"

text ‹A Lie group action is a homomorphism from the Lie group to the automorphism group of a space,
 here a manifold, which is differentiable (smooth). I take here the more explicit definition given
 in Kirillov's lecture notes (2008; page 12), and derive the more abstract version later (after showing
 term‹c_manifold.Diff› is not just a group, but a Lie group).›
text ‹Take care: there are now two manifolds, of which the Lie group is the primary one as far
 as namespace is concerned. Everything pertaining to the manifold acted upon is accessed with
 qualified syntax. This disappears for Lie groups acting on themselves.›
locale lie_group_action =
  lie_group charts tms tms_one dvsn invs + M: c_manifold m_charts k
  for charts::"('a::{t2_space,second_countable_topology}, 'e::euclidean_space) chart set"
    and tms tms_one dvsn invs
    and m_charts::"('b::{t2_space,second_countable_topology}, 'f::euclidean_space) chart set" and k +
  fixes action (‹ρ›)
  assumes act_diff: "g ∈ carrier ==> (ρ g) ∈ M.Diff"
    and act_one: "ρ tms_one = M.Diff_id"
    and act_hom: "f∈G ==> g∈G ==> ρ (tms f g) = M.Diff_comp (ρ f) (ρ g)"
    and act_diff_prod: "diff_action_map charts m_charts (λ(g,m). the ((ρ g) m))"


text ‹After proving Diff is a group, some of these axioms can be replaced.›
locale lie_group_action' =
  lie_group charts tms tms_one dvsn invs +
  M: c_manifold m_charts k +
  A: group_hom_betw carrier M.Diff tms M.Diff_comp tms_one M.Diff_id dvsn M.Diff_comp_inv invs M.Diff_inv ρ
  for charts::"('a::{t2_space,second_countable_topology}, 'e::euclidean_space) chart set"
    and tms tms_one dvsn invs
    and m_charts::"('b::{t2_space,second_countable_topology}, 'f::euclidean_space) chart set" and k
    and ρ :: "'a ==> ('b⇀'b)" +
  assumes diff_action_map: "diff_action_map charts m_charts (λ(g,m). the ((ρ g) m))"


subsection ‹Action of a Lie Group on itself.›
context lie_group begin

abbreviation (input) left_self_action :: "'a==>'a==>'a" (‹L _› [91])
  where "left_self_action g g' ≡ tms g g'"

abbreviation left_action :: "'a==>('a⇀'a)"
  where "left_action g ≡ (λx. if x∈carrier then Some (left_self_action g x) else None)"

abbreviation (input) right_self_action :: "'a==>'a==>'a" (‹R _› [91])
  where "right_self_action g g' ≡ tms g' (invs g)"

abbreviation right_action :: "'a==>('a⇀'a)"
  where "right_action g ≡ (λx. if x∈carrier then Some (right_self_action g x) else None)"

abbreviation (input) adjoint_self_action :: "'a==>'a==>'a" (*(\<open>Ad _ _\<close> [53,53])*)
  where "adjoint_self_action g g' ≡ tms g (tms g' (invs g))"



subsubsection ‹The left action.›

lemma L_action_in: "(left_self_action g g') ∈ carrier" if "g ∈ carrier" "g' ∈ carrier"
  by (simp add: add_mem that)

lemma the_left_action: "left_self_action x y = the (left_action x y)" if "y ∈ carrier"
  by (simp add: that)

lemma L_action_invs: "(left_self_action (invs x) ∘ left_self_action x) y = y"
    "(left_self_action x ∘ left_self_action (invs x)) y = y"
  if "x ∈ carrier" "y ∈ carrier"
  apply (metis (no_types, lifting) add_assoc add_zeroL comp_apply left_minus that uminus_mem)
  by (metis (no_types, lifting) add_assoc add_zeroL comp_apply right_minus that uminus_mem)

lemma L_homeomorphism: "homeomorphism carrier carrier (L x) (L (invs x))" if "x ∈ carrier"
proof -
  {
    fix x y assume xy_in_carrier: "x ∈ carrier" "y ∈ carrier"
    then have "tms (invs x) (tms x y) = y" and "tms x (tms (invs x) y) = y"
      using add_assoc add_zeroL uminus_mem by (metis left_minus, metis right_minus)
  }
  thus "homeomorphism carrier carrier (tms x) (tms (invs x))"
    using that continuous_on_tms(1) by (auto intro: homeomorphismI simp: L_action_in image_subset_iff uminus_mem)
qed

lemma L_homeomorphism': "homeomorphism carrier carrier (L (invs x)) (L x)"
  if "x ∈ carrier"
  using L_homeomorphism homeomorphism_sym that by blast

lemma L_homeomorphism_chart: "homeomorphism (domain c) (L x ` domain c) (L x) (L (invs x))"
  if "x ∈ carrier" "c ∈ atlas" 
  using L_homeomorphism homeomorphism_of_subsets that by blast

lemma L_homeomorphism_chart': "homeomorphism (L x ` domain c) (domain c) (L (invs x)) (L x)"
  if "x ∈ carrier" "c ∈ atlas"
  using L_homeomorphism_chart that homeomorphism_sym by blast

lemma L_open_map:
  assumes "x ∈ carrier" "open S" "S ⊆ carrier"
  shows "open (L x ` S)"
proof -
  obtain C where C: "∀c∈C. c∈atlas" "S = ∪{domain c | c. c∈C}"
    using open_covered_by_charts assms by blast
  have "L x ` S = ∪{L x ` domain c | c. c∈C}"
    using C(2) by auto
  thus "open (L x ` S)"
    using homeomorphism_imp_open_map' L_homeomorphism by (metis assms open_carrier)
qed

lift_definition L_chart :: "'a ==> ('a,'e) chart ==> ('a,'e) chart"
  is "λx. λ(d,d',f,f'). if x∈carrier ∧ d⊆carrier then (L x ` d, d', f ∘ L (invs x), L x ∘ f') else ({}, {}, f, f')"
  using L_homeomorphism by (auto split: if_splits intro!: L_open_map)
    (meson homeomorphism_compose homeomorphism_of_subsets homeomorphism_symD)

lemma L_chart_apply_chart[simp]: "apply_chart (L_chart x c) = apply_chart c ∘ L (invs x)"
  and L_chart_inv_chart[simp]: "inv_chart (L_chart x c) = L x ∘ inv_chart c"
  and domain_L_chart[simp]: "domain (L_chart x c) = L x ` domain c"
  and codomain_L_chart[simp]: "codomain (L_chart x c) = codomain c"
  if "x∈carrier" "c∈atlas"
  using that(1) domain_atlas_subset_carrier[OF that(2)] by (transfer, auto)+

lemma L_chart_apply_chart'[simp]: "apply_chart (L_chart x c) = apply_chart c ∘ L (invs x)"
  and L_chart_inv_chart'[simp]: "inv_chart (L_chart x c) = L x ∘ inv_chart c"
  and domain_L_chart'[simp]: "domain (L_chart x c) = L x ` domain c"
  and codomain_L_chart'[simp]: "codomain (L_chart x c) = codomain c"
  if "x∈carrier" "domain c ⊆ carrier"
  using that by (transfer, auto)+

lemma smooth_compat_L_chart:
  assumes "x ∈ carrier" "c ∈ atlas" "c' ∈ atlas"
  shows "∞-smooth_compat (L_chart x c) c'"
proof -
  let ?dom1 = "(λy. c (tms (invs x) y)) ` (tms x ` domain c ∩ domain c')"
  let ?dom2 = "codomain c ∩ inv_chart c -` (carrier ∩ tms x -` domain c')"
  let ?dom3 = "c' ` (tms x ` domain c ∩ domain c')"
  let ?dom4 = "codomain c' ∩ inv_chart c' -` (carrier ∩ tms (invs x) -` domain c)"

  have invs_tms_defined: "c (tms (invs x) (tms x y)) ∈ codomain c" if "y ∈ domain c" for y
    by (metis add_assoc add_uminus add_zeroL assms(1,2) chart_in_codomain in_carrier_atlasI uminus_mem that)
  have domain_simp_1: "?dom1 = ?dom2"
  proof -
    {
      fix y assume y: "tms x y ∈ domain c'" "y ∈ domain c"
      have "inv_chart c (c (tms (invs x) (tms x y))) ∈ carrier"
        and "tms x (inv_chart c (c (tms (invs x) (tms x y)))) ∈ domain c'"
        subgoal using y assms(2) invs_tms_defined by blast
        subgoal using y by (metis add_assoc add_zeroL assms(1,2) in_carrier_atlasI inv_chart_inverse left_minus uminus_mem)
        done
    } moreover {
      fix y assume y: "y ∈ codomain c" "inv_chart c y ∈ carrier" "tms x (inv_chart c y) ∈ domain c'"
      have "y = c (tms (invs x) (tms x (inv_chart c y)))"
        by (metis (full_types) assms(1) chart_inverse_inv_chart homeomorphism_apply1 L_homeomorphism y(1,2))
      then have "y ∈ (λy. c (tms (invs x) y)) ` (tms x ` domain c ∩ domain c')"
        using y(1,3) by blast
    }
    ultimately show "?dom1 = ?dom2" using invs_tms_defined by auto
  qed
  have domain_simp_2: "?dom3 = ?dom4"
  proof -
    {
      fix y assume y: "tms x y ∈ domain c'" "y ∈ domain c"
      have "tms x y ∈ carrier" and "tms (invs x) (tms x y) ∈ domain c"
        subgoal using y assms(3) by simp
        subgoal using y by (metis add_assoc add_zeroL assms(1,2) in_carrier_atlasI local.left_minus uminus_mem)
        done
    } moreover {
      fix y assume "y ∈ codomain c'" "inv_chart c' y ∈ carrier" "tms (invs x) (inv_chart c' y) ∈ domain c"
      then have "y ∈ c' ` (tms x ` domain c ∩ domain c')"
        by (smt (verit, ccfv_threshold) Int_iff add_assoc add_uminus add_zeroL assms(1)
            chart_inverse_inv_chart inv_chart_in_domain rev_image_eqI uminus_mem)
    }
    ultimately show "?dom3 = ?dom4" by auto
  qed

  have "smooth_on ?dom1 (c' ∘ (tms x ∘ inv_chart c))"
    using diff.diff_chartsD[OF diff_tms(1)[OF assms(1)] assms(2,3)]
    by (simp add: comp_assoc domain_simp_1)
  moreover have "smooth_on ?dom3 (c ∘ tms (invs x) ∘ inv_chart c')"
    using diff.diff_chartsD[OF diff_tms_invs(1)[OF assms(1)] assms(3,2)] by (simp add: domain_simp_2)
  ultimately show ?thesis
    by (unfold smooth_compat_def, auto simp: assms)
qed

lemma L_chart_compat:
  assumes "x ∈ carrier" "c ∈ atlas"
  shows "∞-smooth_compat c (L_chart x c)"
  using smooth_compat_L_chart[OF assms(1,2,2)] by (simp add: smooth_compat_commute)

lemma L_chart_in_atlas: "L_chart x c ∈ atlas" if "x ∈ carrier" "c ∈ atlas"
proof (rule maximal_atlas)
  show "domain (L_chart x c) ⊆ carrier" using L_action_in that by auto
  fix c' assume "c' ∈ atlas"
  with that(2) have "∞-smooth_compat c c'" by (simp add: atlas_is_atlas)
  thus "∞-smooth_compat (L_chart x c) c'"
    using smooth_compat_L_chart[OF that] by (simp add: ‹c' ∈ atlas›)
qed

lemma left_action_automorphic: "c_automorphism ∞ charts (L x) (L (invs x))"
  if "x ∈ carrier"
proof (unfold_locales)
  fix y assume "y ∈ carrier"
  then obtain c1 where c1: "c1 ∈ atlas" "y ∈ domain c1" using atlasE by blast
  let ?L = "left_self_action x"
  let ?L_i = "left_self_action (invs x)"

  text ‹To find the second chart, for the codomain of term‹L x›, just shift the first chart across.›
  show "∃c1∈atlas. ∃c2∈atlas.
    y ∈ domain c1 ∧
    ?L ` domain c1 ⊆ domain c2 ∧
    smooth_on (codomain c1) (c2 ∘ ?L ∘ inv_chart c1)"
  proof (intro bexI conjI)
    let ?c2 = "L_chart x c1"

    show "y ∈ domain c1" by (simp add: c1(2))
    show "c1 ∈ atlas" "?c2 ∈ atlas" by (simp add: L_chart_in_atlas c1(1) that)+
    show "tms x ` domain c1 ⊆ domain ?c2" by (simp add: c1(1) that)
    
    have "(c1 ∘ ?L_i ∘ ?L ∘ inv_chart c1) a = a" if "a ∈ codomain c1" for a
      using L_action_invs(1) ‹x ∈ carrier› c1(1) that by force
    thus "smooth_on (codomain c1) (?c2 ∘ ?L ∘ inv_chart c1)"
      using smooth_on_id smooth_on_cong
      by (smt (verit, del_insts) L_chart_apply_chart c1(1) open_codomain that)
  qed

  show "∃c1∈atlas. ∃c2∈atlas.
    y ∈ domain c1 ∧
    ?L_i ` domain c1 ⊆ domain c2 ∧
    smooth_on (codomain c1) (c2 ∘ ?L_i ∘ inv_chart c1)"
  proof (intro bexI conjI)
    let ?c2 = "L_chart (invs x) c1"

    have [simp]: "invs x ∈ carrier" by (simp add: that uminus_mem)

    show "y ∈ domain c1" by (simp add: c1(2))
    show "c1 ∈ atlas" "?c2 ∈ atlas" by (simp add: L_chart_in_atlas c1(1) that)+
    show "tms (invs x) ` domain c1 ⊆ domain ?c2" by (simp add: c1(1) that)

    have 1: "(c1 ∘ ?L ∘ ?L_i ∘ inv_chart c1) a = a"
      if "a ∈ codomain c1" for a
      using L_action_invs(2) ‹x ∈ carrier› c1 that by force
    show "smooth_on (codomain c1) (?c2 ∘ ?L_i ∘ inv_chart c1)"
      apply (simp add: c1 uminus_uminus[OF that])
      using smooth_on_id 1 by (smt (verit, del_insts) open_codomain smooth_on_cong)
  qed

  { fix y assume "y ∈ carrier"
    show "tms (invs x) (tms x y) = y"
      by (metis ‹y ∈ carrier› add_assoc add_zeroL left_minus that uminus_mem)
    show "tms x (tms (invs x) y) = y"
      by (metis ‹y ∈ carrier› add_assoc add_zeroL right_minus that uminus_mem) }
qed

lemma left_action_in_Diff: "left_action x ∈ Diff" if "x ∈ carrier"
  apply (intro DiffI automorphismI exI[where x="left_self_action (invs x)"])
    subgoal using c_automorphism.c_automorphism_cong left_action_automorphic that by fastforce
    subgoal by (simp add: domIff order_class.order_eq_iff subset_iff)
  done

lemma diff_the_L: "diff ∞ (c_manifold_prod.prod_charts charts charts) charts (λ(g, m). the (left_action g m))"
  (is "diff ∞ ?prod_charts charts ?L")
proof -
  let ?prod_carrier = "manifold.carrier ?prod_charts"
  have L_eq: "?L (g,m) = (L g) m" if "(g,m) ∈ ?prod_carrier" for g m
    using c_manifold_prod.prod_carrier[OF lie_prod] that by fastforce
  show ?thesis
    apply (rule diff.diff_cong[OF smooth_mult])
    using L_eq by fastforce
qed

lemma left_action: "lie_group_action' charts tms tms_one dvsn invs charts ∞ left_action"
  unfolding lie_group_action'_def lie_group_action'_axioms_def
  apply (simp add: lie_group_axioms c_manifold_axioms, intro conjI)
    subgoal using add_assoc add_mem left_action_in_Diff by (unfold_locales, auto)
    subgoal by (rule diff_the_L)
  done

sublocale left_action: lie_group_action' charts tms tms_one dvsn invs charts ∞ left_action
  by (rule left_action)



subsubsection ‹The right action.›

lemma R_action_in: "(right_self_action g g') ∈ carrier" if "g ∈ carrier" "g' ∈ carrier"
  by (simp add: add_mem that uminus_mem)

lemma the_right_action: "right_self_action x y = the (right_action x y)" if "y ∈ carrier"
  by (simp add: that)

lemma R_action_invs: "(right_self_action (invs x) ∘ right_self_action x) y = y"
    "(right_self_action x ∘ right_self_action (invs x)) y = y"
  if "x ∈ carrier" "y ∈ carrier"
  using add_assoc add_zeroR comp_apply right_minus left_minus that uminus_mem by simp_all

lemma R_homeomorphism: "homeomorphism carrier carrier (R x) (R (invs x))"
  if "x ∈ carrier"
proof -
  {
    fix x y assume xy_in_carrier: "x ∈ carrier" "y ∈ carrier"
    then have "tms (tms y (invs x)) (invs (invs x)) = y" and "tms (tms y (invs (invs x))) (invs x) = y"
      using add_assoc add_zeroR uminus_mem by (metis right_minus, metis left_minus)
  }
  thus "homeomorphism carrier carrier (R x) (R (invs x))"
    using that continuous_on_tms(2) by (auto intro!: homeomorphismI simp: R_action_in image_subset_iff uminus_mem)
qed

lemma R_homeomorphism': "homeomorphism carrier carrier (R (invs x)) (R x)"
  if "x ∈ carrier"
  using R_homeomorphism homeomorphism_sym that by blast

lemma R_homeomorphism_chart: "homeomorphism (domain c) (R x ` domain c) (R x) (R (invs x))"
  if "x ∈ carrier" "c ∈ atlas"
  using R_homeomorphism homeomorphism_of_subsets that by blast

lemma R_homeomorphism_chart': "homeomorphism (R x ` domain c) (domain c) (R (invs x)) (R x)"
  if "x ∈ carrier" "c ∈ atlas"
  using R_homeomorphism_chart that homeomorphism_sym by blast

lemma R_open_map:
  assumes "x ∈ carrier" "open S" "S ⊆ carrier"
  shows "open (R x ` S)"
proof -
  obtain C where C: "∀c∈C. c∈atlas" "S = ∪{domain c | c. c∈C}"
    using open_covered_by_charts assms by blast
  have "R x ` S = ∪{R x ` domain c | c. c∈C}"
    using C(2) by auto
  thus "open (R x ` S)"
    using homeomorphism_imp_open_map' R_homeomorphism assms open_carrier by fast
qed

lift_definition R_chart :: "'a ==> ('a,'e) chart ==> ('a,'e) chart"
  is "λx. λ(d,d',f,f'). if x∈carrier ∧ d⊆carrier then (R x ` d, d', f ∘ R (invs x), R x ∘ f') else ({}, {}, f, f')"
  using R_homeomorphism by (auto split: if_splits intro!: R_open_map)
    (meson homeomorphism_compose homeomorphism_of_subsets homeomorphism_symD)

lemma R_chart_apply_chart[simp]: "apply_chart (R_chart x c) = apply_chart c ∘ R (invs x)"
  and R_chart_inv_chart[simp]: "inv_chart (R_chart x c) = R x ∘ inv_chart c"
  and domain_R_chart[simp]: "domain (R_chart x c) = R x ` domain c"
  and codomain_R_chart[simp]: "codomain (R_chart x c) = codomain c"
  if "x∈carrier" "c∈atlas"
  using that(1) domain_atlas_subset_carrier[OF that(2)] by (transfer, auto)+

lemma R_chart_apply_chart'[simp]: "apply_chart (R_chart x c) = apply_chart c ∘ R (invs x)"
  and R_chart_inv_chart'[simp]: "inv_chart (R_chart x c) = R x ∘ inv_chart c"
  and domain_R_chart'[simp]: "domain (R_chart x c) = R x ` domain c"
  and codomain_R_chart'[simp]: "codomain (R_chart x c) = codomain c"
  if "x∈carrier" "domain c ⊆ carrier"
  using that by (transfer, auto)+

lemma smooth_compat_R_chart:
  assumes "x ∈ carrier" "c ∈ atlas" "c' ∈ atlas"
  shows "∞-smooth_compat (R_chart x c) c'"
proof -
  let ?dom1 = "(λy. c (tms y (invs (invs x)))) ` ((λg'. tms g' (invs x)) ` domain c ∩ domain c')"
  let ?dom2 = "codomain c ∩ inv_chart c -` (carrier ∩ (λy. tms y (invs x)) -` domain c')"
  let ?dom3 = "c' ` ((λy. tms y (invs x)) ` domain c ∩ domain c')"
  let ?dom4 = "codomain c' ∩ inv_chart c' -` (carrier ∩ (λy. tms y x) -` domain c)"

  have invs_tms_defined: "c (tms (tms y (invs x)) (invs (invs x))) ∈ codomain c" if "y ∈ domain c" for y
    using add_assoc add_zeroR assms(1,2) local.right_minus that uminus_mem by auto
  then have domain_simp_1: "?dom1 = ?dom2"
  proof -
    {
      fix y assume y: "tms y (invs x) ∈ domain c'" "y ∈ domain c"
      have "inv_chart c (c (tms (tms y (invs x)) (invs (invs x)))) ∈ carrier"
        and "tms (inv_chart c (c (tms (tms y (invs x)) (invs (invs x))))) (invs x) ∈ domain c'"
        subgoal using y invs_tms_defined assms(2) by blast
        subgoal using y add_assoc add_zeroR assms(1,2) in_carrier_atlasI inv_chart_inverse right_minus uminus_mem by metis
        done
    } moreover {
      fix y assume "y ∈ codomain c" "inv_chart c y ∈ carrier" "tms (inv_chart c y) (invs x) ∈ domain c'"
      then have "y ∈ (λy. apply_chart c (tms y (invs (invs x)))) ` ((λg'. tms g' (invs x)) ` domain c ∩ domain c')"
        by (smt (verit, ccfv_threshold) IntI R_action_invs(1) assms(1) chart_inverse_inv_chart
          comp_apply imageI inv_chart_in_domain)
    }
    ultimately show "?dom1 = ?dom2" using invs_tms_defined by auto
  qed
  have domain_simp_2: "?dom3 = ?dom4"
  proof -
    {
      fix y assume y: "tms y (invs x) ∈ domain c'" "y ∈ domain c"
      have "tms y (invs x) ∈ carrier" and "tms (tms y (invs x)) x ∈ domain c"
        subgoal using y assms(3) by simp
        subgoal using y by (metis add_assoc add_zeroR assms(1,2) in_carrier_atlasI left_minus uminus_mem)
        done
    } moreover {
      fix xa assume xa: "xa ∈ codomain c'" "inv_chart c' xa ∈ carrier" "tms (inv_chart c' xa) x ∈ domain c"
      then have "xa ∈ apply_chart c' ` ((λy. tms y (invs x)) ` domain c ∩ domain c')"
        by (smt (verit, ccfv_threshold) Int_iff add_assoc add_zero assms(1) chart_inverse_inv_chart
          inv_chart_in_domain right_minus rev_image_eqI uminus_mem)
    }
    ultimately show "?dom3 = ?dom4" by auto
  qed

  have "smooth_on ?dom1 (c' ∘ ((λg'. tms g' (invs x)) ∘ inv_chart c))"
    using diff.diff_chartsD[OF diff_tms_invs(2)[OF assms(1)] assms(2,3)]
    by (simp add: comp_assoc domain_simp_1)
  moreover have "smooth_on ?dom3 ( c ∘ (λg'. tms g' (invs (invs x))) ∘ inv_chart c')"
    using diff.diff_chartsD[OF diff_tms(2)] uminus_uminus assms by (simp add: domain_simp_2)
  ultimately show ?thesis
    by (unfold smooth_compat_def, auto simp: assms)
qed

lemma R_chart_compat:
  assumes "x ∈ carrier" "c ∈ atlas"
  shows "∞-smooth_compat c (R_chart x c)"
  using smooth_compat_R_chart[OF assms(1,2,2)] by (simp add: smooth_compat_commute)

lemma R_chart_in_atlas: "R_chart x c ∈ atlas" if "x ∈ carrier" "c ∈ atlas"
proof (rule maximal_atlas)
  show "domain (R_chart x c) ⊆ carrier" using R_action_in that by auto
  fix c' assume "c' ∈ atlas"
  with that(2) have "∞-smooth_compat c c'" by (simp add: atlas_is_atlas)
  thus "∞-smooth_compat (R_chart x c) c'"
    using smooth_compat_R_chart[OF that] by (simp add: ‹c' ∈ atlas›)
qed

lemma right_action_automorphic: "c_automorphism ∞ charts (R x) (R (invs x))"
  if "x ∈ carrier"
proof (unfold_locales)
  fix y assume "y ∈ carrier"
  then obtain c1 where c1: "c1 ∈ atlas" "y ∈ domain c1" using atlasE by blast
  let ?R = "right_self_action x"
  let ?R_i = "right_self_action (invs x)"

  text ‹To find the second chart, for the codomain of term‹R x›, just shift the first chart across.›
  show "∃c1∈atlas. ∃c2∈atlas.
    y ∈ domain c1 ∧
    ?R ` domain c1 ⊆ domain c2 ∧
    smooth_on (codomain c1) (c2 ∘ ?R ∘ inv_chart c1)"
  proof (intro bexI conjI)
    let ?c2 = "R_chart x c1"

    show "y ∈ domain c1" by (simp add: c1(2))
    show "c1 ∈ atlas" "?c2 ∈ atlas" by (simp add: R_chart_in_atlas c1(1) that)+
    show "(λy. tms y (invs x)) ` domain c1 ⊆ domain ?c2" by (simp add: c1(1) that)
    
    have cong_to_id: "(c1 ∘ ?R_i ∘ ?R ∘ inv_chart c1) a = a" if "a ∈ codomain c1" for a
      using R_action_invs(1) ‹x ∈ carrier› c1(1) that by force
    show "smooth_on (codomain c1) (?c2 ∘ ?R ∘ inv_chart c1)"
      using smooth_on_id smooth_on_cong cong_to_id
      by (smt (verit, ccfv_threshold) R_chart_apply_chart c1(1) comp_apply open_codomain that uminus_uminus)
  qed

  show "∃c1∈atlas. ∃c2∈atlas.
    y ∈ domain c1 ∧
    ?R_i ` domain c1 ⊆ domain c2 ∧
    smooth_on (codomain c1) (c2 ∘ ?R_i ∘ inv_chart c1)"
  proof (intro bexI conjI)
    let ?c2 = "R_chart (invs x) c1"

    have [simp]: "invs x ∈ carrier" by (simp add: that uminus_mem)

    show "y ∈ domain c1" by (simp add: c1(2))
    show "c1 ∈ atlas" "?c2 ∈ atlas" by (simp add: R_chart_in_atlas c1(1) that)+
    show "(λg'. tms g' (invs (invs x))) ` domain c1 ⊆ domain ?c2" by (simp add: c1(1) that)

    have 1: "(c1 ∘ ?R ∘ ?R_i ∘ inv_chart c1) a = a"
      if "a ∈ codomain c1" for a
      using R_action_invs(2) ‹x ∈ carrier› c1 that by force
    show "smooth_on (codomain c1) (?c2 ∘ ?R_i ∘ inv_chart c1)"
      apply (rule smooth_on_cong)
      using 1 by (auto simp add: c1 uminus_uminus[OF that])
  qed

  { fix y assume "y ∈ carrier"
    show "tms (tms y (invs x)) (invs (invs x)) = y"
      by (metis ‹y ∈ carrier› add_assoc add_zeroR right_minus that uminus_mem)
    show "tms (tms y (invs (invs x))) (invs x) = y"
      by (metis ‹y ∈ carrier› add_assoc add_zeroR left_minus that uminus_mem) }
qed

lemma right_action_in_Diff: "right_action x ∈ Diff" if "x ∈ carrier"
  apply (intro DiffI automorphismI exI[where x="right_self_action (invs x)"])
    subgoal using c_automorphism.c_automorphism_cong right_action_automorphic that by fastforce
    subgoal by (simp add: domIff order_class.order_eq_iff subset_iff)
  done

end


section ‹Models/Instances›

subsection ‹Euclidean Space›
text ‹Euclidean spaces are dealt with at the start of the section ``Differentiable Functions'' in
 🍋‹Smooth_Manifolds.Differentiable_Manifold›.
 Therefore, this section is really just a ``trivial'' exercise to get used to things.›

subsubsection ‹Euclidean Spaces are Lie groups under term‹(+)›.›
locale euclidean_lie_group_add
begin

abbreviation C
  where "C ≡ manifold_eucl.carrier"

abbreviation C_prod
  where "C_prod ≡ manifold.carrier prod_charts_eucl"

lemma eucl_is_group: "group_on_with C (+) 0 (-) uminus"
proof (unfold group_on_with_def, intro conjI)
  show "monoid_on_with C (+) 0"
    unfolding monoid_on_with_def semigroup_add_on_with_def
    using manifold_eucl_carrier
    by (simp add: monoid_on_with_axioms.intro)
  show "group_on_with_axioms C (+) 0 (-) uminus"
    unfolding group_on_with_axioms_def
    using manifold_eucl_carrier UNIV_I ab_group_add_class.ab_diff_conv_add_uminus add.left_inverse
    by auto
qed

lemma prod_domain_codomain: "domain prod_chart_eucl = C×C" "C×C = C_prod" "codomain prod_chart_eucl = C×C"
  using c_manifold_prod.domain_prod_chart [OF eucl_makes_product_manifold]
  apply fastforce
  using c_manifold_prod.prod_carrier eucl_makes_product_manifold
  apply metis
  using c_manifold_prod.codomain_prod_chart [OF eucl_makes_product_manifold]
  by fastforce

lemma smooth_on_add_const: "smooth_on C (λa. a+b)"
proof -
  have sm_id: "smooth_on C (λa. a)"
    by (simp add: smooth_on_id)
  have sm_add: "smooth_on C (λa. b)"
    by (simp add: smooth_on_const)
  show "smooth_on C (λa. a+b)"
    using smooth_on_add [OF sm_id sm_add manifold.open_carrier]
    by simp
qed
                    
lemma smooth_binop_diff:
  fixes tms::"'a==>'a==>'a::euclidean_space"
  assumes "smooth_on C_prod (λ(a,b). tms a b)"
  shows "diff ∞ prod_charts_eucl charts_eucl (λ(x, y). tms x y)"
proof (unfold diff_def diff_axioms_def, intro conjI allI impI)
  let ?prod = "prod_charts_eucl"
  let ?mult = "λ(x, y). tms x y"
  let ?c1 = "prod_chart_eucl"
  let ?c2 = "chart_eucl"
  let ?atl = "manifold_eucl.atlas ∞"
  let ?prod_atl = "c_manifold.atlas prod_charts_eucl ∞"
  fix p::"'a×'a"
  assume "p∈manifold.carrier ?prod"
  show "∃c1∈c_manifold.atlas prod_charts_eucl ∞. ∃c2∈manifold_eucl.atlas ∞.
    p ∈ domain c1 ∧
    (λ(x, y). tms x y) ` domain c1 ⊆ domain c2 ∧
    smooth_on (codomain c1) (apply_chart c2 ∘ (λ(x, y). tms x y) ∘ inv_chart c1)"
  proof (intro bexI, intro conjI)
    show "?c1 ∈ ?prod_atl"
      by (rule c_manifold.in_charts_in_atlas [
        OF c_manifold_prod.c_manifold_atlas_product [
          OF eucl_makes_product_manifold
        ] prod_chart_in_prod_charts
      ])
    show "?c2 ∈ ?atl"
      using c_manifold.in_charts_in_atlas by simp
    show "p ∈ domain ?c1"
      by (simp add: prod_domain_codomain)
    show "(λ(x, y). tms x y) ` domain ?c1 ⊆ domain ?c2"
      by simp
    show "smooth_on (codomain ?c1) (apply_chart ?c2 ∘ (λ(x, y). tms x y) ∘ inv_chart ?c1)"
      using map_fun_eucl_prod_id_f prod_domain_codomain assms
      by metis
  qed
qed (simp add: c_manifold_prod.c_manifold_atlas_product c_manifolds.intro
      eucl_makes_product_manifold manifold_eucl.c_manifold_axioms)

lemma smooth_unop_diff:
  fixes invs::"'a==>'a::euclidean_space"
  assumes "smooth_on C invs"
  shows "diff ∞ charts_eucl charts_eucl invs"
proof (unfold diff_def diff_axioms_def, intro conjI allI impI)
  let ?c1 = "prod_chart_eucl"
  let ?c2 = "chart_eucl"
  let ?atl = "manifold_eucl.atlas ∞"
  fix x::'a
  assume "x ∈ manifold_eucl.carrier"
  show "∃c1∈manifold_eucl.atlas ∞. ∃c2∈manifold_eucl.atlas ∞.
    x ∈ domain c1 ∧
    invs ` domain c1 ⊆ domain c2 ∧
    smooth_on (codomain c1) (apply_chart c2 ∘ invs ∘ inv_chart c1)"
  proof (intro bexI conjI)
    show "invs ` domain chart_eucl ⊆ domain ?c2"
      by (simp add: image_subsetI)
    have "manifold_eucl.carrier = codomain chart_eucl"
      by simp
    thus "smooth_on (codomain chart_eucl) (apply_chart chart_eucl ∘ invs ∘ inv_chart chart_eucl)"
      using assms map_fun_eucl_id_f
      by metis
  qed (simp+)
qed (simp add: manifold_eucl.self.c_manifolds_axioms)

lemma eucl_smooth_group_imp_lie_group:
  assumes is_group: "group_on_with C tms tms_1 dvsn invs"
    and smooth_mult: "smooth_on C_prod (λ(a,b). tms a b)"
    and smooth_inv: "smooth_on C invs"
  shows "lie_group charts_eucl tms tms_1 dvsn invs"
proof (unfold lie_group_def lie_group_axioms_def, (intro conjI))
  show "c_manifold charts_eucl ∞"
    using c_manifold_def by (simp add: c1_manifold_atlas_eucl)
  show "group_on_with manifold_eucl.carrier tms tms_1 dvsn invs"
    using is_group by simp
  show "diff ∞ prod_charts_eucl charts_eucl (λ(a, b). tms a b)"
    using smooth_binop_diff smooth_mult by auto
  show "diff ∞ charts_eucl charts_eucl invs"
    using smooth_unop_diff smooth_inv by simp
qed


text ‹Any Euclidean space is a Lie group under addition.›
theorem lie_group_eucl: "lie_group charts_eucl (+) 0 (-) uminus"
  by (rule eucl_smooth_group_imp_lie_group [OF eucl_is_group eucl_add_smooth eucl_um_smooth])

interpretation lie_group_eucl: lie_group charts_eucl "(+)" 0 "(-)" uminus
  using lie_group_eucl .

end



subsection ‹The real numbers as a Lie group›

lift_definition chart_real::"(real, real) chart" is
  "(UNIV, UNIV, λx. x, λx. x)"
  by (auto simp: homeomorphism_def)

abbreviation "charts_real ≡ {chart_real}"

lemma chart_real_is_eucl: "charts_eucl = charts_real" "chart_eucl = chart_real"
  by (transfer, simp)+

theorem lie_group_real: "lie_group charts_real (+) 0 (-) uminus"
  using euclidean_lie_group_add.lie_group_eucl chart_real_is_eucl by metis


end