A few more topological results. And made some slow proofs faster
authorpaulson <lp15@cam.ac.uk>
Tue Oct 31 13:59:19 2017 +0000 (18 months ago)
changeset 66955289f390c4e57
parent 66954 0230af0f3c59
child 66956 696251bf6aec
A few more topological results. And made some slow proofs faster
src/HOL/Analysis/Further_Topology.thy
src/HOL/Analysis/Path_Connected.thy
     1.1 --- a/src/HOL/Analysis/Further_Topology.thy	Tue Oct 31 07:11:03 2017 +0000
     1.2 +++ b/src/HOL/Analysis/Further_Topology.thy	Tue Oct 31 13:59:19 2017 +0000
     1.3 @@ -3799,7 +3799,7 @@
     1.4      by (simp add: Int_assoc openin_INT2 [OF \<open>finite C\<close> \<open>C \<noteq> {}\<close>])
     1.5    with xin obtain d2 where "d2>0"
     1.6                and d2: "\<And>u v. \<lbrakk>u \<in> S; dist u x < d2; v \<in> C\<rbrakk> \<Longrightarrow> f u \<inter> T \<inter> ball v (e/2) \<noteq> {}"
     1.7 -    by (force simp: openin_euclidean_subtopology_iff)
     1.8 +    unfolding openin_euclidean_subtopology_iff using xin by fastforce
     1.9    show ?thesis
    1.10    proof (intro that conjI ballI)
    1.11      show "0 < min d1 d2"
    1.12 @@ -3827,7 +3827,7 @@
    1.13  qed
    1.14  
    1.15  
    1.16 -subsection\<open>complex logs exist on various "well-behaved" sets\<close>
    1.17 +subsection\<open>Complex logs exist on various "well-behaved" sets\<close>
    1.18  
    1.19  lemma continuous_logarithm_on_contractible:
    1.20    fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
    1.21 @@ -3838,7 +3838,7 @@
    1.22      using nullhomotopic_from_contractible assms
    1.23      by (metis imageE subset_Compl_singleton)
    1.24    then show ?thesis
    1.25 -    by (metis inessential_eq_continuous_logarithm of_real_0 that)
    1.26 +    by (metis inessential_eq_continuous_logarithm that)
    1.27  qed
    1.28  
    1.29  lemma continuous_logarithm_on_simply_connected:
    1.30 @@ -3896,6 +3896,72 @@
    1.31  qed
    1.32  
    1.33  
    1.34 +subsection\<open>Another simple case where sphere maps are nullhomotopic.\<close>
    1.35 +
    1.36 +lemma inessential_spheremap_2_aux:
    1.37 +  fixes f :: "'a::euclidean_space \<Rightarrow> complex"
    1.38 +  assumes 2: "2 < DIM('a)" and contf: "continuous_on (sphere a r) f" 
    1.39 +      and fim: "f `(sphere a r) \<subseteq> (sphere 0 1)" 
    1.40 +  obtains c where "homotopic_with (\<lambda>z. True) (sphere a r) (sphere 0 1) f (\<lambda>x. c)"
    1.41 +proof -
    1.42 +  obtain g where contg: "continuous_on (sphere a r) g" 
    1.43 +             and feq: "\<And>x. x \<in> sphere a r \<Longrightarrow> f x = exp(g x)"
    1.44 +  proof (rule continuous_logarithm_on_simply_connected [OF contf])
    1.45 +    show "simply_connected (sphere a r)"
    1.46 +      using 2 by (simp add: simply_connected_sphere_eq)
    1.47 +    show "locally path_connected (sphere a r)"
    1.48 +      by (simp add: locally_path_connected_sphere)
    1.49 +    show "\<And>z.  z \<in> sphere a r \<Longrightarrow> f z \<noteq> 0"
    1.50 +      using fim by force
    1.51 +  qed auto
    1.52 +  have "\<exists>g. continuous_on (sphere a r) g \<and> (\<forall>x\<in>sphere a r. f x = exp (\<i> * complex_of_real (g x)))"
    1.53 +  proof (intro exI conjI)
    1.54 +    show "continuous_on (sphere a r) (Im \<circ> g)"
    1.55 +      by (intro contg continuous_intros continuous_on_compose)
    1.56 +    show "\<forall>x\<in>sphere a r. f x = exp (\<i> * complex_of_real ((Im \<circ> g) x))"
    1.57 +      using exp_eq_polar feq fim norm_exp_eq_Re by auto
    1.58 +  qed
    1.59 +  with inessential_eq_continuous_logarithm_circle that show ?thesis 
    1.60 +    by metis
    1.61 +qed
    1.62 +
    1.63 +lemma inessential_spheremap_2:
    1.64 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
    1.65 +  assumes a2: "2 < DIM('a)" and b2: "DIM('b) = 2" 
    1.66 +      and contf: "continuous_on (sphere a r) f" and fim: "f `(sphere a r) \<subseteq> (sphere b s)"
    1.67 +  obtains c where "homotopic_with (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. c)"
    1.68 +proof (cases "s \<le> 0")
    1.69 +  case True
    1.70 +  then show ?thesis
    1.71 +    using contf contractible_sphere fim nullhomotopic_into_contractible that by blast
    1.72 +next
    1.73 +  case False
    1.74 +  then have "sphere b s homeomorphic sphere (0::complex) 1"
    1.75 +    using assms by (simp add: homeomorphic_spheres_gen)
    1.76 +  then obtain h k where hk: "homeomorphism (sphere b s) (sphere (0::complex) 1) h k"
    1.77 +    by (auto simp: homeomorphic_def)
    1.78 +  then have conth: "continuous_on (sphere b s) h"
    1.79 +       and  contk: "continuous_on (sphere 0 1) k"
    1.80 +       and  him: "h ` sphere b s \<subseteq> sphere 0 1"
    1.81 +       and  kim: "k ` sphere 0 1 \<subseteq> sphere b s"
    1.82 +    by (simp_all add: homeomorphism_def)
    1.83 +  obtain c where "homotopic_with (\<lambda>z. True) (sphere a r) (sphere 0 1) (h \<circ> f) (\<lambda>x. c)"
    1.84 +  proof (rule inessential_spheremap_2_aux [OF a2])
    1.85 +    show "continuous_on (sphere a r) (h \<circ> f)"
    1.86 +      by (meson continuous_on_compose [OF contf] conth continuous_on_subset fim)
    1.87 +    show "(h \<circ> f) ` sphere a r \<subseteq> sphere 0 1"
    1.88 +      using fim him by force
    1.89 +  qed auto
    1.90 +  then have "homotopic_with (\<lambda>f. True) (sphere a r) (sphere b s) (k \<circ> (h \<circ> f)) (k \<circ> (\<lambda>x. c))"
    1.91 +    by (rule homotopic_compose_continuous_left [OF _ contk kim])
    1.92 +  then have "homotopic_with (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. k c)"
    1.93 +    apply (rule homotopic_with_eq, auto)
    1.94 +    by (metis fim hk homeomorphism_def image_subset_iff mem_sphere)
    1.95 +  then show ?thesis
    1.96 +    by (metis that)
    1.97 +qed
    1.98 +
    1.99 +
   1.100  subsection\<open>Holomorphic logarithms and square roots.\<close>
   1.101  
   1.102  lemma contractible_imp_holomorphic_log:
     2.1 --- a/src/HOL/Analysis/Path_Connected.thy	Tue Oct 31 07:11:03 2017 +0000
     2.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Tue Oct 31 13:59:19 2017 +0000
     2.3 @@ -4864,7 +4864,7 @@
     2.4    assumes "locally P S" "openin (subtopology euclidean S) w" "x \<in> w"
     2.5    obtains u v where "openin (subtopology euclidean S) u"
     2.6                      "P v" "x \<in> u" "u \<subseteq> v" "v \<subseteq> w"
     2.7 -using assms by (force simp: locally_def)
     2.8 +  using assms unfolding locally_def by meson
     2.9  
    2.10  lemma locally_mono:
    2.11    assumes "locally P S" "\<And>t. P t \<Longrightarrow> Q t"
    2.12 @@ -4981,7 +4981,7 @@
    2.13    have contvf: "continuous_on v f"
    2.14      using \<open>v \<subseteq> S\<close> continuous_on_subset f(3) by blast
    2.15    have contvg: "continuous_on (f ` v) g"
    2.16 -    using \<open>f ` v \<subseteq> W\<close> \<open>W \<subseteq> t\<close> continuous_on_subset g(3) by blast
    2.17 +    using \<open>f ` v \<subseteq> W\<close> \<open>W \<subseteq> t\<close> continuous_on_subset [OF g(3)] by blast
    2.18    have homv: "homeomorphism v (f ` v) f g"
    2.19      using \<open>v \<subseteq> S\<close> \<open>W \<subseteq> t\<close> f
    2.20      apply (simp add: homeomorphism_def contvf contvg, auto)
    2.21 @@ -5903,7 +5903,7 @@
    2.22      obtain u where u:
    2.23        "openin (subtopology euclidean S) u \<and> x \<in> u \<and> u \<subseteq> t \<and>
    2.24         (\<forall>y. y \<in> u \<longrightarrow> (\<exists>c. connected c \<and> c \<subseteq> t \<and> x \<in> c \<and> y \<in> c))"
    2.25 -      by auto (meson subsetD in_components_subset)
    2.26 +      using in_components_subset by auto
    2.27      obtain F :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a" where
    2.28        "\<forall>x y. (\<exists>z. z \<in> x \<and> y = connected_component_set x z) = (F x y \<in> x \<and> y = connected_component_set x (F x y))"
    2.29        by moura