(* Title: HOL/Analysis/Path_Connected.thy Authors: LC Paulson and Robert Himmelmann (TU Muenchen), based on material from HOL Light *) section ‹Homotopy of Maps› theory Homotopy imports Path_Connected Product_Topology Uncountable_Sets begin definition✐‹tag important› homotopic_with where "homotopic_with P X Y f g ≡ (∃h. continuous_map (prod_topology (top_of_set {0..1::real}) X) Y h ∧ (∀x. h(0, x) = f x) ∧ (∀x. h(1, x) = g x) ∧ (∀t ∈ {0..1}. P(λx. h(t,x))))" text‹‹p›, ‹q› are functions ‹X → Y›, and the property ‹P› restricts all intermediate maps. We often just want to require that ‹P› fixes some subset, but to include the case of a loop homotopy, it is convenient to have a general property ‹P›.› abbreviation homotopic_with_canon :: "[('a::topological_space ⇒ 'b::topological_space) ⇒ bool, 'a set, 'b set, 'a ⇒ 'b, 'a ⇒ 'b] ⇒ bool" where "homotopic_with_canon P S T p q ≡ homotopic_with P (top_of_set S) (top_of_set T) p q" lemma split_01: "{0..1::real} = {0..1/2} ∪ {1/2..1}" by force lemma split_01_prod: "{0..1::real} × X = ({0..1/2} × X) ∪ ({1/2..1} × X)" by force lemma image_Pair_const: "(λx. (x, c)) ` A = A × {c}" by auto lemma fst_o_paired [simp]: "fst ∘ (λ(x,y). (f x y, g x y)) = (λ(x,y). f x y)" by auto lemma snd_o_paired [simp]: "snd ∘ (λ(x,y). (f x y, g x y)) = (λ(x,y). g x y)" by auto lemma continuous_on_o_Pair: "⟦continuous_on (T × X) h; t ∈ T⟧ ⟹ continuous_on X (h ∘ Pair t)" by (fast intro: continuous_intros elim!: continuous_on_subset) lemma continuous_map_o_Pair: assumes h: "continuous_map (prod_topology X Y) Z h" and t: "t ∈ topspace X" shows "continuous_map Y Z (h ∘ Pair t)" by (intro continuous_map_compose [OF _ h] continuous_intros; simp add: t) subsection✐‹tag unimportant›‹Trivial properties› text ‹We often want to just localize the ending function equality or whatever.› text✐‹tag important› ‹%whitespace› proposition homotopic_with: assumes "⋀h k. (⋀x. x ∈ topspace X ⟹ h x = k x) ⟹ (P h ⟷ P k)" shows "homotopic_with P X Y p q ⟷ (∃h. continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y h ∧ (∀x ∈ topspace X. h(0,x) = p x) ∧ (∀x ∈ topspace X. h(1,x) = q x) ∧ (∀t ∈ {0..1}. P(λx. h(t, x))))" unfolding homotopic_with_def apply (rule iffI, blast, clarify) apply (rule_tac x="λ(u,v). if v ∈ topspace X then h(u,v) else if u = 0 then p v else q v" in exI) apply simp by (smt (verit, best) SigmaE assms case_prod_conv continuous_map_eq topspace_prod_topology) lemma homotopic_with_mono: assumes hom: "homotopic_with P X Y f g" and Q: "⋀h. ⟦continuous_map X Y h; P h⟧ ⟹ Q h" shows "homotopic_with Q X Y f g" using hom unfolding homotopic_with_def by (force simp: o_def dest: continuous_map_o_Pair intro: Q) lemma homotopic_with_imp_continuous_maps: assumes "homotopic_with P X Y f g" shows "continuous_map X Y f ∧ continuous_map X Y g" proof - obtain h :: "real × 'a ⇒ 'b" where conth: "continuous_map (prod_topology (top_of_set {0..1}) X) Y h" and h: "∀x. h (0, x) = f x" "∀x. h (1, x) = g x" using assms by (auto simp: homotopic_with_def) have *: "t ∈ {0..1} ⟹ continuous_map X Y (h ∘ (λx. (t,x)))" for t by (rule continuous_map_compose [OF _ conth]) (simp add: o_def continuous_map_pairwise) show ?thesis using h *[of 0] *[of 1] by (simp add: continuous_map_eq) qed lemma homotopic_with_imp_continuous: assumes "homotopic_with_canon P X Y f g" shows "continuous_on X f ∧ continuous_on X g" by (meson assms continuous_map_subtopology_eu homotopic_with_imp_continuous_maps) lemma homotopic_with_imp_property: assumes "homotopic_with P X Y f g" shows "P f ∧ P g" proof obtain h where h: "⋀x. h(0, x) = f x" "⋀x. h(1, x) = g x" and P: "⋀t. t ∈ {0..1::real} ⟹ P(λx. h(t,x))" using assms by (force simp: homotopic_with_def) show "P f" "P g" using P [of 0] P [of 1] by (force simp: h)+ qed lemma homotopic_with_equal: assumes "P f" "P g" and contf: "continuous_map X Y f" and fg: "⋀x. x ∈ topspace X ⟹ f x = g x" shows "homotopic_with P X Y f g" unfolding homotopic_with_def proof (intro exI conjI allI ballI) let ?h = "λ(t::real,x). if t = 1 then g x else f x" show "continuous_map (prod_topology (top_of_set {0..1}) X) Y ?h" proof (rule continuous_map_eq) show "continuous_map (prod_topology (top_of_set {0..1}) X) Y (f ∘ snd)" by (simp add: contf continuous_map_of_snd) qed (auto simp: fg) show "P (λx. ?h (t, x))" if "t ∈ {0..1}" for t by (cases "t = 1") (simp_all add: assms) qed auto lemma homotopic_with_imp_subset1: "homotopic_with_canon P X Y f g ⟹ f ` X ⊆ Y" by (meson continuous_map_subtopology_eu homotopic_with_imp_continuous_maps) lemma homotopic_with_imp_subset2: "homotopic_with_canon P X Y f g ⟹ g ` X ⊆ Y" by (meson continuous_map_subtopology_eu homotopic_with_imp_continuous_maps) lemma homotopic_with_imp_funspace1: "homotopic_with_canon P X Y f g ⟹ f ∈ X → Y" using homotopic_with_imp_subset1 by blast lemma homotopic_with_imp_funspace2: "homotopic_with_canon P X Y f g ⟹ g ∈ X → Y" using homotopic_with_imp_subset2 by blast lemma homotopic_with_subset_left: "⟦homotopic_with_canon P X Y f g; Z ⊆ X⟧ ⟹ homotopic_with_canon P Z Y f g" unfolding homotopic_with_def by (auto elim!: continuous_on_subset ex_forward) lemma homotopic_with_subset_right: "⟦homotopic_with_canon P X Y f g; Y ⊆ Z⟧ ⟹ homotopic_with_canon P X Z f g" unfolding homotopic_with_def by (auto elim!: continuous_on_subset ex_forward) subsection‹Homotopy with P is an equivalence relation› text ‹(on continuous functions mapping X into Y that satisfy P, though this only affects reflexivity)› lemma homotopic_with_refl [simp]: "homotopic_with P X Y f f ⟷ continuous_map X Y f ∧ P f" by (metis homotopic_with_equal homotopic_with_imp_continuous_maps homotopic_with_imp_property) lemma homotopic_with_symD: assumes "homotopic_with P X Y f g" shows "homotopic_with P X Y g f" proof - let ?I01 = "subtopology euclideanreal {0..1}" let ?j = "λy. (1 - fst y, snd y)" have 1: "continuous_map (prod_topology ?I01 X) (prod_topology euclideanreal X) ?j" by (intro continuous_intros; simp add: continuous_map_subtopology_fst prod_topology_subtopology) have *: "continuous_map (prod_topology ?I01 X) (prod_topology ?I01 X) ?j" proof - have "continuous_map (prod_topology ?I01 X) (subtopology (prod_topology euclideanreal X) ({0..1} × topspace X)) ?j" by (simp add: continuous_map_into_subtopology [OF 1] image_subset_iff flip: image_subset_iff_funcset) then show ?thesis by (simp add: prod_topology_subtopology(1)) qed show ?thesis using assms apply (clarsimp simp: homotopic_with_def) subgoal for h by (rule_tac x="h ∘ (λy. (1 - fst y, snd y))" in exI) (simp add: continuous_map_compose [OF *]) done qed lemma homotopic_with_sym: "homotopic_with P X Y f g ⟷ homotopic_with P X Y g f" by (metis homotopic_with_symD) proposition homotopic_with_trans: assumes "homotopic_with P X Y f g" "homotopic_with P X Y g h" shows "homotopic_with P X Y f h" proof - let ?X01 = "prod_topology (subtopology euclideanreal {0..1}) X" obtain k1 k2 where contk1: "continuous_map ?X01 Y k1" and contk2: "continuous_map ?X01 Y k2" and k12: "∀x. k1 (1, x) = g x" "∀x. k2 (0, x) = g x" "∀x. k1 (0, x) = f x" "∀x. k2 (1, x) = h x" and P: "∀t∈{0..1}. P (λx. k1 (t, x))" "∀t∈{0..1}. P (λx. k2 (t, x))" using assms by (auto simp: homotopic_with_def) define k where "k ≡ λy. if fst y ≤ 1/2 then (k1 ∘ (λx. (2 *⇩_{R}fst x, snd x))) y else (k2 ∘ (λx. (2 *⇩_{R}fst x -1, snd x))) y" have keq: "k1 (2 * u, v) = k2 (2 * u -1, v)" if "u = 1/2" for u v by (simp add: k12 that) show ?thesis unfolding homotopic_with_def proof (intro exI conjI) show "continuous_map ?X01 Y k" unfolding k_def proof (rule continuous_map_cases_le) show fst: "continuous_map ?X01 euclideanreal fst" using continuous_map_fst continuous_map_in_subtopology by blast show "continuous_map ?X01 euclideanreal (λx. 1/2)" by simp show "continuous_map (subtopology ?X01 {y ∈ topspace ?X01. fst y ≤ 1/2}) Y (k1 ∘ (λx. (2 *⇩_{R}fst x, snd x)))" apply (intro fst continuous_map_compose [OF _ contk1] continuous_intros continuous_map_into_subtopology continuous_map_from_subtopology | simp)+ by (force simp: prod_topology_subtopology) show "continuous_map (subtopology ?X01 {y ∈ topspace ?X01. 1/2 ≤ fst y}) Y (k2 ∘ (λx. (2 *⇩_{R}fst x -1, snd x)))" apply (intro fst continuous_map_compose [OF _ contk2] continuous_intros continuous_map_into_subtopology continuous_map_from_subtopology | simp)+ by (force simp: prod_topology_subtopology) show "(k1 ∘ (λx. (2 *⇩_{R}fst x, snd x))) y = (k2 ∘ (λx. (2 *⇩_{R}fst x -1, snd x))) y" if "y ∈ topspace ?X01" and "fst y = 1/2" for y using that by (simp add: keq) qed show "∀x. k (0, x) = f x" by (simp add: k12 k_def) show "∀x. k (1, x) = h x" by (simp add: k12 k_def) show "∀t∈{0..1}. P (λx. k (t, x))" proof fix t show "t∈{0..1} ⟹ P (λx. k (t, x))" by (cases "t ≤ 1/2") (auto simp: k_def P) qed qed qed lemma homotopic_with_id2: "(⋀x. x ∈ topspace X ⟹ g (f x) = x) ⟹ homotopic_with (λx. True) X X (g ∘ f) id" by (metis comp_apply continuous_map_id eq_id_iff homotopic_with_equal homotopic_with_symD) subsection‹Continuity lemmas› lemma homotopic_with_compose_continuous_map_left: "⟦homotopic_with p X1 X2 f g; continuous_map X2 X3 h; ⋀j. p j ⟹ q(h ∘ j)⟧ ⟹ homotopic_with q X1 X3 (h ∘ f) (h ∘ g)" unfolding homotopic_with_def apply clarify subgoal for k by (rule_tac x="h ∘ k" in exI) (rule conjI continuous_map_compose | simp add: o_def)+ done lemma homotopic_with_compose_continuous_map_right: assumes hom: "homotopic_with p X2 X3 f g" and conth: "continuous_map X1 X2 h" and q: "⋀j. p j ⟹ q(j ∘ h)" shows "homotopic_with q X1 X3 (f ∘ h) (g ∘ h)" proof - obtain k where contk: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X2) X3 k" and k: "∀x. k (0, x) = f x" "∀x. k (1, x) = g x" and p: "⋀t. t∈{0..1} ⟹ p (λx. k (t, x))" using hom unfolding homotopic_with_def by blast have hsnd: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) X2 (h ∘ snd)" by (rule continuous_map_compose [OF continuous_map_snd conth]) let ?h = "k ∘ (λ(t,x). (t,h x))" show ?thesis unfolding homotopic_with_def proof (intro exI conjI allI ballI) have "continuous_map (prod_topology (top_of_set {0..1}) X1) (prod_topology (top_of_set {0..1::real}) X2) (λ(t, x). (t, h x))" by (metis (mono_tags, lifting) case_prod_beta' comp_def continuous_map_eq continuous_map_fst continuous_map_pairedI hsnd) then show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) X3 ?h" by (intro conjI continuous_map_compose [OF _ contk]) show "q (λx. ?h (t, x))" if "t ∈ {0..1}" for t using q [OF p [OF that]] by (simp add: o_def) qed (auto simp: k) qed corollary homotopic_compose: assumes "homotopic_with (λx. True) X Y f f'" "homotopic_with (λx. True) Y Z g g'" shows "homotopic_with (λx. True) X Z (g ∘ f) (g' ∘ f')" by (metis assms homotopic_with_compose_continuous_map_left homotopic_with_compose_continuous_map_right homotopic_with_imp_continuous_maps homotopic_with_trans) proposition homotopic_with_compose_continuous_right: "⟦homotopic_with_canon (λf. p (f ∘ h)) X Y f g; continuous_on W h; h ∈ W → X⟧ ⟹ homotopic_with_canon p W Y (f ∘ h) (g ∘ h)" by (simp add: homotopic_with_compose_continuous_map_right image_subset_iff_funcset) proposition homotopic_with_compose_continuous_left: "⟦homotopic_with_canon (λf. p (h ∘ f)) X Y f g; continuous_on Y h; h ∈ Y → Z⟧ ⟹ homotopic_with_canon p X Z (h ∘ f) (h ∘ g)" by (simp add: homotopic_with_compose_continuous_map_left image_subset_iff_funcset) lemma homotopic_from_subtopology: "homotopic_with P X X' f g ⟹ homotopic_with P (subtopology X S) X' f g" by (metis continuous_map_id_subt homotopic_with_compose_continuous_map_right o_id) lemma homotopic_on_emptyI: assumes "P f" "P g" shows "homotopic_with P trivial_topology X f g" by (metis assms continuous_map_on_empty empty_iff homotopic_with_equal topspace_discrete_topology) lemma homotopic_on_empty: "(homotopic_with P trivial_topology X f g ⟷ P f ∧ P g)" using homotopic_on_emptyI homotopic_with_imp_property by metis lemma homotopic_with_canon_on_empty: "homotopic_with_canon (λx. True) {} t f g" by (auto intro: homotopic_with_equal) lemma homotopic_constant_maps: "homotopic_with (λx. True) X X' (λx. a) (λx. b) ⟷ X = trivial_topology ∨ path_component_of X' a b" (is "?lhs = ?rhs") proof (cases "X = trivial_topology") case False then obtain c where c: "c ∈ topspace X" by fastforce have "∃g. continuous_map (top_of_set {0..1::real}) X' g ∧ g 0 = a ∧ g 1 = b" if "x ∈ topspace X" and hom: "homotopic_with (λx. True) X X' (λx. a) (λx. b)" for x proof - obtain h :: "real × 'a ⇒ 'b" where conth: "continuous_map (prod_topology (top_of_set {0..1}) X) X' h" and h: "⋀x. h (0, x) = a" "⋀x. h (1, x) = b" using hom by (auto simp: homotopic_with_def) have cont: "continuous_map (top_of_set {0..1}) X' (h ∘ (λt. (t, c)))" by (rule continuous_map_compose [OF _ conth] continuous_intros | simp add: c)+ then show ?thesis by (force simp: h) qed moreover have "homotopic_with (λx. True) X X' (λx. g 0) (λx. g 1)" if "x ∈ topspace X" "a = g 0" "b = g 1" "continuous_map (top_of_set {0..1}) X' g" for x and g :: "real ⇒ 'b" unfolding homotopic_with_def by (force intro!: continuous_map_compose continuous_intros c that) ultimately show ?thesis using False by (metis c path_component_of_set pathin_def) qed (simp add: homotopic_on_empty) proposition homotopic_with_eq: assumes h: "homotopic_with P X Y f g" and f': "⋀x. x ∈ topspace X ⟹ f' x = f x" and g': "⋀x. x ∈ topspace X ⟹ g' x = g x" and P: "(⋀h k. (⋀x. x ∈ topspace X ⟹ h x = k x) ⟹ P h ⟷ P k)" shows "homotopic_with P X Y f' g'" by (smt (verit, ccfv_SIG) assms homotopic_with) lemma homotopic_with_prod_topology: assumes "homotopic_with p X1 Y1 f f'" and "homotopic_with q X2 Y2 g g'" and r: "⋀i j. ⟦p i; q j⟧ ⟹ r(λ(x,y). (i x, j y))" shows "homotopic_with r (prod_topology X1 X2) (prod_topology Y1 Y2) (λz. (f(fst z),g(snd z))) (λz. (f'(fst z), g'(snd z)))" proof - obtain h where h: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) Y1 h" and h0: "⋀x. h (0, x) = f x" and h1: "⋀x. h (1, x) = f' x" and p: "⋀t. ⟦0 ≤ t; t ≤ 1⟧ ⟹ p (λx. h (t,x))" using assms unfolding homotopic_with_def by auto obtain k where k: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X2) Y2 k" and k0: "⋀x. k (0, x) = g x" and k1: "⋀x. k (1, x) = g' x" and q: "⋀t. ⟦0 ≤ t; t ≤ 1⟧ ⟹ q (λx. k (t,x))" using assms unfolding homotopic_with_def by auto let ?hk = "λ(t,x,y). (h(t,x), k(t,y))" show ?thesis unfolding homotopic_with_def proof (intro conjI allI exI) show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (prod_topology X1 X2)) (prod_topology Y1 Y2) ?hk" unfolding continuous_map_pairwise case_prod_unfold by (rule conjI continuous_map_pairedI continuous_intros continuous_map_id [unfolded id_def] continuous_map_fst_of [unfolded o_def] continuous_map_snd_of [unfolded o_def] continuous_map_compose [OF _ h, unfolded o_def] continuous_map_compose [OF _ k, unfolded o_def])+ next fix x show "?hk (0, x) = (f (fst x), g (snd x))" "?hk (1, x) = (f' (fst x), g' (snd x))" by (auto simp: case_prod_beta h0 k0 h1 k1) qed (auto simp: p q r) qed lemma homotopic_with_product_topology: assumes ht: "⋀i. i ∈ I ⟹ homotopic_with (p i) (X i) (Y i) (f i) (g i)" and pq: "⋀h. (⋀i. i ∈ I ⟹ p i (h i)) ⟹ q(λx. (λi∈I. h i (x i)))" shows "homotopic_with q (product_topology X I) (product_topology Y I) (λz. (λi∈I. (f i) (z i))) (λz. (λi∈I. (g i) (z i)))" proof - obtain h where h: "⋀i. i ∈ I ⟹ continuous_map (prod_topology (subtopology euclideanreal {0..1}) (X i)) (Y i) (h i)" and h0: "⋀i x. i ∈ I ⟹ h i (0, x) = f i x" and h1: "⋀i x. i ∈ I ⟹ h i (1, x) = g i x" and p: "⋀i t. ⟦i ∈ I; t ∈ {0..1}⟧ ⟹ p i (λx. h i (t,x))" using ht unfolding homotopic_with_def by metis show ?thesis unfolding homotopic_with_def proof (intro conjI allI exI) let ?h = "λ(t,z). λi∈I. h i (t,z i)" have "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (product_topology X I)) (Y i) (λx. h i (fst x, snd x i))" if "i ∈ I" for i proof - have §: "continuous_map (prod_topology (top_of_set {0..1}) (product_topology X I)) (X i) (λx. snd x i)" using continuous_map_componentwise continuous_map_snd that by fastforce show ?thesis unfolding continuous_map_pairwise case_prod_unfold by (intro conjI that § continuous_intros continuous_map_compose [OF _ h, unfolded o_def]) qed then show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (product_topology X I)) (product_topology Y I) ?h" by (auto simp: continuous_map_componentwise case_prod_beta) show "?h (0, x) = (λi∈I. f i (x i))" "?h (1, x) = (λi∈I. g i (x i))" for x by (auto simp: case_prod_beta h0 h1) show "∀t∈{0..1}. q (λx. ?h (t, x))" by (force intro: p pq) qed qed text‹Homotopic triviality implicitly incorporates path-connectedness.› lemma homotopic_triviality: shows "(∀f g. continuous_on S f ∧ f ∈ S → T ∧ continuous_on S g ∧ g ∈ S → T ⟶ homotopic_with_canon (λx. True) S T f g) ⟷ (S = {} ∨ path_connected T) ∧ (∀f. continuous_on S f ∧ f ∈ S → T ⟶ (∃c. homotopic_with_canon (λx. True) S T f (λx. c)))" (is "?lhs = ?rhs") proof (cases "S = {} ∨ T = {}") case True then show ?thesis by (auto simp: homotopic_on_emptyI simp flip: image_subset_iff_funcset) next case False show ?thesis proof assume LHS [rule_format]: ?lhs have pab: "path_component T a b" if "a ∈ T" "b ∈ T" for a b proof - have "homotopic_with_canon (λx. True) S T (λx. a) (λx. b)" by (simp add: LHS image_subset_iff that) then show ?thesis using False homotopic_constant_maps [of "top_of_set S" "top_of_set T" a b] by (metis path_component_of_canon_iff topspace_discrete_topology topspace_euclidean_subtopology) qed moreover have "∃c. homotopic_with_canon (λx. True) S T f (λx. c)" if "continuous_on S f" "f ∈ S → T" for f using False LHS continuous_on_const that by blast ultimately show ?rhs by (simp add: path_connected_component) next assume RHS: ?rhs with False have T: "path_connected T" by blast show ?lhs proof clarify fix f g assume "continuous_on S f" "f ∈ S → T" "continuous_on S g" "g ∈ S → T" obtain c d where c: "homotopic_with_canon (λx. True) S T f (λx. c)" and d: "homotopic_with_canon (λx. True) S T g (λx. d)" using RHS ‹continuous_on S f› ‹continuous_on S g› ‹f ∈ S → T› ‹g ∈ S → T› by presburger with T have "path_component T c d" by (metis False ex_in_conv homotopic_with_imp_subset2 image_subset_iff path_connected_component) then have "homotopic_with_canon (λx. True) S T (λx. c) (λx. d)" by (simp add: homotopic_constant_maps) with c d show "homotopic_with_canon (λx. True) S T f g" by (meson homotopic_with_symD homotopic_with_trans) qed qed qed subsection‹Homotopy of paths, maintaining the same endpoints› definition✐‹tag important› homotopic_paths :: "['a set, real ⇒ 'a, real ⇒ 'a::topological_space] ⇒ bool" where "homotopic_paths S p q ≡ homotopic_with_canon (λr. pathstart r = pathstart p ∧ pathfinish r = pathfinish p) {0..1} S p q" lemma homotopic_paths: "homotopic_paths S p q ⟷ (∃h. continuous_on ({0..1} × {0..1}) h ∧ h ∈ ({0..1} × {0..1}) → S ∧ (∀x ∈ {0..1}. h(0,x) = p x) ∧ (∀x ∈ {0..1}. h(1,x) = q x) ∧ (∀t ∈ {0..1::real}. pathstart(h ∘ Pair t) = pathstart p ∧ pathfinish(h ∘ Pair t) = pathfinish p))" by (auto simp: homotopic_paths_def homotopic_with pathstart_def pathfinish_def) proposition homotopic_paths_imp_pathstart: "homotopic_paths S p q ⟹ pathstart p = pathstart q" by (metis (mono_tags, lifting) homotopic_paths_def homotopic_with_imp_property) proposition homotopic_paths_imp_pathfinish: "homotopic_paths S p q ⟹ pathfinish p = pathfinish q" by (metis (mono_tags, lifting) homotopic_paths_def homotopic_with_imp_property) lemma homotopic_paths_imp_path: "homotopic_paths S p q ⟹ path p ∧ path q" using homotopic_paths_def homotopic_with_imp_continuous_maps path_def continuous_map_subtopology_eu by blast lemma homotopic_paths_imp_subset: "homotopic_paths S p q ⟹ path_image p ⊆ S ∧ path_image q ⊆ S" by (metis (mono_tags) continuous_map_subtopology_eu homotopic_paths_def homotopic_with_imp_continuous_maps path_image_def) proposition homotopic_paths_refl [simp]: "homotopic_paths S p p ⟷ path p ∧ path_image p ⊆ S" by (simp add: homotopic_paths_def path_def path_image_def) proposition homotopic_paths_sym: "homotopic_paths S p q ⟹ homotopic_paths S q p" by (metis (mono_tags) homotopic_paths_def homotopic_paths_imp_pathfinish homotopic_paths_imp_pathstart homotopic_with_symD) proposition homotopic_paths_sym_eq: "homotopic_paths S p q ⟷ homotopic_paths S q p" by (metis homotopic_paths_sym) proposition homotopic_paths_trans [trans]: assumes "homotopic_paths S p q" "homotopic_paths S q r" shows "homotopic_paths S p r" using assms homotopic_paths_imp_pathfinish homotopic_paths_imp_pathstart unfolding homotopic_paths_def by (smt (verit, ccfv_SIG) homotopic_with_mono homotopic_with_trans) proposition homotopic_paths_eq: "⟦path p; path_image p ⊆ S; ⋀t. t ∈ {0..1} ⟹ p t = q t⟧ ⟹ homotopic_paths S p q" by (smt (verit, best) homotopic_paths homotopic_paths_refl) proposition homotopic_paths_reparametrize: assumes "path p" and pips: "path_image p ⊆ S" and contf: "continuous_on {0..1} f" and f01 :"f ∈ {0..1} → {0..1}" and [simp]: "f(0) = 0" "f(1) = 1" and q: "⋀t. t ∈ {0..1} ⟹ q(t) = p(f t)" shows "homotopic_paths S p q" proof - have contp: "continuous_on {0..1} p" by (metis ‹path p› path_def) then have "continuous_on {0..1} (p ∘ f)" by (meson assms(4) contf continuous_on_compose continuous_on_subset image_subset_iff_funcset) then have "path q" by (simp add: path_def) (metis q continuous_on_cong) have piqs: "path_image q ⊆ S" by (smt (verit, ccfv_threshold) Pi_iff assms(2) assms(4) assms(7) image_subset_iff path_defs(4)) have fb0: "⋀a b. ⟦0 ≤ a; a ≤ 1; 0 ≤ b; b ≤ 1⟧ ⟹ 0 ≤ (1 - a) * f b + a * b" using f01 by force have fb1: "⟦0 ≤ a; a ≤ 1; 0 ≤ b; b ≤ 1⟧ ⟹ (1 - a) * f b + a * b ≤ 1" for a b by (intro convex_bound_le) (use f01 in auto) have "homotopic_paths S q p" proof (rule homotopic_paths_trans) show "homotopic_paths S q (p ∘ f)" using q by (force intro: homotopic_paths_eq [OF ‹path q› piqs]) next show "homotopic_paths S (p ∘ f) p" using pips [unfolded path_image_def] apply (simp add: homotopic_paths_def homotopic_with_def) apply (rule_tac x="p ∘ (λy. (1 - (fst y)) *⇩_{R}((f ∘ snd) y) + (fst y) *⇩_{R}snd y)" in exI) apply (rule conjI contf continuous_intros continuous_on_subset [OF contp] | simp)+ by (auto simp: fb0 fb1 pathstart_def pathfinish_def) qed then show ?thesis by (simp add: homotopic_paths_sym) qed lemma homotopic_paths_subset: "⟦homotopic_paths S p q; S ⊆ t⟧ ⟹ homotopic_paths t p q" unfolding homotopic_paths by fast text‹ A slightly ad-hoc but useful lemma in constructing homotopies.› lemma continuous_on_homotopic_join_lemma: fixes q :: "[real,real] ⇒ 'a::topological_space" assumes p: "continuous_on ({0..1} × {0..1}) (λy. p (fst y) (snd y))" (is "continuous_on ?A ?p") and q: "continuous_on ({0..1} × {0..1}) (λy. q (fst y) (snd y))" (is "continuous_on ?A ?q") and pf: "⋀t. t ∈ {0..1} ⟹ pathfinish(p t) = pathstart(q t)" shows "continuous_on ({0..1} × {0..1}) (λy. (p(fst y) +++ q(fst y)) (snd y))" proof - have §: "(λt. p (fst t) (2 * snd t)) = ?p ∘ (λy. (fst y, 2 * snd y))" "(λt. q (fst t) (2 * snd t - 1)) = ?q ∘ (λy. (fst y, 2 * snd y - 1))" by force+ show ?thesis unfolding joinpaths_def proof (rule continuous_on_cases_le) show "continuous_on {y ∈ ?A. snd y ≤ 1/2} (λt. p (fst t) (2 * snd t))" "continuous_on {y ∈ ?A. 1/2 ≤ snd y} (λt. q (fst t) (2 * snd t - 1))" "continuous_on ?A snd" unfolding § by (rule continuous_intros continuous_on_subset [OF p] continuous_on_subset [OF q] | force)+ qed (use pf in ‹auto simp: mult.commute pathstart_def pathfinish_def›) qed text‹ Congruence properties of homotopy w.r.t. path-combining operations.› lemma homotopic_paths_reversepath_D: assumes "homotopic_paths S p q" shows "homotopic_paths S (reversepath p) (reversepath q)" using assms apply (simp add: homotopic_paths_def homotopic_with_def, clarify) apply (rule_tac x="h ∘ (λx. (fst x, 1 - snd x))" in exI) apply (rule conjI continuous_intros)+ apply (auto simp: reversepath_def pathstart_def pathfinish_def elim!: continuous_on_subset) done proposition homotopic_paths_reversepath: "homotopic_paths S (reversepath p) (reversepath q) ⟷ homotopic_paths S p q" using homotopic_paths_reversepath_D by force proposition homotopic_paths_join: "⟦homotopic_paths S p p'; homotopic_paths S q q'; pathfinish p = pathstart q⟧ ⟹ homotopic_paths S (p +++ q) (p' +++ q')" apply (clarsimp simp: homotopic_paths_def homotopic_with_def) apply (rename_tac k1 k2) apply (rule_tac x="(λy. ((k1 ∘ Pair (fst y)) +++ (k2 ∘ Pair (fst y))) (snd y))" in exI) apply (intro conjI continuous_intros continuous_on_homotopic_join_lemma; force simp: joinpaths_def pathstart_def pathfinish_def path_image_def) done proposition homotopic_paths_continuous_image: "⟦homotopic_paths S f g; continuous_on S h; h ∈ S → t⟧ ⟹ homotopic_paths t (h ∘ f) (h ∘ g)" unfolding homotopic_paths_def by (simp add: homotopic_with_compose_continuous_map_left pathfinish_compose pathstart_compose image_subset_iff_funcset) subsection‹Group properties for homotopy of paths› text✐‹tag important›‹So taking equivalence classes under homotopy would give the fundamental group› proposition homotopic_paths_rid: assumes "path p" "path_image p ⊆ S" shows "homotopic_paths S (p +++ linepath (pathfinish p) (pathfinish p)) p" proof - have §: "continuous_on {0..1} (λt::real. if t ≤ 1/2 then 2 *⇩_{R}t else 1)" unfolding split_01 by (rule continuous_on_cases continuous_intros | force simp: pathfinish_def joinpaths_def)+ show ?thesis apply (rule homotopic_paths_sym) using assms unfolding pathfinish_def joinpaths_def by (intro § continuous_on_cases continuous_intros homotopic_paths_reparametrize [where f = "λt. if t ≤ 1/2 then 2 *⇩_{R}t else 1"]; force) qed proposition homotopic_paths_lid: "⟦path p; path_image p ⊆ S⟧ ⟹ homotopic_paths S (linepath (pathstart p) (pathstart p) +++ p) p" using homotopic_paths_rid [of "reversepath p" S] by (metis homotopic_paths_reversepath path_image_reversepath path_reversepath pathfinish_linepath pathfinish_reversepath reversepath_joinpaths reversepath_linepath) proposition homotopic_paths_assoc: "⟦path p; path_image p ⊆ S; path q; path_image q ⊆ S; path r; path_image r ⊆ S; pathfinish p = pathstart q; pathfinish q = pathstart r⟧ ⟹ homotopic_paths S (p +++ (q +++ r)) ((p +++ q) +++ r)" apply (subst homotopic_paths_sym) apply (rule homotopic_paths_reparametrize [where f = "λt. if t ≤ 1/2 then inverse 2 *⇩_{R}t else if t ≤ 3 / 4 then t - (1 / 4) else 2 *⇩_{R}t - 1"]) apply (simp_all del: le_divide_eq_numeral1 add: subset_path_image_join) apply (rule continuous_on_cases_1 continuous_intros | auto simp: joinpaths_def)+ done proposition homotopic_paths_rinv: assumes "path p" "path_image p ⊆ S" shows "homotopic_paths S (p +++ reversepath p) (linepath (pathstart p) (pathstart p))" proof - have p: "continuous_on {0..1} p" using assms by (auto simp: path_def) let ?A = "{0..1} × {0..1}" have "continuous_on ?A (λx. (subpath 0 (fst x) p +++ reversepath (subpath 0 (fst x) p)) (snd x))" unfolding joinpaths_def subpath_def reversepath_def path_def add_0_right diff_0_right proof (rule continuous_on_cases_le) show "continuous_on {x ∈ ?A. snd x ≤ 1/2} (λt. p (fst t * (2 * snd t)))" "continuous_on {x ∈ ?A. 1/2 ≤ snd x} (λt. p (fst t * (1 - (2 * snd t - 1))))" "continuous_on ?A snd" by (intro continuous_on_compose2 [OF p] continuous_intros; auto simp: mult_le_one)+ qed (auto simp: algebra_simps) then show ?thesis using assms apply (subst homotopic_paths_sym_eq) unfolding homotopic_paths_def homotopic_with_def apply (rule_tac x="(λy. (subpath 0 (fst y) p +++ reversepath(subpath 0 (fst y) p)) (snd y))" in exI) apply (force simp: mult_le_one path_defs joinpaths_def subpath_def reversepath_def) done qed proposition homotopic_paths_linv: assumes "path p" "path_image p ⊆ S" shows "homotopic_paths S (reversepath p +++ p) (linepath (pathfinish p) (pathfinish p))" using homotopic_paths_rinv [of "reversepath p" S] assms by simp subsection‹Homotopy of loops without requiring preservation of endpoints› definition✐‹tag important› homotopic_loops :: "'a::topological_space set ⇒ (real ⇒ 'a) ⇒ (real ⇒ 'a) ⇒ bool" where "homotopic_loops S p q ≡ homotopic_with_canon (λr. pathfinish r = pathstart r) {0..1} S p q" lemma homotopic_loops: "homotopic_loops S p q ⟷ (∃h. continuous_on ({0..1::real} × {0..1}) h ∧ image h ({0..1} × {0..1}) ⊆ S ∧ (∀x ∈ {0..1}. h(0,x) = p x) ∧ (∀x ∈ {0..1}. h(1,x) = q x) ∧ (∀t ∈ {0..1}. pathfinish(h ∘ Pair t) = pathstart(h ∘ Pair t)))" by (simp add: homotopic_loops_def pathstart_def pathfinish_def homotopic_with) proposition homotopic_loops_imp_loop: "homotopic_loops S p q ⟹ pathfinish p = pathstart p ∧ pathfinish q = pathstart q" using homotopic_with_imp_property homotopic_loops_def by blast proposition homotopic_loops_imp_path: "homotopic_loops S p q ⟹ path p ∧ path q" unfolding homotopic_loops_def path_def using homotopic_with_imp_continuous_maps continuous_map_subtopology_eu by blast proposition homotopic_loops_imp_subset: "homotopic_loops S p q ⟹ path_image p ⊆ S ∧ path_image q ⊆ S" unfolding homotopic_loops_def path_image_def by (meson continuous_map_subtopology_eu homotopic_with_imp_continuous_maps) proposition homotopic_loops_refl: "homotopic_loops S p p ⟷ path p ∧ path_image p ⊆ S ∧ pathfinish p = pathstart p" by (simp add: homotopic_loops_def path_image_def path_def) proposition homotopic_loops_sym: "homotopic_loops S p q ⟹ homotopic_loops S q p" by (simp add: homotopic_loops_def homotopic_with_sym) proposition homotopic_loops_sym_eq: "homotopic_loops S p q ⟷ homotopic_loops S q p" by (metis homotopic_loops_sym) proposition homotopic_loops_trans: "⟦homotopic_loops S p q; homotopic_loops S q r⟧ ⟹ homotopic_loops S p r" unfolding homotopic_loops_def by (blast intro: homotopic_with_trans) proposition homotopic_loops_subset: "⟦homotopic_loops S p q; S ⊆ t⟧ ⟹ homotopic_loops t p q" by (fastforce simp: homotopic_loops) proposition homotopic_loops_eq: "⟦path p; path_image p ⊆ S; pathfinish p = pathstart p; ⋀t. t ∈ {0..1} ⟹ p(t) = q(t)⟧ ⟹ homotopic_loops S p q" unfolding homotopic_loops_def path_image_def path_def pathstart_def pathfinish_def by (auto intro: homotopic_with_eq [OF homotopic_with_refl [where f = p, THEN iffD2]]) proposition homotopic_loops_continuous_image: "⟦homotopic_loops S f g; continuous_on S h; h ∈ S → t⟧ ⟹ homotopic_loops t (h ∘ f) (h ∘ g)" unfolding homotopic_loops_def by (simp add: homotopic_with_compose_continuous_map_left pathfinish_def pathstart_def image_subset_iff_funcset) subsection‹Relations between the two variants of homotopy› proposition homotopic_paths_imp_homotopic_loops: "⟦homotopic_paths S p q; pathfinish p = pathstart p; pathfinish q = pathstart p⟧ ⟹ homotopic_loops S p q" by (auto simp: homotopic_with_def homotopic_paths_def homotopic_loops_def) proposition homotopic_loops_imp_homotopic_paths_null: assumes "homotopic_loops S p (linepath a a)" shows "homotopic_paths S p (linepath (pathstart p) (pathstart p))" proof - have "path p" by (metis assms homotopic_loops_imp_path) have ploop: "pathfinish p = pathstart p" by (metis assms homotopic_loops_imp_loop) have pip: "path_image p ⊆ S" by (metis assms homotopic_loops_imp_subset) let ?A = "{0..1::real} × {0..1::real}" obtain h where conth: "continuous_on ?A h" and hs: "h ∈ ?A → S" and h0[simp]: "⋀x. x ∈ {0..1} ⟹ h(0,x) = p x" and h1[simp]: "⋀x. x ∈ {0..1} ⟹ h(1,x) = a" and ends: "⋀t. t ∈ {0..1} ⟹ pathfinish (h ∘ Pair t) = pathstart (h ∘ Pair t)" using assms by (auto simp: homotopic_loops homotopic_with image_subset_iff_funcset) have conth0: "path (λu. h (u, 0))" unfolding path_def proof (rule continuous_on_compose [of _ _ h, unfolded o_def]) show "continuous_on ((λx. (x, 0)) ` {0..1}) h" by (force intro: continuous_on_subset [OF conth]) qed (force intro: continuous_intros) have pih0: "path_image (λu. h (u, 0)) ⊆ S" using hs by (force simp: path_image_def) have c1: "continuous_on ?A (λx. h (fst x * snd x, 0))" proof (rule continuous_on_compose [of _ _ h, unfolded o_def]) show "continuous_on ((λx. (fst x * snd x, 0)) ` ?A) h" by (force simp: mult_le_one intro: continuous_on_subset [OF conth]) qed (force intro: continuous_intros)+ have c2: "continuous_on ?A (λx. h (fst x - fst x * snd x, 0))" proof (rule continuous_on_compose [of _ _ h, unfolded o_def]) show "continuous_on ((λx. (fst x - fst x * snd x, 0)) ` ?A) h" by (auto simp: algebra_simps add_increasing2 mult_left_le intro: continuous_on_subset [OF conth]) qed (force intro: continuous_intros) have [simp]: "⋀t. ⟦0 ≤ t ∧ t ≤ 1⟧ ⟹ h (t, 1) = h (t, 0)" using ends by (simp add: pathfinish_def pathstart_def) have adhoc_le: "c * 4 ≤ 1 + c * (d * 4)" if "¬ d * 4 ≤ 3" "0 ≤ c" "c ≤ 1" for c d::real proof - have "c * 3 ≤ c * (d * 4)" using that less_eq_real_def by auto with ‹c ≤ 1› show ?thesis by fastforce qed have *: "⋀p x. ⟦path p ∧ path(reversepath p); path_image p ⊆ S ∧ path_image(reversepath p) ⊆ S; pathfinish p = pathstart(linepath a a +++ reversepath p) ∧ pathstart(reversepath p) = a ∧ pathstart p = x⟧ ⟹ homotopic_paths S (p +++ linepath a a +++ reversepath p) (linepath x x)" by (metis homotopic_paths_lid homotopic_paths_join homotopic_paths_trans homotopic_paths_sym homotopic_paths_rinv) have 1: "homotopic_paths S p (p +++ linepath (pathfinish p) (pathfinish p))" using ‹path p› homotopic_paths_rid homotopic_paths_sym pip by blast moreover have "homotopic_paths S (p +++ linepath (pathfinish p) (pathfinish p)) (linepath (pathstart p) (pathstart p) +++ p +++ linepath (pathfinish p) (pathfinish p))" using homotopic_paths_lid [of "p +++ linepath (pathfinish p) (pathfinish p)" S] by (metis 1 homotopic_paths_imp_path homotopic_paths_imp_subset homotopic_paths_sym pathstart_join) moreover have "homotopic_paths S (linepath (pathstart p) (pathstart p) +++ p +++ linepath (pathfinish p) (pathfinish p)) ((λu. h (u, 0)) +++ linepath a a +++ reversepath (λu. h (u, 0)))" unfolding homotopic_paths_def homotopic_with_def proof (intro exI strip conjI) let ?h = "λy. (subpath 0 (fst y) (λu. h (u, 0)) +++ (λu. h (Pair (fst y) u)) +++ subpath (fst y) 0 (λu. h (u, 0))) (snd y)" have "continuous_on ?A ?h" by (intro continuous_on_homotopic_join_lemma; simp add: path_defs joinpaths_def subpath_def conth c1 c2) moreover have "?h ∈ ?A → S" using hs unfolding joinpaths_def subpath_def by (force simp: algebra_simps mult_le_one mult_left_le intro: adhoc_le) ultimately show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1})) (top_of_set S) ?h" by (simp add: subpath_reversepath image_subset_iff_funcset) qed (use ploop in ‹simp_all add: reversepath_def path_defs joinpaths_def o_def subpath_def conth c1 c2›) moreover have "homotopic_paths S ((λu. h (u, 0)) +++ linepath a a +++ reversepath (λu. h (u, 0))) (linepath (pathstart p) (pathstart p))" by (rule *; simp add: pih0 pathstart_def pathfinish_def conth0; simp add: reversepath_def joinpaths_def) ultimately show ?thesis by (blast intro: homotopic_paths_trans) qed proposition homotopic_loops_conjugate: fixes S :: "'a::real_normed_vector set" assumes "path p" "path q" and pip: "path_image p ⊆ S" and piq: "path_image q ⊆ S" and pq: "pathfinish p = pathstart q" and qloop: "pathfinish q = pathstart q" shows "homotopic_loops S (p +++ q +++ reversepath p) q" proof - have contp: "continuous_on {0..1} p" using ‹path p› [unfolded path_def] by blast have contq: "continuous_on {0..1} q" using ‹path q› [unfolded path_def] by blast let ?A = "{0..1::real} × {0..1::real}" have c1: "continuous_on ?A (λx. p ((1 - fst x) * snd x + fst x))" proof (rule continuous_on_compose [of _ _ p, unfolded o_def]) show "continuous_on ((λx. (1 - fst x) * snd x + fst x) ` ?A) p" by (auto intro: continuous_on_subset [OF contp] simp: algebra_simps add_increasing2 mult_right_le_one_le sum_le_prod1) qed (force intro: continuous_intros) have c2: "continuous_on ?A (λx. p ((fst x - 1) * snd x + 1))" proof (rule continuous_on_compose [of _ _ p, unfolded o_def]) show "continuous_on ((λx. (fst x - 1) * snd x + 1) ` ?A) p" by (auto intro: continuous_on_subset [OF contp] simp: algebra_simps add_increasing2 mult_left_le_one_le) qed (force intro: continuous_intros) have ps1: "⋀a b. ⟦b * 2 ≤ 1; 0 ≤ b; 0 ≤ a; a ≤ 1⟧ ⟹ p ((1 - a) * (2 * b) + a) ∈ S" using sum_le_prod1 by (force simp: algebra_simps add_increasing2 mult_left_le intro: pip [unfolded path_image_def, THEN subsetD]) have ps2: "⋀a b. ⟦¬ 4 * b ≤ 3; b ≤ 1; 0 ≤ a; a ≤ 1⟧ ⟹ p ((a - 1) * (4 * b - 3) + 1) ∈ S" apply (rule pip [unfolded path_image_def, THEN subsetD]) apply (rule image_eqI, blast) apply (simp add: algebra_simps) by (metis add_mono affine_ineq linear mult.commute mult.left_neutral mult_right_mono add.commute zero_le_numeral) have qs: "⋀a b. ⟦4 * b ≤ 3; ¬ b * 2 ≤ 1⟧ ⟹ q (4 * b - 2) ∈ S" using path_image_def piq by fastforce have "homotopic_loops S (p +++ q +++ reversepath p) (linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q))" unfolding homotopic_loops_def homotopic_with_def proof (intro exI strip conjI) let ?h = "(λy. (subpath (fst y) 1 p +++ q +++ subpath 1 (fst y) p) (snd y))" have "continuous_on ?A (λy. q (snd y))" by (force simp: contq intro: continuous_on_compose [of _ _ q, unfolded o_def] continuous_on_id continuous_on_snd) then have "continuous_on ?A ?h" using pq qloop by (intro continuous_on_homotopic_join_lemma) (auto simp: path_defs joinpaths_def subpath_def c1 c2) then show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1})) (top_of_set S) ?h" by (auto simp: joinpaths_def subpath_def ps1 ps2 qs) show "?h (1,x) = (linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q)) x" for x using pq by (simp add: pathfinish_def subpath_refl) qed (auto simp: subpath_reversepath) moreover have "homotopic_loops S (linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q)) q" proof - have "homotopic_paths S (linepath (pathfinish q) (pathfinish q) +++ q) q" using ‹path q› homotopic_paths_lid qloop piq by auto hence 1: "⋀f. homotopic_paths S f q ∨ ¬ homotopic_paths S f (linepath (pathfinish q) (pathfinish q) +++ q)" using homotopic_paths_trans by blast hence "homotopic_paths S (linepath (pathfinish q) (pathfinish q) +++ q +++ linepath (pathfinish q) (pathfinish q)) q" by (smt (verit, best) ‹path q› homotopic_paths_imp_path homotopic_paths_imp_subset homotopic_paths_lid homotopic_paths_rid homotopic_paths_trans pathstart_join piq qloop) thus ?thesis by (metis (no_types) qloop homotopic_loops_sym homotopic_paths_imp_homotopic_loops homotopic_paths_imp_pathfinish homotopic_paths_sym) qed ultimately show ?thesis by (blast intro: homotopic_loops_trans) qed lemma homotopic_paths_loop_parts: assumes loops: "homotopic_loops S (p +++ reversepath q) (linepath a a)" and "path q" shows "homotopic_paths S p q" proof - have paths: "homotopic_paths S (p +++ reversepath q) (linepath (pathstart p) (pathstart p))" using homotopic_loops_imp_homotopic_paths_null [OF loops] by simp then have "path p" using ‹path q› homotopic_loops_imp_path loops path_join path_join_path_ends path_reversepath by blast show ?thesis proof (cases "pathfinish p = pathfinish q") case True obtain pipq: "path_image p ⊆ S" "path_image q ⊆ S" by (metis Un_subset_iff paths ‹path p› ‹path q› homotopic_loops_imp_subset homotopic_paths_imp_path loops path_image_join path_image_reversepath path_imp_reversepath path_join_eq) have "homotopic_paths S p (p +++ (linepath (pathfinish p) (pathfinish p)))" using ‹path p› ‹path_image p ⊆ S› homotopic_paths_rid homotopic_paths_sym by blast moreover have "homotopic_paths S (p +++ (linepath (pathfinish p) (pathfinish p))) (p +++ (reversepath q +++ q))" by (simp add: True ‹path p› ‹path q› pipq homotopic_paths_join homotopic_paths_linv homotopic_paths_sym) moreover have "homotopic_paths S (p +++ (reversepath q +++ q)) ((p +++ reversepath q) +++ q)" by (simp add: True ‹path p› ‹path q› homotopic_paths_assoc pipq) moreover have "homotopic_paths S ((p +++ reversepath q) +++ q) (linepath (pathstart p) (pathstart p) +++ q)" by (simp add: ‹path q› homotopic_paths_join paths pipq) ultimately show ?thesis by (metis ‹path q› homotopic_paths_imp_path homotopic_paths_lid homotopic_paths_trans path_join_path_ends pathfinish_linepath pipq(2)) next case False then show ?thesis using ‹path q› homotopic_loops_imp_path loops path_join_path_ends by fastforce qed qed subsection✐‹tag unimportant›‹Homotopy of "nearby" function, paths and loops› lemma homotopic_with_linear: fixes f g :: "_ ⇒ 'b::real_normed_vector" assumes contf: "continuous_on S f" and contg:"continuous_on S g" and sub: "⋀x. x ∈ S ⟹ closed_segment (f x) (g x) ⊆ t" shows "homotopic_with_canon (λz. True) S t f g" unfolding homotopic_with_def apply (rule_tac x="λy. ((1 - (fst y)) *⇩_{R}f(snd y) + (fst y) *⇩_{R}g(snd y))" in exI) using sub closed_segment_def by (fastforce intro: continuous_intros continuous_on_subset [OF contf] continuous_on_compose2 [where g=f] continuous_on_subset [OF contg] continuous_on_compose2 [where g=g]) lemma homotopic_paths_linear: fixes g h :: "real ⇒ 'a::real_normed_vector" assumes "path g" "path h" "pathstart h = pathstart g" "pathfinish h = pathfinish g" "⋀t. t ∈ {0..1} ⟹ closed_segment (g t) (h t) ⊆ S" shows "homotopic_paths S g h" using assms unfolding path_def apply (simp add: closed_segment_def pathstart_def pathfinish_def homotopic_paths_def homotopic_with_def) apply (rule_tac x="λy. ((1 - (fst y)) *⇩_{R}(g ∘ snd) y + (fst y) *⇩_{R}(h ∘ snd) y)" in exI) apply (intro conjI subsetI continuous_intros; force) done lemma homotopic_loops_linear: fixes g h :: "real ⇒ 'a::real_normed_vector" assumes "path g" "path h" "pathfinish g = pathstart g" "pathfinish h = pathstart h" "⋀t x. t ∈ {0..1} ⟹ closed_segment (g t) (h t) ⊆ S" shows "homotopic_loops S g h" using assms unfolding path_defs homotopic_loops_def homotopic_with_def apply (rule_tac x="λy. ((1 - (fst y)) *⇩_{R}g(snd y) + (fst y) *⇩_{R}h(snd y))" in exI) by (force simp: closed_segment_def intro!: continuous_intros intro: continuous_on_compose2 [where g=g] continuous_on_compose2 [where g=h]) lemma homotopic_paths_nearby_explicit: assumes §: "path g" "path h" "pathstart h = pathstart g" "pathfinish h = pathfinish g" and no: "⋀t x. ⟦t ∈ {0..1}; x ∉ S⟧ ⟹ norm(h t - g t) < norm(g t - x)" shows "homotopic_paths S g h" using homotopic_paths_linear [OF §] by (metis linorder_not_le no norm_minus_commute segment_bound1 subsetI) lemma homotopic_loops_nearby_explicit: assumes §: "path g" "path h" "pathfinish g = pathstart g" "pathfinish h = pathstart h" and no: "⋀t x. ⟦t ∈ {0..1}; x ∉ S⟧ ⟹ norm(h t - g t) < norm(g t - x)" shows "homotopic_loops S g h" using homotopic_loops_linear [OF §] by (metis linorder_not_le no norm_minus_commute segment_bound1 subsetI) lemma homotopic_nearby_paths: fixes g h :: "real ⇒ 'a::euclidean_space" assumes "path g" "open S" "path_image g ⊆ S" shows "∃e. 0 < e ∧ (∀h. path h ∧ pathstart h = pathstart g ∧ pathfinish h = pathfinish g ∧ (∀t ∈ {0..1}. norm(h t - g t) < e) ⟶ homotopic_paths S g h)" proof - obtain e where "e > 0" and e: "⋀x y. x ∈ path_image g ⟹ y ∈ - S ⟹ e ≤ dist x y" using separate_compact_closed [of "path_image g" "-S"] assms by force show ?thesis using e [unfolded dist_norm] ‹e > 0› by (fastforce simp: path_image_def intro!: homotopic_paths_nearby_explicit assms exI) qed lemma homotopic_nearby_loops: fixes g h :: "real ⇒ 'a::euclidean_space" assumes "path g" "open S" "path_image g ⊆ S" "pathfinish g = pathstart g" shows "∃e. 0 < e ∧ (∀h. path h ∧ pathfinish h = pathstart h ∧ (∀t ∈ {0..1}. norm(h t - g t) < e) ⟶ homotopic_loops S g h)" proof - obtain e where "e > 0" and e: "⋀x y. x ∈ path_image g ⟹ y ∈ - S ⟹ e ≤ dist x y" using separate_compact_closed [of "path_image g" "-S"] assms by force show ?thesis using e [unfolded dist_norm] ‹e > 0› by (fastforce simp: path_image_def intro!: homotopic_loops_nearby_explicit assms exI) qed subsection‹ Homotopy and subpaths› lemma homotopic_join_subpaths1: assumes "path g" and pag: "path_image g ⊆ S" and u: "u ∈ {0..1}" and v: "v ∈ {0..1}" and w: "w ∈ {0..1}" "u ≤ v" "v ≤ w" shows "homotopic_paths S (subpath u v g +++ subpath v w g) (subpath u w g)" proof - have 1: "t * 2 ≤ 1 ⟹ u + t * (v * 2) ≤ v + t * (u * 2)" for t using affine_ineq ‹u ≤ v› by fastforce have 2: "t * 2 > 1 ⟹ u + (2*t - 1) * v ≤ v + (2*t - 1) * w" for t by (metis add_mono_thms_linordered_semiring(1) diff_gt_0_iff_gt less_eq_real_def mult.commute mult_right_mono ‹u ≤ v› ‹v ≤ w›) have t2: "⋀t::real. t*2 = 1 ⟹ t = 1/2" by auto have "homotopic_paths (path_image g) (subpath u v g +++ subpath v w g) (subpath u w g)" proof (cases "w = u") case True then show ?thesis by (metis ‹path g› homotopic_paths_rinv path_image_subpath_subset path_subpath pathstart_subpath reversepath_subpath subpath_refl u v) next case False let ?f = "λt. if t ≤ 1/2 then inverse((w - u)) *⇩_{R}(2 * (v - u)) *⇩_{R}t else inverse((w - u)) *⇩_{R}((v - u) + (w - v) *⇩_{R}(2 *⇩_{R}t - 1))" show ?thesis proof (rule homotopic_paths_sym [OF homotopic_paths_reparametrize [where f = ?f]]) show "path (subpath u w g)" using assms(1) path_subpath u w(1) by blast show "path_image (subpath u w g) ⊆ path_image g" by (meson path_image_subpath_subset u w(1)) show "continuous_on {0..1} ?f" unfolding split_01 by (rule continuous_on_cases continuous_intros | force simp: pathfinish_def joinpaths_def dest!: t2)+ show "?f ∈ {0..1} → {0..1}" using False assms by (force simp: field_simps not_le mult_left_mono affine_ineq dest!: 1 2) show "(subpath u v g +++ subpath v w g) t = subpath u w g (?f t)" if "t ∈ {0..1}" for t using assms unfolding joinpaths_def subpath_def by (auto simp: divide_simps add.commute mult.commute mult.left_commute) qed (use False in auto) qed then show ?thesis by (rule homotopic_paths_subset [OF _ pag]) qed lemma homotopic_join_subpaths2: assumes "homotopic_paths S (subpath u v g +++ subpath v w g) (subpath u w g)" shows "homotopic_paths S (subpath w v g +++ subpath v u g) (subpath w u g)" by (metis assms homotopic_paths_reversepath_D pathfinish_subpath pathstart_subpath reversepath_joinpaths reversepath_subpath) lemma homotopic_join_subpaths3: assumes hom: "homotopic_paths S (subpath u v g +++ subpath v w g) (subpath u w g)" and "path g" and pag: "path_image g ⊆ S" and u: "u ∈ {0..1}" and v: "v ∈ {0..1}" and w: "w ∈ {0..1}" shows "homotopic_paths S (subpath v w g +++ subpath w u g) (subpath v u g)" proof - obtain wvg: "path (subpath w v g)" "path_image (subpath w v g) ⊆ S" and wug: "path (subpath w u g)" "path_image (subpath w u g) ⊆ S" and vug: "path (subpath v u g)" "path_image (subpath v u g) ⊆ S" by (meson ‹path g› pag path_image_subpath_subset path_subpath subset_trans u v w) have "homotopic_paths S (subpath u w g +++ subpath w v g) ((subpath u v g +++ subpath v w g) +++ subpath w v g)" by (simp add: hom homotopic_paths_join homotopic_paths_sym wvg) also have "homotopic_paths S … (subpath u v g +++ subpath v w g +++ subpath w v g)" using wvg vug ‹path g› by (metis homotopic_paths_assoc homotopic_paths_sym path_image_subpath_commute path_subpath pathfinish_subpath pathstart_subpath u v w) also have "homotopic_paths S … (subpath u v g +++ linepath (pathfinish (subpath u v g)) (pathfinish (subpath u v g)))" using wvg vug ‹path g› by (metis homotopic_paths_join homotopic_paths_linv homotopic_paths_refl path_image_subpath_commute path_subpath pathfinish_subpath pathstart_join pathstart_subpath reversepath_subpath u v) also have "homotopic_paths S … (subpath u v g)" using vug ‹path g› by (metis homotopic_paths_rid path_image_subpath_commute path_subpath u v) finally have "homotopic_paths S (subpath u w g +++ subpath w v g) (subpath u v g)" . then show ?thesis using homotopic_join_subpaths2 by blast qed proposition homotopic_join_subpaths: "⟦path g; path_image g ⊆ S; u ∈ {0..1}; v ∈ {0..1}; w ∈ {0..1}⟧ ⟹ homotopic_paths S (subpath u v g +++ subpath v w g) (subpath u w g)" by (smt (verit, del_insts) homotopic_join_subpaths1 homotopic_join_subpaths2 homotopic_join_subpaths3) text‹Relating homotopy of trivial loops to path-connectedness.› lemma path_component_imp_homotopic_points: assumes "path_component S a b" shows "homotopic_loops S (linepath a a) (linepath b b)" proof - obtain g :: "real ⇒ 'a" where g: "continuous_on {0..1} g" "g ∈ {0..1} → S" "g 0 = a" "g 1 = b" using assms by (auto simp: path_defs) then have "continuous_on ({0..1} × {0..1}) (g ∘ fst)" by (fastforce intro!: continuous_intros)+ with g show ?thesis by (auto simp: homotopic_loops_def homotopic_with_def path_defs Pi_iff) qed lemma homotopic_loops_imp_path_component_value: "⟦homotopic_loops S p q; 0 ≤ t; t ≤ 1⟧ ⟹ path_component S (p t) (q t)" apply (clarsimp simp: homotopic_loops_def homotopic_with_def path_defs) apply (rule_tac x="h ∘ (λu. (u, t))" in exI) apply (fastforce elim!: continuous_on_subset intro!: continuous_intros) done lemma homotopic_points_eq_path_component: "homotopic_loops S (linepath a a) (linepath b b) ⟷ path_component S a b" using homotopic_loops_imp_path_component_value path_component_imp_homotopic_points by fastforce lemma path_connected_eq_homotopic_points: "path_connected S ⟷ (∀a b. a ∈ S ∧ b ∈ S ⟶ homotopic_loops S (linepath a a) (linepath b b))" by (auto simp: path_connected_def path_component_def homotopic_points_eq_path_component) subsection‹Simply connected sets› text✐‹tag important›‹defined as "all loops are homotopic (as loops)› definition✐‹tag important› simply_connected where "simply_connected S ≡ ∀p q. path p ∧ pathfinish p = pathstart p ∧ path_image p ⊆ S ∧ path q ∧ pathfinish q = pathstart q ∧ path_image q ⊆ S ⟶ homotopic_loops S p q" lemma simply_connected_empty [iff]: "simply_connected {}" by (simp add: simply_connected_def) lemma simply_connected_imp_path_connected: fixes S :: "_::real_normed_vector set" shows "simply_connected S ⟹ path_connected S" by (simp add: simply_connected_def path_connected_eq_homotopic_points) lemma simply_connected_imp_connected: fixes S :: "_::real_normed_vector set" shows "simply_connected S ⟹ connected S" by (simp add: path_connected_imp_connected simply_connected_imp_path_connected) lemma simply_connected_eq_contractible_loop_any: fixes S :: "_::real_normed_vector set" shows "simply_connected S ⟷ (∀p a. path p ∧ path_image p ⊆ S ∧ pathfinish p = pathstart p ∧ a ∈ S ⟶ homotopic_loops S p (linepath a a))" (is "?lhs = ?rhs") proof assume ?rhs then show ?lhs unfolding simply_connected_def by (metis pathfinish_in_path_image subsetD homotopic_loops_trans homotopic_loops_sym) qed (force simp: simply_connected_def) lemma simply_connected_eq_contractible_loop_some: fixes S :: "_::real_normed_vector set" shows "simply_connected S ⟷ path_connected S ∧ (∀p. path p ∧ path_image p ⊆ S ∧ pathfinish p = pathstart p ⟶ (∃a. a ∈ S ∧ homotopic_loops S p (linepath a a)))" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs using simply_connected_eq_contractible_loop_any by (blast intro: simply_connected_imp_path_connected) next assume ?rhs then show ?lhs by (meson homotopic_loops_trans path_connected_eq_homotopic_points simply_connected_eq_contractible_loop_any) qed lemma simply_connected_eq_contractible_loop_all: fixes S :: "_::real_normed_vector set" shows "simply_connected S ⟷ S = {} ∨ (∃a ∈ S. ∀p. path p ∧ path_image p ⊆ S ∧ pathfinish p = pathstart p ⟶ homotopic_loops S p (linepath a a))" by (meson ex_in_conv homotopic_loops_sym homotopic_loops_trans simply_connected_def simply_connected_eq_contractible_loop_any) lemma simply_connected_eq_contractible_path: fixes S :: "_::real_normed_vector set" shows "simply_connected S ⟷ path_connected S ∧ (∀p. path p ∧ path_image p ⊆ S ∧ pathfinish p = pathstart p ⟶ homotopic_paths S p (linepath (pathstart p) (pathstart p)))" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs unfolding simply_connected_imp_path_connected by (metis simply_connected_eq_contractible_loop_some homotopic_loops_imp_homotopic_paths_null) next assume ?rhs then show ?lhs using homotopic_paths_imp_homotopic_loops simply_connected_eq_contractible_loop_some by fastforce qed lemma simply_connected_eq_homotopic_paths: fixes S :: "_::real_normed_vector set" shows "simply_connected S ⟷ path_connected S ∧ (∀p q. path p ∧ path_image p ⊆ S ∧ path q ∧ path_image q ⊆ S ∧ pathstart q = pathstart p ∧ pathfinish q = pathfinish p ⟶ homotopic_paths S p q)" (is "?lhs = ?rhs") proof assume ?lhs then have pc: "path_connected S" and *: "⋀p. ⟦path p; path_image p ⊆ S; pathfinish p = pathstart p⟧ ⟹ homotopic_paths S p (linepath (pathstart p) (pathstart p))" by (auto simp: simply_connected_eq_contractible_path) have "homotopic_paths S p q" if "path p" "path_image p ⊆ S" "path q" "path_image q ⊆ S" "pathstart q = pathstart p" "pathfinish q = pathfinish p" for p q proof - have "homotopic_paths S p (p +++ reversepath q +++ q)" using that by (smt (verit, best) homotopic_paths_join homotopic_paths_linv homotopic_paths_rid homotopic_paths_sym homotopic_paths_trans pathstart_linepath) also have "homotopic_paths S … ((p +++ reversepath q) +++ q)" by (simp add: that homotopic_paths_assoc) also have "homotopic_paths S … (linepath (pathstart q) (pathstart q) +++ q)" using * [of "p +++ reversepath q"] that by (simp add: homotopic_paths_assoc homotopic_paths_join path_image_join) also have "homotopic_paths S … q" using that homotopic_paths_lid by blast finally show ?thesis . qed then show ?rhs by (blast intro: pc *) next assume ?rhs then show ?lhs by (force simp: simply_connected_eq_contractible_path) qed proposition simply_connected_Times: fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set" assumes S: "simply_connected S" and T: "simply_connected T" shows "simply_connected(S × T)" proof - have "homotopic_loops (S × T) p (linepath (a, b) (a, b))" if "path p" "path_image p ⊆ S × T" "p 1 = p 0" "a ∈ S" "b ∈ T" for p a b proof - have "path (fst ∘ p)" by (simp add: continuous_on_fst Path_Connected.path_continuous_image [OF ‹path p›]) moreover have "path_image (fst ∘ p) ⊆ S" using that by (force simp: path_image_def) ultimately have p1: "homotopic_loops S (fst ∘ p) (linepath a a)" using S that by (simp add: simply_connected_eq_contractible_loop_any pathfinish_def pathstart_def) have "path (snd ∘ p)" by (simp add: continuous_on_snd Path_Connected.path_continuous_image [OF <