merged
authorpaulson
Tue Apr 09 12:36:53 2019 +0100 (5 months ago)
changeset 70088187ae5cb2f03
parent 70084 f9d8f78ef687
parent 70087 2d19e7eb027a
child 70089 eca8611201e9
merged
NEWS
     1.1 --- a/NEWS	Tue Apr 09 11:24:47 2019 +0200
     1.2 +++ b/NEWS	Tue Apr 09 12:36:53 2019 +0100
     1.3 @@ -233,7 +233,10 @@
     1.4  * Session HOL-Number_Theory: More material on residue rings in
     1.5  Carmichael's function, primitive roots, more properties for "ord".
     1.6  
     1.7 -* Session HOL-Analysis: More material and better organization.
     1.8 +* Session HOL-Analysis: Better organization and much more material,
     1.9 +including algebraic topology.
    1.10 +
    1.11 +* Session HOL-Algebra: Much more material on group theory.
    1.12  
    1.13  * Session HOL-SPARK: .prv files are no longer written to the
    1.14  file-system, but exported to the session database. Results may be
     2.1 --- a/src/HOL/Analysis/Abstract_Euclidean_Space.thy	Tue Apr 09 11:24:47 2019 +0200
     2.2 +++ b/src/HOL/Analysis/Abstract_Euclidean_Space.thy	Tue Apr 09 12:36:53 2019 +0100
     2.3 @@ -89,6 +89,51 @@
     2.4    unfolding Euclidean_space_def continuous_map_in_subtopology
     2.5    by (fastforce simp add: continuous_map_componentwise_UNIV continuous_map_diff)
     2.6  
     2.7 +lemma continuous_map_Euclidean_space_iff:
     2.8 +  "continuous_map (Euclidean_space m) euclideanreal g
     2.9 +   = continuous_on (topspace (Euclidean_space m)) g"
    2.10 +proof
    2.11 +  assume "continuous_map (Euclidean_space m) euclideanreal g"
    2.12 +  then have "continuous_map (top_of_set {f. \<forall>n\<ge>m. f n = 0}) euclideanreal g"
    2.13 +    by (simp add: Euclidean_space_def euclidean_product_topology)
    2.14 +  then show "continuous_on (topspace (Euclidean_space m)) g"
    2.15 +    by (metis continuous_map_subtopology_eu subtopology_topspace topspace_Euclidean_space)
    2.16 +next
    2.17 +  assume "continuous_on (topspace (Euclidean_space m)) g"
    2.18 +  then have "continuous_map (top_of_set {f. \<forall>n\<ge>m. f n = 0}) euclideanreal g"
    2.19 +    by (metis (lifting) continuous_map_into_fulltopology continuous_map_subtopology_eu order_refl topspace_Euclidean_space)
    2.20 +  then show "continuous_map (Euclidean_space m) euclideanreal g"
    2.21 +    by (simp add: Euclidean_space_def euclidean_product_topology)
    2.22 +qed
    2.23 +
    2.24 +lemma cm_Euclidean_space_iff_continuous_on:
    2.25 +  "continuous_map (subtopology (Euclidean_space m) S) (Euclidean_space n) f
    2.26 +   \<longleftrightarrow> continuous_on (topspace (subtopology (Euclidean_space m) S)) f \<and>
    2.27 +       f ` (topspace (subtopology (Euclidean_space m) S)) \<subseteq> topspace (Euclidean_space n)"
    2.28 +  (is "?P \<longleftrightarrow> ?Q \<and> ?R")
    2.29 +proof -
    2.30 +  have ?Q if ?P
    2.31 +  proof -
    2.32 +    have "\<And>n. Euclidean_space n = top_of_set {f. \<forall>m\<ge>n. f m = 0}"
    2.33 +      by (simp add: Euclidean_space_def euclidean_product_topology)
    2.34 +    with that show ?thesis
    2.35 +      by (simp add: subtopology_subtopology)
    2.36 +  qed
    2.37 +  moreover
    2.38 +  have ?R if ?P
    2.39 +    using that by (simp add: image_subset_iff continuous_map_def)
    2.40 +  moreover
    2.41 +  have ?P if ?Q ?R
    2.42 +  proof -
    2.43 +    have "continuous_map (top_of_set (topspace (subtopology (subtopology (powertop_real UNIV) {f. \<forall>n\<ge>m. f n = 0}) S))) (top_of_set (topspace (subtopology (powertop_real UNIV) {f. \<forall>na\<ge>n. f na = 0}))) f"
    2.44 +      using Euclidean_space_def that by auto
    2.45 +    then show ?thesis
    2.46 +      by (simp add: Euclidean_space_def euclidean_product_topology subtopology_subtopology)
    2.47 +  qed
    2.48 +  ultimately show ?thesis
    2.49 +    by auto
    2.50 +qed
    2.51 +
    2.52  lemma homeomorphic_Euclidean_space_product_topology:
    2.53    "Euclidean_space n homeomorphic_space product_topology (\<lambda>i. euclideanreal) {..<n}"
    2.54  proof -
    2.55 @@ -125,6 +170,7 @@
    2.56     "compact_space (Euclidean_space n) \<longleftrightarrow> n = 0"
    2.57    by (auto simp: homeomorphic_compact_space [OF homeomorphic_Euclidean_space_product_topology] compact_space_product_topology)
    2.58  
    2.59 +
    2.60  subsection\<open>n-dimensional spheres\<close>
    2.61  
    2.62  definition nsphere where
     3.1 --- a/src/HOL/Analysis/Abstract_Topology.thy	Tue Apr 09 11:24:47 2019 +0200
     3.2 +++ b/src/HOL/Analysis/Abstract_Topology.thy	Tue Apr 09 12:36:53 2019 +0100
     3.3 @@ -2728,7 +2728,7 @@
     3.4     "X homeomorphic_space Y \<longleftrightarrow> Y homeomorphic_space X"
     3.5    unfolding homeomorphic_space_def by (metis homeomorphic_maps_sym)
     3.6  
     3.7 -lemma homeomorphic_space_trans:
     3.8 +lemma homeomorphic_space_trans [trans]:
     3.9       "\<lbrakk>X1 homeomorphic_space X2; X2 homeomorphic_space X3\<rbrakk> \<Longrightarrow> X1 homeomorphic_space X3"
    3.10    unfolding homeomorphic_space_def by (metis homeomorphic_maps_compose)
    3.11  
     4.1 --- a/src/HOL/Analysis/Analysis.thy	Tue Apr 09 11:24:47 2019 +0200
     4.2 +++ b/src/HOL/Analysis/Analysis.thy	Tue Apr 09 12:36:53 2019 +0100
     4.3 @@ -7,6 +7,8 @@
     4.4    Connected
     4.5    Abstract_Limits
     4.6    Abstract_Euclidean_Space
     4.7 +  (*Homology*)
     4.8 +  Simplices
     4.9    (* Functional Analysis *)
    4.10    Elementary_Normed_Spaces
    4.11    Norm_Arith
     5.1 --- a/src/HOL/Analysis/Convex.thy	Tue Apr 09 11:24:47 2019 +0200
     5.2 +++ b/src/HOL/Analysis/Convex.thy	Tue Apr 09 12:36:53 2019 +0100
     5.3 @@ -1,4 +1,4 @@
     5.4 -(* Title:      HOL/Analysis/Convex_Euclidean_Space.thy
     5.5 +(* Title:      HOL/Analysis/Convex.thy
     5.6     Author:     L C Paulson, University of Cambridge
     5.7     Author:     Robert Himmelmann, TU Muenchen
     5.8     Author:     Bogdan Grechuk, University of Edinburgh
     6.1 --- a/src/HOL/Analysis/Function_Topology.thy	Tue Apr 09 11:24:47 2019 +0200
     6.2 +++ b/src/HOL/Analysis/Function_Topology.thy	Tue Apr 09 12:36:53 2019 +0100
     6.3 @@ -642,6 +642,17 @@
     6.4    shows "continuous_on (A \<inter> S) f \<longleftrightarrow> (\<forall>i. continuous_on (A \<inter> S) (\<lambda>x. f x i))"
     6.5    by (auto simp: continuous_on_product_then_coordinatewise continuous_on_coordinatewise_then_product)
     6.6  
     6.7 +lemma continuous_map_span_sum:
     6.8 +  fixes B :: "'a::real_inner set"
     6.9 +  assumes biB: "\<And>i. i \<in> I \<Longrightarrow> b i \<in> B"
    6.10 +  shows "continuous_map euclidean (top_of_set (span B)) (\<lambda>x. \<Sum>i\<in>I. x i *\<^sub>R b i)"
    6.11 +proof (rule continuous_map_euclidean_top_of_set)
    6.12 +  show "(\<lambda>x. \<Sum>i\<in>I. x i *\<^sub>R b i) -` span B = UNIV"
    6.13 +    by auto (meson biB lessThan_iff span_base span_scale span_sum)
    6.14 +  show "continuous_on UNIV (\<lambda>x. \<Sum>i\<in> I. x i *\<^sub>R b i)"
    6.15 +    by (intro continuous_intros) auto
    6.16 +qed
    6.17 +
    6.18  subsubsection%important \<open>Topological countability for product spaces\<close>
    6.19  
    6.20  text \<open>The next two lemmas are useful to prove first or second countability
    6.21 @@ -867,7 +878,6 @@
    6.22    apply standard
    6.23    using product_topology_countable_basis topological_basis_imp_subbasis by auto
    6.24  
    6.25 -
    6.26  subsection \<open>Metrics on product spaces\<close>
    6.27  
    6.28  
    6.29 @@ -1242,7 +1252,7 @@
    6.30  qed
    6.31  
    6.32  instance "fun" :: (countable, polish_space) polish_space
    6.33 -by standard
    6.34 +  by standard
    6.35  
    6.36  
    6.37  subsection\<open>The Alexander subbase theorem\<close>
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Analysis/Simplices.thy	Tue Apr 09 12:36:53 2019 +0100
     7.3 @@ -0,0 +1,2785 @@
     7.4 +section\<open>Homology, I: Simplices\<close>
     7.5 +
     7.6 +theory "Simplices"
     7.7 +  imports "Abstract_Euclidean_Space" "HOL-Algebra.Free_Abelian_Groups"
     7.8 +
     7.9 +begin
    7.10 +subsection\<open>Standard simplices, all of which are topological subspaces of @{text"R^n"}.      \<close>
    7.11 +
    7.12 +type_synonym 'a chain = "((nat \<Rightarrow> real) \<Rightarrow> 'a) \<Rightarrow>\<^sub>0 int"
    7.13 +
    7.14 +definition standard_simplex :: "nat \<Rightarrow> (nat \<Rightarrow> real) set" where
    7.15 +  "standard_simplex p \<equiv>
    7.16 +    {x. (\<forall>i. 0 \<le> x i \<and> x i \<le> 1) \<and> (\<forall>i>p. x i = 0) \<and> (\<Sum>i\<le>p. x i) = 1}"
    7.17 +
    7.18 +lemma topspace_standard_simplex:
    7.19 +  "topspace(subtopology (powertop_real UNIV) (standard_simplex p))
    7.20 +    = standard_simplex p"
    7.21 +  by simp
    7.22 +
    7.23 +lemma basis_in_standard_simplex [simp]:
    7.24 +   "(\<lambda>j. if j = i then 1 else 0) \<in> standard_simplex p \<longleftrightarrow> i \<le> p"
    7.25 +  by (auto simp: standard_simplex_def)
    7.26 +
    7.27 +lemma nonempty_standard_simplex: "standard_simplex p \<noteq> {}"
    7.28 +  using basis_in_standard_simplex by blast
    7.29 +
    7.30 +lemma standard_simplex_0: "standard_simplex 0 = {(\<lambda>j. if j = 0 then 1 else 0)}"
    7.31 +  by (auto simp: standard_simplex_def)
    7.32 +
    7.33 +lemma standard_simplex_mono:
    7.34 +  assumes "p \<le> q"
    7.35 +  shows "standard_simplex p \<subseteq> standard_simplex q"
    7.36 +  using assms
    7.37 +proof (clarsimp simp: standard_simplex_def)
    7.38 +  fix x :: "nat \<Rightarrow> real"
    7.39 +  assume "\<forall>i. 0 \<le> x i \<and> x i \<le> 1" and "\<forall>i>p. x i = 0" and "sum x {..p} = 1"
    7.40 +  then show "sum x {..q} = 1"
    7.41 +    using sum.mono_neutral_left [of "{..q}" "{..p}" x] assms by auto
    7.42 +qed
    7.43 +
    7.44 +lemma closedin_standard_simplex:
    7.45 +   "closedin (powertop_real UNIV) (standard_simplex p)"
    7.46 +    (is "closedin ?X ?S")
    7.47 +proof -
    7.48 +  have eq: "standard_simplex p =
    7.49 +              (\<Inter>i. {x. x \<in> topspace ?X \<and> x i \<in> {0..1}}) \<inter>
    7.50 +              (\<Inter>i \<in> {p<..}. {x \<in> topspace ?X. x i \<in> {0}}) \<inter>
    7.51 +              {x \<in> topspace ?X. (\<Sum>i\<le>p. x i) \<in> {1}}"
    7.52 +    by (auto simp: standard_simplex_def topspace_product_topology)
    7.53 +  show ?thesis
    7.54 +    unfolding eq
    7.55 +    by (rule closedin_Int closedin_Inter continuous_map_sum
    7.56 +             continuous_map_product_projection closedin_continuous_map_preimage | force | clarify)+
    7.57 +qed
    7.58 +
    7.59 +lemma standard_simplex_01: "standard_simplex p \<subseteq> UNIV \<rightarrow>\<^sub>E {0..1}"
    7.60 +  using standard_simplex_def by auto
    7.61 +
    7.62 +lemma compactin_standard_simplex:
    7.63 +   "compactin (powertop_real UNIV) (standard_simplex p)"
    7.64 +  apply (rule closed_compactin [where K = "PiE UNIV (\<lambda>i. {0..1})"])
    7.65 +    apply (simp_all add: compactin_PiE standard_simplex_01 closedin_standard_simplex)
    7.66 +  done
    7.67 +
    7.68 +lemma convex_standard_simplex:
    7.69 +   "\<lbrakk>x \<in> standard_simplex p; y \<in> standard_simplex p;
    7.70 +     0 \<le> u; u \<le> 1\<rbrakk>
    7.71 +    \<Longrightarrow> (\<lambda>i. (1 - u) * x i + u * y i) \<in> standard_simplex p"
    7.72 +  by (simp add: standard_simplex_def sum.distrib convex_bound_le flip: sum_distrib_left)
    7.73 +
    7.74 +lemma path_connectedin_standard_simplex:
    7.75 +   "path_connectedin (powertop_real UNIV) (standard_simplex p)"
    7.76 +proof -
    7.77 +  define g where "g \<equiv> \<lambda>x y::nat\<Rightarrow>real. \<lambda>u i. (1 - u) * x i + u * y i"
    7.78 +  have 1: "continuous_map
    7.79 +                (subtopology euclideanreal {0..1}) (powertop_real UNIV)
    7.80 +                (g x y)"
    7.81 +    if "x \<in> standard_simplex p" "y \<in> standard_simplex p" for x y
    7.82 +    unfolding g_def continuous_map_componentwise
    7.83 +    by (force intro: continuous_intros)
    7.84 +  have 2: "g x y ` {0..1} \<subseteq> standard_simplex p" "g x y 0 = x" "g x y 1 = y"
    7.85 +    if "x \<in> standard_simplex p" "y \<in> standard_simplex p" for x y
    7.86 +    using that by (auto simp: convex_standard_simplex g_def)
    7.87 +  show ?thesis
    7.88 +    unfolding path_connectedin_def path_connected_space_def pathin_def
    7.89 +    apply (simp add: topspace_standard_simplex topspace_product_topology continuous_map_in_subtopology)
    7.90 +    by (metis 1 2)
    7.91 +qed
    7.92 +
    7.93 +lemma connectedin_standard_simplex:
    7.94 +   "connectedin (powertop_real UNIV) (standard_simplex p)"
    7.95 +  by (simp add: path_connectedin_imp_connectedin path_connectedin_standard_simplex)
    7.96 +
    7.97 +subsection\<open>Face map\<close>
    7.98 +
    7.99 +definition simplical_face :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a::comm_monoid_add" where
   7.100 +   "simplical_face k x \<equiv> \<lambda>i. if i < k then x i else if i = k then 0 else x(i -1)"
   7.101 +
   7.102 +lemma simplical_face_in_standard_simplex:
   7.103 +  assumes "1 \<le> p" "k \<le> p" "x \<in> standard_simplex (p - Suc 0)"
   7.104 +  shows "(simplical_face k x) \<in> standard_simplex p"
   7.105 +proof -
   7.106 +  have x01: "\<And>i. 0 \<le> x i \<and> x i \<le> 1" and sumx: "sum x {..p - Suc 0} = 1"
   7.107 +    using assms by (auto simp: standard_simplex_def simplical_face_def)
   7.108 +  have gg: "\<And>g. sum g {..p} = sum g {..<k} + sum g {k..p}"
   7.109 +    using \<open>k \<le> p\<close> sum.union_disjoint [of "{..<k}" "{k..p}"]
   7.110 +    by (force simp: ivl_disj_un ivl_disj_int)
   7.111 +  have eq: "(\<Sum>i\<le>p. if i < k then x i else if i = k then 0 else x (i -1))
   7.112 +         = (\<Sum>i < k. x i) + (\<Sum>i \<in> {k..p}. if i = k then 0 else x (i -1))"
   7.113 +    by (simp add: gg)
   7.114 +  consider "k \<le> p - Suc 0" | "k = p"
   7.115 +    using \<open>k \<le> p\<close> by linarith
   7.116 +  then have "(\<Sum>i\<le>p. if i < k then x i else if i = k then 0 else x (i -1)) = 1"
   7.117 +  proof cases
   7.118 +    case 1
   7.119 +    have [simp]: "Suc (p - Suc 0) = p"
   7.120 +      using \<open>1 \<le> p\<close> by auto
   7.121 +    have "(\<Sum>i = k..p. if i = k then 0 else x (i -1)) = (\<Sum>i = k+1..p. if i = k then 0 else x (i -1))"
   7.122 +      by (rule sum.mono_neutral_right) auto
   7.123 +    also have "\<dots> = (\<Sum>i = k+1..p. x (i -1))"
   7.124 +      by simp
   7.125 +    also have "\<dots> = (\<Sum>i = k..p-1. x i)"
   7.126 +      using sum.atLeastAtMost_reindex [of Suc k "p-1" "\<lambda>i. x (i - Suc 0)"] 1 by simp
   7.127 +    finally have eq2: "(\<Sum>i = k..p. if i = k then 0 else x (i -1)) = (\<Sum>i = k..p-1. x i)" .
   7.128 +    with 1 show ?thesis
   7.129 +      apply (simp add: eq eq2)
   7.130 +      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)
   7.131 +  next
   7.132 +    case 2
   7.133 +    have [simp]: "({..p} \<inter> {x. x < p}) = {..p - Suc 0}"
   7.134 +      using assms by auto
   7.135 +    have "(\<Sum>i\<le>p. if i < p then x i else if i = k then 0 else x (i -1)) = (\<Sum>i\<le>p. if i < p then x i else 0)"
   7.136 +      by (rule sum.cong) (auto simp: 2)
   7.137 +    also have "\<dots> = sum x {..p-1}"
   7.138 +      by (simp add: sum.If_cases)
   7.139 +    also have "\<dots> = 1"
   7.140 +      by (simp add: sumx)
   7.141 +    finally show ?thesis
   7.142 +      using 2 by simp
   7.143 +  qed
   7.144 +  then show ?thesis
   7.145 +    using assms by (auto simp: standard_simplex_def simplical_face_def)
   7.146 +qed
   7.147 +
   7.148 +subsection\<open>Singular simplices, forcing canonicity outside the intended domain\<close>
   7.149 +
   7.150 +definition singular_simplex :: "nat \<Rightarrow> 'a topology \<Rightarrow> ((nat \<Rightarrow> real) \<Rightarrow> 'a) \<Rightarrow> bool" where
   7.151 + "singular_simplex p X f \<equiv>
   7.152 +      continuous_map(subtopology (powertop_real UNIV) (standard_simplex p)) X f
   7.153 +    \<and> f \<in> extensional (standard_simplex p)"
   7.154 +
   7.155 +abbreviation singular_simplex_set :: "nat \<Rightarrow> 'a topology \<Rightarrow> ((nat \<Rightarrow> real) \<Rightarrow> 'a) set" where
   7.156 + "singular_simplex_set p X \<equiv> Collect (singular_simplex p X)"
   7.157 +
   7.158 +lemma singular_simplex_empty:
   7.159 +   "topspace X = {} \<Longrightarrow> \<not> singular_simplex p X f"
   7.160 +  by (simp add: singular_simplex_def continuous_map nonempty_standard_simplex)
   7.161 +
   7.162 +lemma singular_simplex_mono:
   7.163 +   "\<lbrakk>singular_simplex p (subtopology X T) f; T \<subseteq> S\<rbrakk> \<Longrightarrow> singular_simplex p (subtopology X S) f"
   7.164 +  by (auto simp: singular_simplex_def continuous_map_in_subtopology)
   7.165 +
   7.166 +lemma singular_simplex_subtopology:
   7.167 +   "singular_simplex p (subtopology X S) f \<longleftrightarrow>
   7.168 +        singular_simplex p X f \<and> f ` (standard_simplex p) \<subseteq> S"
   7.169 +  by (auto simp: singular_simplex_def continuous_map_in_subtopology)
   7.170 +
   7.171 +subsubsection\<open>Singular face\<close>
   7.172 +
   7.173 +definition singular_face :: "nat \<Rightarrow> nat \<Rightarrow> ((nat \<Rightarrow> real) \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> 'a"
   7.174 +  where "singular_face p k f \<equiv> restrict (f \<circ> simplical_face k) (standard_simplex (p - Suc 0))"
   7.175 +
   7.176 +lemma singular_simplex_singular_face:
   7.177 +  assumes f: "singular_simplex p X f" and "1 \<le> p" "k \<le> p"
   7.178 +  shows "singular_simplex (p - Suc 0) X (singular_face p k f)"
   7.179 +proof -
   7.180 +  let ?PT = "(powertop_real UNIV)"
   7.181 +  have 0: "simplical_face k ` standard_simplex (p - Suc 0) \<subseteq> standard_simplex p"
   7.182 +    using assms simplical_face_in_standard_simplex by auto
   7.183 +  have 1: "continuous_map (subtopology ?PT (standard_simplex (p - Suc 0)))
   7.184 +                          (subtopology ?PT (standard_simplex p))
   7.185 +                          (simplical_face k)"
   7.186 +  proof (clarsimp simp add: continuous_map_in_subtopology simplical_face_in_standard_simplex continuous_map_componentwise 0)
   7.187 +    fix i
   7.188 +    have "continuous_map ?PT euclideanreal (\<lambda>x. if i < k then x i else if i = k then 0 else x (i -1))"
   7.189 +      by (auto intro: continuous_map_product_projection)
   7.190 +    then show "continuous_map (subtopology ?PT (standard_simplex (p - Suc 0))) euclideanreal
   7.191 +                              (\<lambda>x. simplical_face k x i)"
   7.192 +      by (simp add: simplical_face_def continuous_map_from_subtopology)
   7.193 +  qed
   7.194 +  have 2: "continuous_map (subtopology ?PT (standard_simplex p)) X f"
   7.195 +    using assms(1) singular_simplex_def by blast
   7.196 +  show ?thesis
   7.197 +    by (simp add: singular_simplex_def singular_face_def continuous_map_compose [OF 1 2])
   7.198 +qed
   7.199 +
   7.200 +
   7.201 +subsection\<open>Singular chains\<close>
   7.202 +
   7.203 +definition singular_chain :: "[nat, 'a topology, 'a chain] \<Rightarrow> bool"
   7.204 +  where "singular_chain p X c \<equiv> Poly_Mapping.keys c \<subseteq> singular_simplex_set p X"
   7.205 +
   7.206 +abbreviation singular_chain_set :: "[nat, 'a topology] \<Rightarrow> ('a chain) set"
   7.207 +  where "singular_chain_set p X \<equiv> Collect (singular_chain p X)"
   7.208 +
   7.209 +lemma singular_chain_empty:
   7.210 +   "topspace X = {} \<Longrightarrow> singular_chain p X c \<longleftrightarrow> c = 0"
   7.211 +  by (auto simp: singular_chain_def singular_simplex_empty subset_eq poly_mapping_eqI)
   7.212 +
   7.213 +lemma singular_chain_mono:
   7.214 +   "\<lbrakk>singular_chain p (subtopology X T) c;  T \<subseteq> S\<rbrakk>
   7.215 +        \<Longrightarrow> singular_chain p (subtopology X S) c"
   7.216 +  unfolding singular_chain_def using singular_simplex_mono by blast
   7.217 +
   7.218 +lemma singular_chain_subtopology:
   7.219 +   "singular_chain p (subtopology X S) c \<longleftrightarrow>
   7.220 +        singular_chain p X c \<and> (\<forall>f \<in> Poly_Mapping.keys c. f ` (standard_simplex p) \<subseteq> S)"
   7.221 +  unfolding singular_chain_def
   7.222 +  by (fastforce simp add: singular_simplex_subtopology subset_eq)
   7.223 +
   7.224 +lemma singular_chain_0 [iff]: "singular_chain p X 0"
   7.225 +  by (auto simp: singular_chain_def)
   7.226 +
   7.227 +lemma singular_chain_of:
   7.228 +   "singular_chain p X (frag_of c) \<longleftrightarrow> singular_simplex p X c"
   7.229 +  by (auto simp: singular_chain_def)
   7.230 +
   7.231 +lemma singular_chain_cmul:
   7.232 +   "singular_chain p X c \<Longrightarrow> singular_chain p X (frag_cmul a c)"
   7.233 +  by (auto simp: singular_chain_def)
   7.234 +
   7.235 +lemma singular_chain_minus:
   7.236 +   "singular_chain p X (-c) \<longleftrightarrow> singular_chain p X c"
   7.237 +  by (auto simp: singular_chain_def)
   7.238 +
   7.239 +lemma singular_chain_add:
   7.240 +   "\<lbrakk>singular_chain p X a; singular_chain p X b\<rbrakk> \<Longrightarrow> singular_chain p X (a+b)"
   7.241 +  unfolding singular_chain_def
   7.242 +  using keys_add [of a b] by blast
   7.243 +
   7.244 +lemma singular_chain_diff:
   7.245 +   "\<lbrakk>singular_chain p X a; singular_chain p X b\<rbrakk> \<Longrightarrow> singular_chain p X (a-b)"
   7.246 +  unfolding singular_chain_def
   7.247 +  using keys_diff [of a b] by blast
   7.248 +
   7.249 +lemma singular_chain_sum:
   7.250 +   "(\<And>i. i \<in> I \<Longrightarrow> singular_chain p X (f i)) \<Longrightarrow> singular_chain p X (\<Sum>i\<in>I. f i)"
   7.251 +  unfolding singular_chain_def
   7.252 +  using keys_sum [of f I] by blast
   7.253 +
   7.254 +lemma singular_chain_extend:
   7.255 +   "(\<And>c. c \<in> Poly_Mapping.keys x \<Longrightarrow> singular_chain p X (f c))
   7.256 +        \<Longrightarrow> singular_chain p X (frag_extend f x)"
   7.257 +  by (simp add: frag_extend_def singular_chain_cmul singular_chain_sum)
   7.258 +
   7.259 +subsection\<open>Boundary homomorphism for singular chains\<close>
   7.260 +
   7.261 +definition chain_boundary :: "nat \<Rightarrow> ('a chain) \<Rightarrow> 'a chain"
   7.262 +  where "chain_boundary p c \<equiv>
   7.263 +          (if p = 0 then 0 else
   7.264 +           frag_extend (\<lambda>f. (\<Sum>k\<le>p. frag_cmul ((-1) ^ k) (frag_of(singular_face p k f)))) c)"
   7.265 +
   7.266 +lemma singular_chain_boundary:
   7.267 +  "singular_chain p X c
   7.268 +        \<Longrightarrow> singular_chain (p - Suc 0) X (chain_boundary p c)"
   7.269 +  unfolding chain_boundary_def
   7.270 +  apply (clarsimp intro!: singular_chain_extend singular_chain_sum singular_chain_cmul)
   7.271 +  apply (auto simp: singular_chain_def intro: singular_simplex_singular_face)
   7.272 +  done
   7.273 +
   7.274 +lemma singular_chain_boundary_alt:
   7.275 +   "singular_chain (Suc p) X c \<Longrightarrow> singular_chain p X (chain_boundary (Suc p) c)"
   7.276 +  using singular_chain_boundary by force
   7.277 +
   7.278 +lemma chain_boundary_0 [simp]: "chain_boundary p 0 = 0"
   7.279 +  by (simp add: chain_boundary_def)
   7.280 +
   7.281 +lemma chain_boundary_cmul:
   7.282 +   "chain_boundary p (frag_cmul k c) = frag_cmul k (chain_boundary p c)"
   7.283 +  by (auto simp: chain_boundary_def frag_extend_cmul)
   7.284 +
   7.285 +lemma chain_boundary_minus:
   7.286 +   "chain_boundary p (- c) = - (chain_boundary p c)"
   7.287 +  by (metis chain_boundary_cmul frag_cmul_minus_one)
   7.288 +
   7.289 +lemma chain_boundary_add:
   7.290 +   "chain_boundary p (a+b) = chain_boundary p a + chain_boundary p b"
   7.291 +  by (simp add: chain_boundary_def frag_extend_add)
   7.292 +
   7.293 +lemma chain_boundary_diff:
   7.294 +   "chain_boundary p (a-b) = chain_boundary p a - chain_boundary p b"
   7.295 +  using chain_boundary_add [of p a "-b"]
   7.296 +  by (simp add: chain_boundary_minus)
   7.297 +
   7.298 +lemma chain_boundary_sum:
   7.299 +   "chain_boundary p (sum g I) = sum (chain_boundary p \<circ> g) I"
   7.300 +  by (induction I rule: infinite_finite_induct) (simp_all add: chain_boundary_add)
   7.301 +
   7.302 +lemma chain_boundary_sum':
   7.303 +   "finite I \<Longrightarrow> chain_boundary p (sum' g I) = sum' (chain_boundary p \<circ> g) I"
   7.304 +  by (induction I rule: finite_induct) (simp_all add: chain_boundary_add)
   7.305 +
   7.306 +lemma chain_boundary_of:
   7.307 +   "chain_boundary p (frag_of f) =
   7.308 +        (if p = 0 then 0
   7.309 +         else (\<Sum>k\<le>p. frag_cmul ((-1) ^ k) (frag_of(singular_face p k f))))"
   7.310 +  by (simp add: chain_boundary_def)
   7.311 +
   7.312 +subsection\<open>Factoring out chains in a subtopology for relative homology\<close>
   7.313 +
   7.314 +definition mod_subset
   7.315 +  where "mod_subset p X \<equiv> {(a,b). singular_chain p X (a - b)}"
   7.316 +
   7.317 +lemma mod_subset_empty [simp]:
   7.318 +   "(a,b) \<in> (mod_subset p (subtopology X {})) \<longleftrightarrow> a = b"
   7.319 +  by (simp add: mod_subset_def singular_chain_empty topspace_subtopology)
   7.320 +
   7.321 +lemma mod_subset_refl [simp]: "(c,c) \<in> mod_subset p X"
   7.322 +  by (auto simp: mod_subset_def)
   7.323 +
   7.324 +lemma mod_subset_cmul:
   7.325 +  "(a,b) \<in> (mod_subset p X) \<Longrightarrow> (frag_cmul k a, frag_cmul k b) \<in> (mod_subset p X)"
   7.326 +  apply (simp add: mod_subset_def)
   7.327 +  by (metis add_diff_cancel diff_add_cancel frag_cmul_distrib2 singular_chain_cmul)
   7.328 +
   7.329 +lemma mod_subset_add:
   7.330 +   "\<lbrakk>(c1,c2) \<in> (mod_subset p X); (d1,d2) \<in> (mod_subset p X)\<rbrakk>
   7.331 +    \<Longrightarrow> (c1+d1, c2+d2) \<in> (mod_subset p X)"
   7.332 +  apply (simp add: mod_subset_def)
   7.333 +  by (simp add: add_diff_add singular_chain_add)
   7.334 +
   7.335 +subsection\<open>Relative cycles $Z_pX (S)$ where $X$ is a topology and $S$ a subset \<close>
   7.336 +
   7.337 +definition singular_relcycle :: "nat \<Rightarrow> 'a topology \<Rightarrow> 'a set \<Rightarrow> ('a chain) \<Rightarrow> bool"
   7.338 +  where "singular_relcycle p X S \<equiv>
   7.339 +        \<lambda>c. singular_chain p X c \<and> (chain_boundary p c, 0) \<in> mod_subset (p-1) (subtopology X S)"
   7.340 +
   7.341 +abbreviation singular_relcycle_set
   7.342 +  where "singular_relcycle_set p X S \<equiv> Collect (singular_relcycle p X S)"
   7.343 +
   7.344 +lemma singular_relcycle_restrict [simp]:
   7.345 +   "singular_relcycle p X (topspace X \<inter> S) = singular_relcycle p X S"
   7.346 +proof -
   7.347 +  have eq: "subtopology X (topspace X \<inter> S) = subtopology X S"
   7.348 +    by (metis subtopology_subtopology subtopology_topspace)
   7.349 +  show ?thesis
   7.350 +    by (force simp: singular_relcycle_def eq)
   7.351 +qed
   7.352 +
   7.353 +lemma singular_relcycle:
   7.354 +   "singular_relcycle p X S c \<longleftrightarrow>
   7.355 +    singular_chain p X c \<and> singular_chain (p-1) (subtopology X S) (chain_boundary p c)"
   7.356 +  by (simp add: singular_relcycle_def mod_subset_def)
   7.357 +
   7.358 +lemma singular_relcycle_0 [simp]: "singular_relcycle p X S 0"
   7.359 +  by (auto simp: singular_relcycle_def)
   7.360 +
   7.361 +lemma singular_relcycle_cmul:
   7.362 +   "singular_relcycle p X S c \<Longrightarrow> singular_relcycle p X S (frag_cmul k c)"
   7.363 +  by (auto simp: singular_relcycle_def chain_boundary_cmul dest: singular_chain_cmul mod_subset_cmul)
   7.364 +
   7.365 +lemma singular_relcycle_minus:
   7.366 +   "singular_relcycle p X S (-c) \<longleftrightarrow> singular_relcycle p X S c"
   7.367 +  by (simp add: chain_boundary_minus singular_chain_minus singular_relcycle)
   7.368 +
   7.369 +lemma singular_relcycle_add:
   7.370 +   "\<lbrakk>singular_relcycle p X S a; singular_relcycle p X S b\<rbrakk>
   7.371 +        \<Longrightarrow> singular_relcycle p X S (a+b)"
   7.372 +  by (simp add: singular_relcycle_def chain_boundary_add mod_subset_def singular_chain_add)
   7.373 +
   7.374 +lemma singular_relcycle_sum:
   7.375 +   "\<lbrakk>\<And>i. i \<in> I \<Longrightarrow> singular_relcycle p X S (f i)\<rbrakk>
   7.376 +        \<Longrightarrow> singular_relcycle p X S (sum f I)"
   7.377 +  by (induction I rule: infinite_finite_induct) (auto simp: singular_relcycle_add)
   7.378 +
   7.379 +lemma singular_relcycle_diff:
   7.380 +   "\<lbrakk>singular_relcycle p X S a; singular_relcycle p X S b\<rbrakk>
   7.381 +        \<Longrightarrow> singular_relcycle p X S (a-b)"
   7.382 +  by (metis singular_relcycle_add singular_relcycle_minus uminus_add_conv_diff)
   7.383 +
   7.384 +lemma singular_cycle:
   7.385 +   "singular_relcycle p X {} c \<longleftrightarrow> singular_chain p X c \<and> chain_boundary p c = 0"
   7.386 +  by (simp add: singular_relcycle_def)
   7.387 +
   7.388 +lemma singular_cycle_mono:
   7.389 +   "\<lbrakk>singular_relcycle p (subtopology X T) {} c; T \<subseteq> S\<rbrakk>
   7.390 +        \<Longrightarrow> singular_relcycle p (subtopology X S) {} c"
   7.391 +  by (auto simp: singular_cycle elim: singular_chain_mono)
   7.392 +
   7.393 +
   7.394 +subsection\<open>Relative boundaries $B_p X S$, where $X$ is a topology and $S$ a subset.\<close>
   7.395 +
   7.396 +definition singular_relboundary :: "nat \<Rightarrow> 'a topology \<Rightarrow> 'a set \<Rightarrow> ('a chain) \<Rightarrow> bool"
   7.397 +  where
   7.398 +  "singular_relboundary p X S \<equiv>
   7.399 +    \<lambda>c. \<exists>d. singular_chain (Suc p) X d \<and> (chain_boundary (Suc p) d, c) \<in> (mod_subset p (subtopology X S))"
   7.400 +
   7.401 +abbreviation singular_relboundary_set :: "nat \<Rightarrow> 'a topology \<Rightarrow> 'a set \<Rightarrow> ('a chain) set"
   7.402 +  where "singular_relboundary_set p X S \<equiv> Collect (singular_relboundary p X S)"
   7.403 +
   7.404 +lemma singular_relboundary_restrict [simp]:
   7.405 +   "singular_relboundary p X (topspace X \<inter> S) = singular_relboundary p X S"
   7.406 +  unfolding singular_relboundary_def
   7.407 +  by (metis (no_types, hide_lams) subtopology_subtopology subtopology_topspace)
   7.408 +
   7.409 +lemma singular_relboundary_alt:
   7.410 +   "singular_relboundary p X S c \<longleftrightarrow>
   7.411 +    (\<exists>d e. singular_chain (Suc p) X d \<and> singular_chain p (subtopology X S) e \<and>
   7.412 +           chain_boundary (Suc p) d = c + e)"
   7.413 +  unfolding singular_relboundary_def mod_subset_def by fastforce
   7.414 +
   7.415 +lemma singular_relboundary:
   7.416 +   "singular_relboundary p X S c \<longleftrightarrow>
   7.417 +    (\<exists>d e. singular_chain (Suc p) X d \<and> singular_chain p (subtopology X S) e \<and>
   7.418 +              (chain_boundary (Suc p) d) + e = c)"
   7.419 +  using singular_chain_minus
   7.420 +  by (fastforce simp add: singular_relboundary_alt)
   7.421 +
   7.422 +lemma singular_boundary:
   7.423 +   "singular_relboundary p X {} c \<longleftrightarrow>
   7.424 +    (\<exists>d. singular_chain (Suc p) X d \<and> chain_boundary (Suc p) d = c)"
   7.425 +  by (simp add: singular_relboundary_def)
   7.426 +
   7.427 +lemma singular_boundary_imp_chain:
   7.428 +   "singular_relboundary p X {} c \<Longrightarrow> singular_chain p X c"
   7.429 +  by (auto simp: singular_relboundary singular_chain_boundary_alt singular_chain_empty topspace_subtopology)
   7.430 +
   7.431 +lemma singular_boundary_mono:
   7.432 +   "\<lbrakk>T \<subseteq> S; singular_relboundary p (subtopology X T) {} c\<rbrakk>
   7.433 +        \<Longrightarrow> singular_relboundary p (subtopology X S) {} c"
   7.434 +  by (metis mod_subset_empty singular_chain_mono singular_relboundary_def)
   7.435 +
   7.436 +lemma singular_relboundary_imp_chain:
   7.437 +   "singular_relboundary p X S c \<Longrightarrow> singular_chain p X c"
   7.438 +  unfolding singular_relboundary singular_chain_subtopology
   7.439 +  by (blast intro: singular_chain_add singular_chain_boundary_alt)
   7.440 +
   7.441 +lemma singular_chain_imp_relboundary:
   7.442 +   "singular_chain p (subtopology X S) c \<Longrightarrow> singular_relboundary p X S c"
   7.443 +  unfolding singular_relboundary_def
   7.444 +  apply (rule_tac x=0 in exI)
   7.445 +  using mod_subset_def singular_chain_diff by fastforce
   7.446 +
   7.447 +lemma singular_relboundary_0 [simp]: "singular_relboundary p X S 0"
   7.448 +  unfolding singular_relboundary_def
   7.449 +  by (rule_tac x=0 in exI) auto
   7.450 +
   7.451 +lemma singular_relboundary_cmul:
   7.452 +   "singular_relboundary p X S c \<Longrightarrow> singular_relboundary p X S (frag_cmul a c)"
   7.453 +  unfolding singular_relboundary_def
   7.454 +  by (metis chain_boundary_cmul mod_subset_cmul singular_chain_cmul)
   7.455 +
   7.456 +lemma singular_relboundary_minus:
   7.457 +   "singular_relboundary p X S (-c) \<longleftrightarrow> singular_relboundary p X S c"
   7.458 +  using singular_relboundary_cmul
   7.459 +  by (metis add.inverse_inverse frag_cmul_minus_one)
   7.460 +
   7.461 +lemma singular_relboundary_add:
   7.462 +   "\<lbrakk>singular_relboundary p X S a; singular_relboundary p X S b\<rbrakk> \<Longrightarrow> singular_relboundary p X S (a+b)"
   7.463 +  unfolding singular_relboundary_def
   7.464 +  by (metis chain_boundary_add mod_subset_add singular_chain_add)
   7.465 +
   7.466 +lemma singular_relboundary_diff:
   7.467 +   "\<lbrakk>singular_relboundary p X S a; singular_relboundary p X S b\<rbrakk> \<Longrightarrow> singular_relboundary p X S (a-b)"
   7.468 +  by (metis uminus_add_conv_diff singular_relboundary_minus singular_relboundary_add)
   7.469 +
   7.470 +subsection\<open>The (relative) homology relation\<close>
   7.471 +
   7.472 +definition homologous_rel :: "[nat,'a topology,'a set,'a chain,'a chain] \<Rightarrow> bool"
   7.473 +  where "homologous_rel p X S \<equiv> \<lambda>a b. singular_relboundary p X S (a-b)"
   7.474 +
   7.475 +abbreviation homologous_rel_set
   7.476 +  where "homologous_rel_set p X S a \<equiv> Collect (homologous_rel p X S a)"
   7.477 +
   7.478 +lemma homologous_rel_restrict [simp]:
   7.479 +   "homologous_rel p X (topspace X \<inter> S) = homologous_rel p X S"
   7.480 +  unfolding homologous_rel_def by (metis singular_relboundary_restrict)
   7.481 +
   7.482 +lemma homologous_rel_refl [simp]: "homologous_rel p X S c c"
   7.483 +  unfolding homologous_rel_def by auto
   7.484 +
   7.485 +lemma homologous_rel_sym:
   7.486 +   "homologous_rel p X S a b = homologous_rel p X S b a"
   7.487 +  unfolding homologous_rel_def
   7.488 +  using singular_relboundary_minus by fastforce
   7.489 +
   7.490 +lemma homologous_rel_trans:
   7.491 +  assumes "homologous_rel p X S b c" "homologous_rel p X S a b"
   7.492 +  shows "homologous_rel p X S a c"
   7.493 +  using homologous_rel_def
   7.494 +proof -
   7.495 +  have "singular_relboundary p X S (b - c)"
   7.496 +    using assms unfolding homologous_rel_def by blast
   7.497 +  moreover have "singular_relboundary p X S (b - a)"
   7.498 +    using assms by (meson homologous_rel_def homologous_rel_sym)
   7.499 +  ultimately have "singular_relboundary p X S (c - a)"
   7.500 +    using singular_relboundary_diff by fastforce
   7.501 +  then show ?thesis
   7.502 +    by (meson homologous_rel_def homologous_rel_sym)
   7.503 +qed
   7.504 +
   7.505 +lemma homologous_rel_eq:
   7.506 +   "homologous_rel p X S a = homologous_rel p X S b \<longleftrightarrow>
   7.507 +    homologous_rel p X S a b"
   7.508 +  using homologous_rel_sym homologous_rel_trans by fastforce
   7.509 +
   7.510 +lemma homologous_rel_set_eq:
   7.511 +   "homologous_rel_set p X S a = homologous_rel_set p X S b \<longleftrightarrow>
   7.512 +    homologous_rel p X S a b"
   7.513 +  by (metis homologous_rel_eq mem_Collect_eq)
   7.514 +
   7.515 +lemma homologous_rel_singular_chain:
   7.516 +  "homologous_rel p X S a b \<Longrightarrow> (singular_chain p X a \<longleftrightarrow> singular_chain p X b)"
   7.517 +  unfolding homologous_rel_def
   7.518 +  using singular_chain_diff singular_chain_add
   7.519 +  by (fastforce dest: singular_relboundary_imp_chain)
   7.520 +
   7.521 +lemma homologous_rel_add:
   7.522 +   "\<lbrakk>homologous_rel p X S a a'; homologous_rel p X S b b'\<rbrakk>
   7.523 +        \<Longrightarrow> homologous_rel p X S (a+b) (a'+b')"
   7.524 +  unfolding homologous_rel_def
   7.525 +  by (simp add: add_diff_add singular_relboundary_add)
   7.526 +
   7.527 +lemma homologous_rel_diff:
   7.528 +  assumes "homologous_rel p X S a a'" "homologous_rel p X S b b'"
   7.529 +  shows "homologous_rel p X S (a - b) (a' - b')"
   7.530 +proof -
   7.531 +  have "singular_relboundary p X S ((a - a') - (b - b'))"
   7.532 +    using assms singular_relboundary_diff unfolding homologous_rel_def by blast
   7.533 +  then show ?thesis
   7.534 +    by (simp add: homologous_rel_def algebra_simps)
   7.535 +qed
   7.536 +
   7.537 +lemma homologous_rel_sum:
   7.538 +  assumes f: "finite {i \<in> I. f i \<noteq> 0}" and g: "finite {i \<in> I. g i \<noteq> 0}"
   7.539 +    and h: "\<And>i. i \<in> I \<Longrightarrow> homologous_rel p X S (f i) (g i)"
   7.540 +  shows "homologous_rel p X S (sum f I) (sum g I)"
   7.541 +proof (cases "finite I")
   7.542 +  case True
   7.543 +  let ?L = "{i \<in> I. f i \<noteq> 0} \<union> {i \<in> I. g i \<noteq> 0}"
   7.544 +  have L: "finite ?L" "?L \<subseteq> I"
   7.545 +    using f g by blast+
   7.546 +  have "sum f I = sum f ?L"
   7.547 +    by (rule comm_monoid_add_class.sum.mono_neutral_right [OF True]) auto
   7.548 +  moreover have "sum g I = sum g ?L"
   7.549 +    by (rule comm_monoid_add_class.sum.mono_neutral_right [OF True]) auto
   7.550 +  moreover have *: "homologous_rel p X S (f i) (g i)" if "i \<in> ?L" for i
   7.551 +    using h that by auto
   7.552 +  have "homologous_rel p X S (sum f ?L) (sum g ?L)"
   7.553 +    using L
   7.554 +  proof induction
   7.555 +    case (insert j J)
   7.556 +    then show ?case
   7.557 +      by (simp add: h homologous_rel_add)
   7.558 +  qed auto
   7.559 +  ultimately show ?thesis
   7.560 +    by simp
   7.561 +qed auto
   7.562 +
   7.563 +
   7.564 +lemma chain_homotopic_imp_homologous_rel:
   7.565 +  assumes
   7.566 +   "\<And>c. singular_chain p X c \<Longrightarrow> singular_chain (Suc p) X' (h c)"
   7.567 +   "\<And>c. singular_chain (p -1) (subtopology X S) c \<Longrightarrow> singular_chain p (subtopology X' T) (h' c)"
   7.568 +   "\<And>c. singular_chain p X c
   7.569 +             \<Longrightarrow> (chain_boundary (Suc p) (h c)) + (h'(chain_boundary p c)) = f c - g c"
   7.570 +    "singular_relcycle p X S c"
   7.571 +  shows "homologous_rel p X' T (f c) (g c)"
   7.572 +  using assms
   7.573 +  unfolding singular_relcycle_def mod_subset_def homologous_rel_def singular_relboundary_def
   7.574 +  apply (rule_tac x="h c" in exI, simp)
   7.575 +  by (metis (no_types, lifting) add_diff_cancel_left' minus_diff_eq singular_chain_minus)
   7.576 +
   7.577 +
   7.578 +subsection\<open>Show that all boundaries are cycles, the key "chain complex" property.\<close>
   7.579 +
   7.580 +lemma sum_Int_Diff: "finite A \<Longrightarrow> sum f A = sum f (A \<inter> B) + sum f (A - B)"
   7.581 +  by (metis Diff_Diff_Int Diff_subset sum.subset_diff)
   7.582 +
   7.583 +lemma chain_boundary_boundary:
   7.584 +  assumes "singular_chain p X c"
   7.585 +  shows "chain_boundary (p - Suc 0) (chain_boundary p c) = 0"
   7.586 +proof (cases "p -1 = 0")
   7.587 +  case False
   7.588 +  then have "2 \<le> p"
   7.589 +    by auto
   7.590 +  show ?thesis
   7.591 +    using assms
   7.592 +    unfolding singular_chain_def
   7.593 +  proof (induction rule: frag_induction)
   7.594 +    case (one g)
   7.595 +    then have ss: "singular_simplex p X g"
   7.596 +      by simp
   7.597 +    have eql: "{..p} \<times> {..p - Suc 0} \<inter> {(x, y). y < x} = (\<lambda>(j,i). (Suc i, j)) ` {(i,j). i \<le> j \<and> j \<le> p -1}"
   7.598 +      using False
   7.599 +      by (auto simp: image_def) (metis One_nat_def diff_Suc_1 diff_le_mono le_refl lessE less_imp_le_nat)
   7.600 +    have eqr: "{..p} \<times> {..p - Suc 0} - {(x, y). y < x} = {(i,j). i \<le> j \<and> j \<le> p -1}"
   7.601 +      by auto
   7.602 +    have eqf: "singular_face (p - Suc 0) i (singular_face p (Suc j) g) =
   7.603 +               singular_face (p - Suc 0) j (singular_face p i g)" if "i \<le> j" "j \<le> p - Suc 0" for i j
   7.604 +    proof (rule ext)
   7.605 +      fix t
   7.606 +      show "singular_face (p - Suc 0) i (singular_face p (Suc j) g) t =
   7.607 +            singular_face (p - Suc 0) j (singular_face p i g) t"
   7.608 +      proof (cases "t \<in> standard_simplex (p -1 -1)")
   7.609 +        case True
   7.610 +        have fi: "simplical_face i t \<in> standard_simplex (p - Suc 0)"
   7.611 +          using False True simplical_face_in_standard_simplex that by force
   7.612 +        have fj: "simplical_face j t \<in> standard_simplex (p - Suc 0)"
   7.613 +          by (metis False One_nat_def True simplical_face_in_standard_simplex less_one not_less that(2))
   7.614 +        have eq: "simplical_face (Suc j) (simplical_face i t) = simplical_face i (simplical_face j t)"
   7.615 +          using True that ss
   7.616 +          unfolding standard_simplex_def simplical_face_def by fastforce
   7.617 +        show ?thesis by (simp add: singular_face_def fi fj eq)
   7.618 +      qed (simp add: singular_face_def)
   7.619 +    qed
   7.620 +    show ?case
   7.621 +    proof (cases "p = 1")
   7.622 +      case False
   7.623 +      have eq0: "frag_cmul (-1) a = b \<Longrightarrow> a + b = 0" for a b
   7.624 +        by (simp add: neg_eq_iff_add_eq_0)
   7.625 +      have *: "(\<Sum>x\<le>p. \<Sum>i\<le>p - Suc 0.
   7.626 +                 frag_cmul ((-1) ^ (x + i)) (frag_of (singular_face (p - Suc 0) i (singular_face p x g))))
   7.627 +              = 0"
   7.628 +        apply (simp add: sum.cartesian_product sum_Int_Diff [of "_ \<times> _" _ "{(x,y). y < x}"])
   7.629 +        apply (rule eq0)
   7.630 +        apply (simp only: frag_cmul_sum prod.case_distrib [of "frag_cmul (-1)"] frag_cmul_cmul eql eqr flip: power_Suc)
   7.631 +        apply (force simp: simp add: inj_on_def sum.reindex add.commute eqf intro: sum.cong)
   7.632 +        done
   7.633 +      show ?thesis
   7.634 +        using False by (simp add: chain_boundary_of chain_boundary_sum chain_boundary_cmul frag_cmul_sum * flip: power_add)
   7.635 +    qed (simp add: chain_boundary_def)
   7.636 +  next
   7.637 +    case (diff a b)
   7.638 +    then show ?case
   7.639 +      by (simp add: chain_boundary_diff)
   7.640 +  qed auto
   7.641 +qed (simp add: chain_boundary_def)
   7.642 +
   7.643 +
   7.644 +lemma chain_boundary_boundary_alt:
   7.645 +   "singular_chain (Suc p) X c \<Longrightarrow> chain_boundary p (chain_boundary (Suc p) c) = 0"
   7.646 +  using chain_boundary_boundary by force
   7.647 +
   7.648 +lemma singular_relboundary_imp_relcycle:
   7.649 +  assumes "singular_relboundary p X S c"
   7.650 +  shows "singular_relcycle p X S c"
   7.651 +proof -
   7.652 +  obtain d e where d: "singular_chain (Suc p) X d"
   7.653 +               and e: "singular_chain p (subtopology X S) e"
   7.654 +               and c: "c = chain_boundary (Suc p) d + e"
   7.655 +    using assms by (auto simp: singular_relboundary singular_relcycle)
   7.656 +  have 1: "singular_chain (p - Suc 0) (subtopology X S) (chain_boundary p (chain_boundary (Suc p) d))"
   7.657 +    using d chain_boundary_boundary_alt by fastforce
   7.658 +  have 2: "singular_chain (p - Suc 0) (subtopology X S) (chain_boundary p e)"
   7.659 +    using \<open>singular_chain p (subtopology X S) e\<close> singular_chain_boundary by auto
   7.660 +  have "singular_chain p X c"
   7.661 +    using assms singular_relboundary_imp_chain by auto
   7.662 +  moreover have "singular_chain (p - Suc 0) (subtopology X S) (chain_boundary p c)"
   7.663 +    by (simp add: c chain_boundary_add singular_chain_add 1 2)
   7.664 +  ultimately show ?thesis
   7.665 +    by (simp add: singular_relcycle)
   7.666 +qed
   7.667 +
   7.668 +lemma homologous_rel_singular_relcycle_1:
   7.669 +  assumes "homologous_rel p X S c1 c2" "singular_relcycle p X S c1"
   7.670 +  shows "singular_relcycle p X S c2"
   7.671 +  using assms
   7.672 +  by (metis diff_add_cancel homologous_rel_def homologous_rel_sym singular_relboundary_imp_relcycle singular_relcycle_add)
   7.673 +
   7.674 +lemma homologous_rel_singular_relcycle:
   7.675 +  assumes "homologous_rel p X S c1 c2"
   7.676 +  shows "singular_relcycle p X S c1 = singular_relcycle p X S c2"
   7.677 +  using assms homologous_rel_singular_relcycle_1
   7.678 +  using homologous_rel_sym by blast
   7.679 +
   7.680 +
   7.681 +subsection\<open>Operations induced by a continuous map g between topological spaces\<close>
   7.682 +
   7.683 +definition simplex_map :: "nat \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> ((nat \<Rightarrow> real) \<Rightarrow> 'b) \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> 'a"
   7.684 +  where "simplex_map p g c \<equiv> restrict (g \<circ> c) (standard_simplex p)"
   7.685 +
   7.686 +lemma singular_simplex_simplex_map:
   7.687 +   "\<lbrakk>singular_simplex p X f; continuous_map X X' g\<rbrakk>
   7.688 +        \<Longrightarrow> singular_simplex p X' (simplex_map p g f)"
   7.689 +  unfolding singular_simplex_def simplex_map_def
   7.690 +  by (auto simp: continuous_map_compose)
   7.691 +
   7.692 +lemma simplex_map_eq:
   7.693 +   "\<lbrakk>singular_simplex p X c;
   7.694 +     \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk>
   7.695 +    \<Longrightarrow> simplex_map p f c = simplex_map p g c"
   7.696 +  by (auto simp: singular_simplex_def simplex_map_def continuous_map_def)
   7.697 +
   7.698 +lemma simplex_map_id_gen:
   7.699 +   "\<lbrakk>singular_simplex p X c;
   7.700 +     \<And>x. x \<in> topspace X \<Longrightarrow> f x = x\<rbrakk>
   7.701 +    \<Longrightarrow> simplex_map p f c = c"
   7.702 +  unfolding singular_simplex_def simplex_map_def continuous_map_def
   7.703 +  using extensional_arb by fastforce
   7.704 +
   7.705 +lemma simplex_map_id [simp]:
   7.706 +   "simplex_map p id = (\<lambda>c. restrict c (standard_simplex p))"
   7.707 +  by (auto simp: simplex_map_def)
   7.708 +
   7.709 +lemma simplex_map_compose:
   7.710 +   "simplex_map p (h \<circ> g) = simplex_map p h \<circ> simplex_map p g"
   7.711 +  unfolding simplex_map_def by force
   7.712 +
   7.713 +lemma singular_face_simplex_map:
   7.714 +   "\<lbrakk>1 \<le> p; k \<le> p\<rbrakk>
   7.715 +        \<Longrightarrow> singular_face p k (simplex_map p f c) = simplex_map (p - Suc 0) f (c \<circ> simplical_face k)"
   7.716 +  unfolding simplex_map_def singular_face_def
   7.717 +  by (force simp: simplical_face_in_standard_simplex)
   7.718 +
   7.719 +lemma singular_face_restrict [simp]:
   7.720 +  assumes "p > 0" "i \<le> p"
   7.721 +  shows "singular_face p i (restrict f (standard_simplex p)) = singular_face p i f"
   7.722 +  by (metis assms One_nat_def Suc_leI simplex_map_id singular_face_def singular_face_simplex_map)
   7.723 +
   7.724 +
   7.725 +definition chain_map :: "nat \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> (((nat \<Rightarrow> real) \<Rightarrow> 'b) \<Rightarrow>\<^sub>0 int) \<Rightarrow> 'a chain"
   7.726 +  where "chain_map p g c \<equiv> frag_extend (frag_of \<circ> simplex_map p g) c"
   7.727 +
   7.728 +lemma singular_chain_chain_map:
   7.729 +   "\<lbrakk>singular_chain p X c; continuous_map X X' g\<rbrakk> \<Longrightarrow> singular_chain p X' (chain_map p g c)"
   7.730 +  unfolding chain_map_def
   7.731 +  apply (rule singular_chain_extend)
   7.732 +  by (metis comp_apply subsetD mem_Collect_eq singular_chain_def singular_chain_of singular_simplex_simplex_map)
   7.733 +
   7.734 +lemma chain_map_0 [simp]: "chain_map p g 0 = 0"
   7.735 +  by (auto simp: chain_map_def)
   7.736 +
   7.737 +lemma chain_map_of [simp]: "chain_map p g (frag_of f) = frag_of (simplex_map p g f)"
   7.738 +  by (simp add: chain_map_def)
   7.739 +
   7.740 +lemma chain_map_cmul [simp]:
   7.741 +   "chain_map p g (frag_cmul a c) = frag_cmul a (chain_map p g c)"
   7.742 +  by (simp add: frag_extend_cmul chain_map_def)
   7.743 +
   7.744 +lemma chain_map_minus: "chain_map p g (-c) = - (chain_map p g c)"
   7.745 +  by (simp add: frag_extend_minus chain_map_def)
   7.746 +
   7.747 +lemma chain_map_add:
   7.748 +   "chain_map p g (a+b) = chain_map p g a + chain_map p g b"
   7.749 +  by (simp add: frag_extend_add chain_map_def)
   7.750 +
   7.751 +lemma chain_map_diff:
   7.752 +   "chain_map p g (a-b) = chain_map p g a - chain_map p g b"
   7.753 +  by (simp add: frag_extend_diff chain_map_def)
   7.754 +
   7.755 +lemma chain_map_sum:
   7.756 +   "finite I \<Longrightarrow> chain_map p g (sum f I) = sum (chain_map p g \<circ> f) I"
   7.757 +  by (simp add: frag_extend_sum chain_map_def)
   7.758 +
   7.759 +lemma chain_map_eq:
   7.760 +   "\<lbrakk>singular_chain p X c; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk>
   7.761 +    \<Longrightarrow> chain_map p f c = chain_map p g c"
   7.762 +  unfolding singular_chain_def
   7.763 +  apply (erule frag_induction)
   7.764 +    apply (auto simp: chain_map_diff)
   7.765 +  apply (metis simplex_map_eq)
   7.766 +  done
   7.767 +
   7.768 +lemma chain_map_id_gen:
   7.769 +   "\<lbrakk>singular_chain p X c; \<And>x. x \<in> topspace X \<Longrightarrow> f x = x\<rbrakk>
   7.770 +    \<Longrightarrow>  chain_map p f c = c"
   7.771 +  unfolding singular_chain_def
   7.772 +  by (erule frag_induction) (auto simp: chain_map_diff simplex_map_id_gen)
   7.773 +
   7.774 +lemma chain_map_ident:
   7.775 +   "singular_chain p X c \<Longrightarrow> chain_map p id c = c"
   7.776 +  by (simp add: chain_map_id_gen)
   7.777 +
   7.778 +lemma chain_map_id:
   7.779 +   "chain_map p id = frag_extend (frag_of \<circ> (\<lambda>f. restrict f (standard_simplex p)))"
   7.780 +  by (auto simp: chain_map_def)
   7.781 +
   7.782 +lemma chain_map_compose:
   7.783 +   "chain_map p (h \<circ> g) = chain_map p h \<circ> chain_map p g"
   7.784 +proof
   7.785 +  show "chain_map p (h \<circ> g) c = (chain_map p h \<circ> chain_map p g) c" for c
   7.786 +    using subset_UNIV
   7.787 +  proof (induction c rule: frag_induction)
   7.788 +    case (one x)
   7.789 +    then show ?case
   7.790 +      by simp (metis (mono_tags, lifting) comp_eq_dest_lhs restrict_apply simplex_map_def)
   7.791 +  next
   7.792 +    case (diff a b)
   7.793 +    then show ?case
   7.794 +      by (simp add: chain_map_diff)
   7.795 +  qed auto
   7.796 +qed
   7.797 +
   7.798 +lemma singular_simplex_chain_map_id:
   7.799 +  assumes "singular_simplex p X f"
   7.800 +  shows "chain_map p f (frag_of (restrict id (standard_simplex p))) = frag_of f"
   7.801 +proof -
   7.802 +  have "(restrict (f \<circ> restrict id (standard_simplex p)) (standard_simplex p)) = f"
   7.803 +    by (rule ext) (metis assms comp_apply extensional_arb id_apply restrict_apply singular_simplex_def)
   7.804 +  then show ?thesis
   7.805 +    by (simp add: simplex_map_def)
   7.806 +qed
   7.807 +
   7.808 +lemma chain_boundary_chain_map:
   7.809 +  assumes "singular_chain p X c"
   7.810 +  shows "chain_boundary p (chain_map p g c) = chain_map (p - Suc 0) g (chain_boundary p c)"
   7.811 +  using assms unfolding singular_chain_def
   7.812 +proof (induction c rule: frag_induction)
   7.813 +  case (one x)
   7.814 +  then have "singular_face p i (simplex_map p g x) = simplex_map (p - Suc 0) g (singular_face p i x)"
   7.815 +    if "0 \<le> i" "i \<le> p" "p \<noteq> 0" for i
   7.816 +    using that
   7.817 +    by (fastforce simp add: singular_face_def simplex_map_def simplical_face_in_standard_simplex)
   7.818 +  then show ?case
   7.819 +    by (auto simp: chain_boundary_of chain_map_sum)
   7.820 +next
   7.821 +  case (diff a b)
   7.822 +  then show ?case
   7.823 +    by (simp add: chain_boundary_diff chain_map_diff)
   7.824 +qed auto
   7.825 +
   7.826 +lemma singular_relcycle_chain_map:
   7.827 +  assumes "singular_relcycle p X S c" "continuous_map X X' g" "g ` S \<subseteq> T"
   7.828 +  shows "singular_relcycle p X' T (chain_map p g c)"
   7.829 +proof -
   7.830 +  have "continuous_map (subtopology X S) (subtopology X' T) g"
   7.831 +    using assms
   7.832 +    using continuous_map_from_subtopology continuous_map_in_subtopology topspace_subtopology by fastforce
   7.833 +  then show ?thesis
   7.834 +    using chain_boundary_chain_map [of p X c g]
   7.835 +    by (metis One_nat_def assms(1) assms(2) singular_chain_chain_map singular_relcycle)
   7.836 +qed
   7.837 +
   7.838 +lemma singular_relboundary_chain_map:
   7.839 +  assumes "singular_relboundary p X S c" "continuous_map X X' g" "g ` S \<subseteq> T"
   7.840 +  shows "singular_relboundary p X' T (chain_map p g c)"
   7.841 +proof -
   7.842 +  obtain d e where d: "singular_chain (Suc p) X d"
   7.843 +    and e: "singular_chain p (subtopology X S) e" and c: "c = chain_boundary (Suc p) d + e"
   7.844 +    using assms by (auto simp: singular_relboundary)
   7.845 +  have "singular_chain (Suc p) X' (chain_map (Suc p) g d)"
   7.846 +    using assms(2) d singular_chain_chain_map by blast
   7.847 +  moreover have "singular_chain p (subtopology X' T) (chain_map p g e)"
   7.848 +  proof -
   7.849 +    have "\<forall>t. g ` topspace (subtopology t S) \<subseteq> T"
   7.850 +      by (metis assms(3) closure_of_subset_subtopology closure_of_topspace dual_order.trans image_mono)
   7.851 +    then show ?thesis
   7.852 +      by (meson assms(2) continuous_map_from_subtopology continuous_map_in_subtopology e singular_chain_chain_map)
   7.853 +  qed
   7.854 +  moreover have "chain_boundary (Suc p) (chain_map (Suc p) g d) + chain_map p g e =
   7.855 +                 chain_map p g (chain_boundary (Suc p) d + e)"
   7.856 +    by (metis One_nat_def chain_boundary_chain_map chain_map_add d diff_Suc_1)
   7.857 +  ultimately show ?thesis
   7.858 +    unfolding singular_relboundary
   7.859 +    using c by blast
   7.860 +qed
   7.861 +
   7.862 +
   7.863 +subsection\<open>Homology of one-point spaces degenerates except for $p = 0$.\<close>
   7.864 +
   7.865 +lemma singular_simplex_singleton:
   7.866 +  assumes "topspace X = {a}"
   7.867 +  shows "singular_simplex p X f \<longleftrightarrow> f = restrict (\<lambda>x. a) (standard_simplex p)" (is "?lhs = ?rhs")
   7.868 +proof
   7.869 +  assume L: ?lhs
   7.870 +  then show ?rhs
   7.871 +  proof -
   7.872 +    have "continuous_map (subtopology (product_topology (\<lambda>n. euclideanreal) UNIV) (standard_simplex p)) X f"
   7.873 +      using \<open>singular_simplex p X f\<close> singular_simplex_def by blast
   7.874 +    then have "\<And>c. c \<notin> standard_simplex p \<or> f c = a"
   7.875 +      by (simp add: assms continuous_map_def)
   7.876 +    then show ?thesis
   7.877 +      by (metis (no_types) L extensional_restrict restrict_ext singular_simplex_def)
   7.878 +  qed
   7.879 +next
   7.880 +  assume ?rhs
   7.881 +  with assms show ?lhs
   7.882 +    by (auto simp: singular_simplex_def topspace_subtopology)
   7.883 +qed
   7.884 +
   7.885 +lemma singular_chain_singleton:
   7.886 +  assumes "topspace X = {a}"
   7.887 +  shows "singular_chain p X c \<longleftrightarrow>
   7.888 +         (\<exists>b. c = frag_cmul b (frag_of(restrict (\<lambda>x. a) (standard_simplex p))))"
   7.889 +    (is "?lhs = ?rhs")
   7.890 +proof
   7.891 +  let ?f = "restrict (\<lambda>x. a) (standard_simplex p)"
   7.892 +  assume L: ?lhs
   7.893 +  with assms have "Poly_Mapping.keys c \<subseteq> {?f}"
   7.894 +    by (auto simp: singular_chain_def singular_simplex_singleton)
   7.895 +  then consider "Poly_Mapping.keys c = {}" | "Poly_Mapping.keys c = {?f}"
   7.896 +    by blast
   7.897 +  then show ?rhs
   7.898 +  proof cases
   7.899 +    case 1
   7.900 +    with L show ?thesis
   7.901 +      by (metis frag_cmul_zero keys_eq_empty)
   7.902 +  next
   7.903 +    case 2
   7.904 +    then have "\<exists>b. frag_extend frag_of c = frag_cmul b (frag_of (\<lambda>x\<in>standard_simplex p. a))"
   7.905 +      by (force simp: frag_extend_def)
   7.906 +    then show ?thesis
   7.907 +      by (metis frag_expansion)
   7.908 +  qed
   7.909 +next
   7.910 +  assume ?rhs
   7.911 +  with assms show ?lhs
   7.912 +    by (auto simp: singular_chain_def singular_simplex_singleton)
   7.913 +qed
   7.914 +
   7.915 +lemma chain_boundary_of_singleton:
   7.916 +  assumes tX: "topspace X = {a}" and sc: "singular_chain p X c"
   7.917 +  shows "chain_boundary p c =
   7.918 +         (if p = 0 \<or> odd p then 0
   7.919 +          else frag_extend (\<lambda>f. frag_of(restrict (\<lambda>x. a) (standard_simplex (p -1)))) c)"
   7.920 +    (is "?lhs = ?rhs")
   7.921 +proof (cases "p = 0")
   7.922 +  case False
   7.923 +  have "?lhs = frag_extend (\<lambda>f. if odd p then 0 else frag_of(restrict (\<lambda>x. a) (standard_simplex (p -1)))) c"
   7.924 +  proof (simp only: chain_boundary_def False if_False, rule frag_extend_eq)
   7.925 +    fix f
   7.926 +    assume "f \<in> Poly_Mapping.keys c"
   7.927 +    with assms have "singular_simplex p X f"
   7.928 +      by (auto simp: singular_chain_def)
   7.929 +    then have *: "\<And>k. k \<le> p \<Longrightarrow> singular_face p k f = (\<lambda>x\<in>standard_simplex (p -1). a)"
   7.930 +      apply (subst singular_simplex_singleton [OF tX, symmetric])
   7.931 +      using False singular_simplex_singular_face by fastforce
   7.932 +    define c where "c \<equiv> frag_of (\<lambda>x\<in>standard_simplex (p -1). a)"
   7.933 +    have "(\<Sum>k\<le>p. frag_cmul ((-1) ^ k) (frag_of (singular_face p k f)))
   7.934 +        = (\<Sum>k\<le>p. frag_cmul ((-1) ^ k) c)"
   7.935 +      by (auto simp: c_def * intro: sum.cong)
   7.936 +    also have "\<dots> = (if odd p then 0 else c)"
   7.937 +      by (induction p) (auto simp: c_def restrict_def)
   7.938 +    finally show "(\<Sum>k\<le>p. frag_cmul ((-1) ^ k) (frag_of (singular_face p k f)))
   7.939 +                = (if odd p then 0 else frag_of (\<lambda>x\<in>standard_simplex (p -1). a))"
   7.940 +      unfolding c_def .
   7.941 +  qed
   7.942 +  also have "\<dots> = ?rhs"
   7.943 +    by (auto simp: False frag_extend_eq_0)
   7.944 +  finally show ?thesis .
   7.945 +qed (simp add: chain_boundary_def)
   7.946 +
   7.947 +
   7.948 +lemma singular_cycle_singleton:
   7.949 +  assumes "topspace X = {a}"
   7.950 +  shows "singular_relcycle p X {} c \<longleftrightarrow> singular_chain p X c \<and> (p = 0 \<or> odd p \<or> c = 0)"
   7.951 +proof -
   7.952 +  have "c = 0" if "singular_chain p X c" and "chain_boundary p c = 0" and "even p" and "p \<noteq> 0"
   7.953 +    using that assms singular_chain_singleton [of X a p c] chain_boundary_of_singleton [OF assms]
   7.954 +    by (auto simp: frag_extend_cmul)
   7.955 +  moreover
   7.956 +  have "chain_boundary p c = 0" if sc: "singular_chain p X c" and "odd p"
   7.957 +    by (simp add: chain_boundary_of_singleton [OF assms sc] that)
   7.958 +  moreover have "chain_boundary 0 c = 0" if "singular_chain 0 X c" and "p = 0"
   7.959 +    by (simp add: chain_boundary_def)
   7.960 +  ultimately show ?thesis
   7.961 +  using assms by (auto simp: singular_cycle)
   7.962 +qed
   7.963 +
   7.964 +
   7.965 +lemma singular_boundary_singleton:
   7.966 +  assumes "topspace X = {a}"
   7.967 +  shows "singular_relboundary p X {} c \<longleftrightarrow> singular_chain p X c \<and> (odd p \<or> c = 0)"
   7.968 +proof (cases "singular_chain p X c")
   7.969 +  case True
   7.970 +  have eq: "frag_extend (\<lambda>f. frag_of (\<lambda>x\<in>standard_simplex p. a)) (frag_of (\<lambda>x\<in>standard_simplex (Suc p). a))
   7.971 +          = frag_of (\<lambda>x\<in>standard_simplex p. a)"
   7.972 +    by (simp add: singular_chain_singleton frag_extend_cmul assms)
   7.973 +  have "\<exists>d. singular_chain (Suc p) X d \<and> chain_boundary (Suc p) d = c"
   7.974 +    if "singular_chain p X c" and "odd p"
   7.975 +    using assms that
   7.976 +    apply (clarsimp simp: singular_chain_singleton)
   7.977 +    apply (rule_tac x = "frag_cmul b (frag_of (\<lambda>x\<in>standard_simplex (Suc p). a))" in exI)
   7.978 +    apply (subst chain_boundary_of_singleton [of X a "Suc p"])
   7.979 +    apply (auto simp: singular_chain_singleton frag_extend_cmul eq)
   7.980 +    done
   7.981 +  with True assms show ?thesis
   7.982 +    by (auto simp: singular_boundary chain_boundary_of_singleton)
   7.983 +next
   7.984 +  case False
   7.985 +  with assms singular_boundary_imp_chain show ?thesis
   7.986 +    by metis
   7.987 +qed
   7.988 +
   7.989 +
   7.990 +lemma singular_boundary_eq_cycle_singleton:
   7.991 +  assumes "topspace X = {a}" "1 \<le> p"
   7.992 +  shows "singular_relboundary p X {} c \<longleftrightarrow> singular_relcycle p X {} c"
   7.993 +  using assms
   7.994 +  apply (auto simp: singular_boundary chain_boundary_boundary_alt singular_chain_boundary_alt singular_cycle)
   7.995 +  by (metis Suc_neq_Zero le_zero_eq singular_boundary singular_boundary_singleton singular_chain_0 singular_cycle_singleton singular_relcycle)
   7.996 +
   7.997 +lemma singular_boundary_set_eq_cycle_singleton:
   7.998 +  assumes "topspace X = {a}" "1 \<le> p"
   7.999 +  shows "singular_relboundary_set p X {} = singular_relcycle_set p X {}"
  7.1000 +  using singular_boundary_eq_cycle_singleton [OF assms]
  7.1001 +  by blast
  7.1002 +
  7.1003 +subsection\<open>Simplicial chains\<close>
  7.1004 +
  7.1005 +text\<open>Simplicial chains, effectively those resulting from linear maps.
  7.1006 + We still allow the map to be singular, so the name is questionable.
  7.1007 +These are intended as building-blocks for singular subdivision, rather  than as a axis
  7.1008 +for 1 simplicial homology.\<close>
  7.1009 +
  7.1010 +definition oriented_simplex
  7.1011 +  where "oriented_simplex p l \<equiv> (\<lambda>x\<in>standard_simplex p. \<lambda>i. (\<Sum>j\<le>p. l j i * x j))"
  7.1012 +
  7.1013 +definition simplicial_simplex
  7.1014 +  where
  7.1015 + "simplicial_simplex p S f \<equiv>
  7.1016 +        singular_simplex p (subtopology (powertop_real UNIV) S) f \<and>
  7.1017 +        (\<exists>l. f = oriented_simplex p l)"
  7.1018 +
  7.1019 +lemma simplicial_simplex:
  7.1020 +  "simplicial_simplex p S f \<longleftrightarrow> f ` (standard_simplex p) \<subseteq> S \<and> (\<exists>l. f = oriented_simplex p l)"
  7.1021 +  (is "?lhs = ?rhs")
  7.1022 +proof
  7.1023 +  assume R: ?rhs
  7.1024 +  show ?lhs
  7.1025 +    using R
  7.1026 +    apply (clarsimp simp: simplicial_simplex_def singular_simplex_subtopology)
  7.1027 +    apply (simp add: singular_simplex_def oriented_simplex_def)
  7.1028 +    apply (clarsimp simp: continuous_map_componentwise)
  7.1029 +    apply (intro continuous_intros continuous_map_from_subtopology continuous_map_product_projection, auto)
  7.1030 +    done
  7.1031 +qed (simp add: simplicial_simplex_def singular_simplex_subtopology)
  7.1032 +
  7.1033 +lemma simplicial_simplex_empty [simp]: "\<not> simplicial_simplex p {} f"
  7.1034 +  by (simp add: nonempty_standard_simplex simplicial_simplex)
  7.1035 +
  7.1036 +definition simplicial_chain
  7.1037 +  where "simplicial_chain p S c \<equiv> Poly_Mapping.keys c \<subseteq> Collect (simplicial_simplex p S)"
  7.1038 +
  7.1039 +lemma simplicial_chain_0 [simp]: "simplicial_chain p S 0"
  7.1040 +  by (simp add: simplicial_chain_def)
  7.1041 +
  7.1042 +lemma simplicial_chain_of [simp]:
  7.1043 +   "simplicial_chain p S (frag_of c) \<longleftrightarrow> simplicial_simplex p S c"
  7.1044 +  by (simp add: simplicial_chain_def)
  7.1045 +
  7.1046 +lemma simplicial_chain_cmul:
  7.1047 +   "simplicial_chain p S c \<Longrightarrow> simplicial_chain p S (frag_cmul a c)"
  7.1048 +  by (auto simp: simplicial_chain_def)
  7.1049 +
  7.1050 +lemma simplicial_chain_diff:
  7.1051 +   "\<lbrakk>simplicial_chain p S c1; simplicial_chain p S c2\<rbrakk> \<Longrightarrow> simplicial_chain p S (c1 - c2)"
  7.1052 +  unfolding simplicial_chain_def  by (meson UnE keys_diff subset_iff)
  7.1053 +
  7.1054 +lemma simplicial_chain_sum:
  7.1055 +   "(\<And>i. i \<in> I \<Longrightarrow> simplicial_chain p S (f i)) \<Longrightarrow> simplicial_chain p S (sum f I)"
  7.1056 +  unfolding simplicial_chain_def
  7.1057 +  using order_trans [OF keys_sum [of f I]]
  7.1058 +  by (simp add: UN_least)
  7.1059 +
  7.1060 +lemma simplicial_simplex_oriented_simplex:
  7.1061 +   "simplicial_simplex p S (oriented_simplex p l)
  7.1062 +    \<longleftrightarrow> ((\<lambda>x i. \<Sum>j\<le>p. l j i * x j) ` standard_simplex p \<subseteq> S)"
  7.1063 +  by (auto simp: simplicial_simplex oriented_simplex_def)
  7.1064 +
  7.1065 +lemma simplicial_imp_singular_simplex:
  7.1066 +   "simplicial_simplex p S f
  7.1067 +      \<Longrightarrow> singular_simplex p (subtopology (powertop_real UNIV) S) f"
  7.1068 +  by (simp add: simplicial_simplex_def)
  7.1069 +
  7.1070 +lemma simplicial_imp_singular_chain:
  7.1071 +   "simplicial_chain p S c
  7.1072 +      \<Longrightarrow> singular_chain p (subtopology (powertop_real UNIV) S) c"
  7.1073 +  unfolding simplicial_chain_def singular_chain_def
  7.1074 +  by (auto intro: simplicial_imp_singular_simplex)
  7.1075 +
  7.1076 +lemma oriented_simplex_eq:
  7.1077 +  "oriented_simplex p l = oriented_simplex p l' \<longleftrightarrow> (\<forall>i. i \<le> p \<longrightarrow> l i = l' i)"
  7.1078 +  (is "?lhs = ?rhs")
  7.1079 +proof
  7.1080 +  assume L: ?lhs
  7.1081 +  show ?rhs
  7.1082 +  proof clarify
  7.1083 +    fix i
  7.1084 +    assume "i \<le> p"
  7.1085 +    let ?fi = "(\<lambda>j. if j = i then 1 else 0)"
  7.1086 +    have "(\<Sum>j\<le>p. l j k * ?fi j) = (\<Sum>j\<le>p. l' j k * ?fi j)" for k
  7.1087 +      apply (rule fun_cong [where x=k])
  7.1088 +      using fun_cong [OF L, of ?fi]
  7.1089 +      apply (simp add: \<open>i \<le> p\<close> oriented_simplex_def)
  7.1090 +      done
  7.1091 +    with \<open>i \<le> p\<close> show "l i = l' i"
  7.1092 +      by (simp add: if_distrib ext cong: if_cong)
  7.1093 +  qed
  7.1094 +qed (auto simp: oriented_simplex_def)
  7.1095 +
  7.1096 +lemma sum_zero_middle:
  7.1097 +  fixes g :: "nat \<Rightarrow> 'a::comm_monoid_add"
  7.1098 +  assumes "1 \<le> p" "k \<le> p"
  7.1099 +  shows "(\<Sum>j\<le>p. if j < k then f j else if j = k then 0 else g (j - Suc 0))
  7.1100 +       = (\<Sum>j\<le>p - Suc 0. if j < k then f j else g j)"  (is "?lhs = ?rhs")
  7.1101 +proof -
  7.1102 +  have [simp]: "{..p - Suc 0} \<inter> {j. j < k} = {..<k}" "{..p - Suc 0} \<inter> - {j. j < k} = {k..p - Suc 0}"
  7.1103 +    using assms by auto
  7.1104 +  have "?lhs = (\<Sum>j<k. f j)  + (\<Sum>j = k..p. if j = k then 0 else g (j - Suc 0))"
  7.1105 +    using sum.union_disjoint [of "{..<k}" "{k..p}", where 'a='a] assms
  7.1106 +    by (simp add: ivl_disj_int_one ivl_disj_un_one)
  7.1107 +  also have "\<dots> = (\<Sum>j<k. f j) + (\<Sum>j = Suc k..p. g (j - Suc 0))"
  7.1108 +    by (simp add: sum_head_Suc [of k p] assms)
  7.1109 +  also have "\<dots> = (\<Sum>j<k. f j) + (\<Sum>j = k..p - Suc 0. g j)"
  7.1110 +    using sum.reindex [of Suc "{k..p - Suc 0}", where 'a='a] assms by simp
  7.1111 +  also have "\<dots> = ?rhs"
  7.1112 +    by (simp add: comm_monoid_add_class.sum.If_cases)
  7.1113 +  finally show ?thesis .
  7.1114 +qed
  7.1115 +
  7.1116 +lemma singular_face_oriented_simplex:
  7.1117 +  assumes "1 \<le> p" "k \<le> p"
  7.1118 +  shows "singular_face p k (oriented_simplex p l) =
  7.1119 +         oriented_simplex (p -1) (\<lambda>j. if j < k then l j else l (Suc j))"
  7.1120 +proof -
  7.1121 +  have "(\<Sum>j\<le>p. l j i * simplical_face k x j)
  7.1122 +      = (\<Sum>j\<le>p - Suc 0. (if j < k then l j else l (Suc j)) i * x j)"
  7.1123 +    if "x \<in> standard_simplex (p - Suc 0)" for i x
  7.1124 +  proof -
  7.1125 +    show ?thesis
  7.1126 +      unfolding simplical_face_def
  7.1127 +      using sum_zero_middle [OF assms, where 'a=real, symmetric]
  7.1128 +      apply (simp add: if_distrib [of "\<lambda>x. _ * x"] if_distrib [of "\<lambda>f. f i * _"] atLeast0AtMost cong: if_cong)
  7.1129 +      done
  7.1130 +  qed
  7.1131 +  then show ?thesis
  7.1132 +    using simplical_face_in_standard_simplex assms
  7.1133 +    by (auto simp: singular_face_def oriented_simplex_def restrict_def)
  7.1134 +qed
  7.1135 +
  7.1136 +lemma simplicial_simplex_singular_face:
  7.1137 +  fixes f :: "(nat \<Rightarrow> real) \<Rightarrow> nat \<Rightarrow> real"
  7.1138 +  assumes ss: "simplicial_simplex p S f" and p: "1 \<le> p" "k \<le> p"
  7.1139 +  shows "simplicial_simplex (p - Suc 0) S (singular_face p k f)"
  7.1140 +proof -
  7.1141 +  let ?X = "subtopology (powertop_real UNIV) S"
  7.1142 +  obtain m where l: "singular_simplex p ?X (oriented_simplex p m)"
  7.1143 +       and feq: "f = oriented_simplex p m"
  7.1144 +    using assms by (force simp: simplicial_simplex_def)
  7.1145 +  moreover have "\<exists>l. singular_face p k f = oriented_simplex (p - Suc 0) l"
  7.1146 +    apply (simp add: feq singular_face_def oriented_simplex_def)
  7.1147 +    apply (simp add: simplical_face_in_standard_simplex [OF p] restrict_compose_left subset_eq)
  7.1148 +    apply (rule_tac x="\<lambda>i. if i < k then m i else m (Suc i)" in exI)
  7.1149 +    using sum_zero_middle [OF p, where 'a=real, symmetric]  unfolding simplical_face_def o_def
  7.1150 +    apply (simp add: if_distrib [of "\<lambda>x. _ * x"] if_distrib [of "\<lambda>f. f _ * _"] atLeast0AtMost cong: if_cong)
  7.1151 +    done
  7.1152 +  ultimately
  7.1153 +  show ?thesis
  7.1154 +    using assms by (simp add: singular_simplex_singular_face simplicial_simplex_def)
  7.1155 +qed
  7.1156 +
  7.1157 +lemma simplicial_chain_boundary:
  7.1158 +   "simplicial_chain p S c \<Longrightarrow> simplicial_chain (p -1) S (chain_boundary p c)"
  7.1159 +  unfolding simplicial_chain_def
  7.1160 +proof (induction rule: frag_induction)
  7.1161 +  case (one f)
  7.1162 +  then have "simplicial_simplex p S f"
  7.1163 +    by simp
  7.1164 +  have "simplicial_chain (p - Suc 0) S (frag_of (singular_face p i f))"
  7.1165 +    if "0 < p" "i \<le> p" for i
  7.1166 +    using that one
  7.1167 +    apply (simp add: simplicial_simplex_def singular_simplex_singular_face)
  7.1168 +    apply (force simp: singular_face_oriented_simplex)
  7.1169 +    done
  7.1170 +  then have "simplicial_chain (p - Suc 0) S (chain_boundary p (frag_of f))"
  7.1171 +    unfolding chain_boundary_def frag_extend_of
  7.1172 +    by (auto intro!: simplicial_chain_cmul simplicial_chain_sum)
  7.1173 +  then show ?case
  7.1174 +    by (simp add: simplicial_chain_def [symmetric])
  7.1175 +next
  7.1176 +  case (diff a b)
  7.1177 +  then show ?case
  7.1178 +    by (metis chain_boundary_diff simplicial_chain_def simplicial_chain_diff)
  7.1179 +qed auto
  7.1180 +
  7.1181 +
  7.1182 +subsection\<open>The cone construction on simplicial simplices.\<close>
  7.1183 +
  7.1184 +consts simplex_cone :: "[nat, nat \<Rightarrow> real, [nat \<Rightarrow> real, nat] \<Rightarrow> real, nat \<Rightarrow> real, nat] \<Rightarrow> real"
  7.1185 +specification (simplex_cone)
  7.1186 +  simplex_cone:
  7.1187 +    "\<And>p v l. simplex_cone p v (oriented_simplex p l) =
  7.1188 +          oriented_simplex (Suc p) (\<lambda>i. if i = 0 then v else l(i -1))"
  7.1189 +proof -
  7.1190 +  have *: "\<And>x. \<exists>y. \<forall>v. (\<lambda>l. oriented_simplex (Suc x) (\<lambda>i. if i = 0 then v else l (i -1)))
  7.1191 +                  = (y v \<circ> (oriented_simplex x))"
  7.1192 +    apply (subst choice_iff [symmetric])
  7.1193 +    apply (subst function_factors_left [symmetric])
  7.1194 +    by (simp add: oriented_simplex_eq)
  7.1195 +  then show ?thesis
  7.1196 +    apply (subst choice_iff [symmetric])
  7.1197 +    apply (subst fun_eq_iff [symmetric])
  7.1198 +    unfolding o_def
  7.1199 +    apply (blast intro: sym)
  7.1200 +    done
  7.1201 +qed
  7.1202 +
  7.1203 +lemma simplicial_simplex_simplex_cone:
  7.1204 +  assumes f: "simplicial_simplex p S f"
  7.1205 +    and T: "\<And>x u. \<lbrakk>0 \<le> u; u \<le> 1; x \<in> S\<rbrakk> \<Longrightarrow> (\<lambda>i. (1 - u) * v i + u * x i) \<in> T"
  7.1206 +  shows "simplicial_simplex (Suc p) T (simplex_cone p v f)"
  7.1207 +proof -
  7.1208 +  obtain l where l: "\<And>x. x \<in> standard_simplex p \<Longrightarrow> oriented_simplex p l x \<in> S"
  7.1209 +    and feq: "f = oriented_simplex p l"
  7.1210 +    using f by (auto simp: simplicial_simplex)
  7.1211 +  have "oriented_simplex p l x \<in> S" if "x \<in> standard_simplex p" for x
  7.1212 +    using f that by (auto simp: simplicial_simplex feq)
  7.1213 +  then have S: "\<And>x. \<lbrakk>\<And>i. 0 \<le> x i \<and> x i \<le> 1; \<And>i. i>p \<Longrightarrow> x i = 0; sum x {..p} = 1\<rbrakk>
  7.1214 +                 \<Longrightarrow> (\<lambda>i. \<Sum>j\<le>p. l j i * x j) \<in> S"
  7.1215 +    by (simp add: oriented_simplex_def standard_simplex_def)
  7.1216 +  have "oriented_simplex (Suc p) (\<lambda>i. if i = 0 then v else l (i -1)) x \<in> T"
  7.1217 +    if "x \<in> standard_simplex (Suc p)" for x
  7.1218 +  proof (simp add: that oriented_simplex_def sum_atMost_Suc_shift del: sum_atMost_Suc)
  7.1219 +    have x01: "\<And>i. 0 \<le> x i \<and> x i \<le> 1" and x0: "\<And>i. i > Suc p \<Longrightarrow> x i = 0" and x1: "sum x {..Suc p} = 1"
  7.1220 +      using that by (auto simp: oriented_simplex_def standard_simplex_def)
  7.1221 +    obtain a where "a \<in> S"
  7.1222 +      using f by force
  7.1223 +    show "(\<lambda>i. v i * x 0 + (\<Sum>j\<le>p. l j i * x (Suc j))) \<in> T"
  7.1224 +    proof (cases "x 0 = 1")
  7.1225 +      case True
  7.1226 +      then have "sum x {Suc 0..Suc p} = 0"
  7.1227 +        using x1 by (simp add: atMost_atLeast0 sum_head_Suc)
  7.1228 +      then have [simp]: "x (Suc j) = 0" if "j\<le>p" for j
  7.1229 +        unfolding sum.atLeast_Suc_atMost_Suc_shift
  7.1230 +        using x01 that by (simp add: sum_nonneg_eq_0_iff)
  7.1231 +      then show ?thesis
  7.1232 +        using T [of 0 a] \<open>a \<in> S\<close> by (auto simp: True)
  7.1233 +    next
  7.1234 +      case False
  7.1235 +      then have "(\<lambda>i. v i * x 0 + (\<Sum>j\<le>p. l j i * x (Suc j))) = (\<lambda>i. (1 - (1 - x 0)) * v i + (1 - x 0) * (inverse (1 - x 0) * (\<Sum>j\<le>p. l j i * x (Suc j))))"
  7.1236 +        by (force simp: field_simps)
  7.1237 +      also have "\<dots> \<in> T"
  7.1238 +      proof (rule T)
  7.1239 +        have "x 0 < 1"
  7.1240 +          by (simp add: False less_le x01)
  7.1241 +        have xle: "x (Suc i) \<le> (1 - x 0)" for i
  7.1242 +        proof (cases "i \<le> p")
  7.1243 +          case True
  7.1244 +          have "sum x {0, Suc i} \<le> sum x {..Suc p}"
  7.1245 +            by (rule sum_mono2) (auto simp: True x01)
  7.1246 +          then show ?thesis
  7.1247 +           using x1 x01 by (simp add: algebra_simps not_less)
  7.1248 +        qed (simp add: x0 x01)
  7.1249 +        have "(\<lambda>i. (\<Sum>j\<le>p. l j i * (x (Suc j) * inverse (1 - x 0)))) \<in> S"
  7.1250 +        proof (rule S)
  7.1251 +          have "x 0 + (\<Sum>j\<le>p. x (Suc j)) = sum x {..Suc p}"
  7.1252 +            by (metis sum_atMost_Suc_shift)
  7.1253 +          with x1 have "(\<Sum>j\<le>p. x (Suc j)) = 1 - x 0"
  7.1254 +            by simp
  7.1255 +          with False show "(\<Sum>j\<le>p. x (Suc j) * inverse (1 - x 0)) = 1"
  7.1256 +            by (metis add_diff_cancel_left' diff_diff_eq2 diff_zero right_inverse sum_distrib_right)
  7.1257 +      qed (use x01 x0 xle \<open>x 0 < 1\<close> in \<open>auto simp: divide_simps\<close>)
  7.1258 +      then show "(\<lambda>i. inverse (1 - x 0) * (\<Sum>j\<le>p. l j i * x (Suc j))) \<in> S"
  7.1259 +        by (simp add: field_simps sum_divide_distrib)
  7.1260 +    qed (use x01 in auto)
  7.1261 +    finally show ?thesis .
  7.1262 +  qed
  7.1263 +qed
  7.1264 +  then show ?thesis
  7.1265 +    by (auto simp: simplicial_simplex feq  simplex_cone)
  7.1266 +qed
  7.1267 +
  7.1268 +definition simplicial_cone
  7.1269 +  where "simplicial_cone p v \<equiv> frag_extend (frag_of \<circ> simplex_cone p v)"
  7.1270 +
  7.1271 +lemma simplicial_chain_simplicial_cone:
  7.1272 +  assumes c: "simplicial_chain p S c"
  7.1273 +    and T: "\<And>x u. \<lbrakk>0 \<le> u; u \<le> 1; x \<in> S\<rbrakk> \<Longrightarrow> (\<lambda>i. (1 - u) * v i + u * x i) \<in> T"
  7.1274 +  shows "simplicial_chain (Suc p) T (simplicial_cone p v c)"
  7.1275 +  using c unfolding simplicial_chain_def simplicial_cone_def
  7.1276 +proof (induction rule: frag_induction)
  7.1277 +  case (one x)
  7.1278 +  then show ?case
  7.1279 +    by (simp add: T simplicial_simplex_simplex_cone)
  7.1280 +next
  7.1281 +  case (diff a b)
  7.1282 +  then show ?case
  7.1283 +    by (metis frag_extend_diff simplicial_chain_def simplicial_chain_diff)
  7.1284 +qed auto
  7.1285 +
  7.1286 +
  7.1287 +lemma chain_boundary_simplicial_cone_of':
  7.1288 +  assumes "f = oriented_simplex p l"
  7.1289 +  shows "chain_boundary (Suc p) (simplicial_cone p v (frag_of f)) =
  7.1290 +         frag_of f
  7.1291 +         - (if p = 0 then frag_of (\<lambda>u\<in>standard_simplex p. v)
  7.1292 +            else simplicial_cone (p -1) v (chain_boundary p (frag_of f)))"
  7.1293 +proof (simp, intro impI conjI)
  7.1294 +  assume "p = 0"
  7.1295 +  have eq: "(oriented_simplex 0 (\<lambda>j. if j = 0 then v else l j)) = (\<lambda>u\<in>standard_simplex 0. v)"
  7.1296 +    by (force simp: oriented_simplex_def standard_simplex_def)
  7.1297 +  show "chain_boundary (Suc 0) (simplicial_cone 0 v (frag_of f))
  7.1298 +        = frag_of f - frag_of (\<lambda>u\<in>standard_simplex 0. v)"
  7.1299 +    by (simp add: assms simplicial_cone_def chain_boundary_of \<open>p = 0\<close> simplex_cone singular_face_oriented_simplex eq cong: if_cong)
  7.1300 +next
  7.1301 +  assume "0 < p"
  7.1302 +  have 0: "simplex_cone (p - Suc 0) v (singular_face p x (oriented_simplex p l))
  7.1303 +         = oriented_simplex p
  7.1304 +              (\<lambda>j. if j < Suc x
  7.1305 +                   then if j = 0 then v else l (j -1)
  7.1306 +                   else if Suc j = 0 then v else l (Suc j -1))" if "x \<le> p" for x
  7.1307 +    using \<open>0 < p\<close> that
  7.1308 +    by (auto simp: Suc_leI singular_face_oriented_simplex simplex_cone oriented_simplex_eq)
  7.1309 +  have 1: "frag_extend (frag_of \<circ> simplex_cone (p - Suc 0) v)
  7.1310 +                     (\<Sum>k = 0..p. frag_cmul ((-1) ^ k) (frag_of (singular_face p k (oriented_simplex p l))))
  7.1311 +         = - (\<Sum>k = Suc 0..Suc p. frag_cmul ((-1) ^ k)
  7.1312 +               (frag_of (singular_face (Suc p) k (simplex_cone p v (oriented_simplex p l)))))"
  7.1313 +    apply (subst sum.atLeast_Suc_atMost_Suc_shift)
  7.1314 +    apply (simp add: frag_extend_sum frag_extend_cmul flip: sum_negf)
  7.1315 +    apply (auto simp: simplex_cone singular_face_oriented_simplex 0 intro: sum.cong)
  7.1316 +    done
  7.1317 +  moreover have 2: "singular_face (Suc p) 0 (simplex_cone p v (oriented_simplex p l))
  7.1318 +                    = oriented_simplex p l"
  7.1319 +    by (simp add: simplex_cone singular_face_oriented_simplex)
  7.1320 +  show "chain_boundary (Suc p) (simplicial_cone p v (frag_of f))
  7.1321 +        = frag_of f - simplicial_cone (p - Suc 0) v (chain_boundary p (frag_of f))"
  7.1322 +    using \<open>p > 0\<close>
  7.1323 +    apply (simp add: assms simplicial_cone_def chain_boundary_of atMost_atLeast0 del: sum_atMost_Suc)
  7.1324 +    apply (subst sum_head_Suc [of 0])
  7.1325 +     apply (simp_all add: 1 2 del: sum_atMost_Suc)
  7.1326 +    done
  7.1327 +qed
  7.1328 +
  7.1329 +lemma chain_boundary_simplicial_cone_of:
  7.1330 +  assumes "simplicial_simplex p S f"
  7.1331 +  shows "chain_boundary (Suc p) (simplicial_cone p v (frag_of f)) =
  7.1332 +         frag_of f
  7.1333 +         - (if p = 0 then frag_of (\<lambda>u\<in>standard_simplex p. v)
  7.1334 +            else simplicial_cone (p -1) v (chain_boundary p (frag_of f)))"
  7.1335 +  using chain_boundary_simplicial_cone_of' assms unfolding simplicial_simplex_def
  7.1336 +  by blast
  7.1337 +
  7.1338 +lemma chain_boundary_simplicial_cone:
  7.1339 +  "simplicial_chain p S c
  7.1340 +   \<Longrightarrow> chain_boundary (Suc p) (simplicial_cone p v c) =
  7.1341 +       c - (if p = 0 then frag_extend (\<lambda>f. frag_of (\<lambda>u\<in>standard_simplex p. v)) c
  7.1342 +            else simplicial_cone (p -1) v (chain_boundary p c))"
  7.1343 +  unfolding simplicial_chain_def
  7.1344 +proof (induction rule: frag_induction)
  7.1345 +  case (one x)
  7.1346 +  then show ?case
  7.1347 +    by (auto simp: chain_boundary_simplicial_cone_of)
  7.1348 +qed (auto simp: chain_boundary_diff simplicial_cone_def frag_extend_diff)
  7.1349 +
  7.1350 +lemma simplex_map_oriented_simplex:
  7.1351 +  assumes l: "simplicial_simplex p (standard_simplex q) (oriented_simplex p l)"
  7.1352 +    and g: "simplicial_simplex r S g" and "q \<le> r"
  7.1353 +  shows "simplex_map p g (oriented_simplex p l) = oriented_simplex p (g \<circ> l)"
  7.1354 +proof -
  7.1355 +  obtain m where geq: "g = oriented_simplex r m"
  7.1356 +    using g by (auto simp: simplicial_simplex_def)
  7.1357 +  have "g (\<lambda>i. \<Sum>j\<le>p. l j i * x j) i = (\<Sum>j\<le>p. g (l j) i * x j)"
  7.1358 +    if "x \<in> standard_simplex p" for x i
  7.1359 +  proof -
  7.1360 +    have ssr: "(\<lambda>i. \<Sum>j\<le>p. l j i * x j) \<in> standard_simplex r"
  7.1361 +      using l that standard_simplex_mono [OF \<open>q \<le> r\<close>]
  7.1362 +      unfolding simplicial_simplex_oriented_simplex by auto
  7.1363 +    have lss: "l j \<in> standard_simplex r" if "j\<le>p" for j
  7.1364 +    proof -
  7.1365 +      have q: "(\<lambda>x i. \<Sum>j\<le>p. l j i * x j) ` standard_simplex p \<subseteq> standard_simplex q"
  7.1366 +        using l by (simp add: simplicial_simplex_oriented_simplex)
  7.1367 +      have p: "l j \<in> (\<lambda>x i. \<Sum>j\<le>p. l j i * x j) ` standard_simplex p"
  7.1368 +        apply (rule_tac x="(\<lambda>i. if i = j then 1 else 0)" in rev_image_eqI)
  7.1369 +        using \<open>j\<le>p\<close> by (force simp: basis_in_standard_simplex if_distrib cong: if_cong)+
  7.1370 +      show ?thesis
  7.1371 +        apply (rule subsetD [OF standard_simplex_mono [OF \<open>q \<le> r\<close>]])
  7.1372 +        apply (rule subsetD [OF q p])
  7.1373 +        done
  7.1374 +    qed
  7.1375 +    show ?thesis
  7.1376 +      apply (simp add: geq oriented_simplex_def sum_distrib_left sum_distrib_right mult.assoc ssr lss)
  7.1377 +      by (rule sum.swap)
  7.1378 +  qed
  7.1379 +  then show ?thesis
  7.1380 +    by (force simp: oriented_simplex_def simplex_map_def o_def)
  7.1381 +qed
  7.1382 +
  7.1383 +
  7.1384 +lemma chain_map_simplicial_cone:
  7.1385 +  assumes g: "simplicial_simplex r S g"
  7.1386 +      and c: "simplicial_chain p (standard_simplex q) c"
  7.1387 +      and v: "v \<in> standard_simplex q" and "q \<le> r"
  7.1388 +  shows "chain_map (Suc p) g (simplicial_cone p v c) = simplicial_cone p (g v) (chain_map p g c)"
  7.1389 +proof -
  7.1390 +  have *: "simplex_map (Suc p) g (simplex_cone p v f) = simplex_cone p (g v) (simplex_map p g f)"
  7.1391 +    if "f \<in> Poly_Mapping.keys c" for f
  7.1392 +  proof -
  7.1393 +    have "simplicial_simplex p (standard_simplex q) f"
  7.1394 +      using c that by (auto simp: simplicial_chain_def)
  7.1395 +    then obtain m where feq: "f = oriented_simplex p m"
  7.1396 +      by (auto simp: simplicial_simplex)
  7.1397 +    have 0: "simplicial_simplex p (standard_simplex q) (oriented_simplex p m)"
  7.1398 +      using \<open>simplicial_simplex p (standard_simplex q) f\<close> feq by blast
  7.1399 +    then have 1: "simplicial_simplex (Suc p) (standard_simplex q)
  7.1400 +                      (oriented_simplex (Suc p) (\<lambda>i. if i = 0 then v else m (i -1)))"
  7.1401 +      using convex_standard_simplex v
  7.1402 +      by (simp flip: simplex_cone add: simplicial_simplex_simplex_cone)
  7.1403 +    show ?thesis
  7.1404 +      using simplex_map_oriented_simplex [OF 1 g \<open>q \<le> r\<close>]
  7.1405 +            simplex_map_oriented_simplex [of p q m r S g, OF 0 g \<open>q \<le> r\<close>]
  7.1406 +      by (simp add: feq oriented_simplex_eq simplex_cone)
  7.1407 +  qed
  7.1408 +  show ?thesis
  7.1409 +    by (auto simp: chain_map_def simplicial_cone_def frag_extend_compose * intro: frag_extend_eq)
  7.1410 +qed
  7.1411 +
  7.1412 +
  7.1413 +subsection\<open>Barycentric subdivision of a linear ("simplicial") simplex's image\<close>
  7.1414 +
  7.1415 +definition simplicial_vertex
  7.1416 +  where "simplicial_vertex i f = f(\<lambda>j. if j = i then 1 else 0)"
  7.1417 +
  7.1418 +lemma simplicial_vertex_oriented_simplex:
  7.1419 +   "simplicial_vertex i (oriented_simplex p l) = (if i \<le> p then l i else undefined)"
  7.1420 +  by (simp add: simplicial_vertex_def oriented_simplex_def if_distrib cong: if_cong)
  7.1421 +
  7.1422 +
  7.1423 +primrec simplicial_subdivision
  7.1424 +where
  7.1425 +  "simplicial_subdivision 0 = id"
  7.1426 +| "simplicial_subdivision (Suc p) =
  7.1427 +     frag_extend
  7.1428 +      (\<lambda>f. simplicial_cone p
  7.1429 +            (\<lambda>i. (\<Sum>j\<le>Suc p. simplicial_vertex j f i) / (p + 2))
  7.1430 +            (simplicial_subdivision p (chain_boundary (Suc p) (frag_of f))))"
  7.1431 +
  7.1432 +
  7.1433 +lemma simplicial_subdivision_0 [simp]:
  7.1434 +   "simplicial_subdivision p 0 = 0"
  7.1435 +  by (induction p) auto
  7.1436 +
  7.1437 +lemma simplicial_subdivision_diff:
  7.1438 +   "simplicial_subdivision p (c1-c2) = simplicial_subdivision p c1 - simplicial_subdivision p c2"
  7.1439 +  by (induction p) (auto simp: frag_extend_diff)
  7.1440 +
  7.1441 +lemma simplicial_subdivision_of:
  7.1442 +   "simplicial_subdivision p (frag_of f) =
  7.1443 +         (if p = 0 then frag_of f
  7.1444 +         else simplicial_cone (p -1)
  7.1445 +               (\<lambda>i. (\<Sum>j\<le>p. simplicial_vertex j f i) / (Suc p))
  7.1446 +               (simplicial_subdivision (p -1) (chain_boundary p (frag_of f))))"
  7.1447 +  by (induction p) (auto simp: add.commute)
  7.1448 +
  7.1449 +
  7.1450 +lemma simplicial_chain_simplicial_subdivision:
  7.1451 +   "simplicial_chain p S c
  7.1452 +           \<Longrightarrow> simplicial_chain p S (simplicial_subdivision p c)"
  7.1453 +proof (induction p arbitrary: S c)
  7.1454 +  case (Suc p)
  7.1455 +  show ?case
  7.1456 +    using Suc.prems [unfolded simplicial_chain_def]
  7.1457 +  proof (induction c rule: frag_induction)
  7.1458 +    case (one f)
  7.1459 +    then have f: "simplicial_simplex (Suc p) S f"
  7.1460 +      by auto
  7.1461 +    then have "simplicial_chain p (f ` standard_simplex (Suc p))
  7.1462 +                 (simplicial_subdivision p (chain_boundary (Suc p) (frag_of f)))"
  7.1463 +      by (metis Suc.IH diff_Suc_1 simplicial_chain_boundary simplicial_chain_of simplicial_simplex subsetI)
  7.1464 +    moreover
  7.1465 +    obtain l where l: "\<And>x. x \<in> standard_simplex (Suc p) \<Longrightarrow> (\<lambda>i. (\<Sum>j\<le>Suc p. l j i * x j)) \<in> S"
  7.1466 +      and feq: "f = oriented_simplex (Suc p) l"
  7.1467 +      using f by (fastforce simp: simplicial_simplex oriented_simplex_def simp del: sum_atMost_Suc)
  7.1468 +    have "(\<lambda>i. (1 - u) * ((\<Sum>j\<le>Suc p. simplicial_vertex j f i) / (real p + 2)) + u * y i) \<in> S"
  7.1469 +      if "0 \<le> u" "u \<le> 1" and y: "y \<in> f ` standard_simplex (Suc p)" for y u
  7.1470 +    proof -
  7.1471 +      obtain x where x: "x \<in> standard_simplex (Suc p)" and yeq: "y = oriented_simplex (Suc p) l x"
  7.1472 +        using y feq by blast
  7.1473 +      have "(\<lambda>i. \<Sum>j\<le>Suc p. l j i * ((if j \<le> Suc p then (1 - u) * inverse (p + 2) + u * x j else 0))) \<in> S"
  7.1474 +      proof (rule l)
  7.1475 +        have i2p: "inverse (2 + real p) \<le> 1"
  7.1476 +          by (simp add: divide_simps)
  7.1477 +        show "(\<lambda>j. if j \<le> Suc p then (1 - u) * inverse (real (p + 2)) + u * x j else 0) \<in> standard_simplex (Suc p)"
  7.1478 +          using x \<open>0 \<le> u\<close> \<open>u \<le> 1\<close>
  7.1479 +          apply (simp add: sum.distrib standard_simplex_def i2p linepath_le_1 flip: sum_distrib_left del: sum_atMost_Suc)
  7.1480 +          apply (simp add: divide_simps)
  7.1481 +          done
  7.1482 +      qed
  7.1483 +      moreover have "(\<lambda>i. \<Sum>j\<le>Suc p. l j i * ((1 - u) * inverse (2 + real p) + u * x j))
  7.1484 +                   = (\<lambda>i. (1 - u) * (\<Sum>j\<le>Suc p. l j i) / (real p + 2) + u * (\<Sum>j\<le>Suc p. l j i * x j))"
  7.1485 +      proof
  7.1486 +        fix i
  7.1487 +        have "(\<Sum>j\<le>Suc p. l j i * ((1 - u) * inverse (2 + real p) + u * x j))
  7.1488 +            = (\<Sum>j\<le>Suc p. (1 - u) * l j i / (real p + 2) + u * l j i * x j)" (is "?lhs = _")
  7.1489 +          by (simp add: field_simps cong: sum.cong)
  7.1490 +        also have "\<dots> = (1 - u) * (\<Sum>j\<le>Suc p. l j i) / (real p + 2) + u * (\<Sum>j\<le>Suc p. l j i * x j)" (is "_ = ?rhs")
  7.1491 +          by (simp add: sum_distrib_left sum.distrib sum_divide_distrib mult.assoc del: sum_atMost_Suc)
  7.1492 +        finally show "?lhs = ?rhs" .
  7.1493 +      qed
  7.1494 +      ultimately show ?thesis
  7.1495 +        using feq x yeq
  7.1496 +        by (simp add: simplicial_vertex_oriented_simplex) (simp add: oriented_simplex_def)
  7.1497 +    qed
  7.1498 +    ultimately show ?case
  7.1499 +      by (simp add: simplicial_chain_simplicial_cone)
  7.1500 +  next
  7.1501 +    case (diff a b)
  7.1502 +    then show ?case
  7.1503 +      by (metis simplicial_chain_diff simplicial_subdivision_diff)
  7.1504 +  qed auto
  7.1505 +qed auto
  7.1506 +
  7.1507 +lemma chain_boundary_simplicial_subdivision:
  7.1508 +   "simplicial_chain p S c
  7.1509 +    \<Longrightarrow> chain_boundary p (simplicial_subdivision p c) = simplicial_subdivision (p -1) (chain_boundary p c)"
  7.1510 +proof (induction p arbitrary: c)
  7.1511 +  case (Suc p)
  7.1512 +  show ?case
  7.1513 +    using Suc.prems [unfolded simplicial_chain_def]
  7.1514 +  proof (induction c rule: frag_induction)
  7.1515 +    case (one f)
  7.1516 +    then have f: "simplicial_simplex (Suc p) S f"
  7.1517 +      by simp
  7.1518 +    then have "simplicial_chain p S (simplicial_subdivision p (chain_boundary (Suc p) (frag_of f)))"
  7.1519 +      by (metis diff_Suc_1 simplicial_chain_boundary simplicial_chain_of simplicial_chain_simplicial_subdivision)
  7.1520 +    moreover have "simplicial_chain p S (chain_boundary (Suc p) (frag_of f))"
  7.1521 +      using one simplicial_chain_boundary simplicial_chain_of by fastforce
  7.1522 +    moreover have "simplicial_subdivision (p - Suc 0) (chain_boundary p (chain_boundary (Suc p) (frag_of f))) = 0"
  7.1523 +      by (metis f chain_boundary_boundary_alt simplicial_simplex_def simplicial_subdivision_0 singular_chain_of)
  7.1524 +    ultimately show ?case
  7.1525 +      apply (simp add: chain_boundary_simplicial_cone Suc)
  7.1526 +       apply (auto simp: chain_boundary_of frag_extend_diff simplicial_cone_def)
  7.1527 +      done
  7.1528 +  next
  7.1529 +    case (diff a b)
  7.1530 +    then show ?case
  7.1531 +      by (simp add: simplicial_subdivision_diff chain_boundary_diff frag_extend_diff)
  7.1532 +  qed auto
  7.1533 +qed auto
  7.1534 +
  7.1535 +
  7.1536 +(*A MESS AND USED ONLY ONCE*)
  7.1537 +lemma simplicial_subdivision_shrinks:
  7.1538 +   "\<lbrakk>simplicial_chain p S c;
  7.1539 +     \<And>f x y. \<lbrakk>f \<in> Poly_Mapping.keys c; x \<in> standard_simplex p; y \<in> standard_simplex p\<rbrakk> \<Longrightarrow> \<bar>f x k - f y k\<bar> \<le> d;
  7.1540 +     f \<in> Poly_Mapping.keys(simplicial_subdivision p c);
  7.1541 +     x \<in> standard_simplex p; y \<in> standard_simplex p\<rbrakk>
  7.1542 +    \<Longrightarrow> \<bar>f x k - f y k\<bar> \<le> (p / (Suc p)) * d"
  7.1543 +proof (induction p arbitrary: d c f x y)
  7.1544 +  case (Suc p)
  7.1545 +  define Sigp where "Sigp \<equiv> \<lambda>f:: (nat \<Rightarrow> real) \<Rightarrow> nat \<Rightarrow> real. \<lambda>i. (\<Sum>j\<le>Suc p. simplicial_vertex j f i) / real (p + 2)"
  7.1546 +  let ?CB = "\<lambda>f. chain_boundary (Suc p) (frag_of f)"
  7.1547 +  have *: "Poly_Mapping.keys
  7.1548 +             (simplicial_cone p (Sigp f)
  7.1549 +               (simplicial_subdivision p (?CB f)))
  7.1550 +           \<subseteq> {f. \<forall>x\<in>standard_simplex (Suc p). \<forall>y\<in>standard_simplex (Suc p).
  7.1551 +                      \<bar>f x k - f y k\<bar> \<le> real (Suc p) / real (Suc p + 1) * d}" (is "?lhs \<subseteq> ?rhs")
  7.1552 +    if f: "f \<in> Poly_Mapping.keys c" for f
  7.1553 +  proof -
  7.1554 +    have ssf: "simplicial_simplex (Suc p) S f"
  7.1555 +      using Suc.prems(1) simplicial_chain_def that by auto
  7.1556 +    have 2: "\<And>x y. \<lbrakk>x \<in> standard_simplex (Suc p); y \<in> standard_simplex (Suc p)\<rbrakk> \<Longrightarrow> \<bar>f x k - f y k\<bar> \<le> d"
  7.1557 +      by (meson Suc.prems(2) f subsetD le_Suc_eq order_refl standard_simplex_mono)
  7.1558 +    have sub: "Poly_Mapping.keys ((frag_of \<circ> simplex_cone p (Sigp f)) g) \<subseteq> ?rhs"
  7.1559 +      if "g \<in> Poly_Mapping.keys (simplicial_subdivision p (?CB f))" for g
  7.1560 +    proof -
  7.1561 +      have 1: "simplicial_chain p S (?CB f)"
  7.1562 +        using ssf simplicial_chain_boundary simplicial_chain_of by fastforce
  7.1563 +      have "simplicial_chain (Suc p) (f ` standard_simplex(Suc p)) (frag_of f)"
  7.1564 +        by (metis simplicial_chain_of simplicial_simplex ssf subset_refl)
  7.1565 +      then have sc_sub: "Poly_Mapping.keys (?CB f)
  7.1566 +                         \<subseteq> Collect (simplicial_simplex p (f ` standard_simplex (Suc p)))"
  7.1567 +        by (metis diff_Suc_1 simplicial_chain_boundary simplicial_chain_def)
  7.1568 +      have led: "\<And>h x y. \<lbrakk>h \<in> Poly_Mapping.keys (chain_boundary (Suc p) (frag_of f));
  7.1569 +                          x \<in> standard_simplex p; y \<in> standard_simplex p\<rbrakk> \<Longrightarrow> \<bar>h x k - h y k\<bar> \<le> d"
  7.1570 +        using Suc.prems(2) f sc_sub
  7.1571 +        by (simp add: simplicial_simplex subset_iff image_iff) metis
  7.1572 +      have "\<And>f' x y. \<lbrakk>f' \<in> Poly_Mapping.keys (simplicial_subdivision p (?CB f)); x \<in> standard_simplex p; y \<in> standard_simplex p\<rbrakk>
  7.1573 +            \<Longrightarrow> \<bar>f' x k - f' y k\<bar> \<le> (p / (Suc p)) * d"
  7.1574 +        by (blast intro: led Suc.IH [of "chain_boundary (Suc p) (frag_of f)", OF 1])
  7.1575 +      then have g: "\<And>x y. \<lbrakk>x \<in> standard_simplex p; y \<in> standard_simplex p\<rbrakk> \<Longrightarrow> \<bar>g x k - g y k\<bar> \<le> (p / (Suc p)) * d"
  7.1576 +        using that by blast
  7.1577 +      have "d \<ge> 0"
  7.1578 +        using Suc.prems(2)[OF f] \<open>x \<in> standard_simplex (Suc p)\<close> by force
  7.1579 +      have 3: "simplex_cone p (Sigp f) g \<in> ?rhs"
  7.1580 +      proof -
  7.1581 +        have "simplicial_simplex p (f ` standard_simplex(Suc p)) g"
  7.1582 +          by (metis (mono_tags, hide_lams) sc_sub mem_Collect_eq simplicial_chain_def simplicial_chain_simplicial_subdivision subsetD that)
  7.1583 +        then obtain m where m: "g ` standard_simplex p \<subseteq> f ` standard_simplex (Suc p)"
  7.1584 +          and geq: "g = oriented_simplex p m"
  7.1585 +          using ssf by (auto simp: simplicial_simplex)
  7.1586 +        have m_in_gim: "\<And>i. i \<le> p \<Longrightarrow> m i \<in> g ` standard_simplex p"
  7.1587 +          apply (rule_tac x = "\<lambda>j. if j = i then 1 else 0" in image_eqI)
  7.1588 +           apply (simp_all add: geq oriented_simplex_def if_distrib cong: if_cong)
  7.1589 +          done
  7.1590 +        obtain l where l: "f ` standard_simplex (Suc p) \<subseteq> S"
  7.1591 +          and feq: "f = oriented_simplex (Suc p) l"
  7.1592 +          using ssf by (auto simp: simplicial_simplex)
  7.1593 +        show ?thesis
  7.1594 +        proof (clarsimp simp add: geq simp del: sum_atMost_Suc)
  7.1595 +          fix x y
  7.1596 +          assume x: "x \<in> standard_simplex (Suc p)" and y: "y \<in> standard_simplex (Suc p)"
  7.1597 +          then have x': "(\<forall>i. 0 \<le> x i \<and> x i \<le> 1) \<and> (\<forall>i>Suc p. x i = 0) \<and> (\<Sum>i\<le>Suc p. x i) = 1"
  7.1598 +            and y': "(\<forall>i. 0 \<le> y i \<and> y i \<le> 1) \<and> (\<forall>i>Suc p. y i = 0) \<and> (\<Sum>i\<le>Suc p. y i) = 1"
  7.1599 +            by (auto simp: standard_simplex_def)
  7.1600 +          have "\<bar>(\<Sum>j\<le>Suc p. (if j = 0 then \<lambda>i. (\<Sum>j\<le>Suc p. l j i) / (2 + real p) else m (j -1)) k * x j) -
  7.1601 +                 (\<Sum>j\<le>Suc p. (if j = 0 then \<lambda>i. (\<Sum>j\<le>Suc p. l j i) / (2 + real p) else m (j -1)) k * y j)\<bar>
  7.1602 +                \<le> (1 + real p) * d / (2 + real p)"
  7.1603 +          proof -
  7.1604 +            have zero: "\<bar>m (s - Suc 0) k - (\<Sum>j\<le>Suc p. l j k) / (2 + real p)\<bar> \<le> (1 + real p) * d / (2 + real p)"
  7.1605 +              if "0 < s" and "s \<le> Suc p" for s
  7.1606 +            proof -
  7.1607 +              have "m (s - Suc 0) \<in> f ` standard_simplex (Suc p)"
  7.1608 +                using m m_in_gim that(2) by auto
  7.1609 +              then obtain z where eq: "m (s - Suc 0) = (\<lambda>i. \<Sum>j\<le>Suc p. l j i * z j)" and z: "z \<in> standard_simplex (Suc p)"
  7.1610 +                using feq unfolding oriented_simplex_def by auto
  7.1611 +              show ?thesis
  7.1612 +                unfolding eq
  7.1613 +              proof (rule convex_sum_bound_le)
  7.1614 +                fix i
  7.1615 +                assume i: "i \<in> {..Suc p}"
  7.1616 +                then have [simp]: "card ({..Suc p} - {i}) = Suc p"
  7.1617 +                  by (simp add: card_Suc_Diff1)
  7.1618 +                have "(\<Sum>j\<le>Suc p. \<bar>l i k / (p + 2) - l j k / (p + 2)\<bar>) = (\<Sum>j\<le>Suc p. \<bar>l i k - l j k\<bar> / (p + 2))"
  7.1619 +                  by (rule sum.cong) (simp_all add: flip: diff_divide_distrib)
  7.1620 +                also have "\<dots> = (\<Sum>j \<in> {..Suc p} - {i}. \<bar>l i k - l j k\<bar> / (p + 2))"
  7.1621 +                  by (rule sum.mono_neutral_right) auto
  7.1622 +                also have "\<dots> \<le> (1 + real p) * d / (p + 2)"
  7.1623 +                proof (rule sum_bounded_above_divide)
  7.1624 +                  fix i' :: "nat"
  7.1625 +                  assume i': "i' \<in> {..Suc p} - {i}"
  7.1626 +                  have lf: "\<And>r. r \<le> Suc p \<Longrightarrow> l r \<in> f ` standard_simplex(Suc p)"
  7.1627 +                    apply (rule_tac x="\<lambda>j. if j = r then 1 else 0" in image_eqI)
  7.1628 +                     apply (auto simp: feq oriented_simplex_def if_distrib [of "\<lambda>x. _ * x"] cong: if_cong)
  7.1629 +                    done
  7.1630 +                  show "\<bar>l i k - l i' k\<bar> / real (p + 2) \<le> (1 + real p) * d / real (p + 2) / real (card ({..Suc p} - {i}))"
  7.1631 +                    using i i' lf [of i] lf [of i'] 2
  7.1632 +                    by (auto simp: divide_simps image_iff)
  7.1633 +                qed auto
  7.1634 +                finally have "(\<Sum>j\<le>Suc p. \<bar>l i k / (p + 2) - l j k / (p + 2)\<bar>) \<le> (1 + real p) * d / (p + 2)" .
  7.1635 +                then have "\<bar>\<Sum>j\<le>Suc p. l i k / (p + 2) - l j k / (p + 2)\<bar> \<le> (1 + real p) * d / (p + 2)"
  7.1636 +                  by (rule order_trans [OF sum_abs])
  7.1637 +                then show "\<bar>l i k - (\<Sum>j\<le>Suc p. l j k) / (2 + real p)\<bar> \<le> (1 + real p) * d / (2 + real p)"
  7.1638 +                  by (simp add: sum_subtractf sum_divide_distrib del: sum_atMost_Suc)
  7.1639 +              qed (use standard_simplex_def z in auto)
  7.1640 +            qed
  7.1641 +            have nonz: "\<bar>m (s - Suc 0) k - m (r - Suc 0) k\<bar> \<le> (1 + real p) * d / (2 + real p)" (is "?lhs \<le> ?rhs")
  7.1642 +              if "r < s" and "0 < r" and "r \<le> Suc p" and "s \<le> Suc p" for r s
  7.1643 +            proof -
  7.1644 +              have "?lhs \<le> (p / (Suc p)) * d"
  7.1645 +                using m_in_gim [of "r - Suc 0"] m_in_gim [of "s - Suc 0"] that g by fastforce
  7.1646 +              also have "\<dots> \<le> ?rhs"
  7.1647 +                by (simp add: field_simps \<open>0 \<le> d\<close>)
  7.1648 +              finally show ?thesis .
  7.1649 +            qed
  7.1650 +            have jj: "j \<le> Suc p \<and> j' \<le> Suc p
  7.1651 +                \<longrightarrow> \<bar>(if j' = 0 then \<lambda>i. (\<Sum>j\<le>Suc p. l j i) / (2 + real p) else m (j' -1)) k -
  7.1652 +                     (if j = 0 then \<lambda>i. (\<Sum>j\<le>Suc p. l j i) / (2 + real p) else m (j -1)) k\<bar>
  7.1653 +                     \<le> (1 + real p) * d / (2 + real p)" for j j'
  7.1654 +              apply (rule_tac a=j and b = "j'" in linorder_less_wlog)
  7.1655 +                apply (force simp: zero nonz \<open>0 \<le> d\<close> simp del: sum_atMost_Suc)+
  7.1656 +              done
  7.1657 +            show ?thesis
  7.1658 +              apply (rule convex_sum_bound_le)
  7.1659 +              using x' apply blast
  7.1660 +              using x' apply blast
  7.1661 +              apply (subst abs_minus_commute)
  7.1662 +              apply (rule convex_sum_bound_le)
  7.1663 +              using y' apply blast
  7.1664 +              using y' apply blast
  7.1665 +              using jj by blast
  7.1666 +          qed
  7.1667 +          then show "\<bar>simplex_cone p (Sigp f) (oriented_simplex p m) x k - simplex_cone p (Sigp f) (oriented_simplex p m) y k\<bar>
  7.1668 +                \<le> (1 + real p) * d / (2 + real p)"
  7.1669 +            apply (simp add: feq Sigp_def simplicial_vertex_oriented_simplex simplex_cone del: sum_atMost_Suc)
  7.1670 +            apply (simp add: oriented_simplex_def x y del: sum_atMost_Suc)
  7.1671 +            done
  7.1672 +        qed
  7.1673 +      qed
  7.1674 +      show ?thesis
  7.1675 +        using Suc.IH [OF 1, where f=g] 2 3 by simp
  7.1676 +    qed
  7.1677 +    then show ?thesis
  7.1678 +      unfolding simplicial_chain_def simplicial_cone_def
  7.1679 +      by (simp add: order_trans [OF keys_frag_extend] sub UN_subset_iff)
  7.1680 +  qed
  7.1681 +  show ?case
  7.1682 +    using Suc
  7.1683 +    apply (simp del: sum_atMost_Suc)
  7.1684 +    apply (drule subsetD [OF keys_frag_extend])
  7.1685 +    apply (simp del: sum_atMost_Suc)
  7.1686 +    apply clarify (*OBTAIN?*)
  7.1687 +    apply (rename_tac FFF)
  7.1688 +    using *
  7.1689 +    apply (simp add: add.commute Sigp_def subset_iff)
  7.1690 +    done
  7.1691 +qed (auto simp: standard_simplex_0)
  7.1692 +
  7.1693 +
  7.1694 +subsection\<open>Singular subdivision\<close>
  7.1695 +
  7.1696 +definition singular_subdivision
  7.1697 +  where "singular_subdivision p \<equiv>
  7.1698 +        frag_extend
  7.1699 +           (\<lambda>f. chain_map p f
  7.1700 +                  (simplicial_subdivision p
  7.1701 +                         (frag_of(restrict id (standard_simplex p)))))"
  7.1702 +
  7.1703 +lemma singular_subdivision_0 [simp]: "singular_subdivision p 0 = 0"
  7.1704 +  by (simp add: singular_subdivision_def)
  7.1705 +
  7.1706 +lemma singular_subdivision_add:
  7.1707 +   "singular_subdivision p (a + b) = singular_subdivision p a + singular_subdivision p b"
  7.1708 +  by (simp add: singular_subdivision_def frag_extend_add)
  7.1709 +
  7.1710 +lemma singular_subdivision_diff:
  7.1711 +   "singular_subdivision p (a - b) = singular_subdivision p a - singular_subdivision p b"
  7.1712 +  by (simp add: singular_subdivision_def frag_extend_diff)
  7.1713 +
  7.1714 +lemma simplicial_simplex_id [simp]:
  7.1715 +   "simplicial_simplex p S (restrict id (standard_simplex p)) \<longleftrightarrow> standard_simplex p \<subseteq> S"
  7.1716 +    (is "?lhs = ?rhs")
  7.1717 +proof
  7.1718 +  assume ?lhs
  7.1719 +  then show ?rhs
  7.1720 +    by (simp add: simplicial_simplex_def singular_simplex_def continuous_map_in_subtopology set_mp)
  7.1721 +next
  7.1722 +  assume R: ?rhs
  7.1723 +  then have cm: "continuous_map
  7.1724 +                 (subtopology (powertop_real UNIV) (standard_simplex p))
  7.1725 +                 (subtopology (powertop_real UNIV) S) id"
  7.1726 +    using continuous_map_from_subtopology_mono continuous_map_id by blast
  7.1727 +  moreover have "\<exists>l. restrict id (standard_simplex p) = oriented_simplex p l"
  7.1728 +    apply (rule_tac x="\<lambda>i j. if i = j then 1 else 0" in exI)
  7.1729 +    apply (force simp: oriented_simplex_def standard_simplex_def if_distrib [of "\<lambda>u. u * _"] cong: if_cong)
  7.1730 +    done
  7.1731 +  ultimately show ?lhs
  7.1732 +    by (simp add: simplicial_simplex_def singular_simplex_def)
  7.1733 +qed
  7.1734 +
  7.1735 +lemma singular_chain_singular_subdivision:
  7.1736 +   "singular_chain p X c
  7.1737 +        \<Longrightarrow> singular_chain p X (singular_subdivision p c)"
  7.1738 +  unfolding singular_subdivision_def
  7.1739 +  apply (rule singular_chain_extend)
  7.1740 +  apply (rule singular_chain_chain_map [where X = "subtopology (powertop_real UNIV)
  7.1741 +                          (standard_simplex p)"])
  7.1742 +  apply (simp add: simplicial_chain_simplicial_subdivision simplicial_imp_singular_chain)
  7.1743 +  by (simp add: singular_chain_def singular_simplex_def subset_iff)
  7.1744 +
  7.1745 +lemma naturality_singular_subdivision:
  7.1746 +   "singular_chain p X c
  7.1747 +    \<Longrightarrow> singular_subdivision p (chain_map p g c) = chain_map p g (singular_subdivision p c)"
  7.1748 +  unfolding singular_chain_def
  7.1749 +proof (induction rule: frag_induction)
  7.1750 +  case (one f)
  7.1751 +  then have "singular_simplex p X f"
  7.1752 +    by auto
  7.1753 +  have "\<lbrakk>simplicial_chain p (standard_simplex p) d\<rbrakk>
  7.1754 +    \<Longrightarrow> chain_map p (simplex_map p g f) d = chain_map p g (chain_map p f d)" for d
  7.1755 +    unfolding simplicial_chain_def
  7.1756 +  proof (induction rule: frag_induction)
  7.1757 +    case (one x)
  7.1758 +    then have "simplex_map p (simplex_map p g f) x = simplex_map p g (simplex_map p f x)"
  7.1759 +      by (force simp: simplex_map_def restrict_compose_left simplicial_simplex)
  7.1760 +    then show ?case
  7.1761 +      by auto
  7.1762 +  qed (auto simp: chain_map_diff)
  7.1763 +  then show ?case
  7.1764 +    using simplicial_chain_simplicial_subdivision [of p "standard_simplex p" "frag_of (restrict id (standard_simplex p))"]
  7.1765 +    by (simp add: singular_subdivision_def)
  7.1766 +next
  7.1767 +  case (diff a b)
  7.1768 +  then show ?case
  7.1769 +    by (simp add: chain_map_diff singular_subdivision_diff)
  7.1770 +qed auto
  7.1771 +
  7.1772 +lemma simplicial_chain_chain_map:
  7.1773 +  assumes f: "simplicial_simplex q X f" and c: "simplicial_chain p (standard_simplex q) c"
  7.1774 +  shows "simplicial_chain p X (chain_map p f c)"
  7.1775 +  using c unfolding simplicial_chain_def
  7.1776 +proof (induction c rule: frag_induction)
  7.1777 +  case (one g)
  7.1778 +  have "\<exists>n. simplex_map p (oriented_simplex q l)
  7.1779 +                 (oriented_simplex p m) = oriented_simplex p n"
  7.1780 +    if m: "singular_simplex p
  7.1781 +                (subtopology (powertop_real UNIV) (standard_simplex q)) (oriented_simplex p m)"
  7.1782 +    for l m
  7.1783 +  proof -
  7.1784 +    have "(\<lambda>i. \<Sum>j\<le>p. m j i * x j) \<in> standard_simplex q"
  7.1785 +      if "x \<in> standard_simplex p" for x
  7.1786 +      using that m unfolding oriented_simplex_def singular_simplex_def
  7.1787 +      by (auto simp: continuous_map_in_subtopology image_subset_iff)
  7.1788 +    then show ?thesis
  7.1789 +      unfolding oriented_simplex_def simplex_map_def
  7.1790 +      apply (rule_tac x="\<lambda>j k. (\<Sum>i\<le>q. l i k * m j i)" in exI)
  7.1791 +      apply (force simp: sum_distrib_left sum_distrib_right mult.assoc intro: sum.swap)
  7.1792 +      done
  7.1793 +  qed
  7.1794 +  then show ?case
  7.1795 +    using f one
  7.1796 +    apply (auto simp: simplicial_simplex_def)
  7.1797 +    apply (rule singular_simplex_simplex_map
  7.1798 +        [where X = "subtopology (powertop_real UNIV) (standard_simplex q)"])
  7.1799 +    unfolding singular_simplex_def apply (fastforce simp add:)+
  7.1800 +    done
  7.1801 +next
  7.1802 +  case (diff a b)
  7.1803 +  then show ?case
  7.1804 +    by (metis chain_map_diff simplicial_chain_def simplicial_chain_diff)
  7.1805 +qed auto
  7.1806 +
  7.1807 +
  7.1808 +lemma singular_subdivision_simplicial_simplex:
  7.1809 +   "simplicial_chain p S c
  7.1810 +           \<Longrightarrow> singular_subdivision p c = simplicial_subdivision p c"
  7.1811 +proof (induction p arbitrary: S c)
  7.1812 +  case 0
  7.1813 +  then show ?case
  7.1814 +    unfolding simplicial_chain_def
  7.1815 +  proof (induction rule: frag_induction)
  7.1816 +    case (one x)
  7.1817 +    then show ?case
  7.1818 +      using singular_simplex_chain_map_id simplicial_imp_singular_simplex
  7.1819 +      by (fastforce simp: singular_subdivision_def simplicial_subdivision_def)
  7.1820 +  qed (auto simp: singular_subdivision_diff)
  7.1821 +next
  7.1822 +  case (Suc p)
  7.1823 +  show ?case
  7.1824 +    using Suc.prems unfolding simplicial_chain_def
  7.1825 +  proof (induction rule: frag_induction)
  7.1826 +    case (one f)
  7.1827 +    then have ssf: "simplicial_simplex (Suc p) S f"
  7.1828 +      by (auto simp: simplicial_simplex)
  7.1829 +    then have 1: "simplicial_chain p (standard_simplex (Suc p))
  7.1830 +                   (simplicial_subdivision p
  7.1831 +                     (chain_boundary (Suc p)
  7.1832 +                       (frag_of (restrict id (standard_simplex (Suc p))))))"
  7.1833 +      by (metis diff_Suc_1 order_refl simplicial_chain_boundary simplicial_chain_of simplicial_chain_simplicial_subdivision simplicial_simplex_id)
  7.1834 +    have 2: "(\<lambda>i. (\<Sum>j\<le>Suc p. simplicial_vertex j (restrict id (standard_simplex (Suc p))) i) / (real p + 2))
  7.1835 +                  \<in> standard_simplex (Suc p)"
  7.1836 +      by (simp add: simplicial_vertex_def standard_simplex_def del: sum_atMost_Suc)
  7.1837 +    have ss_Sp: "(\<lambda>i. (if i \<le> Suc p then 1 else 0) / (real p + 2)) \<in> standard_simplex (Suc p)"
  7.1838 +      by (simp add: standard_simplex_def divide_simps)
  7.1839 +    obtain l where feq: "f = oriented_simplex (Suc p) l"
  7.1840 +      using one unfolding simplicial_simplex by blast
  7.1841 +    then have 3: "f (\<lambda>i. (\<Sum>j\<le>Suc p. simplicial_vertex j (restrict id (standard_simplex (Suc p))) i) / (real p + 2))
  7.1842 +                = (\<lambda>i. (\<Sum>j\<le>Suc p. simplicial_vertex j f i) / (real p + 2))"
  7.1843 +      unfolding simplicial_vertex_def oriented_simplex_def
  7.1844 +      by (simp add: ss_Sp if_distrib [of "\<lambda>x. _ * x"] sum_divide_distrib del: sum_atMost_Suc cong: if_cong)
  7.1845 +    have scp: "singular_chain (Suc p)
  7.1846 +                 (subtopology (powertop_real UNIV) (standard_simplex (Suc p)))
  7.1847 +                 (frag_of (restrict id (standard_simplex (Suc p))))"
  7.1848 +      by (simp add: simplicial_imp_singular_chain)
  7.1849 +    have scps: "simplicial_chain p (standard_simplex (Suc p))
  7.1850 +                  (chain_boundary (Suc p) (frag_of (restrict id (standard_simplex (Suc p)))))"
  7.1851 +      by (metis diff_Suc_1 order_refl simplicial_chain_boundary simplicial_chain_of simplicial_simplex_id)
  7.1852 +    have scpf: "simplicial_chain p S
  7.1853 +                 (chain_map p f
  7.1854 +                   (chain_boundary (Suc p) (frag_of (restrict id (standard_simplex (Suc p))))))"
  7.1855 +      using scps simplicial_chain_chain_map ssf by blast
  7.1856 +    have 4: "chain_map p f
  7.1857 +                (simplicial_subdivision p
  7.1858 +                   (chain_boundary (Suc p) (frag_of (restrict id (standard_simplex (Suc p))))))
  7.1859 +           = simplicial_subdivision p (chain_boundary (Suc p) (frag_of f))"
  7.1860 +      apply (simp add: chain_boundary_chain_map [OF scp] del: chain_map_of
  7.1861 +          flip: singular_simplex_chain_map_id [OF simplicial_imp_singular_simplex [OF ssf]])
  7.1862 +      by (metis (no_types) scp singular_chain_boundary_alt Suc.IH [OF scps] Suc.IH [OF scpf] naturality_singular_subdivision)
  7.1863 +    show ?case
  7.1864 +      apply (simp add: singular_subdivision_def del: sum_atMost_Suc)
  7.1865 +      apply (simp only: ssf 1 2 3 4 chain_map_simplicial_cone [of "Suc p" S _ p "Suc p"])
  7.1866 +      done
  7.1867 +  qed (auto simp: frag_extend_diff singular_subdivision_diff)
  7.1868 +qed
  7.1869 +
  7.1870 +
  7.1871 +lemma naturality_simplicial_subdivision:
  7.1872 +   "\<lbrakk>simplicial_chain p (standard_simplex q) c; simplicial_simplex q S g\<rbrakk>
  7.1873 +    \<Longrightarrow> simplicial_subdivision p (chain_map p g c) = chain_map p g (simplicial_subdivision p c)"
  7.1874 +apply (simp flip: singular_subdivision_simplicial_simplex)
  7.1875 +  by (metis naturality_singular_subdivision simplicial_chain_chain_map simplicial_imp_singular_chain singular_subdivision_simplicial_simplex)
  7.1876 +
  7.1877 +lemma chain_boundary_singular_subdivision:
  7.1878 +   "singular_chain p X c
  7.1879 +        \<Longrightarrow> chain_boundary p (singular_subdivision p c) =
  7.1880 +            singular_subdivision (p - Suc 0) (chain_boundary p c)"
  7.1881 +  unfolding singular_chain_def
  7.1882 +proof (induction rule: frag_induction)
  7.1883 +  case (one f)
  7.1884 +    then have ssf: "singular_simplex p X f"
  7.1885 +      by (auto simp: singular_simplex_def)
  7.1886 +    then have scp: "simplicial_chain p (standard_simplex p) (frag_of (restrict id (standard_simplex p)))"
  7.1887 +      by simp
  7.1888 +    have scp1: "simplicial_chain (p - Suc 0) (standard_simplex p)
  7.1889 +                  (chain_boundary p (frag_of (restrict id (standard_simplex p))))"
  7.1890 +      using simplicial_chain_boundary by force
  7.1891 +    have sgp1: "singular_chain (p - Suc 0)
  7.1892 +                   (subtopology (powertop_real UNIV) (standard_simplex p))
  7.1893 +                   (chain_boundary p (frag_of (restrict id (standard_simplex p))))"
  7.1894 +      using scp1 simplicial_imp_singular_chain by blast
  7.1895 +    have scpp: "singular_chain p (subtopology (powertop_real UNIV) (standard_simplex p))
  7.1896 +                  (frag_of (restrict id (standard_simplex p)))"
  7.1897 +      using scp simplicial_imp_singular_chain by blast
  7.1898 +    then show ?case
  7.1899 +      unfolding singular_subdivision_def
  7.1900 +      using chain_boundary_chain_map [of p "subtopology (powertop_real UNIV)
  7.1901 +                              (standard_simplex p)" _ f]
  7.1902 +      apply (simp add: simplicial_chain_simplicial_subdivision
  7.1903 +          simplicial_imp_singular_chain chain_boundary_simplicial_subdivision [OF scp]
  7.1904 +          flip: singular_subdivision_simplicial_simplex [OF scp1] naturality_singular_subdivision [OF sgp1])
  7.1905 +      by (metis (full_types)   singular_subdivision_def  chain_boundary_chain_map [OF scpp] singular_simplex_chain_map_id [OF ssf])
  7.1906 +qed (auto simp: singular_subdivision_def frag_extend_diff chain_boundary_diff)
  7.1907 +
  7.1908 +lemma singular_subdivision_zero:
  7.1909 +  "singular_chain 0 X c \<Longrightarrow> singular_subdivision 0 c = c"
  7.1910 +  unfolding singular_chain_def
  7.1911 +proof (induction rule: frag_induction)
  7.1912 +  case (one f)
  7.1913 +  then have "restrict (f \<circ> restrict id (standard_simplex 0)) (standard_simplex 0) = f"
  7.1914 +    by (simp add: extensional_restrict restrict_compose_right singular_simplex_def)
  7.1915 +  then show ?case
  7.1916 +    by (auto simp: singular_subdivision_def simplex_map_def)
  7.1917 +qed (auto simp: singular_subdivision_def frag_extend_diff)
  7.1918 +
  7.1919 +
  7.1920 +primrec subd where
  7.1921 +  "subd 0 = (\<lambda>x. 0)"
  7.1922 +| "subd (Suc p) =
  7.1923 +      frag_extend
  7.1924 +       (\<lambda>f. simplicial_cone (Suc p) (\<lambda>i. (\<Sum>j\<le>Suc p. simplicial_vertex j f i) / real (Suc p + 1))
  7.1925 +               (simplicial_subdivision (Suc p) (frag_of f) - frag_of f -
  7.1926 +                subd p (chain_boundary (Suc p) (frag_of f))))"
  7.1927 +
  7.1928 +lemma subd_0 [simp]: "subd p 0 = 0"
  7.1929 +  by (induction p) auto
  7.1930 +
  7.1931 +lemma subd_diff [simp]: "subd p (c1 - c2) = subd p c1 - subd p c2"
  7.1932 +  by (induction p) (auto simp: frag_extend_diff)
  7.1933 +
  7.1934 +lemma subd_uminus [simp]: "subd p (-c) = - subd p c"
  7.1935 +  by (metis diff_0 subd_0 subd_diff)
  7.1936 +
  7.1937 +lemma subd_power_uminus: "subd p (frag_cmul ((-1) ^ k) c) = frag_cmul ((-1) ^ k) (subd p c)"
  7.1938 +  apply (induction k, simp_all)
  7.1939 +  by (metis minus_frag_cmul subd_uminus)
  7.1940 +
  7.1941 +lemma subd_power_sum: "subd p (sum f I) = sum (subd p \<circ> f) I"
  7.1942 +  apply (induction I rule: infinite_finite_induct)
  7.1943 +  by auto (metis add_diff_cancel_left' diff_add_cancel subd_diff)
  7.1944 +
  7.1945 +lemma subd: "simplicial_chain p (standard_simplex s) c
  7.1946 +     \<Longrightarrow> (\<forall>r g. simplicial_simplex s (standard_simplex r) g \<longrightarrow> chain_map (Suc p) g (subd p c) = subd p (chain_map p g c))
  7.1947 +         \<and> simplicial_chain (Suc p) (standard_simplex s) (subd p c)
  7.1948 +         \<and> (chain_boundary (Suc p) (subd p c)) + (subd (p - Suc 0) (chain_boundary p c)) = (simplicial_subdivision p c) - c"
  7.1949 +proof (induction p arbitrary: c)
  7.1950 +  case (Suc p)
  7.1951 +  show ?case
  7.1952 +    using Suc.prems [unfolded simplicial_chain_def]
  7.1953 +  proof (induction rule: frag_induction)
  7.1954 +    case (one f)
  7.1955 +    then obtain l where l: "(\<lambda>x i. \<Sum>j\<le>Suc p. l j i * x j) ` standard_simplex (Suc p) \<subseteq> standard_simplex s"
  7.1956 +                  and feq: "f = oriented_simplex (Suc p) l"
  7.1957 +      by (metis (mono_tags) mem_Collect_eq simplicial_simplex simplicial_simplex_oriented_simplex)
  7.1958 +    have scf: "simplicial_chain (Suc p) (standard_simplex s) (frag_of f)"
  7.1959 +      using one by simp
  7.1960 +    have lss: "l i \<in> standard_simplex s" if "i \<le> Suc p" for i
  7.1961 +    proof -
  7.1962 +      have "(\<lambda>i'. \<Sum>j\<le>Suc p. l j i' * (if j = i then 1 else 0)) \<in> standard_simplex s"
  7.1963 +        using subsetD [OF l] basis_in_standard_simplex that by blast
  7.1964 +      moreover have "(\<lambda>i'. \<Sum>j\<le>Suc p. l j i' * (if j = i then 1 else 0)) = l i"
  7.1965 +        using that by (simp add: if_distrib [of "\<lambda>x. _ * x"] del: sum_atMost_Suc cong: if_cong)
  7.1966 +      ultimately show ?thesis
  7.1967 +        by simp
  7.1968 +    qed
  7.1969 +    have *: "(\<And>i. i \<le> n \<Longrightarrow> l i \<in> standard_simplex s)
  7.1970 +     \<Longrightarrow> (\<lambda>i. (\<Sum>j\<le>n. l j i) / (Suc n)) \<in> standard_simplex s" for n
  7.1971 +    proof (induction n)
  7.1972 +      case (Suc n)
  7.1973 +      let ?x = "\<lambda>i. (1 - inverse (n + 2)) * ((\<Sum>j\<le>n. l j i) / (Suc n)) + inverse (n + 2) * l (Suc n) i"
  7.1974 +      have "?x \<in> standard_simplex s"
  7.1975 +      proof (rule convex_standard_simplex)
  7.1976 +        show "(\<lambda>i. (\<Sum>j\<le>n. l j i) / real (Suc n)) \<in> standard_simplex s"
  7.1977 +          using Suc by simp
  7.1978 +      qed (auto simp: lss Suc inverse_le_1_iff)
  7.1979 +      moreover have "?x = (\<lambda>i. (\<Sum>j\<le>Suc n. l j i) / real (Suc (Suc n)))"
  7.1980 +        by (force simp: divide_simps)
  7.1981 +      ultimately show ?case
  7.1982 +        by simp
  7.1983 +    qed auto
  7.1984 +    have **: "(\<lambda>i. (\<Sum>j\<le>Suc p. simplicial_vertex j f i) / (2 + real p)) \<in> standard_simplex s"
  7.1985 +      using * [of "Suc p"] lss by (simp add: simplicial_vertex_oriented_simplex feq)
  7.1986 +    show ?case
  7.1987 +    proof (intro conjI impI allI)
  7.1988 +      fix r g
  7.1989 +      assume g: "simplicial_simplex s (standard_simplex r) g"
  7.1990 +      then obtain m where geq: "g = oriented_simplex s m"
  7.1991 +        using simplicial_simplex by blast
  7.1992 +      have 1: "simplicial_chain (Suc p) (standard_simplex s) (simplicial_subdivision (Suc p) (frag_of f))"
  7.1993 +        by (metis mem_Collect_eq one.hyps simplicial_chain_of simplicial_chain_simplicial_subdivision)
  7.1994 +      have 2: "(\<Sum>j\<le>Suc p. \<Sum>i\<le>s. m i k * simplicial_vertex j f i)
  7.1995 +             = (\<Sum>j\<le>Suc p. simplicial_vertex j
  7.1996 +                                (simplex_map (Suc p) (oriented_simplex s m) f) k)" for k
  7.1997 +      proof (rule sum.cong [OF refl])
  7.1998 +        fix j
  7.1999 +        assume j: "j \<in> {..Suc p}"
  7.2000 +        have eq: "simplex_map (Suc p) (oriented_simplex s m) (oriented_simplex (Suc p) l)
  7.2001 +                = oriented_simplex (Suc p) (oriented_simplex s m \<circ> l)"
  7.2002 +        proof (rule simplex_map_oriented_simplex)
  7.2003 +          show "simplicial_simplex (Suc p) (standard_simplex s) (oriented_simplex (Suc p) l)"
  7.2004 +            using one by (simp add: feq flip: oriented_simplex_def)
  7.2005 +          show "simplicial_simplex s (standard_simplex r) (oriented_simplex s m)"
  7.2006 +            using g by (simp add: geq)
  7.2007 +        qed auto
  7.2008 +        show "(\<Sum>i\<le>s. m i k * simplicial_vertex j f i)
  7.2009 +            = simplicial_vertex j (simplex_map (Suc p) (oriented_simplex s m) f) k"
  7.2010 +          using one j
  7.2011 +          apply (simp add: feq eq simplicial_vertex_oriented_simplex simplicial_simplex_oriented_simplex image_subset_iff)
  7.2012 +          apply (drule_tac x="(\<lambda>i. if i = j then 1 else 0)" in bspec)
  7.2013 +           apply (auto simp: oriented_simplex_def lss)
  7.2014 +          done
  7.2015 +      qed
  7.2016 +      have 4: "chain_map (Suc p) g (subd p (chain_boundary (Suc p) (frag_of f)))
  7.2017 +             = subd p (chain_boundary (Suc p) (frag_of (simplex_map (Suc p) g f)))"
  7.2018 +        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)
  7.2019 +      show "chain_map (Suc (Suc p)) g (subd (Suc p) (frag_of f)) = subd (Suc p) (chain_map (Suc p) g (frag_of f))"
  7.2020 +        using g
  7.2021 +        apply (simp only: subd.simps frag_extend_of)
  7.2022 +        apply (subst chain_map_simplicial_cone [of s "standard_simplex r" _ "Suc p" s], assumption)
  7.2023 +           apply (intro simplicial_chain_diff)
  7.2024 +        using "1" apply auto[1]
  7.2025 +        using one.hyps apply auto[1]
  7.2026 +        apply (metis Suc.IH diff_Suc_1 mem_Collect_eq one.hyps simplicial_chain_boundary simplicial_chain_of)
  7.2027 +        using "**" apply auto[1]
  7.2028 +         apply (rule order_refl)
  7.2029 +         apply (simp only: chain_map_of frag_extend_of)
  7.2030 +        apply (rule arg_cong2 [where f = "simplicial_cone (Suc p)"])
  7.2031 +         apply (simp add: geq sum_distrib_left oriented_simplex_def ** del: sum_atMost_Suc flip: sum_divide_distrib)
  7.2032 +        using 2  apply (simp only: oriented_simplex_def sum.swap [where A = "{..s}"])
  7.2033 +        using naturality_simplicial_subdivision scf apply (fastforce simp add: 4 chain_map_diff)
  7.2034 +        done
  7.2035 +    next
  7.2036 +      have sc: "simplicial_chain (Suc p) (standard_simplex s)
  7.2037 +               (simplicial_cone p
  7.2038 +                 (\<lambda>i. (\<Sum>j\<le>Suc p. simplicial_vertex j f i) / (Suc (Suc p)))
  7.2039 +                 (simplicial_subdivision p
  7.2040 +                   (chain_boundary (Suc p) (frag_of f))))"
  7.2041 +          by (metis diff_Suc_1 nat.simps(3) simplicial_subdivision_of scf simplicial_chain_simplicial_subdivision)
  7.2042 +      have ff: "simplicial_chain (Suc p) (standard_simplex s) (subd p (chain_boundary (Suc p) (frag_of f)))"
  7.2043 +        by (metis (no_types) Suc.IH diff_Suc_1 scf simplicial_chain_boundary)
  7.2044 +      show "simplicial_chain (Suc (Suc p)) (standard_simplex s) (subd (Suc p) (frag_of f))"
  7.2045 +        using one
  7.2046 +        apply (simp only: subd.simps frag_extend_of)
  7.2047 +        apply (rule_tac S="standard_simplex s" in simplicial_chain_simplicial_cone)
  7.2048 +         apply (intro simplicial_chain_diff ff)
  7.2049 +        using sc apply (simp add: algebra_simps)
  7.2050 +        using "**" convex_standard_simplex  apply force+
  7.2051 +        done
  7.2052 +      have "simplicial_chain p (standard_simplex s) (chain_boundary (Suc p) (frag_of f))"
  7.2053 +        using scf simplicial_chain_boundary by fastforce
  7.2054 +      then have "chain_boundary (Suc p) (simplicial_subdivision (Suc p) (frag_of f) - frag_of f
  7.2055 +                                         - subd p (chain_boundary (Suc p) (frag_of f))) = 0"
  7.2056 +        apply (simp only: chain_boundary_diff)
  7.2057 +        using Suc.IH chain_boundary_boundary [of "Suc p" "subtopology (powertop_real UNIV)
  7.2058 +                                (standard_simplex s)" "frag_of f"]
  7.2059 +        by (metis One_nat_def add_diff_cancel_left' subd_0 chain_boundary_simplicial_subdivision plus_1_eq_Suc scf simplicial_imp_singular_chain)
  7.2060 +      then show "chain_boundary (Suc (Suc p)) (subd (Suc p) (frag_of f))
  7.2061 +          + subd (Suc p - Suc 0) (chain_boundary (Suc p) (frag_of f))
  7.2062 +          = simplicial_subdivision (Suc p) (frag_of f) - frag_of f"
  7.2063 +        apply (simp only: subd.simps frag_extend_of)
  7.2064 +        apply (subst chain_boundary_simplicial_cone [of "Suc p" "standard_simplex s"])
  7.2065 +         apply (meson ff scf simplicial_chain_diff simplicial_chain_simplicial_subdivision)
  7.2066 +        apply (simp add: simplicial_cone_def del: sum_atMost_Suc simplicial_subdivision.simps)
  7.2067 +        done
  7.2068 +    qed
  7.2069 +  next
  7.2070 +    case (diff a b)
  7.2071 +    then show ?case
  7.2072 +      apply safe
  7.2073 +        apply (metis chain_map_diff subd_diff)
  7.2074 +       apply (metis simplicial_chain_diff subd_diff)
  7.2075 +      apply (auto simp:  simplicial_subdivision_diff chain_boundary_diff
  7.2076 +          simp del: simplicial_subdivision.simps subd.simps)
  7.2077 +      by (metis (no_types, lifting) add_diff_add add_uminus_conv_diff diff_0 diff_diff_add)
  7.2078 +  qed auto
  7.2079 +qed simp
  7.2080 +
  7.2081 +lemma chain_homotopic_simplicial_subdivision1:
  7.2082 +  "\<lbrakk>simplicial_chain p (standard_simplex q) c; simplicial_simplex q (standard_simplex r) g\<rbrakk>
  7.2083 +       \<Longrightarrow> chain_map (Suc p) g (subd p c) = subd p (chain_map p g c)"
  7.2084 +  by (simp add: subd)
  7.2085 +
  7.2086 +lemma chain_homotopic_simplicial_subdivision2:
  7.2087 +  "simplicial_chain p (standard_simplex q) c
  7.2088 +       \<Longrightarrow> simplicial_chain (Suc p) (standard_simplex q) (subd p c)"
  7.2089 +  by (simp add: subd)
  7.2090 +
  7.2091 +lemma chain_homotopic_simplicial_subdivision3:
  7.2092 +  "simplicial_chain p (standard_simplex q) c
  7.2093 +   \<Longrightarrow> chain_boundary (Suc p) (subd p c) = (simplicial_subdivision p c) - c - subd (p - Suc 0) (chain_boundary p c)"
  7.2094 +  by (simp add: subd algebra_simps)
  7.2095 +
  7.2096 +lemma chain_homotopic_simplicial_subdivision:
  7.2097 +  "\<exists>h. (\<forall>p. h p 0 = 0) \<and>
  7.2098 +       (\<forall>p c1 c2. h p (c1-c2) = h p c1 - h p c2) \<and>
  7.2099 +       (\<forall>p q r g c.
  7.2100 +                simplicial_chain p (standard_simplex q) c
  7.2101 +                \<longrightarrow> simplicial_simplex q (standard_simplex r) g
  7.2102 +                \<longrightarrow> chain_map (Suc p) g (h p c) = h p (chain_map p g c)) \<and>
  7.2103 +       (\<forall>p q c. simplicial_chain p (standard_simplex q) c
  7.2104 +                \<longrightarrow> simplicial_chain (Suc p) (standard_simplex q) (h p c)) \<and>
  7.2105 +       (\<forall>p q c. simplicial_chain p (standard_simplex q) c
  7.2106 +                \<longrightarrow> chain_boundary (Suc p) (h p c) + h (p - Suc 0) (chain_boundary p c)
  7.2107 +                  = (simplicial_subdivision p c) - c)"
  7.2108 +  by (rule_tac x=subd in exI) (fastforce simp: subd)
  7.2109 +
  7.2110 +lemma chain_homotopic_singular_subdivision:
  7.2111 +  obtains h where
  7.2112 +        "\<And>p. h p 0 = 0"
  7.2113 +        "\<And>p c1 c2. h p (c1-c2) = h p c1 - h p c2"
  7.2114 +        "\<And>p X c. singular_chain p X c \<Longrightarrow> singular_chain (Suc p) X (h p c)"
  7.2115 +        "\<And>p X c. singular_chain p X c
  7.2116 +                 \<Longrightarrow> chain_boundary (Suc p) (h p c) + h (p - Suc 0) (chain_boundary p c) = singular_subdivision p c - c"
  7.2117 +proof -
  7.2118 +  define k where "k \<equiv> \<lambda>p. frag_extend (\<lambda>f:: (nat \<Rightarrow> real) \<Rightarrow> 'a. chain_map (Suc p) f (subd p (frag_of(restrict id (standard_simplex p)))))"
  7.2119 +  show ?thesis
  7.2120 +  proof
  7.2121 +    fix p X and c :: "'a chain"
  7.2122 +    assume c: "singular_chain p X c"
  7.2123 +    have "singular_chain (Suc p) X (k p c) \<and>
  7.2124 +               chain_boundary (Suc p) (k p c) + k (p - Suc 0) (chain_boundary p c) = singular_subdivision p c - c"
  7.2125 +      using c [unfolded singular_chain_def]
  7.2126 +    proof (induction rule: frag_induction)
  7.2127 +      case (one f)
  7.2128 +      let ?X = "subtopology (powertop_real UNIV) (standard_simplex p)"
  7.2129 +      show ?case
  7.2130 +      proof (simp add: k_def, intro conjI)
  7.2131 +        show "singular_chain (Suc p) X (chain_map (Suc p) f (subd p (frag_of (restrict id (standard_simplex p)))))"
  7.2132 +        proof (rule singular_chain_chain_map)
  7.2133 +          show "singular_chain (Suc p) ?X  (subd p (frag_of (restrict id (standard_simplex p))))"
  7.2134 +            by (simp add: chain_homotopic_simplicial_subdivision2 simplicial_imp_singular_chain)
  7.2135 +          show "continuous_map ?X X f"
  7.2136 +            using one.hyps singular_simplex_def by auto
  7.2137 +        qed
  7.2138 +      next
  7.2139 +        have scp: "singular_chain (Suc p) ?X (subd p (frag_of (restrict id (standard_simplex p))))"
  7.2140 +          by (simp add: chain_homotopic_simplicial_subdivision2 simplicial_imp_singular_chain)
  7.2141 +        have feqf: "frag_of (simplex_map p f (restrict id (standard_simplex p))) = frag_of f"
  7.2142 +          using one.hyps singular_simplex_chain_map_id by auto
  7.2143 +        have *: "chain_map p f
  7.2144 +                   (subd (p - Suc 0)
  7.2145 +                     (\<Sum>k\<le>p. frag_cmul ((-1) ^ k) (frag_of (singular_face p k id))))
  7.2146 +              = (\<Sum>x\<le>p. frag_cmul ((-1) ^ x)
  7.2147 +                         (chain_map p (singular_face p x f)
  7.2148 +                           (subd (p - Suc 0) (frag_of (restrict id (standard_simplex (p - Suc 0)))))))"
  7.2149 +                  (is "?lhs = ?rhs")
  7.2150 +                  if "p > 0"
  7.2151 +        proof -
  7.2152 +          have eqc: "subd (p - Suc 0) (frag_of (singular_face p i id))
  7.2153 +                   = chain_map p (singular_face p i id)
  7.2154 +                                 (subd (p - Suc 0) (frag_of (restrict id (standard_simplex (p - Suc 0)))))"
  7.2155 +            if "i \<le> p" for i
  7.2156 +          proof -
  7.2157 +            have 1: "simplicial_chain (p - Suc 0) (standard_simplex (p - Suc 0))
  7.2158 +                       (frag_of (restrict id (standard_simplex (p - Suc 0))))"
  7.2159 +              by simp
  7.2160 +            have 2: "simplicial_simplex (p - Suc 0) (standard_simplex p) (singular_face p i id)"
  7.2161 +              by (metis One_nat_def Suc_leI \<open>0 < p\<close> simplicial_simplex_id simplicial_simplex_singular_face singular_face_restrict subsetI that)
  7.2162 +            have 3: "simplex_map (p - Suc 0) (singular_face p i id) (restrict id (standard_simplex (p - Suc 0)))
  7.2163 +                   = singular_face p i id"
  7.2164 +              by (force simp: simplex_map_def singular_face_def)
  7.2165 +            show ?thesis
  7.2166 +              using chain_homotopic_simplicial_subdivision1 [OF 1 2]
  7.2167 +                that \<open>p > 0\<close>  by (simp add: 3)
  7.2168 +          qed
  7.2169 +          have xx: "simplicial_chain p (standard_simplex(p - Suc 0))
  7.2170 +                    (subd (p - Suc 0) (frag_of (restrict id (standard_simplex (p - Suc 0)))))"
  7.2171 +            by (metis Suc_pred chain_homotopic_simplicial_subdivision2 order_refl simplicial_chain_of simplicial_simplex_id that)
  7.2172 +          have yy: "\<And>k. k \<le> p \<Longrightarrow>
  7.2173 +                 chain_map p f
  7.2174 +                  (chain_map p (singular_face p k id) h) = chain_map p (singular_face p k f) h"
  7.2175 +            if "simplicial_chain p (standard_simplex(p - Suc 0)) h" for h
  7.2176 +            using that unfolding simplicial_chain_def
  7.2177 +          proof (induction h rule: frag_induction)
  7.2178 +            case (one x)
  7.2179 +            then show ?case
  7.2180 +                using one
  7.2181 +              apply (simp add: chain_map_of singular_simplex_def simplicial_simplex_def, auto)
  7.2182 +                apply (rule_tac f=frag_of in arg_cong, rule)
  7.2183 +                apply (simp add: simplex_map_def)
  7.2184 +                by (simp add: continuous_map_in_subtopology image_subset_iff singular_face_def)
  7.2185 +          qed (auto simp: chain_map_diff)
  7.2186 +          have "?lhs
  7.2187 +                = chain_map p f
  7.2188 +                      (\<Sum>k\<le>p. frag_cmul ((-1) ^ k)
  7.2189 +                          (chain_map p (singular_face p k id)
  7.2190 +                           (subd (p - Suc 0) (frag_of (restrict id (standard_simplex (p - Suc 0)))))))"
  7.2191 +            by (simp add: subd_power_sum subd_power_uminus eqc)
  7.2192 +          also have "\<dots> = ?rhs"
  7.2193 +            by (simp add: chain_map_sum xx yy)
  7.2194 +          finally show ?thesis .
  7.2195 +      qed
  7.2196 +        have "chain_map p f
  7.2197 +                   (simplicial_subdivision p (frag_of (restrict id (standard_simplex p)))
  7.2198 +                   - subd (p - Suc 0) (chain_boundary p (frag_of (restrict id (standard_simplex p)))))
  7.2199 +              = singular_subdivision p (frag_of f)
  7.2200 +              - frag_extend
  7.2201 +                   (\<lambda>f. chain_map (Suc (p - Suc 0)) f
  7.2202 +                         (subd (p - Suc 0) (frag_of (restrict id (standard_simplex (p - Suc 0))))))
  7.2203 +                   (chain_boundary p (frag_of f))"
  7.2204 +          apply (simp add: singular_subdivision_def chain_map_diff)
  7.2205 +          apply (clarsimp simp add: chain_boundary_def)
  7.2206 +          apply (simp add: frag_extend_sum frag_extend_cmul *)
  7.2207 +          done
  7.2208 +        then show "chain_boundary (Suc p) (chain_map (Suc p) f (subd p (frag_of (restrict id (standard_simplex p)))))
  7.2209 +                 + frag_extend
  7.2210 +                   (\<lambda>f. chain_map (Suc (p - Suc 0)) f
  7.2211 +                         (subd (p - Suc 0) (frag_of (restrict id (standard_simplex (p - Suc 0))))))
  7.2212 +                   (chain_boundary p (frag_of f))
  7.2213 +                 = singular_subdivision p (frag_of f) - frag_of f"
  7.2214 +          by (simp add: chain_boundary_chain_map [OF scp] chain_homotopic_simplicial_subdivision3 [where q=p] chain_map_diff feqf)
  7.2215 +      qed
  7.2216 +    next
  7.2217 +      case (diff a b)
  7.2218 +      then show ?case
  7.2219 +        apply (simp only: k_def singular_chain_diff chain_boundary_diff frag_extend_diff singular_subdivision_diff)
  7.2220 +        by (metis (no_types, lifting) add_diff_add diff_add_cancel)
  7.2221 +    qed (auto simp: k_def)
  7.2222 +    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"
  7.2223 +        by auto
  7.2224 +  qed (auto simp: k_def frag_extend_diff)
  7.2225 +qed
  7.2226 +
  7.2227 +
  7.2228 +lemma homologous_rel_singular_subdivision:
  7.2229 +  assumes "singular_relcycle p X T c"
  7.2230 +  shows "homologous_rel p X T (singular_subdivision p c) c"
  7.2231 +proof (cases "p = 0")
  7.2232 +  case True
  7.2233 +  with assms show ?thesis
  7.2234 +    by (auto simp: singular_relcycle_def singular_subdivision_zero)
  7.2235 +next
  7.2236 +  case False
  7.2237 +  with assms show ?thesis
  7.2238 +    unfolding homologous_rel_def singular_relboundary singular_relcycle
  7.2239 +    by (metis One_nat_def Suc_diff_1 chain_homotopic_singular_subdivision gr_zeroI)
  7.2240 +qed
  7.2241 +
  7.2242 +
  7.2243 +subsection\<open>Excision argument that we keep doing singular subdivision\<close>
  7.2244 +
  7.2245 +lemma singular_subdivision_power_0 [simp]: "(singular_subdivision p ^^ n) 0 = 0"
  7.2246 +  by (induction n) auto
  7.2247 +
  7.2248 +lemma singular_subdivision_power_diff:
  7.2249 +  "(singular_subdivision p ^^ n) (a - b) = (singular_subdivision p ^^ n) a - (singular_subdivision p ^^ n) b"
  7.2250 +  by (induction n) (auto simp: singular_subdivision_diff)
  7.2251 +
  7.2252 +lemma iterated_singular_subdivision:
  7.2253 +   "singular_chain p X c
  7.2254 +        \<Longrightarrow> (singular_subdivision p ^^ n) c =
  7.2255 +            frag_extend
  7.2256 +             (\<lambda>f. chain_map p f
  7.2257 +                       ((simplicial_subdivision p ^^ n)
  7.2258 +                         (frag_of(restrict id (standard_simplex p))))) c"
  7.2259 +proof (induction n arbitrary: c)
  7.2260 +  case 0
  7.2261 +  then show ?case
  7.2262 +    unfolding singular_chain_def
  7.2263 +  proof (induction c rule: frag_induction)
  7.2264 +    case (one f)
  7.2265 +    then have "restrict f (standard_simplex p) = f"
  7.2266 +      by (simp add: extensional_restrict singular_simplex_def)
  7.2267 +    then show ?case
  7.2268 +      by (auto simp: simplex_map_def cong: restrict_cong)
  7.2269 +  qed (auto simp: frag_extend_diff)
  7.2270 +next
  7.2271 +  case (Suc n)
  7.2272 +  show ?case
  7.2273 +    using Suc.prems unfolding singular_chain_def
  7.2274 +  proof (induction c rule: frag_induction)
  7.2275 +    case (one f)
  7.2276 +    then have "singular_simplex p X f"
  7.2277 +      by simp
  7.2278 +    have scp: "simplicial_chain p (standard_simplex p)
  7.2279 +                 ((simplicial_subdivision p ^^ n) (frag_of (restrict id (standard_simplex p))))"
  7.2280 +    proof (induction n)
  7.2281 +      case 0
  7.2282 +      then show ?case
  7.2283 +        by (metis funpow_0 order_refl simplicial_chain_of simplicial_simplex_id)
  7.2284 +    next
  7.2285 +      case (Suc n)
  7.2286 +      then show ?case
  7.2287 +        by (simp add: simplicial_chain_simplicial_subdivision)
  7.2288 +    qed
  7.2289 +    have scnp: "simplicial_chain p (standard_simplex p)
  7.2290 +                  ((simplicial_subdivision p ^^ n) (frag_of (\<lambda>x\<in>standard_simplex p. x)))"
  7.2291 +    proof (induction n)
  7.2292 +      case 0
  7.2293 +      then show ?case
  7.2294 +        by (metis eq_id_iff funpow_0 order_refl simplicial_chain_of simplicial_simplex_id)
  7.2295 +    next
  7.2296 +      case (Suc n)
  7.2297 +      then show ?case
  7.2298 +        by (simp add: simplicial_chain_simplicial_subdivision)
  7.2299 +    qed
  7.2300 +    have sff: "singular_chain p X (frag_of f)"
  7.2301 +      by (simp add: \<open>singular_simplex p X f\<close> singular_chain_of)
  7.2302 +    then show ?case
  7.2303 +      using Suc.IH [OF sff] naturality_singular_subdivision [OF simplicial_imp_singular_chain [OF scp], of f] singular_subdivision_simplicial_simplex [OF scnp]
  7.2304 +      by (simp add: singular_chain_of id_def del: restrict_apply)
  7.2305 +  qed (auto simp: singular_subdivision_power_diff singular_subdivision_diff frag_extend_diff)
  7.2306 +qed
  7.2307 +
  7.2308 +
  7.2309 +lemma chain_homotopic_iterated_singular_subdivision:
  7.2310 +  obtains h where
  7.2311 +        "\<And>p. h p 0 = (0 :: 'a chain)"
  7.2312 +        "\<And>p c1 c2. h p (c1-c2) = h p c1 - h p c2"
  7.2313 +        "\<And>p X c. singular_chain p X c \<Longrightarrow> singular_chain (Suc p) X (h p c)"
  7.2314 +        "\<And>p X c. singular_chain p X c
  7.2315 +                 \<Longrightarrow> chain_boundary (Suc p) (h p c) + h (p - Suc 0) (chain_boundary p c)
  7.2316 +                   = (singular_subdivision p ^^ n) c - c"
  7.2317 +proof (induction n arbitrary: thesis)
  7.2318 +  case 0
  7.2319 +  show ?case
  7.2320 +    by (rule 0 [of "(\<lambda>p x. 0)"]) auto
  7.2321 +next
  7.2322 +  case (Suc n)
  7.2323 +  then obtain k where k:
  7.2324 +        "\<And>p. k p 0 = (0 :: 'a chain)"
  7.2325 +        "\<And>p c1 c2. k p (c1-c2) = k p c1 - k p c2"
  7.2326 +        "\<And>p X c. singular_chain p X c \<Longrightarrow> singular_chain (Suc p) X (k p c)"
  7.2327 +        "\<And>p X c. singular_chain p X c
  7.2328 +                 \<Longrightarrow> chain_boundary (Suc p) (k p c) + k (p - Suc 0) (chain_boundary p c)
  7.2329 +                     = (singular_subdivision p ^^ n) c - c"
  7.2330 +    by metis
  7.2331 +  obtain h where h:
  7.2332 +        "\<And>p. h p 0 = (0 :: 'a chain)"
  7.2333 +        "\<And>p c1 c2. h p (c1-c2) = h p c1 - h p c2"
  7.2334 +        "\<And>p X c. singular_chain p X c \<Longrightarrow> singular_chain (Suc p) X (h p c)"
  7.2335 +        "\<And>p X c. singular_chain p X c
  7.2336 +                 \<Longrightarrow> chain_boundary (Suc p) (h p c) + h (p - Suc 0) (chain_boundary p c) = singular_subdivision p c - c"
  7.2337 +    by (blast intro: chain_homotopic_singular_subdivision)
  7.2338 +  let ?h = "(\<lambda>p c. singular_subdivision (Suc p) (k p c) + h p c)"
  7.2339 +  show ?case
  7.2340 +  proof (rule Suc.prems)
  7.2341 +    fix p X and c :: "'a chain"
  7.2342 +    assume "singular_chain p X c"
  7.2343 +    then show "singular_chain (Suc p) X (?h p c)"
  7.2344 +      by (simp add: h k singular_chain_add singular_chain_singular_subdivision)
  7.2345 +  next
  7.2346 +    fix p :: "nat" and X :: "'a topology" and c :: "'a chain"
  7.2347 +    assume sc: "singular_chain p X c"
  7.2348 +    have f5: "chain_boundary (Suc p) (singular_subdivision (Suc p) (k p c)) = singular_subdivision p (chain_boundary (Suc p) (k p c))"
  7.2349 +      using chain_boundary_singular_subdivision k(3) sc by fastforce
  7.2350 +    have [simp]: "singular_subdivision (Suc (p - Suc 0)) (k (p - Suc 0) (chain_boundary p c)) =
  7.2351 +                  singular_subdivision p (k (p - Suc 0) (chain_boundary p c))"
  7.2352 +    proof (cases p)
  7.2353 +      case 0
  7.2354 +      then show ?thesis
  7.2355 +        by (simp add: k chain_boundary_def)
  7.2356 +    qed auto
  7.2357 +    show "chain_boundary (Suc p) (?h p c) + ?h (p - Suc 0) (chain_boundary p c) = (singular_subdivision p ^^ Suc n) c - c"
  7.2358 +      using chain_boundary_singular_subdivision [of "Suc p" X]
  7.2359 +      apply (simp add: chain_boundary_add f5 h k algebra_simps)
  7.2360 +      apply (erule thin_rl)
  7.2361 +      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)"]
  7.2362 +      apply (simp add: algebra_simps)
  7.2363 +      by (smt add.assoc add.left_commute singular_subdivision_add)
  7.2364 +  qed (auto simp: k h singular_subdivision_diff)
  7.2365 +qed
  7.2366 +
  7.2367 +lemma llemma:
  7.2368 +  assumes p: "standard_simplex p \<subseteq> \<Union>\<C>"
  7.2369 +      and \<C>: "\<And>U. U \<in> \<C> \<Longrightarrow> openin (powertop_real UNIV) U"
  7.2370 +  obtains d where "0 < d"
  7.2371 +                  "\<And>K. \<lbrakk>K \<subseteq> standard_simplex p;
  7.2372 +                        \<And>x y i. \<lbrakk>i \<le> p; x \<in> K; y \<in> K\<rbrakk> \<Longrightarrow> \<bar>x i - y i\<bar> \<le> d\<rbrakk>
  7.2373 +                       \<Longrightarrow> \<exists>U. U \<in> \<C> \<and> K \<subseteq> U"
  7.2374 +proof -
  7.2375 +  have "\<exists>e U. 0 < e \<and> U \<in> \<C> \<and> x \<in> U \<and>
  7.2376 +                (\<forall>y. (\<forall>i\<le>p. \<bar>y i - x i\<bar> \<le> 2 * e) \<and> (\<forall>i>p. y i = 0) \<longrightarrow> y \<in> U)"
  7.2377 +    if x: "x \<in> standard_simplex p" for x
  7.2378 +  proof-
  7.2379 +    obtain U where U: "U \<in> \<C>" "x \<in> U"
  7.2380 +      using x p by blast
  7.2381 +    then obtain V where finV: "finite {i. V i \<noteq> UNIV}" and openV: "\<And>i. open (V i)"
  7.2382 +                  and xV: "x \<in> Pi\<^sub>E UNIV V" and UV: "Pi\<^sub>E UNIV V \<subseteq> U"
  7.2383 +      using \<C> unfolding openin_product_topology_alt by force
  7.2384 +    have xVi: "x i \<in> V i" for i
  7.2385 +      using PiE_mem [OF xV] by simp
  7.2386 +    have "\<And>i. \<exists>e>0. \<forall>x'. \<bar>x' - x i\<bar> < e \<longrightarrow> x' \<in> V i"
  7.2387 +      by (rule openV [unfolded open_real, rule_format, OF xVi])
  7.2388 +    then obtain d where d: "\<And>i. d i > 0" and dV: "\<And>i x'. \<bar>x' - x i\<bar> < d i \<Longrightarrow> x' \<in> V i"
  7.2389 +      by metis
  7.2390 +    define e where "e \<equiv> Inf (insert 1 (d ` {i. V i \<noteq> UNIV})) / 3"
  7.2391 +    have ed3: "e \<le> d i / 3" if "V i \<noteq> UNIV" for i
  7.2392 +      using that finV by (auto simp: e_def intro: cInf_le_finite)
  7.2393 +    show "\<exists>e U. 0 < e \<and> U \<in> \<C> \<and> x \<in> U \<and>
  7.2394 +                (\<forall>y. (\<forall>i\<le>p. \<bar>y i - x i\<bar> \<le> 2 * e) \<and> (\<forall>i>p. y i = 0) \<longrightarrow> y \<in> U)"
  7.2395 +    proof (intro exI conjI allI impI)
  7.2396 +      show "e > 0"
  7.2397 +        using d finV by (simp add: e_def finite_less_Inf_iff)
  7.2398 +      fix y assume y: "(\<forall>i\<le>p. \<bar>y i - x i\<bar> \<le> 2 * e) \<and> (\<forall>i>p. y i = 0)"
  7.2399 +      have "y \<in> Pi\<^sub>E UNIV V"
  7.2400 +      proof
  7.2401 +        show "y i \<in> V i" for i
  7.2402 +        proof (cases "p < i")
  7.2403 +          case True
  7.2404 +          then show ?thesis
  7.2405 +            by (metis (mono_tags, lifting) y x mem_Collect_eq standard_simplex_def xVi)
  7.2406 +        next
  7.2407 +          case False show ?thesis
  7.2408 +          proof (cases "V i = UNIV")
  7.2409 +            case False show ?thesis
  7.2410 +            proof (rule dV)
  7.2411 +              have "\<bar>y i - x i\<bar> \<le> 2 * e"
  7.2412 +                using y \<open>\<not> p < i\<close> by simp
  7.2413 +              also have "\<dots> < d i"
  7.2414 +                using ed3 [OF False] \<open>e > 0\<close> by simp
  7.2415 +              finally show "\<bar>y i - x i\<bar> < d i" .
  7.2416 +            qed
  7.2417 +          qed auto
  7.2418 +        qed
  7.2419 +      qed auto
  7.2420 +      with UV show "y \<in> U"
  7.2421 +        by blast
  7.2422 +    qed (use U in auto)
  7.2423 +  qed
  7.2424 +  then obtain e U where
  7.2425 +      eU: "\<And>x. x \<in> standard_simplex p \<Longrightarrow>
  7.2426 +                0 < e x \<and> U x \<in> \<C> \<and> x \<in> U x"
  7.2427 +      and  UI: "\<And>x y. \<lbrakk>x \<in> standard_simplex p;  \<And>i. i \<le> p \<Longrightarrow> \<bar>y i - x i\<bar> \<le> 2 * e x; \<And>i. i > p \<Longrightarrow> y i = 0\<rbrakk>
  7.2428 +                       \<Longrightarrow> y \<in> U x"
  7.2429 +    by metis
  7.2430 +  define F where "F \<equiv> \<lambda>x. Pi\<^sub>E UNIV (\<lambda>i. if i \<le> p then {x i - e x<..<x i + e x} else UNIV)"
  7.2431 +  have "\<forall>S \<in> F ` standard_simplex p. openin (powertop_real UNIV) S"
  7.2432 +    by (simp add: F_def openin_PiE_gen)
  7.2433 +  moreover have pF: "standard_simplex p \<subseteq> \<Union>(F ` standard_simplex p)"
  7.2434 +    by (force simp: F_def PiE_iff eU)
  7.2435 +  ultimately have "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> F ` standard_simplex p \<and> standard_simplex p \<subseteq> \<Union>\<F>"
  7.2436 +    using compactin_standard_simplex [of p]
  7.2437 +    unfolding compactin_def by force
  7.2438 +  then obtain S where "finite S" and ssp: "S \<subseteq> standard_simplex p" "standard_simplex p \<subseteq> \<Union>(F ` S)"
  7.2439 +    unfolding exists_finite_subset_image by (auto simp: exists_finite_subset_image)
  7.2440 +  then have "S \<noteq> {}"
  7.2441 +    by (auto simp: nonempty_standard_simplex)
  7.2442 +  show ?thesis
  7.2443 +  proof
  7.2444 +    show "Inf (e ` S) > 0"
  7.2445 +      using \<open>finite S\<close> \<open>S \<noteq> {}\<close> ssp eU by (auto simp: finite_less_Inf_iff)
  7.2446 +    fix k :: "(nat \<Rightarrow> real) set"
  7.2447 +    assume k: "k \<subseteq> standard_simplex p"
  7.2448 +         and kle: "\<And>x y i. \<lbrakk>i \<le> p; x \<in> k; y \<in> k\<rbrakk> \<Longrightarrow> \<bar>x i - y i\<bar> \<le> Inf (e ` S)"
  7.2449 +    show "\<exists>U. U \<in> \<C> \<and> k \<subseteq> U"
  7.2450 +    proof (cases "k = {}")
  7.2451 +      case True
  7.2452 +      then show ?thesis
  7.2453 +        using \<open>S \<noteq> {}\<close> eU equals0I ssp(1) subset_eq p by auto
  7.2454 +    next
  7.2455 +      case False
  7.2456 +      with k ssp obtain x a where "x \<in> k" "x \<in> standard_simplex p"
  7.2457 +                            and a: "a \<in> S" and Fa: "x \<in> F a"
  7.2458 +        by blast
  7.2459 +      then have le_ea: "\<And>i. i \<le> p \<Longrightarrow> abs (x i - a i) < e a"
  7.2460 +        by (simp add: F_def PiE_iff if_distrib abs_diff_less_iff cong: if_cong)
  7.2461 +      show ?thesis
  7.2462 +      proof (intro exI conjI)
  7.2463 +        show "U a \<in> \<C>"
  7.2464 +          using a eU ssp(1) by auto
  7.2465 +        show "k \<subseteq> U a"
  7.2466 +        proof clarify
  7.2467 +          fix y assume "y \<in> k"
  7.2468 +          with k have y: "y \<in> standard_simplex p"
  7.2469 +            by blast
  7.2470 +          show "y \<in> U a"
  7.2471 +          proof (rule UI)
  7.2472 +            show "a \<in> standard_simplex p"
  7.2473 +              using a ssp(1) by auto
  7.2474 +            fix i :: "nat"
  7.2475 +            assume "i \<le> p"
  7.2476 +            then have "\<bar>x i - y i\<bar> \<le> e a"
  7.2477 +              by (meson kle [OF \<open>i \<le> p\<close>] a \<open>finite S\<close> \<open>x \<in> k\<close> \<open>y \<in> k\<close> cInf_le_finite finite_imageI imageI order_trans)
  7.2478 +            then show "\<bar>y i - a i\<bar> \<le> 2 * e a"
  7.2479 +              using le_ea [OF \<open>i \<le> p\<close>] by linarith
  7.2480 +          next
  7.2481 +            fix i assume "p < i"
  7.2482 +            then show "y i = 0"
  7.2483 +              using standard_simplex_def y by auto
  7.2484 +          qed
  7.2485 +        qed
  7.2486 +      qed
  7.2487 +    qed
  7.2488 +  qed
  7.2489 +qed
  7.2490 +
  7.2491 +
  7.2492 +proposition sufficient_iterated_singular_subdivision_exists:
  7.2493 +  assumes \<C>: "\<And>U. U \<in> \<C> \<Longrightarrow> openin X U"
  7.2494 +      and X: "topspace X \<subseteq> \<Union>\<C>"
  7.2495 +      and p: "singular_chain p X c"
  7.2496 +  obtains n where "\<And>m f. \<lbrakk>n \<le> m; f \<in> Poly_Mapping.keys ((singular_subdivision p ^^ m) c)\<rbrakk>
  7.2497 +                      \<Longrightarrow> \<exists>V \<in> \<C>. f ` (standard_simplex p) \<subseteq> V"
  7.2498 +proof (cases "c = 0")
  7.2499 +  case False
  7.2500 +  then show ?thesis
  7.2501 +  proof (cases "topspace X = {}")
  7.2502 +    case True
  7.2503 +    show ?thesis
  7.2504 +      using p that by (force simp: singular_chain_empty True)
  7.2505 +  next
  7.2506 +    case False
  7.2507 +    show ?thesis
  7.2508 +    proof (cases "\<C> = {}")
  7.2509 +      case True
  7.2510 +      then show ?thesis
  7.2511 +        using False X by blast
  7.2512 +    next
  7.2513 +      case False
  7.2514 +      have "\<exists>e. 0 < e \<and>
  7.2515 +                (\<forall>K. K \<subseteq> standard_simplex p \<longrightarrow> (\<forall>x y i. x \<in> K \<and> y \<in> K \<and> i \<le> p \<longrightarrow> \<bar>x i - y i\<bar> \<le> e)
  7.2516 +                     \<longrightarrow> (\<exists>V. V \<in> \<C> \<and> f ` K \<subseteq> V))"
  7.2517 +        if f: "f \<in> Poly_Mapping.keys c" for f
  7.2518 +      proof -
  7.2519 +        have ssf: "singular_simplex p X f"
  7.2520 +          using f p by (auto simp: singular_chain_def)
  7.2521 +        then have fp: "\<And>x. x \<in> standard_simplex p \<Longrightarrow> f x \<in> topspace X"
  7.2522 +          by (auto simp: singular_simplex_def image_subset_iff dest: continuous_map_image_subset_topspace)
  7.2523 +        have "\<exists>T. openin (powertop_real UNIV) T \<and>
  7.2524 +                    standard_simplex p \<inter> f -` V = T \<inter> standard_simplex p"
  7.2525 +          if V: "V \<in> \<C>" for V
  7.2526 +        proof -
  7.2527 +          have "singular_simplex p X f"
  7.2528 +            using p f unfolding singular_chain_def by blast
  7.2529 +          then have "openin (subtopology (powertop_real UNIV) (standard_simplex p))
  7.2530 +                            {x \<in> standard_simplex p. f x \<in> V}"
  7.2531 +            using \<C> [OF \<open>V \<in> \<C>\<close>] by (simp add: singular_simplex_def continuous_map_def)
  7.2532 +          moreover have "standard_simplex p \<inter> f -` V = {x \<in> standard_simplex p. f x \<in> V}"
  7.2533 +            by blast
  7.2534 +          ultimately show ?thesis
  7.2535 +            by (simp add: openin_subtopology)
  7.2536 +        qed
  7.2537 +        then obtain g where gope: "\<And>V. V \<in> \<C> \<Longrightarrow> openin (powertop_real UNIV) (g V)"
  7.2538 +                and geq: "\<And>V. V \<in> \<C> \<Longrightarrow> standard_simplex p \<inter> f -` V = g V \<inter> standard_simplex p"
  7.2539 +          by metis
  7.2540 +        obtain d where "0 < d"
  7.2541 +              and d: "\<And>K. \<lbrakk>K \<subseteq> standard_simplex p; \<And>x y i. \<lbrakk>i \<le> p; x \<in> K; y \<in> K\<rbrakk> \<Longrightarrow> \<bar>x i - y i\<bar> \<le> d\<rbrakk>
  7.2542 +                       \<Longrightarrow> \<exists>U. U \<in> g ` \<C> \<and> K \<subseteq> U"
  7.2543 +        proof (rule llemma [of p "g ` \<C>"])
  7.2544 +          show "standard_simplex p \<subseteq> \<Union>(g ` \<C>)"
  7.2545 +            using geq X fp by (fastforce simp add:)
  7.2546 +          show "openin (powertop_real UNIV) U" if "U \<in> g ` \<C>" for U :: "(nat \<Rightarrow> real) set"
  7.2547 +            using gope that by blast
  7.2548 +        qed auto
  7.2549 +        show ?thesis
  7.2550 +        proof (rule exI, intro allI conjI impI)
  7.2551 +          fix K :: "(nat \<Rightarrow> real) set"
  7.2552 +          assume K: "K \<subseteq> standard_simplex p"
  7.2553 +             and Kd: "\<forall>x y i. x \<in> K \<and> y \<in> K \<and> i \<le> p \<longrightarrow> \<bar>x i - y i\<bar> \<le> d"
  7.2554 +          then have "\<exists>U. U \<in> g ` \<C> \<and> K \<subseteq> U"
  7.2555 +            using d [OF K] by auto
  7.2556 +          then show "\<exists>V. V \<in> \<C> \<and> f ` K \<subseteq> V"
  7.2557 +            using K geq by fastforce
  7.2558 +        qed (rule \<open>d > 0\<close>)
  7.2559 +      qed
  7.2560 +      then obtain \<psi> where epos: "\<forall>f \<in> Poly_Mapping.keys c. 0 < \<psi> f"
  7.2561 +                 and e: "\<And>f K. \<lbrakk>f \<in> Poly_Mapping.keys c; K \<subseteq> standard_simplex p;
  7.2562 +                                \<And>x y i. x \<in> K \<and> y \<in> K \<and> i \<le> p \<Longrightarrow> \<bar>x i - y i\<bar> \<le> \<psi> f\<rbrakk>
  7.2563 +                               \<Longrightarrow> \<exists>V. V \<in> \<C> \<and> f ` K \<subseteq> V"
  7.2564 +        by metis
  7.2565 +      obtain d where "0 < d"
  7.2566 +               and d: "\<And>f K. \<lbrakk>f \<in> Poly_Mapping.keys c; K \<subseteq> standard_simplex p;
  7.2567 +                              \<And>x y i. \<lbrakk>x \<in> K; y \<in> K; i \<le> p\<rbrakk> \<Longrightarrow> \<bar>x i - y i\<bar> \<le> d\<rbrakk>
  7.2568 +                              \<Longrightarrow> \<exists>V. V \<in> \<C> \<and> f ` K \<subseteq> V"
  7.2569 +      proof
  7.2570 +        show "Inf (\<psi> ` Poly_Mapping.keys c) > 0"
  7.2571 +          by (simp add: finite_less_Inf_iff \<open>c \<noteq> 0\<close> epos)
  7.2572 +        fix f K
  7.2573 +        assume fK: "f \<in> Poly_Mapping.keys c" "K \<subseteq> standard_simplex p"
  7.2574 +          and le: "\<And>x y i. \<lbrakk>x \<in> K; y \<in> K; i \<le> p\<rbrakk> \<Longrightarrow> \<bar>x i - y i\<bar> \<le> Inf (\<psi> ` Poly_Mapping.keys c)"
  7.2575 +        then have lef: "Inf (\<psi> ` Poly_Mapping.keys c) \<le> \<psi> f"
  7.2576 +          by (auto intro: cInf_le_finite)
  7.2577 +        show "\<exists>V. V \<in> \<C> \<and> f ` K \<subseteq> V"
  7.2578 +          using le lef by (blast intro: dual_order.trans e [OF fK])
  7.2579 +      qed
  7.2580 +      let ?d = "\<lambda>m. (simplicial_subdivision p ^^ m) (frag_of (restrict id (standard_simplex p)))"
  7.2581 +      obtain n where n: "(p / (Suc p)) ^ n < d"
  7.2582 +        using real_arch_pow_inv \<open>0 < d\<close> by fastforce
  7.2583 +      show ?thesis
  7.2584 +      proof
  7.2585 +        fix m h
  7.2586 +        assume "n \<le> m" and "h \<in> Poly_Mapping.keys ((singular_subdivision p ^^ m) c)"
  7.2587 +        then obtain f where "f \<in> Poly_Mapping.keys c" "h \<in> Poly_Mapping.keys (chain_map p f (?d m))"
  7.2588 +          using subsetD [OF keys_frag_extend] iterated_singular_subdivision [OF p, of m] by force
  7.2589 +        then obtain g where g: "g \<in> Poly_Mapping.keys (?d m)" and heq: "h = restrict (f \<circ> g) (standard_simplex p)"
  7.2590 +          using keys_frag_extend by (force simp: chain_map_def simplex_map_def)
  7.2591 +        have xx: "simplicial_chain p (standard_simplex p) (?d n) \<and>
  7.2592 +                  (\<forall>f \<in> Poly_Mapping.keys(?d n). \<forall>x \<in> standard_simplex p. \<forall>y \<in> standard_simplex p.
  7.2593 +                       \<bar>f x i - f y i\<bar> \<le> (p / (Suc p)) ^ n)"
  7.2594 +          for n i
  7.2595 +        proof (induction n)
  7.2596 +          case 0
  7.2597 +          have "simplicial_simplex p (standard_simplex p) (\<lambda>a\<in>standard_simplex p. a)"
  7.2598 +            by (metis eq_id_iff order_refl simplicial_simplex_id)
  7.2599 +          moreover have "(\<forall>x\<in>standard_simplex p. \<forall>y\<in>standard_simplex p. \<bar>x i - y i\<bar> \<le> 1)"
  7.2600 +            unfolding standard_simplex_def
  7.2601 +            by (auto simp: abs_if dest!: spec [where x=i])
  7.2602 +          ultimately show ?case
  7.2603 +            unfolding power_0 funpow_0 by simp
  7.2604 +        next
  7.2605 +          case (Suc n)
  7.2606 +          show ?case
  7.2607 +            unfolding power_Suc funpow.simps o_def
  7.2608 +          proof (intro conjI ballI)
  7.2609 +            show "simplicial_chain p (standard_simplex p) (simplicial_subdivision p (?d n))"
  7.2610 +              by (simp add: Suc simplicial_chain_simplicial_subdivision)
  7.2611 +            show "\<bar>f x i - f y i\<bar> \<le> real p / real (Suc p) * (real p / real (Suc p)) ^ n"
  7.2612 +              if "f \<in> Poly_Mapping.keys (simplicial_subdivision p (?d n))"
  7.2613 +                and "x \<in> standard_simplex p" and "y \<in> standard_simplex p" for f x y
  7.2614 +              using Suc that by (blast intro: simplicial_subdivision_shrinks)
  7.2615 +          qed
  7.2616 +        qed
  7.2617 +        have "g ` standard_simplex p \<subseteq> standard_simplex p"
  7.2618 +          using g xx [of m] unfolding simplicial_chain_def simplicial_simplex by auto
  7.2619 +        moreover
  7.2620 +        have "\<bar>g x i - g y i\<bar> \<le> d" if "i \<le> p" "x \<in> standard_simplex p" "y \<in> standard_simplex p" for x y i
  7.2621 +        proof -
  7.2622 +          have "\<bar>g x i - g y i\<bar> \<le> (p / (Suc p)) ^ m"
  7.2623 +            using g xx [of m] that by blast
  7.2624 +          also have "\<dots> \<le> (p / (Suc p)) ^ n"
  7.2625 +            by (auto intro: power_decreasing [OF \<open>n \<le> m\<close>])
  7.2626 +          finally show ?thesis using n by simp
  7.2627 +        qed
  7.2628 +        then have "\<bar>x i - y i\<bar> \<le> d"
  7.2629 +          if "x \<in> g ` (standard_simplex p)" "y \<in> g ` (standard_simplex p)" "i \<le> p" for i x y
  7.2630 +          using that by blast
  7.2631 +        ultimately show "\<exists>V\<in>\<C>. h ` standard_simplex p \<subseteq> V"
  7.2632 +          using \<open>f \<in> Poly_Mapping.keys c\<close> d [of f "g ` standard_simplex p"]
  7.2633 +          by (simp add: Bex_def heq image_image)
  7.2634 +      qed
  7.2635 +    qed
  7.2636 +  qed
  7.2637 +qed force
  7.2638 +
  7.2639 +
  7.2640 +lemma small_homologous_rel_relcycle_exists:
  7.2641 +  assumes \<C>: "\<And>U. U \<in> \<C> \<Longrightarrow> openin X U"
  7.2642 +      and X: "topspace X \<subseteq> \<Union>\<C>"
  7.2643 +      and p: "singular_relcycle p X S c"
  7.2644 +    obtains c' where "singular_relcycle p X S c'" "homologous_rel p X S c c'"
  7.2645 +                      "\<And>f. f \<in> Poly_Mapping.keys c' \<Longrightarrow> \<exists>V \<in> \<C>. f ` (standard_simplex p) \<subseteq> V"
  7.2646 +proof -
  7.2647 +  have "singular_chain p X c"
  7.2648 +       "(chain_boundary p c, 0) \<in> (mod_subset (p - Suc 0) (subtopology X S))"
  7.2649 +    using p unfolding singular_relcycle_def by auto
  7.2650 +  then obtain n where n: "\<And>m f. \<lbrakk>n \<le> m; f \<in> Poly_Mapping.keys ((singular_subdivision p ^^ m) c)\<rbrakk>
  7.2651 +                            \<Longrightarrow> \<exists>V \<in> \<C>. f ` (standard_simplex p) \<subseteq> V"
  7.2652 +    by (blast intro: sufficient_iterated_singular_subdivision_exists [OF \<C> X])
  7.2653 +  let ?c' = "(singular_subdivision p ^^ n) c"
  7.2654 +  show ?thesis
  7.2655 +  proof
  7.2656 +    show "homologous_rel p X S c ?c'"
  7.2657 +      apply (induction n, simp_all)
  7.2658 +      by (metis p homologous_rel_singular_subdivision homologous_rel_singular_relcycle homologous_rel_trans homologous_rel_sym)
  7.2659 +    then show "singular_relcycle p X S ?c'"
  7.2660 +      by (metis homologous_rel_singular_relcycle p)
  7.2661 +  next
  7.2662 +    fix f :: "(nat \<Rightarrow> real) \<Rightarrow> 'a"
  7.2663 +    assume "f \<in> Poly_Mapping.keys ?c'"
  7.2664 +    then show "\<exists>V\<in>\<C>. f ` standard_simplex p \<subseteq> V"
  7.2665 +      by (rule n [OF order_refl])
  7.2666 +  qed
  7.2667 +qed
  7.2668 +
  7.2669 +lemma excised_chain_exists:
  7.2670 +  fixes S :: "'a set"
  7.2671 +  assumes "X closure_of U \<subseteq> X interior_of T" "T \<subseteq> S" "singular_chain p (subtopology X S) c"
  7.2672 +  obtains n d e where "singular_chain p (subtopology X (S - U)) d"
  7.2673 +                      "singular_chain p (subtopology X T) e"
  7.2674 +                      "(singular_subdivision p ^^ n) c = d + e"
  7.2675 +proof -
  7.2676 +  have *: "\<exists>n d e. singular_chain p (subtopology X (S - U)) d \<and>
  7.2677 +                  singular_chain p (subtopology X T) e \<and>
  7.2678 +                  (singular_subdivision p ^^ n) c = d + e"
  7.2679 +    if c: "singular_chain p (subtopology X S) c"
  7.2680 +       and X: "X closure_of U \<subseteq> X interior_of T" "U \<subseteq> topspace X" and S: "T \<subseteq> S" "S \<subseteq> topspace X"
  7.2681 +       for p X c S and T U :: "'a set"
  7.2682 +  proof -
  7.2683 +    obtain n where n: "\<And>m f. \<lbrakk>n \<le> m; f \<in> Poly_Mapping.keys ((singular_subdivision p ^^ m) c)\<rbrakk>
  7.2684 +                             \<Longrightarrow> \<exists>V \<in> {S \<inter> X interior_of T, S - X closure_of U}. f ` standard_simplex p \<subseteq> V"
  7.2685 +      apply (rule sufficient_iterated_singular_subdivision_exists
  7.2686 +                   [of "{S \<inter> X interior_of T, S - X closure_of U}"])
  7.2687 +      using X S c
  7.2688 +      by (auto simp: topspace_subtopology openin_subtopology_Int2 openin_subtopology_diff_closed)
  7.2689 +    let ?c' = "\<lambda>n. (singular_subdivision p ^^ n) c"
  7.2690 +    have "singular_chain p (subtopology X S) (?c' m)" for m
  7.2691 +      by (induction m) (auto simp: singular_chain_singular_subdivision c)
  7.2692 +    then have scp: "singular_chain p (subtopology X S) (?c' n)" .
  7.2693 +
  7.2694 +    have SS: "Poly_Mapping.keys (?c' n) \<subseteq> singular_simplex_set p (subtopology X (S - U))
  7.2695 +                              \<union> singular_simplex_set p (subtopology X T)"
  7.2696 +    proof (clarsimp)
  7.2697 +      fix f
  7.2698 +      assume f: "f \<in> Poly_Mapping.keys ((singular_subdivision p ^^ n) c)"
  7.2699 +         and non: "\<not> singular_simplex p (subtopology X T) f"
  7.2700 +      show "singular_simplex p (subtopology X (S - U)) f"
  7.2701 +        using n [OF order_refl f] scp f non closure_of_subset [OF \<open>U \<subseteq> topspace X\<close>] interior_of_subset [of X T]
  7.2702 +        by (fastforce simp: image_subset_iff singular_simplex_subtopology singular_chain_def)
  7.2703 +    qed
  7.2704 +    show ?thesis
  7.2705 +       unfolding singular_chain_def using frag_split [OF SS] by metis
  7.2706 +  qed
  7.2707 +  have "(subtopology X (topspace X \<inter> S)) = (subtopology X S)"
  7.2708 +    by (metis subtopology_subtopology subtopology_topspace)
  7.2709 +  with assms have c: "singular_chain p (subtopology X (topspace X \<inter> S)) c"
  7.2710 +    by simp
  7.2711 +  have Xsub: "X closure_of (topspace X \<inter> U) \<subseteq> X interior_of (topspace X \<inter> T)"
  7.2712 +    using assms closure_of_restrict interior_of_restrict by fastforce
  7.2713 +  obtain n d e where
  7.2714 +    d: "singular_chain p (subtopology X (topspace X \<inter> S - topspace X \<inter> U)) d"
  7.2715 +    and e: "singular_chain p (subtopology X (topspace X \<inter> T)) e"
  7.2716 +    and de: "(singular_subdivision p ^^ n) c = d + e"
  7.2717 +    using *[OF c Xsub, simplified] assms by force
  7.2718 +  show thesis
  7.2719 +  proof
  7.2720 +    show "singular_chain p (subtopology X (S - U)) d"
  7.2721 +      by (metis d Diff_Int_distrib inf.cobounded2 singular_chain_mono)
  7.2722 +    show "singular_chain p (subtopology X T) e"
  7.2723 +      by (metis e inf.cobounded2 singular_chain_mono)
  7.2724 +    show "(singular_subdivision p ^^ n) c = d + e"
  7.2725 +      by (rule de)
  7.2726 +  qed
  7.2727 +qed
  7.2728 +
  7.2729 +
  7.2730 +lemma excised_relcycle_exists:
  7.2731 +  fixes S :: "'a set"
  7.2732 +  assumes X: "X closure_of U \<subseteq> X interior_of T" and "T \<subseteq> S"
  7.2733 +      and c: "singular_relcycle p (subtopology X S) T c"
  7.2734 +  obtains c' where "singular_relcycle p (subtopology X (S - U)) (T - U) c'"
  7.2735 +                   "homologous_rel p (subtopology X S) T c c'"
  7.2736 +proof -
  7.2737 +  have [simp]: "(S - U) \<inter> (T - U) = T - U" "S \<inter> T = T"
  7.2738 +    using \<open>T \<subseteq> S\<close> by auto
  7.2739 +  have scc: "singular_chain p (subtopology X S) c"
  7.2740 +    and scp1: "singular_chain (p - Suc 0) (subtopology X T) (chain_boundary p c)"
  7.2741 +    using c by (auto simp: singular_relcycle_def mod_subset_def subtopology_subtopology)
  7.2742 +  obtain n d e where d: "singular_chain p (subtopology X (S - U)) d"
  7.2743 +    and e: "singular_chain p (subtopology X T) e"
  7.2744 +    and de: "(singular_subdivision p ^^ n) c = d + e"
  7.2745 +    using excised_chain_exists [OF X \<open>T \<subseteq> S\<close> scc] .
  7.2746 +  have scSUd: "singular_chain (p - Suc 0) (subtopology X (S - U)) (chain_boundary p d)"
  7.2747 +    by (simp add: singular_chain_boundary d)
  7.2748 +  have sccn: "singular_chain p (subtopology X S) ((singular_subdivision p ^^ n) c)" for n
  7.2749 +    by (induction n) (auto simp: singular_chain_singular_subdivision scc)
  7.2750 +  have "singular_chain (p - Suc 0) (subtopology X T) (chain_boundary p ((singular_subdivision p ^^ n) c))"
  7.2751 +  proof (induction n)
  7.2752 +    case (Suc n)
  7.2753 +    then show ?case
  7.2754 +      by (simp add: singular_chain_singular_subdivision chain_boundary_singular_subdivision [OF sccn])
  7.2755 +  qed (auto simp: scp1)
  7.2756 +  then have "singular_chain (p - Suc 0) (subtopology X T) (chain_boundary p ((singular_subdivision p ^^ n) c - e))"
  7.2757 +    by (simp add: chain_boundary_diff singular_chain_diff singular_chain_boundary e)
  7.2758 +  with de have scTd: "singular_chain (p - Suc 0) (subtopology X T) (chain_boundary p d)"
  7.2759 +    by simp
  7.2760 +  show thesis
  7.2761 +  proof
  7.2762 +    have "singular_chain (p - Suc 0) X (chain_boundary p d)"
  7.2763 +      using scTd singular_chain_subtopology by blast
  7.2764 +    with scSUd scTd have "singular_chain (p - Suc 0) (subtopology X (T - U)) (chain_boundary p d)"
  7.2765 +      by (fastforce simp add: singular_chain_subtopology)
  7.2766 +    then show "singular_relcycle p (subtopology X (S - U)) (T - U) d"
  7.2767 +      by (auto simp: singular_relcycle_def mod_subset_def subtopology_subtopology d)
  7.2768 +    have "homologous_rel p (subtopology X S) T (c-0) ((singular_subdivision p ^^ n) c - e)"
  7.2769 +    proof (rule homologous_rel_diff)
  7.2770 +      show "homologous_rel p (subtopology X S) T c ((singular_subdivision p ^^ n) c)"
  7.2771 +      proof (induction n)
  7.2772 +        case (Suc n)
  7.2773 +        then show ?case
  7.2774 +          apply simp
  7.2775 +          apply (rule homologous_rel_trans)
  7.2776 +          using c homologous_rel_singular_relcycle_1 homologous_rel_singular_subdivision homologous_rel_sym by blast
  7.2777 +      qed auto
  7.2778 +      show "homologous_rel p (subtopology X S) T 0 e"
  7.2779 +        unfolding homologous_rel_def using e
  7.2780 +        by (intro singular_relboundary_diff singular_chain_imp_relboundary; simp add: subtopology_subtopology)
  7.2781 +    qed
  7.2782 +    with de show "homologous_rel p (subtopology X S) T c d"
  7.2783 +      by simp
  7.2784 +  qed
  7.2785 +qed
  7.2786 +
  7.2787 +end
  7.2788 +
     8.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Apr 09 11:24:47 2019 +0200
     8.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Apr 09 12:36:53 2019 +0100
     8.3 @@ -34,6 +34,9 @@
     8.4  
     8.5  subsection \<open>Continuity of the representation WRT an orthogonal basis\<close>
     8.6  
     8.7 +lemma orthogonal_Basis: "pairwise orthogonal Basis"
     8.8 +  by (simp add: inner_not_same_Basis orthogonal_def pairwise_def)
     8.9 +
    8.10  lemma representation_bound:
    8.11    fixes B :: "'N::real_inner set"
    8.12    assumes "finite B" "independent B" "b \<in> B" and orth: "pairwise orthogonal B"
     9.1 --- a/src/HOL/ROOT	Tue Apr 09 11:24:47 2019 +0200
     9.2 +++ b/src/HOL/ROOT	Tue Apr 09 12:36:53 2019 +0100
     9.3 @@ -63,6 +63,7 @@
     9.4      document_variants = "document:manual=-proof,-ML,-unimportant"]
     9.5    sessions
     9.6      "HOL-Library"
     9.7 +    "HOL-Algebra"
     9.8      "HOL-Computational_Algebra"
     9.9    theories
    9.10      Analysis