Theory Topological_Space

text ‹Authors: Anthony Bordg and Lawrence Paulson,
with some contributions from Wenda Li›

theory Topological_Space
  imports Complex_Main
          "Jacobson_Basic_Algebra.Set_Theory"
          Set_Extras

begin

section ‹Topological Spaces›

locale topological_space = fixes S :: "'a set" and is_open :: "'a set ⇒ bool"
  assumes open_space [simp, intro]: "is_open S" and open_empty [simp, intro]: "is_open {}"
    and open_imp_subset: "is_open U ⟹ U ⊆ S"
    and open_inter [intro]: "⟦is_open U; is_open V⟧ ⟹ is_open (U ∩ V)"
    and open_union [intro]: "⋀F::('a set) set. (⋀x. x ∈ F ⟹ is_open x) ⟹ is_open (⋃x∈F. x)"

begin

definition is_closed :: "'a set ⇒ bool"
  where "is_closed U ≡ U ⊆ S ∧ is_open (S - U)"

definition neighborhoods:: "'a ⇒ ('a set) set"
  where "neighborhoods x ≡ {U. is_open U ∧ x ∈ U}"

text ‹Note that by a neighborhood we mean what some authors call an open neighborhood.›

lemma open_union' [intro]: "⋀F::('a set) set. (⋀x. x ∈ F ⟹ is_open x) ⟹ is_open (⋃F)"
  using open_union by auto

lemma open_preimage_identity [simp]: "is_open B ⟹ identity S ⇧¯ S B = B"
  by (metis inf.orderE open_imp_subset preimage_identity_self)


definition is_connected:: "bool" where
"is_connected ≡ ¬ (∃U V. is_open U ∧ is_open V ∧ (U ≠ {}) ∧ (V ≠ {}) ∧ (U ∩ V = {}) ∧ (U ∪ V = S))"

definition is_hausdorff:: "bool" where
"is_hausdorff ≡
∀x y. (x ∈ S ∧ y ∈ S ∧ x ≠ y) ⟶ (∃U V. U ∈ neighborhoods x ∧ V ∈ neighborhoods y ∧ U ∩ V = {})"

end (* topological_space *)

text ‹T2 spaces are also known as Hausdorff spaces.›

locale t2_space = topological_space +
  assumes hausdorff: "is_hausdorff"


subsection ‹Topological Basis›

inductive generated_topology :: "'a set ⇒ 'a set set ⇒ 'a set ⇒ bool"
    for S :: "'a set" and B :: "'a set set"
  where
    UNIV: "generated_topology S B S"
  | Int: "generated_topology S B (U ∩ V)"
            if "generated_topology S B U" and "generated_topology S B V"
  | UN: "generated_topology S B (⋃K)" if "(⋀U. U ∈ K ⟹ generated_topology S B U)"
  | Basis: "generated_topology S B b" if "b ∈ B ∧ b ⊆ S"

lemma generated_topology_empty [simp]: "generated_topology S B {}"
  by (metis UN Union_empty empty_iff)

lemma generated_topology_subset: "generated_topology S B U ⟹ U ⊆ S"
  by (induct rule:generated_topology.induct) auto

lemma generated_topology_is_topology:
  fixes S:: "'a set" and B:: "'a set set"
  shows "topological_space S (generated_topology S B)"
  by (simp add: Int UN UNIV generated_topology_subset topological_space_def)


subsection ‹Covers›

locale cover_of_subset =
  fixes X:: "'a set" and U:: "'a set" and index:: "real set" and cover:: "real ⇒ 'a set"
(* We use real instead of index::"'b set" otherwise we get some troubles with locale sheaf_of_rings
in Comm_Ring_Theory.thy *)
  assumes is_subset: "U ⊆ X" and are_subsets: "⋀i. i ∈ index ⟹ cover i ⊆ X"
and covering: "U ⊆ (⋃i∈index. cover i)"
begin

lemma
  assumes "x ∈ U"
  shows "∃i∈index. x ∈ cover i"
  using assms covering by auto

