Theory Chart

section ‹Charts›
theory Chart
  imports Analysis_More
begin

subsection ‹Definition›

text ‹A chart on ‹M› is a homeomorphism from an open subset of ‹M› to an open subset
  of some Euclidean space ‹E›. Here ‹d› and ‹d'› are open subsets of ‹M› and ‹E›, respectively,
  ‹f: d → d'› is the mapping, and ‹f': d' → d› is the inverse mapping.›
typedef (overloaded) ('a::topological_space, 'e::euclidean_space) chart =
  "{(d::'a set, d'::'e set, f, f').
    open d ∧ open d' ∧ homeomorphism d d' f f'}"
  by (rule exI[where x="({}, {}, (λx. undefined), (λx. undefined))"]) simp

setup_lifting type_definition_chart

lift_definition apply_chart::"('a::topological_space, 'e::euclidean_space) chart ⇒ 'a ⇒ 'e"
  is "λ(d, d', f, f'). f" .

declare [[coercion apply_chart]]

lift_definition inv_chart::"('a::topological_space, 'e::euclidean_space) chart ⇒ 'e ⇒ 'a"
  is "λ(d, d', f, f'). f'" .

lift_definition domain::"('a::topological_space, 'e::euclidean_space) chart ⇒ 'a set"
  is "λ(d, d', f, f'). d" .

lift_definition codomain::"('a::topological_space, 'e::euclidean_space) chart ⇒ 'e set"
  is "λ(d, d', f, f'). d'" .


subsection ‹Properties›

lemma open_domain[intro, simp]: "open (domain c)"
  and open_codomain[intro, simp]: "open (codomain c)"
  and chart_homeomorphism: "homeomorphism (domain c) (codomain c) c (inv_chart c)"
  by (transfer, auto)+

lemma at_within_domain: "at x within domain c = at x" if "x ∈ domain c"
  by (rule at_within_open[OF that open_domain])

lemma at_within_codomain: "at x within codomain c = at x" if "x ∈ codomain c"
  by (rule at_within_open[OF that open_codomain])

lemma
  chart_in_codomain[intro, simp]: "x ∈ domain c ⟹ c x ∈ codomain c"
  and inv_chart_inverse[simp]: "x ∈ domain c ⟹ inv_chart c (c x) = x"
  and inv_chart_in_domain[intro, simp]:"y ∈ codomain c ⟹ inv_chart c y ∈ domain c"
  and chart_inverse_inv_chart[simp]: "y ∈ codomain c ⟹ c (inv_chart c y) = y"
  and image_domain_eq: "c ` (domain c) = codomain c"
  and inv_image_codomain_eq[simp]: "inv_chart c ` (codomain c) = domain c"
  and continuous_on_domain: "continuous_on (domain c) c"
  and continuous_on_codomain: "continuous_on (codomain c) (inv_chart c)"
  using chart_homeomorphism[of c]
  by (auto simp: homeomorphism_def)

lemma chart_eqI: "c = d"
  if "domain c = domain d"
    "codomain c = codomain d"
    "⋀x. c x = d x"
    "⋀x. inv_chart c x = inv_chart  d x"
  using that
  by transfer auto

lemmas continuous_on_chart[continuous_intros] =
  continuous_on_compose2[OF continuous_on_domain]
  continuous_on_compose2[OF continuous_on_codomain]

lemma continuous_apply_chart: "continuous (at x within X) c" if "x ∈ domain c"
  apply (rule continuous_at_imp_continuous_within)
  using continuous_on_domain[of c] that at_within_domain[OF that]
  by (auto simp: continuous_on_eq_continuous_within)

lemma continuous_inv_chart: "continuous (at x within X) (inv_chart c)" if "x ∈ codomain c"
  apply (rule continuous_at_imp_continuous_within)
  using continuous_on_codomain[of c] that at_within_codomain[OF that]
  by (auto simp: continuous_on_eq_continuous_within)

lemmas apply_chart_tendsto[tendsto_intros] = isCont_tendsto_compose[OF continuous_apply_chart, rotated]
lemmas inv_chart_tendsto[tendsto_intros] = isCont_tendsto_compose[OF continuous_inv_chart, rotated]

lemma continuous_within_compose2':
  "continuous (at (f x) within t) g ⟹ f ` s ⊆ t ⟹
    continuous (at x within s) f ⟹
    continuous (at x within s) (λx. g (f x))"
  by (simp add: continuous_within_compose2 continuous_within_subset)

lemmas continuous_chart[continuous_intros] =
  continuous_within_compose2'[OF continuous_apply_chart]
  continuous_within_compose2'[OF continuous_inv_chart]

lemma continuous_on_chart_inv:
  assumes "continuous_on s (apply_chart c o f)"
    "f ` s ⊆ domain c"
  shows "continuous_on s f"
proof -
  have "continuous_on s (inv_chart c o apply_chart c o f)"
    using assms by (auto intro!: continuous_on_chart(2))
  moreover have "⋀x. x ∈ s ⟹ (inv_chart c o apply_chart c o f) x = f x"
    using assms by auto
  ultimately show ?thesis by auto
