Theory Topological_Manifold

section ‹Topological Manifolds›
theory Topological_Manifold
  imports Chart
begin

text ‹Definition of topological manifolds. Existence of locally finite cover.›

subsection ‹Defintition›

text ‹We define topological manifolds as a second-countable Hausdorff space, where
  every point in the carrier set has a neighborhood that is homeomorphic to an open
  subset of the Euclidean space. Here topological manifolds are specified by a set
  of charts, and the carrier set is simply defined to be the union of the domain of
  the charts.›
locale manifold =
  fixes charts::"('a::{second_countable_topology, t2_space}, 'e::euclidean_space) chart set"
begin

definition "carrier = (⋃(domain ` charts))"

lemma open_carrier[intro, simp]: "open carrier"
  by (auto simp: carrier_def)

lemma carrierE:
  assumes "x ∈ carrier"
  obtains c where "c ∈ charts" "x ∈ domain c"
  using assms by (auto simp: carrier_def)

lemma domain_subset_carrier[simp]: "domain c ⊆ carrier" if "c ∈ charts"
  using that
  by (auto simp: carrier_def)

lemma in_domain_in_carrier[intro, simp]: "c ∈ charts ⟹ x ∈ domain c ⟹ x ∈ carrier"
  by (auto simp: carrier_def)


subsection ‹Existence of locally finite cover›

text ‹Every point has a precompact neighborhood.›
lemma precompact_neighborhoodE:
  assumes "x ∈ carrier"
  obtains C where "x ∈ C" "open C" "compact (closure C)" "closure C ⊆ carrier"
proof -
  from carrierE[OF assms] obtain c where c: "c ∈ charts" "x ∈ domain c" by auto
  then have "c x ∈ codomain c" by auto
  with open_contains_cball[of "codomain c"]
  obtain e where e: "0 < e" "cball (apply_chart c x) e ⊆ codomain c"
    by auto
  then have e': "ball (apply_chart c x) e ⊆ codomain c"
    by (auto simp: mem_ball)
  define C where "C = inv_chart c ` ball (c x) e"
  have "x ∈ C"
    using c ‹e > 0›
    unfolding C_def
    by (auto intro!: image_eqI[where x="apply_chart c x"])
  moreover have "open C"
    using e'
    by (auto simp: C_def)
  moreover
  have compact: "compact (inv_chart c ` cball (apply_chart c x) e)"
    using e
    by (intro compact_continuous_image continuous_on_chart) auto
  have closure_subset: "closure C ⊆ inv_chart c ` cball (apply_chart c x) e"
    apply (rule closure_minimal)
    subgoal by (auto simp: C_def mem_ball)
    subgoal by (rule compact_imp_closed) (rule compact)
    done
  have "compact (closure C)"
    apply (rule compact_if_closed_subset_of_compact[where T="inv_chart c ` cball (c x) e"])
    subgoal by simp
    subgoal by (rule compact)
    subgoal by (rule closure_subset)
    done
  moreover have "closure C ⊆ carrier"
    using closure_subset c e
    by force
  ultimately show ?thesis ..
qed

text ‹There exists a covering of the carrier by precompact sets.›
lemma precompact_open_coverE:
  obtains U::"nat⇒'a set"
  where "(⋃i. U i) = carrier" "⋀i. open (U i)" "⋀i. compact (closure (U i))"
    "⋀i. closure (U i) ⊆ carrier"
proof cases
  assume "carrier = {}"
  then have "(⋃i. {}) = carrier" "open {}" "compact (closure {})" "closure {} ⊆ carrier"
    by auto
  then show ?thesis ..
