--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Thu Jan 05 14:18:24 2017 +0000
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Thu Jan 05 15:03:37 2017 +0000
@@ -2021,6 +2021,55 @@
done
qed
+lemma connected_sphere_eq:
+ fixes a :: "'a :: euclidean_space"
+ shows "connected(sphere a r) \<longleftrightarrow> 2 \<le> DIM('a) \<or> r \<le> 0"
+ (is "?lhs = ?rhs")
+proof (cases r "0::real" rule: linorder_cases)
+ case less
+ then show ?thesis by auto
+next
+ case equal
+ then show ?thesis by auto
+next
+ case greater
+ show ?thesis
+ proof
+ assume L: ?lhs
+ have "False" if 1: "DIM('a) = 1"
+ proof -
+ obtain x y where xy: "sphere a r = {x,y}" "x \<noteq> y"
+ using sphere_1D_doubleton [OF 1 greater]
+ by (metis dist_self greater insertI1 less_add_same_cancel1 mem_sphere mult_2 not_le zero_le_dist)
+ then have "finite (sphere a r)"
+ by auto
+ with L \<open>r > 0\<close> show "False"
+ apply (auto simp: connected_finite_iff_sing)
+ using xy by auto
+ qed
+ with greater show ?rhs
+ by (metis DIM_ge_Suc0 One_nat_def Suc_1 le_antisym not_less_eq_eq)
+ next
+ assume ?rhs
+ then show ?lhs
+ using connected_sphere greater by auto
+ qed
+qed
+
+lemma path_connected_sphere_eq:
+ fixes a :: "'a :: euclidean_space"
+ shows "path_connected(sphere a r) \<longleftrightarrow> 2 \<le> DIM('a) \<or> r \<le> 0"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then show ?rhs
+ using connected_sphere_eq path_connected_imp_connected by blast
+next
+ assume R: ?rhs
+ then show ?lhs
+ by (auto simp: contractible_imp_path_connected contractible_sphere path_connected_sphere)
+qed
+
proposition frontier_subset_retraction:
fixes S :: "'a::euclidean_space set"
assumes "bounded S" and fros: "frontier S \<subseteq> T"
@@ -2073,7 +2122,7 @@
ultimately show False by simp
qed
-subsection\<open>Retractions\<close>
+subsection\<open>More Properties of Retractions\<close>
lemma retraction:
"retraction s t r \<longleftrightarrow>
@@ -2272,6 +2321,60 @@
using assms
by (auto simp: retract_of_def retraction intro!: retraction_imp_quotient_map elim!: locally_path_connected_quotient_image)
+subsubsection\<open>A few simple lemmas about deformation retracts\<close>
+
+lemma deformation_retract_imp_homotopy_eqv:
+ fixes S :: "'a::euclidean_space set"
+ assumes "homotopic_with (\<lambda>x. True) S S id r" "retraction S T r"
+ shows "S homotopy_eqv T"
+ apply (simp add: homotopy_eqv_def)
+ apply (rule_tac x=r in exI)
+ using assms apply (simp add: retraction_def)
+ apply (rule_tac x=id in exI)
+ apply (auto simp: continuous_on_id)
+ apply (metis homotopic_with_symD)
+ by (metis continuous_on_id' homotopic_with_equal homotopic_with_symD id_apply image_id subset_refl)
+
+lemma deformation_retract:
+ fixes S :: "'a::euclidean_space set"
+ shows "(\<exists>r. homotopic_with (\<lambda>x. True) S S id r \<and> retraction S T r) \<longleftrightarrow>
+ T retract_of S \<and> (\<exists>f. homotopic_with (\<lambda>x. True) S S id f \<and> f ` S \<subseteq> T)"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then show ?rhs
+ by (auto simp: retract_of_def retraction_def)
+next
+ assume ?rhs
+ then show ?lhs
+ apply (clarsimp simp add: retract_of_def retraction_def)
+ apply (rule_tac x=r in exI, simp)
+ apply (rule homotopic_with_trans, assumption)
+ apply (rule_tac f = "r \<circ> f" and g="r \<circ> id" in homotopic_with_eq)
+ apply (rule_tac Y=S in homotopic_compose_continuous_left)
+ apply (auto simp: homotopic_with_sym)
+ done
+qed
+
+lemma deformation_retract_of_contractible_sing:
+ fixes S :: "'a::euclidean_space set"
+ assumes "contractible S" "a \<in> S"
+ obtains r where "homotopic_with (\<lambda>x. True) S S id r" "retraction S {a} r"
+proof -
+ have "{a} retract_of S"
+ by (simp add: \<open>a \<in> S\<close>)
+ moreover have "homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
+ using assms
+ apply (clarsimp simp add: contractible_def)
+ apply (rule homotopic_with_trans, assumption)
+ by (metis assms(1) contractible_imp_path_connected homotopic_constant_maps homotopic_with_sym homotopic_with_trans insert_absorb insert_not_empty path_component_mem(1) path_connected_component)
+ moreover have "(\<lambda>x. a) ` S \<subseteq> {a}"
+ by (simp add: image_subsetI)
+ ultimately show ?thesis
+ using that deformation_retract by metis
+qed
+
+
subsection\<open>Punctured affine hulls, etc.\<close>
lemma continuous_on_compact_surface_projection_aux:
@@ -2493,6 +2596,23 @@
by (metis assms closure_closed compact_eq_bounded_closed rel_frontier_def
rel_frontier_retract_of_punctured_affine_hull)
+lemma homotopy_eqv_rel_frontier_punctured_convex:
+ fixes S :: "'a::euclidean_space set"
+ assumes "convex S" "bounded S" "a \<in> rel_interior S" "convex T" "rel_frontier S \<subseteq> T" "T \<subseteq> affine hull S"
+ shows "(rel_frontier S) homotopy_eqv (T - {a})"
+ apply (rule rel_frontier_deformation_retract_of_punctured_convex [of S T])
+ using assms
+ apply auto
+ apply (subst homotopy_eqv_sym)
+ using deformation_retract_imp_homotopy_eqv by blast
+
+lemma homotopy_eqv_rel_frontier_punctured_affine_hull:
+ fixes S :: "'a::euclidean_space set"
+ assumes "convex S" "bounded S" "a \<in> rel_interior S"
+ shows "(rel_frontier S) homotopy_eqv (affine hull S - {a})"
+apply (rule homotopy_eqv_rel_frontier_punctured_convex)
+ using assms rel_frontier_affine_hull by force+
+
lemma path_connected_sphere_gen:
assumes "convex S" "bounded S" "aff_dim S \<noteq> 1"
shows "path_connected(rel_frontier S)"
--- a/src/HOL/Analysis/Further_Topology.thy Thu Jan 05 14:18:24 2017 +0000
+++ b/src/HOL/Analysis/Further_Topology.thy Thu Jan 05 15:03:37 2017 +0000
@@ -2976,6 +2976,72 @@
by (simp add: aff_dim_cball)
qed
+lemma simply_connected_sphere_eq:
+ fixes a :: "'a::euclidean_space"
+ shows "simply_connected(sphere a r) \<longleftrightarrow> 3 \<le> DIM('a) \<or> r \<le> 0" (is "?lhs = ?rhs")
+proof (cases "r \<le> 0")
+ case True
+ have "simply_connected (sphere a r)"
+ apply (rule convex_imp_simply_connected)
+ using True less_eq_real_def by auto
+ with True show ?thesis by auto
+next
+ case False
+ show ?thesis
+ proof
+ assume L: ?lhs
+ have "False" if "DIM('a) = 1 \<or> DIM('a) = 2"
+ using that
+ proof
+ assume "DIM('a) = 1"
+ with L show False
+ using connected_sphere_eq simply_connected_imp_connected
+ by (metis False Suc_1 not_less_eq_eq order_refl)
+ next
+ assume "DIM('a) = 2"
+ then have "sphere a r homeomorphic sphere (0::complex) 1"
+ by (metis DIM_complex False homeomorphic_spheres_gen not_less zero_less_one)
+ then have "simply_connected(sphere (0::complex) 1)"
+ using L homeomorphic_simply_connected_eq by blast
+ then obtain a::complex where "homotopic_with (\<lambda>h. True) (sphere 0 1) (sphere 0 1) id (\<lambda>x. a)"
+ apply (simp add: simply_connected_eq_contractible_circlemap)
+ by (metis continuous_on_id' id_apply image_id subset_refl)
+ then show False
+ using contractible_sphere contractible_def not_one_le_zero by blast
+ qed
+ with False show ?rhs
+ apply simp
+ by (metis DIM_ge_Suc0 le_antisym not_less_eq_eq numeral_2_eq_2 numeral_3_eq_3)
+ next
+ assume ?rhs
+ with False show ?lhs by (simp add: simply_connected_sphere)
+ qed
+qed
+
+
+lemma simply_connected_punctured_universe_eq:
+ fixes a :: "'a::euclidean_space"
+ shows "simply_connected(- {a}) \<longleftrightarrow> 3 \<le> DIM('a)"
+proof -
+ have [simp]: "a \<in> rel_interior (cball a 1)"
+ by (simp add: rel_interior_nonempty_interior)
+ have [simp]: "affine hull cball a 1 - {a} = -{a}"
+ by (metis Compl_eq_Diff_UNIV aff_dim_cball aff_dim_lt_full not_less_iff_gr_or_eq zero_less_one)
+ have "simply_connected(- {a}) \<longleftrightarrow> simply_connected(sphere a 1)"
+ apply (rule sym)
+ apply (rule homotopy_eqv_simple_connectedness)
+ using homotopy_eqv_rel_frontier_punctured_affine_hull [of "cball a 1" a] apply auto
+ done
+ also have "... \<longleftrightarrow> 3 \<le> DIM('a)"
+ by (simp add: simply_connected_sphere_eq)
+ finally show ?thesis .
+qed
+
+lemma not_simply_connected_circle:
+ fixes a :: complex
+ shows "0 < r \<Longrightarrow> \<not> simply_connected(sphere a r)"
+by (simp add: simply_connected_sphere_eq)
+
subsection\<open>The power, squaring and exponential functions as covering maps\<close>
--- a/src/HOL/Analysis/Homeomorphism.thy Thu Jan 05 14:18:24 2017 +0000
+++ b/src/HOL/Analysis/Homeomorphism.thy Thu Jan 05 15:03:37 2017 +0000
@@ -8,6 +8,34 @@
imports Path_Connected
begin
+lemma homeomorphic_spheres':
+ fixes a ::"'a::euclidean_space" and b ::"'b::euclidean_space"
+ assumes "0 < \<delta>" and dimeq: "DIM('a) = DIM('b)"
+ shows "(sphere a \<delta>) homeomorphic (sphere b \<delta>)"
+proof -
+ obtain f :: "'a\<Rightarrow>'b" and g where "linear f" "linear g"
+ and fg: "\<And>x. norm(f x) = norm x" "\<And>y. norm(g y) = norm y" "\<And>x. g(f x) = x" "\<And>y. f(g y) = y"
+ by (blast intro: isomorphisms_UNIV_UNIV [OF dimeq])
+ then have "continuous_on UNIV f" "continuous_on UNIV g"
+ using linear_continuous_on linear_linear by blast+
+ then show ?thesis
+ unfolding homeomorphic_minimal
+ apply(rule_tac x="\<lambda>x. b + f(x - a)" in exI)
+ apply(rule_tac x="\<lambda>x. a + g(x - b)" in exI)
+ using assms
+ apply (force intro: continuous_intros
+ continuous_on_compose2 [of _ f] continuous_on_compose2 [of _ g] simp: dist_commute dist_norm fg)
+ done
+qed
+
+lemma homeomorphic_spheres_gen:
+ fixes a :: "'a::euclidean_space" and b :: "'b::euclidean_space"
+ assumes "0 < r" "0 < s" "DIM('a::euclidean_space) = DIM('b::euclidean_space)"
+ shows "(sphere a r homeomorphic sphere b s)"
+ apply (rule homeomorphic_trans [OF homeomorphic_spheres homeomorphic_spheres'])
+ using assms apply auto
+ done
+
subsection \<open>Homeomorphism of all convex compact sets with nonempty interior\<close>
proposition ray_to_rel_frontier: