# HG changeset patch # User paulson # Date 1554899695 -3600 # Node ID 4005298550a69e1af773eb4da784ede61b3e7037 # Parent c4f2cac288d27da17567dbc75ef8b96504695efe The last big tranche of Homology material: invariance of domain; renamings to use generic sum/prod lemmas from their locale diff -r c4f2cac288d2 -r 4005298550a6 src/HOL/Analysis/Abstract_Euclidean_Space.thy --- a/src/HOL/Analysis/Abstract_Euclidean_Space.thy Tue Apr 09 21:05:48 2019 +0100 +++ b/src/HOL/Analysis/Abstract_Euclidean_Space.thy Wed Apr 10 13:34:55 2019 +0100 @@ -90,19 +90,19 @@ by (fastforce simp add: continuous_map_componentwise_UNIV continuous_map_diff) lemma continuous_map_Euclidean_space_iff: - "continuous_map (Euclidean_space m) euclideanreal g + "continuous_map (Euclidean_space m) euclidean g = continuous_on (topspace (Euclidean_space m)) g" proof - assume "continuous_map (Euclidean_space m) euclideanreal g" - then have "continuous_map (top_of_set {f. \n\m. f n = 0}) euclideanreal g" + assume "continuous_map (Euclidean_space m) euclidean g" + then have "continuous_map (top_of_set {f. \n\m. f n = 0}) euclidean g" by (simp add: Euclidean_space_def euclidean_product_topology) then show "continuous_on (topspace (Euclidean_space m)) g" by (metis continuous_map_subtopology_eu subtopology_topspace topspace_Euclidean_space) next assume "continuous_on (topspace (Euclidean_space m)) g" - then have "continuous_map (top_of_set {f. \n\m. f n = 0}) euclideanreal g" + then have "continuous_map (top_of_set {f. \n\m. f n = 0}) euclidean g" by (metis (lifting) continuous_map_into_fulltopology continuous_map_subtopology_eu order_refl topspace_Euclidean_space) - then show "continuous_map (Euclidean_space m) euclideanreal g" + then show "continuous_map (Euclidean_space m) euclidean g" by (simp add: Euclidean_space_def euclidean_product_topology) qed @@ -201,6 +201,21 @@ by (simp add: nsphere subtopology_subtopology) qed +lemma topspace_nsphere_minus1: + assumes x: "x \ topspace (nsphere n)" and "x n = 0" + shows "x \ topspace (nsphere (n - Suc 0))" +proof (cases "n = 0") + case True + then show ?thesis + using x by auto +next + case False + have subt_eq: "nsphere (n - Suc 0) = subtopology (nsphere n) {x. x n = 0}" + by (metis False Suc_pred le_zero_eq not_le subtopology_nsphere_equator) + with x show ?thesis + by (simp add: assms) +qed + lemma continuous_map_nsphere_reflection: "continuous_map (nsphere n) (nsphere n) (\x i. if i = k then -x i else x i)" proof - diff -r c4f2cac288d2 -r 4005298550a6 src/HOL/Analysis/Convex.thy --- a/src/HOL/Analysis/Convex.thy Tue Apr 09 21:05:48 2019 +0100 +++ b/src/HOL/Analysis/Convex.thy Wed Apr 10 13:34:55 2019 +0100 @@ -272,8 +272,8 @@ with *[rule_format, of "2" ?u ?x] have s: "(\j \ {1..2}. ?u j *\<^sub>R ?x j) \ s" using mu xy by auto have grarr: "(\j \ {Suc (Suc 0)..2}. ?u j *\<^sub>R ?x j) = (1 - \) *\<^sub>R y" - using sum_head_Suc[of "Suc (Suc 0)" 2 "\ j. (1 - \) *\<^sub>R y"] by auto - from sum_head_Suc[of "Suc 0" 2 "\ j. ?u j *\<^sub>R ?x j", simplified this] + using sum.atLeast_Suc_atMost[of "Suc (Suc 0)" 2 "\ j. (1 - \) *\<^sub>R y"] by auto + from sum.atLeast_Suc_atMost[of "Suc 0" 2 "\ j. ?u j *\<^sub>R ?x j", simplified this] have "(\j \ {1..2}. ?u j *\<^sub>R ?x j) = \ *\<^sub>R x + (1 - \) *\<^sub>R y" by auto then have "(1 - \) *\<^sub>R y + \ *\<^sub>R x \ s" diff -r c4f2cac288d2 -r 4005298550a6 src/HOL/Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Tue Apr 09 21:05:48 2019 +0100 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Wed Apr 10 13:34:55 2019 +0100 @@ -2090,6 +2090,14 @@ lemma is_interval_cball_1[intro, simp]: "is_interval (cball a b)" for a b::real by (simp add: is_interval_convex_1) +lemma [simp]: + fixes r s::real + shows is_interval_io: "is_interval {..Another intermediate value theorem formulation\ diff -r c4f2cac288d2 -r 4005298550a6 src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy --- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Tue Apr 09 21:05:48 2019 +0100 +++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Wed Apr 10 13:34:55 2019 +0100 @@ -1142,7 +1142,7 @@ unfolding nn_integral_sum[OF f] .. also have "\ = \\<^sup>+x. (SUP n. \iM" using f all_pos by (intro nn_integral_monotone_convergence_SUP_AE[symmetric]) - (elim AE_mp, auto simp: sum_nonneg simp del: sum_lessThan_Suc intro!: AE_I2 sum_mono2) + (elim AE_mp, auto simp: sum_nonneg simp del: sum.lessThan_Suc intro!: AE_I2 sum_mono2) also have "\ = \\<^sup>+x. (\i. f i x) \M" using all_pos by (intro nn_integral_cong_AE) (auto simp: suminf_eq_SUP) finally show ?thesis by simp diff -r c4f2cac288d2 -r 4005298550a6 src/HOL/Analysis/Ordered_Euclidean_Space.thy --- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy Tue Apr 09 21:05:48 2019 +0100 +++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy Wed Apr 10 13:34:55 2019 +0100 @@ -221,14 +221,9 @@ by (simp add: cbox_interval) lemma [simp]: - fixes a b::"'a::ordered_euclidean_space" and r s::real - shows is_interval_io: "is_interval {.. a = b" by fast @@ -814,7 +814,7 @@ by (auto simp: fps_pow_nth_below_subdegree) with False Suc show ?thesis using fps_mult_nth_conv_inside_subdegrees[of f "f^n" "Suc n * subdegree f"] - sum_head_Suc[of + sum.atLeast_Suc_atMost[of "subdegree f" "Suc n * subdegree f - subdegree (f ^ n)" "\i. f $ i * f ^ n $ (Suc n * subdegree f - i)" @@ -857,7 +857,7 @@ proof (cases m) case 0 thus ?thesis using fps_mult_nth_1[of "fps_X" f] by (simp add: fps_X_def) next - case (Suc k) thus ?thesis by (simp add: fps_mult_nth fps_X_def sum_head_Suc) + case (Suc k) thus ?thesis by (simp add: fps_mult_nth fps_X_def sum.atLeast_Suc_atMost) qed ultimately show ?thesis by simp qed (simp add: fps_X_def) @@ -949,7 +949,7 @@ lemma fps_X_power_mult_nth: "(fps_X^k * f) $ n = (if n < k then 0 else f $ (n - k))" by (cases "n subdegree a" hence "fps_shift 1 (a*b) $ n = (\i=Suc 0..Suc n. a$i * b$(n+1-i))" - using sum_head_Suc[of 0 "n+1" "\i. a$i * b$(n+1-i)"] + using sum.atLeast_Suc_atMost[of 0 "n+1" "\i. a$i * b$(n+1-i)"] by (simp add: fps_mult_nth nth_less_subdegree_zero) thus "fps_shift 1 (a*b) $ n = (fps_shift 1 a * b) $ n" using sum_shift_bounds_cl_Suc_ivl[of "\i. a$i * b$(n+1-i)" 0 n] @@ -1763,7 +1763,7 @@ "(f * fps_right_inverse f y) $ n = - 1 * sum (\i. f$i * fps_right_inverse_constructor f y (n - i)) {1..n} + sum (\i. f$i * (fps_right_inverse_constructor f y (n - i))) {1..n}" - by (simp add: fps_mult_nth sum_head_Suc mult.assoc f0[symmetric]) + by (simp add: fps_mult_nth sum.atLeast_Suc_atMost mult.assoc f0[symmetric]) thus "(f * fps_right_inverse f y) $ n = 1 $ n" by (simp add: Suc) qed (simp add: f0 fps_inverse_def) qed @@ -1935,7 +1935,7 @@ using 1 by auto hence "fps_right_inverse f (g$0) $ Suc k = 1 * g $ Suc k - g$0 * 1 $ Suc k" - by (simp add: fps_mult_nth fg(1)[symmetric] algebra_simps fg(2)[symmetric] sum_head_Suc) + by (simp add: fps_mult_nth fg(1)[symmetric] algebra_simps fg(2)[symmetric] sum.atLeast_Suc_atMost) with Suc show ?thesis by simp qed simp qed @@ -2116,7 +2116,7 @@ moreover have "fps_left_inverse ones 1 $ Suc m = ones_inv $ Suc m" proof (cases m) case (Suc k) thus ?thesis - using Suc m 1 by (simp add: ones_def ones_inv_def sum_head_Suc) + using Suc m 1 by (simp add: ones_def ones_inv_def sum.atLeast_Suc_atMost) qed (simp add: ones_def ones_inv_def) ultimately show ?thesis by simp qed (simp add: ones_inv_def) @@ -2183,7 +2183,7 @@ have f2_nth_simps: "f^2 $ 1 = - of_nat 2" "f^2 $ 2 = 1" "\n. n>2 \ f^2 $ n = 0" - by (simp_all add: power2_eq_square f_def fps_mult_nth sum_head_Suc) + by (simp_all add: power2_eq_square f_def fps_mult_nth sum.atLeast_Suc_atMost) show "fps_left_inverse (f^2) 1 = invf2" proof (intro fps_ext) @@ -3086,7 +3086,7 @@ of_nat (Suc n) * f$0 * g$(Suc n) + (\i=1..n. (of_nat (n - i + 1) + of_nat i) * f $ i * g $ (n - i + 1)) + of_nat (Suc n) * f$(Suc n) * g$0" - by (simp add: fps_mult_nth algebra_simps mult_of_nat_commute sum_head_Suc sum.distrib) + by (simp add: fps_mult_nth algebra_simps mult_of_nat_commute sum.atLeast_Suc_atMost sum.distrib) moreover have "\i\{1..n}. (of_nat (n - i + 1) + of_nat i) * f $ i * g $ (n - i + 1) = @@ -3103,7 +3103,7 @@ ultimately have "(f * fps_deriv g + fps_deriv f * g) $ n = (\i=0..Suc n. of_nat (Suc n) * f $ i * g $ (Suc n - i))" - by (simp add: sum_head_Suc) + by (simp add: sum.atLeast_Suc_atMost) with LHS show "fps_deriv (f * g) $ n = (f * fps_deriv g + fps_deriv f * g) $ n" by simp qed @@ -3413,7 +3413,7 @@ next case (Suc i) with 1 j have "\m\{0<..j}. a ^ i $ (j - m) = 0" by auto - with Suc a0 show ?thesis by (simp add: fps_mult_nth sum_head_Suc) + with Suc a0 show ?thesis by (simp add: fps_mult_nth sum.atLeast_Suc_atMost) qed qed @@ -3436,8 +3436,8 @@ have "\i\{Suc 1..Suc n}. a ^ n $ (Suc n - i) = 0" using a0 startsby_zero_power_prefix[of a n] by auto thus ?case - using a0 Suc sum_head_Suc[of 0 "Suc n" "\i. a $ i * a ^ n $ (Suc n - i)"] - sum_head_Suc[of 1 "Suc n" "\i. a $ i * a ^ n $ (Suc n - i)"] + using a0 Suc sum.atLeast_Suc_atMost[of 0 "Suc n" "\i. a $ i * a ^ n $ (Suc n - i)"] + sum.atLeast_Suc_atMost[of 1 "Suc n" "\i. a $ i * a ^ n $ (Suc n - i)"] by (simp add: fps_mult_nth) qed simp @@ -3806,8 +3806,8 @@ case (Suc m) hence "(f * g) $ n = g $ Suc m - g $ m" using fps_mult_nth[of f g "Suc m"] - sum_head_Suc[of 0 "Suc m" "\i. f $ i * g $ (Suc m - i)"] - sum_head_Suc[of 1 "Suc m" "\i. f $ i * g $ (Suc m - i)"] + sum.atLeast_Suc_atMost[of 0 "Suc m" "\i. f $ i * g $ (Suc m - i)"] + sum.atLeast_Suc_atMost[of 1 "Suc m" "\i. f $ i * g $ (Suc m - i)"] by (simp add: f_def) with Suc show ?thesis by (simp add: g_def) qed (simp add: f_def g_def) @@ -6368,7 +6368,7 @@ lemma sum_eq_if: "sum f {(n::nat) .. m} = (if m < n then 0 else f n + sum f {n+1 .. m})" apply simp apply (subst sum.insert[symmetric]) - apply (auto simp add: not_less sum_head_Suc) + apply (auto simp add: not_less sum.atLeast_Suc_atMost) done lemma pochhammer_rec_if: "pochhammer a n = (if n = 0 then 1 else a * pochhammer (a + 1) (n - 1))" diff -r c4f2cac288d2 -r 4005298550a6 src/HOL/Computational_Algebra/Polynomial.thy --- a/src/HOL/Computational_Algebra/Polynomial.thy Tue Apr 09 21:05:48 2019 +0100 +++ b/src/HOL/Computational_Algebra/Polynomial.thy Wed Apr 10 13:34:55 2019 +0100 @@ -1000,7 +1000,7 @@ next case (pCons a p n) then show ?case - by (cases n) (simp_all add: sum_atMost_Suc_shift del: sum_atMost_Suc) + by (cases n) (simp_all add: sum_atMost_Suc_shift del: sum.atMost_Suc) qed lemma degree_mult_le: "degree (p * q) \ degree p + degree q" diff -r c4f2cac288d2 -r 4005298550a6 src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Tue Apr 09 21:05:48 2019 +0100 +++ b/src/HOL/Decision_Procs/Approximation.thy Wed Apr 10 13:34:55 2019 +0100 @@ -1183,7 +1183,7 @@ by auto have sum_move0: "\k F. sum F {0.. k. F (Suc k)) {0.. n. (-1)^n *a n * x^n"] by auto qed diff -r c4f2cac288d2 -r 4005298550a6 src/HOL/Groups_Big.thy --- a/src/HOL/Groups_Big.thy Tue Apr 09 21:05:48 2019 +0100 +++ b/src/HOL/Groups_Big.thy Wed Apr 10 13:34:55 2019 +0100 @@ -106,6 +106,11 @@ ultimately show ?thesis by simp qed +lemma Int_Diff: + assumes "finite A" + shows "F g A = F g (A \ B) \<^bold>* F g (A - B)" + by (subst subset_diff [where B = "A - B"]) (auto simp: Diff_Diff_Int assms) + lemma setdiff_irrelevant: assumes "finite A" shows "F g (A - {x. g x = z}) = F g A" diff -r c4f2cac288d2 -r 4005298550a6 src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Tue Apr 09 21:05:48 2019 +0100 +++ b/src/HOL/Hilbert_Choice.thy Wed Apr 10 13:34:55 2019 +0100 @@ -43,6 +43,11 @@ subsection \Hilbert's Epsilon-operator\ +lemma Eps_cong: + assumes "\x. P x = Q x" + shows "Eps P = Eps Q" + using ext[of P Q, OF assms] by simp + text \ Easier to apply than \someI\ if the witness comes from an existential formula. diff -r c4f2cac288d2 -r 4005298550a6 src/HOL/Homology/Brouwer_Degree.thy --- a/src/HOL/Homology/Brouwer_Degree.thy Tue Apr 09 21:05:48 2019 +0100 +++ b/src/HOL/Homology/Brouwer_Degree.thy Wed Apr 10 13:34:55 2019 +0100 @@ -5,11 +5,6 @@ begin -lemma Eps_cong: - assumes "\x. P x = Q x" - shows "Eps P = Eps Q" - using ext[of P Q, OF assms] by simp - subsection\Reduced Homology\ definition reduced_homology_group :: "int \ 'a topology \ 'a chain set monoid" diff -r c4f2cac288d2 -r 4005298550a6 src/HOL/Homology/Invariance_of_Domain.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Homology/Invariance_of_Domain.thy Wed Apr 10 13:34:55 2019 +0100 @@ -0,0 +1,2429 @@ +section\Invariance of Domain\ + +theory Invariance_of_Domain + imports Brouwer_Degree + +begin + +subsection\Degree invariance mod 2 for map between pairs\ + +theorem Borsuk_odd_mapping_degree_step: + assumes cmf: "continuous_map (nsphere n) (nsphere n) f" + and f: "\x. x \ topspace(nsphere n) \ (f \ (\x i. -x i)) x = ((\x i. -x i) \ f) x" + and fim: "f ` (topspace(nsphere(n - Suc 0))) \ topspace(nsphere(n - Suc 0))" + shows "even (Brouwer_degree2 n f - Brouwer_degree2 (n - Suc 0) f)" +proof (cases "n = 0") + case False + define neg where "neg \ \x::nat\real. \i. -x i" + define upper where "upper \ \n. {x::nat\real. x n \ 0}" + define lower where "lower \ \n. {x::nat\real. x n \ 0}" + define equator where "equator \ \n. {x::nat\real. x n = 0}" + define usphere where "usphere \ \n. subtopology (nsphere n) (upper n)" + define lsphere where "lsphere \ \n. subtopology (nsphere n) (lower n)" + have [simp]: "neg x i = -x i" for x i + by (force simp: neg_def) + have equator_upper: "equator n \ upper n" + by (force simp: equator_def upper_def) + have upper_usphere: "subtopology (nsphere n) (upper n) = usphere n" + by (simp add: usphere_def) + let ?rhgn = "relative_homology_group n (nsphere n)" + let ?hi_ee = "hom_induced n (nsphere n) (equator n) (nsphere n) (equator n)" + interpret GE: comm_group "?rhgn (equator n)" + by simp + interpret HB: group_hom "?rhgn (equator n)" + "homology_group (int n - 1) (subtopology (nsphere n) (equator n))" + "hom_boundary n (nsphere n) (equator n)" + by (simp add: group_hom_axioms_def group_hom_def hom_boundary_hom) + interpret HIU: group_hom "?rhgn (equator n)" + "?rhgn (upper n)" + "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id" + by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom) + have subt_eq: "subtopology (nsphere n) {x. x n = 0} = nsphere (n - Suc 0)" + by (metis False Suc_pred le_zero_eq not_le subtopology_nsphere_equator) + then have equ: "subtopology (nsphere n) (equator n) = nsphere(n - Suc 0)" + "subtopology (lsphere n) (equator n) = nsphere(n - Suc 0)" + "subtopology (usphere n) (equator n) = nsphere(n - Suc 0)" + using False by (auto simp: lsphere_def usphere_def equator_def lower_def upper_def subtopology_subtopology simp flip: Collect_conj_eq cong: rev_conj_cong) + have cmr: "continuous_map (nsphere(n - Suc 0)) (nsphere(n - Suc 0)) f" + by (metis (no_types, lifting) IntE cmf fim continuous_map_from_subtopology continuous_map_in_subtopology equ(1) image_subset_iff topspace_subtopology) + + have "f x n = 0" if "x \ topspace (nsphere n)" "x n = 0" for x + proof - + have "x \ topspace (nsphere (n - Suc 0))" + by (simp add: that topspace_nsphere_minus1) + moreover have "topspace (nsphere n) \ {f. f n = 0} = topspace (nsphere (n - Suc 0))" + by (metis subt_eq topspace_subtopology) + ultimately show ?thesis + using cmr continuous_map_def by fastforce + qed + then have fimeq: "f ` (topspace (nsphere n) \ equator n) \ topspace (nsphere n) \ equator n" + using fim cmf by (auto simp: equator_def continuous_map_def image_subset_iff) + have "\k. continuous_map (powertop_real UNIV) euclideanreal (\x. - x k)" + by (metis UNIV_I continuous_map_product_projection continuous_map_minus) + then have cm_neg: "continuous_map (nsphere m) (nsphere m) neg" for m + by (force simp: nsphere continuous_map_in_subtopology neg_def continuous_map_componentwise_UNIV intro: continuous_map_from_subtopology) + then have cm_neg_lu: "continuous_map (lsphere n) (usphere n) neg" + by (auto simp: lsphere_def usphere_def lower_def upper_def continuous_map_from_subtopology continuous_map_in_subtopology) + have neg_in_top_iff: "neg x \ topspace(nsphere m) \ x \ topspace(nsphere m)" for m x + by (simp add: nsphere_def neg_def topspace_Euclidean_space) + obtain z where zcarr: "z \ carrier (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))" + and zeq: "subgroup_generated (reduced_homology_group (int n - 1) (nsphere (n - Suc 0))) {z} + = reduced_homology_group (int n - 1) (nsphere (n - Suc 0))" + using cyclic_reduced_homology_group_nsphere [of "int n - 1" "n - Suc 0"] by (auto simp: cyclic_group_def) + have "hom_boundary n (subtopology (nsphere n) {x. x n \ 0}) {x. x n = 0} + \ Group.iso (relative_homology_group n + (subtopology (nsphere n) {x. x n \ 0}) {x. x n = 0}) + (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))" + using iso_lower_hemisphere_reduced_homology_group [of "int n - 1" "n - Suc 0"] False by simp + then obtain gp where g: "group_isomorphisms + (relative_homology_group n (subtopology (nsphere n) {x. x n \ 0}) {x. x n = 0}) + (reduced_homology_group (int n - 1) (nsphere (n - Suc 0))) + (hom_boundary n (subtopology (nsphere n) {x. x n \ 0}) {x. x n = 0}) + gp" + by (auto simp: group.iso_iff_group_isomorphisms) + then interpret gp: group_hom "reduced_homology_group (int n - 1) (nsphere (n - Suc 0))" + "relative_homology_group n (subtopology (nsphere n) {x. x n \ 0}) {x. x n = 0}" gp + by (simp add: group_hom_axioms_def group_hom_def group_isomorphisms_def) + obtain zp where zpcarr: "zp \ carrier(relative_homology_group n (lsphere n) (equator n))" + and zp_z: "hom_boundary n (lsphere n) (equator n) zp = z" + and zp_sg: "subgroup_generated (relative_homology_group n (lsphere n) (equator n)) {zp} + = relative_homology_group n (lsphere n) (equator n)" + proof + show "gp z \ carrier (relative_homology_group n (lsphere n) (equator n))" + "hom_boundary n (lsphere n) (equator n) (gp z) = z" + using g zcarr by (auto simp: lsphere_def equator_def lower_def group_isomorphisms_def) + have giso: "gp \ Group.iso (reduced_homology_group (int n - 1) (nsphere (n - Suc 0))) + (relative_homology_group n (subtopology (nsphere n) {x. x n \ 0}) {x. x n = 0})" + by (metis (mono_tags, lifting) g group_isomorphisms_imp_iso group_isomorphisms_sym) + show "subgroup_generated (relative_homology_group n (lsphere n) (equator n)) {gp z} = + relative_homology_group n (lsphere n) (equator n)" + apply (rule monoid.equality) + using giso gp.subgroup_generated_by_image [of "{z}"] zcarr + by (auto simp: lsphere_def equator_def lower_def zeq gp.iso_iff) + qed + have hb_iso: "hom_boundary n (subtopology (nsphere n) {x. x n \ 0}) {x. x n = 0} + \ iso (relative_homology_group n (subtopology (nsphere n) {x. x n \ 0}) {x. x n = 0}) + (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))" + using iso_upper_hemisphere_reduced_homology_group [of "int n - 1" "n - Suc 0"] False by simp + then obtain gn where g: "group_isomorphisms + (relative_homology_group n (subtopology (nsphere n) {x. x n \ 0}) {x. x n = 0}) + (reduced_homology_group (int n - 1) (nsphere (n - Suc 0))) + (hom_boundary n (subtopology (nsphere n) {x. x n \ 0}) {x. x n = 0}) + gn" + by (auto simp: group.iso_iff_group_isomorphisms) + then interpret gn: group_hom "reduced_homology_group (int n - 1) (nsphere (n - Suc 0))" + "relative_homology_group n (subtopology (nsphere n) {x. x n \ 0}) {x. x n = 0}" gn + by (simp add: group_hom_axioms_def group_hom_def group_isomorphisms_def) + obtain zn where zncarr: "zn \ carrier(relative_homology_group n (usphere n) (equator n))" + and zn_z: "hom_boundary n (usphere n) (equator n) zn = z" + and zn_sg: "subgroup_generated (relative_homology_group n (usphere n) (equator n)) {zn} + = relative_homology_group n (usphere n) (equator n)" + proof + show "gn z \ carrier (relative_homology_group n (usphere n) (equator n))" + "hom_boundary n (usphere n) (equator n) (gn z) = z" + using g zcarr by (auto simp: usphere_def equator_def upper_def group_isomorphisms_def) + have giso: "gn \ Group.iso (reduced_homology_group (int n - 1) (nsphere (n - Suc 0))) + (relative_homology_group n (subtopology (nsphere n) {x. x n \ 0}) {x. x n = 0})" + by (metis (mono_tags, lifting) g group_isomorphisms_imp_iso group_isomorphisms_sym) + show "subgroup_generated (relative_homology_group n (usphere n) (equator n)) {gn z} = + relative_homology_group n (usphere n) (equator n)" + apply (rule monoid.equality) + using giso gn.subgroup_generated_by_image [of "{z}"] zcarr + by (auto simp: usphere_def equator_def upper_def zeq gn.iso_iff) + qed + let ?hi_lu = "hom_induced n (lsphere n) (equator n) (nsphere n) (upper n) id" + interpret gh_lu: group_hom "relative_homology_group n (lsphere n) (equator n)" "?rhgn (upper n)" ?hi_lu + by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom) + interpret gh_eef: group_hom "?rhgn (equator n)" "?rhgn (equator n)" "?hi_ee f" + by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom) + define wp where "wp \ ?hi_lu zp" + then have wpcarr: "wp \ carrier(?rhgn (upper n))" + by (simp add: hom_induced_carrier) + have "hom_induced n (nsphere n) {} (nsphere n) {x. x n \ 0} id + \ iso (reduced_homology_group n (nsphere n)) + (?rhgn {x. x n \ 0})" + using iso_reduced_homology_group_upper_hemisphere [of n n n] by auto + then have "carrier(?rhgn {x. x n \ 0}) + \ (hom_induced n (nsphere n) {} (nsphere n) {x. x n \ 0} id) + ` carrier(reduced_homology_group n (nsphere n))" + by (simp add: iso_iff) + then obtain vp where vpcarr: "vp \ carrier(reduced_homology_group n (nsphere n))" + and eqwp: "hom_induced n (nsphere n) {} (nsphere n) (upper n) id vp = wp" + using wpcarr by (auto simp: upper_def) + define wn where "wn \ hom_induced n (usphere n) (equator n) (nsphere n) (lower n) id zn" + then have wncarr: "wn \ carrier(?rhgn (lower n))" + by (simp add: hom_induced_carrier) + have "hom_induced n (nsphere n) {} (nsphere n) {x. x n \ 0} id + \ iso (reduced_homology_group n (nsphere n)) + (?rhgn {x. x n \ 0})" + using iso_reduced_homology_group_lower_hemisphere [of n n n] by auto + then have "carrier(?rhgn {x. x n \ 0}) + \ (hom_induced n (nsphere n) {} (nsphere n) {x. x n \ 0} id) + ` carrier(reduced_homology_group n (nsphere n))" + by (simp add: iso_iff) + then obtain vn where vpcarr: "vn \ carrier(reduced_homology_group n (nsphere n))" + and eqwp: "hom_induced n (nsphere n) {} (nsphere n) (lower n) id vn = wn" + using wncarr by (auto simp: lower_def) + define up where "up \ hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id zp" + then have upcarr: "up \ carrier(?rhgn (equator n))" + by (simp add: hom_induced_carrier) + define un where "un \ hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id zn" + then have uncarr: "un \ carrier(?rhgn (equator n))" + by (simp add: hom_induced_carrier) + have *: "(\(x, y). + hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id x + \\<^bsub>?rhgn (equator n)\<^esub> + hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id y) + \ Group.iso + (relative_homology_group n (lsphere n) (equator n) \\ + relative_homology_group n (usphere n) (equator n)) + (?rhgn (equator n))" + proof (rule conjunct1 [OF exact_sequence_sum_lemma [OF abelian_relative_homology_group]]) + show "hom_induced n (lsphere n) (equator n) (nsphere n) (upper n) id + \ Group.iso (relative_homology_group n (lsphere n) (equator n)) + (?rhgn (upper n))" + apply (simp add: lsphere_def usphere_def equator_def lower_def upper_def) + using iso_relative_homology_group_lower_hemisphere by blast + show "hom_induced n (usphere n) (equator n) (nsphere n) (lower n) id + \ Group.iso (relative_homology_group n (usphere n) (equator n)) + (?rhgn (lower n))" + apply (simp_all add: lsphere_def usphere_def equator_def lower_def upper_def) + using iso_relative_homology_group_upper_hemisphere by blast+ + show "exact_seq + ([?rhgn (lower n), + ?rhgn (equator n), + relative_homology_group n (lsphere n) (equator n)], + [hom_induced n (nsphere n) (equator n) (nsphere n) (lower n) id, + hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id])" + unfolding lsphere_def usphere_def equator_def lower_def upper_def + by (rule homology_exactness_triple_3) force + show "exact_seq + ([?rhgn (upper n), + ?rhgn (equator n), + relative_homology_group n (usphere n) (equator n)], + [hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id, + hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id])" + unfolding lsphere_def usphere_def equator_def lower_def upper_def + by (rule homology_exactness_triple_3) force + next + fix x + assume "x \ carrier (relative_homology_group n (lsphere n) (equator n))" + show "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id + (hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id x) = + hom_induced n (lsphere n) (equator n) (nsphere n) (upper n) id x" + by (simp add: hom_induced_compose' subset_iff lsphere_def usphere_def equator_def lower_def upper_def) + next + fix x + assume "x \ carrier (relative_homology_group n (usphere n) (equator n))" + show "hom_induced n (nsphere n) (equator n) (nsphere n) (lower n) id + (hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id x) = + hom_induced n (usphere n) (equator n) (nsphere n) (lower n) id x" + by (simp add: hom_induced_compose' subset_iff lsphere_def usphere_def equator_def lower_def upper_def) + qed + then have sb: "carrier (?rhgn (equator n)) + \ (\(x, y). + hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id x + \\<^bsub>?rhgn (equator n)\<^esub> + hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id y) + ` carrier (relative_homology_group n (lsphere n) (equator n) \\ + relative_homology_group n (usphere n) (equator n))" + by (simp add: iso_iff) + obtain a b::int + where up_ab: "?hi_ee f up + = up [^]\<^bsub>?rhgn (equator n)\<^esub> a\\<^bsub>?rhgn (equator n)\<^esub> un [^]\<^bsub>?rhgn (equator n)\<^esub> b" + proof - + have hiupcarr: "?hi_ee f up \ carrier(?rhgn (equator n))" + by (simp add: hom_induced_carrier) + obtain u v where u: "u \ carrier (relative_homology_group n (lsphere n) (equator n))" + and v: "v \ carrier (relative_homology_group n (usphere n) (equator n))" + and eq: "?hi_ee f up = + hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id u + \\<^bsub>?rhgn (equator n)\<^esub> + hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id v" + using subsetD [OF sb hiupcarr] by auto + have "u \ carrier (subgroup_generated (relative_homology_group n (lsphere n) (equator n)) {zp})" + by (simp_all add: u zp_sg) + then obtain a::int where a: "u = zp [^]\<^bsub>relative_homology_group n (lsphere n) (equator n)\<^esub> a" + by (metis group.carrier_subgroup_generated_by_singleton group_relative_homology_group rangeE zpcarr) + have ae: "hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id + (pow (relative_homology_group n (lsphere n) (equator n)) zp a) + = pow (?rhgn (equator n)) (hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id zp) a" + by (meson group_hom.hom_int_pow group_hom_axioms_def group_hom_def group_relative_homology_group hom_induced zpcarr) + have "v \ carrier (subgroup_generated (relative_homology_group n (usphere n) (equator n)) {zn})" + by (simp_all add: v zn_sg) + then obtain b::int where b: "v = zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub> b" + by (metis group.carrier_subgroup_generated_by_singleton group_relative_homology_group rangeE zncarr) + have be: "hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id + (zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub> b) + = hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id + zn [^]\<^bsub>relative_homology_group n (nsphere n) (equator n)\<^esub> b" + by (meson group_hom.hom_int_pow group_hom_axioms_def group_hom_def group_relative_homology_group hom_induced zncarr) + show thesis + proof + show "?hi_ee f up + = up [^]\<^bsub>?rhgn (equator n)\<^esub> a \\<^bsub>?rhgn (equator n)\<^esub> un [^]\<^bsub>?rhgn (equator n)\<^esub> b" + using a ae b be eq local.up_def un_def by auto + qed + qed + have "(hom_boundary n (nsphere n) (equator n) + \ hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id) zp = z" + using zp_z equ apply (simp add: lsphere_def naturality_hom_induced) + by (metis hom_boundary_carrier hom_induced_id) + then have up_z: "hom_boundary n (nsphere n) (equator n) up = z" + by (simp add: up_def) + have "(hom_boundary n (nsphere n) (equator n) + \ hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id) zn = z" + using zn_z equ apply (simp add: usphere_def naturality_hom_induced) + by (metis hom_boundary_carrier hom_induced_id) + then have un_z: "hom_boundary n (nsphere n) (equator n) un = z" + by (simp add: un_def) + have Bd_ab: "Brouwer_degree2 (n - Suc 0) f = a + b" + proof (rule Brouwer_degree2_unique_generator; use False int_ops in simp_all) + show "continuous_map (nsphere (n - Suc 0)) (nsphere (n - Suc 0)) f" + using cmr by auto + show "subgroup_generated (reduced_homology_group (int n - 1) (nsphere (n - Suc 0))) {z} = + reduced_homology_group (int n - 1) (nsphere (n - Suc 0))" + using zeq by blast + have "(hom_induced (int n - 1) (nsphere (n - Suc 0)) {} (nsphere (n - Suc 0)) {} f + \ hom_boundary n (nsphere n) (equator n)) up + = (hom_boundary n (nsphere n) (equator n) \ + ?hi_ee f) up" + using naturality_hom_induced [OF cmf fimeq, of n, symmetric] + by (simp add: subtopology_restrict equ fun_eq_iff) + also have "\ = hom_boundary n (nsphere n) (equator n) + (up [^]\<^bsub>relative_homology_group n (nsphere n) (equator n)\<^esub> + a \\<^bsub>relative_homology_group n (nsphere n) (equator n)\<^esub> + un [^]\<^bsub>relative_homology_group n (nsphere n) (equator n)\<^esub> b)" + by (simp add: o_def up_ab) + also have "\ = z [^]\<^bsub>reduced_homology_group (int n - 1) (nsphere (n - Suc 0))\<^esub> (a + b)" + using zcarr + apply (simp add: HB.hom_int_pow reduced_homology_group_def group.int_pow_subgroup_generated upcarr uncarr) + by (metis equ(1) group.int_pow_mult group_relative_homology_group hom_boundary_carrier un_z up_z) + finally show "hom_induced (int n - 1) (nsphere (n - Suc 0)) {} (nsphere (n - Suc 0)) {} f z = + z [^]\<^bsub>reduced_homology_group (int n - 1) (nsphere (n - Suc 0))\<^esub> (a + b)" + by (simp add: up_z) + qed + define u where "u \ up \\<^bsub>?rhgn (equator n)\<^esub> inv\<^bsub>?rhgn (equator n)\<^esub> un" + have ucarr: "u \ carrier (?rhgn (equator n))" + by (simp add: u_def uncarr upcarr) + then have "u [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 n f = u [^]\<^bsub>?rhgn (equator n)\<^esub> (a - b) + \ (GE.ord u) dvd a - b - Brouwer_degree2 n f" + by (simp add: GE.int_pow_eq) + moreover + have "GE.ord u = 0" + proof (clarsimp simp add: GE.ord_eq_0 ucarr) + fix d :: nat + assume "0 < d" + and "u [^]\<^bsub>?rhgn (equator n)\<^esub> d = singular_relboundary_set n (nsphere n) (equator n)" + then have "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id u [^]\<^bsub>?rhgn (upper n)\<^esub> d + = \\<^bsub>?rhgn (upper n)\<^esub>" + by (metis HIU.hom_one HIU.hom_nat_pow one_relative_homology_group ucarr) + moreover + have "?hi_lu + = hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id \ + hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id" + by (simp add: lsphere_def image_subset_iff equator_upper flip: hom_induced_compose) + then have p: "wp = hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id up" + by (simp add: local.up_def wp_def) + have n: "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id un = \\<^bsub>?rhgn (upper n)\<^esub>" + using homology_exactness_triple_3 [OF equator_upper, of n "nsphere n"] + using un_def zncarr by (auto simp: upper_usphere kernel_def) + have "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id u = wp" + unfolding u_def + using p n HIU.inv_one HIU.r_one uncarr upcarr by auto + ultimately have "(wp [^]\<^bsub>?rhgn (upper n)\<^esub> d) = \\<^bsub>?rhgn (upper n)\<^esub>" + by simp + moreover have "infinite (carrier (subgroup_generated (?rhgn (upper n)) {wp}))" + proof - + have "?rhgn (upper n) \ reduced_homology_group n (nsphere n)" + unfolding upper_def + using iso_reduced_homology_group_upper_hemisphere [of n n n] + by (blast intro: group.iso_sym group_reduced_homology_group is_isoI) + also have "\ \ integer_group" + by (simp add: reduced_homology_group_nsphere) + finally have iso: "?rhgn (upper n) \ integer_group" . + have "carrier (subgroup_generated (?rhgn (upper n)) {wp}) = carrier (?rhgn (upper n))" + using gh_lu.subgroup_generated_by_image [of "{zp}"] zpcarr HIU.carrier_subgroup_generated_subset + gh_lu.iso_iff iso_relative_homology_group_lower_hemisphere zp_sg + by (auto simp: lower_def lsphere_def upper_def equator_def wp_def) + then show ?thesis + using infinite_UNIV_int iso_finite [OF iso] by simp + qed + ultimately show False + using HIU.finite_cyclic_subgroup \0 < d\ wpcarr by blast + qed + ultimately have iff: "u [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 n f = u [^]\<^bsub>?rhgn (equator n)\<^esub> (a - b) + \ Brouwer_degree2 n f = a - b" + by auto + have "u [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 n f = ?hi_ee f u" + proof - + have ne: "topspace (nsphere n) \ equator n \ {}" + by (metis equ(1) nonempty_nsphere topspace_subtopology) + have eq1: "hom_boundary n (nsphere n) (equator n) u + = \\<^bsub>reduced_homology_group (int n - 1) (subtopology (nsphere n) (equator n))\<^esub>" + using one_reduced_homology_group u_def un_z uncarr up_z upcarr by force + then have uhom: "u \ hom_induced n (nsphere n) {} (nsphere n) (equator n) id ` + carrier (reduced_homology_group (int n) (nsphere n))" + using homology_exactness_reduced_1 [OF ne, of n] eq1 ucarr by (auto simp: kernel_def) + then obtain v where vcarr: "v \ carrier (reduced_homology_group (int n) (nsphere n))" + and ueq: "u = hom_induced n (nsphere n) {} (nsphere n) (equator n) id v" + by blast + interpret GH_hi: group_hom "homology_group n (nsphere n)" + "?rhgn (equator n)" + "hom_induced n (nsphere n) {} (nsphere n) (equator n) id" + by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom) + have poweq: "pow (homology_group n (nsphere n)) x i = pow (reduced_homology_group n (nsphere n)) x i" + for x and i::int + by (simp add: False un_reduced_homology_group) + have vcarr': "v \ carrier (homology_group n (nsphere n))" + using carrier_reduced_homology_group_subset vcarr by blast + have "u [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 n f + = hom_induced n (nsphere n) {} (nsphere n) (equator n) f v" + using vcarr vcarr' + by (simp add: ueq poweq hom_induced_compose' cmf flip: GH_hi.hom_int_pow Brouwer_degree2) + also have "\ = hom_induced n (nsphere n) (topspace(nsphere n) \ equator n) (nsphere n) (equator n) f + (hom_induced n (nsphere n) {} (nsphere n) (topspace(nsphere n) \ equator n) id v)" + using fimeq by (simp add: hom_induced_compose' cmf) + also have "\ = ?hi_ee f u" + by (metis hom_induced inf.left_idem ueq) + finally show ?thesis . + qed + moreover + interpret gh_een: group_hom "?rhgn (equator n)" "?rhgn (equator n)" "?hi_ee neg" + by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom) + have hi_up_eq_un: "?hi_ee neg up = un [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg" + proof - + have "?hi_ee neg (hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id zp) + = hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) (neg \ id) zp" + by (intro hom_induced_compose') (auto simp: lsphere_def equator_def cm_neg) + also have "\ = hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id + (hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg zp)" + by (subst hom_induced_compose' [OF cm_neg_lu]) (auto simp: usphere_def equator_def) + also have "hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg zp + = zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg" + proof - + let ?hb = "hom_boundary n (usphere n) (equator n)" + have eq: "subtopology (nsphere n) {x. x n \ 0} = usphere n \ {x. x n = 0} = equator n" + by (auto simp: usphere_def upper_def equator_def) + with hb_iso have inj: "inj_on (?hb) (carrier (relative_homology_group n (usphere n) (equator n)))" + by (simp add: iso_iff) + interpret hb_hom: group_hom "relative_homology_group n (usphere n) (equator n)" + "reduced_homology_group (int n - 1) (nsphere (n - Suc 0))" + "?hb" + using hb_iso iso_iff eq group_hom_axioms_def group_hom_def by fastforce + show ?thesis + proof (rule inj_onD [OF inj]) + have *: "hom_induced (int n - 1) (nsphere (n - Suc 0)) {} (nsphere (n - Suc 0)) {} neg z + = z [^]\<^bsub>homology_group (int n - 1) (nsphere (n - Suc 0))\<^esub> Brouwer_degree2 (n - Suc 0) neg" + using Brouwer_degree2 [of z "n - Suc 0" neg] False zcarr + by (simp add: int_ops group.int_pow_subgroup_generated reduced_homology_group_def) + have "?hb \ + hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg + = hom_induced (int n - 1) (nsphere (n - Suc 0)) {} (nsphere (n - Suc 0)) {} neg \ + hom_boundary n (lsphere n) (equator n)" + apply (subst naturality_hom_induced [OF cm_neg_lu]) + apply (force simp: equator_def neg_def) + by (simp add: equ) + then have "?hb + (hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg zp) + = (z [^]\<^bsub>homology_group (int n - 1) (nsphere (n - Suc 0))\<^esub> Brouwer_degree2 (n - Suc 0) neg)" + by (metis "*" comp_apply zp_z) + also have "\ = ?hb (zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub> + Brouwer_degree2 (n - Suc 0) neg)" + by (metis group.int_pow_subgroup_generated group_relative_homology_group hb_hom.hom_int_pow reduced_homology_group_def zcarr zn_z zncarr) + finally show "?hb (hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg zp) = + ?hb (zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub> + Brouwer_degree2 (n - Suc 0) neg)" by simp + qed (auto simp: hom_induced_carrier group.int_pow_closed zncarr) + qed + finally show ?thesis + by (metis (no_types, lifting) group_hom.hom_int_pow group_hom_axioms_def group_hom_def group_relative_homology_group hom_induced local.up_def un_def zncarr) + qed + have "continuous_map (nsphere (n - Suc 0)) (nsphere (n - Suc 0)) neg" + using cm_neg by blast + then have "homeomorphic_map (nsphere (n - Suc 0)) (nsphere (n - Suc 0)) neg" + apply (auto simp: homeomorphic_map_maps homeomorphic_maps_def) + apply (rule_tac x=neg in exI, auto) + done + then have Brouwer_degree2_21: "Brouwer_degree2 (n - Suc 0) neg ^ 2 = 1" + using Brouwer_degree2_homeomorphic_map power2_eq_1_iff by force + have hi_un_eq_up: "?hi_ee neg un = up [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg" (is "?f un = ?y") + proof - + have [simp]: "neg \ neg = id" + by force + have "?f (?f ?y) = ?y" + apply (subst hom_induced_compose' [OF cm_neg _ cm_neg]) + apply(force simp: equator_def) + apply (simp add: upcarr hom_induced_id_gen) + done + moreover have "?f ?y = un" + using upcarr apply (simp only: gh_een.hom_int_pow hi_up_eq_un) + by (metis (no_types, lifting) Brouwer_degree2_21 GE.group_l_invI GE.l_inv_ex group.int_pow_1 group.int_pow_pow power2_eq_1_iff uncarr zmult_eq_1_iff) + ultimately show "?f un = ?y" + by simp + qed + have "?hi_ee f un = un [^]\<^bsub>?rhgn (equator n)\<^esub> a \\<^bsub>?rhgn (equator n)\<^esub> up [^]\<^bsub>?rhgn (equator n)\<^esub> b" + proof - + let ?TE = "topspace (nsphere n) \ equator n" + have fneg: "(f \ neg) x = (neg \ f) x" if "x \ topspace (nsphere n)" for x + using f [OF that] by (force simp: neg_def) + have neg_im: "neg ` (topspace (nsphere n) \ equator n) \ topspace (nsphere n) \ equator n" + by (metis cm_neg continuous_map_image_subset_topspace equ(1) topspace_subtopology) + have 1: "hom_induced n (nsphere n) ?TE (nsphere n) ?TE f \ hom_induced n (nsphere n) ?TE (nsphere n) ?TE neg + = hom_induced n (nsphere n) ?TE (nsphere n) ?TE neg \ hom_induced n (nsphere n) ?TE (nsphere n) ?TE f" + using neg_im fimeq cm_neg cmf + apply (simp add: flip: hom_induced_compose del: hom_induced_restrict) + using fneg by (auto intro: hom_induced_eq) + have "(un [^]\<^bsub>?rhgn (equator n)\<^esub> a) \\<^bsub>?rhgn (equator n)\<^esub> (up [^]\<^bsub>?rhgn (equator n)\<^esub> b) + = un [^]\<^bsub>?rhgn (equator n)\<^esub> (Brouwer_degree2 (n - 1) neg * a * Brouwer_degree2 (n - 1) neg) + \\<^bsub>?rhgn (equator n)\<^esub> + up [^]\<^bsub>?rhgn (equator n)\<^esub> (Brouwer_degree2 (n - 1) neg * b * Brouwer_degree2 (n - 1) neg)" + proof - + have "Brouwer_degree2 (n - Suc 0) neg = 1 \ Brouwer_degree2 (n - Suc 0) neg = - 1" + using Brouwer_degree2_21 power2_eq_1_iff by blast + then show ?thesis + by fastforce + qed + also have "\ = ((un [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - 1) neg) [^]\<^bsub>?rhgn (equator n)\<^esub> a \\<^bsub>?rhgn (equator n)\<^esub> + (up [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - 1) neg) [^]\<^bsub>?rhgn (equator n)\<^esub> b) [^]\<^bsub>?rhgn (equator n)\<^esub> + Brouwer_degree2 (n - 1) neg" + by (simp add: GE.int_pow_distrib GE.int_pow_pow uncarr upcarr) + also have "\ = ?hi_ee neg (?hi_ee f up) [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg" + by (simp add: gh_een.hom_int_pow hi_un_eq_up hi_up_eq_un uncarr up_ab upcarr) + finally have 2: "(un [^]\<^bsub>?rhgn (equator n)\<^esub> a) \\<^bsub>?rhgn (equator n)\<^esub> (up [^]\<^bsub>?rhgn (equator n)\<^esub> b) + = ?hi_ee neg (?hi_ee f up) [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg" . + have "un = ?hi_ee neg up [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg" + by (metis (no_types, hide_lams) Brouwer_degree2_21 GE.int_pow_1 GE.int_pow_pow hi_up_eq_un power2_eq_1_iff uncarr zmult_eq_1_iff) + moreover have "?hi_ee f ((?hi_ee neg up) [^]\<^bsub>?rhgn (equator n)\<^esub> (Brouwer_degree2 (n - Suc 0) neg)) + = un [^]\<^bsub>?rhgn (equator n)\<^esub> a \\<^bsub>?rhgn (equator n)\<^esub> up [^]\<^bsub>?rhgn (equator n)\<^esub> b" + using 1 2 by (simp add: hom_induced_carrier gh_eef.hom_int_pow fun_eq_iff) + ultimately show ?thesis + by blast + qed + then have "?hi_ee f u = u [^]\<^bsub>?rhgn (equator n)\<^esub> (a - b)" + by (simp add: u_def upcarr uncarr up_ab GE.int_pow_diff GE.m_ac GE.int_pow_distrib GE.int_pow_inv GE.inv_mult_group) + ultimately + have "Brouwer_degree2 n f = a - b" + using iff by blast + with Bd_ab show ?thesis + by simp +qed simp + + +subsection \General Jordan-Brouwer separation theorem and invariance of dimension\ + +proposition relative_homology_group_Euclidean_complement_step: + assumes "closedin (Euclidean_space n) S" + shows "relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - S) + \ relative_homology_group (p + k) (Euclidean_space (n+k)) (topspace(Euclidean_space (n+k)) - S)" +proof - + have *: "relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - S) + \ relative_homology_group (p + 1) (Euclidean_space (Suc n)) (topspace(Euclidean_space (Suc n)) - {x \ S. x n = 0})" + (is "?lhs \ ?rhs") + if clo: "closedin (Euclidean_space (Suc n)) S" and cong: "\x y. \x \ S; \i. i \ n \ x i = y i\ \ y \ S" + for p n S + proof - + have Ssub: "S \ topspace (Euclidean_space (Suc n))" + by (meson clo closedin_def) + define lo where "lo \ {x \ topspace(Euclidean_space (Suc n)). x n < (if x \ S then 0 else 1)}" + define hi where "hi = {x \ topspace(Euclidean_space (Suc n)). x n > (if x \ S then 0 else -1)}" + have lo_hi_Int: "lo \ hi = {x \ topspace(Euclidean_space (Suc n)) - S. x n \ {-1<..<1}}" + by (auto simp: hi_def lo_def) + have lo_hi_Un: "lo \ hi = topspace(Euclidean_space (Suc n)) - {x \ S. x n = 0}" + by (auto simp: hi_def lo_def) + define ret where "ret \ \c::real. \x i. if i = n then c else x i" + have cm_ret: "continuous_map (powertop_real UNIV) (powertop_real UNIV) (ret t)" for t + by (auto simp: ret_def continuous_map_componentwise_UNIV intro: continuous_map_product_projection) + let ?ST = "\t. subtopology (Euclidean_space (Suc n)) {x. x n = t}" + define squashable where + "squashable \ \t S. \x t'. x \ S \ (x n \ t' \ t' \ t \ t \ t' \ t' \ x n) \ ret t' x \ S" + have squashable: "squashable t (topspace(Euclidean_space(Suc n)))" for t + by (simp add: squashable_def topspace_Euclidean_space ret_def) + have squashableD: "\squashable t S; x \ S; x n \ t' \ t' \ t \ t \ t' \ t' \ x n\ \ ret t' x \ S" for x t' t S + by (auto simp: squashable_def) + have "squashable 1 hi" + by (force simp: squashable_def hi_def ret_def topspace_Euclidean_space intro: cong) + have "squashable t UNIV" for t + by (force simp: squashable_def hi_def ret_def topspace_Euclidean_space intro: cong) + have squashable_0_lohi: "squashable 0 (lo \ hi)" + using Ssub + by (auto simp: squashable_def hi_def lo_def ret_def topspace_Euclidean_space intro: cong) + have rm_ret: "retraction_maps (subtopology (Euclidean_space (Suc n)) U) + (subtopology (Euclidean_space (Suc n)) {x. x \ U \ x n = t}) + (ret t) id" + if "squashable t U" for t U + unfolding retraction_maps_def + proof (intro conjI ballI) + show "continuous_map (subtopology (Euclidean_space (Suc n)) U) + (subtopology (Euclidean_space (Suc n)) {x \ U. x n = t}) (ret t)" + apply (simp add: cm_ret continuous_map_in_subtopology continuous_map_from_subtopology Euclidean_space_def) + using that by (fastforce simp: squashable_def ret_def) + next + show "continuous_map (subtopology (Euclidean_space (Suc n)) {x \ U. x n = t}) + (subtopology (Euclidean_space (Suc n)) U) id" + using continuous_map_in_subtopology by fastforce + show "ret t (id x) = x" + if "x \ topspace (subtopology (Euclidean_space (Suc n)) {x \ U. x n = t})" for x + using that by (simp add: topspace_Euclidean_space ret_def fun_eq_iff) + qed + have cm_snd: "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (powertop_real UNIV) S)) + euclideanreal (\x. snd x k)" for k::nat and S + using continuous_map_componentwise_UNIV continuous_map_into_fulltopology continuous_map_snd by fastforce + have cm_fstsnd: "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (powertop_real UNIV) S)) + euclideanreal (\x. fst x * snd x k)" for k::nat and S + by (intro continuous_intros continuous_map_into_fulltopology [OF continuous_map_fst] cm_snd) + have hw_sub: "homotopic_with (\k. k ` V \ V) (subtopology (Euclidean_space (Suc n)) U) + (subtopology (Euclidean_space (Suc n)) U) (ret t) id" + if "squashable t U" "squashable t V" for U V t + unfolding homotopic_with_def + proof (intro exI conjI allI ballI) + let ?h = "\(z,x). ret ((1 - z) * t + z * x n) x" + show "(\x. ?h (u, x)) ` V \ V" if "u \ {0..1}" for u + using that + by clarsimp (metis squashableD [OF \squashable t V\] convex_bound_le diff_ge_0_iff_ge eq_diff_eq' le_cases less_eq_real_def segment_bound_lemma) + have 1: "?h ` ({0..1} \ ({x. \i\Suc n. x i = 0} \ U)) \ U" + by clarsimp (metis squashableD [OF \squashable t U\] convex_bound_le diff_ge_0_iff_ge eq_diff_eq' le_cases less_eq_real_def segment_bound_lemma) + show "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (Euclidean_space (Suc n)) U)) + (subtopology (Euclidean_space (Suc n)) U) ?h" + apply (simp add: continuous_map_in_subtopology Euclidean_space_def subtopology_subtopology 1) + apply (auto simp: case_prod_unfold ret_def continuous_map_componentwise_UNIV) + apply (intro continuous_map_into_fulltopology [OF continuous_map_fst] cm_snd continuous_intros) + by (auto simp: cm_snd) + qed (auto simp: ret_def) + have cs_hi: "contractible_space(subtopology (Euclidean_space(Suc n)) hi)" + proof - + have "homotopic_with (\x. True) (?ST 1) (?ST 1) id (\x. (\i. if i = n then 1 else 0))" + apply (subst homotopic_with_sym) + apply (simp add: homotopic_with) + apply (rule_tac x="(\(z,x) i. if i=n then 1 else z * x i)" in exI) + apply (auto simp: Euclidean_space_def subtopology_subtopology continuous_map_in_subtopology case_prod_unfold continuous_map_componentwise_UNIV cm_fstsnd) + done + then have "contractible_space (?ST 1)" + unfolding contractible_space_def by metis + moreover have "?thesis = contractible_space (?ST 1)" + proof (intro deformation_retract_imp_homotopy_equivalent_space homotopy_equivalent_space_contractibility) + have "{x. \i\Suc n. x i = 0} \ {x \ hi. x n = 1} = {x. \i\Suc n. x i = 0} \ {x. x n = 1}" + by (auto simp: hi_def topspace_Euclidean_space) + then have eq: "subtopology (Euclidean_space (Suc n)) {x. x \ hi \ x n = 1} = ?ST 1" + by (simp add: Euclidean_space_def subtopology_subtopology) + show "homotopic_with (\x. True) (subtopology (Euclidean_space (Suc n)) hi) (subtopology (Euclidean_space (Suc n)) hi) (ret 1) id" + using hw_sub [OF \squashable 1 hi\ \squashable 1 UNIV\] eq by simp + show "retraction_maps (subtopology (Euclidean_space (Suc n)) hi) (?ST 1) (ret 1) id" + using rm_ret [OF \squashable 1 hi\] eq by simp + qed + ultimately show ?thesis by metis + qed + have "?lhs \ relative_homology_group p (Euclidean_space (Suc n)) (lo \ hi)" + proof (rule group.iso_sym [OF _ deformation_retract_imp_isomorphic_relative_homology_groups]) + have "{x. \i\Suc n. x i = 0} \ {x. x n = 0} = {x. \i\n. x i = (0::real)}" + by auto (metis le_less_Suc_eq not_le) + then have "?ST 0 = Euclidean_space n" + by (simp add: Euclidean_space_def subtopology_subtopology) + then show "retraction_maps (Euclidean_space (Suc n)) (Euclidean_space n) (ret 0) id" + using rm_ret [OF \squashable 0 UNIV\] by auto + then have "ret 0 x \ topspace (Euclidean_space n)" + if "x \ topspace (Euclidean_space (Suc n))" "-1 < x n" "x n < 1" for x + using that by (simp add: continuous_map_def retraction_maps_def) + then show "(ret 0) ` (lo \ hi) \ topspace (Euclidean_space n) - S" + by (auto simp: local.cong ret_def hi_def lo_def) + show "homotopic_with (\h. h ` (lo \ hi) \ lo \ hi) (Euclidean_space (Suc n)) (Euclidean_space (Suc n)) (ret 0) id" + using hw_sub [OF squashable squashable_0_lohi] by simp + qed (auto simp: lo_def hi_def Euclidean_space_def) + also have "\ \ relative_homology_group p (subtopology (Euclidean_space (Suc n)) hi) (lo \ hi)" + proof (rule group.iso_sym [OF _ isomorphic_relative_homology_groups_inclusion_contractible]) + show "contractible_space (subtopology (Euclidean_space (Suc n)) hi)" + by (simp add: cs_hi) + show "topspace (Euclidean_space (Suc n)) \ hi \ {}" + apply (simp add: hi_def topspace_Euclidean_space set_eq_iff) + apply (rule_tac x="\i. if i = n then 1 else 0" in exI, auto) + done + qed auto + also have "\ \ relative_homology_group p (subtopology (Euclidean_space (Suc n)) (lo \ hi)) lo" + proof - + have oo: "openin (Euclidean_space (Suc n)) {x \ topspace (Euclidean_space (Suc n)). x n \ A}" + if "open A" for A + proof (rule openin_continuous_map_preimage) + show "continuous_map (Euclidean_space (Suc n)) euclideanreal (\x. x n)" + proof - + have "\n f. continuous_map (product_topology f UNIV) (f (n::nat)) (\f. f n::real)" + by (simp add: continuous_map_product_projection) + then show ?thesis + using Euclidean_space_def continuous_map_from_subtopology + by (metis (mono_tags)) + qed + qed (auto intro: that) + have "openin (Euclidean_space(Suc n)) lo" + apply (simp add: openin_subopen [of _ lo]) + apply (simp add: lo_def, safe) + apply (force intro: oo [of "lessThan 0", simplified] open_Collect_less) + apply (rule_tac x="{x \ topspace(Euclidean_space(Suc n)). x n < 1} + \ (topspace(Euclidean_space(Suc n)) - S)" in exI) + using clo apply (force intro: oo [of "lessThan 1", simplified] open_Collect_less) + done + moreover have "openin (Euclidean_space(Suc n)) hi" + apply (simp add: openin_subopen [of _ hi]) + apply (simp add: hi_def, safe) + apply (force intro: oo [of "greaterThan 0", simplified] open_Collect_less) + apply (rule_tac x="{x \ topspace(Euclidean_space(Suc n)). x n > -1} + \ (topspace(Euclidean_space(Suc n)) - S)" in exI) + using clo apply (force intro: oo [of "greaterThan (-1)", simplified] open_Collect_less) + done + ultimately + have *: "subtopology (Euclidean_space (Suc n)) (lo \ hi) closure_of + (topspace (subtopology (Euclidean_space (Suc n)) (lo \ hi)) - hi) + \ subtopology (Euclidean_space (Suc n)) (lo \ hi) interior_of lo" + by (metis (no_types, lifting) Diff_idemp Diff_subset_conv Un_commute Un_upper2 closure_of_interior_of interior_of_closure_of interior_of_complement interior_of_eq lo_hi_Un openin_Un openin_open_subtopology topspace_subtopology_subset) + have eq: "((lo \ hi) \ (lo \ hi - (topspace (Euclidean_space (Suc n)) \ (lo \ hi) - hi))) = hi" + "(lo - (topspace (Euclidean_space (Suc n)) \ (lo \ hi) - hi)) = lo \ hi" + by (auto simp: lo_def hi_def Euclidean_space_def) + show ?thesis + using homology_excision_axiom [OF *, of "lo \ hi" p] + by (force simp: subtopology_subtopology eq is_iso_def) + qed + also have "\ \ relative_homology_group (p + 1 - 1) (subtopology (Euclidean_space (Suc n)) (lo \