next
  assume "carrier ≠ {}"
  have "∃b. x ∈ b ∧ open b ∧ compact (closure b) ∧ closure b ⊆ carrier" if "x ∈ carrier" for x
    using that
    by (rule precompact_neighborhoodE) auto
  then obtain balls where balls:
    "⋀x. x ∈ carrier ⟹ x ∈ balls x"
    "⋀x. x ∈ carrier ⟹ open (balls x)"
    "⋀x. x ∈ carrier ⟹ compact (closure (balls x))"
    "⋀x. x ∈ carrier ⟹ closure (balls x) ⊆ carrier"
    by metis
  let ?balls = "balls ` carrier"
  have *: "⋀x::'a set. x ∈ ?balls ⟹ open x" by (auto simp: balls)
  from Lindelof[of "?balls", OF this]
  obtain ℱ' where ℱ': "ℱ' ⊆ ?balls" "countable ℱ'" "⋃ℱ' = ⋃?balls"
    by auto
  have "ℱ' ≠ {}" using ℱ' balls ‹carrier ≠ {}›
    by auto
  define U where "U = from_nat_into ℱ'"
  have into_range_balls: "U i ∈ ?balls" for i
  proof -
    have "from_nat_into ℱ' i ∈ ℱ'" for i
      by (rule from_nat_into) fact
    also have "ℱ' ⊆ ?balls" by fact
    finally show ?thesis by (simp add: U_def)
  qed
  have U: "open (U i)" "compact (closure (U i))" "closure (U i) ⊆ carrier" for i
    using balls into_range_balls[of i]
    by force+
  then have "U i ⊆ carrier" for i using closure_subset by force
  have "(⋃i. U i) = carrier"
  proof (rule antisym)
    show "(⋃i. U i) ⊆ carrier" using ‹U _ ⊆ carrier› by force
  next
    show "carrier ⊆ (⋃i. U i)"
    proof safe
      fix x::'a
      assume "x ∈ carrier"
      then have "x ∈ balls x" by fact
      with ‹x ∈ carrier› ℱ' obtain F where "x ∈ F" "F ∈ ℱ'" by blast
      with from_nat_into_surj[OF ‹countable ℱ'› ‹F ∈ ℱ'›]
      obtain i where "x ∈ U i" by (auto simp: U_def)
      then show "x ∈ (⋃i. U i)" by auto
    qed
  qed
  then show ?thesis using U ..
qed

text ‹There exists a locally finite covering of the carrier by precompact sets.›
lemma precompact_locally_finite_open_coverE:
  obtains W::"nat⇒'a set"
  where "carrier = (⋃i. W i)" "⋀i. open (W i)" "⋀i. compact (closure (W i))"
    "⋀i. closure (W i) ⊆ carrier"
    "locally_finite_on carrier UNIV W"
