Quelle Homotopy.thy Sprache: Isabelle

(*  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 Product_Topology Uncountable_Sets
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 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_funspace1:
     "homotopic_with_canon P X Y f g \ f \ X \ Y"
  using homotopic_with_imp_continuous_maps by fastforce

lemma homotopic_with_imp_subset1:
     "homotopic_with_canon P X Y f g \ f ` X \ Y"
  using homotopic_with_imp_funspace1 by blast

lemma homotopic_with_imp_funspace2:
     "homotopic_with_canon P X Y f g \ g \ X \ Y"
  using homotopic_with_imp_continuous_maps by force

lemma homotopic_with_imp_subset2:
     "homotopic_with_canon P X Y f g \ g ` X \ Y"
  using homotopic_with_imp_funspace2 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\<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 (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 \<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: 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')"
  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\
     \<Longrightarrow> homotopic_with_canon p W Y (f \<circ> h) (g \<circ> 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\
      \<Longrightarrow> homotopic_with_canon p X Z (h \<circ> f) (h \<circ> 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 \<or> 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)
                          (\<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 \<in> S \<rightarrow> 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 \<in> S \<rightarrow> 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 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 \<open>continuous_on S f\<close> \<open>continuous_on S g\<close> \<open>f \<in> S \<rightarrow> T\<close> \<open>g \<in> S \<rightarrow> T\<close> 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\<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 \<in> ({0..1} \<times> {0..1}) \<rightarrow> 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 (simp add: homotopic_paths_def homotopic_with_imp_subset1 homotopic_with_imp_subset2
      path_image_def)

proposition homotopic_paths_refl [simp]: "homotopic_paths S p p \ path p \ path_image p \ S"
  by (auto 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 \<open>path p\<close> 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  \<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: 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\<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)

lemma homotopic_paths_rid':
  assumes "path p" "path_image p \ s" "x = pathfinish p"
  shows "homotopic_paths s (p +++ linepath x x) p"
  using homotopic_paths_rid[of p s] assms by simp

lemma homotopic_paths_lid':
   "\path p; path_image p \ s; x = pathstart p\ \ homotopic_paths s (linepath x x +++ p) p"
  using homotopic_paths_lid[of p s] by simp

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: 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\<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>
          h \<in> ({0..1} \<times> {0..1}) \<rightarrow> 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 (simp add: homotopic_with_imp_subset1 homotopic_with_imp_subset2)

proposition homotopic_loops_refl:
     "homotopic_loops S p p \
      path p \<and> path_image p \<subseteq> S \<and> pathfinish p = pathstart p"
  by (metis (mono_tags, lifting) homotopic_loops_def homotopic_paths_def
      homotopic_paths_refl homotopic_with_refl)

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)\
          \<Longrightarrow> homotopic_loops S p q"
  unfolding homotopic_loops_def path_image_def path_def pathstart_def pathfinish_def image_subset_iff_funcset
  using homotopic_with_eq [OF homotopic_with_refl [where f = p, THEN iffD2]]
  by fastforce

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\<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 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 \<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))"
    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))
                                   ((\<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"
      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 \<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))"
    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 \<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 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"
      by (smt (verit, best) \<open>path q\<close> 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 \<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
    obtain 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)
    ultimately show ?thesis
      by (metis \<open>path q\<close> 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 \<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"
  using homotopic_paths_linear [OF \<section>] by (metis linorder_not_le no norm_minus_commute segment_bound1 subsetI)

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"
  using homotopic_loops_linear [OF \<section>] 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 \
               (\<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: 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 \<open>path g\<close> 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 \<open>path g\<close>
    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 \<open>path g\<close>
    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 \<open>path g\<close> 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}\
    \<Longrightarrow> 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\<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: 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 \
      (\<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 ?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 \<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 ?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 = {} \<or>
         (\<exists>a \<in> S. \<forall>p. path p \<and> path_image p \<subseteq> S \<and> pathfinish p = pathstart p
                \<longrightarrow> 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 \<and>
           (\<forall>p. path p \<and> path_image p \<subseteq> S \<and> pathfinish p = pathstart p
            \<longrightarrow> 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 \<and>
          (\<forall>p q. path p \<and> path_image p \<subseteq> S \<and>
                path q \<and> path_image q \<subseteq> S \<and>
                pathstart q = pathstart p \<and> pathfinish q = pathfinish p
                \<longrightarrow> 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\<rbrakk>
                      \<Longrightarrow> 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
--> --------------------

--> maximum size reached

--> --------------------

quality99%

¤ Dauer der Verarbeitung: 0.27 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.