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 (xF. 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  (iindex. cover i)"
begin

lemma
  assumes "x  U"
  shows "iindex. 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. iI  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 "(xF. x) = S   (F' ` F)"
    using F' x. x  F  ind_is_open x by fastforce
  ultimately show "ind_is_open (xF. 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  (iI. 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