proof -
  from precompact_open_coverE obtain U
    where U: "(⋃i::nat. U i) = carrier" "⋀i. open (U i)" "⋀i. compact (closure (U i))"
      "⋀i. closure (U i) ⊆ carrier"
    by auto
  have "∃V. ∀j.
    (open (V j) ∧
    compact (closure (V j)) ∧
    U j ⊆ V j ∧
    closure (V j) ⊆ carrier) ∧
    closure (V j) ⊆ V (Suc j)"
    (is "∃V. ∀j. ?P j (V j) ∧ ?Q j (V j) (V (Suc j))")
  proof (rule dependent_nat_choice)
    show "∃x. ?P 0 x" using U by (force intro!: exI[where x="U 0"])
  next
    fix X n
    assume P: "?P n X"
    have "closure X ⊆ (⋃c. U c)"
      unfolding U using P by auto
    have "compact (closure X)" using P by auto
    from compactE_image[OF this, of UNIV U, OF ‹open (U _)› ‹closure X ⊆ _›]
    obtain M where M: "M ⊆ UNIV" "finite M" "closure X ⊆ (⋃c∈M. U c)"
      by auto
    show "∃y. ?P (Suc n) y ∧ ?Q n X y"
    proof (intro exI[where x="U (Suc n) ∪ (⋃c∈M. U c)"] impI conjI)
      show "open (U (Suc n) ∪ ⋃(U ` M))"
        by (auto intro!: U)
      show "compact (closure (U (Suc n) ∪ ⋃(U ` M)))"
        using ‹finite M›
        by (auto simp add: closure_Union intro!: U)
      show "U (Suc n) ⊆ U (Suc n) ∪ ⋃(U ` M)" by auto
      show "closure (U (Suc n) ∪ ⋃(U ` M)) ⊆ carrier"
        using U ‹finite M›
        by (force simp: closure_Union)
      show "closure X ⊆ U (Suc n) ∪ (⋃c∈M. U c)"
        using M by auto
    qed
  qed
  then obtain V where V:
    "⋀j. closure (V j) ⊆ V (Suc j)"
    "⋀j. open (V j)"
    "⋀j. compact (closure (V j))"
    "⋀j. U j ⊆ V j"
    "⋀j. closure (V j) ⊆ carrier"
    by metis
  have V_mono_Suc: "⋀j. V j ⊆ V (Suc j)"
    using V by auto
  have V_mono: "V l ⊆ V m" if "l ≤ m" for l m
    using V_mono_Suc that
    by (rule lift_Suc_mono_le[of V])
  have V_cover: "carrier = ⋃(V ` UNIV)"
  proof (rule antisym)
    show "carrier ⊆ ⋃(V ` UNIV)"
      unfolding U(1)[symmetric]
      using V(4)
      by auto
    show "⋃(V ` UNIV) ⊆ carrier"
      using V(5) by force
  qed
  define W where "W j = (if j < 2 then V j else V j - closure (V (j - 2)))" for j
  have "compact (closure (W j))" for j
    apply (rule compact_if_closed_subset_of_compact[where T="closure (V j)"])
    subgoal by simp
    subgoal by (simp add: V)
    subgoal
      apply (rule closure_mono)
      using V(1)[of j] V(1)[of "Suc j"]
      by (auto simp: W_def)
    done
  have open_W: "open (W j)" for j
    by (auto simp: W_def V)
  have W_cover: "p ∈ ⋃(W ` UNIV)" if "p ∈ carrier" for p
  proof -
    have "p ∈ ⋃(V ` UNIV)" using that V_cover
      by auto
    then have ex: "∃i. p ∈ V i" by auto
    define k where "k = (LEAST i. p ∈ V i)"
    from LeastI_ex[OF ex]
    have k: "p ∈ V k" by (auto simp: k_def)
    have "p ∈ W k"
    proof cases
      assume "k < 2"
      then show ?thesis using k
        by (auto simp: W_def)
    next
      assume k2: "¬k < 2"
      have False if "p ∈ closure (V (k - 2))"
      proof -
        have "Suc (k - 2) = k - 1" using k2 by arith
        then have "p ∈ V (k - 1)"
          using k2 that V(1)[of "k - 2"]
          by auto
        moreover
        have "k - 1 < k" using k2 by arith
        from not_less_Least[OF this[unfolded k_def], folded k_def]
        have "p ∉ V (k - 1)" .
        ultimately show ?thesis by simp
      qed
      then show ?thesis
        using k
        by (auto simp: W_def)
    qed
    then show ?thesis by auto
  qed
  have W_eq_carrier: "carrier = (⋃i. W i)"
  proof (rule antisym)
    show "carrier ⊆ (⋃i. W i)"
      using W_cover by auto
    have "(⋃i. W i) ⊆ (⋃i. V i)"
      by (auto simp: W_def split: if_splits)
    also have "… = carrier" by (simp add: V_cover)
    finally show "(⋃i. W i) ⊆ carrier" .
  qed
  have W_disjoint: "W k ∩ W l = {}" if less: "l < k - 1" for l k
  proof -
    from less have "k ≥ 2" by arith
    then have "W k = V k - closure (V (k - 2))"
      by (auto simp: W_def)
    moreover have "W l ⊆ V (k - 2)"
    proof -
      have "W l ⊆ V l"
        by (auto simp: W_def)
      also have "… ⊆ V (k - 2)"
        by (rule V_mono) (use less in arith)
      finally show ?thesis .
    qed
    ultimately show ?thesis
      by auto
  qed
  have "locally_finite_on carrier UNIV W"
  proof (rule locally_finite_on_open_coverI)
    show "carrier ⊆ ⋃(W ` UNIV)" unfolding W_eq_carrier by simp
    show "open (W i)" for i by (auto simp: open_W)
    fix k
    have "{i. W i ∩ W k ≠ {}} ⊆ {(k - 1) .. (k + 1)}"
    proof (rule subsetI)
      fix l
      assume "l ∈ {i. W i ∩ W k ≠ {}} "
      then have l: "W l ∩ W k ≠ {}"
        by auto
      consider "l < k - 1" | "l > k + 1" | "k-1 ≤ l" "l ≤ k+1" by arith
      then show "l ∈ {(k - 1) .. (k + 1)}"
      proof cases
        case 1
        from W_disjoint[OF this] l
        show ?thesis by auto
      next
        case 2
        then have "k < l - 1" by arith
        from W_disjoint[OF this] l
        show ?thesis by auto
      next
        case 3
        then show ?thesis
          by (auto simp: l)
      qed
    qed
    also have "finite …" by simp
    finally (finite_subset)
    show "finite {i∈UNIV . W i ∩ W k ≠ {}}" by simp
  qed
  have "closure (W i) ⊆ carrier" for i
    using V closure_mono
    apply (auto simp: W_def)
    using Diff_subset subsetD by blast
  have "carrier = (⋃i. W i)" "⋀i. open (W i)" "⋀i. compact (closure (W i))"
    "⋀i. closure (W i) ⊆ carrier"
    "locally_finite_on carrier UNIV W"
    by fact+
  then show ?thesis ..
qed

end

end