definition select_index:: "'a ⇒ real"
  where "select_index x ≡ SOME i. i ∈ index ∧ x ∈ cover i"

lemma cover_of_select_index:
  assumes "x ∈ U"
  shows "x ∈ cover (select_index x)"
  using assms by (metis (mono_tags, lifting) UN_iff covering select_index_def someI_ex subset_iff)

lemma select_index_belongs:
  assumes "x ∈ U"
  shows "select_index x ∈ index"
  using assms by (metis (full_types, lifting) UN_iff covering in_mono select_index_def tfl_some)

end (* cover_of_subset *)

locale open_cover_of_subset = topological_space X is_open + cover_of_subset X U I C
  for X and is_open and U and I and C +
  assumes are_open_subspaces: "⋀i. i∈I ⟹ is_open (C i)"
begin

lemma cover_of_select_index_is_open:
  assumes "x ∈ U"
  shows "is_open (C (select_index x))"
  using assms by (simp add: are_open_subspaces select_index_belongs)

end (* open_cover_of_subset *)

locale open_cover_of_open_subset = open_cover_of_subset X is_open U I C
  for X and is_open and U and I and C +
  assumes is_open_subset: "is_open U"


subsection ‹Induced Topology›

locale ind_topology = topological_space X is_open for X and is_open +
  fixes S:: "'a set"
  assumes is_subset: "S ⊆ X"
begin

definition ind_is_open:: "'a set ⇒ bool"
  where "ind_is_open U ≡ U ⊆ S ∧ (∃V. V ⊆ X ∧ is_open V ∧ U = S ∩ V)"

lemma ind_is_open_S [iff]: "ind_is_open S"
    by (metis ind_is_open_def inf.orderE is_subset open_space order_refl)

lemma ind_is_open_empty [iff]: "ind_is_open {}"
    using ind_is_open_def by auto

lemma ind_space_is_top_space:
  shows "topological_space S (ind_is_open)"
proof
  fix U V
  assume "ind_is_open U" then obtain UX where "UX ⊆ X" "is_open UX" "U = S ∩ UX"
    using ind_is_open_def by auto
  moreover
  assume "ind_is_open V" then obtain VX where "VX ⊆ X" "is_open VX" "V = S ∩ VX"
    using ind_is_open_def by auto
  ultimately have "is_open (UX ∩ VX) ∧ (U ∩ V = S ∩ (UX ∩ VX))" using open_inter by auto
  then show "ind_is_open (U ∩ V)"
    by (metis ‹UX ⊆ X› ind_is_open_def le_infI1 subset_refl)
