# HG changeset patch # User paulson # Date 1554820274 -3600 # Node ID 10fe23659be3f7303ae2144ad0fd4b10d6604e02 # Parent 23c0dfa39dced453d2e1252da94cba512f5c3aa9# Parent eca8611201e9c4b4332640a15640e8398755e3ca merged diff -r 23c0dfa39dce -r 10fe23659be3 NEWS --- a/NEWS Tue Apr 09 14:17:29 2019 +0200 +++ b/NEWS Tue Apr 09 15:31:14 2019 +0100 @@ -233,7 +233,10 @@ * Session HOL-Number_Theory: More material on residue rings in Carmichael's function, primitive roots, more properties for "ord". -* Session HOL-Analysis: More material and better organization. +* Session HOL-Analysis: Better organization and much more material, +including algebraic topology. + +* Session HOL-Algebra: Much more material on group theory. * Session HOL-SPARK: .prv files are no longer written to the file-system, but exported to the session database. Results may be diff -r 23c0dfa39dce -r 10fe23659be3 src/HOL/Analysis/Abstract_Euclidean_Space.thy --- a/src/HOL/Analysis/Abstract_Euclidean_Space.thy Tue Apr 09 14:17:29 2019 +0200 +++ b/src/HOL/Analysis/Abstract_Euclidean_Space.thy Tue Apr 09 15:31:14 2019 +0100 @@ -89,6 +89,51 @@ unfolding Euclidean_space_def continuous_map_in_subtopology 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_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" + 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" + 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" + by (simp add: Euclidean_space_def euclidean_product_topology) +qed + +lemma cm_Euclidean_space_iff_continuous_on: + "continuous_map (subtopology (Euclidean_space m) S) (Euclidean_space n) f + \ continuous_on (topspace (subtopology (Euclidean_space m) S)) f \ + f ` (topspace (subtopology (Euclidean_space m) S)) \ topspace (Euclidean_space n)" + (is "?P \ ?Q \ ?R") +proof - + have ?Q if ?P + proof - + have "\n. Euclidean_space n = top_of_set {f. \m\n. f m = 0}" + by (simp add: Euclidean_space_def euclidean_product_topology) + with that show ?thesis + by (simp add: subtopology_subtopology) + qed + moreover + have ?R if ?P + using that by (simp add: image_subset_iff continuous_map_def) + moreover + have ?P if ?Q ?R + proof - + have "continuous_map (top_of_set (topspace (subtopology (subtopology (powertop_real UNIV) {f. \n\m. f n = 0}) S))) (top_of_set (topspace (subtopology (powertop_real UNIV) {f. \na\n. f na = 0}))) f" + using Euclidean_space_def that by auto + then show ?thesis + by (simp add: Euclidean_space_def euclidean_product_topology subtopology_subtopology) + qed + ultimately show ?thesis + by auto +qed + lemma homeomorphic_Euclidean_space_product_topology: "Euclidean_space n homeomorphic_space product_topology (\i. euclideanreal) {.. n = 0" by (auto simp: homeomorphic_compact_space [OF homeomorphic_Euclidean_space_product_topology] compact_space_product_topology) + subsection\n-dimensional spheres\ definition nsphere where diff -r 23c0dfa39dce -r 10fe23659be3 src/HOL/Analysis/Abstract_Topology.thy --- a/src/HOL/Analysis/Abstract_Topology.thy Tue Apr 09 14:17:29 2019 +0200 +++ b/src/HOL/Analysis/Abstract_Topology.thy Tue Apr 09 15:31:14 2019 +0100 @@ -2728,7 +2728,7 @@ "X homeomorphic_space Y \ Y homeomorphic_space X" unfolding homeomorphic_space_def by (metis homeomorphic_maps_sym) -lemma homeomorphic_space_trans: +lemma homeomorphic_space_trans [trans]: "\X1 homeomorphic_space X2; X2 homeomorphic_space X3\ \ X1 homeomorphic_space X3" unfolding homeomorphic_space_def by (metis homeomorphic_maps_compose) diff -r 23c0dfa39dce -r 10fe23659be3 src/HOL/Analysis/Analysis.thy diff -r 23c0dfa39dce -r 10fe23659be3 src/HOL/Analysis/Convex.thy --- a/src/HOL/Analysis/Convex.thy Tue Apr 09 14:17:29 2019 +0200 +++ b/src/HOL/Analysis/Convex.thy Tue Apr 09 15:31:14 2019 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/Analysis/Convex_Euclidean_Space.thy +(* Title: HOL/Analysis/Convex.thy Author: L C Paulson, University of Cambridge Author: Robert Himmelmann, TU Muenchen Author: Bogdan Grechuk, University of Edinburgh diff -r 23c0dfa39dce -r 10fe23659be3 src/HOL/Analysis/Function_Topology.thy --- a/src/HOL/Analysis/Function_Topology.thy Tue Apr 09 14:17:29 2019 +0200 +++ b/src/HOL/Analysis/Function_Topology.thy Tue Apr 09 15:31:14 2019 +0100 @@ -642,6 +642,17 @@ shows "continuous_on (A \ S) f \ (\i. continuous_on (A \ S) (\x. f x i))" by (auto simp: continuous_on_product_then_coordinatewise continuous_on_coordinatewise_then_product) +lemma continuous_map_span_sum: + fixes B :: "'a::real_inner set" + assumes biB: "\i. i \ I \ b i \ B" + shows "continuous_map euclidean (top_of_set (span B)) (\x. \i\I. x i *\<^sub>R b i)" +proof (rule continuous_map_euclidean_top_of_set) + show "(\x. \i\I. x i *\<^sub>R b i) -` span B = UNIV" + by auto (meson biB lessThan_iff span_base span_scale span_sum) + show "continuous_on UNIV (\x. \i\ I. x i *\<^sub>R b i)" + by (intro continuous_intros) auto +qed + subsubsection%important \Topological countability for product spaces\ text \The next two lemmas are useful to prove first or second countability @@ -867,7 +878,6 @@ apply standard using product_topology_countable_basis topological_basis_imp_subbasis by auto - subsection \Metrics on product spaces\ @@ -1242,7 +1252,7 @@ qed instance "fun" :: (countable, polish_space) polish_space -by standard + by standard subsection\The Alexander subbase theorem\ diff -r 23c0dfa39dce -r 10fe23659be3 src/HOL/Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue Apr 09 14:17:29 2019 +0200 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue Apr 09 15:31:14 2019 +0100 @@ -34,6 +34,9 @@ subsection \Continuity of the representation WRT an orthogonal basis\ +lemma orthogonal_Basis: "pairwise orthogonal Basis" + by (simp add: inner_not_same_Basis orthogonal_def pairwise_def) + lemma representation_bound: fixes B :: "'N::real_inner set" assumes "finite B" "independent B" "b \ B" and orth: "pairwise orthogonal B" diff -r 23c0dfa39dce -r 10fe23659be3 src/HOL/Homology/Homology.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Homology/Homology.thy Tue Apr 09 15:31:14 2019 +0100 @@ -0,0 +1,6 @@ +theory Homology + imports + Simplices +begin + +end diff -r 23c0dfa39dce -r 10fe23659be3 src/HOL/Homology/Simplices.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Homology/Simplices.thy Tue Apr 09 15:31:14 2019 +0100 @@ -0,0 +1,2785 @@ +section\Homology, I: Simplices\ + +theory "Simplices" + imports "HOL-Analysis.Abstract_Euclidean_Space" "HOL-Algebra.Free_Abelian_Groups" + +begin +subsection\Standard simplices, all of which are topological subspaces of @{text"R^n"}. \ + +type_synonym 'a chain = "((nat \ real) \ 'a) \\<^sub>0 int" + +definition standard_simplex :: "nat \ (nat \ real) set" where + "standard_simplex p \ + {x. (\i. 0 \ x i \ x i \ 1) \ (\i>p. x i = 0) \ (\i\p. x i) = 1}" + +lemma topspace_standard_simplex: + "topspace(subtopology (powertop_real UNIV) (standard_simplex p)) + = standard_simplex p" + by simp + +lemma basis_in_standard_simplex [simp]: + "(\j. if j = i then 1 else 0) \ standard_simplex p \ i \ p" + by (auto simp: standard_simplex_def) + +lemma nonempty_standard_simplex: "standard_simplex p \ {}" + using basis_in_standard_simplex by blast + +lemma standard_simplex_0: "standard_simplex 0 = {(\j. if j = 0 then 1 else 0)}" + by (auto simp: standard_simplex_def) + +lemma standard_simplex_mono: + assumes "p \ q" + shows "standard_simplex p \ standard_simplex q" + using assms +proof (clarsimp simp: standard_simplex_def) + fix x :: "nat \ real" + assume "\i. 0 \ x i \ x i \ 1" and "\i>p. x i = 0" and "sum x {..p} = 1" + then show "sum x {..q} = 1" + using sum.mono_neutral_left [of "{..q}" "{..p}" x] assms by auto +qed + +lemma closedin_standard_simplex: + "closedin (powertop_real UNIV) (standard_simplex p)" + (is "closedin ?X ?S") +proof - + have eq: "standard_simplex p = + (\i. {x. x \ topspace ?X \ x i \ {0..1}}) \ + (\i \ {p<..}. {x \ topspace ?X. x i \ {0}}) \ + {x \ topspace ?X. (\i\p. x i) \ {1}}" + by (auto simp: standard_simplex_def topspace_product_topology) + show ?thesis + unfolding eq + by (rule closedin_Int closedin_Inter continuous_map_sum + continuous_map_product_projection closedin_continuous_map_preimage | force | clarify)+ +qed + +lemma standard_simplex_01: "standard_simplex p \ UNIV \\<^sub>E {0..1}" + using standard_simplex_def by auto + +lemma compactin_standard_simplex: + "compactin (powertop_real UNIV) (standard_simplex p)" + apply (rule closed_compactin [where K = "PiE UNIV (\i. {0..1})"]) + apply (simp_all add: compactin_PiE standard_simplex_01 closedin_standard_simplex) + done + +lemma convex_standard_simplex: + "\x \ standard_simplex p; y \ standard_simplex p; + 0 \ u; u \ 1\ + \ (\i. (1 - u) * x i + u * y i) \ standard_simplex p" + by (simp add: standard_simplex_def sum.distrib convex_bound_le flip: sum_distrib_left) + +lemma path_connectedin_standard_simplex: + "path_connectedin (powertop_real UNIV) (standard_simplex p)" +proof - + define g where "g \ \x y::nat\real. \u i. (1 - u) * x i + u * y i" + have 1: "continuous_map + (subtopology euclideanreal {0..1}) (powertop_real UNIV) + (g x y)" + if "x \ standard_simplex p" "y \ standard_simplex p" for x y + unfolding g_def continuous_map_componentwise + by (force intro: continuous_intros) + have 2: "g x y ` {0..1} \ standard_simplex p" "g x y 0 = x" "g x y 1 = y" + if "x \ standard_simplex p" "y \ standard_simplex p" for x y + using that by (auto simp: convex_standard_simplex g_def) + show ?thesis + unfolding path_connectedin_def path_connected_space_def pathin_def + apply (simp add: topspace_standard_simplex topspace_product_topology continuous_map_in_subtopology) + by (metis 1 2) +qed + +lemma connectedin_standard_simplex: + "connectedin (powertop_real UNIV) (standard_simplex p)" + by (simp add: path_connectedin_imp_connectedin path_connectedin_standard_simplex) + +subsection\Face map\ + +definition simplical_face :: "nat \ (nat \ 'a) \ nat \ 'a::comm_monoid_add" where + "simplical_face k x \ \i. if i < k then x i else if i = k then 0 else x(i -1)" + +lemma simplical_face_in_standard_simplex: + assumes "1 \ p" "k \ p" "x \ standard_simplex (p - Suc 0)" + shows "(simplical_face k x) \ standard_simplex p" +proof - + have x01: "\i. 0 \ x i \ x i \ 1" and sumx: "sum x {..p - Suc 0} = 1" + using assms by (auto simp: standard_simplex_def simplical_face_def) + have gg: "\g. sum g {..p} = sum g {..k \ p\ sum.union_disjoint [of "{..i\p. if i < k then x i else if i = k then 0 else x (i -1)) + = (\i < k. x i) + (\i \ {k..p}. if i = k then 0 else x (i -1))" + by (simp add: gg) + consider "k \ p - Suc 0" | "k = p" + using \k \ p\ by linarith + then have "(\i\p. if i < k then x i else if i = k then 0 else x (i -1)) = 1" + proof cases + case 1 + have [simp]: "Suc (p - Suc 0) = p" + using \1 \ p\ by auto + have "(\i = k..p. if i = k then 0 else x (i -1)) = (\i = k+1..p. if i = k then 0 else x (i -1))" + by (rule sum.mono_neutral_right) auto + also have "\ = (\i = k+1..p. x (i -1))" + by simp + also have "\ = (\i = k..p-1. x i)" + using sum.atLeastAtMost_reindex [of Suc k "p-1" "\i. x (i - Suc 0)"] 1 by simp + finally have eq2: "(\i = k..p. if i = k then 0 else x (i -1)) = (\i = k..p-1. x i)" . + with 1 show ?thesis + apply (simp add: eq eq2) + by (metis (mono_tags, lifting) One_nat_def assms(3) finite_atLeastAtMost finite_lessThan ivl_disj_int(4) ivl_disj_un(10) mem_Collect_eq standard_simplex_def sum.union_disjoint) + next + case 2 + have [simp]: "({..p} \ {x. x < p}) = {..p - Suc 0}" + using assms by auto + have "(\i\p. if i < p then x i else if i = k then 0 else x (i -1)) = (\i\p. if i < p then x i else 0)" + by (rule sum.cong) (auto simp: 2) + also have "\ = sum x {..p-1}" + by (simp add: sum.If_cases) + also have "\ = 1" + by (simp add: sumx) + finally show ?thesis + using 2 by simp + qed + then show ?thesis + using assms by (auto simp: standard_simplex_def simplical_face_def) +qed + +subsection\Singular simplices, forcing canonicity outside the intended domain\ + +definition singular_simplex :: "nat \ 'a topology \ ((nat \ real) \ 'a) \ bool" where + "singular_simplex p X f \ + continuous_map(subtopology (powertop_real UNIV) (standard_simplex p)) X f + \ f \ extensional (standard_simplex p)" + +abbreviation singular_simplex_set :: "nat \ 'a topology \ ((nat \ real) \ 'a) set" where + "singular_simplex_set p X \ Collect (singular_simplex p X)" + +lemma singular_simplex_empty: + "topspace X = {} \ \ singular_simplex p X f" + by (simp add: singular_simplex_def continuous_map nonempty_standard_simplex) + +lemma singular_simplex_mono: + "\singular_simplex p (subtopology X T) f; T \ S\ \ singular_simplex p (subtopology X S) f" + by (auto simp: singular_simplex_def continuous_map_in_subtopology) + +lemma singular_simplex_subtopology: + "singular_simplex p (subtopology X S) f \ + singular_simplex p X f \ f ` (standard_simplex p) \ S" + by (auto simp: singular_simplex_def continuous_map_in_subtopology) + +subsubsection\Singular face\ + +definition singular_face :: "nat \ nat \ ((nat \ real) \ 'a) \ (nat \ real) \ 'a" + where "singular_face p k f \ restrict (f \ simplical_face k) (standard_simplex (p - Suc 0))" + +lemma singular_simplex_singular_face: + assumes f: "singular_simplex p X f" and "1 \ p" "k \ p" + shows "singular_simplex (p - Suc 0) X (singular_face p k f)" +proof - + let ?PT = "(powertop_real UNIV)" + have 0: "simplical_face k ` standard_simplex (p - Suc 0) \ standard_simplex p" + using assms simplical_face_in_standard_simplex by auto + have 1: "continuous_map (subtopology ?PT (standard_simplex (p - Suc 0))) + (subtopology ?PT (standard_simplex p)) + (simplical_face k)" + proof (clarsimp simp add: continuous_map_in_subtopology simplical_face_in_standard_simplex continuous_map_componentwise 0) + fix i + have "continuous_map ?PT euclideanreal (\x. if i < k then x i else if i = k then 0 else x (i -1))" + by (auto intro: continuous_map_product_projection) + then show "continuous_map (subtopology ?PT (standard_simplex (p - Suc 0))) euclideanreal + (\x. simplical_face k x i)" + by (simp add: simplical_face_def continuous_map_from_subtopology) + qed + have 2: "continuous_map (subtopology ?PT (standard_simplex p)) X f" + using assms(1) singular_simplex_def by blast + show ?thesis + by (simp add: singular_simplex_def singular_face_def continuous_map_compose [OF 1 2]) +qed + + +subsection\Singular chains\ + +definition singular_chain :: "[nat, 'a topology, 'a chain] \ bool" + where "singular_chain p X c \ Poly_Mapping.keys c \ singular_simplex_set p X" + +abbreviation singular_chain_set :: "[nat, 'a topology] \ ('a chain) set" + where "singular_chain_set p X \ Collect (singular_chain p X)" + +lemma singular_chain_empty: + "topspace X = {} \ singular_chain p X c \ c = 0" + by (auto simp: singular_chain_def singular_simplex_empty subset_eq poly_mapping_eqI) + +lemma singular_chain_mono: + "\singular_chain p (subtopology X T) c; T \ S\ + \ singular_chain p (subtopology X S) c" + unfolding singular_chain_def using singular_simplex_mono by blast + +lemma singular_chain_subtopology: + "singular_chain p (subtopology X S) c \ + singular_chain p X c \ (\f \ Poly_Mapping.keys c. f ` (standard_simplex p) \ S)" + unfolding singular_chain_def + by (fastforce simp add: singular_simplex_subtopology subset_eq) + +lemma singular_chain_0 [iff]: "singular_chain p X 0" + by (auto simp: singular_chain_def) + +lemma singular_chain_of: + "singular_chain p X (frag_of c) \ singular_simplex p X c" + by (auto simp: singular_chain_def) + +lemma singular_chain_cmul: + "singular_chain p X c \ singular_chain p X (frag_cmul a c)" + by (auto simp: singular_chain_def) + +lemma singular_chain_minus: + "singular_chain p X (-c) \ singular_chain p X c" + by (auto simp: singular_chain_def) + +lemma singular_chain_add: + "\singular_chain p X a; singular_chain p X b\ \ singular_chain p X (a+b)" + unfolding singular_chain_def + using keys_add [of a b] by blast + +lemma singular_chain_diff: + "\singular_chain p X a; singular_chain p X b\ \ singular_chain p X (a-b)" + unfolding singular_chain_def + using keys_diff [of a b] by blast + +lemma singular_chain_sum: + "(\i. i \ I \ singular_chain p X (f i)) \ singular_chain p X (\i\I. f i)" + unfolding singular_chain_def + using keys_sum [of f I] by blast + +lemma singular_chain_extend: + "(\c. c \ Poly_Mapping.keys x \ singular_chain p X (f c)) + \ singular_chain p X (frag_extend f x)" + by (simp add: frag_extend_def singular_chain_cmul singular_chain_sum) + +subsection\Boundary homomorphism for singular chains\ + +definition chain_boundary :: "nat \ ('a chain) \ 'a chain" + where "chain_boundary p c \ + (if p = 0 then 0 else + frag_extend (\f. (\k\p. frag_cmul ((-1) ^ k) (frag_of(singular_face p k f)))) c)" + +lemma singular_chain_boundary: + "singular_chain p X c + \ singular_chain (p - Suc 0) X (chain_boundary p c)" + unfolding chain_boundary_def + apply (clarsimp intro!: singular_chain_extend singular_chain_sum singular_chain_cmul) + apply (auto simp: singular_chain_def intro: singular_simplex_singular_face) + done + +lemma singular_chain_boundary_alt: + "singular_chain (Suc p) X c \ singular_chain p X (chain_boundary (Suc p) c)" + using singular_chain_boundary by force + +lemma chain_boundary_0 [simp]: "chain_boundary p 0 = 0" + by (simp add: chain_boundary_def) + +lemma chain_boundary_cmul: + "chain_boundary p (frag_cmul k c) = frag_cmul k (chain_boundary p c)" + by (auto simp: chain_boundary_def frag_extend_cmul) + +lemma chain_boundary_minus: + "chain_boundary p (- c) = - (chain_boundary p c)" + by (metis chain_boundary_cmul frag_cmul_minus_one) + +lemma chain_boundary_add: + "chain_boundary p (a+b) = chain_boundary p a + chain_boundary p b" + by (simp add: chain_boundary_def frag_extend_add) + +lemma chain_boundary_diff: + "chain_boundary p (a-b) = chain_boundary p a - chain_boundary p b" + using chain_boundary_add [of p a "-b"] + by (simp add: chain_boundary_minus) + +lemma chain_boundary_sum: + "chain_boundary p (sum g I) = sum (chain_boundary p \ g) I" + by (induction I rule: infinite_finite_induct) (simp_all add: chain_boundary_add) + +lemma chain_boundary_sum': + "finite I \ chain_boundary p (sum' g I) = sum' (chain_boundary p \ g) I" + by (induction I rule: finite_induct) (simp_all add: chain_boundary_add) + +lemma chain_boundary_of: + "chain_boundary p (frag_of f) = + (if p = 0 then 0 + else (\k\p. frag_cmul ((-1) ^ k) (frag_of(singular_face p k f))))" + by (simp add: chain_boundary_def) + +subsection\Factoring out chains in a subtopology for relative homology\ + +definition mod_subset + where "mod_subset p X \ {(a,b). singular_chain p X (a - b)}" + +lemma mod_subset_empty [simp]: + "(a,b) \ (mod_subset p (subtopology X {})) \ a = b" + by (simp add: mod_subset_def singular_chain_empty topspace_subtopology) + +lemma mod_subset_refl [simp]: "(c,c) \ mod_subset p X" + by (auto simp: mod_subset_def) + +lemma mod_subset_cmul: + "(a,b) \ (mod_subset p X) \ (frag_cmul k a, frag_cmul k b) \ (mod_subset p X)" + apply (simp add: mod_subset_def) + by (metis add_diff_cancel diff_add_cancel frag_cmul_distrib2 singular_chain_cmul) + +lemma mod_subset_add: + "\(c1,c2) \ (mod_subset p X); (d1,d2) \ (mod_subset p X)\ + \ (c1+d1, c2+d2) \ (mod_subset p X)" + apply (simp add: mod_subset_def) + by (simp add: add_diff_add singular_chain_add) + +subsection\Relative cycles $Z_pX (S)$ where $X$ is a topology and $S$ a subset \ + +definition singular_relcycle :: "nat \ 'a topology \ 'a set \ ('a chain) \ bool" + where "singular_relcycle p X S \ + \c. singular_chain p X c \ (chain_boundary p c, 0) \ mod_subset (p-1) (subtopology X S)" + +abbreviation singular_relcycle_set + where "singular_relcycle_set p X S \ Collect (singular_relcycle p X S)" + +lemma singular_relcycle_restrict [simp]: + "singular_relcycle p X (topspace X \ S) = singular_relcycle p X S" +proof - + have eq: "subtopology X (topspace X \ S) = subtopology X S" + by (metis subtopology_subtopology subtopology_topspace) + show ?thesis + by (force simp: singular_relcycle_def eq) +qed + +lemma singular_relcycle: + "singular_relcycle p X S c \ + singular_chain p X c \ singular_chain (p-1) (subtopology X S) (chain_boundary p c)" + by (simp add: singular_relcycle_def mod_subset_def) + +lemma singular_relcycle_0 [simp]: "singular_relcycle p X S 0" + by (auto simp: singular_relcycle_def) + +lemma singular_relcycle_cmul: + "singular_relcycle p X S c \ singular_relcycle p X S (frag_cmul k c)" + by (auto simp: singular_relcycle_def chain_boundary_cmul dest: singular_chain_cmul mod_subset_cmul) + +lemma singular_relcycle_minus: + "singular_relcycle p X S (-c) \ singular_relcycle p X S c" + by (simp add: chain_boundary_minus singular_chain_minus singular_relcycle) + +lemma singular_relcycle_add: + "\singular_relcycle p X S a; singular_relcycle p X S b\ + \ singular_relcycle p X S (a+b)" + by (simp add: singular_relcycle_def chain_boundary_add mod_subset_def singular_chain_add) + +lemma singular_relcycle_sum: + "\\i. i \ I \ singular_relcycle p X S (f i)\ + \ singular_relcycle p X S (sum f I)" + by (induction I rule: infinite_finite_induct) (auto simp: singular_relcycle_add) + +lemma singular_relcycle_diff: + "\singular_relcycle p X S a; singular_relcycle p X S b\ + \ singular_relcycle p X S (a-b)" + by (metis singular_relcycle_add singular_relcycle_minus uminus_add_conv_diff) + +lemma singular_cycle: + "singular_relcycle p X {} c \ singular_chain p X c \ chain_boundary p c = 0" + by (simp add: singular_relcycle_def) + +lemma singular_cycle_mono: + "\singular_relcycle p (subtopology X T) {} c; T \ S\ + \ singular_relcycle p (subtopology X S) {} c" + by (auto simp: singular_cycle elim: singular_chain_mono) + + +subsection\Relative boundaries $B_p X S$, where $X$ is a topology and $S$ a subset.\ + +definition singular_relboundary :: "nat \ 'a topology \ 'a set \ ('a chain) \ bool" + where + "singular_relboundary p X S \ + \c. \d. singular_chain (Suc p) X d \ (chain_boundary (Suc p) d, c) \ (mod_subset p (subtopology X S))" + +abbreviation singular_relboundary_set :: "nat \ 'a topology \ 'a set \ ('a chain) set" + where "singular_relboundary_set p X S \ Collect (singular_relboundary p X S)" + +lemma singular_relboundary_restrict [simp]: + "singular_relboundary p X (topspace X \ S) = singular_relboundary p X S" + unfolding singular_relboundary_def + by (metis (no_types, hide_lams) subtopology_subtopology subtopology_topspace) + +lemma singular_relboundary_alt: + "singular_relboundary p X S c \ + (\d e. singular_chain (Suc p) X d \ singular_chain p (subtopology X S) e \ + chain_boundary (Suc p) d = c + e)" + unfolding singular_relboundary_def mod_subset_def by fastforce + +lemma singular_relboundary: + "singular_relboundary p X S c \ + (\d e. singular_chain (Suc p) X d \ singular_chain p (subtopology X S) e \ + (chain_boundary (Suc p) d) + e = c)" + using singular_chain_minus + by (fastforce simp add: singular_relboundary_alt) + +lemma singular_boundary: + "singular_relboundary p X {} c \ + (\d. singular_chain (Suc p) X d \ chain_boundary (Suc p) d = c)" + by (simp add: singular_relboundary_def) + +lemma singular_boundary_imp_chain: + "singular_relboundary p X {} c \ singular_chain p X c" + by (auto simp: singular_relboundary singular_chain_boundary_alt singular_chain_empty topspace_subtopology) + +lemma singular_boundary_mono: + "\T \ S; singular_relboundary p (subtopology X T) {} c\ + \ singular_relboundary p (subtopology X S) {} c" + by (metis mod_subset_empty singular_chain_mono singular_relboundary_def) + +lemma singular_relboundary_imp_chain: + "singular_relboundary p X S c \ singular_chain p X c" + unfolding singular_relboundary singular_chain_subtopology + by (blast intro: singular_chain_add singular_chain_boundary_alt) + +lemma singular_chain_imp_relboundary: + "singular_chain p (subtopology X S) c \ singular_relboundary p X S c" + unfolding singular_relboundary_def + apply (rule_tac x=0 in exI) + using mod_subset_def singular_chain_diff by fastforce + +lemma singular_relboundary_0 [simp]: "singular_relboundary p X S 0" + unfolding singular_relboundary_def + by (rule_tac x=0 in exI) auto + +lemma singular_relboundary_cmul: + "singular_relboundary p X S c \ singular_relboundary p X S (frag_cmul a c)" + unfolding singular_relboundary_def + by (metis chain_boundary_cmul mod_subset_cmul singular_chain_cmul) + +lemma singular_relboundary_minus: + "singular_relboundary p X S (-c) \ singular_relboundary p X S c" + using singular_relboundary_cmul + by (metis add.inverse_inverse frag_cmul_minus_one) + +lemma singular_relboundary_add: + "\singular_relboundary p X S a; singular_relboundary p X S b\ \ singular_relboundary p X S (a+b)" + unfolding singular_relboundary_def + by (metis chain_boundary_add mod_subset_add singular_chain_add) + +lemma singular_relboundary_diff: + "\singular_relboundary p X S a; singular_relboundary p X S b\ \ singular_relboundary p X S (a-b)" + by (metis uminus_add_conv_diff singular_relboundary_minus singular_relboundary_add) + +subsection\The (relative) homology relation\ + +definition homologous_rel :: "[nat,'a topology,'a set,'a chain,'a chain] \ bool" + where "homologous_rel p X S \ \a b. singular_relboundary p X S (a-b)" + +abbreviation homologous_rel_set + where "homologous_rel_set p X S a \ Collect (homologous_rel p X S a)" + +lemma homologous_rel_restrict [simp]: + "homologous_rel p X (topspace X \ S) = homologous_rel p X S" + unfolding homologous_rel_def by (metis singular_relboundary_restrict) + +lemma homologous_rel_refl [simp]: "homologous_rel p X S c c" + unfolding homologous_rel_def by auto + +lemma homologous_rel_sym: + "homologous_rel p X S a b = homologous_rel p X S b a" + unfolding homologous_rel_def + using singular_relboundary_minus by fastforce + +lemma homologous_rel_trans: + assumes "homologous_rel p X S b c" "homologous_rel p X S a b" + shows "homologous_rel p X S a c" + using homologous_rel_def +proof - + have "singular_relboundary p X S (b - c)" + using assms unfolding homologous_rel_def by blast + moreover have "singular_relboundary p X S (b - a)" + using assms by (meson homologous_rel_def homologous_rel_sym) + ultimately have "singular_relboundary p X S (c - a)" + using singular_relboundary_diff by fastforce + then show ?thesis + by (meson homologous_rel_def homologous_rel_sym) +qed + +lemma homologous_rel_eq: + "homologous_rel p X S a = homologous_rel p X S b \ + homologous_rel p X S a b" + using homologous_rel_sym homologous_rel_trans by fastforce + +lemma homologous_rel_set_eq: + "homologous_rel_set p X S a = homologous_rel_set p X S b \ + homologous_rel p X S a b" + by (metis homologous_rel_eq mem_Collect_eq) + +lemma homologous_rel_singular_chain: + "homologous_rel p X S a b \ (singular_chain p X a \ singular_chain p X b)" + unfolding homologous_rel_def + using singular_chain_diff singular_chain_add + by (fastforce dest: singular_relboundary_imp_chain) + +lemma homologous_rel_add: + "\homologous_rel p X S a a'; homologous_rel p X S b b'\ + \ homologous_rel p X S (a+b) (a'+b')" + unfolding homologous_rel_def + by (simp add: add_diff_add singular_relboundary_add) + +lemma homologous_rel_diff: + assumes "homologous_rel p X S a a'" "homologous_rel p X S b b'" + shows "homologous_rel p X S (a - b) (a' - b')" +proof - + have "singular_relboundary p X S ((a - a') - (b - b'))" + using assms singular_relboundary_diff unfolding homologous_rel_def by blast + then show ?thesis + by (simp add: homologous_rel_def algebra_simps) +qed + +lemma homologous_rel_sum: + assumes f: "finite {i \ I. f i \ 0}" and g: "finite {i \ I. g i \ 0}" + and h: "\i. i \ I \ homologous_rel p X S (f i) (g i)" + shows "homologous_rel p X S (sum f I) (sum g I)" +proof (cases "finite I") + case True + let ?L = "{i \ I. f i \ 0} \ {i \ I. g i \ 0}" + have L: "finite ?L" "?L \ I" + using f g by blast+ + have "sum f I = sum f ?L" + by (rule comm_monoid_add_class.sum.mono_neutral_right [OF True]) auto + moreover have "sum g I = sum g ?L" + by (rule comm_monoid_add_class.sum.mono_neutral_right [OF True]) auto + moreover have *: "homologous_rel p X S (f i) (g i)" if "i \ ?L" for i + using h that by auto + have "homologous_rel p X S (sum f ?L) (sum g ?L)" + using L + proof induction + case (insert j J) + then show ?case + by (simp add: h homologous_rel_add) + qed auto + ultimately show ?thesis + by simp +qed auto + + +lemma chain_homotopic_imp_homologous_rel: + assumes + "\c. singular_chain p X c \ singular_chain (Suc p) X' (h c)" + "\c. singular_chain (p -1) (subtopology X S) c \ singular_chain p (subtopology X' T) (h' c)" + "\c. singular_chain p X c + \ (chain_boundary (Suc p) (h c)) + (h'(chain_boundary p c)) = f c - g c" + "singular_relcycle p X S c" + shows "homologous_rel p X' T (f c) (g c)" + using assms + unfolding singular_relcycle_def mod_subset_def homologous_rel_def singular_relboundary_def + apply (rule_tac x="h c" in exI, simp) + by (metis (no_types, lifting) add_diff_cancel_left' minus_diff_eq singular_chain_minus) + + +subsection\Show that all boundaries are cycles, the key "chain complex" property.\ + +lemma sum_Int_Diff: "finite A \ sum f A = sum f (A \ B) + sum f (A - B)" + by (metis Diff_Diff_Int Diff_subset sum.subset_diff) + +lemma chain_boundary_boundary: + assumes "singular_chain p X c" + shows "chain_boundary (p - Suc 0) (chain_boundary p c) = 0" +proof (cases "p -1 = 0") + case False + then have "2 \ p" + by auto + show ?thesis + using assms + unfolding singular_chain_def + proof (induction rule: frag_induction) + case (one g) + then have ss: "singular_simplex p X g" + by simp + have eql: "{..p} \ {..p - Suc 0} \ {(x, y). y < x} = (\(j,i). (Suc i, j)) ` {(i,j). i \ j \ j \ p -1}" + using False + by (auto simp: image_def) (metis One_nat_def diff_Suc_1 diff_le_mono le_refl lessE less_imp_le_nat) + have eqr: "{..p} \ {..p - Suc 0} - {(x, y). y < x} = {(i,j). i \ j \ j \ p -1}" + by auto + have eqf: "singular_face (p - Suc 0) i (singular_face p (Suc j) g) = + singular_face (p - Suc 0) j (singular_face p i g)" if "i \ j" "j \ p - Suc 0" for i j + proof (rule ext) + fix t + show "singular_face (p - Suc 0) i (singular_face p (Suc j) g) t = + singular_face (p - Suc 0) j (singular_face p i g) t" + proof (cases "t \ standard_simplex (p -1 -1)") + case True + have fi: "simplical_face i t \ standard_simplex (p - Suc 0)" + using False True simplical_face_in_standard_simplex that by force + have fj: "simplical_face j t \ standard_simplex (p - Suc 0)" + by (metis False One_nat_def True simplical_face_in_standard_simplex less_one not_less that(2)) + have eq: "simplical_face (Suc j) (simplical_face i t) = simplical_face i (simplical_face j t)" + using True that ss + unfolding standard_simplex_def simplical_face_def by fastforce + show ?thesis by (simp add: singular_face_def fi fj eq) + qed (simp add: singular_face_def) + qed + show ?case + proof (cases "p = 1") + case False + have eq0: "frag_cmul (-1) a = b \ a + b = 0" for a b + by (simp add: neg_eq_iff_add_eq_0) + have *: "(\x\p. \i\p - Suc 0. + frag_cmul ((-1) ^ (x + i)) (frag_of (singular_face (p - Suc 0) i (singular_face p x g)))) + = 0" + apply (simp add: sum.cartesian_product sum_Int_Diff [of "_ \ _" _ "{(x,y). y < x}"]) + apply (rule eq0) + apply (simp only: frag_cmul_sum prod.case_distrib [of "frag_cmul (-1)"] frag_cmul_cmul eql eqr flip: power_Suc) + apply (force simp: simp add: inj_on_def sum.reindex add.commute eqf intro: sum.cong) + done + show ?thesis + using False by (simp add: chain_boundary_of chain_boundary_sum chain_boundary_cmul frag_cmul_sum * flip: power_add) + qed (simp add: chain_boundary_def) + next + case (diff a b) + then show ?case + by (simp add: chain_boundary_diff) + qed auto +qed (simp add: chain_boundary_def) + + +lemma chain_boundary_boundary_alt: + "singular_chain (Suc p) X c \ chain_boundary p (chain_boundary (Suc p) c) = 0" + using chain_boundary_boundary by force + +lemma singular_relboundary_imp_relcycle: + assumes "singular_relboundary p X S c" + shows "singular_relcycle p X S c" +proof - + obtain d e where d: "singular_chain (Suc p) X d" + and e: "singular_chain p (subtopology X S) e" + and c: "c = chain_boundary (Suc p) d + e" + using assms by (auto simp: singular_relboundary singular_relcycle) + have 1: "singular_chain (p - Suc 0) (subtopology X S) (chain_boundary p (chain_boundary (Suc p) d))" + using d chain_boundary_boundary_alt by fastforce + have 2: "singular_chain (p - Suc 0) (subtopology X S) (chain_boundary p e)" + using \singular_chain p (subtopology X S) e\ singular_chain_boundary by auto + have "singular_chain p X c" + using assms singular_relboundary_imp_chain by auto + moreover have "singular_chain (p - Suc 0) (subtopology X S) (chain_boundary p c)" + by (simp add: c chain_boundary_add singular_chain_add 1 2) + ultimately show ?thesis + by (simp add: singular_relcycle) +qed + +lemma homologous_rel_singular_relcycle_1: + assumes "homologous_rel p X S c1 c2" "singular_relcycle p X S c1" + shows "singular_relcycle p X S c2" + using assms + by (metis diff_add_cancel homologous_rel_def homologous_rel_sym singular_relboundary_imp_relcycle singular_relcycle_add) + +lemma homologous_rel_singular_relcycle: + assumes "homologous_rel p X S c1 c2" + shows "singular_relcycle p X S c1 = singular_relcycle p X S c2" + using assms homologous_rel_singular_relcycle_1 + using homologous_rel_sym by blast + + +subsection\Operations induced by a continuous map g between topological spaces\ + +definition simplex_map :: "nat \ ('b \ 'a) \ ((nat \ real) \ 'b) \ (nat \ real) \ 'a" + where "simplex_map p g c \ restrict (g \ c) (standard_simplex p)" + +lemma singular_simplex_simplex_map: + "\singular_simplex p X f; continuous_map X X' g\ + \ singular_simplex p X' (simplex_map p g f)" + unfolding singular_simplex_def simplex_map_def + by (auto simp: continuous_map_compose) + +lemma simplex_map_eq: + "\singular_simplex p X c; + \x. x \ topspace X \ f x = g x\ + \ simplex_map p f c = simplex_map p g c" + by (auto simp: singular_simplex_def simplex_map_def continuous_map_def) + +lemma simplex_map_id_gen: + "\singular_simplex p X c; + \x. x \ topspace X \ f x = x\ + \ simplex_map p f c = c" + unfolding singular_simplex_def simplex_map_def continuous_map_def + using extensional_arb by fastforce + +lemma simplex_map_id [simp]: + "simplex_map p id = (\c. restrict c (standard_simplex p))" + by (auto simp: simplex_map_def) + +lemma simplex_map_compose: + "simplex_map p (h \ g) = simplex_map p h \ simplex_map p g" + unfolding simplex_map_def by force + +lemma singular_face_simplex_map: + "\1 \ p; k \ p\ + \ singular_face p k (simplex_map p f c) = simplex_map (p - Suc 0) f (c \ simplical_face k)" + unfolding simplex_map_def singular_face_def + by (force simp: simplical_face_in_standard_simplex) + +lemma singular_face_restrict [simp]: + assumes "p > 0" "i \ p" + shows "singular_face p i (restrict f (standard_simplex p)) = singular_face p i f" + by (metis assms One_nat_def Suc_leI simplex_map_id singular_face_def singular_face_simplex_map) + + +definition chain_map :: "nat \ ('b \ 'a) \ (((nat \ real) \ 'b) \\<^sub>0 int) \ 'a chain" + where "chain_map p g c \ frag_extend (frag_of \ simplex_map p g) c" + +lemma singular_chain_chain_map: + "\singular_chain p X c; continuous_map X X' g\ \ singular_chain p X' (chain_map p g c)" + unfolding chain_map_def + apply (rule singular_chain_extend) + by (metis comp_apply subsetD mem_Collect_eq singular_chain_def singular_chain_of singular_simplex_simplex_map) + +lemma chain_map_0 [simp]: "chain_map p g 0 = 0" + by (auto simp: chain_map_def) + +lemma chain_map_of [simp]: "chain_map p g (frag_of f) = frag_of (simplex_map p g f)" + by (simp add: chain_map_def) + +lemma chain_map_cmul [simp]: + "chain_map p g (frag_cmul a c) = frag_cmul a (chain_map p g c)" + by (simp add: frag_extend_cmul chain_map_def) + +lemma chain_map_minus: "chain_map p g (-c) = - (chain_map p g c)" + by (simp add: frag_extend_minus chain_map_def) + +lemma chain_map_add: + "chain_map p g (a+b) = chain_map p g a + chain_map p g b" + by (simp add: frag_extend_add chain_map_def) + +lemma chain_map_diff: + "chain_map p g (a-b) = chain_map p g a - chain_map p g b" + by (simp add: frag_extend_diff chain_map_def) + +lemma chain_map_sum: + "finite I \ chain_map p g (sum f I) = sum (chain_map p g \ f) I" + by (simp add: frag_extend_sum chain_map_def) + +lemma chain_map_eq: + "\singular_chain p X c; \x. x \ topspace X \ f x = g x\ + \ chain_map p f c = chain_map p g c" + unfolding singular_chain_def + apply (erule frag_induction) + apply (auto simp: chain_map_diff) + apply (metis simplex_map_eq) + done + +lemma chain_map_id_gen: + "\singular_chain p X c; \x. x \ topspace X \ f x = x\ + \ chain_map p f c = c" + unfolding singular_chain_def + by (erule frag_induction) (auto simp: chain_map_diff simplex_map_id_gen) + +lemma chain_map_ident: + "singular_chain p X c \ chain_map p id c = c" + by (simp add: chain_map_id_gen) + +lemma chain_map_id: + "chain_map p id = frag_extend (frag_of \ (\f. restrict f (standard_simplex p)))" + by (auto simp: chain_map_def) + +lemma chain_map_compose: + "chain_map p (h \ g) = chain_map p h \ chain_map p g" +proof + show "chain_map p (h \ g) c = (chain_map p h \ chain_map p g) c" for c + using subset_UNIV + proof (induction c rule: frag_induction) + case (one x) + then show ?case + by simp (metis (mono_tags, lifting) comp_eq_dest_lhs restrict_apply simplex_map_def) + next + case (diff a b) + then show ?case + by (simp add: chain_map_diff) + qed auto +qed + +lemma singular_simplex_chain_map_id: + assumes "singular_simplex p X f" + shows "chain_map p f (frag_of (restrict id (standard_simplex p))) = frag_of f" +proof - + have "(restrict (f \ restrict id (standard_simplex p)) (standard_simplex p)) = f" + by (rule ext) (metis assms comp_apply extensional_arb id_apply restrict_apply singular_simplex_def) + then show ?thesis + by (simp add: simplex_map_def) +qed + +lemma chain_boundary_chain_map: + assumes "singular_chain p X c" + shows "chain_boundary p (chain_map p g c) = chain_map (p - Suc 0) g (chain_boundary p c)" + using assms unfolding singular_chain_def +proof (induction c rule: frag_induction) + case (one x) + then have "singular_face p i (simplex_map p g x) = simplex_map (p - Suc 0) g (singular_face p i x)" + if "0 \ i" "i \ p" "p \ 0" for i + using that + by (fastforce simp add: singular_face_def simplex_map_def simplical_face_in_standard_simplex) + then show ?case + by (auto simp: chain_boundary_of chain_map_sum) +next + case (diff a b) + then show ?case + by (simp add: chain_boundary_diff chain_map_diff) +qed auto + +lemma singular_relcycle_chain_map: + assumes "singular_relcycle p X S c" "continuous_map X X' g" "g ` S \ T" + shows "singular_relcycle p X' T (chain_map p g c)" +proof - + have "continuous_map (subtopology X S) (subtopology X' T) g" + using assms + using continuous_map_from_subtopology continuous_map_in_subtopology topspace_subtopology by fastforce + then show ?thesis + using chain_boundary_chain_map [of p X c g] + by (metis One_nat_def assms(1) assms(2) singular_chain_chain_map singular_relcycle) +qed + +lemma singular_relboundary_chain_map: + assumes "singular_relboundary p X S c" "continuous_map X X' g" "g ` S \ T" + shows "singular_relboundary p X' T (chain_map p g c)" +proof - + obtain d e where d: "singular_chain (Suc p) X d" + and e: "singular_chain p (subtopology X S) e" and c: "c = chain_boundary (Suc p) d + e" + using assms by (auto simp: singular_relboundary) + have "singular_chain (Suc p) X' (chain_map (Suc p) g d)" + using assms(2) d singular_chain_chain_map by blast + moreover have "singular_chain p (subtopology X' T) (chain_map p g e)" + proof - + have "\t. g ` topspace (subtopology t S) \ T" + by (metis assms(3) closure_of_subset_subtopology closure_of_topspace dual_order.trans image_mono) + then show ?thesis + by (meson assms(2) continuous_map_from_subtopology continuous_map_in_subtopology e singular_chain_chain_map) + qed + moreover have "chain_boundary (Suc p) (chain_map (Suc p) g d) + chain_map p g e = + chain_map p g (chain_boundary (Suc p) d + e)" + by (metis One_nat_def chain_boundary_chain_map chain_map_add d diff_Suc_1) + ultimately show ?thesis + unfolding singular_relboundary + using c by blast +qed + + +subsection\Homology of one-point spaces degenerates except for $p = 0$.\ + +lemma singular_simplex_singleton: + assumes "topspace X = {a}" + shows "singular_simplex p X f \ f = restrict (\x. a) (standard_simplex p)" (is "?lhs = ?rhs") +proof + assume L: ?lhs + then show ?rhs + proof - + have "continuous_map (subtopology (product_topology (\n. euclideanreal) UNIV) (standard_simplex p)) X f" + using \singular_simplex p X f\ singular_simplex_def by blast + then have "\c. c \ standard_simplex p \ f c = a" + by (simp add: assms continuous_map_def) + then show ?thesis + by (metis (no_types) L extensional_restrict restrict_ext singular_simplex_def) + qed +next + assume ?rhs + with assms show ?lhs + by (auto simp: singular_simplex_def topspace_subtopology) +qed + +lemma singular_chain_singleton: + assumes "topspace X = {a}" + shows "singular_chain p X c \ + (\b. c = frag_cmul b (frag_of(restrict (\x. a) (standard_simplex p))))" + (is "?lhs = ?rhs") +proof + let ?f = "restrict (\x. a) (standard_simplex p)" + assume L: ?lhs + with assms have "Poly_Mapping.keys c \ {?f}" + by (auto simp: singular_chain_def singular_simplex_singleton) + then consider "Poly_Mapping.keys c = {}" | "Poly_Mapping.keys c = {?f}" + by blast + then show ?rhs + proof cases + case 1 + with L show ?thesis + by (metis frag_cmul_zero keys_eq_empty) + next + case 2 + then have "\b. frag_extend frag_of c = frag_cmul b (frag_of (\x\standard_simplex p. a))" + by (force simp: frag_extend_def) + then show ?thesis + by (metis frag_expansion) + qed +next + assume ?rhs + with assms show ?lhs + by (auto simp: singular_chain_def singular_simplex_singleton) +qed + +lemma chain_boundary_of_singleton: + assumes tX: "topspace X = {a}" and sc: "singular_chain p X c" + shows "chain_boundary p c = + (if p = 0 \ odd p then 0 + else frag_extend (\f. frag_of(restrict (\x. a) (standard_simplex (p -1)))) c)" + (is "?lhs = ?rhs") +proof (cases "p = 0") + case False + have "?lhs = frag_extend (\f. if odd p then 0 else frag_of(restrict (\x. a) (standard_simplex (p -1)))) c" + proof (simp only: chain_boundary_def False if_False, rule frag_extend_eq) + fix f + assume "f \ Poly_Mapping.keys c" + with assms have "singular_simplex p X f" + by (auto simp: singular_chain_def) + then have *: "\k. k \ p \ singular_face p k f = (\x\standard_simplex (p -1). a)" + apply (subst singular_simplex_singleton [OF tX, symmetric]) + using False singular_simplex_singular_face by fastforce + define c where "c \ frag_of (\x\standard_simplex (p -1). a)" + have "(\k\p. frag_cmul ((-1) ^ k) (frag_of (singular_face p k f))) + = (\k\p. frag_cmul ((-1) ^ k) c)" + by (auto simp: c_def * intro: sum.cong) + also have "\ = (if odd p then 0 else c)" + by (induction p) (auto simp: c_def restrict_def) + finally show "(\k\p. frag_cmul ((-1) ^ k) (frag_of (singular_face p k f))) + = (if odd p then 0 else frag_of (\x\standard_simplex (p -1). a))" + unfolding c_def . + qed + also have "\ = ?rhs" + by (auto simp: False frag_extend_eq_0) + finally show ?thesis . +qed (simp add: chain_boundary_def) + + +lemma singular_cycle_singleton: + assumes "topspace X = {a}" + shows "singular_relcycle p X {} c \ singular_chain p X c \ (p = 0 \ odd p \ c = 0)" +proof - + have "c = 0" if "singular_chain p X c" and "chain_boundary p c = 0" and "even p" and "p \ 0" + using that assms singular_chain_singleton [of X a p c] chain_boundary_of_singleton [OF assms] + by (auto simp: frag_extend_cmul) + moreover + have "chain_boundary p c = 0" if sc: "singular_chain p X c" and "odd p" + by (simp add: chain_boundary_of_singleton [OF assms sc] that) + moreover have "chain_boundary 0 c = 0" if "singular_chain 0 X c" and "p = 0" + by (simp add: chain_boundary_def) + ultimately show ?thesis + using assms by (auto simp: singular_cycle) +qed + + +lemma singular_boundary_singleton: + assumes "topspace X = {a}" + shows "singular_relboundary p X {} c \ singular_chain p X c \ (odd p \ c = 0)" +proof (cases "singular_chain p X c") + case True + have eq: "frag_extend (\f. frag_of (\x\standard_simplex p. a)) (frag_of (\x\standard_simplex (Suc p). a)) + = frag_of (\x\standard_simplex p. a)" + by (simp add: singular_chain_singleton frag_extend_cmul assms) + have "\d. singular_chain (Suc p) X d \ chain_boundary (Suc p) d = c" + if "singular_chain p X c" and "odd p" + using assms that + apply (clarsimp simp: singular_chain_singleton) + apply (rule_tac x = "frag_cmul b (frag_of (\x\standard_simplex (Suc p). a))" in exI) + apply (subst chain_boundary_of_singleton [of X a "Suc p"]) + apply (auto simp: singular_chain_singleton frag_extend_cmul eq) + done + with True assms show ?thesis + by (auto simp: singular_boundary chain_boundary_of_singleton) +next + case False + with assms singular_boundary_imp_chain show ?thesis + by metis +qed + + +lemma singular_boundary_eq_cycle_singleton: + assumes "topspace X = {a}" "1 \ p" + shows "singular_relboundary p X {} c \ singular_relcycle p X {} c" + using assms + apply (auto simp: singular_boundary chain_boundary_boundary_alt singular_chain_boundary_alt singular_cycle) + by (metis Suc_neq_Zero le_zero_eq singular_boundary singular_boundary_singleton singular_chain_0 singular_cycle_singleton singular_relcycle) + +lemma singular_boundary_set_eq_cycle_singleton: + assumes "topspace X = {a}" "1 \ p" + shows "singular_relboundary_set p X {} = singular_relcycle_set p X {}" + using singular_boundary_eq_cycle_singleton [OF assms] + by blast + +subsection\Simplicial chains\ + +text\Simplicial chains, effectively those resulting from linear maps. + We still allow the map to be singular, so the name is questionable. +These are intended as building-blocks for singular subdivision, rather than as a axis +for 1 simplicial homology.\ + +definition oriented_simplex + where "oriented_simplex p l \ (\x\standard_simplex p. \i. (\j\p. l j i * x j))" + +definition simplicial_simplex + where + "simplicial_simplex p S f \ + singular_simplex p (subtopology (powertop_real UNIV) S) f \ + (\l. f = oriented_simplex p l)" + +lemma simplicial_simplex: + "simplicial_simplex p S f \ f ` (standard_simplex p) \ S \ (\l. f = oriented_simplex p l)" + (is "?lhs = ?rhs") +proof + assume R: ?rhs + show ?lhs + using R + apply (clarsimp simp: simplicial_simplex_def singular_simplex_subtopology) + apply (simp add: singular_simplex_def oriented_simplex_def) + apply (clarsimp simp: continuous_map_componentwise) + apply (intro continuous_intros continuous_map_from_subtopology continuous_map_product_projection, auto) + done +qed (simp add: simplicial_simplex_def singular_simplex_subtopology) + +lemma simplicial_simplex_empty [simp]: "\ simplicial_simplex p {} f" + by (simp add: nonempty_standard_simplex simplicial_simplex) + +definition simplicial_chain + where "simplicial_chain p S c \ Poly_Mapping.keys c \ Collect (simplicial_simplex p S)" + +lemma simplicial_chain_0 [simp]: "simplicial_chain p S 0" + by (simp add: simplicial_chain_def) + +lemma simplicial_chain_of [simp]: + "simplicial_chain p S (frag_of c) \ simplicial_simplex p S c" + by (simp add: simplicial_chain_def) + +lemma simplicial_chain_cmul: + "simplicial_chain p S c \ simplicial_chain p S (frag_cmul a c)" + by (auto simp: simplicial_chain_def) + +lemma simplicial_chain_diff: + "\simplicial_chain p S c1; simplicial_chain p S c2\ \ simplicial_chain p S (c1 - c2)" + unfolding simplicial_chain_def by (meson UnE keys_diff subset_iff) + +lemma simplicial_chain_sum: + "(\i. i \ I \ simplicial_chain p S (f i)) \ simplicial_chain p S (sum f I)" + unfolding simplicial_chain_def + using order_trans [OF keys_sum [of f I]] + by (simp add: UN_least) + +lemma simplicial_simplex_oriented_simplex: + "simplicial_simplex p S (oriented_simplex p l) + \ ((\x i. \j\p. l j i * x j) ` standard_simplex p \ S)" + by (auto simp: simplicial_simplex oriented_simplex_def) + +lemma simplicial_imp_singular_simplex: + "simplicial_simplex p S f + \ singular_simplex p (subtopology (powertop_real UNIV) S) f" + by (simp add: simplicial_simplex_def) + +lemma simplicial_imp_singular_chain: + "simplicial_chain p S c + \ singular_chain p (subtopology (powertop_real UNIV) S) c" + unfolding simplicial_chain_def singular_chain_def + by (auto intro: simplicial_imp_singular_simplex) + +lemma oriented_simplex_eq: + "oriented_simplex p l = oriented_simplex p l' \ (\i. i \ p \ l i = l' i)" + (is "?lhs = ?rhs") +proof + assume L: ?lhs + show ?rhs + proof clarify + fix i + assume "i \ p" + let ?fi = "(\j. if j = i then 1 else 0)" + have "(\j\p. l j k * ?fi j) = (\j\p. l' j k * ?fi j)" for k + apply (rule fun_cong [where x=k]) + using fun_cong [OF L, of ?fi] + apply (simp add: \i \ p\ oriented_simplex_def) + done + with \i \ p\ show "l i = l' i" + by (simp add: if_distrib ext cong: if_cong) + qed +qed (auto simp: oriented_simplex_def) + +lemma sum_zero_middle: + fixes g :: "nat \ 'a::comm_monoid_add" + assumes "1 \ p" "k \ p" + shows "(\j\p. if j < k then f j else if j = k then 0 else g (j - Suc 0)) + = (\j\p - Suc 0. if j < k then f j else g j)" (is "?lhs = ?rhs") +proof - + have [simp]: "{..p - Suc 0} \ {j. j < k} = {.. - {j. j < k} = {k..p - Suc 0}" + using assms by auto + have "?lhs = (\jj = k..p. if j = k then 0 else g (j - Suc 0))" + using sum.union_disjoint [of "{..x. _ * x"] if_distrib [of "\f. f i * _"] atLeast0AtMost cong: if_cong) + done + qed + then show ?thesis + using simplical_face_in_standard_simplex assms + by (auto simp: singular_face_def oriented_simplex_def restrict_def) +qed + +lemma simplicial_simplex_singular_face: + fixes f :: "(nat \ real) \ nat \ real" + assumes ss: "simplicial_simplex p S f" and p: "1 \ p" "k \ p" + shows "simplicial_simplex (p - Suc 0) S (singular_face p k f)" +proof - + let ?X = "subtopology (powertop_real UNIV) S" + obtain m where l: "singular_simplex p ?X (oriented_simplex p m)" + and feq: "f = oriented_simplex p m" + using assms by (force simp: simplicial_simplex_def) + moreover have "\l. singular_face p k f = oriented_simplex (p - Suc 0) l" + apply (simp add: feq singular_face_def oriented_simplex_def) + apply (simp add: simplical_face_in_standard_simplex [OF p] restrict_compose_left subset_eq) + apply (rule_tac x="\i. if i < k then m i else m (Suc i)" in exI) + using sum_zero_middle [OF p, where 'a=real, symmetric] unfolding simplical_face_def o_def + apply (simp add: if_distrib [of "\x. _ * x"] if_distrib [of "\f. f _ * _"] atLeast0AtMost cong: if_cong) + done + ultimately + show ?thesis + using assms by (simp add: singular_simplex_singular_face simplicial_simplex_def) +qed + +lemma simplicial_chain_boundary: + "simplicial_chain p S c \ simplicial_chain (p -1) S (chain_boundary p c)" + unfolding simplicial_chain_def +proof (induction rule: frag_induction) + case (one f) + then have "simplicial_simplex p S f" + by simp + have "simplicial_chain (p - Suc 0) S (frag_of (singular_face p i f))" + if "0 < p" "i \ p" for i + using that one + apply (simp add: simplicial_simplex_def singular_simplex_singular_face) + apply (force simp: singular_face_oriented_simplex) + done + then have "simplicial_chain (p - Suc 0) S (chain_boundary p (frag_of f))" + unfolding chain_boundary_def frag_extend_of + by (auto intro!: simplicial_chain_cmul simplicial_chain_sum) + then show ?case + by (simp add: simplicial_chain_def [symmetric]) +next + case (diff a b) + then show ?case + by (metis chain_boundary_diff simplicial_chain_def simplicial_chain_diff) +qed auto + + +subsection\The cone construction on simplicial simplices.\ + +consts simplex_cone :: "[nat, nat \ real, [nat \ real, nat] \ real, nat \ real, nat] \ real" +specification (simplex_cone) + simplex_cone: + "\p v l. simplex_cone p v (oriented_simplex p l) = + oriented_simplex (Suc p) (\i. if i = 0 then v else l(i -1))" +proof - + have *: "\x. \y. \v. (\l. oriented_simplex (Suc x) (\i. if i = 0 then v else l (i -1))) + = (y v \ (oriented_simplex x))" + apply (subst choice_iff [symmetric]) + apply (subst function_factors_left [symmetric]) + by (simp add: oriented_simplex_eq) + then show ?thesis + apply (subst choice_iff [symmetric]) + apply (subst fun_eq_iff [symmetric]) + unfolding o_def + apply (blast intro: sym) + done +qed + +lemma simplicial_simplex_simplex_cone: + assumes f: "simplicial_simplex p S f" + and T: "\x u. \0 \ u; u \ 1; x \ S\ \ (\i. (1 - u) * v i + u * x i) \ T" + shows "simplicial_simplex (Suc p) T (simplex_cone p v f)" +proof - + obtain l where l: "\x. x \ standard_simplex p \ oriented_simplex p l x \ S" + and feq: "f = oriented_simplex p l" + using f by (auto simp: simplicial_simplex) + have "oriented_simplex p l x \ S" if "x \ standard_simplex p" for x + using f that by (auto simp: simplicial_simplex feq) + then have S: "\x. \\i. 0 \ x i \ x i \ 1; \i. i>p \ x i = 0; sum x {..p} = 1\ + \ (\i. \j\p. l j i * x j) \ S" + by (simp add: oriented_simplex_def standard_simplex_def) + have "oriented_simplex (Suc p) (\i. if i = 0 then v else l (i -1)) x \ T" + if "x \ standard_simplex (Suc p)" for x + proof (simp add: that oriented_simplex_def sum_atMost_Suc_shift del: sum_atMost_Suc) + have x01: "\i. 0 \ x i \ x i \ 1" and x0: "\i. i > Suc p \ x i = 0" and x1: "sum x {..Suc p} = 1" + using that by (auto simp: oriented_simplex_def standard_simplex_def) + obtain a where "a \ S" + using f by force + show "(\i. v i * x 0 + (\j\p. l j i * x (Suc j))) \ T" + proof (cases "x 0 = 1") + case True + then have "sum x {Suc 0..Suc p} = 0" + using x1 by (simp add: atMost_atLeast0 sum_head_Suc) + then have [simp]: "x (Suc j) = 0" if "j\p" for j + unfolding sum.atLeast_Suc_atMost_Suc_shift + using x01 that by (simp add: sum_nonneg_eq_0_iff) + then show ?thesis + using T [of 0 a] \a \ S\ by (auto simp: True) + next + case False + then have "(\i. v i * x 0 + (\j\p. l j i * x (Suc j))) = (\i. (1 - (1 - x 0)) * v i + (1 - x 0) * (inverse (1 - x 0) * (\j\p. l j i * x (Suc j))))" + by (force simp: field_simps) + also have "\ \ T" + proof (rule T) + have "x 0 < 1" + by (simp add: False less_le x01) + have xle: "x (Suc i) \ (1 - x 0)" for i + proof (cases "i \ p") + case True + have "sum x {0, Suc i} \ sum x {..Suc p}" + by (rule sum_mono2) (auto simp: True x01) + then show ?thesis + using x1 x01 by (simp add: algebra_simps not_less) + qed (simp add: x0 x01) + have "(\i. (\j\p. l j i * (x (Suc j) * inverse (1 - x 0)))) \ S" + proof (rule S) + have "x 0 + (\j\p. x (Suc j)) = sum x {..Suc p}" + by (metis sum_atMost_Suc_shift) + with x1 have "(\j\p. x (Suc j)) = 1 - x 0" + by simp + with False show "(\j\p. x (Suc j) * inverse (1 - x 0)) = 1" + by (metis add_diff_cancel_left' diff_diff_eq2 diff_zero right_inverse sum_distrib_right) + qed (use x01 x0 xle \x 0 < 1\ in \auto simp: divide_simps\) + then show "(\i. inverse (1 - x 0) * (\j\p. l j i * x (Suc j))) \ S" + by (simp add: field_simps sum_divide_distrib) + qed (use x01 in auto) + finally show ?thesis . + qed +qed + then show ?thesis + by (auto simp: simplicial_simplex feq simplex_cone) +qed + +definition simplicial_cone + where "simplicial_cone p v \ frag_extend (frag_of \ simplex_cone p v)" + +lemma simplicial_chain_simplicial_cone: + assumes c: "simplicial_chain p S c" + and T: "\x u. \0 \ u; u \ 1; x \ S\ \ (\i. (1 - u) * v i + u * x i) \ T" + shows "simplicial_chain (Suc p) T (simplicial_cone p v c)" + using c unfolding simplicial_chain_def simplicial_cone_def +proof (induction rule: frag_induction) + case (one x) + then show ?case + by (simp add: T simplicial_simplex_simplex_cone) +next + case (diff a b) + then show ?case + by (metis frag_extend_diff simplicial_chain_def simplicial_chain_diff) +qed auto + + +lemma chain_boundary_simplicial_cone_of': + assumes "f = oriented_simplex p l" + shows "chain_boundary (Suc p) (simplicial_cone p v (frag_of f)) = + frag_of f + - (if p = 0 then frag_of (\u\standard_simplex p. v) + else simplicial_cone (p -1) v (chain_boundary p (frag_of f)))" +proof (simp, intro impI conjI) + assume "p = 0" + have eq: "(oriented_simplex 0 (\j. if j = 0 then v else l j)) = (\u\standard_simplex 0. v)" + by (force simp: oriented_simplex_def standard_simplex_def) + show "chain_boundary (Suc 0) (simplicial_cone 0 v (frag_of f)) + = frag_of f - frag_of (\u\standard_simplex 0. v)" + by (simp add: assms simplicial_cone_def chain_boundary_of \p = 0\ simplex_cone singular_face_oriented_simplex eq cong: if_cong) +next + assume "0 < p" + have 0: "simplex_cone (p - Suc 0) v (singular_face p x (oriented_simplex p l)) + = oriented_simplex p + (\j. if j < Suc x + then if j = 0 then v else l (j -1) + else if Suc j = 0 then v else l (Suc j -1))" if "x \ p" for x + using \0 < p\ that + by (auto simp: Suc_leI singular_face_oriented_simplex simplex_cone oriented_simplex_eq) + have 1: "frag_extend (frag_of \ simplex_cone (p - Suc 0) v) + (\k = 0..p. frag_cmul ((-1) ^ k) (frag_of (singular_face p k (oriented_simplex p l)))) + = - (\k = Suc 0..Suc p. frag_cmul ((-1) ^ k) + (frag_of (singular_face (Suc p) k (simplex_cone p v (oriented_simplex p l)))))" + apply (subst sum.atLeast_Suc_atMost_Suc_shift) + apply (simp add: frag_extend_sum frag_extend_cmul flip: sum_negf) + apply (auto simp: simplex_cone singular_face_oriented_simplex 0 intro: sum.cong) + done + moreover have 2: "singular_face (Suc p) 0 (simplex_cone p v (oriented_simplex p l)) + = oriented_simplex p l" + by (simp add: simplex_cone singular_face_oriented_simplex) + show "chain_boundary (Suc p) (simplicial_cone p v (frag_of f)) + = frag_of f - simplicial_cone (p - Suc 0) v (chain_boundary p (frag_of f))" + using \p > 0\ + apply (simp add: assms simplicial_cone_def chain_boundary_of atMost_atLeast0 del: sum_atMost_Suc) + apply (subst sum_head_Suc [of 0]) + apply (simp_all add: 1 2 del: sum_atMost_Suc) + done +qed + +lemma chain_boundary_simplicial_cone_of: + assumes "simplicial_simplex p S f" + shows "chain_boundary (Suc p) (simplicial_cone p v (frag_of f)) = + frag_of f + - (if p = 0 then frag_of (\u\standard_simplex p. v) + else simplicial_cone (p -1) v (chain_boundary p (frag_of f)))" + using chain_boundary_simplicial_cone_of' assms unfolding simplicial_simplex_def + by blast + +lemma chain_boundary_simplicial_cone: + "simplicial_chain p S c + \ chain_boundary (Suc p) (simplicial_cone p v c) = + c - (if p = 0 then frag_extend (\f. frag_of (\u\standard_simplex p. v)) c + else simplicial_cone (p -1) v (chain_boundary p c))" + unfolding simplicial_chain_def +proof (induction rule: frag_induction) + case (one x) + then show ?case + by (auto simp: chain_boundary_simplicial_cone_of) +qed (auto simp: chain_boundary_diff simplicial_cone_def frag_extend_diff) + +lemma simplex_map_oriented_simplex: + assumes l: "simplicial_simplex p (standard_simplex q) (oriented_simplex p l)" + and g: "simplicial_simplex r S g" and "q \ r" + shows "simplex_map p g (oriented_simplex p l) = oriented_simplex p (g \ l)" +proof - + obtain m where geq: "g = oriented_simplex r m" + using g by (auto simp: simplicial_simplex_def) + have "g (\i. \j\p. l j i * x j) i = (\j\p. g (l j) i * x j)" + if "x \ standard_simplex p" for x i + proof - + have ssr: "(\i. \j\p. l j i * x j) \ standard_simplex r" + using l that standard_simplex_mono [OF \q \ r\] + unfolding simplicial_simplex_oriented_simplex by auto + have lss: "l j \ standard_simplex r" if "j\p" for j + proof - + have q: "(\x i. \j\p. l j i * x j) ` standard_simplex p \ standard_simplex q" + using l by (simp add: simplicial_simplex_oriented_simplex) + have p: "l j \ (\x i. \j\p. l j i * x j) ` standard_simplex p" + apply (rule_tac x="(\i. if i = j then 1 else 0)" in rev_image_eqI) + using \j\p\ by (force simp: basis_in_standard_simplex if_distrib cong: if_cong)+ + show ?thesis + apply (rule subsetD [OF standard_simplex_mono [OF \q \ r\]]) + apply (rule subsetD [OF q p]) + done + qed + show ?thesis + apply (simp add: geq oriented_simplex_def sum_distrib_left sum_distrib_right mult.assoc ssr lss) + by (rule sum.swap) + qed + then show ?thesis + by (force simp: oriented_simplex_def simplex_map_def o_def) +qed + + +lemma chain_map_simplicial_cone: + assumes g: "simplicial_simplex r S g" + and c: "simplicial_chain p (standard_simplex q) c" + and v: "v \ standard_simplex q" and "q \ r" + shows "chain_map (Suc p) g (simplicial_cone p v c) = simplicial_cone p (g v) (chain_map p g c)" +proof - + have *: "simplex_map (Suc p) g (simplex_cone p v f) = simplex_cone p (g v) (simplex_map p g f)" + if "f \ Poly_Mapping.keys c" for f + proof - + have "simplicial_simplex p (standard_simplex q) f" + using c that by (auto simp: simplicial_chain_def) + then obtain m where feq: "f = oriented_simplex p m" + by (auto simp: simplicial_simplex) + have 0: "simplicial_simplex p (standard_simplex q) (oriented_simplex p m)" + using \simplicial_simplex p (standard_simplex q) f\ feq by blast + then have 1: "simplicial_simplex (Suc p) (standard_simplex q) + (oriented_simplex (Suc p) (\i. if i = 0 then v else m (i -1)))" + using convex_standard_simplex v + by (simp flip: simplex_cone add: simplicial_simplex_simplex_cone) + show ?thesis + using simplex_map_oriented_simplex [OF 1 g \q \ r\] + simplex_map_oriented_simplex [of p q m r S g, OF 0 g \q \ r\] + by (simp add: feq oriented_simplex_eq simplex_cone) + qed + show ?thesis + by (auto simp: chain_map_def simplicial_cone_def frag_extend_compose * intro: frag_extend_eq) +qed + + +subsection\Barycentric subdivision of a linear ("simplicial") simplex's image\ + +definition simplicial_vertex + where "simplicial_vertex i f = f(\j. if j = i then 1 else 0)" + +lemma simplicial_vertex_oriented_simplex: + "simplicial_vertex i (oriented_simplex p l) = (if i \ p then l i else undefined)" + by (simp add: simplicial_vertex_def oriented_simplex_def if_distrib cong: if_cong) + + +primrec simplicial_subdivision +where + "simplicial_subdivision 0 = id" +| "simplicial_subdivision (Suc p) = + frag_extend + (\f. simplicial_cone p + (\i. (\j\Suc p. simplicial_vertex j f i) / (p + 2)) + (simplicial_subdivision p (chain_boundary (Suc p) (frag_of f))))" + + +lemma simplicial_subdivision_0 [simp]: + "simplicial_subdivision p 0 = 0" + by (induction p) auto + +lemma simplicial_subdivision_diff: + "simplicial_subdivision p (c1-c2) = simplicial_subdivision p c1 - simplicial_subdivision p c2" + by (induction p) (auto simp: frag_extend_diff) + +lemma simplicial_subdivision_of: + "simplicial_subdivision p (frag_of f) = + (if p = 0 then frag_of f + else simplicial_cone (p -1) + (\i. (\j\p. simplicial_vertex j f i) / (Suc p)) + (simplicial_subdivision (p -1) (chain_boundary p (frag_of f))))" + by (induction p) (auto simp: add.commute) + + +lemma simplicial_chain_simplicial_subdivision: + "simplicial_chain p S c + \ simplicial_chain p S (simplicial_subdivision p c)" +proof (induction p arbitrary: S c) + case (Suc p) + show ?case + using Suc.prems [unfolded simplicial_chain_def] + proof (induction c rule: frag_induction) + case (one f) + then have f: "simplicial_simplex (Suc p) S f" + by auto + then have "simplicial_chain p (f ` standard_simplex (Suc p)) + (simplicial_subdivision p (chain_boundary (Suc p) (frag_of f)))" + by (metis Suc.IH diff_Suc_1 simplicial_chain_boundary simplicial_chain_of simplicial_simplex subsetI) + moreover + obtain l where l: "\x. x \ standard_simplex (Suc p) \ (\i. (\j\Suc p. l j i * x j)) \ S" + and feq: "f = oriented_simplex (Suc p) l" + using f by (fastforce simp: simplicial_simplex oriented_simplex_def simp del: sum_atMost_Suc) + have "(\i. (1 - u) * ((\j\Suc p. simplicial_vertex j f i) / (real p + 2)) + u * y i) \ S" + if "0 \ u" "u \ 1" and y: "y \ f ` standard_simplex (Suc p)" for y u + proof - + obtain x where x: "x \ standard_simplex (Suc p)" and yeq: "y = oriented_simplex (Suc p) l x" + using y feq by blast + have "(\i. \j\Suc p. l j i * ((if j \ Suc p then (1 - u) * inverse (p + 2) + u * x j else 0))) \ S" + proof (rule l) + have i2p: "inverse (2 + real p) \ 1" + by (simp add: divide_simps) + show "(\j. if j \ Suc p then (1 - u) * inverse (real (p + 2)) + u * x j else 0) \ standard_simplex (Suc p)" + using x \0 \ u\ \u \ 1\ + apply (simp add: sum.distrib standard_simplex_def i2p linepath_le_1 flip: sum_distrib_left del: sum_atMost_Suc) + apply (simp add: divide_simps) + done + qed + moreover have "(\i. \j\Suc p. l j i * ((1 - u) * inverse (2 + real p) + u * x j)) + = (\i. (1 - u) * (\j\Suc p. l j i) / (real p + 2) + u * (\j\Suc p. l j i * x j))" + proof + fix i + have "(\j\Suc p. l j i * ((1 - u) * inverse (2 + real p) + u * x j)) + = (\j\Suc p. (1 - u) * l j i / (real p + 2) + u * l j i * x j)" (is "?lhs = _") + by (simp add: field_simps cong: sum.cong) + also have "\ = (1 - u) * (\j\Suc p. l j i) / (real p + 2) + u * (\j\Suc p. l j i * x j)" (is "_ = ?rhs") + by (simp add: sum_distrib_left sum.distrib sum_divide_distrib mult.assoc del: sum_atMost_Suc) + finally show "?lhs = ?rhs" . + qed + ultimately show ?thesis + using feq x yeq + by (simp add: simplicial_vertex_oriented_simplex) (simp add: oriented_simplex_def) + qed + ultimately show ?case + by (simp add: simplicial_chain_simplicial_cone) + next + case (diff a b) + then show ?case + by (metis simplicial_chain_diff simplicial_subdivision_diff) + qed auto +qed auto + +lemma chain_boundary_simplicial_subdivision: + "simplicial_chain p S c + \ chain_boundary p (simplicial_subdivision p c) = simplicial_subdivision (p -1) (chain_boundary p c)" +proof (induction p arbitrary: c) + case (Suc p) + show ?case + using Suc.prems [unfolded simplicial_chain_def] + proof (induction c rule: frag_induction) + case (one f) + then have f: "simplicial_simplex (Suc p) S f" + by simp + then have "simplicial_chain p S (simplicial_subdivision p (chain_boundary (Suc p) (frag_of f)))" + by (metis diff_Suc_1 simplicial_chain_boundary simplicial_chain_of simplicial_chain_simplicial_subdivision) + moreover have "simplicial_chain p S (chain_boundary (Suc p) (frag_of f))" + using one simplicial_chain_boundary simplicial_chain_of by fastforce + moreover have "simplicial_subdivision (p - Suc 0) (chain_boundary p (chain_boundary (Suc p) (frag_of f))) = 0" + by (metis f chain_boundary_boundary_alt simplicial_simplex_def simplicial_subdivision_0 singular_chain_of) + ultimately show ?case + apply (simp add: chain_boundary_simplicial_cone Suc) + apply (auto simp: chain_boundary_of frag_extend_diff simplicial_cone_def) + done + next + case (diff a b) + then show ?case + by (simp add: simplicial_subdivision_diff chain_boundary_diff frag_extend_diff) + qed auto +qed auto + + +(*A MESS AND USED ONLY ONCE*) +lemma simplicial_subdivision_shrinks: + "\simplicial_chain p S c; + \f x y. \f \ Poly_Mapping.keys c; x \ standard_simplex p; y \ standard_simplex p\ \ \f x k - f y k\ \ d; + f \ Poly_Mapping.keys(simplicial_subdivision p c); + x \ standard_simplex p; y \ standard_simplex p\ + \ \f x k - f y k\ \ (p / (Suc p)) * d" +proof (induction p arbitrary: d c f x y) + case (Suc p) + define Sigp where "Sigp \ \f:: (nat \ real) \ nat \ real. \i. (\j\Suc p. simplicial_vertex j f i) / real (p + 2)" + let ?CB = "\f. chain_boundary (Suc p) (frag_of f)" + have *: "Poly_Mapping.keys + (simplicial_cone p (Sigp f) + (simplicial_subdivision p (?CB f))) + \ {f. \x\standard_simplex (Suc p). \y\standard_simplex (Suc p). + \f x k - f y k\ \ real (Suc p) / real (Suc p + 1) * d}" (is "?lhs \ ?rhs") + if f: "f \ Poly_Mapping.keys c" for f + proof - + have ssf: "simplicial_simplex (Suc p) S f" + using Suc.prems(1) simplicial_chain_def that by auto + have 2: "\x y. \x \ standard_simplex (Suc p); y \ standard_simplex (Suc p)\ \ \f x k - f y k\ \ d" + by (meson Suc.prems(2) f subsetD le_Suc_eq order_refl standard_simplex_mono) + have sub: "Poly_Mapping.keys ((frag_of \ simplex_cone p (Sigp f)) g) \ ?rhs" + if "g \ Poly_Mapping.keys (simplicial_subdivision p (?CB f))" for g + proof - + have 1: "simplicial_chain p S (?CB f)" + using ssf simplicial_chain_boundary simplicial_chain_of by fastforce + have "simplicial_chain (Suc p) (f ` standard_simplex(Suc p)) (frag_of f)" + by (metis simplicial_chain_of simplicial_simplex ssf subset_refl) + then have sc_sub: "Poly_Mapping.keys (?CB f) + \ Collect (simplicial_simplex p (f ` standard_simplex (Suc p)))" + by (metis diff_Suc_1 simplicial_chain_boundary simplicial_chain_def) + have led: "\h x y. \h \ Poly_Mapping.keys (chain_boundary (Suc p) (frag_of f)); + x \ standard_simplex p; y \ standard_simplex p\ \ \h x k - h y k\ \ d" + using Suc.prems(2) f sc_sub + by (simp add: simplicial_simplex subset_iff image_iff) metis + have "\f' x y. \f' \ Poly_Mapping.keys (simplicial_subdivision p (?CB f)); x \ standard_simplex p; y \ standard_simplex p\ + \ \f' x k - f' y k\ \ (p / (Suc p)) * d" + by (blast intro: led Suc.IH [of "chain_boundary (Suc p) (frag_of f)", OF 1]) + then have g: "\x y. \x \ standard_simplex p; y \ standard_simplex p\ \ \g x k - g y k\ \ (p / (Suc p)) * d" + using that by blast + have "d \ 0" + using Suc.prems(2)[OF f] \x \ standard_simplex (Suc p)\ by force + have 3: "simplex_cone p (Sigp f) g \ ?rhs" + proof - + have "simplicial_simplex p (f ` standard_simplex(Suc p)) g" + by (metis (mono_tags, hide_lams) sc_sub mem_Collect_eq simplicial_chain_def simplicial_chain_simplicial_subdivision subsetD that) + then obtain m where m: "g ` standard_simplex p \ f ` standard_simplex (Suc p)" + and geq: "g = oriented_simplex p m" + using ssf by (auto simp: simplicial_simplex) + have m_in_gim: "\i. i \ p \ m i \ g ` standard_simplex p" + apply (rule_tac x = "\j. if j = i then 1 else 0" in image_eqI) + apply (simp_all add: geq oriented_simplex_def if_distrib cong: if_cong) + done + obtain l where l: "f ` standard_simplex (Suc p) \ S" + and feq: "f = oriented_simplex (Suc p) l" + using ssf by (auto simp: simplicial_simplex) + show ?thesis + proof (clarsimp simp add: geq simp del: sum_atMost_Suc) + fix x y + assume x: "x \ standard_simplex (Suc p)" and y: "y \ standard_simplex (Suc p)" + then have x': "(\i. 0 \ x i \ x i \ 1) \ (\i>Suc p. x i = 0) \ (\i\Suc p. x i) = 1" + and y': "(\i. 0 \ y i \ y i \ 1) \ (\i>Suc p. y i = 0) \ (\i\Suc p. y i) = 1" + by (auto simp: standard_simplex_def) + have "\(\j\Suc p. (if j = 0 then \i. (\j\Suc p. l j i) / (2 + real p) else m (j -1)) k * x j) - + (\j\Suc p. (if j = 0 then \i. (\j\Suc p. l j i) / (2 + real p) else m (j -1)) k * y j)\ + \ (1 + real p) * d / (2 + real p)" + proof - + have zero: "\m (s - Suc 0) k - (\j\Suc p. l j k) / (2 + real p)\ \ (1 + real p) * d / (2 + real p)" + if "0 < s" and "s \ Suc p" for s + proof - + have "m (s - Suc 0) \ f ` standard_simplex (Suc p)" + using m m_in_gim that(2) by auto + then obtain z where eq: "m (s - Suc 0) = (\i. \j\Suc p. l j i * z j)" and z: "z \ standard_simplex (Suc p)" + using feq unfolding oriented_simplex_def by auto + show ?thesis + unfolding eq + proof (rule convex_sum_bound_le) + fix i + assume i: "i \ {..Suc p}" + then have [simp]: "card ({..Suc p} - {i}) = Suc p" + by (simp add: card_Suc_Diff1) + have "(\j\Suc p. \l i k / (p + 2) - l j k / (p + 2)\) = (\j\Suc p. \l i k - l j k\ / (p + 2))" + by (rule sum.cong) (simp_all add: flip: diff_divide_distrib) + also have "\ = (\j \ {..Suc p} - {i}. \l i k - l j k\ / (p + 2))" + by (rule sum.mono_neutral_right) auto + also have "\ \ (1 + real p) * d / (p + 2)" + proof (rule sum_bounded_above_divide) + fix i' :: "nat" + assume i': "i' \ {..Suc p} - {i}" + have lf: "\r. r \ Suc p \ l r \ f ` standard_simplex(Suc p)" + apply (rule_tac x="\j. if j = r then 1 else 0" in image_eqI) + apply (auto simp: feq oriented_simplex_def if_distrib [of "\x. _ * x"] cong: if_cong) + done + show "\l i k - l i' k\ / real (p + 2) \ (1 + real p) * d / real (p + 2) / real (card ({..Suc p} - {i}))" + using i i' lf [of i] lf [of i'] 2 + by (auto simp: divide_simps image_iff) + qed auto + finally have "(\j\Suc p. \l i k / (p + 2) - l j k / (p + 2)\) \ (1 + real p) * d / (p + 2)" . + then have "\\j\Suc p. l i k / (p + 2) - l j k / (p + 2)\ \ (1 + real p) * d / (p + 2)" + by (rule order_trans [OF sum_abs]) + then show "\l i k - (\j\Suc p. l j k) / (2 + real p)\ \ (1 + real p) * d / (2 + real p)" + by (simp add: sum_subtractf sum_divide_distrib del: sum_atMost_Suc) + qed (use standard_simplex_def z in auto) + qed + have nonz: "\m (s - Suc 0) k - m (r - Suc 0) k\ \ (1 + real p) * d / (2 + real p)" (is "?lhs \ ?rhs") + if "r < s" and "0 < r" and "r \ Suc p" and "s \ Suc p" for r s + proof - + have "?lhs \ (p / (Suc p)) * d" + using m_in_gim [of "r - Suc 0"] m_in_gim [of "s - Suc 0"] that g by fastforce + also have "\ \ ?rhs" + by (simp add: field_simps \0 \ d\) + finally show ?thesis . + qed + have jj: "j \ Suc p \ j' \ Suc p + \ \(if j' = 0 then \i. (\j\Suc p. l j i) / (2 + real p) else m (j' -1)) k - + (if j = 0 then \i. (\j\Suc p. l j i) / (2 + real p) else m (j -1)) k\ + \ (1 + real p) * d / (2 + real p)" for j j' + apply (rule_tac a=j and b = "j'" in linorder_less_wlog) + apply (force simp: zero nonz \0 \ d\ simp del: sum_atMost_Suc)+ + done + show ?thesis + apply (rule convex_sum_bound_le) + using x' apply blast + using x' apply blast + apply (subst abs_minus_commute) + apply (rule convex_sum_bound_le) + using y' apply blast + using y' apply blast + using jj by blast + qed + then show "\simplex_cone p (Sigp f) (oriented_simplex p m) x k - simplex_cone p (Sigp f) (oriented_simplex p m) y k\ + \ (1 + real p) * d / (2 + real p)" + apply (simp add: feq Sigp_def simplicial_vertex_oriented_simplex simplex_cone del: sum_atMost_Suc) + apply (simp add: oriented_simplex_def x y del: sum_atMost_Suc) + done + qed + qed + show ?thesis + using Suc.IH [OF 1, where f=g] 2 3 by simp + qed + then show ?thesis + unfolding simplicial_chain_def simplicial_cone_def + by (simp add: order_trans [OF keys_frag_extend] sub UN_subset_iff) + qed + show ?case + using Suc + apply (simp del: sum_atMost_Suc) + apply (drule subsetD [OF keys_frag_extend]) + apply (simp del: sum_atMost_Suc) + apply clarify (*OBTAIN?*) + apply (rename_tac FFF) + using * + apply (simp add: add.commute Sigp_def subset_iff) + done +qed (auto simp: standard_simplex_0) + + +subsection\Singular subdivision\ + +definition singular_subdivision + where "singular_subdivision p \ + frag_extend + (\f. chain_map p f + (simplicial_subdivision p + (frag_of(restrict id (standard_simplex p)))))" + +lemma singular_subdivision_0 [simp]: "singular_subdivision p 0 = 0" + by (simp add: singular_subdivision_def) + +lemma singular_subdivision_add: + "singular_subdivision p (a + b) = singular_subdivision p a + singular_subdivision p b" + by (simp add: singular_subdivision_def frag_extend_add) + +lemma singular_subdivision_diff: + "singular_subdivision p (a - b) = singular_subdivision p a - singular_subdivision p b" + by (simp add: singular_subdivision_def frag_extend_diff) + +lemma simplicial_simplex_id [simp]: + "simplicial_simplex p S (restrict id (standard_simplex p)) \ standard_simplex p \ S" + (is "?lhs = ?rhs") +proof + assume ?lhs + then show ?rhs + by (simp add: simplicial_simplex_def singular_simplex_def continuous_map_in_subtopology set_mp) +next + assume R: ?rhs + then have cm: "continuous_map + (subtopology (powertop_real UNIV) (standard_simplex p)) + (subtopology (powertop_real UNIV) S) id" + using continuous_map_from_subtopology_mono continuous_map_id by blast + moreover have "\l. restrict id (standard_simplex p) = oriented_simplex p l" + apply (rule_tac x="\i j. if i = j then 1 else 0" in exI) + apply (force simp: oriented_simplex_def standard_simplex_def if_distrib [of "\u. u * _"] cong: if_cong) + done + ultimately show ?lhs + by (simp add: simplicial_simplex_def singular_simplex_def) +qed + +lemma singular_chain_singular_subdivision: + "singular_chain p X c + \ singular_chain p X (singular_subdivision p c)" + unfolding singular_subdivision_def + apply (rule singular_chain_extend) + apply (rule singular_chain_chain_map [where X = "subtopology (powertop_real UNIV) + (standard_simplex p)"]) + apply (simp add: simplicial_chain_simplicial_subdivision simplicial_imp_singular_chain) + by (simp add: singular_chain_def singular_simplex_def subset_iff) + +lemma naturality_singular_subdivision: + "singular_chain p X c + \ singular_subdivision p (chain_map p g c) = chain_map p g (singular_subdivision p c)" + unfolding singular_chain_def +proof (induction rule: frag_induction) + case (one f) + then have "singular_simplex p X f" + by auto + have "\simplicial_chain p (standard_simplex p) d\ + \ chain_map p (simplex_map p g f) d = chain_map p g (chain_map p f d)" for d + unfolding simplicial_chain_def + proof (induction rule: frag_induction) + case (one x) + then have "simplex_map p (simplex_map p g f) x = simplex_map p g (simplex_map p f x)" + by (force simp: simplex_map_def restrict_compose_left simplicial_simplex) + then show ?case + by auto + qed (auto simp: chain_map_diff) + then show ?case + using simplicial_chain_simplicial_subdivision [of p "standard_simplex p" "frag_of (restrict id (standard_simplex p))"] + by (simp add: singular_subdivision_def) +next + case (diff a b) + then show ?case + by (simp add: chain_map_diff singular_subdivision_diff) +qed auto + +lemma simplicial_chain_chain_map: + assumes f: "simplicial_simplex q X f" and c: "simplicial_chain p (standard_simplex q) c" + shows "simplicial_chain p X (chain_map p f c)" + using c unfolding simplicial_chain_def +proof (induction c rule: frag_induction) + case (one g) + have "\n. simplex_map p (oriented_simplex q l) + (oriented_simplex p m) = oriented_simplex p n" + if m: "singular_simplex p + (subtopology (powertop_real UNIV) (standard_simplex q)) (oriented_simplex p m)" + for l m + proof - + have "(\i. \j\p. m j i * x j) \ standard_simplex q" + if "x \ standard_simplex p" for x + using that m unfolding oriented_simplex_def singular_simplex_def + by (auto simp: continuous_map_in_subtopology image_subset_iff) + then show ?thesis + unfolding oriented_simplex_def simplex_map_def + apply (rule_tac x="\j k. (\i\q. l i k * m j i)" in exI) + apply (force simp: sum_distrib_left sum_distrib_right mult.assoc intro: sum.swap) + done + qed + then show ?case + using f one + apply (auto simp: simplicial_simplex_def) + apply (rule singular_simplex_simplex_map + [where X = "subtopology (powertop_real UNIV) (standard_simplex q)"]) + unfolding singular_simplex_def apply (fastforce simp add:)+ + done +next + case (diff a b) + then show ?case + by (metis chain_map_diff simplicial_chain_def simplicial_chain_diff) +qed auto + + +lemma singular_subdivision_simplicial_simplex: + "simplicial_chain p S c + \ singular_subdivision p c = simplicial_subdivision p c" +proof (induction p arbitrary: S c) + case 0 + then show ?case + unfolding simplicial_chain_def + proof (induction rule: frag_induction) + case (one x) + then show ?case + using singular_simplex_chain_map_id simplicial_imp_singular_simplex + by (fastforce simp: singular_subdivision_def simplicial_subdivision_def) + qed (auto simp: singular_subdivision_diff) +next + case (Suc p) + show ?case + using Suc.prems unfolding simplicial_chain_def + proof (induction rule: frag_induction) + case (one f) + then have ssf: "simplicial_simplex (Suc p) S f" + by (auto simp: simplicial_simplex) + then have 1: "simplicial_chain p (standard_simplex (Suc p)) + (simplicial_subdivision p + (chain_boundary (Suc p) + (frag_of (restrict id (standard_simplex (Suc p))))))" + by (metis diff_Suc_1 order_refl simplicial_chain_boundary simplicial_chain_of simplicial_chain_simplicial_subdivision simplicial_simplex_id) + have 2: "(\i. (\j\Suc p. simplicial_vertex j (restrict id (standard_simplex (Suc p))) i) / (real p + 2)) + \ standard_simplex (Suc p)" + by (simp add: simplicial_vertex_def standard_simplex_def del: sum_atMost_Suc) + have ss_Sp: "(\i. (if i \ Suc p then 1 else 0) / (real p + 2)) \ standard_simplex (Suc p)" + by (simp add: standard_simplex_def divide_simps) + obtain l where feq: "f = oriented_simplex (Suc p) l" + using one unfolding simplicial_simplex by blast + then have 3: "f (\i. (\j\Suc p. simplicial_vertex j (restrict id (standard_simplex (Suc p))) i) / (real p + 2)) + = (\i. (\j\Suc p. simplicial_vertex j f i) / (real p + 2))" + unfolding simplicial_vertex_def oriented_simplex_def + by (simp add: ss_Sp if_distrib [of "\x. _ * x"] sum_divide_distrib del: sum_atMost_Suc cong: if_cong) + have scp: "singular_chain (Suc p) + (subtopology (powertop_real UNIV) (standard_simplex (Suc p))) + (frag_of (restrict id (standard_simplex (Suc p))))" + by (simp add: simplicial_imp_singular_chain) + have scps: "simplicial_chain p (standard_simplex (Suc p)) + (chain_boundary (Suc p) (frag_of (restrict id (standard_simplex (Suc p)))))" + by (metis diff_Suc_1 order_refl simplicial_chain_boundary simplicial_chain_of simplicial_simplex_id) + have scpf: "simplicial_chain p S + (chain_map p f + (chain_boundary (Suc p) (frag_of (restrict id (standard_simplex (Suc p))))))" + using scps simplicial_chain_chain_map ssf by blast + have 4: "chain_map p f + (simplicial_subdivision p + (chain_boundary (Suc p) (frag_of (restrict id (standard_simplex (Suc p)))))) + = simplicial_subdivision p (chain_boundary (Suc p) (frag_of f))" + apply (simp add: chain_boundary_chain_map [OF scp] del: chain_map_of + flip: singular_simplex_chain_map_id [OF simplicial_imp_singular_simplex [OF ssf]]) + by (metis (no_types) scp singular_chain_boundary_alt Suc.IH [OF scps] Suc.IH [OF scpf] naturality_singular_subdivision) + show ?case + apply (simp add: singular_subdivision_def del: sum_atMost_Suc) + apply (simp only: ssf 1 2 3 4 chain_map_simplicial_cone [of "Suc p" S _ p "Suc p"]) + done + qed (auto simp: frag_extend_diff singular_subdivision_diff) +qed + + +lemma naturality_simplicial_subdivision: + "\simplicial_chain p (standard_simplex q) c; simplicial_simplex q S g\ + \ simplicial_subdivision p (chain_map p g c) = chain_map p g (simplicial_subdivision p c)" +apply (simp flip: singular_subdivision_simplicial_simplex) + by (metis naturality_singular_subdivision simplicial_chain_chain_map simplicial_imp_singular_chain singular_subdivision_simplicial_simplex) + +lemma chain_boundary_singular_subdivision: + "singular_chain p X c + \ chain_boundary p (singular_subdivision p c) = + singular_subdivision (p - Suc 0) (chain_boundary p c)" + unfolding singular_chain_def +proof (induction rule: frag_induction) + case (one f) + then have ssf: "singular_simplex p X f" + by (auto simp: singular_simplex_def) + then have scp: "simplicial_chain p (standard_simplex p) (frag_of (restrict id (standard_simplex p)))" + by simp + have scp1: "simplicial_chain (p - Suc 0) (standard_simplex p) + (chain_boundary p (frag_of (restrict id (standard_simplex p))))" + using simplicial_chain_boundary by force + have sgp1: "singular_chain (p - Suc 0) + (subtopology (powertop_real UNIV) (standard_simplex p)) + (chain_boundary p (frag_of (restrict id (standard_simplex p))))" + using scp1 simplicial_imp_singular_chain by blast + have scpp: "singular_chain p (subtopology (powertop_real UNIV) (standard_simplex p)) + (frag_of (restrict id (standard_simplex p)))" + using scp simplicial_imp_singular_chain by blast + then show ?case + unfolding singular_subdivision_def + using chain_boundary_chain_map [of p "subtopology (powertop_real UNIV) + (standard_simplex p)" _ f] + apply (simp add: simplicial_chain_simplicial_subdivision + simplicial_imp_singular_chain chain_boundary_simplicial_subdivision [OF scp] + flip: singular_subdivision_simplicial_simplex [OF scp1] naturality_singular_subdivision [OF sgp1]) + by (metis (full_types) singular_subdivision_def chain_boundary_chain_map [OF scpp] singular_simplex_chain_map_id [OF ssf]) +qed (auto simp: singular_subdivision_def frag_extend_diff chain_boundary_diff) + +lemma singular_subdivision_zero: + "singular_chain 0 X c \ singular_subdivision 0 c = c" + unfolding singular_chain_def +proof (induction rule: frag_induction) + case (one f) + then have "restrict (f \ restrict id (standard_simplex 0)) (standard_simplex 0) = f" + by (simp add: extensional_restrict restrict_compose_right singular_simplex_def) + then show ?case + by (auto simp: singular_subdivision_def simplex_map_def) +qed (auto simp: singular_subdivision_def frag_extend_diff) + + +primrec subd where + "subd 0 = (\x. 0)" +| "subd (Suc p) = + frag_extend + (\f. simplicial_cone (Suc p) (\i. (\j\Suc p. simplicial_vertex j f i) / real (Suc p + 1)) + (simplicial_subdivision (Suc p) (frag_of f) - frag_of f - + subd p (chain_boundary (Suc p) (frag_of f))))" + +lemma subd_0 [simp]: "subd p 0 = 0" + by (induction p) auto + +lemma subd_diff [simp]: "subd p (c1 - c2) = subd p c1 - subd p c2" + by (induction p) (auto simp: frag_extend_diff) + +lemma subd_uminus [simp]: "subd p (-c) = - subd p c" + by (metis diff_0 subd_0 subd_diff) + +lemma subd_power_uminus: "subd p (frag_cmul ((-1) ^ k) c) = frag_cmul ((-1) ^ k) (subd p c)" + apply (induction k, simp_all) + by (metis minus_frag_cmul subd_uminus) + +lemma subd_power_sum: "subd p (sum f I) = sum (subd p \ f) I" + apply (induction I rule: infinite_finite_induct) + by auto (metis add_diff_cancel_left' diff_add_cancel subd_diff) + +lemma subd: "simplicial_chain p (standard_simplex s) c + \ (\r g. simplicial_simplex s (standard_simplex r) g \ chain_map (Suc p) g (subd p c) = subd p (chain_map p g c)) + \ simplicial_chain (Suc p) (standard_simplex s) (subd p c) + \ (chain_boundary (Suc p) (subd p c)) + (subd (p - Suc 0) (chain_boundary p c)) = (simplicial_subdivision p c) - c" +proof (induction p arbitrary: c) + case (Suc p) + show ?case + using Suc.prems [unfolded simplicial_chain_def] + proof (induction rule: frag_induction) + case (one f) + then obtain l where l: "(\x i. \j\Suc p. l j i * x j) ` standard_simplex (Suc p) \ standard_simplex s" + and feq: "f = oriented_simplex (Suc p) l" + by (metis (mono_tags) mem_Collect_eq simplicial_simplex simplicial_simplex_oriented_simplex) + have scf: "simplicial_chain (Suc p) (standard_simplex s) (frag_of f)" + using one by simp + have lss: "l i \ standard_simplex s" if "i \ Suc p" for i + proof - + have "(\i'. \j\Suc p. l j i' * (if j = i then 1 else 0)) \ standard_simplex s" + using subsetD [OF l] basis_in_standard_simplex that by blast + moreover have "(\i'. \j\Suc p. l j i' * (if j = i then 1 else 0)) = l i" + using that by (simp add: if_distrib [of "\x. _ * x"] del: sum_atMost_Suc cong: if_cong) + ultimately show ?thesis + by simp + qed + have *: "(\i. i \ n \ l i \ standard_simplex s) + \ (\i. (\j\n. l j i) / (Suc n)) \ standard_simplex s" for n + proof (induction n) + case (Suc n) + let ?x = "\i. (1 - inverse (n + 2)) * ((\j\n. l j i) / (Suc n)) + inverse (n + 2) * l (Suc n) i" + have "?x \ standard_simplex s" + proof (rule convex_standard_simplex) + show "(\i. (\j\n. l j i) / real (Suc n)) \ standard_simplex s" + using Suc by simp + qed (auto simp: lss Suc inverse_le_1_iff) + moreover have "?x = (\i. (\j\Suc n. l j i) / real (Suc (Suc n)))" + by (force simp: divide_simps) + ultimately show ?case + by simp + qed auto + have **: "(\i. (\j\Suc p. simplicial_vertex j f i) / (2 + real p)) \ standard_simplex s" + using * [of "Suc p"] lss by (simp add: simplicial_vertex_oriented_simplex feq) + show ?case + proof (intro conjI impI allI) + fix r g + assume g: "simplicial_simplex s (standard_simplex r) g" + then obtain m where geq: "g = oriented_simplex s m" + using simplicial_simplex by blast + have 1: "simplicial_chain (Suc p) (standard_simplex s) (simplicial_subdivision (Suc p) (frag_of f))" + by (metis mem_Collect_eq one.hyps simplicial_chain_of simplicial_chain_simplicial_subdivision) + have 2: "(\j\Suc p. \i\s. m i k * simplicial_vertex j f i) + = (\j\Suc p. simplicial_vertex j + (simplex_map (Suc p) (oriented_simplex s m) f) k)" for k + proof (rule sum.cong [OF refl]) + fix j + assume j: "j \ {..Suc p}" + have eq: "simplex_map (Suc p) (oriented_simplex s m) (oriented_simplex (Suc p) l) + = oriented_simplex (Suc p) (oriented_simplex s m \ l)" + proof (rule simplex_map_oriented_simplex) + show "simplicial_simplex (Suc p) (standard_simplex s) (oriented_simplex (Suc p) l)" + using one by (simp add: feq flip: oriented_simplex_def) + show "simplicial_simplex s (standard_simplex r) (oriented_simplex s m)" + using g by (simp add: geq) + qed auto + show "(\i\s. m i k * simplicial_vertex j f i) + = simplicial_vertex j (simplex_map (Suc p) (oriented_simplex s m) f) k" + using one j + apply (simp add: feq eq simplicial_vertex_oriented_simplex simplicial_simplex_oriented_simplex image_subset_iff) + apply (drule_tac x="(\i. if i = j then 1 else 0)" in bspec) + apply (auto simp: oriented_simplex_def lss) + done + qed + have 4: "chain_map (Suc p) g (subd p (chain_boundary (Suc p) (frag_of f))) + = subd p (chain_boundary (Suc p) (frag_of (simplex_map (Suc p) g f)))" + by (metis (no_types) One_nat_def scf Suc.IH chain_boundary_chain_map chain_map_of diff_Suc_Suc diff_zero g simplicial_chain_boundary simplicial_imp_singular_chain) + show "chain_map (Suc (Suc p)) g (subd (Suc p) (frag_of f)) = subd (Suc p) (chain_map (Suc p) g (frag_of f))" + using g + apply (simp only: subd.simps frag_extend_of) + apply (subst chain_map_simplicial_cone [of s "standard_simplex r" _ "Suc p" s], assumption) + apply (intro simplicial_chain_diff) + using "1" apply auto[1] + using one.hyps apply auto[1] + apply (metis Suc.IH diff_Suc_1 mem_Collect_eq one.hyps simplicial_chain_boundary simplicial_chain_of) + using "**" apply auto[1] + apply (rule order_refl) + apply (simp only: chain_map_of frag_extend_of) + apply (rule arg_cong2 [where f = "simplicial_cone (Suc p)"]) + apply (simp add: geq sum_distrib_left oriented_simplex_def ** del: sum_atMost_Suc flip: sum_divide_distrib) + using 2 apply (simp only: oriented_simplex_def sum.swap [where A = "{..s}"]) + using naturality_simplicial_subdivision scf apply (fastforce simp add: 4 chain_map_diff) + done + next + have sc: "simplicial_chain (Suc p) (standard_simplex s) + (simplicial_cone p + (\i. (\j\Suc p. simplicial_vertex j f i) / (Suc (Suc p))) + (simplicial_subdivision p + (chain_boundary (Suc p) (frag_of f))))" + by (metis diff_Suc_1 nat.simps(3) simplicial_subdivision_of scf simplicial_chain_simplicial_subdivision) + have ff: "simplicial_chain (Suc p) (standard_simplex s) (subd p (chain_boundary (Suc p) (frag_of f)))" + by (metis (no_types) Suc.IH diff_Suc_1 scf simplicial_chain_boundary) + show "simplicial_chain (Suc (Suc p)) (standard_simplex s) (subd (Suc p) (frag_of f))" + using one + apply (simp only: subd.simps frag_extend_of) + apply (rule_tac S="standard_simplex s" in simplicial_chain_simplicial_cone) + apply (intro simplicial_chain_diff ff) + using sc apply (simp add: algebra_simps) + using "**" convex_standard_simplex apply force+ + done + have "simplicial_chain p (standard_simplex s) (chain_boundary (Suc p) (frag_of f))" + using scf simplicial_chain_boundary by fastforce + then have "chain_boundary (Suc p) (simplicial_subdivision (Suc p) (frag_of f) - frag_of f + - subd p (chain_boundary (Suc p) (frag_of f))) = 0" + apply (simp only: chain_boundary_diff) + using Suc.IH chain_boundary_boundary [of "Suc p" "subtopology (powertop_real UNIV) + (standard_simplex s)" "frag_of f"] + by (metis One_nat_def add_diff_cancel_left' subd_0 chain_boundary_simplicial_subdivision plus_1_eq_Suc scf simplicial_imp_singular_chain) + then show "chain_boundary (Suc (Suc p)) (subd (Suc p) (frag_of f)) + + subd (Suc p - Suc 0) (chain_boundary (Suc p) (frag_of f)) + = simplicial_subdivision (Suc p) (frag_of f) - frag_of f" + apply (simp only: subd.simps frag_extend_of) + apply (subst chain_boundary_simplicial_cone [of "Suc p" "standard_simplex s"]) + apply (meson ff scf simplicial_chain_diff simplicial_chain_simplicial_subdivision) + apply (simp add: simplicial_cone_def del: sum_atMost_Suc simplicial_subdivision.simps) + done + qed + next + case (diff a b) + then show ?case + apply safe + apply (metis chain_map_diff subd_diff) + apply (metis simplicial_chain_diff subd_diff) + apply (auto simp: simplicial_subdivision_diff chain_boundary_diff + simp del: simplicial_subdivision.simps subd.simps) + by (metis (no_types, lifting) add_diff_add add_uminus_conv_diff diff_0 diff_diff_add) + qed auto +qed simp + +lemma chain_homotopic_simplicial_subdivision1: + "\simplicial_chain p (standard_simplex q) c; simplicial_simplex q (standard_simplex r) g\ + \ chain_map (Suc p) g (subd p c) = subd p (chain_map p g c)" + by (simp add: subd) + +lemma chain_homotopic_simplicial_subdivision2: + "simplicial_chain p (standard_simplex q) c + \ simplicial_chain (Suc p) (standard_simplex q) (subd p c)" + by (simp add: subd) + +lemma chain_homotopic_simplicial_subdivision3: + "simplicial_chain p (standard_simplex q) c + \ chain_boundary (Suc p) (subd p c) = (simplicial_subdivision p c) - c - subd (p - Suc 0) (chain_boundary p c)" + by (simp add: subd algebra_simps) + +lemma chain_homotopic_simplicial_subdivision: + "\h. (\p. h p 0 = 0) \ + (\p c1 c2. h p (c1-c2) = h p c1 - h p c2) \ + (\p q r g c. + simplicial_chain p (standard_simplex q) c + \ simplicial_simplex q (standard_simplex r) g + \ chain_map (Suc p) g (h p c) = h p (chain_map p g c)) \ + (\p q c. simplicial_chain p (standard_simplex q) c + \ simplicial_chain (Suc p) (standard_simplex q) (h p c)) \ + (\p q c. simplicial_chain p (standard_simplex q) c + \ chain_boundary (Suc p) (h p c) + h (p - Suc 0) (chain_boundary p c) + = (simplicial_subdivision p c) - c)" + by (rule_tac x=subd in exI) (fastforce simp: subd) + +lemma chain_homotopic_singular_subdivision: + obtains h where + "\p. h p 0 = 0" + "\p c1 c2. h p (c1-c2) = h p c1 - h p c2" + "\p X c. singular_chain p X c \ singular_chain (Suc p) X (h p c)" + "\p X c. singular_chain p X c + \ chain_boundary (Suc p) (h p c) + h (p - Suc 0) (chain_boundary p c) = singular_subdivision p c - c" +proof - + define k where "k \ \p. frag_extend (\f:: (nat \ real) \ 'a. chain_map (Suc p) f (subd p (frag_of(restrict id (standard_simplex p)))))" + show ?thesis + proof + fix p X and c :: "'a chain" + assume c: "singular_chain p X c" + have "singular_chain (Suc p) X (k p c) \ + chain_boundary (Suc p) (k p c) + k (p - Suc 0) (chain_boundary p c) = singular_subdivision p c - c" + using c [unfolded singular_chain_def] + proof (induction rule: frag_induction) + case (one f) + let ?X = "subtopology (powertop_real UNIV) (standard_simplex p)" + show ?case + proof (simp add: k_def, intro conjI) + show "singular_chain (Suc p) X (chain_map (Suc p) f (subd p (frag_of (restrict id (standard_simplex p)))))" + proof (rule singular_chain_chain_map) + show "singular_chain (Suc p) ?X (subd p (frag_of (restrict id (standard_simplex p))))" + by (simp add: chain_homotopic_simplicial_subdivision2 simplicial_imp_singular_chain) + show "continuous_map ?X X f" + using one.hyps singular_simplex_def by auto + qed + next + have scp: "singular_chain (Suc p) ?X (subd p (frag_of (restrict id (standard_simplex p))))" + by (simp add: chain_homotopic_simplicial_subdivision2 simplicial_imp_singular_chain) + have feqf: "frag_of (simplex_map p f (restrict id (standard_simplex p))) = frag_of f" + using one.hyps singular_simplex_chain_map_id by auto + have *: "chain_map p f + (subd (p - Suc 0) + (\k\p. frag_cmul ((-1) ^ k) (frag_of (singular_face p k id)))) + = (\x\p. frag_cmul ((-1) ^ x) + (chain_map p (singular_face p x f) + (subd (p - Suc 0) (frag_of (restrict id (standard_simplex (p - Suc 0)))))))" + (is "?lhs = ?rhs") + if "p > 0" + proof - + have eqc: "subd (p - Suc 0) (frag_of (singular_face p i id)) + = chain_map p (singular_face p i id) + (subd (p - Suc 0) (frag_of (restrict id (standard_simplex (p - Suc 0)))))" + if "i \ p" for i + proof - + have 1: "simplicial_chain (p - Suc 0) (standard_simplex (p - Suc 0)) + (frag_of (restrict id (standard_simplex (p - Suc 0))))" + by simp + have 2: "simplicial_simplex (p - Suc 0) (standard_simplex p) (singular_face p i id)" + by (metis One_nat_def Suc_leI \0 < p\ simplicial_simplex_id simplicial_simplex_singular_face singular_face_restrict subsetI that) + have 3: "simplex_map (p - Suc 0) (singular_face p i id) (restrict id (standard_simplex (p - Suc 0))) + = singular_face p i id" + by (force simp: simplex_map_def singular_face_def) + show ?thesis + using chain_homotopic_simplicial_subdivision1 [OF 1 2] + that \p > 0\ by (simp add: 3) + qed + have xx: "simplicial_chain p (standard_simplex(p - Suc 0)) + (subd (p - Suc 0) (frag_of (restrict id (standard_simplex (p - Suc 0)))))" + by (metis Suc_pred chain_homotopic_simplicial_subdivision2 order_refl simplicial_chain_of simplicial_simplex_id that) + have yy: "\k. k \ p \ + chain_map p f + (chain_map p (singular_face p k id) h) = chain_map p (singular_face p k f) h" + if "simplicial_chain p (standard_simplex(p - Suc 0)) h" for h + using that unfolding simplicial_chain_def + proof (induction h rule: frag_induction) + case (one x) + then show ?case + using one + apply (simp add: chain_map_of singular_simplex_def simplicial_simplex_def, auto) + apply (rule_tac f=frag_of in arg_cong, rule) + apply (simp add: simplex_map_def) + by (simp add: continuous_map_in_subtopology image_subset_iff singular_face_def) + qed (auto simp: chain_map_diff) + have "?lhs + = chain_map p f + (\k\p. frag_cmul ((-1) ^ k) + (chain_map p (singular_face p k id) + (subd (p - Suc 0) (frag_of (restrict id (standard_simplex (p - Suc 0)))))))" + by (simp add: subd_power_sum subd_power_uminus eqc) + also have "\ = ?rhs" + by (simp add: chain_map_sum xx yy) + finally show ?thesis . + qed + have "chain_map p f + (simplicial_subdivision p (frag_of (restrict id (standard_simplex p))) + - subd (p - Suc 0) (chain_boundary p (frag_of (restrict id (standard_simplex p))))) + = singular_subdivision p (frag_of f) + - frag_extend + (\f. chain_map (Suc (p - Suc 0)) f + (subd (p - Suc 0) (frag_of (restrict id (standard_simplex (p - Suc 0)))))) + (chain_boundary p (frag_of f))" + apply (simp add: singular_subdivision_def chain_map_diff) + apply (clarsimp simp add: chain_boundary_def) + apply (simp add: frag_extend_sum frag_extend_cmul *) + done + then show "chain_boundary (Suc p) (chain_map (Suc p) f (subd p (frag_of (restrict id (standard_simplex p))))) + + frag_extend + (\f. chain_map (Suc (p - Suc 0)) f + (subd (p - Suc 0) (frag_of (restrict id (standard_simplex (p - Suc 0)))))) + (chain_boundary p (frag_of f)) + = singular_subdivision p (frag_of f) - frag_of f" + by (simp add: chain_boundary_chain_map [OF scp] chain_homotopic_simplicial_subdivision3 [where q=p] chain_map_diff feqf) + qed + next + case (diff a b) + then show ?case + apply (simp only: k_def singular_chain_diff chain_boundary_diff frag_extend_diff singular_subdivision_diff) + by (metis (no_types, lifting) add_diff_add diff_add_cancel) + qed (auto simp: k_def) + then show "singular_chain (Suc p) X (k p c)" "chain_boundary (Suc p) (k p c) + k (p - Suc 0) (chain_boundary p c) = singular_subdivision p c - c" + by auto + qed (auto simp: k_def frag_extend_diff) +qed + + +lemma homologous_rel_singular_subdivision: + assumes "singular_relcycle p X T c" + shows "homologous_rel p X T (singular_subdivision p c) c" +proof (cases "p = 0") + case True + with assms show ?thesis + by (auto simp: singular_relcycle_def singular_subdivision_zero) +next + case False + with assms show ?thesis + unfolding homologous_rel_def singular_relboundary singular_relcycle + by (metis One_nat_def Suc_diff_1 chain_homotopic_singular_subdivision gr_zeroI) +qed + + +subsection\Excision argument that we keep doing singular subdivision\ + +lemma singular_subdivision_power_0 [simp]: "(singular_subdivision p ^^ n) 0 = 0" + by (induction n) auto + +lemma singular_subdivision_power_diff: + "(singular_subdivision p ^^ n) (a - b) = (singular_subdivision p ^^ n) a - (singular_subdivision p ^^ n) b" + by (induction n) (auto simp: singular_subdivision_diff) + +lemma iterated_singular_subdivision: + "singular_chain p X c + \ (singular_subdivision p ^^ n) c = + frag_extend + (\f. chain_map p f + ((simplicial_subdivision p ^^ n) + (frag_of(restrict id (standard_simplex p))))) c" +proof (induction n arbitrary: c) + case 0 + then show ?case + unfolding singular_chain_def + proof (induction c rule: frag_induction) + case (one f) + then have "restrict f (standard_simplex p) = f" + by (simp add: extensional_restrict singular_simplex_def) + then show ?case + by (auto simp: simplex_map_def cong: restrict_cong) + qed (auto simp: frag_extend_diff) +next + case (Suc n) + show ?case + using Suc.prems unfolding singular_chain_def + proof (induction c rule: frag_induction) + case (one f) + then have "singular_simplex p X f" + by simp + have scp: "simplicial_chain p (standard_simplex p) + ((simplicial_subdivision p ^^ n) (frag_of (restrict id (standard_simplex p))))" + proof (induction n) + case 0 + then show ?case + by (metis funpow_0 order_refl simplicial_chain_of simplicial_simplex_id) + next + case (Suc n) + then show ?case + by (simp add: simplicial_chain_simplicial_subdivision) + qed + have scnp: "simplicial_chain p (standard_simplex p) + ((simplicial_subdivision p ^^ n) (frag_of (\x\standard_simplex p. x)))" + proof (induction n) + case 0 + then show ?case + by (metis eq_id_iff funpow_0 order_refl simplicial_chain_of simplicial_simplex_id) + next + case (Suc n) + then show ?case + by (simp add: simplicial_chain_simplicial_subdivision) + qed + have sff: "singular_chain p X (frag_of f)" + by (simp add: \singular_simplex p X f\ singular_chain_of) + then show ?case + using Suc.IH [OF sff] naturality_singular_subdivision [OF simplicial_imp_singular_chain [OF scp], of f] singular_subdivision_simplicial_simplex [OF scnp] + by (simp add: singular_chain_of id_def del: restrict_apply) + qed (auto simp: singular_subdivision_power_diff singular_subdivision_diff frag_extend_diff) +qed + + +lemma chain_homotopic_iterated_singular_subdivision: + obtains h where + "\p. h p 0 = (0 :: 'a chain)" + "\p c1 c2. h p (c1-c2) = h p c1 - h p c2" + "\p X c. singular_chain p X c \ singular_chain (Suc p) X (h p c)" + "\p X c. singular_chain p X c + \ chain_boundary (Suc p) (h p c) + h (p - Suc 0) (chain_boundary p c) + = (singular_subdivision p ^^ n) c - c" +proof (induction n arbitrary: thesis) + case 0 + show ?case + by (rule 0 [of "(\p x. 0)"]) auto +next + case (Suc n) + then obtain k where k: + "\p. k p 0 = (0 :: 'a chain)" + "\p c1 c2. k p (c1-c2) = k p c1 - k p c2" + "\p X c. singular_chain p X c \ singular_chain (Suc p) X (k p c)" + "\p X c. singular_chain p X c + \ chain_boundary (Suc p) (k p c) + k (p - Suc 0) (chain_boundary p c) + = (singular_subdivision p ^^ n) c - c" + by metis + obtain h where h: + "\p. h p 0 = (0 :: 'a chain)" + "\p c1 c2. h p (c1-c2) = h p c1 - h p c2" + "\p X c. singular_chain p X c \ singular_chain (Suc p) X (h p c)" + "\p X c. singular_chain p X c + \ chain_boundary (Suc p) (h p c) + h (p - Suc 0) (chain_boundary p c) = singular_subdivision p c - c" + by (blast intro: chain_homotopic_singular_subdivision) + let ?h = "(\p c. singular_subdivision (Suc p) (k p c) + h p c)" + show ?case + proof (rule Suc.prems) + fix p X and c :: "'a chain" + assume "singular_chain p X c" + then show "singular_chain (Suc p) X (?h p c)" + by (simp add: h k singular_chain_add singular_chain_singular_subdivision) + next + fix p :: "nat" and X :: "'a topology" and c :: "'a chain" + assume sc: "singular_chain p X c" + have f5: "chain_boundary (Suc p) (singular_subdivision (Suc p) (k p c)) = singular_subdivision p (chain_boundary (Suc p) (k p c))" + using chain_boundary_singular_subdivision k(3) sc by fastforce + have [simp]: "singular_subdivision (Suc (p - Suc 0)) (k (p - Suc 0) (chain_boundary p c)) = + singular_subdivision p (k (p - Suc 0) (chain_boundary p c))" + proof (cases p) + case 0 + then show ?thesis + by (simp add: k chain_boundary_def) + qed auto + show "chain_boundary (Suc p) (?h p c) + ?h (p - Suc 0) (chain_boundary p c) = (singular_subdivision p ^^ Suc n) c - c" + using chain_boundary_singular_subdivision [of "Suc p" X] + apply (simp add: chain_boundary_add f5 h k algebra_simps) + apply (erule thin_rl) + using h(4) [OF sc] k(4) [OF sc] singular_subdivision_add [of p "chain_boundary (Suc p) (k p c)" "k (p - Suc 0) (chain_boundary p c)"] + apply (simp add: algebra_simps) + by (smt add.assoc add.left_commute singular_subdivision_add) + qed (auto simp: k h singular_subdivision_diff) +qed + +lemma llemma: + assumes p: "standard_simplex p \ \\" + and \: "\U. U \ \ \ openin (powertop_real UNIV) U" + obtains d where "0 < d" + "\K. \K \ standard_simplex p; + \x y i. \i \ p; x \ K; y \ K\ \ \x i - y i\ \ d\ + \ \U. U \ \ \ K \ U" +proof - + have "\e U. 0 < e \ U \ \ \ x \ U \ + (\y. (\i\p. \y i - x i\ \ 2 * e) \ (\i>p. y i = 0) \ y \ U)" + if x: "x \ standard_simplex p" for x + proof- + obtain U where U: "U \ \" "x \ U" + using x p by blast + then obtain V where finV: "finite {i. V i \ UNIV}" and openV: "\i. open (V i)" + and xV: "x \ Pi\<^sub>E UNIV V" and UV: "Pi\<^sub>E UNIV V \ U" + using \ unfolding openin_product_topology_alt by force + have xVi: "x i \ V i" for i + using PiE_mem [OF xV] by simp + have "\i. \e>0. \x'. \x' - x i\ < e \ x' \ V i" + by (rule openV [unfolded open_real, rule_format, OF xVi]) + then obtain d where d: "\i. d i > 0" and dV: "\i x'. \x' - x i\ < d i \ x' \ V i" + by metis + define e where "e \ Inf (insert 1 (d ` {i. V i \ UNIV})) / 3" + have ed3: "e \ d i / 3" if "V i \ UNIV" for i + using that finV by (auto simp: e_def intro: cInf_le_finite) + show "\e U. 0 < e \ U \ \ \ x \ U \ + (\y. (\i\p. \y i - x i\ \ 2 * e) \ (\i>p. y i = 0) \ y \ U)" + proof (intro exI conjI allI impI) + show "e > 0" + using d finV by (simp add: e_def finite_less_Inf_iff) + fix y assume y: "(\i\p. \y i - x i\ \ 2 * e) \ (\i>p. y i = 0)" + have "y \ Pi\<^sub>E UNIV V" + proof + show "y i \ V i" for i + proof (cases "p < i") + case True + then show ?thesis + by (metis (mono_tags, lifting) y x mem_Collect_eq standard_simplex_def xVi) + next + case False show ?thesis + proof (cases "V i = UNIV") + case False show ?thesis + proof (rule dV) + have "\y i - x i\ \ 2 * e" + using y \\ p < i\ by simp + also have "\ < d i" + using ed3 [OF False] \e > 0\ by simp + finally show "\y i - x i\ < d i" . + qed + qed auto + qed + qed auto + with UV show "y \ U" + by blast + qed (use U in auto) + qed + then obtain e U where + eU: "\x. x \ standard_simplex p \ + 0 < e x \ U x \ \ \ x \ U x" + and UI: "\x y. \x \ standard_simplex p; \i. i \ p \ \y i - x i\ \ 2 * e x; \i. i > p \ y i = 0\ + \ y \ U x" + by metis + define F where "F \ \x. Pi\<^sub>E UNIV (\i. if i \ p then {x i - e x<..S \ F ` standard_simplex p. openin (powertop_real UNIV) S" + by (simp add: F_def openin_PiE_gen) + moreover have pF: "standard_simplex p \ \(F ` standard_simplex p)" + by (force simp: F_def PiE_iff eU) + ultimately have "\\. finite \ \ \ \ F ` standard_simplex p \ standard_simplex p \ \\" + using compactin_standard_simplex [of p] + unfolding compactin_def by force + then obtain S where "finite S" and ssp: "S \ standard_simplex p" "standard_simplex p \ \(F ` S)" + unfolding exists_finite_subset_image by (auto simp: exists_finite_subset_image) + then have "S \ {}" + by (auto simp: nonempty_standard_simplex) + show ?thesis + proof + show "Inf (e ` S) > 0" + using \finite S\ \S \ {}\ ssp eU by (auto simp: finite_less_Inf_iff) + fix k :: "(nat \ real) set" + assume k: "k \ standard_simplex p" + and kle: "\x y i. \i \ p; x \ k; y \ k\ \ \x i - y i\ \ Inf (e ` S)" + show "\U. U \ \ \ k \ U" + proof (cases "k = {}") + case True + then show ?thesis + using \S \ {}\ eU equals0I ssp(1) subset_eq p by auto + next + case False + with k ssp obtain x a where "x \ k" "x \ standard_simplex p" + and a: "a \ S" and Fa: "x \ F a" + by blast + then have le_ea: "\i. i \ p \ abs (x i - a i) < e a" + by (simp add: F_def PiE_iff if_distrib abs_diff_less_iff cong: if_cong) + show ?thesis + proof (intro exI conjI) + show "U a \ \" + using a eU ssp(1) by auto + show "k \ U a" + proof clarify + fix y assume "y \ k" + with k have y: "y \ standard_simplex p" + by blast + show "y \ U a" + proof (rule UI) + show "a \ standard_simplex p" + using a ssp(1) by auto + fix i :: "nat" + assume "i \ p" + then have "\x i - y i\ \ e a" + by (meson kle [OF \i \ p\] a \finite S\ \x \ k\ \y \ k\ cInf_le_finite finite_imageI imageI order_trans) + then show "\y i - a i\ \ 2 * e a" + using le_ea [OF \i \ p\] by linarith + next + fix i assume "p < i" + then show "y i = 0" + using standard_simplex_def y by auto + qed + qed + qed + qed + qed +qed + + +proposition sufficient_iterated_singular_subdivision_exists: + assumes \: "\U. U \ \ \ openin X U" + and X: "topspace X \ \\" + and p: "singular_chain p X c" + obtains n where "\m f. \n \ m; f \ Poly_Mapping.keys ((singular_subdivision p ^^ m) c)\ + \ \V \ \. f ` (standard_simplex p) \ V" +proof (cases "c = 0") + case False + then show ?thesis + proof (cases "topspace X = {}") + case True + show ?thesis + using p that by (force simp: singular_chain_empty True) + next + case False + show ?thesis + proof (cases "\ = {}") + case True + then show ?thesis + using False X by blast + next + case False + have "\e. 0 < e \ + (\K. K \ standard_simplex p \ (\x y i. x \ K \ y \ K \ i \ p \ \x i - y i\ \ e) + \ (\V. V \ \ \ f ` K \ V))" + if f: "f \ Poly_Mapping.keys c" for f + proof - + have ssf: "singular_simplex p X f" + using f p by (auto simp: singular_chain_def) + then have fp: "\x. x \ standard_simplex p \ f x \ topspace X" + by (auto simp: singular_simplex_def image_subset_iff dest: continuous_map_image_subset_topspace) + have "\T. openin (powertop_real UNIV) T \ + standard_simplex p \ f -` V = T \ standard_simplex p" + if V: "V \ \" for V + proof - + have "singular_simplex p X f" + using p f unfolding singular_chain_def by blast + then have "openin (subtopology (powertop_real UNIV) (standard_simplex p)) + {x \ standard_simplex p. f x \ V}" + using \ [OF \V \ \\] by (simp add: singular_simplex_def continuous_map_def) + moreover have "standard_simplex p \ f -` V = {x \ standard_simplex p. f x \ V}" + by blast + ultimately show ?thesis + by (simp add: openin_subtopology) + qed + then obtain g where gope: "\V. V \ \ \ openin (powertop_real UNIV) (g V)" + and geq: "\V. V \ \ \ standard_simplex p \ f -` V = g V \ standard_simplex p" + by metis + obtain d where "0 < d" + and d: "\K. \K \ standard_simplex p; \x y i. \i \ p; x \ K; y \ K\ \ \x i - y i\ \ d\ + \ \U. U \ g ` \ \ K \ U" + proof (rule llemma [of p "g ` \"]) + show "standard_simplex p \ \(g ` \)" + using geq X fp by (fastforce simp add:) + show "openin (powertop_real UNIV) U" if "U \ g ` \" for U :: "(nat \ real) set" + using gope that by blast + qed auto + show ?thesis + proof (rule exI, intro allI conjI impI) + fix K :: "(nat \ real) set" + assume K: "K \ standard_simplex p" + and Kd: "\x y i. x \ K \ y \ K \ i \ p \ \x i - y i\ \ d" + then have "\U. U \ g ` \ \ K \ U" + using d [OF K] by auto + then show "\V. V \ \ \ f ` K \ V" + using K geq by fastforce + qed (rule \d > 0\) + qed + then obtain \ where epos: "\f \ Poly_Mapping.keys c. 0 < \ f" + and e: "\f K. \f \ Poly_Mapping.keys c; K \ standard_simplex p; + \x y i. x \ K \ y \ K \ i \ p \ \x i - y i\ \ \ f\ + \ \V. V \ \ \ f ` K \ V" + by metis + obtain d where "0 < d" + and d: "\f K. \f \ Poly_Mapping.keys c; K \ standard_simplex p; + \x y i. \x \ K; y \ K; i \ p\ \ \x i - y i\ \ d\ + \ \V. V \ \ \ f ` K \ V" + proof + show "Inf (\ ` Poly_Mapping.keys c) > 0" + by (simp add: finite_less_Inf_iff \c \ 0\ epos) + fix f K + assume fK: "f \ Poly_Mapping.keys c" "K \ standard_simplex p" + and le: "\x y i. \x \ K; y \ K; i \ p\ \ \x i - y i\ \ Inf (\ ` Poly_Mapping.keys c)" + then have lef: "Inf (\ ` Poly_Mapping.keys c) \ \ f" + by (auto intro: cInf_le_finite) + show "\V. V \ \ \ f ` K \ V" + using le lef by (blast intro: dual_order.trans e [OF fK]) + qed + let ?d = "\m. (simplicial_subdivision p ^^ m) (frag_of (restrict id (standard_simplex p)))" + obtain n where n: "(p / (Suc p)) ^ n < d" + using real_arch_pow_inv \0 < d\ by fastforce + show ?thesis + proof + fix m h + assume "n \ m" and "h \ Poly_Mapping.keys ((singular_subdivision p ^^ m) c)" + then obtain f where "f \ Poly_Mapping.keys c" "h \ Poly_Mapping.keys (chain_map p f (?d m))" + using subsetD [OF keys_frag_extend] iterated_singular_subdivision [OF p, of m] by force + then obtain g where g: "g \ Poly_Mapping.keys (?d m)" and heq: "h = restrict (f \ g) (standard_simplex p)" + using keys_frag_extend by (force simp: chain_map_def simplex_map_def) + have xx: "simplicial_chain p (standard_simplex p) (?d n) \ + (\f \ Poly_Mapping.keys(?d n). \x \ standard_simplex p. \y \ standard_simplex p. + \f x i - f y i\ \ (p / (Suc p)) ^ n)" + for n i + proof (induction n) + case 0 + have "simplicial_simplex p (standard_simplex p) (\a\standard_simplex p. a)" + by (metis eq_id_iff order_refl simplicial_simplex_id) + moreover have "(\x\standard_simplex p. \y\standard_simplex p. \x i - y i\ \ 1)" + unfolding standard_simplex_def + by (auto simp: abs_if dest!: spec [where x=i]) + ultimately show ?case + unfolding power_0 funpow_0 by simp + next + case (Suc n) + show ?case + unfolding power_Suc funpow.simps o_def + proof (intro conjI ballI) + show "simplicial_chain p (standard_simplex p) (simplicial_subdivision p (?d n))" + by (simp add: Suc simplicial_chain_simplicial_subdivision) + show "\f x i - f y i\ \ real p / real (Suc p) * (real p / real (Suc p)) ^ n" + if "f \ Poly_Mapping.keys (simplicial_subdivision p (?d n))" + and "x \ standard_simplex p" and "y \ standard_simplex p" for f x y + using Suc that by (blast intro: simplicial_subdivision_shrinks) + qed + qed + have "g ` standard_simplex p \ standard_simplex p" + using g xx [of m] unfolding simplicial_chain_def simplicial_simplex by auto + moreover + have "\g x i - g y i\ \ d" if "i \ p" "x \ standard_simplex p" "y \ standard_simplex p" for x y i + proof - + have "\g x i - g y i\ \ (p / (Suc p)) ^ m" + using g xx [of m] that by blast + also have "\ \ (p / (Suc p)) ^ n" + by (auto intro: power_decreasing [OF \n \ m\]) + finally show ?thesis using n by simp + qed + then have "\x i - y i\ \ d" + if "x \ g ` (standard_simplex p)" "y \ g ` (standard_simplex p)" "i \ p" for i x y + using that by blast + ultimately show "\V\\. h ` standard_simplex p \ V" + using \f \ Poly_Mapping.keys c\ d [of f "g ` standard_simplex p"] + by (simp add: Bex_def heq image_image) + qed + qed + qed +qed force + + +lemma small_homologous_rel_relcycle_exists: + assumes \: "\U. U \ \ \ openin X U" + and X: "topspace X \ \\" + and p: "singular_relcycle p X S c" + obtains c' where "singular_relcycle p X S c'" "homologous_rel p X S c c'" + "\f. f \ Poly_Mapping.keys c' \ \V \ \. f ` (standard_simplex p) \ V" +proof - + have "singular_chain p X c" + "(chain_boundary p c, 0) \ (mod_subset (p - Suc 0) (subtopology X S))" + using p unfolding singular_relcycle_def by auto + then obtain n where n: "\m f. \n \ m; f \ Poly_Mapping.keys ((singular_subdivision p ^^ m) c)\ + \ \V \ \. f ` (standard_simplex p) \ V" + by (blast intro: sufficient_iterated_singular_subdivision_exists [OF \ X]) + let ?c' = "(singular_subdivision p ^^ n) c" + show ?thesis + proof + show "homologous_rel p X S c ?c'" + apply (induction n, simp_all) + by (metis p homologous_rel_singular_subdivision homologous_rel_singular_relcycle homologous_rel_trans homologous_rel_sym) + then show "singular_relcycle p X S ?c'" + by (metis homologous_rel_singular_relcycle p) + next + fix f :: "(nat \ real) \ 'a" + assume "f \ Poly_Mapping.keys ?c'" + then show "\V\\. f ` standard_simplex p \ V" + by (rule n [OF order_refl]) + qed +qed + +lemma excised_chain_exists: + fixes S :: "'a set" + assumes "X closure_of U \ X interior_of T" "T \ S" "singular_chain p (subtopology X S) c" + obtains n d e where "singular_chain p (subtopology X (S - U)) d" + "singular_chain p (subtopology X T) e" + "(singular_subdivision p ^^ n) c = d + e" +proof - + have *: "\n d e. singular_chain p (subtopology X (S - U)) d \ + singular_chain p (subtopology X T) e \ + (singular_subdivision p ^^ n) c = d + e" + if c: "singular_chain p (subtopology X S) c" + and X: "X closure_of U \ X interior_of T" "U \ topspace X" and S: "T \ S" "S \ topspace X" + for p X c S and T U :: "'a set" + proof - + obtain n where n: "\m f. \n \ m; f \ Poly_Mapping.keys ((singular_subdivision p ^^ m) c)\ + \ \V \ {S \ X interior_of T, S - X closure_of U}. f ` standard_simplex p \ V" + apply (rule sufficient_iterated_singular_subdivision_exists + [of "{S \ X interior_of T, S - X closure_of U}"]) + using X S c + by (auto simp: topspace_subtopology openin_subtopology_Int2 openin_subtopology_diff_closed) + let ?c' = "\n. (singular_subdivision p ^^ n) c" + have "singular_chain p (subtopology X S) (?c' m)" for m + by (induction m) (auto simp: singular_chain_singular_subdivision c) + then have scp: "singular_chain p (subtopology X S) (?c' n)" . + + have SS: "Poly_Mapping.keys (?c' n) \ singular_simplex_set p (subtopology X (S - U)) + \ singular_simplex_set p (subtopology X T)" + proof (clarsimp) + fix f + assume f: "f \ Poly_Mapping.keys ((singular_subdivision p ^^ n) c)" + and non: "\ singular_simplex p (subtopology X T) f" + show "singular_simplex p (subtopology X (S - U)) f" + using n [OF order_refl f] scp f non closure_of_subset [OF \U \ topspace X\] interior_of_subset [of X T] + by (fastforce simp: image_subset_iff singular_simplex_subtopology singular_chain_def) + qed + show ?thesis + unfolding singular_chain_def using frag_split [OF SS] by metis + qed + have "(subtopology X (topspace X \ S)) = (subtopology X S)" + by (metis subtopology_subtopology subtopology_topspace) + with assms have c: "singular_chain p (subtopology X (topspace X \ S)) c" + by simp + have Xsub: "X closure_of (topspace X \ U) \ X interior_of (topspace X \ T)" + using assms closure_of_restrict interior_of_restrict by fastforce + obtain n d e where + d: "singular_chain p (subtopology X (topspace X \ S - topspace X \ U)) d" + and e: "singular_chain p (subtopology X (topspace X \ T)) e" + and de: "(singular_subdivision p ^^ n) c = d + e" + using *[OF c Xsub, simplified] assms by force + show thesis + proof + show "singular_chain p (subtopology X (S - U)) d" + by (metis d Diff_Int_distrib inf.cobounded2 singular_chain_mono) + show "singular_chain p (subtopology X T) e" + by (metis e inf.cobounded2 singular_chain_mono) + show "(singular_subdivision p ^^ n) c = d + e" + by (rule de) + qed +qed + + +lemma excised_relcycle_exists: + fixes S :: "'a set" + assumes X: "X closure_of U \ X interior_of T" and "T \ S" + and c: "singular_relcycle p (subtopology X S) T c" + obtains c' where "singular_relcycle p (subtopology X (S - U)) (T - U) c'" + "homologous_rel p (subtopology X S) T c c'" +proof - + have [simp]: "(S - U) \ (T - U) = T - U" "S \ T = T" + using \T \ S\ by auto + have scc: "singular_chain p (subtopology X S) c" + and scp1: "singular_chain (p - Suc 0) (subtopology X T) (chain_boundary p c)" + using c by (auto simp: singular_relcycle_def mod_subset_def subtopology_subtopology) + obtain n d e where d: "singular_chain p (subtopology X (S - U)) d" + and e: "singular_chain p (subtopology X T) e" + and de: "(singular_subdivision p ^^ n) c = d + e" + using excised_chain_exists [OF X \T \ S\ scc] . + have scSUd: "singular_chain (p - Suc 0) (subtopology X (S - U)) (chain_boundary p d)" + by (simp add: singular_chain_boundary d) + have sccn: "singular_chain p (subtopology X S) ((singular_subdivision p ^^ n) c)" for n + by (induction n) (auto simp: singular_chain_singular_subdivision scc) + have "singular_chain (p - Suc 0) (subtopology X T) (chain_boundary p ((singular_subdivision p ^^ n) c))" + proof (induction n) + case (Suc n) + then show ?case + by (simp add: singular_chain_singular_subdivision chain_boundary_singular_subdivision [OF sccn]) + qed (auto simp: scp1) + then have "singular_chain (p - Suc 0) (subtopology X T) (chain_boundary p ((singular_subdivision p ^^ n) c - e))" + by (simp add: chain_boundary_diff singular_chain_diff singular_chain_boundary e) + with de have scTd: "singular_chain (p - Suc 0) (subtopology X T) (chain_boundary p d)" + by simp + show thesis + proof + have "singular_chain (p - Suc 0) X (chain_boundary p d)" + using scTd singular_chain_subtopology by blast + with scSUd scTd have "singular_chain (p - Suc 0) (subtopology X (T - U)) (chain_boundary p d)" + by (fastforce simp add: singular_chain_subtopology) + then show "singular_relcycle p (subtopology X (S - U)) (T - U) d" + by (auto simp: singular_relcycle_def mod_subset_def subtopology_subtopology d) + have "homologous_rel p (subtopology X S) T (c-0) ((singular_subdivision p ^^ n) c - e)" + proof (rule homologous_rel_diff) + show "homologous_rel p (subtopology X S) T c ((singular_subdivision p ^^ n) c)" + proof (induction n) + case (Suc n) + then show ?case + apply simp + apply (rule homologous_rel_trans) + using c homologous_rel_singular_relcycle_1 homologous_rel_singular_subdivision homologous_rel_sym by blast + qed auto + show "homologous_rel p (subtopology X S) T 0 e" + unfolding homologous_rel_def using e + by (intro singular_relboundary_diff singular_chain_imp_relboundary; simp add: subtopology_subtopology) + qed + with de show "homologous_rel p (subtopology X S) T c d" + by simp + qed +qed + +end + diff -r 23c0dfa39dce -r 10fe23659be3 src/HOL/Homology/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Homology/document/root.tex Tue Apr 09 15:31:14 2019 +0100 @@ -0,0 +1,42 @@ +\documentclass[11pt,a4paper]{book} +\usepackage{graphicx} +\usepackage{isabelle} +\usepackage{isabellesym} +\usepackage{latexsym} +\usepackage{textcomp} +\usepackage{amsmath} +\usepackage{amssymb} +\usepackage[only,bigsqcap]{stmaryrd} +\usepackage{pdfsetup} + +\usepackage{tocloft} +\setlength{\cftsubsecnumwidth}{3em} +\cftsetpnumwidth{2em} +\cftsetrmarg{3em} + +\urlstyle{rm} +\isabellestyle{literalunderscore} +\pagestyle{myheadings} + +\begin{document} + +\title{Homology} +\maketitle + +\tableofcontents + +\begin{center} + \includegraphics[height=\textheight]{session_graph} +\end{center} + +\newpage + +\renewcommand{\setisabellecontext}[1]{\markright{\href{#1.html}{#1.thy}}} + +\parindent 0pt\parskip 0.5ex +\input{session} + +\pagestyle{headings} +\bibliographystyle{abbrv} + +\end{document} diff -r 23c0dfa39dce -r 10fe23659be3 src/HOL/ROOT --- a/src/HOL/ROOT Tue Apr 09 14:17:29 2019 +0200 +++ b/src/HOL/ROOT Tue Apr 09 15:31:14 2019 +0100 @@ -74,6 +74,16 @@ theories Approximations +session "HOL-Homology" (main timing) in Homology = "HOL-Analysis" + + options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", + document_variants = "document:manual=-proof,-ML,-unimportant"] + sessions + "HOL-Algebra" + theories + Homology + document_files + "root.tex" + session "HOL-Computational_Algebra" (main timing) in "Computational_Algebra" = "HOL-Library" + theories Computational_Algebra