5761 |
5761 |
5762 lemma homeomorphic_simply_connected_eq: |
5762 lemma homeomorphic_simply_connected_eq: |
5763 "S homeomorphic T \<Longrightarrow> (simply_connected S \<longleftrightarrow> simply_connected T)" |
5763 "S homeomorphic T \<Longrightarrow> (simply_connected S \<longleftrightarrow> simply_connected T)" |
5764 by (metis homeomorphic_simply_connected homeomorphic_sym) |
5764 by (metis homeomorphic_simply_connected homeomorphic_sym) |
5765 |
5765 |
|
5766 subsection\<open>Homotopy equivalence\<close> |
|
5767 |
|
5768 definition homotopy_eqv :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool" |
|
5769 (infix "homotopy'_eqv" 50) |
|
5770 where "S homotopy_eqv T \<equiv> |
|
5771 \<exists>f g. continuous_on S f \<and> f ` S \<subseteq> T \<and> |
|
5772 continuous_on T g \<and> g ` T \<subseteq> S \<and> |
|
5773 homotopic_with (\<lambda>x. True) S S (g o f) id \<and> |
|
5774 homotopic_with (\<lambda>x. True) T T (f o g) id" |
|
5775 |
|
5776 lemma homeomorphic_imp_homotopy_eqv: "S homeomorphic T \<Longrightarrow> S homotopy_eqv T" |
|
5777 unfolding homeomorphic_def homotopy_eqv_def homeomorphism_def |
|
5778 by (fastforce intro!: homotopic_with_equal continuous_on_compose) |
|
5779 |
|
5780 lemma homotopy_eqv_refl: "S homotopy_eqv S" |
|
5781 by (rule homeomorphic_imp_homotopy_eqv homeomorphic_refl)+ |
|
5782 |
|
5783 lemma homotopy_eqv_sym: "S homotopy_eqv T \<longleftrightarrow> T homotopy_eqv S" |
|
5784 by (auto simp: homotopy_eqv_def) |
|
5785 |
|
5786 lemma homotopy_eqv_trans [trans]: |
|
5787 fixes S :: "'a::real_normed_vector set" and U :: "'c::real_normed_vector set" |
|
5788 assumes ST: "S homotopy_eqv T" and TU: "T homotopy_eqv U" |
|
5789 shows "S homotopy_eqv U" |
|
5790 proof - |
|
5791 obtain f1 g1 where f1: "continuous_on S f1" "f1 ` S \<subseteq> T" |
|
5792 and g1: "continuous_on T g1" "g1 ` T \<subseteq> S" |
|
5793 and hom1: "homotopic_with (\<lambda>x. True) S S (g1 o f1) id" |
|
5794 "homotopic_with (\<lambda>x. True) T T (f1 o g1) id" |
|
5795 using ST by (auto simp: homotopy_eqv_def) |
|
5796 obtain f2 g2 where f2: "continuous_on T f2" "f2 ` T \<subseteq> U" |
|
5797 and g2: "continuous_on U g2" "g2 ` U \<subseteq> T" |
|
5798 and hom2: "homotopic_with (\<lambda>x. True) T T (g2 o f2) id" |
|
5799 "homotopic_with (\<lambda>x. True) U U (f2 o g2) id" |
|
5800 using TU by (auto simp: homotopy_eqv_def) |
|
5801 have "homotopic_with (\<lambda>f. True) S T (g2 \<circ> f2 \<circ> f1) (id \<circ> f1)" |
|
5802 by (rule homotopic_with_compose_continuous_right hom2 f1)+ |
|
5803 then have "homotopic_with (\<lambda>f. True) S T (g2 \<circ> (f2 \<circ> f1)) (id \<circ> f1)" |
|
5804 by (simp add: o_assoc) |
|
5805 then have "homotopic_with (\<lambda>x. True) S S |
|
5806 (g1 \<circ> (g2 \<circ> (f2 \<circ> f1))) (g1 o (id o f1))" |
|
5807 by (simp add: g1 homotopic_with_compose_continuous_left) |
|
5808 moreover have "homotopic_with (\<lambda>x. True) S S (g1 o id o f1) id" |
|
5809 using hom1 by simp |
|
5810 ultimately have SS: "homotopic_with (\<lambda>x. True) S S (g1 \<circ> g2 \<circ> (f2 \<circ> f1)) id" |
|
5811 apply (simp add: o_assoc) |
|
5812 apply (blast intro: homotopic_with_trans) |
|
5813 done |
|
5814 have "homotopic_with (\<lambda>f. True) U T (f1 \<circ> g1 \<circ> g2) (id \<circ> g2)" |
|
5815 by (rule homotopic_with_compose_continuous_right hom1 g2)+ |
|
5816 then have "homotopic_with (\<lambda>f. True) U T (f1 \<circ> (g1 \<circ> g2)) (id \<circ> g2)" |
|
5817 by (simp add: o_assoc) |
|
5818 then have "homotopic_with (\<lambda>x. True) U U |
|
5819 (f2 \<circ> (f1 \<circ> (g1 \<circ> g2))) (f2 o (id o g2))" |
|
5820 by (simp add: f2 homotopic_with_compose_continuous_left) |
|
5821 moreover have "homotopic_with (\<lambda>x. True) U U (f2 o id o g2) id" |
|
5822 using hom2 by simp |
|
5823 ultimately have UU: "homotopic_with (\<lambda>x. True) U U (f2 \<circ> f1 \<circ> (g1 \<circ> g2)) id" |
|
5824 apply (simp add: o_assoc) |
|
5825 apply (blast intro: homotopic_with_trans) |
|
5826 done |
|
5827 show ?thesis |
|
5828 unfolding homotopy_eqv_def |
|
5829 apply (rule_tac x = "f2 \<circ> f1" in exI) |
|
5830 apply (rule_tac x = "g1 \<circ> g2" in exI) |
|
5831 apply (intro conjI continuous_on_compose SS UU) |
|
5832 using f1 f2 g1 g2 apply (force simp: elim!: continuous_on_subset)+ |
|
5833 done |
|
5834 qed |
|
5835 |
|
5836 lemma homotopy_eqv_inj_linear_image: |
|
5837 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
5838 assumes "linear f" "inj f" |
|
5839 shows "(f ` S) homotopy_eqv S" |
|
5840 apply (rule homeomorphic_imp_homotopy_eqv) |
|
5841 using assms homeomorphic_sym linear_homeomorphic_image by auto |
|
5842 |
|
5843 lemma homotopy_eqv_translation: |
|
5844 fixes S :: "'a::real_normed_vector set" |
|
5845 shows "op + a ` S homotopy_eqv S" |
|
5846 apply (rule homeomorphic_imp_homotopy_eqv) |
|
5847 using homeomorphic_translation homeomorphic_sym by blast |
|
5848 |
|
5849 lemma homotopy_eqv_homotopic_triviality_imp: |
|
5850 fixes S :: "'a::real_normed_vector set" |
|
5851 and T :: "'b::real_normed_vector set" |
|
5852 and U :: "'c::real_normed_vector set" |
|
5853 assumes "S homotopy_eqv T" |
|
5854 and f: "continuous_on U f" "f ` U \<subseteq> T" |
|
5855 and g: "continuous_on U g" "g ` U \<subseteq> T" |
|
5856 and homUS: "\<And>f g. \<lbrakk>continuous_on U f; f ` U \<subseteq> S; |
|
5857 continuous_on U g; g ` U \<subseteq> S\<rbrakk> |
|
5858 \<Longrightarrow> homotopic_with (\<lambda>x. True) U S f g" |
|
5859 shows "homotopic_with (\<lambda>x. True) U T f g" |
|
5860 proof - |
|
5861 obtain h k where h: "continuous_on S h" "h ` S \<subseteq> T" |
|
5862 and k: "continuous_on T k" "k ` T \<subseteq> S" |
|
5863 and hom: "homotopic_with (\<lambda>x. True) S S (k o h) id" |
|
5864 "homotopic_with (\<lambda>x. True) T T (h o k) id" |
|
5865 using assms by (auto simp: homotopy_eqv_def) |
|
5866 have "homotopic_with (\<lambda>f. True) U S (k \<circ> f) (k \<circ> g)" |
|
5867 apply (rule homUS) |
|
5868 using f g k |
|
5869 apply (safe intro!: continuous_on_compose h k f elim!: continuous_on_subset) |
|
5870 apply (force simp: o_def)+ |
|
5871 done |
|
5872 then have "homotopic_with (\<lambda>x. True) U T (h o (k o f)) (h o (k o g))" |
|
5873 apply (rule homotopic_with_compose_continuous_left) |
|
5874 apply (simp_all add: h) |
|
5875 done |
|
5876 moreover have "homotopic_with (\<lambda>x. True) U T (h o k o f) (id o f)" |
|
5877 apply (rule homotopic_with_compose_continuous_right [where X=T and Y=T]) |
|
5878 apply (auto simp: hom f) |
|
5879 done |
|
5880 moreover have "homotopic_with (\<lambda>x. True) U T (h o k o g) (id o g)" |
|
5881 apply (rule homotopic_with_compose_continuous_right [where X=T and Y=T]) |
|
5882 apply (auto simp: hom g) |
|
5883 done |
|
5884 ultimately show "homotopic_with (\<lambda>x. True) U T f g" |
|
5885 apply (simp add: o_assoc) |
|
5886 using homotopic_with_trans homotopic_with_sym by blast |
|
5887 qed |
|
5888 |
|
5889 lemma homotopy_eqv_homotopic_triviality: |
|
5890 fixes S :: "'a::real_normed_vector set" |
|
5891 and T :: "'b::real_normed_vector set" |
|
5892 and U :: "'c::real_normed_vector set" |
|
5893 assumes "S homotopy_eqv T" |
|
5894 shows "(\<forall>f g. continuous_on U f \<and> f ` U \<subseteq> S \<and> |
|
5895 continuous_on U g \<and> g ` U \<subseteq> S |
|
5896 \<longrightarrow> homotopic_with (\<lambda>x. True) U S f g) \<longleftrightarrow> |
|
5897 (\<forall>f g. continuous_on U f \<and> f ` U \<subseteq> T \<and> |
|
5898 continuous_on U g \<and> g ` U \<subseteq> T |
|
5899 \<longrightarrow> homotopic_with (\<lambda>x. True) U T f g)" |
|
5900 apply (rule iffI) |
|
5901 apply (metis assms homotopy_eqv_homotopic_triviality_imp) |
|
5902 by (metis (no_types) assms homotopy_eqv_homotopic_triviality_imp homotopy_eqv_sym) |
|
5903 |
|
5904 |
|
5905 lemma homotopy_eqv_cohomotopic_triviality_null_imp: |
|
5906 fixes S :: "'a::real_normed_vector set" |
|
5907 and T :: "'b::real_normed_vector set" |
|
5908 and U :: "'c::real_normed_vector set" |
|
5909 assumes "S homotopy_eqv T" |
|
5910 and f: "continuous_on T f" "f ` T \<subseteq> U" |
|
5911 and homSU: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> U\<rbrakk> |
|
5912 \<Longrightarrow> \<exists>c. homotopic_with (\<lambda>x. True) S U f (\<lambda>x. c)" |
|
5913 obtains c where "homotopic_with (\<lambda>x. True) T U f (\<lambda>x. c)" |
|
5914 proof - |
|
5915 obtain h k where h: "continuous_on S h" "h ` S \<subseteq> T" |
|
5916 and k: "continuous_on T k" "k ` T \<subseteq> S" |
|
5917 and hom: "homotopic_with (\<lambda>x. True) S S (k o h) id" |
|
5918 "homotopic_with (\<lambda>x. True) T T (h o k) id" |
|
5919 using assms by (auto simp: homotopy_eqv_def) |
|
5920 obtain c where "homotopic_with (\<lambda>x. True) S U (f \<circ> h) (\<lambda>x. c)" |
|
5921 apply (rule exE [OF homSU [of "f \<circ> h"]]) |
|
5922 apply (intro continuous_on_compose h) |
|
5923 using h f apply (force elim!: continuous_on_subset)+ |
|
5924 done |
|
5925 then have "homotopic_with (\<lambda>x. True) T U ((f o h) o k) ((\<lambda>x. c) o k)" |
|
5926 apply (rule homotopic_with_compose_continuous_right [where X=S]) |
|
5927 using k by auto |
|
5928 moreover have "homotopic_with (\<lambda>x. True) T U (f \<circ> id) (f \<circ> (h \<circ> k))" |
|
5929 apply (rule homotopic_with_compose_continuous_left [where Y=T]) |
|
5930 apply (simp add: hom homotopic_with_symD) |
|
5931 using f apply auto |
|
5932 done |
|
5933 ultimately show ?thesis |
|
5934 apply (rule_tac c=c in that) |
|
5935 apply (simp add: o_def) |
|
5936 using homotopic_with_trans by blast |
|
5937 qed |
|
5938 |
|
5939 lemma homotopy_eqv_cohomotopic_triviality_null: |
|
5940 fixes S :: "'a::real_normed_vector set" |
|
5941 and T :: "'b::real_normed_vector set" |
|
5942 and U :: "'c::real_normed_vector set" |
|
5943 assumes "S homotopy_eqv T" |
|
5944 shows "(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> U |
|
5945 \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) S U f (\<lambda>x. c))) \<longleftrightarrow> |
|
5946 (\<forall>f. continuous_on T f \<and> f ` T \<subseteq> U |
|
5947 \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) T U f (\<lambda>x. c)))" |
|
5948 apply (rule iffI) |
|
5949 apply (metis assms homotopy_eqv_cohomotopic_triviality_null_imp) |
|
5950 by (metis assms homotopy_eqv_cohomotopic_triviality_null_imp homotopy_eqv_sym) |
|
5951 |
|
5952 |
|
5953 lemma homotopy_eqv_contractible_sets: |
|
5954 fixes S :: "'a::real_normed_vector set" |
|
5955 and T :: "'b::real_normed_vector set" |
|
5956 assumes "contractible S" "contractible T" "S = {} \<longleftrightarrow> T = {}" |
|
5957 shows "S homotopy_eqv T" |
|
5958 proof (cases "S = {}") |
|
5959 case True with assms show ?thesis |
|
5960 by (simp add: homeomorphic_imp_homotopy_eqv) |
|
5961 next |
|
5962 case False |
|
5963 with assms obtain a b where "a \<in> S" "b \<in> T" |
|
5964 by auto |
|
5965 then show ?thesis |
|
5966 unfolding homotopy_eqv_def |
|
5967 apply (rule_tac x="\<lambda>x. b" in exI) |
|
5968 apply (rule_tac x="\<lambda>x. a" in exI) |
|
5969 apply (intro assms conjI continuous_on_id' homotopic_into_contractible) |
|
5970 apply (auto simp: o_def continuous_on_const) |
|
5971 done |
|
5972 qed |
|
5973 |
|
5974 lemma homotopy_eqv_empty1 [simp]: |
|
5975 fixes S :: "'a::real_normed_vector set" |
|
5976 shows "S homotopy_eqv ({}::'b::real_normed_vector set) \<longleftrightarrow> S = {}" |
|
5977 apply (rule iffI) |
|
5978 using homotopy_eqv_def apply fastforce |
|
5979 by (simp add: homotopy_eqv_contractible_sets contractible_empty) |
|
5980 |
|
5981 lemma homotopy_eqv_empty2 [simp]: |
|
5982 fixes S :: "'a::real_normed_vector set" |
|
5983 shows "({}::'b::real_normed_vector set) homotopy_eqv S \<longleftrightarrow> S = {}" |
|
5984 by (metis homotopy_eqv_empty1 homotopy_eqv_sym) |
|
5985 |
|
5986 lemma homotopy_eqv_contractibility: |
|
5987 fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set" |
|
5988 shows "S homotopy_eqv T \<Longrightarrow> (contractible S \<longleftrightarrow> contractible T)" |
|
5989 unfolding homotopy_eqv_def |
|
5990 by (blast intro: homotopy_dominated_contractibility) |
|
5991 |
|
5992 lemma homotopy_eqv_sing: |
|
5993 fixes S :: "'a::real_normed_vector set" and a :: "'b::real_normed_vector" |
|
5994 shows "S homotopy_eqv {a} \<longleftrightarrow> S \<noteq> {} \<and> contractible S" |
|
5995 proof (cases "S = {}") |
|
5996 case True then show ?thesis |
|
5997 by simp |
|
5998 next |
|
5999 case False then show ?thesis |
|
6000 by (metis contractible_sing empty_not_insert homotopy_eqv_contractibility homotopy_eqv_contractible_sets) |
|
6001 qed |
|
6002 |
|
6003 lemma homeomorphic_contractible_eq: |
|
6004 fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set" |
|
6005 shows "S homeomorphic T \<Longrightarrow> (contractible S \<longleftrightarrow> contractible T)" |
|
6006 by (simp add: homeomorphic_imp_homotopy_eqv homotopy_eqv_contractibility) |
|
6007 |
|
6008 lemma homeomorphic_contractible: |
|
6009 fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set" |
|
6010 shows "\<lbrakk>contractible S; S homeomorphic T\<rbrakk> \<Longrightarrow> contractible T" |
|
6011 by (metis homeomorphic_contractible_eq) |
|
6012 |
5766 end |
6013 end |