next
  fix F
  assume F: "⋀x. x ∈ F ⟹ ind_is_open x"
  obtain F' where F': "⋀x. x ∈ F ∧ ind_is_open x ⟹ is_open (F' x) ∧ x = S ∩ (F' x)"
    using ind_is_open_def by metis
  have "is_open (⋃ (F' ` F))"
    by (metis (mono_tags, lifting) F F' imageE image_ident open_union)
  moreover
  have "(⋃x∈F. x) = S ∩ ⋃ (F' ` F)"
    using F' ‹⋀x. x ∈ F ⟹ ind_is_open x› by fastforce
  ultimately show "ind_is_open (⋃x∈F. x)"
    by (metis ind_is_open_def inf_sup_ord(1) open_imp_subset)
next
  show "⋀U. ind_is_open U ⟹ U ⊆ S"
    by (simp add: ind_is_open_def)
qed auto

lemma is_open_from_ind_is_open:
  assumes "is_open S" and "ind_is_open U"
  shows "is_open U"
  using assms open_inter ind_is_open_def is_subset by auto

lemma open_cover_from_ind_open_cover:
  assumes "is_open S" and "open_cover_of_open_subset S ind_is_open U I C"
  shows "open_cover_of_open_subset X is_open U I C"
proof
  show "is_open U"
    using assms is_open_from_ind_is_open open_cover_of_open_subset.is_open_subset by blast
  show "⋀i. i ∈ I ⟹ is_open (C i)"
    using assms is_open_from_ind_is_open open_cover_of_open_subset_def open_cover_of_subset.are_open_subspaces by blast
  show "⋀i. i ∈ I ⟹ C i ⊆ X"
    using assms(2) is_subset
    by (meson cover_of_subset_def open_cover_of_open_subset_def open_cover_of_subset_def subset_trans)
  show "U ⊆ X"
    by (simp add: ‹is_open U› open_imp_subset)
  show "U ⊆ ⋃ (C ` I)"
    by (meson assms(2) cover_of_subset_def open_cover_of_open_subset_def open_cover_of_subset_def)
qed

end (* induced topology *)

lemma (in topological_space) ind_topology_is_open_self [iff]: "ind_topology S is_open S"
  by (simp add: ind_topology_axioms_def ind_topology_def topological_space_axioms)

lemma (in topological_space) ind_topology_is_open_empty [iff]: "ind_topology S is_open {}"
  by (simp add: ind_topology_axioms_def ind_topology_def topological_space_axioms)

lemma (in topological_space) ind_is_open_iff_open:
  shows "ind_topology.ind_is_open S is_open S U ⟷ is_open U ∧ U ⊆ S"
  by (metis ind_topology.ind_is_open_def ind_topology_is_open_self inf.absorb_iff2)

subsection ‹Continuous Maps›

locale continuous_map = source: topological_space S is_open + target: topological_space S' is_open'
+ map f S S'
  for S and is_open and S' and is_open' and f +
  assumes is_continuous: "⋀U. is_open' U ⟹ is_open (f⇧¯ S U)"
begin

lemma open_cover_of_open_subset_from_target_to_source:
  assumes "open_cover_of_open_subset S' is_open' U I C"
  shows "open_cover_of_open_subset S is_open (f⇧¯ S U) I (λi. f⇧¯ S (C i))"
proof
  show "f ⇧¯ S U ⊆ S" by simp
  show "f ⇧¯ S (C i) ⊆ S" if "i ∈ I" for i
    using that by simp
  show "is_open (f ⇧¯ S U)"
    by (meson assms is_continuous open_cover_of_open_subset.is_open_subset)
  show "⋀i. i ∈ I ⟹ is_open (f ⇧¯ S (C i))"
    by (meson assms is_continuous open_cover_of_open_subset_def open_cover_of_subset.are_open_subspaces)
  show "f ⇧¯ S U ⊆ (⋃i∈I. f ⇧¯ S (C i))"
    using assms unfolding open_cover_of_open_subset_def cover_of_subset_def open_cover_of_subset_def
    by blast
qed

end (* continuous map *)


subsection ‹Homeomorphisms›

text ‹The topological isomorphisms between topological spaces are called homeomorphisms.›

locale homeomorphism =
  continuous_map + bijective_map f S S' +
  continuous_map S' is_open' S is_open "inverse_map f S S'"

lemma (in topological_space) id_is_homeomorphism:
  shows "homeomorphism S is_open S is_open (identity S)"
proof
  show "inverse_map (identity S) S S ∈ S →⇩E S"
    by (simp add: inv_into_into inverse_map_def)
qed (auto simp: open_inter bij_betwI')


subsection ‹Topological Filters› (* Imported from HOL.Topological_Spaces *)

definition (in topological_space) nhds :: "'a ⇒ 'a filter"
  where "nhds a = (INF S∈{S. is_open S ∧ a ∈ S}. principal S)"

abbreviation (in topological_space)
  tendsto :: "('b ⇒ 'a) ⇒ 'a ⇒ 'b filter ⇒ bool"  (infixr "⤏" 55)
  where "(f ⤏ l) F ≡ filterlim f (nhds l) F"

definition (in t2_space) Lim :: "'f filter ⇒ ('f ⇒ 'a) ⇒ 'a"
  where "Lim A f = (THE l. (f ⤏ l) A)"

end