src/HOL/Analysis/Homotopy.thy

 
 theory Homotopy
   imports Path_Connected Continuum_Not_Denumerable Product_Topology
 begin
 
-definition%important homotopic_with
+definition\<^marker>\<open>tag important\<close> homotopic_with
 where
  "homotopic_with P X Y f g \<equiv>
    (\<exists>h. continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y h \<and>
        (\<forall>x. h(0, x) = f x) \<and>
        (\<forall>x. h(1, x) = g x) \<and>

   shows "continuous_map Y Z (h \<circ> Pair t)"
   apply (intro continuous_map_compose [OF _ h] continuous_map_id [unfolded id_def] continuous_intros)
   apply (simp add: t)
   done
 
-subsection%unimportant\<open>Trivial properties\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Trivial properties\<close>
 
 text \<open>We often want to just localize the ending function equality or whatever.\<close>
-text%important \<open>%whitespace\<close>
+text\<^marker>\<open>tag important\<close> \<open>%whitespace\<close>
 proposition homotopic_with:
   assumes "\<And>h k. (\<And>x. x \<in> topspace X \<Longrightarrow> h x = k x) \<Longrightarrow> (P h \<longleftrightarrow> P k)"
   shows "homotopic_with P X Y p q \<longleftrightarrow>
            (\<exists>h. continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y h \<and>
               (\<forall>x \<in> topspace X. h(0,x) = p x) \<and>

 
 
 subsection\<open>Homotopy of paths, maintaining the same endpoints\<close>
 
 
-definition%important homotopic_paths :: "['a set, real \<Rightarrow> 'a, real \<Rightarrow> 'a::topological_space] \<Rightarrow> bool"
+definition\<^marker>\<open>tag important\<close> homotopic_paths :: "['a set, real \<Rightarrow> 'a, real \<Rightarrow> 'a::topological_space] \<Rightarrow> bool"
   where
      "homotopic_paths s p q \<equiv>
        homotopic_with_canon (\<lambda>r. pathstart r = pathstart p \<and> pathfinish r = pathfinish p) {0..1} s p q"
 
 lemma homotopic_paths:

   by (simp add: homotopic_with_compose_continuous_map_left pathfinish_compose pathstart_compose)
 
 
 subsection\<open>Group properties for homotopy of paths\<close>
 
-text%important\<open>So taking equivalence classes under homotopy would give the fundamental group\<close>
+text\<^marker>\<open>tag important\<close>\<open>So taking equivalence classes under homotopy would give the fundamental group\<close>
 
 proposition homotopic_paths_rid:
     "\<lbrakk>path p; path_image p \<subseteq> s\<rbrakk> \<Longrightarrow> homotopic_paths s (p +++ linepath (pathfinish p) (pathfinish p)) p"
   apply (subst homotopic_paths_sym)
   apply (rule homotopic_paths_reparametrize [where f = "\<lambda>t. if  t \<le> 1 / 2 then 2 *\<^sub>R t else 1"])

   using homotopic_paths_rinv [of "reversepath p" s] assms by simp
 
 
 subsection\<open>Homotopy of loops without requiring preservation of endpoints\<close>
 
-definition%important homotopic_loops :: "'a::topological_space set \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> bool"  where
+definition\<^marker>\<open>tag important\<close> homotopic_loops :: "'a::topological_space set \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> bool"  where
  "homotopic_loops s p q \<equiv>
      homotopic_with_canon (\<lambda>r. pathfinish r = pathstart r) {0..1} s p q"
 
 lemma homotopic_loops:
    "homotopic_loops s p q \<longleftrightarrow>

       using \<open>path q\<close> homotopic_loops_imp_path loops path_join_path_ends by fastforce
   qed
 qed
 
 
-subsection%unimportant\<open>Homotopy of "nearby" function, paths and loops\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Homotopy of "nearby" function, paths and loops\<close>
 
 lemma homotopic_with_linear:
   fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
   assumes contf: "continuous_on s f"
       and contg:"continuous_on s g"

 by (auto simp: path_connected_def path_component_def homotopic_points_eq_path_component)
 
 
 subsection\<open>Simply connected sets\<close>
 
-text%important\<open>defined as "all loops are homotopic (as loops)\<close>
-
-definition%important simply_connected where
+text\<^marker>\<open>tag important\<close>\<open>defined as "all loops are homotopic (as loops)\<close>
+
+definition\<^marker>\<open>tag important\<close> simply_connected where
   "simply_connected S \<equiv>
         \<forall>p q. path p \<and> pathfinish p = pathstart p \<and> path_image p \<subseteq> S \<and>
               path q \<and> pathfinish q = pathstart q \<and> path_image q \<subseteq> S
               \<longrightarrow> homotopic_loops S p q"
 

 qed
 
 
 subsection\<open>Contractible sets\<close>
 
-definition%important contractible where
+definition\<^marker>\<open>tag important\<close> contractible where
  "contractible S \<equiv> \<exists>a. homotopic_with_canon (\<lambda>x. True) S S id (\<lambda>x. a)"
 
 proposition contractible_imp_simply_connected:
   fixes S :: "_::real_normed_vector set"
   assumes "contractible S" shows "simply_connected S"

 qed
 
 
 subsection\<open>Local versions of topological properties in general\<close>
 
-definition%important locally :: "('a::topological_space set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
+definition\<^marker>\<open>tag important\<close> locally :: "('a::topological_space set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
 where
  "locally P S \<equiv>
         \<forall>w x. openin (top_of_set S) w \<and> x \<in> w
               \<longrightarrow> (\<exists>u v. openin (top_of_set S) u \<and> P v \<and>
                         x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w)"

   qed
   ultimately show "openin (top_of_set (f ` S)) (path_component_set U y)"
     by metis
 qed
 
-subsection%unimportant\<open>Components, continuity, openin, closedin\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Components, continuity, openin, closedin\<close>
 
 lemma continuous_on_components_gen:
  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   assumes "\<And>c. c \<in> components S \<Longrightarrow>
               openin (top_of_set S) c \<and> continuous_on c f"

 qed
 
 
 subsection\<open>Retracts, in a general sense, preserve (co)homotopic triviality)\<close>
 
-locale%important Retracts =
+locale\<^marker>\<open>tag important\<close> Retracts =
   fixes s h t k
   assumes conth: "continuous_on s h"
       and imh: "h ` s = t"
       and contk: "continuous_on t k"
       and imk: "k ` t \<subseteq> s"

 
 subsection\<open>Homotopy equivalence\<close>
 
 subsection\<open>Homotopy equivalence of topological spaces.\<close>
 
-definition%important homotopy_equivalent_space
+definition\<^marker>\<open>tag important\<close> homotopy_equivalent_space
              (infix "homotopy'_equivalent'_space" 50)
   where "X homotopy_equivalent_space Y \<equiv>
         (\<exists>f g. continuous_map X Y f \<and>
               continuous_map Y X g \<and>
               homotopic_with (\<lambda>x. True) X X (g \<circ> f) id \<and>

   then show ?thesis
     by simp
 qed
 
 
-abbreviation%important homotopy_eqv :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
+abbreviation\<^marker>\<open>tag important\<close> homotopy_eqv :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
              (infix "homotopy'_eqv" 50)
   where "S homotopy_eqv T \<equiv> top_of_set S homotopy_equivalent_space top_of_set T"
 
 
 

   fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
   shows "\<lbrakk>contractible S; S homeomorphic T\<rbrakk> \<Longrightarrow> contractible T"
   by (metis homeomorphic_contractible_eq)
 
 
-subsection%unimportant\<open>Misc other results\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Misc other results\<close>
 
 lemma bounded_connected_Compl_real:
   fixes S :: "real set"
   assumes "bounded S" and conn: "connected(- S)"
     shows "S = {}"

   then show ?thesis
     by blast
 qed
 
 
-subsection%unimportant\<open>Some Uncountable Sets\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Some Uncountable Sets\<close>
 
 lemma uncountable_closed_segment:
   fixes a :: "'a::real_normed_vector"
   assumes "a \<noteq> b" shows "uncountable (closed_segment a b)"
 unfolding path_image_linepath [symmetric] path_image_def

   assumes "arc g"
   shows "uncountable (path_image g)"
   by (simp add: arc_imp_simple_path assms simple_path_image_uncountable)
 
 
-subsection%unimportant\<open> Some simple positive connection theorems\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open> Some simple positive connection theorems\<close>
 
 proposition path_connected_convex_diff_countable:
   fixes U :: "'a::euclidean_space set"
   assumes "convex U" "\<not> collinear U" "countable S"
     shows "path_connected(U - S)"

   shows "connected(S - T)"
 by (simp add: assms path_connected_imp_connected path_connected_open_diff_countable)
 
 
 
-subsection%unimportant \<open>Self-homeomorphisms shuffling points about\<close>
-
-subsubsection%unimportant\<open>The theorem \<open>homeomorphism_moving_points_exists\<close>\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Self-homeomorphisms shuffling points about\<close>
+
+subsubsection\<^marker>\<open>tag unimportant\<close>\<open>The theorem \<open>homeomorphism_moving_points_exists\<close>\<close>
 
 lemma homeomorphism_moving_point_1:
   fixes a :: "'a::euclidean_space"
   assumes "affine T" "a \<in> T" and u: "u \<in> ball a r \<inter> T"
   obtains f g where "homeomorphism (cball a r \<inter> T) (cball a r \<inter> T) f g"

     using \<open>r > 0\<close>
      apply (simp_all add: f_def dist_norm norm_minus_commute)
     done
 qed
 
-corollary%unimportant homeomorphism_moving_point_2:
+corollary\<^marker>\<open>tag unimportant\<close> homeomorphism_moving_point_2:
   fixes a :: "'a::euclidean_space"
   assumes "affine T" "a \<in> T" and u: "u \<in> ball a r \<inter> T" and v: "v \<in> ball a r \<inter> T"
   obtains f g where "homeomorphism (cball a r \<inter> T) (cball a r \<inter> T) f g"
                     "f u = v" "\<And>x. \<lbrakk>x \<in> sphere a r; x \<in> T\<rbrakk> \<Longrightarrow> f x = x"
 proof -

       using f1 f2 hom1 homeomorphism_apply1 by fastforce
   qed
 qed
 
 
-corollary%unimportant homeomorphism_moving_point_3:
+corollary\<^marker>\<open>tag unimportant\<close> homeomorphism_moving_point_3:
   fixes a :: "'a::euclidean_space"
   assumes "affine T" "a \<in> T" and ST: "ball a r \<inter> T \<subseteq> S" "S \<subseteq> T"
       and u: "u \<in> ball a r \<inter> T" and v: "v \<in> ball a r \<inter> T"
   obtains f g where "homeomorphism S S f g"
                     "f u = v" "{x. \<not> (f x = x \<and> g x = x)} \<subseteq> ball a r \<inter> T"

       by (auto simp: ff_def gg_def)
   qed
 qed
 
 
-proposition%unimportant homeomorphism_moving_point:
+proposition\<^marker>\<open>tag unimportant\<close> homeomorphism_moving_point:
   fixes a :: "'a::euclidean_space"
   assumes ope: "openin (top_of_set (affine hull S)) S"
       and "S \<subseteq> T"
       and TS: "T \<subseteq> affine hull S"
       and S: "connected S" "a \<in> S" "b \<in> S"

     then show "bounded {x. \<not> ((h \<circ> f) x = x \<and> (g \<circ> k) x = x)}"
       by (rule bounded_subset) auto
   qed
 qed
 
-proposition%unimportant homeomorphism_moving_points_exists:
+proposition\<^marker>\<open>tag unimportant\<close> homeomorphism_moving_points_exists:
   fixes S :: "'a::euclidean_space set"
   assumes 2: "2 \<le> DIM('a)" "open S" "connected S" "S \<subseteq> T" "finite K"
       and KS: "\<And>i. i \<in> K \<Longrightarrow> x i \<in> S \<and> y i \<in> S"
       and pw: "pairwise (\<lambda>i j. (x i \<noteq> x j) \<and> (y i \<noteq> y j)) K"
       and S: "S \<subseteq> T" "T \<subseteq> affine hull S" "connected S"

     by linarith
   then show ?thesis
     using homeomorphism_moving_points_exists_gen [OF \<open>finite K\<close> KS pw _ ope S] that by fastforce
 qed
 
-subsubsection%unimportant\<open>The theorem \<open>homeomorphism_grouping_points_exists\<close>\<close>
+subsubsection\<^marker>\<open>tag unimportant\<close>\<open>The theorem \<open>homeomorphism_grouping_points_exists\<close>\<close>
 
 lemma homeomorphism_grouping_point_1:
   fixes a::real and c::real
   assumes "a < b" "c < d"
   obtains f g where "homeomorphism (cbox a b) (cbox c d) f g" "f a = c" "f b = d"

       apply (auto simp: f'_def g'_def)
       done
   qed
 qed
 
-proposition%unimportant homeomorphism_grouping_points_exists:
+proposition\<^marker>\<open>tag unimportant\<close> homeomorphism_grouping_points_exists:
   fixes S :: "'a::euclidean_space set"
   assumes "open U" "open S" "connected S" "U \<noteq> {}" "finite K" "K \<subseteq> S" "U \<subseteq> S" "S \<subseteq> T"
   obtains f g where "homeomorphism T T f g" "{x. (\<not> (f x = x \<and> g x = x))} \<subseteq> S"
                     "bounded {x. (\<not> (f x = x \<and> g x = x))}" "\<And>x. x \<in> K \<Longrightarrow> f x \<in> U"
 proof (cases "2 \<le> DIM('a)")

       using f hj by fastforce
   qed
 qed
 
 
-proposition%unimportant homeomorphism_grouping_points_exists_gen:
+proposition\<^marker>\<open>tag unimportant\<close> homeomorphism_grouping_points_exists_gen:
   fixes S :: "'a::euclidean_space set"
   assumes opeU: "openin (top_of_set S) U"
       and opeS: "openin (top_of_set (affine hull S)) S"
       and "U \<noteq> {}" "finite K" "K \<subseteq> S" and S: "S \<subseteq> T" "T \<subseteq> affine hull S" "connected S"
   obtains f g where "homeomorphism T T f g" "{x. (\<not> (f x = x \<and> g x = x))} \<subseteq> S"