qed

lemma continuous_on_chart_inv':
  assumes "continuous_on (apply_chart c ` s) (f o inv_chart c)"
    "s ⊆ domain c"
  shows "continuous_on s f"
proof -
  have "continuous_on s (apply_chart c)"
    using assms continuous_on_domain continuous_on_subset by blast
  then have "continuous_on s (f o inv_chart c o apply_chart c)"
    apply (rule continuous_on_compose) using assms by auto
  moreover have "(f o inv_chart c o apply_chart c) x = f x" if "x ∈ s" for x
    using assms that by auto
  ultimately show ?thesis by auto
qed

lemma inj_on_apply_chart: "inj_on (apply_chart f) (domain f)"
  by (auto simp: intro!: inj_on_inverseI[where g="inv_chart f"])

lemma apply_chart_Int: "f ` (X ∩ Y) = f ` X ∩ f ` Y" if "X ⊆ domain f" "Y ⊆ domain f"
  using inj_on_apply_chart that
  by (rule inj_on_image_Int)

lemma chart_image_eq_vimage: "c ` X = inv_chart c -` X ∩ codomain c"
  if "X ⊆ domain c"
  using that
  by force

lemma open_chart_image[simp, intro]: "open (c ` X)"
  if "open X" "X ⊆ domain c"
proof -
  have "c ` X = inv_chart c -` X ∩ codomain c"
    using that(2)
    by (rule chart_image_eq_vimage)
  also have "open …"
    using that
    by (metis continuous_on_codomain continuous_on_open_vimage open_codomain)
  finally show ?thesis .
qed

lemma open_inv_chart_image[simp, intro]: "open (inv_chart c ` X)"
  if "open X" "X ⊆ codomain c"
proof -
  have "inv_chart c ` X = c -` X ∩ domain c"
    using that(2)
    apply auto
    using image_iff by fastforce
  also have "open …"
    using that
    by (metis continuous_on_domain continuous_on_open_vimage open_domain)
  finally show ?thesis .
qed

lemma homeomorphism_UNIV_imp_open_map:
  "homeomorphism UNIV UNIV p p' ⟹ open f' ⟹ open (p ` f')"
  by (auto dest: homeomorphism_imp_open_map[where U=f'])


subsection ‹Restriction›

lemma homeomorphism_restrict:
  "homeomorphism (a ∩ s) (b ∩ f' -` s) f f'" if "homeomorphism a b f f'"
  using that
  by (fastforce simp: homeomorphism_def intro: continuous_on_subset intro!: imageI)

lift_definition restrict_chart::"'a set ⇒ ('a::t2_space, 'e::euclidean_space) chart ⇒ ('a, 'e) chart"
  is "λS. λ(d, d', f, f'). if open S then (d ∩ S, d' ∩ f' -` S, f, f') else ({}, {}, f, f')"
  by (auto simp: split: if_splits intro!: open_continuous_vimage' homeomorphism_restrict
      intro: homeomorphism_cont2 homeomorphism_cont1 )

lemma restrict_chart_restrict_chart:
  "restrict_chart X (restrict_chart Y c) = restrict_chart (X ∩ Y) c"
  if "open X" "open Y"
  using that
  by transfer auto

lemma domain_restrict_chart[simp]: "open S ⟹ domain (restrict_chart S c) = domain c ∩ S"
  and domain_restrict_chart_if: "domain (restrict_chart S c) = (if open S then domain c ∩ S else {})"
  and codomain_restrict_chart[simp]: "open S ⟹ codomain (restrict_chart S c) = codomain c ∩ inv_chart c -` S"
  and codomain_restrict_chart_if: "codomain (restrict_chart S c) = (if open S then codomain c ∩ inv_chart c -` S else {})"
  and apply_chart_restrict_chart[simp]: "apply_chart (restrict_chart S c) = apply_chart c"
  and inv_chart_restrict_chart[simp]: "inv_chart (restrict_chart S c) = inv_chart c"
  by (transfer, auto)+


subsection ‹Composition›

lift_definition compose_chart::"('e⇒'e) ⇒ ('e⇒'e) ⇒
  ('a::topological_space, 'e::euclidean_space) chart ⇒ ('a, 'e) chart"
  is "λp p'. λ(d, d', f, f'). if homeomorphism UNIV UNIV p p' then (d, p ` d', p o f, f' o p')
    else ({}, {}, f, f')"
  by (auto split: if_splits)
    (auto intro: homeomorphism_UNIV_imp_open_map homeomorphism_compose homeomorphism_of_subsets)

lemma compose_chart_apply_chart[simp]: "apply_chart (compose_chart p p' c) = p o apply_chart c"
  and compose_chart_inv_chart[simp]: "inv_chart (compose_chart p p' c) = inv_chart c o p'"
  and domain_compose_chart[simp]: "domain (compose_chart p p' c) = domain c"
  and codomain_compose_chart[simp]: "codomain (compose_chart p p' c) = p ` codomain c"
  if "homeomorphism UNIV UNIV p p'"
  using that by (transfer, auto)+

end