(* Title: HOL/Analysis/Path_Connected.thy
Authors: LC Paulson and Robert Himmelmann (TU Muenchen), based on material from HOL Light
*)
section \<open>Homotopy of Maps\<close>
theory Homotopy
imports Path_Connected Continuum_Not_Denumerable Product_Topology
begin
definition\<^marker>\<open>tag important\<close> homotopic_with
where
"homotopic_with P X Y f g \
(\<exists>h. continuous_map (prod_topology (top_of_set {0..1::real}) X) Y h \<and>
(\<forall>x. h(0, x) = f x) \<and>
(\<forall>x. h(1, x) = g x) \<and>
(\<forall>t \<in> {0..1}. P(\<lambda>x. h(t,x))))"
text\<open>\<open>p\<close>, \<open>q\<close> are functions \<open>X \<rightarrow> Y\<close>, and the property \<open>P\<close> restricts all intermediate maps.
We often just want to require that \<open>P\<close> fixes some subset, but to include the case of a loop homotopy,
it is convenient to have a general property \<open>P\<close>.\<close>
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\<^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\<^marker>\<open>tag important\<close> \<open>%whitespace\<close>
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 \
(\<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>
(\<forall>x \<in> topspace X. h(1,x) = q x) \<and>
(\<forall>t \<in> {0..1}. P(\<lambda>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 auto
using continuous_map_eq apply fastforce
apply (drule_tac x=t in bspec, force)
apply (subst assms; simp)
done
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 (simp add: homotopic_with_def image_subset_iff) (metis atLeastAtMost_iff order_refl zero_le_one)
lemma homotopic_with_imp_subset2:
"homotopic_with_canon P X Y f g \ g ` X \ Y"
by (simp add: homotopic_with_def image_subset_iff) (metis atLeastAtMost_iff order_refl zero_le_one)
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\<open>Homotopy with P is an equivalence relation\<close>
text \<open>(on continuous functions mapping X into Y that satisfy P, though this only affects reflexivity)\<close>
lemma homotopic_with_refl [simp]: "homotopic_with P X Y f f \ continuous_map X Y f \ P f"
by (auto simp: homotopic_with_imp_continuous_maps intro: homotopic_with_equal dest: 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)
then show ?thesis
by (simp add: prod_topology_subtopology(1))
qed
show ?thesis
using assms
apply (clarsimp simp add: 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 \<circ> (\<lambda>x. (2 *\<^sub>R fst x, snd x))) y
else (k2 \<circ> (\<lambda>x. (2 *\<^sub>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 \<circ> (\<lambda>x. (2 *\<^sub>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 \<circ> (\<lambda>x. (2 *\<^sub>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 *\<^sub>R fst x, snd x))) y = (k2 \ (\x. (2 *\<^sub>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 add: 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\<open>Continuity lemmas\<close>
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)\
\<Longrightarrow> homotopic_with q X1 X3 (h \<circ> f) (h \<circ> 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) (\<lambda>(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')"
proof (rule homotopic_with_trans [where g = "g \ f'"])
show "homotopic_with (\x. True) X Z (g \ f) (g \ f')"
using assms by (simp add: homotopic_with_compose_continuous_map_left homotopic_with_imp_continuous_maps)
show "homotopic_with (\x. True) X Z (g \ f') (g' \ f')"
using assms by (simp add: homotopic_with_compose_continuous_map_right homotopic_with_imp_continuous_maps)
qed
proposition homotopic_with_compose_continuous_right:
"\homotopic_with_canon (\f. p (f \ h)) X Y f g; continuous_on W h; h ` W \ X\
\<Longrightarrow> homotopic_with_canon p W Y (f \<circ> h) (g \<circ> h)"
apply (clarsimp simp add: homotopic_with_def)
subgoal for k
apply (rule_tac x="k \ (\y. (fst y, h (snd y)))" in exI)
by (intro conjI continuous_intros continuous_on_compose2 [where f=snd and g=h]; fastforce simp: o_def elim: continuous_on_subset)
done
proposition homotopic_with_compose_continuous_left:
"\homotopic_with_canon (\f. p (h \ f)) X Y f g; continuous_on Y h; h ` Y \ Z\
\<Longrightarrow> homotopic_with_canon p X Z (h \<circ> f) (h \<circ> g)"
apply (clarsimp simp add: homotopic_with_def)
subgoal for k
apply (rule_tac x="h \ k" in exI)
by (intro conjI continuous_intros continuous_on_compose [where f=snd and g=h, unfolded o_def]; fastforce simp: o_def elim: continuous_on_subset)
done
lemma homotopic_from_subtopology:
"homotopic_with P X X' f g \ homotopic_with P (subtopology X s) X' f g"
unfolding homotopic_with_def
by (force simp add: continuous_map_from_subtopology prod_topology_subtopology(2) elim!: ex_forward)
lemma homotopic_on_emptyI:
assumes "topspace X = {}" "P f" "P g"
shows "homotopic_with P X X' f g"
unfolding homotopic_with_def
proof (intro exI conjI ballI)
show "P (\x. (\(t,x). if t = 0 then f x else g x) (t, x))" if "t \ {0..1}" for t::real
by (cases "t = 0", auto simp: assms)
qed (auto simp: continuous_map_atin assms)
lemma homotopic_on_empty:
"topspace X = {} \ (homotopic_with P X X' f g \ P f \ P g)"
using homotopic_on_emptyI homotopic_with_imp_property by metis
lemma homotopic_with_canon_on_empty [simp]: "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) \
topspace X = {} \<or> path_component_of X' a b" (is "?lhs = ?rhs")
proof (cases "topspace X = {}")
case False
then obtain c where c: "c \ topspace X"
by blast
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 c | simp)+
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 (auto simp: path_component_of_def 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'"
using h unfolding homotopic_with_def
apply clarify
subgoal for h
apply (rule_tac x="\(u,v). if v \ topspace X then h(u,v) else if u = 0 then f' v else g' v" in exI)
apply (simp add: f' g', safe)
apply (fastforce intro: continuous_map_eq)
apply (subst P; fastforce)
done
done
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)
(\<lambda>z. (f(fst z),g(snd z))) (\<lambda>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)
(\<lambda>z. (\<lambda>i\<in>I. (f i) (z i))) (\<lambda>z. (\<lambda>i\<in>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) (\<lambda>x. h i (fst x, snd x i))" if "i \<in> I" for i
proof -
have \<section>: "continuous_map (prod_topology (top_of_set {0..1}) (product_topology X I)) (X i) (\<lambda>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 \<section> 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\<open>Homotopic triviality implicitly incorporates path-connectedness.\<close>
lemma homotopic_triviality:
shows "(\f g. continuous_on S f \ f ` S \ T \
continuous_on S g \<and> g ` S \<subseteq> T
\<longrightarrow> homotopic_with_canon (\<lambda>x. True) S T f g) \<longleftrightarrow>
(S = {} \<or> path_connected T) \<and>
(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> T \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) S T f (\<lambda>x. c)))"
(is "?lhs = ?rhs")
proof (cases "S = {} \ T = {}")
case True then show ?thesis
by (auto simp: homotopic_on_emptyI)
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 auto
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 False \<open>continuous_on S f\<close> \<open>f ` S \<subseteq> T\<close> RHS \<open>continuous_on S g\<close> \<open>g ` S \<subseteq> T\<close> by blast
then have "c \ T" "d \ T"
using False homotopic_with_imp_continuous_maps by fastforce+
with T have "path_component T c d"
using path_connected_component by blast
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\<open>Homotopy of paths, maintaining the same endpoints\<close>
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 \
homotopic_with_canon (\<lambda>r. pathstart r = pathstart p \<and> pathfinish r = pathfinish p) {0..1} s p q"
lemma homotopic_paths:
"homotopic_paths s p q \
(\<exists>h. continuous_on ({0..1} \<times> {0..1}) h \<and>
h ` ({0..1} \<times> {0..1}) \<subseteq> s \<and>
(\<forall>x \<in> {0..1}. h(0,x) = p x) \<and>
(\<forall>x \<in> {0..1}. h(1,x) = q x) \<and>
(\<forall>t \<in> {0..1::real}. pathstart(h \<circ> Pair t) = pathstart p \<and>
pathfinish(h \<circ> 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"
proof -
have "pathstart q = pathstart p" "pathfinish q = pathfinish p"
using assms by (simp_all add: homotopic_paths_imp_pathstart homotopic_paths_imp_pathfinish)
then have "homotopic_with_canon (\f. pathstart f = pathstart p \ pathfinish f = pathfinish p) {0..1} s q r"
using \<open>homotopic_paths s q r\<close> homotopic_paths_def by force
then show ?thesis
using assms homotopic_paths_def homotopic_with_trans by blast
qed
proposition homotopic_paths_eq:
"\path p; path_image p \ s; \t. t \ {0..1} \ p t = q t\ \ homotopic_paths s p q"
unfolding homotopic_paths_def
by (rule homotopic_with_eq)
(auto simp: path_def pathstart_def pathfinish_def path_image_def elim: continuous_on_eq)
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 \<open>path p\<close> path_def)
then have "continuous_on {0..1} (p \ f)"
using contf continuous_on_compose continuous_on_subset f01 by blast
then have "path q"
by (simp add: path_def) (metis q continuous_on_cong)
have piqs: "path_image q \ s"
by (metis (no_types, hide_lams) pips f01 image_subset_iff path_image_def q)
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
using f01 [THEN subsetD, of "f b"] by (simp add: convex_bound_le)
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 \<open>path q\<close> 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)) *\<^sub>R ((f \ snd) y) + (fst y) *\<^sub>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\<open> A slightly ad-hoc but useful lemma in constructing homotopies.\<close>
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 \<section>: "(\<lambda>t. p (fst t) (2 * snd t)) = ?p \<circ> (\<lambda>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 \<section>
by (rule continuous_intros continuous_on_subset [OF p] continuous_on_subset [OF q] | force)+
qed (use pf in \<open>auto simp: mult.commute pathstart_def pathfinish_def\<close>)
qed
text\<open> Congruence properties of homotopy w.r.t. path-combining operations.\<close>
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 add: 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)
subsection\<open>Group properties for homotopy of paths\<close>
text\<^marker>\<open>tag important\<close>\<open>So taking equivalence classes under homotopy would give the fundamental group\<close>
proposition homotopic_paths_rid:
assumes "path p" "path_image p \ s"
shows "homotopic_paths s (p +++ linepath (pathfinish p) (pathfinish p)) p"
proof -
have \<section>: "continuous_on {0..1} (\<lambda>t::real. if t \<le> 1/2 then 2 *\<^sub>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 \<section> continuous_on_cases continuous_intros homotopic_paths_reparametrize [where f = "\<lambda>t. if t \<le> 1/2 then 2 *\<^sub>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\<rbrakk>
\<Longrightarrow> 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 *\<^sub>R t
else if t \<le> 3 / 4 then t - (1 / 4)
else 2 *\<^sub>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 add: mult_le_one)+
qed (auto simp add: 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\<open>Homotopy of loops without requiring preservation of endpoints\<close>
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 \
homotopic_with_canon (\<lambda>r. pathfinish r = pathstart r) {0..1} s p q"
lemma homotopic_loops:
"homotopic_loops s p q \
(\<exists>h. continuous_on ({0..1::real} \<times> {0..1}) h \<and>
image h ({0..1} \<times> {0..1}) \<subseteq> s \<and>
(\<forall>x \<in> {0..1}. h(0,x) = p x) \<and>
(\<forall>x \<in> {0..1}. h(1,x) = q x) \<and>
(\<forall>t \<in> {0..1}. pathfinish(h \<circ> Pair t) = pathstart(h \<circ> 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 \<and> path_image p \<subseteq> s \<and> 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 add: homotopic_loops)
proposition homotopic_loops_eq:
"\path p; path_image p \ s; pathfinish p = pathstart p; \t. t \ {0..1} \ p(t) = q(t)\
\<Longrightarrow> 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)
subsection\<open>Relations between the two variants of homotopy\<close>
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 [simp]: "\x. x \ {0..1} \ h(0,x) = p x"
and [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)
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 \<open>c \<le> 1\<close> show ?thesis by fastforce
qed
have *: "\p x. \path p \ path(reversepath p);
path_image p \<subseteq> s \<and> path_image(reversepath p) \<subseteq> s;
pathfinish p = pathstart(linepath a a +++ reversepath p) \<and>
pathstart(reversepath p) = a \<and> pathstart p = x\<rbrakk>
\<Longrightarrow> 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 \<open>path p\<close> 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))"
apply (rule homotopic_paths_sym)
using homotopic_paths_lid [of "p +++ linepath (pathfinish p) (pathfinish p)" s]
by (metis 1 homotopic_paths_imp_path homotopic_paths_imp_pathstart homotopic_paths_imp_subset)
moreover
have "homotopic_paths s (linepath (pathstart p) (pathstart p) +++ p +++ linepath (pathfinish p) (pathfinish p))
((\<lambda>u. h (u, 0)) +++ linepath a a +++ reversepath (\<lambda>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 (\<lambda>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"
unfolding joinpaths_def subpath_def
by (force simp: algebra_simps mult_le_one mult_left_le intro: hs [THEN subsetD] 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)
qed (use ploop in \<open>simp_all add: reversepath_def path_defs joinpaths_def o_def subpath_def conth c1 c2\<close>)
moreover have "homotopic_paths s ((\u. h (u, 0)) +++ linepath a a +++ reversepath (\u. h (u, 0)))
(linepath (pathstart p) (pathstart p))"
proof (rule *; simp add: pih0 pathstart_def pathfinish_def conth0)
show "a = (linepath a a +++ reversepath (\u. h (u, 0))) 0 \ reversepath (\u. h (u, 0)) 0 = a"
by (simp_all add: reversepath_def joinpaths_def)
qed
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 \<open>path p\<close> [unfolded path_def] by blast
have contq: "continuous_on {0..1} q" using \<open>path q\<close> [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_thms_linordered_semiring(1) 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 \<open>path q\<close> 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"
proof -
have "homotopic_paths s (q +++ linepath (pathfinish q) (pathfinish q)) q"
by (simp add: \<open>path q\<close> homotopic_paths_rid piq)
thus ?thesis
by (metis (no_types) 1 \<open>path q\<close> homotopic_paths_join homotopic_paths_rinv homotopic_paths_sym
homotopic_paths_trans qloop pathfinish_linepath piq)
qed
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 \<open>path q\<close> 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
have pipq: "path_image p \ S" "path_image q \ S"
by (metis Un_subset_iff paths \<open>path p\<close> \<open>path q\<close> 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 \<open>path p\<close> \<open>path_image p \<subseteq> S\<close> 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 \<open>path p\<close> \<open>path q\<close> 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 \<open>path p\<close> \<open>path q\<close> homotopic_paths_assoc pipq)
moreover have "homotopic_paths S ((p +++ reversepath q) +++ q) (linepath (pathstart p) (pathstart p) +++ q)"
by (simp add: \<open>path q\<close> homotopic_paths_join paths pipq)
moreover then have "homotopic_paths S (linepath (pathstart p) (pathstart p) +++ q) q"
by (metis \<open>path q\<close> homotopic_paths_imp_path homotopic_paths_lid linepath_trivial path_join_path_ends pathfinish_def pipq(2))
ultimately show ?thesis
using homotopic_paths_trans by metis
next
case False
then show ?thesis
using \<open>path q\<close> homotopic_loops_imp_path loops path_join_path_ends by fastforce
qed
qed
subsection\<^marker>\<open>tag unimportant\<close>\<open>Homotopy of "nearby" function, paths and loops\<close>
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)) *\<^sub>R f(snd y) + (fst y) *\<^sub>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)) *\<^sub>R (g \ snd) y + (fst y) *\<^sub>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)) *\<^sub>R g(snd y) + (fst y) *\<^sub>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 \<section>: "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"
proof (rule homotopic_paths_linear [OF \<section>])
show "\t. t \ {0..1} \ closed_segment (g t) (h t) \ S"
by (metis no segment_bound(1) subsetI norm_minus_commute not_le)
qed
lemma homotopic_loops_nearby_explicit:
assumes \<section>: "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"
proof (rule homotopic_loops_linear [OF \<section>])
show "\t. t \ {0..1} \ closed_segment (g t) (h t) \ S"
by (metis no segment_bound(1) subsetI norm_minus_commute not_le)
qed
lemma homotopic_nearby_paths:
fixes g h :: "real \ 'a::euclidean_space"
assumes "path g" "open S" "path_image g \ S"
shows "\e. 0 < e \
(\<forall>h. path h \<and>
pathstart h = pathstart g \<and> pathfinish h = pathfinish g \<and>
(\<forall>t \<in> {0..1}. norm(h t - g t) < e) \<longrightarrow> 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] \<open>e > 0\<close>
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 \
(\<forall>h. path h \<and> pathfinish h = pathstart h \<and>
(\<forall>t \<in> {0..1}. norm(h t - g t) < e) \<longrightarrow> 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] \<open>e > 0\<close>
by (fastforce simp: path_image_def intro!: homotopic_loops_nearby_explicit assms exI)
qed
subsection\<open> Homotopy and subpaths\<close>
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 \<open>u \<le> v\<close> 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 \<open>u \<le> v\<close> \<open>v \<le> w\<close>)
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 \<open>path g\<close> 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)) *\<^sub>R (2 * (v - u)) *\<^sub>R t
else inverse((w - u)) *\<^sub>R ((v - u) + (w - v) *\<^sub>R (2 *\<^sub>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 add: 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 -
have "homotopic_paths s (subpath u w g +++ subpath w v g) ((subpath u v g +++ subpath v w g) +++ subpath w v g)"
proof (rule homotopic_paths_join)
show "homotopic_paths s (subpath u w g) (subpath u v g +++ subpath v w g)"
using hom homotopic_paths_sym_eq by blast
show "homotopic_paths s (subpath w v g) (subpath w v g)"
by (metis \<open>path g\<close> homotopic_paths_eq pag path_image_subpath_subset path_subpath subset_trans v w)
qed auto
also have "homotopic_paths s ((subpath u v g +++ subpath v w g) +++ subpath w v g) (subpath u v g +++ subpath v w g +++ subpath w v g)"
by (rule homotopic_paths_sym [OF homotopic_paths_assoc])
(use assms in \<open>simp_all add: path_image_subpath_subset [THEN order_trans]\<close>)
also have "homotopic_paths s (subpath u v g +++ subpath v w g +++ subpath w v g)
(subpath u v g +++ linepath (pathfinish (subpath u v g)) (pathfinish (subpath u v g)))"
proof (rule homotopic_paths_join; simp)
show "path (subpath u v g) \ path_image (subpath u v g) \ s"
by (metis \<open>path g\<close> order.trans pag path_image_subpath_subset path_subpath u v)
show "homotopic_paths s (subpath v w g +++ subpath w v g) (linepath (g v) (g v))"
by (metis (no_types, lifting) \<open>path g\<close> homotopic_paths_linv order_trans pag path_image_subpath_subset path_subpath pathfinish_subpath reversepath_subpath v w)
qed
also have "homotopic_paths s (subpath u v g +++ linepath (pathfinish (subpath u v g)) (pathfinish (subpath u v g))) (subpath u v g)"
proof (rule homotopic_paths_rid)
show "path (subpath u v g)"
using \<open>path g\<close> path_subpath u v by blast
show "path_image (subpath u v g) \ s"
by (meson \<open>path g\<close> order.trans pag path_image_subpath_subset u v)
qed
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}\
\<Longrightarrow> homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)"
using le_cases3 [of u v w] homotopic_join_subpaths1 homotopic_join_subpaths2 homotopic_join_subpaths3
by metis
text\<open>Relating homotopy of trivial loops to path-connectedness.\<close>
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 add: homotopic_loops_def homotopic_with_def path_defs image_subset_iff)
qed
lemma homotopic_loops_imp_path_component_value:
"\homotopic_loops S p q; 0 \ t; t \ 1\
\<Longrightarrow> path_component S (p t) (q t)"
apply (clarsimp simp add: 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"
by (auto simp: path_component_imp_homotopic_points
dest: homotopic_loops_imp_path_component_value [where t=1])
lemma path_connected_eq_homotopic_points:
"path_connected S \
(\<forall>a b. a \<in> S \<and> b \<in> S \<longrightarrow> homotopic_loops S (linepath a a) (linepath b b))"
by (auto simp: path_connected_def path_component_def homotopic_points_eq_path_component)
subsection\<open>Simply connected sets\<close>
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 \
\<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"
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 \
(\<forall>p a. path p \<and> path_image p \<subseteq> S \<and> pathfinish p = pathstart p \<and> a \<in> S
\<longrightarrow> homotopic_loops S p (linepath a a))"
(is "?lhs = ?rhs")
proof
assume ?lhs then show ?rhs
unfolding simply_connected_def by force
next
assume ?rhs then show ?lhs
unfolding simply_connected_def
by (metis pathfinish_in_path_image subsetD homotopic_loops_trans homotopic_loops_sym)
qed
lemma simply_connected_eq_contractible_loop_some:
fixes S :: "_::real_normed_vector set"
shows "simply_connected S \
path_connected S \<and>
(\<forall>p. path p \<and> path_image p \<subseteq> S \<and> pathfinish p = pathstart p
\<longrightarrow> (\<exists>a. a \<in> S \<and> 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 r: ?rhs
note pa = r [THEN conjunct2, rule_format]
show ?lhs
proof (clarsimp simp add: simply_connected_eq_contractible_loop_any)
fix p a
assume "path p" and "path_image p \ S" "pathfinish p = pathstart p"
and "a \ S"
with pa [of p] show "homotopic_loops S p (linepath a a)"
using homotopic_loops_trans path_connected_eq_homotopic_points r by blast
qed
qed
lemma simply_connected_eq_contractible_loop_all:
fixes S :: "_::real_normed_vector set"
shows "simply_connected S \
S = {} \<or>
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.47 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
