Theory Simplices

section‹Homology, I: Simplices›

theory "Simplices"
  imports
    "HOL-Analysis.Function_Metric"
    "HOL-Analysis.Abstract_Euclidean_Space"
    "HOL-Algebra.Free_Abelian_Groups"
begin

subsection‹Standard simplices, all of which are topological subspaces of @{text"R^n"}.      ›

type_synonym 'a chain = "((nat ⇒ real) ⇒ 'a) ⇒⇩0 int"

definition standard_simplex :: "nat ⇒ (nat ⇒ real) set" where
  "standard_simplex p ≡
    {x. (∀i. 0 ≤ x i ∧ x i ≤ 1) ∧ (∀i>p. x i = 0) ∧ (∑i≤p. x i) = 1}"

lemma topspace_standard_simplex:
  "topspace(subtopology (powertop_real UNIV) (standard_simplex p))
    = standard_simplex p"
  by simp

lemma basis_in_standard_simplex [simp]:
   "(λj. if j = i then 1 else 0) ∈ standard_simplex p ⟷ i ≤ p"
  by (auto simp: standard_simplex_def)

lemma nonempty_standard_simplex: "standard_simplex p ≠ {}"
  using basis_in_standard_simplex by blast

lemma standard_simplex_0: "standard_simplex 0 = {(λj. if j = 0 then 1 else 0)}"
  by (auto simp: standard_simplex_def)

lemma standard_simplex_mono:
  assumes "p ≤ q"
  shows "standard_simplex p ⊆ standard_simplex q"
  using assms
proof (clarsimp simp: standard_simplex_def)
  fix x :: "nat ⇒ real"
  assume "∀i. 0 ≤ x i ∧ x i ≤ 1" and "∀i>p. x i = 0" and "sum x {..p} = 1"
  then show "sum x {..q} = 1"
    using sum.mono_neutral_left [of "{..q}" "{..p}" x] assms by auto
qed

lemma closedin_standard_simplex:
   "closedin (powertop_real UNIV) (standard_simplex p)"
    (is "closedin ?X ?S")
proof -
  have eq: "standard_simplex p =
              (⋂i. {x. x ∈ topspace ?X ∧ x i ∈ {0..1}}) ∩
              (⋂i ∈ {p<..}. {x ∈ topspace ?X. x i ∈ {0}}) ∩
              {x ∈ topspace ?X. (∑i≤p. x i) ∈ {1}}"
    by (auto simp: standard_simplex_def topspace_product_topology)
  show ?thesis
    unfolding eq
    by (rule closedin_Int closedin_Inter continuous_map_sum
             continuous_map_product_projection closedin_continuous_map_preimage | force | clarify)+
qed

lemma standard_simplex_01: "standard_simplex p ⊆ UNIV →⇩E {0..1}"
  using standard_simplex_def by auto

lemma compactin_standard_simplex:
   "compactin (powertop_real UNIV) (standard_simplex p)"
proof (rule closed_compactin)
  show "compactin (powertop_real UNIV) (UNIV →⇩E {0..1})"
    by (simp add: compactin_PiE)
  show "standard_simplex p ⊆ UNIV →⇩E {0..1}"
    by (simp add: standard_simplex_01)
  show "closedin (powertop_real UNIV) (standard_simplex p)"
    by (simp add: closedin_standard_simplex)
qed

lemma convex_standard_simplex:
   "⟦x ∈ standard_simplex p; y ∈ standard_simplex p;
     0 ≤ u; u ≤ 1⟧
    ⟹ (λi. (1 - u) * x i + u * y i) ∈ standard_simplex p"
  by (simp add: standard_simplex_def sum.distrib convex_bound_le flip: sum_distrib_left)

lemma path_connectedin_standard_simplex:
   "path_connectedin (powertop_real UNIV) (standard_simplex p)"
proof -
  define g where "g ≡ λx y::nat⇒real. λu i. (1 - u) * x i + u * y i"
  have "continuous_map
                (subtopology euclideanreal {0..1}) (powertop_real UNIV)
                (g x y)"
    if "x ∈ standard_simplex p" "y ∈ standard_simplex p" for x y
    unfolding g_def continuous_map_componentwise
    by (force intro: continuous_intros)
  moreover
  have "g x y ` {0..1} ⊆ standard_simplex p" "g x y 0 = x" "g x y 1 = y"
    if "x ∈ standard_simplex p" "y ∈ standard_simplex p" for x y
    using that by (auto simp: convex_standard_simplex g_def)
  ultimately
  show ?thesis
    unfolding path_connectedin_def path_connected_space_def pathin_def
    by (metis continuous_map_in_subtopology euclidean_product_topology top_greatest topspace_euclidean topspace_euclidean_subtopology)
qed

lemma connectedin_standard_simplex:
   "connectedin (powertop_real UNIV) (standard_simplex p)"
  by (simp add: path_connectedin_imp_connectedin path_connectedin_standard_simplex)

subsection‹Face map›

definition simplical_face :: "nat ⇒ (nat ⇒ 'a) ⇒ nat ⇒ 'a::comm_monoid_add" where
   "simplical_face k x ≡ λi. if i < k then x i else if i = k then 0 else x(i -1)"

lemma simplical_face_in_standard_simplex:
  assumes "1 ≤ p" "k ≤ p" "x ∈ standard_simplex (p - Suc 0)"
  shows "(simplical_face k x) ∈ standard_simplex p"
proof -
  have x01: "⋀i. 0 ≤ x i ∧ x i ≤ 1" and sumx: "sum x {..p - Suc 0} = 1"
    using assms by (auto simp: standard_simplex_def simplical_face_def)
  have gg: "⋀g. sum g {..p} = sum g {..<k} + sum g {k..p}"
    using ‹k ≤ p› sum.union_disjoint [of "{..<k}" "{k..p}"]
    by (force simp: ivl_disj_un ivl_disj_int)
  have eq: "(∑i≤p. if i < k then x i else if i = k then 0 else x (i -1))
         = (∑i < k. x i) + (∑i ∈ {k..p}. if i = k then 0 else x (i -1))"
    by (simp add: gg)
  consider "k ≤ p - Suc 0" | "k = p"
    using ‹k ≤ p› by linarith
  then have "(∑i≤p. if i < k then x i else if i = k then 0 else x (i -1)) = 1"
  proof cases
    case 1
    have [simp]: "Suc (p - Suc 0) = p"
      using ‹1 ≤ p› by auto
    have "(∑i = k..p. if i = k then 0 else x (i -1)) = (∑i = k+1..p. if i = k then 0 else x (i -1))"
      by (rule sum.mono_neutral_right) auto
    also have "… = (∑i = k+1..p. x (i -1))"
      by simp
    also have "… = (∑i = k..p-1. x i)"
      using sum.atLeastAtMost_reindex [of Suc k "p-1" "λi. x (i - Suc 0)"] 1 by simp
    finally have eq2: "(∑i = k..p. if i = k then 0 else x (i -1)) = (∑i = k..p-1. x i)" .
    with 1 show ?thesis 
      by (metis (no_types, lifting) One_nat_def eq finite_atLeastAtMost finite_lessThan ivl_disj_int(4) ivl_disj_un(10) sum.union_disjoint sumx)
  next
    case 2
    have [simp]: "({..p} ∩ {x. x < p}) = {..p - Suc 0}"
      using assms by auto
    have "(∑i≤p. if i < p then x i else if i = k then 0 else x (i -1)) = (∑i≤p. if i < p then x i else 0)"
      by (rule sum.cong) (auto simp: 2)
    also have "… = sum x {..p-1}"
      by (simp add: sum.If_cases)
    also have "… = 1"
      by (simp add: sumx)
    finally show ?thesis
      using 2 by simp
  qed
  then show ?thesis
    using assms by (auto simp: standard_simplex_def simplical_face_def)
qed

subsection‹Singular simplices, forcing canonicity outside the intended domain›

definition singular_simplex :: "nat ⇒ 'a topology ⇒ ((nat ⇒ real) ⇒ 'a) ⇒ bool" where
 "singular_simplex p X f ≡
      continuous_map(subtopology (powertop_real UNIV) (standard_simplex p)) X f
    ∧ f ∈ extensional (standard_simplex p)"

abbreviation singular_simplex_set :: "nat ⇒ 'a topology ⇒ ((nat ⇒ real) ⇒ 'a) set" where
 "singular_simplex_set p X ≡ Collect (singular_simplex p X)"

lemma singular_simplex_empty:
   "topspace X = {} ⟹ ¬ singular_simplex p X f"
  by (simp add: singular_simplex_def continuous_map nonempty_standard_simplex)

lemma singular_simplex_mono:
   "⟦singular_simplex p (subtopology X T) f; T ⊆ S⟧ ⟹ singular_simplex p (subtopology X S) f"
  by (auto simp: singular_simplex_def continuous_map_in_subtopology)

lemma singular_simplex_subtopology:
   "singular_simplex p (subtopology X S) f ⟷
        singular_simplex p X f ∧ f ` (standard_simplex p) ⊆ S"
  by (auto simp: singular_simplex_def continuous_map_in_subtopology)

subsubsection‹Singular face›

definition singular_face :: "nat ⇒ nat ⇒ ((nat ⇒ real) ⇒ 'a) ⇒ (nat ⇒ real) ⇒ 'a"
  where "singular_face p k f ≡ restrict (f ∘ simplical_face k) (standard_simplex (p - Suc 0))"

lemma singular_simplex_singular_face:
  assumes f: "singular_simplex p X f" and "1 ≤ p" "k ≤ p"
  shows "singular_simplex (p - Suc 0) X (singular_face p k f)"
proof -
  let ?PT = "(powertop_real UNIV)"
  have 0: "simplical_face k ` standard_simplex (p - Suc 0) ⊆ standard_simplex p"
    using assms simplical_face_in_standard_simplex by auto
  have 1: "continuous_map (subtopology ?PT (standard_simplex (p - Suc 0)))
                          (subtopology ?PT (standard_simplex p))
                          (simplical_face k)"
  proof (clarsimp simp add: continuous_map_in_subtopology simplical_face_in_standard_simplex continuous_map_componentwise 0)
    fix i
    have "continuous_map ?PT euclideanreal (λx. if i < k then x i else if i = k then 0 else x (i -1))"
      by (auto intro: continuous_map_product_projection)
    then show "continuous_map (subtopology ?PT (standard_simplex (p - Suc 0))) euclideanreal
                              (λx. simplical_face k x i)"
      by (simp add: simplical_face_def continuous_map_from_subtopology)
  qed
  have 2: "continuous_map (subtopology ?PT (standard_simplex p)) X f"
    using assms(1) singular_simplex_def by blast
  show ?thesis
    by (simp add: singular_simplex_def singular_face_def continuous_map_compose [OF 1 2])
qed


subsection‹Singular chains›

definition singular_chain :: "[nat, 'a topology, 'a chain] ⇒ bool"
  where "singular_chain p X c ≡ Poly_Mapping.keys c ⊆ singular_simplex_set p X"

abbreviation singular_chain_set :: "[nat, 'a topology] ⇒ ('a chain) set"
  where "singular_chain_set p X ≡ Collect (singular_chain p X)"

lemma singular_chain_empty:
   "topspace X = {} ⟹ singular_chain p X c ⟷ c = 0"
  by (auto simp: singular_chain_def singular_simplex_empty subset_eq poly_mapping_eqI)

lemma singular_chain_mono:
   "⟦singular_chain p (subtopology X T) c;  T ⊆ S⟧
        ⟹ singular_chain p (subtopology X S) c"
  unfolding singular_chain_def using singular_simplex_mono by blast

lemma singular_chain_subtopology:
   "singular_chain p (subtopology X S) c ⟷
        singular_chain p X c ∧ (∀f ∈ Poly_Mapping.keys c. f ` (standard_simplex p) ⊆ S)"
  unfolding singular_chain_def
  by (fastforce simp add: singular_simplex_subtopology subset_eq)

lemma singular_chain_0 [iff]: "singular_chain p X 0"
  by (auto simp: singular_chain_def)

lemma singular_chain_of:
   "singular_chain p X (frag_of c) ⟷ singular_simplex p X c"
  by (auto simp: singular_chain_def)

lemma singular_chain_cmul:
   "singular_chain p X c ⟹ singular_chain p X (frag_cmul a c)"
  by (auto simp: singular_chain_def)

lemma singular_chain_minus:
   "singular_chain p X (-c) ⟷ singular_chain p X c"
  by (auto simp: singular_chain_def)

lemma singular_chain_add:
   "⟦singular_chain p X a; singular_chain p X b⟧ ⟹ singular_chain p X (a+b)"
  unfolding singular_chain_def
  using keys_add [of a b] by blast

lemma singular_chain_diff:
   "⟦singular_chain p X a; singular_chain p X b⟧ ⟹ singular_chain p X (a-b)"
  unfolding singular_chain_def
  using keys_diff [of a b] by blast

lemma singular_chain_sum:
   "(⋀i. i ∈ I ⟹ singular_chain p X (f i)) ⟹ singular_chain p X (∑i∈I. f i)"
  unfolding singular_chain_def
  using keys_sum [of f I] by blast

lemma singular_chain_extend:
   "(⋀c. c ∈ Poly_Mapping.keys x ⟹ singular_chain p X (f c))
        ⟹ singular_chain p X (frag_extend f x)"
  by (simp add: frag_extend_def singular_chain_cmul singular_chain_sum)

subsection‹Boundary homomorphism for singular chains›

definition chain_boundary :: "nat ⇒ ('a chain) ⇒ 'a chain"
  where "chain_boundary p c ≡
          (if p = 0 then 0 else
           frag_extend (λf. (∑k≤p. frag_cmul ((-1) ^ k) (frag_of(singular_face p k f)))) c)"

lemma singular_chain_boundary:
  assumes "singular_chain p X c"
  shows "singular_chain (p - Suc 0) X (chain_boundary p c)"
  unfolding chain_boundary_def
proof (clarsimp intro!: singular_chain_extend singular_chain_sum singular_chain_cmul)
  show "⋀d k. ⟦0 < p; d ∈ Poly_Mapping.keys c; k ≤ p⟧
       ⟹ singular_chain (p - Suc 0) X (frag_of (singular_face p k d))"
    using assms by (auto simp: singular_chain_def intro: singular_simplex_singular_face)
qed

lemma singular_chain_boundary_alt:
   "singular_chain (Suc p) X c ⟹ singular_chain p X (chain_boundary (Suc p) c)"
  using singular_chain_boundary by force

lemma chain_boundary_0 [simp]: "chain_boundary p 0 = 0"
  by (simp add: chain_boundary_def)

lemma chain_boundary_cmul:
   "chain_boundary p (frag_cmul k c) = frag_cmul k (chain_boundary p c)"
  by (auto simp: chain_boundary_def frag_extend_cmul)

lemma chain_boundary_minus:
   "chain_boundary p (- c) = - (chain_boundary p c)"
  by (metis chain_boundary_cmul frag_cmul_minus_one)

lemma chain_boundary_add:
   "chain_boundary p (a+b) = chain_boundary p a + chain_boundary p b"
  by (simp add: chain_boundary_def frag_extend_add)

lemma chain_boundary_diff:
   "chain_boundary p (a-b) = chain_boundary p a - chain_boundary p b"
  using chain_boundary_add [of p a "-b"]
  by (simp add: chain_boundary_minus)

lemma chain_boundary_sum:
   "chain_boundary p (sum g I) = sum (chain_boundary p ∘ g) I"
  by (induction I rule: infinite_finite_induct) (simp_all add: chain_boundary_add)

lemma chain_boundary_sum':
   "finite I ⟹ chain_boundary p (sum' g I) = sum' (chain_boundary p ∘ g) I"
  by (induction I rule: finite_induct) (simp_all add: chain_boundary_add)

lemma chain_boundary_of:
   "chain_boundary p (frag_of f) =
        (if p = 0 then 0
         else (∑k≤p. frag_cmul ((-1) ^ k) (frag_of(singular_face p k f))))"
  by (simp add: chain_boundary_def)

subsection‹Factoring out chains in a subtopology for relative homology›

definition mod_subset
  where "mod_subset p X ≡ {(a,b). singular_chain p X (a - b)}"

lemma mod_subset_empty [simp]:
   "(a,b) ∈ (mod_subset p (subtopology X {})) ⟷ a = b"
  by (simp add: mod_subset_def singular_chain_empty)

lemma mod_subset_refl [simp]: "(c,c) ∈ mod_subset p X"
  by (auto simp: mod_subset_def)

lemma mod_subset_cmul:
  assumes "(a,b) ∈ mod_subset p X"
  shows "(frag_cmul k a, frag_cmul k b) ∈ mod_subset p X"
  using assms
  by (simp add: mod_subset_def) (metis (no_types, lifting) add_diff_cancel diff_add_cancel frag_cmul_distrib2 singular_chain_cmul)

lemma mod_subset_add:
   "⟦(c1,c2) ∈ mod_subset p X; (d1,d2) ∈ mod_subset p X⟧ ⟹ (c1+d1, c2+d2) ∈ mod_subset p X"
  by (simp add: mod_subset_def add_diff_add singular_chain_add)

subsection‹Relative cycles $Z_pX (S)$ where $X$ is a topology and $S$ a subset ›

definition singular_relcycle :: "nat ⇒ 'a topology ⇒ 'a set ⇒ ('a chain) ⇒ bool"
  where "singular_relcycle p X S ≡
        λc. singular_chain p X c ∧ (chain_boundary p c, 0) ∈ mod_subset (p-1) (subtopology X S)"

abbreviation singular_relcycle_set
  where "singular_relcycle_set p X S ≡ Collect (singular_relcycle p X S)"

lemma singular_relcycle_restrict [simp]:
   "singular_relcycle p X (topspace X ∩ S) = singular_relcycle p X S"
proof -
  have eq: "subtopology X (topspace X ∩ S) = subtopology X S"
    by (metis subtopology_subtopology subtopology_topspace)
  show ?thesis
    by (force simp: singular_relcycle_def eq)
qed

lemma singular_relcycle:
   "singular_relcycle p X S c ⟷
    singular_chain p X c ∧ singular_chain (p-1) (subtopology X S) (chain_boundary p c)"
  by (simp add: singular_relcycle_def mod_subset_def)

lemma singular_relcycle_0 [simp]: "singular_relcycle p X S 0"
  by (auto simp: singular_relcycle_def)

lemma singular_relcycle_cmul:
   "singular_relcycle p X S c ⟹ singular_relcycle p X S (frag_cmul k c)"
  by (auto simp: singular_relcycle_def chain_boundary_cmul dest: singular_chain_cmul mod_subset_cmul)

lemma singular_relcycle_minus:
   "singular_relcycle p X S (-c) ⟷ singular_relcycle p X S c"
  by (simp add: chain_boundary_minus singular_chain_minus singular_relcycle)

lemma singular_relcycle_add:
   "⟦singular_relcycle p X S a; singular_relcycle p X S b⟧
        ⟹ singular_relcycle p X S (a+b)"
  by (simp add: singular_relcycle_def chain_boundary_add mod_subset_def singular_chain_add)

lemma singular_relcycle_sum:
   "⟦⋀i. i ∈ I ⟹ singular_relcycle p X S (f i)⟧
        ⟹ singular_relcycle p X S (sum f I)"
  by (induction I rule: infinite_finite_induct) (auto simp: singular_relcycle_add)

lemma singular_relcycle_diff:
   "⟦singular_relcycle p X S a; singular_relcycle p X S b⟧
        ⟹ singular_relcycle p X S (a-b)"
  by (metis singular_relcycle_add singular_relcycle_minus uminus_add_conv_diff)

lemma singular_cycle:
   "singular_relcycle p X {} c ⟷ singular_chain p X c ∧ chain_boundary p c = 0"
  using mod_subset_empty by (auto simp: singular_relcycle_def)

lemma singular_cycle_mono:
   "⟦singular_relcycle p (subtopology X T) {} c; T ⊆ S⟧
        ⟹ singular_relcycle p (subtopology X S) {} c"
  by (auto simp: singular_cycle elim: singular_chain_mono)


subsection‹Relative boundaries $B_p X S$, where $X$ is a topology and $S$ a subset.›

definition singular_relboundary :: "nat ⇒ 'a topology ⇒ 'a set ⇒ ('a chain) ⇒ bool"
  where
  "singular_relboundary p X S ≡
    λc. ∃d. singular_chain (Suc p) X d ∧ (chain_boundary (Suc p) d, c) ∈ (mod_subset p (subtopology X S))"

abbreviation singular_relboundary_set :: "nat ⇒ 'a topology ⇒ 'a set ⇒ ('a chain) set"
  where "singular_relboundary_set p X S ≡ Collect (singular_relboundary p X S)"

lemma singular_relboundary_restrict [simp]:
   "singular_relboundary p X (topspace X ∩ S) = singular_relboundary p X S"
  unfolding singular_relboundary_def
  by (metis (no_types, opaque_lifting) subtopology_subtopology subtopology_topspace)

lemma singular_relboundary_alt:
   "singular_relboundary p X S c ⟷
    (∃d e. singular_chain (Suc p) X d ∧ singular_chain p (subtopology X S) e ∧
           chain_boundary (Suc p) d = c + e)"
  unfolding singular_relboundary_def mod_subset_def by fastforce

lemma singular_relboundary:
   "singular_relboundary p X S c ⟷
    (∃d e. singular_chain (Suc p) X d ∧ singular_chain p (subtopology X S) e ∧
              (chain_boundary (Suc p) d) + e = c)"
  using singular_chain_minus
  by (fastforce simp add: singular_relboundary_alt)

lemma singular_boundary:
   "singular_relboundary p X {} c ⟷
    (∃d. singular_chain (Suc p) X d ∧ chain_boundary (Suc p) d = c)"
  by (meson mod_subset_empty singular_relboundary_def)

lemma singular_boundary_imp_chain:
   "singular_relboundary p X {} c ⟹ singular_chain p X c"
  by (auto simp: singular_relboundary singular_chain_boundary_alt singular_chain_empty)

lemma singular_boundary_mono:
   "⟦T ⊆ S; singular_relboundary p (subtopology X T) {} c⟧
        ⟹ singular_relboundary p (subtopology X S) {} c"
  by (metis mod_subset_empty singular_chain_mono singular_relboundary_def)

lemma singular_relboundary_imp_chain:
   "singular_relboundary p X S c ⟹ singular_chain p X c"
  unfolding singular_relboundary singular_chain_subtopology
  by (blast intro: singular_chain_add singular_chain_boundary_alt)

lemma singular_chain_imp_relboundary:
   "singular_chain p (subtopology X S) c ⟹ singular_relboundary p X S c"
  unfolding singular_relboundary_def
  using mod_subset_def singular_chain_minus by fastforce

lemma singular_relboundary_0 [simp]: "singular_relboundary p X S 0"
  unfolding singular_relboundary_def
  by (rule_tac x=0 in exI) auto

lemma singular_relboundary_cmul:
   "singular_relboundary p X S c ⟹ singular_relboundary p X S (frag_cmul a c)"
  unfolding singular_relboundary_def
  by (metis chain_boundary_cmul mod_subset_cmul singular_chain_cmul)

lemma singular_relboundary_minus:
   "singular_relboundary p X S (-c) ⟷ singular_relboundary p X S c"
  using singular_relboundary_cmul
  by (metis add.inverse_inverse frag_cmul_minus_one)

lemma singular_relboundary_add:
   "⟦singular_relboundary p X S a; singular_relboundary p X S b⟧ ⟹ singular_relboundary p X S (a+b)"
  unfolding singular_relboundary_def
  by (metis chain_boundary_add mod_subset_add singular_chain_add)

lemma singular_relboundary_diff:
   "⟦singular_relboundary p X S a; singular_relboundary p X S b⟧ ⟹ singular_relboundary p X S (a-b)"
  by (metis uminus_add_conv_diff singular_relboundary_minus singular_relboundary_add)

subsection‹The (relative) homology relation›

definition homologous_rel :: "[nat,'a topology,'a set,'a chain,'a chain] ⇒ bool"
  where "homologous_rel p X S ≡ λa b. singular_relboundary p X S (a-b)"

abbreviation homologous_rel_set
  where "homologous_rel_set p X S a ≡ Collect (homologous_rel p X S a)"

lemma homologous_rel_restrict [simp]:
   "homologous_rel p X (topspace X ∩ S) = homologous_rel p X S"
  unfolding homologous_rel_def by (metis singular_relboundary_restrict)

lemma homologous_rel_refl [simp]: "homologous_rel p X S c c"
  unfolding homologous_rel_def by auto

lemma homologous_rel_sym:
   "homologous_rel p X S a b = homologous_rel p X S b a"
  unfolding homologous_rel_def
  using singular_relboundary_minus by fastforce

lemma homologous_rel_trans:
  assumes "homologous_rel p X S b c" "homologous_rel p X S a b"
  shows "homologous_rel p X S a c"
  using homologous_rel_def
proof -
  have "singular_relboundary p X S (b - c)"
    using assms unfolding homologous_rel_def by blast
  moreover have "singular_relboundary p X S (b - a)"
    using assms by (meson homologous_rel_def homologous_rel_sym)
  ultimately have "singular_relboundary p X S (c - a)"
    using singular_relboundary_diff by fastforce
  then show ?thesis
    by (meson homologous_rel_def homologous_rel_sym)
qed

lemma homologous_rel_eq:
   "homologous_rel p X S a = homologous_rel p X S b ⟷
    homologous_rel p X S a b"
  using homologous_rel_sym homologous_rel_trans by fastforce

lemma homologous_rel_set_eq:
   "homologous_rel_set p X S a = homologous_rel_set p X S b ⟷
    homologous_rel p X S a b"
  by (metis homologous_rel_eq mem_Collect_eq)

lemma homologous_rel_singular_chain:
  "homologous_rel p X S a b ⟹ (singular_chain p X a ⟷ singular_chain p X b)"
  unfolding homologous_rel_def
  using singular_chain_diff singular_chain_add
  by (fastforce dest: singular_relboundary_imp_chain)

lemma homologous_rel_add:
   "⟦homologous_rel p X S a a'; homologous_rel p X S b b'⟧
        ⟹ homologous_rel p X S (a+b) (a'+b')"
  unfolding homologous_rel_def
  by (simp add: add_diff_add singular_relboundary_add)

lemma homologous_rel_diff:
  assumes "homologous_rel p X S a a'" "homologous_rel p X S b b'"
  shows "homologous_rel p X S (a - b) (a' - b')"
proof -
  have "singular_relboundary p X S ((a - a') - (b - b'))"
    using assms singular_relboundary_diff unfolding homologous_rel_def by blast
  then show ?thesis
    by (simp add: homologous_rel_def algebra_simps)
qed

lemma homologous_rel_sum:
  assumes f: "finite {i ∈ I. f i ≠ 0}" and g: "finite {i ∈ I. g i ≠ 0}"
    and h: "⋀i. i ∈ I ⟹ homologous_rel p X S (f i) (g i)"
  shows "homologous_rel p X S (sum f I) (sum g I)"
proof (cases "finite I")
  case True
  let ?L = "{i ∈ I. f i ≠ 0} ∪ {i ∈ I. g i ≠ 0}"
  have L: "finite ?L" "?L ⊆ I"
    using f g by blast+
  have "sum f I = sum f ?L"
    by (rule comm_monoid_add_class.sum.mono_neutral_right [OF True]) auto
  moreover have "sum g I = sum g ?L"
    by (rule comm_monoid_add_class.sum.mono_neutral_right [OF True]) auto
  moreover have *: "homologous_rel p X S (f i) (g i)" if "i ∈ ?L" for i
    using h that by auto
  have "homologous_rel p X S (sum f ?L) (sum g ?L)"
    using L
  proof induction
    case (insert j J)
    then show ?case
      by (simp add: h homologous_rel_add)
  qed auto
  ultimately show ?thesis
    by simp
qed auto


lemma chain_homotopic_imp_homologous_rel:
  assumes
   "⋀c. singular_chain p X c ⟹ singular_chain (Suc p) X' (h c)"
   "⋀c. singular_chain (p -1) (subtopology X S) c ⟹ singular_chain p (subtopology X' T) (h' c)"
   "⋀c. singular_chain p X c
             ⟹ (chain_boundary (Suc p) (h c)) + (h'(chain_boundary p c)) = f c - g c"
    "singular_relcycle p X S c"
  shows "homologous_rel p X' T (f c) (g c)"
proof -
  have "singular_chain p (subtopology X' T) (chain_boundary (Suc p) (h c) - (f c - g c))"
    using assms
    by (metis (no_types, lifting) add_diff_cancel_left' minus_diff_eq singular_chain_minus singular_relcycle)
  then show ?thesis
  using assms
    by (metis homologous_rel_def singular_relboundary singular_relcycle)
qed


subsection‹Show that all boundaries are cycles, the key "chain complex" property.›

lemma chain_boundary_boundary:
  assumes "singular_chain p X c"
  shows "chain_boundary (p - Suc 0) (chain_boundary p c) = 0"
proof (cases "p -1 = 0")
  case False
  then have "2 ≤ p"
    by auto
  show ?thesis
    using assms
    unfolding singular_chain_def
  proof (induction rule: frag_induction)
    case (one g)
    then have ss: "singular_simplex p X g"
      by simp
    have eql: "{..p} × {..p - Suc 0} ∩ {(x, y). y < x} = (λ(j,i). (Suc i, j)) ` {(i,j). i ≤ j ∧ j ≤ p -1}"
      using False
      by (auto simp: image_def) (metis One_nat_def diff_Suc_1 diff_le_mono le_refl lessE less_imp_le_nat)
    have eqr: "{..p} × {..p - Suc 0} - {(x, y). y < x} = {(i,j). i ≤ j ∧ j ≤ p -1}"
      by auto
    have eqf: "singular_face (p - Suc 0) i (singular_face p (Suc j) g) =
               singular_face (p - Suc 0) j (singular_face p i g)" if "i ≤ j" "j ≤ p - Suc 0" for i j
    proof (rule ext)
      fix t
      show "singular_face (p - Suc 0) i (singular_face p (Suc j) g) t =
            singular_face (p - Suc 0) j (singular_face p i g) t"
      proof (cases "t ∈ standard_simplex (p -1 -1)")
        case True
        have fi: "simplical_face i t ∈ standard_simplex (p - Suc 0)"
          using False True simplical_face_in_standard_simplex that by force
        have fj: "simplical_face j t ∈ standard_simplex (p - Suc 0)"
          by (metis False One_nat_def True simplical_face_in_standard_simplex less_one not_less that(2))
        have eq: "simplical_face (Suc j) (simplical_face i t) = simplical_face i (simplical_face j t)"
          using True that ss
          unfolding standard_simplex_def simplical_face_def by fastforce
        show ?thesis by (simp add: singular_face_def fi fj eq)
      qed (simp add: singular_face_def)
    qed
    show ?case
    proof (cases "p = 1")
      case False
      have eq0: "frag_cmul (-1) a = b ⟹ a + b = 0" for a b
        by (simp add: neg_eq_iff_add_eq_0)
      have *: "(∑x≤p. ∑i≤p - Suc 0.
                 frag_cmul ((-1) ^ (x + i)) (frag_of (singular_face (p - Suc 0) i (singular_face p x g))))
              = 0"
        apply (simp add: sum.cartesian_product sum.Int_Diff [of "_ × _" _ "{(x,y). y < x}"])
        apply (rule eq0)
        unfolding frag_cmul_sum prod.case_distrib [of "frag_cmul (-1)"] frag_cmul_cmul eql eqr 
        apply (force simp: inj_on_def sum.reindex add.commute eqf intro: sum.cong)
        done
      show ?thesis
        using False by (simp add: chain_boundary_of chain_boundary_sum chain_boundary_cmul frag_cmul_sum * flip: power_add)
    qed (simp add: chain_boundary_def)
  next
    case (diff a b)
    then show ?case
      by (simp add: chain_boundary_diff)
  qed auto
qed (simp add: chain_boundary_def)


lemma chain_boundary_boundary_alt:
   "singular_chain (Suc p) X c ⟹ chain_boundary p (chain_boundary (Suc p) c) = 0"
  using chain_boundary_boundary by force

lemma singular_relboundary_imp_relcycle:
  assumes "singular_relboundary p X S c"
  shows "singular_relcycle p X S c"
proof -
  obtain d e where d: "singular_chain (Suc p) X d"
               and e: "singular_chain p (subtopology X S) e"
               and c: "c = chain_boundary (Suc p) d + e"
    using assms by (auto simp: singular_relboundary singular_relcycle)
  have 1: "singular_chain (p - Suc 0) (subtopology X S) (chain_boundary p (chain_boundary (Suc p) d))"
    using d chain_boundary_boundary_alt by fastforce
  have 2: "singular_chain (p - Suc 0) (subtopology X S) (chain_boundary p e)"
    using ‹singular_chain p (subtopology X S) e› singular_chain_boundary by auto
  have "singular_chain p X c"
    using assms singular_relboundary_imp_chain by auto
  moreover have "singular_chain (p - Suc 0) (subtopology X S) (chain_boundary p c)"
    by (simp add: c chain_boundary_add singular_chain_add 1 2)
  ultimately show ?thesis
    by (simp add: singular_relcycle)
qed

lemma homologous_rel_singular_relcycle_1:
  assumes "homologous_rel p X S c1 c2" "singular_relcycle p X S c1"
  shows "singular_relcycle p X S c2"
  using assms
  by (metis diff_add_cancel homologous_rel_def homologous_rel_sym singular_relboundary_imp_relcycle singular_relcycle_add)

lemma homologous_rel_singular_relcycle:
  assumes "homologous_rel p X S c1 c2"
  shows "singular_relcycle p X S c1 = singular_relcycle p X S c2"
  using assms homologous_rel_singular_relcycle_1
  using homologous_rel_sym by blast


subsection‹Operations induced by a continuous map g between topological spaces›

definition simplex_map :: "nat ⇒ ('b ⇒ 'a) ⇒ ((nat ⇒ real) ⇒ 'b) ⇒ (nat ⇒ real) ⇒ 'a"
  where "simplex_map p g c ≡ restrict (g ∘ c) (standard_simplex p)"

lemma singular_simplex_simplex_map:
   "⟦singular_simplex p X f; continuous_map X X' g⟧
        ⟹ singular_simplex p X' (simplex_map p g f)"
  unfolding singular_simplex_def simplex_map_def
  by (auto simp: continuous_map_compose)

lemma simplex_map_eq:
   "⟦singular_simplex p X c;
     ⋀x. x ∈ topspace X ⟹ f x = g x⟧
    ⟹ simplex_map p f c = simplex_map p g c"
  by (auto simp: singular_simplex_def simplex_map_def continuous_map_def Pi_iff)

lemma simplex_map_id_gen:
   "⟦singular_simplex p X c;
     ⋀x. x ∈ topspace X ⟹ f x = x⟧
    ⟹ simplex_map p f c = c"
  unfolding singular_simplex_def simplex_map_def continuous_map_def
  using extensional_arb by fastforce

lemma simplex_map_id [simp]:
   "simplex_map p id = (λc. restrict c (standard_simplex p))"
  by (auto simp: simplex_map_def)

lemma simplex_map_compose:
   "simplex_map p (h ∘ g) = simplex_map p h ∘ simplex_map p g"
  unfolding simplex_map_def by force

lemma singular_face_simplex_map:
   "⟦1 ≤ p; k ≤ p⟧
        ⟹ singular_face p k (simplex_map p f c) = simplex_map (p - Suc 0) f (c ∘ simplical_face k)"
  unfolding simplex_map_def singular_face_def
  by (force simp: simplical_face_in_standard_simplex)

lemma singular_face_restrict [simp]:
  assumes "p > 0" "i ≤ p"
  shows "singular_face p i (restrict f (standard_simplex p)) = singular_face p i f"
  by (metis assms One_nat_def Suc_leI simplex_map_id singular_face_def singular_face_simplex_map)


definition chain_map :: "nat ⇒ ('b ⇒ 'a) ⇒ (((nat ⇒ real) ⇒ 'b) ⇒⇩0 int) ⇒ 'a chain"
  where "chain_map p g c ≡ frag_extend (frag_of ∘ simplex_map p g) c"

lemma singular_chain_chain_map:
   "⟦singular_chain p X c; continuous_map X X' g⟧ ⟹ singular_chain p X' (chain_map p g c)"
  unfolding chain_map_def
  by (force simp add: singular_chain_def subset_iff 
      intro!: singular_chain_extend singular_simplex_simplex_map)

lemma chain_map_0 [simp]: "chain_map p g 0 = 0"
  by (auto simp: chain_map_def)

lemma chain_map_of [simp]: "chain_map p g (frag_of f) = frag_of (simplex_map p g f)"
  by (simp add: chain_map_def)

lemma chain_map_cmul [simp]:
   "chain_map p g (frag_cmul a c) = frag_cmul a (chain_map p g c)"
  by (simp add: frag_extend_cmul chain_map_def)

lemma chain_map_minus: "chain_map p g (-c) = - (chain_map p g c)"
  by (simp add: frag_extend_minus chain_map_def)

lemma chain_map_add:
   "chain_map p g (a+b) = chain_map p g a + chain_map p g b"
  by (simp add: frag_extend_add chain_map_def)

lemma chain_map_diff:
   "chain_map p g (a-b) = chain_map p g a - chain_map p g b"
  by (simp add: frag_extend_diff chain_map_def)

lemma chain_map_sum:
   "finite I ⟹ chain_map p g (sum f I) = sum (chain_map p g ∘ f) I"
  by (simp add: frag_extend_sum chain_map_def)

lemma chain_map_eq:
   "⟦singular_chain p X c; ⋀x. x ∈ topspace X ⟹ f x = g x⟧
    ⟹ chain_map p f c = chain_map p g c"
  unfolding singular_chain_def
proof (induction rule: frag_induction)
  case (one x)
  then show ?case
    by (metis (no_types, lifting) chain_map_of mem_Collect_eq simplex_map_eq)
qed (auto simp: chain_map_diff)

lemma chain_map_id_gen:
   "⟦singular_chain p X c; ⋀x. x ∈ topspace X ⟹ f x = x⟧
    ⟹  chain_map p f c = c"
  unfolding singular_chain_def
  by (erule frag_induction) (auto simp: chain_map_diff simplex_map_id_gen)

lemma chain_map_ident:
   "singular_chain p X c ⟹ chain_map p id c = c"
  by (simp add: chain_map_id_gen)

lemma chain_map_id:
   "chain_map p id = frag_extend (frag_of ∘ (λf. restrict f (standard_simplex p)))"
  by (auto simp: chain_map_def)

lemma chain_map_compose:
   "chain_map p (h ∘ g) = chain_map p h ∘ chain_map p g"
proof
  show "chain_map p (h ∘ g) c = (chain_map p h ∘ chain_map p g) c" for c
    using subset_UNIV
  proof (induction c rule: frag_induction)
    case (one x)
    then show ?case
      by simp (metis (mono_tags, lifting) comp_eq_dest_lhs restrict_apply simplex_map_def)
  next
    case (diff a b)
    then show ?case
      by (simp add: chain_map_diff)
  qed auto
qed

lemma singular_simplex_chain_map_id:
  assumes "singular_simplex p X f"
  shows "chain_map p f (frag_of (restrict id (standard_simplex p))) = frag_of f"
proof -
  have "(restrict (f ∘ restrict id (standard_simplex p)) (standard_simplex p)) = f"
    by (rule ext) (metis assms comp_apply extensional_arb id_apply restrict_apply singular_simplex_def)
  then show ?thesis
    by (simp add: simplex_map_def)
qed

lemma chain_boundary_chain_map:
  assumes "singular_chain p X c"
  shows "chain_boundary p (chain_map p g c) = chain_map (p - Suc 0) g (chain_boundary p c)"
  using assms unfolding singular_chain_def
proof (induction c rule: frag_induction)
  case (one x)
  then have "singular_face p i (simplex_map p g x) = simplex_map (p - Suc 0) g (singular_face p i x)"
    if "0 ≤ i" "i ≤ p" "p ≠ 0" for i
    using that
    by (fastforce simp add: singular_face_def simplex_map_def simplical_face_in_standard_simplex)
  then show ?case
    by (auto simp: chain_boundary_of chain_map_sum)
next
  case (diff a b)
  then show ?case
    by (simp add: chain_boundary_diff chain_map_diff)
qed auto

lemma singular_relcycle_chain_map:
  assumes "singular_relcycle p X S c" "continuous_map X X' g" "g ` S ⊆ T"
  shows "singular_relcycle p X' T (chain_map p g c)"
proof -
  have "continuous_map (subtopology X S) (subtopology X' T) g"
    using assms
    using continuous_map_from_subtopology continuous_map_in_subtopology topspace_subtopology by fastforce
  then show ?thesis
    using chain_boundary_chain_map [of p X c g]
    by (metis One_nat_def assms(1) assms(2) singular_chain_chain_map singular_relcycle)
qed

lemma singular_relboundary_chain_map:
  assumes "singular_relboundary p X S c" "continuous_map X X' g" "g ` S ⊆ T"
  shows "singular_relboundary p X' T (chain_map p g c)"
proof -
  obtain d e where d: "singular_chain (Suc p) X d"
    and e: "singular_chain p (subtopology X S) e" and c: "c = chain_boundary (Suc p) d + e"
    using assms by (auto simp: singular_relboundary)
  have "singular_chain (Suc p) X' (chain_map (Suc p) g d)"
    using assms(2) d singular_chain_chain_map by blast
  moreover have "singular_chain p (subtopology X' T) (chain_map p g e)"
  proof -
    have "∀t. g ` topspace (subtopology t S) ⊆ T"
      by (metis assms(3) closure_of_subset_subtopology closure_of_topspace dual_order.trans image_mono)
    then show ?thesis
      by (meson assms(2) continuous_map_from_subtopology continuous_map_in_subtopology e singular_chain_chain_map)
  qed
  moreover have "chain_boundary (Suc p) (chain_map (Suc p) g d) + chain_map p g e =
                 chain_map p g (chain_boundary (Suc p) d + e)"
    by (metis One_nat_def chain_boundary_chain_map chain_map_add d diff_Suc_1)
  ultimately show ?thesis
    unfolding singular_relboundary
    using c by blast
qed


subsection‹Homology of one-point spaces degenerates except for $p = 0$.›

lemma singular_simplex_singleton:
  assumes "topspace X = {a}"
  shows "singular_simplex p X f ⟷ f = restrict (λx. a) (standard_simplex p)" (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  then show ?rhs
  proof -
    have "continuous_map (subtopology (product_topology (λn. euclideanreal) UNIV) (standard_simplex p)) X f"
      using ‹singular_simplex p X f› singular_simplex_def by blast
    then have "⋀c. c ∉ standard_simplex p ∨ f c = a"
      by (simp add: assms continuous_map_def Pi_iff)
    then show ?thesis
      by (metis (no_types) L extensional_restrict restrict_ext singular_simplex_def)
  qed
next
  assume ?rhs
  with assms show ?lhs
    by (auto simp: singular_simplex_def)
qed

lemma singular_chain_singleton:
  assumes "topspace X = {a}"
  shows "singular_chain p X c ⟷
         (∃b. c = frag_cmul b (frag_of(restrict (λx. a) (standard_simplex p))))"
    (is "?lhs = ?rhs")
proof
  let ?f = "restrict (λx. a) (standard_simplex p)"
  assume L: ?lhs
  with assms have "Poly_Mapping.keys c ⊆ {?f}"
    by (auto simp: singular_chain_def singular_simplex_singleton)
  then consider "Poly_Mapping.keys c = {}" | "Poly_Mapping.keys c = {?f}"
    by blast
  then show ?rhs
  proof cases
    case 1
    with L show ?thesis
      by (metis frag_cmul_zero keys_eq_empty)
  next
    case 2
    then have "∃b. frag_extend frag_of c = frag_cmul b (frag_of (λx∈standard_simplex p. a))"
      by (force simp: frag_extend_def)
    then show ?thesis
      by (metis frag_expansion)
  qed
next
  assume ?rhs
  with assms show ?lhs
    by (auto simp: singular_chain_def singular_simplex_singleton)
qed

lemma chain_boundary_of_singleton:
  assumes tX: "topspace X = {a}" and sc: "singular_chain p X c"
  shows "chain_boundary p c =
         (if p = 0 ∨ odd p then 0
          else frag_extend (λf. frag_of(restrict (λx. a) (standard_simplex (p -1)))) c)"
    (is "?lhs = ?rhs")
proof (cases "p = 0")
  case False
  have "?lhs = frag_extend (λf. if odd p then 0 else frag_of(restrict (λx. a) (standard_simplex (p -1)))) c"
  proof (simp only: chain_boundary_def False if_False, rule frag_extend_eq)
    fix f
    assume "f ∈ Poly_Mapping.keys c"
    with assms have "singular_simplex p X f"
      by (auto simp: singular_chain_def)
    then have *: "⋀k. k ≤ p ⟹ singular_face p k f = (λx∈standard_simplex (p -1). a)"
      using False singular_simplex_singular_face 
      by (fastforce simp flip: singular_simplex_singleton [OF tX])
    define c where "c ≡ frag_of (λx∈standard_simplex (p -1). a)"
    have "(∑k≤p. frag_cmul ((-1) ^ k) (frag_of (singular_face p k f)))
        = (∑k≤p. frag_cmul ((-1) ^ k) c)"
      by (auto simp: c_def * intro: sum.cong)
    also have "… = (if odd p then 0 else c)"
      by (induction p) (auto simp: c_def restrict_def)
    finally show "(∑k≤p. frag_cmul ((-1) ^ k) (frag_of (singular_face p k f)))
                = (if odd p then 0 else frag_of (λx∈standard_simplex (p -1). a))"
      unfolding c_def .
  qed
  also have "… = ?rhs"
    by (auto simp: False frag_extend_eq_0)
  finally show ?thesis .
qed (simp add: chain_boundary_def)


lemma singular_cycle_singleton:
  assumes "topspace X = {a}"
  shows "singular_relcycle p X {} c ⟷ singular_chain p X c ∧ (p = 0 ∨ odd p ∨ c = 0)"
proof -
  have "c = 0" if "singular_chain p X c" and "chain_boundary p c = 0" and "even p" and "p ≠ 0"
    using that assms singular_chain_singleton [of X a p c] chain_boundary_of_singleton [OF assms]
    by (auto simp: frag_extend_cmul)
  moreover
  have "chain_boundary p c = 0" if sc: "singular_chain p X c" and "odd p"
    by (simp add: chain_boundary_of_singleton [OF assms sc] that)
  moreover have "chain_boundary 0 c = 0" if "singular_chain 0 X c" and "p = 0"
    by (simp add: chain_boundary_def)
  ultimately show ?thesis
  using assms by (auto simp: singular_cycle)
qed


lemma singular_boundary_singleton:
  assumes "topspace X = {a}"
  shows "singular_relboundary p X {} c ⟷ singular_chain p X c ∧ (odd p ∨ c = 0)"
proof (cases "singular_chain p X c")
  case True
  have "∃d. singular_chain (Suc p) X d ∧ chain_boundary (Suc p) d = c"
    if "singular_chain p X c" and "odd p"
  proof -
    obtain b where b: "c = frag_cmul b (frag_of(restrict (λx. a) (standard_simplex p)))"
      by (metis True assms singular_chain_singleton)
    let ?d = "frag_cmul b (frag_of (λx∈standard_simplex (Suc p). a))"
    have scd: "singular_chain (Suc p) X ?d"
      by (metis assms singular_chain_singleton)
    moreover have "chain_boundary (Suc p) ?d = c"
      by (simp add: assms scd chain_boundary_of_singleton [of X a "Suc p"] b frag_extend_cmul ‹odd p›)
    ultimately show ?thesis
      by metis
  qed
  with True assms show ?thesis
    by (auto simp: singular_boundary chain_boundary_of_singleton)
next
  case False
  with assms singular_boundary_imp_chain show ?thesis
    by metis
qed


lemma singular_boundary_eq_cycle_singleton:
  assumes "topspace X = {a}" "1 ≤ p"
  shows "singular_relboundary p X {} c ⟷ singular_relcycle p X {} c" (is "?lhs = ?rhs")
proof
  show "?lhs ⟹ ?rhs"
    by (simp add: singular_relboundary_imp_relcycle)
  show "?rhs ⟹ ?lhs"
    by (metis assms not_one_le_zero singular_boundary_singleton singular_cycle_singleton)
qed

lemma singular_boundary_set_eq_cycle_singleton:
  assumes "topspace X = {a}" "1 ≤ p"
  shows "singular_relboundary_set p X {} = singular_relcycle_set p X {}"
  using singular_boundary_eq_cycle_singleton [OF assms]
  by blast

subsection‹Simplicial chains›

text‹Simplicial chains, effectively those resulting from linear maps.
 We still allow the map to be singular, so the name is questionable.
These are intended as building-blocks for singular subdivision, rather  than as a axis
for 1 simplicial homology.›

definition oriented_simplex
  where "oriented_simplex p l ≡ (λx∈standard_simplex p. λi. (∑j≤p. l j i * x j))"

definition simplicial_simplex
  where
 "simplicial_simplex p S f ≡
        singular_simplex p (subtopology (powertop_real UNIV) S) f ∧
        (∃l. f = oriented_simplex p l)"

lemma simplicial_simplex:
  "simplicial_simplex p S f ⟷ f ` (standard_simplex p) ⊆ S ∧ (∃l. f = oriented_simplex p l)"
  (is "?lhs = ?rhs")
proof
  assume R: ?rhs  
  have "continuous_map (subtopology (powertop_real UNIV) (standard_simplex p))
                (powertop_real UNIV) (λx i. ∑j≤p. l j i * x j)" for l :: " nat ⇒ 'a ⇒ real"
    unfolding continuous_map_componentwise
    by (force intro: continuous_intros continuous_map_from_subtopology continuous_map_product_projection)
  with R show ?lhs
    unfolding simplicial_simplex_def singular_simplex_subtopology
    by (auto simp add: singular_simplex_def oriented_simplex_def)
qed (simp add: simplicial_simplex_def singular_simplex_subtopology)

lemma simplicial_simplex_empty [simp]: "¬ simplicial_simplex p {} f"
  by (simp add: nonempty_standard_simplex simplicial_simplex)

definition simplicial_chain
  where "simplicial_chain p S c ≡ Poly_Mapping.keys c ⊆ Collect (simplicial_simplex p S)"

lemma simplicial_chain_0 [simp]: "simplicial_chain p S 0"
  by (simp add: simplicial_chain_def)

lemma simplicial_chain_of [simp]:
   "simplicial_chain p S (frag_of c) ⟷ simplicial_simplex p S c"
  by (simp add: simplicial_chain_def)

lemma simplicial_chain_cmul:
   "simplicial_chain p S c ⟹ simplicial_chain p S (frag_cmul a c)"
  by (auto simp: simplicial_chain_def)

lemma simplicial_chain_diff:
   "⟦simplicial_chain p S c1; simplicial_chain p S c2⟧ ⟹ simplicial_chain p S (c1 - c2)"
  unfolding simplicial_chain_def  by (meson UnE keys_diff subset_iff)

lemma simplicial_chain_sum:
   "(⋀i. i ∈ I ⟹ simplicial_chain p S (f i)) ⟹ simplicial_chain p S (sum f I)"
  unfolding simplicial_chain_def
  using order_trans [OF keys_sum [of f I]]
  by (simp add: UN_least)

lemma simplicial_simplex_oriented_simplex:
   "simplicial_simplex p S (oriented_simplex p l)
    ⟷ ((λx i. ∑j≤p. l j i * x j) ` standard_simplex p ⊆ S)"
  by (auto simp: simplicial_simplex oriented_simplex_def)

lemma simplicial_imp_singular_simplex:
   "simplicial_simplex p S f
      ⟹ singular_simplex p (subtopology (powertop_real UNIV) S) f"
  by (simp add: simplicial_simplex_def)

lemma simplicial_imp_singular_chain:
   "simplicial_chain p S c
      ⟹ singular_chain p (subtopology (powertop_real UNIV) S) c"
  unfolding simplicial_chain_def singular_chain_def
  by (auto intro: simplicial_imp_singular_simplex)

lemma oriented_simplex_eq:
  "oriented_simplex p l = oriented_simplex p l' ⟷ (∀i. i ≤ p ⟶ l i = l' i)"
  (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  show ?rhs
  proof clarify
    fix i
    assume "i ≤ p"
    let ?fi = "(λj. if j = i then 1 else 0)"
    have "(∑j≤p. l j k * ?fi j) = (∑j≤p. l' j k * ?fi j)" for k
      using L ‹i ≤ p›
      by (simp add: fun_eq_iff oriented_simplex_def split: if_split_asm)
    with ‹i ≤ p› show "l i = l' i"
      by (simp add: if_distrib ext cong: if_cong)
  qed
qed (auto simp: oriented_simplex_def)

lemma singular_face_oriented_simplex:
  assumes "1 ≤ p" "k ≤ p"
  shows "singular_face p k (oriented_simplex p l) =
         oriented_simplex (p -1) (λj. if j < k then l j else l (Suc j))"
proof -
  have "(∑j≤p. l j i * simplical_face k x j)
      = (∑j≤p - Suc 0. (if j < k then l j else l (Suc j)) i * x j)"
    if "x ∈ standard_simplex (p - Suc 0)" for i x
  proof -
    show ?thesis
      unfolding simplical_face_def
      using sum.zero_middle [OF assms, where 'a=real, symmetric]
      by (simp add: if_distrib [of "λx. _ * x"] if_distrib [of "λf. f i * _"] atLeast0AtMost cong: if_cong)
  qed
  then show ?thesis
    using simplical_face_in_standard_simplex assms
    by (auto simp: singular_face_def oriented_simplex_def restrict_def)
qed

lemma simplicial_simplex_singular_face:
  fixes f :: "(nat ⇒ real) ⇒ nat ⇒ real"
  assumes ss: "simplicial_simplex p S f" and p: "1 ≤ p" "k ≤ p"
  shows "simplicial_simplex (p - Suc 0) S (singular_face p k f)"
proof -
  let ?X = "subtopology (powertop_real UNIV) S"
  obtain m where l: "singular_simplex p ?X (oriented_simplex p m)"
       and feq: "f = oriented_simplex p m"
    using assms by (force simp: simplicial_simplex_def)
  moreover   
  have "singular_face p k f = oriented_simplex (p - Suc 0) (λi. if i < k then m i else m (Suc i))"
    unfolding feq singular_face_def oriented_simplex_def
    apply (simp add: simplical_face_in_standard_simplex [OF p] restrict_compose_left subset_eq)
    using sum.zero_middle [OF p, where 'a=real, symmetric]  unfolding simplical_face_def o_def
    apply (simp add: if_distrib [of "λx. _ * x"] if_distrib [of "λf. f _ * _"] atLeast0AtMost cong: if_cong)
    done
  ultimately
  show ?thesis
    using p simplicial_simplex_def singular_simplex_singular_face by blast
qed

lemma simplicial_chain_boundary:
   "simplicial_chain p S c ⟹ simplicial_chain (p -1) S (chain_boundary p c)"
  unfolding simplicial_chain_def
proof (induction rule: frag_induction)
  case (one f)
  then have "simplicial_simplex p S f"
    by simp
  have "simplicial_chain (p - Suc 0) S (frag_of (singular_face p i f))"
    if "0 < p" "i ≤ p" for i
    using that one
    by (force simp: simplicial_simplex_def singular_simplex_singular_face singular_face_oriented_simplex)
  then have "simplicial_chain (p - Suc 0) S (chain_boundary p (frag_of f))"
    unfolding chain_boundary_def frag_extend_of
    by (auto intro!: simplicial_chain_cmul simplicial_chain_sum)
  then show ?case
    by (simp add: simplicial_chain_def [symmetric])
next
  case (diff a b)
  then show ?case
    by (metis chain_boundary_diff simplicial_chain_def simplicial_chain_diff)
qed auto


subsection‹The cone construction on simplicial simplices.›

consts simplex_cone :: "[nat, nat ⇒ real, [nat ⇒ real, nat] ⇒ real, nat ⇒ real, nat] ⇒ real"
specification (simplex_cone)
  simplex_cone:
    "⋀p v l. simplex_cone p v (oriented_simplex p l) =
          oriented_simplex (Suc p) (λi. if i = 0 then v else l(i -1))"
proof -
  have *: "⋀x. ∃y. ∀v. (λl. oriented_simplex (Suc x) (λi. if i = 0 then v else l (i -1)))
                  = (y v ∘ (oriented_simplex x))"
    apply (subst choice_iff [symmetric])
    by (simp add: oriented_simplex_eq  choice_iff [symmetric] function_factors_left [symmetric])
  then show ?thesis
    unfolding o_def by (metis(no_types))
qed

lemma simplicial_simplex_simplex_cone:
  assumes f: "simplicial_simplex p S f"
    and T: "⋀x u. ⟦0 ≤ u; u ≤ 1; x ∈ S⟧ ⟹ (λi. (1 - u) * v i + u * x i) ∈ T"
  shows "simplicial_simplex (Suc p) T (simplex_cone p v f)"
proof -
  obtain l where l: "⋀x. x ∈ standard_simplex p ⟹ oriented_simplex p l x ∈ S"
    and feq: "f = oriented_simplex p l"
    using f by (auto simp: simplicial_simplex)
  have "oriented_simplex p l x ∈ S" if "x ∈ standard_simplex p" for x
    using f that by (auto simp: simplicial_simplex feq)
  then have S: "⋀x. ⟦⋀i. 0 ≤ x i ∧ x i ≤ 1; ⋀i. i>p ⟹ x i = 0; sum x {..p} = 1⟧
                 ⟹ (λi. ∑j≤p. l j i * x j) ∈ S"
    by (simp add: oriented_simplex_def standard_simplex_def)
  have "oriented_simplex (Suc p) (λi. if i = 0 then v else l (i -1)) x ∈ T"
    if "x ∈ standard_simplex (Suc p)" for x
  proof (simp add: that oriented_simplex_def sum.atMost_Suc_shift del: sum.atMost_Suc)
    have x01: "⋀i. 0 ≤ x i ∧ x i ≤ 1" and x0: "⋀i. i > Suc p ⟹ x i = 0" and x1: "sum x {..Suc p} = 1"
      using that by (auto simp: oriented_simplex_def standard_simplex_def)
    obtain a where "a ∈ S"
      using f by force
    show "(λi. v i * x 0 + (∑j≤p. l j i * x (Suc j))) ∈ T"
    proof (cases "x 0 = 1")
      case True
      then have "sum x {Suc 0..Suc p} = 0"
        using x1 by (simp add: atMost_atLeast0 sum.atLeast_Suc_atMost)
      then have [simp]: "x (Suc j) = 0" if "j≤p" for j
        unfolding sum.atLeast_Suc_atMost_Suc_shift
        using x01 that by (simp add: sum_nonneg_eq_0_iff)
      then show ?thesis
        using T [of 0 a] ‹a ∈ S› by (auto simp: True)
    next
      case False
      then have "(λi. v i * x 0 + (∑j≤p. l j i * x (Suc j))) = (λi. (1 - (1 - x 0)) * v i + (1 - x 0) * (inverse (1 - x 0) * (∑j≤p. l j i * x (Suc j))))"
        by (force simp: field_simps)
      also have "… ∈ T"
      proof (rule T)
        have "x 0 < 1"
          by (simp add: False less_le x01)
        have xle: "x (Suc i) ≤ (1 - x 0)" for i
        proof (cases "i ≤ p")
          case True
          have "sum x {0, Suc i} ≤ sum x {..Suc p}"
            by (rule sum_mono2) (auto simp: True x01)
          then show ?thesis
           using x1 x01 by (simp add: algebra_simps not_less)
        qed (simp add: x0 x01)
        have "(λi. (∑j≤p. l j i * (x (Suc j) * inverse (1 - x 0)))) ∈ S"
        proof (rule S)
          have "x 0 + (∑j≤p. x (Suc j)) = sum x {..Suc p}"
            by (metis sum.atMost_Suc_shift)
          with x1 have "(∑j≤p. x (Suc j)) = 1 - x 0"
            by simp
          with False show "(∑j≤p. x (Suc j) * inverse (1 - x 0)) = 1"
            by (metis add_diff_cancel_left' diff_diff_eq2 diff_zero right_inverse sum_distrib_right)
      qed (use x01 x0 xle ‹x 0 < 1› in ‹auto simp: field_split_simps›)
      then show "(λi. inverse (1 - x 0) * (∑j≤p. l j i * x (Suc j))) ∈ S"
        by (simp add: field_simps sum_divide_distrib)
    qed (use x01 in auto)
    finally show ?thesis .
  qed
qed
  then show ?thesis
    by (auto simp: simplicial_simplex feq  simplex_cone)
qed

definition simplicial_cone
  where "simplicial_cone p v ≡ frag_extend (frag_of ∘ simplex_cone p v)"

lemma simplicial_chain_simplicial_cone:
  assumes c: "simplicial_chain p S c"
    and T: "⋀x u. ⟦0 ≤ u; u ≤ 1; x ∈ S⟧ ⟹ (λi. (1 - u) * v i + u * x i) ∈ T"
  shows "simplicial_chain (Suc p) T (simplicial_cone p v c)"
  using c unfolding simplicial_chain_def simplicial_cone_def
proof (induction rule: frag_induction)
  case (one x)
  then show ?case
    by (simp add: T simplicial_simplex_simplex_cone)
next
  case (diff a b)
  then show ?case
    by (metis frag_extend_diff simplicial_chain_def simplicial_chain_diff)
qed auto


lemma chain_boundary_simplicial_cone_of':
  assumes "f = oriented_simplex p l"
  shows "chain_boundary (Suc p) (simplicial_cone p v (frag_of f)) =
         frag_of f
         - (if p = 0 then frag_of (λu∈standard_simplex p. v)
            else simplicial_cone (p -1) v (chain_boundary p (frag_of f)))"
proof (simp, intro impI conjI)
  assume "p = 0"
  have eq: "(oriented_simplex 0 (λj. if j = 0 then v else l j)) = (λu∈standard_simplex 0. v)"
    by (force simp: oriented_simplex_def standard_simplex_def)
  show "chain_boundary (Suc 0) (simplicial_cone 0 v (frag_of f))
        = frag_of f - frag_of (λu∈standard_simplex 0. v)"
    by (simp add: assms simplicial_cone_def chain_boundary_of ‹p = 0› simplex_cone singular_face_oriented_simplex eq cong: if_cong)
next
  assume "0 < p"
  have 0: "simplex_cone (p - Suc 0) v (singular_face p x (oriented_simplex p l))
         = oriented_simplex p
              (λj. if j < Suc x
                   then if j = 0 then v else l (j -1)
                   else if Suc j = 0 then v else l (Suc j -1))" if "x ≤ p" for x
    using ‹0 < p› that
    by (auto simp: Suc_leI singular_face_oriented_simplex simplex_cone oriented_simplex_eq)
  have 1: "frag_extend (frag_of ∘ simplex_cone (p - Suc 0) v)
                     (∑k = 0..p. frag_cmul ((-1) ^ k) (frag_of (singular_face p k (oriented_simplex p l))))
         = - (∑k = Suc 0..Suc p. frag_cmul ((-1) ^ k)
               (frag_of (singular_face (Suc p) k (simplex_cone p v (oriented_simplex p l)))))"
    unfolding sum.atLeast_Suc_atMost_Suc_shift
    by (auto simp: 0 simplex_cone singular_face_oriented_simplex frag_extend_sum frag_extend_cmul simp flip: sum_negf)
  moreover have 2: "singular_face (Suc p) 0 (simplex_cone p v (oriented_simplex p l))
                    = oriented_simplex p l"
    by (simp add: simplex_cone singular_face_oriented_simplex)
  show "chain_boundary (Suc p) (simplicial_cone p v (frag_of f))
        = frag_of f - simplicial_cone (p - Suc 0) v (chain_boundary p (frag_of f))"
    using ‹p > 0›
    apply (simp add: assms simplicial_cone_def chain_boundary_of atMost_atLeast0 del: sum.atMost_Suc)
    apply (subst sum.atLeast_Suc_atMost [of 0])
     apply (simp_all add: 1 2 del: sum.atMost_Suc)
    done
qed

lemma chain_boundary_simplicial_cone_of:
  assumes "simplicial_simplex p S f"
  shows "chain_boundary (Suc p) (simplicial_cone p v (frag_of f)) =
         frag_of f
         - (if p = 0 then frag_of (λu∈standard_simplex p. v)
            else simplicial_cone (p -1) v (chain_boundary p (frag_of f)))"
  using chain_boundary_simplicial_cone_of' assms unfolding simplicial_simplex_def
  by blast

lemma chain_boundary_simplicial_cone:
  "simplicial_chain p S c
   ⟹ chain_boundary (Suc p) (simplicial_cone p v c) =
       c - (if p = 0 then frag_extend (λf. frag_of (λu∈standard_simplex p. v)) c
            else simplicial_cone (p -1) v (chain_boundary p c))"
  unfolding simplicial_chain_def
proof (induction rule: frag_induction)
  case (one x)
  then show ?case
    by (auto simp: chain_boundary_simplicial_cone_of)
qed (auto simp: chain_boundary_diff simplicial_cone_def frag_extend_diff)

lemma simplex_map_oriented_simplex:
  assumes l: "simplicial_simplex p (standard_simplex q) (oriented_simplex p l)"
    and g: "simplicial_simplex r S g" and "q ≤ r"
  shows "simplex_map p g (oriented_simplex p l) = oriented_simplex p (g ∘ l)"
proof -
  obtain m where geq: "g = oriented_simplex r m"
    using g by (auto simp: simplicial_simplex_def)
  have "g (λi. ∑j≤p. l j i * x j) i = (∑j≤p. g (l j) i * x j)"
    if "x ∈ standard_simplex p" for x i
  proof -
    have ssr: "(λi. ∑j≤p. l j i * x j) ∈ standard_simplex r"
      using l that standard_simplex_mono [OF ‹q ≤ r›]
      unfolding simplicial_simplex_oriented_simplex by auto
    have lss: "l j ∈ standard_simplex r" if "j≤p" for j
    proof -
      have q: "(λx i. ∑j≤p. l j i * x j) ` standard_simplex p ⊆ standard_simplex q"
        using l by (simp add: simplicial_simplex_oriented_simplex)
      let ?x = "(λi. if i = j then 1 else 0)"
      have p: "l j ∈ (λx i. ∑j≤p. l j i * x j) ` standard_simplex p"
      proof
        show "l j = (λi. ∑j≤p. l j i * ?x j)"
          using ‹j≤p› by (force simp: if_distrib cong: if_cong)
        show "?x ∈ standard_simplex p"
          by (simp add: that)
      qed
      show ?thesis
        using standard_simplex_mono [OF ‹q ≤ r›] q p
        by blast
    qed
    have "g (λi. ∑j≤p. l j i * x j) i = (∑j≤r. ∑n≤p. m j i * (l n j * x n))"
      by (simp add: geq oriented_simplex_def sum_distrib_left ssr)
    also have "... =  (∑j≤p. ∑n≤r. m n i * (l j n * x j))"
      by (rule sum.swap)
    also have "... = (∑j≤p. g (l j) i * x j)"
      by (simp add: geq oriented_simplex_def sum_distrib_right mult.assoc lss)
    finally show ?thesis .
  qed
  then show ?thesis
    by (force simp: oriented_simplex_def simplex_map_def o_def)
qed


lemma chain_map_simplicial_cone:
  assumes g: "simplicial_simplex r S g"
      and c: "simplicial_chain p (standard_simplex q) c"
      and v: "v ∈ standard_simplex q" and "q ≤ r"
  shows "chain_map (Suc p) g (simplicial_cone p v c) = simplicial_cone p (g v) (chain_map p g c)"
proof -
  have *: "simplex_map (Suc p) g (simplex_cone p v f) = simplex_cone p (g v) (simplex_map p g f)"
    if "f ∈ Poly_Mapping.keys c" for f
  proof -
    have "simplicial_simplex p (standard_simplex q) f"
      using c that by (auto simp: simplicial_chain_def)
    then obtain m where feq: "f = oriented_simplex p m"
      by (auto simp: simplicial_simplex)
    have 0: "simplicial_simplex p (standard_simplex q) (oriented_simplex p m)"
      using ‹simplicial_simplex p (standard_simplex q) f› feq by blast
    then have 1: "simplicial_simplex (Suc p) (standard_simplex q)
                      (oriented_simplex (Suc p) (λi. if i = 0 then v else m (i -1)))"
      using convex_standard_simplex v
      by (simp flip: simplex_cone add: simplicial_simplex_simplex_cone)
    show ?thesis
      using simplex_map_oriented_simplex [OF 1 g ‹q ≤ r›]
            simplex_map_oriented_simplex [of p q m r S g, OF 0 g ‹q ≤ r›]
      by (simp add: feq oriented_simplex_eq simplex_cone)
  qed
  show ?thesis
    by (auto simp: chain_map_def simplicial_cone_def frag_extend_compose * intro: frag_extend_eq)
qed


subsection‹Barycentric subdivision of a linear ("simplicial") simplex's image›

definition simplicial_vertex
  where "simplicial_vertex i f = f(λj. if j = i then 1 else 0)"

lemma simplicial_vertex_oriented_simplex:
   "simplicial_vertex i (oriented_simplex p l) = (if i ≤ p then l i else undefined)"
  by (simp add: simplicial_vertex_def oriented_simplex_def if_distrib cong: if_cong)


primrec simplicial_subdivision
where
  "simplicial_subdivision 0 = id"
| "simplicial_subdivision (Suc p) =
     frag_extend
      (λf. simplicial_cone p
            (λi. (∑j≤Suc p. simplicial_vertex j f i) / (p + 2))
            (simplicial_subdivision p (chain_boundary (Suc p) (frag_of f))))"


lemma simplicial_subdivision_0 [simp]:
   "simplicial_subdivision p 0 = 0"
  by (induction p) auto

lemma simplicial_subdivision_diff:
   "simplicial_subdivision p (c1-c2) = simplicial_subdivision p c1 - simplicial_subdivision p c2"
  by (induction p) (auto simp: frag_extend_diff)

lemma simplicial_subdivision_of:
   "simplicial_subdivision p (frag_of f) =
         (if p = 0 then frag_of f
         else simplicial_cone (p -1)
               (λi. (∑j≤p. simplicial_vertex j f i) / (Suc p))
               (simplicial_subdivision (p -1) (chain_boundary p (frag_of f))))"
  by (induction p) (auto simp: add.commute)


lemma simplicial_chain_simplicial_subdivision:
   "simplicial_chain p S c
           ⟹ simplicial_chain p S (simplicial_subdivision p c)"
proof (induction p arbitrary: S c)
  case (Suc p)
  show ?case
    using Suc.prems [unfolded simplicial_chain_def]
  proof (induction c rule: frag_induction)
    case (one f)
    then have f: "simplicial_simplex (Suc p) S f"
      by auto
    then have "simplicial_chain p (f ` standard_simplex (Suc p))
                 (simplicial_subdivision p (chain_boundary (Suc p) (frag_of f)))"
      by (metis Suc.IH diff_Suc_1 simplicial_chain_boundary simplicial_chain_of simplicial_simplex subsetI)
    moreover
    obtain l where l: "⋀x. x ∈ standard_simplex (Suc p) ⟹ (λi. (∑j≤Suc p. l j i * x j)) ∈ S"
      and feq: "f = oriented_simplex (Suc p) l"
      using f by (fastforce simp: simplicial_simplex oriented_simplex_def simp del: sum.atMost_Suc)
    have "(λi. (1 - u) * ((∑j≤Suc p. simplicial_vertex j f i) / (real p + 2)) + u * y i) ∈ S"
      if "0 ≤ u" "u ≤ 1" and y: "y ∈ f ` standard_simplex (Suc p)" for y u
    proof -
      obtain x where x: "x ∈ standard_simplex (Suc p)" and yeq: "y = oriented_simplex (Suc p) l x"
        using y feq by blast
      have "(λi. ∑j≤Suc p. l j i * ((if j ≤ Suc p then (1 - u) * inverse (p + 2) + u * x j else 0))) ∈ S"
      proof (rule l)
        have "inverse (2 + real p) ≤ 1" "(2 + real p) * ((1 - u) * inverse (2 + real p)) + u = 1"
          by (auto simp add: field_split_simps)
        then show "(λj. if j ≤ Suc p then (1 - u) * inverse (real (p + 2)) + u * x j else 0) ∈ standard_simplex (Suc p)"
          using x ‹0 ≤ u› ‹u ≤ 1›
          by (simp add: sum.distrib standard_simplex_def linepath_le_1 flip: sum_distrib_left del: sum.atMost_Suc)
      qed
      moreover have "(λi. ∑j≤Suc p. l j i * ((1 - u) * inverse (2 + real p) + u * x j))
                   = (λi. (1 - u) * (∑j≤Suc p. l j i) / (real p + 2) + u * (∑j≤Suc p. l j i * x j))"
      proof
        fix i
        have "(∑j≤Suc p. l j i * ((1 - u) * inverse (2 + real p) + u * x j))
            = (∑j≤Suc p. (1 - u) * l j i / (real p + 2) + u * l j i * x j)" (is "?lhs = _")
          by (simp add: field_simps cong: sum.cong)
        also have "… = (1 - u) * (∑j≤Suc p. l j i) / (real p + 2) + u * (∑j≤Suc p. l j i * x j)" (is "_ = ?rhs")
          by (simp add: sum_distrib_left sum.distrib sum_divide_distrib mult.assoc del: sum.atMost_Suc)
        finally show "?lhs = ?rhs" .
      qed
      ultimately show ?thesis
        using feq x yeq
        by (simp add: simplicial_vertex_oriented_simplex) (simp add: oriented_simplex_def)
    qed
    ultimately show ?case
      by (simp add: simplicial_chain_simplicial_cone)
  next
    case (diff a b)
    then show ?case
      by (metis simplicial_chain_diff simplicial_subdivision_diff)
  qed auto
qed auto

lemma chain_boundary_simplicial_subdivision:
   "simplicial_chain p S c
    ⟹ chain_boundary p (simplicial_subdivision p c) = simplicial_subdivision (p -1) (chain_boundary p c)"
proof (induction p arbitrary: c)
  case (Suc p)
  show ?case
    using Suc.prems [unfolded simplicial_chain_def]
  proof (induction c rule: frag_induction)
    case (one f)
    then have f: "simplicial_simplex (Suc p) S f"
      by simp
    then have "simplicial_chain p S (simplicial_subdivision p (chain_boundary (Suc p) (frag_of f)))"
      by (metis diff_Suc_1 simplicial_chain_boundary simplicial_chain_of simplicial_chain_simplicial_subdivision)
    moreover have "simplicial_chain p S (chain_boundary (Suc p) (frag_of f))"
      using one simplicial_chain_boundary simplicial_chain_of by fastforce
    moreover have "simplicial_subdivision (p - Suc 0) (chain_boundary p (chain_boundary (Suc p) (frag_of f))) = 0"
      by (metis f chain_boundary_boundary_alt simplicial_simplex_def simplicial_subdivision_0 singular_chain_of)
    ultimately show ?case
      using chain_boundary_simplicial_cone Suc
      by (auto simp: chain_boundary_of frag_extend_diff simplicial_cone_def)
  next
    case (diff a b)
    then show ?case
      by (simp add: simplicial_subdivision_diff chain_boundary_diff frag_extend_diff)
  qed auto
qed auto


text ‹A MESS AND USED ONLY ONCE›
lemma simplicial_subdivision_shrinks:
   "⟦simplicial_chain p S c;
     ⋀f x y. ⟦f ∈ Poly_Mapping.keys c; x ∈ standard_simplex p; y ∈ standard_simplex p⟧ ⟹ ¦f x k - f y k¦ ≤ d;
     f ∈ Poly_Mapping.keys(simplicial_subdivision p c);
     x ∈ standard_simplex p; y ∈ standard_simplex p⟧
    ⟹ ¦f x k - f y k¦ ≤ (p / (Suc p)) * d"
proof (induction p arbitrary: d c f x y)
  case (Suc p)
  define Sigp where "Sigp ≡ λf:: (nat ⇒ real) ⇒ nat ⇒ real. λi. (∑j≤Suc p. simplicial_vertex j f i) / real (p + 2)"
  let ?CB = "λf. chain_boundary (Suc p) (frag_of f)"
  have *: "Poly_Mapping.keys
             (simplicial_cone p (Sigp f)
               (simplicial_subdivision p (?CB f)))
           ⊆ {f. ∀x∈standard_simplex (Suc p). ∀y∈standard_simplex (Suc p).
                      ¦f x k - f y k¦ ≤ real (Suc p) / (real p + 2) * d}" (is "?lhs ⊆ ?rhs")
    if f: "f ∈ Poly_Mapping.keys c" for f
  proof -
    have ssf: "simplicial_simplex (Suc p) S f"
      using Suc.prems(1) simplicial_chain_def that by auto
    have 2: "⋀x y. ⟦x ∈ standard_simplex (Suc p); y ∈ standard_simplex (Suc p)⟧ ⟹ ¦f x k - f y k¦ ≤ d"
      by (meson Suc.prems(2) f subsetD le_Suc_eq order_refl standard_simplex_mono)
    have sub: "Poly_Mapping.keys ((frag_of ∘ simplex_cone p (Sigp f)) g) ⊆ ?rhs"
      if "g ∈ Poly_Mapping.keys (simplicial_subdivision p (?CB f))" for g
    proof -
      have 1: "simplicial_chain p S (?CB f)"
        using ssf simplicial_chain_boundary simplicial_chain_of by fastforce
      have "simplicial_chain (Suc p) (f ` standard_simplex(Suc p)) (frag_of f)"
        by (metis simplicial_chain_of simplicial_simplex ssf subset_refl)
      then have sc_sub: "Poly_Mapping.keys (?CB f)
                         ⊆ Collect (simplicial_simplex p (f ` standard_simplex (Suc p)))"
        by (metis diff_Suc_1 simplicial_chain_boundary simplicial_chain_def)
      have led: "⋀h x y. ⟦h ∈ Poly_Mapping.keys (chain_boundary (Suc p) (frag_of f));
                          x ∈ standard_simplex p; y ∈ standard_simplex p⟧ ⟹ ¦h x k - h y k¦ ≤ d"
        using Suc.prems(2) f sc_sub
        by (simp add: simplicial_simplex subset_iff image_iff) metis
      have "⋀f' x y. ⟦f' ∈ Poly_Mapping.keys (simplicial_subdivision p (?CB f)); x ∈ standard_simplex p; y ∈ standard_simplex p⟧
            ⟹ ¦f' x k - f' y k¦ ≤ (p / (Suc p)) * d"
        by (blast intro: led Suc.IH [of "chain_boundary (Suc p) (frag_of f)", OF 1])
      then have g: "⋀x y. ⟦x ∈ standard_simplex p; y ∈ standard_simplex p⟧ ⟹ ¦g x k - g y k¦ ≤ (p / (Suc p)) * d"
        using that by blast
      have "d ≥ 0"
        using Suc.prems(2)[OF f] ‹x ∈ standard_simplex (Suc p)› by force
      have 3: "simplex_cone p (Sigp f) g ∈ ?rhs"
      proof -
        have "simplicial_simplex p (f ` standard_simplex(Suc p)) g"
          by (metis (mono_tags, opaque_lifting) sc_sub mem_Collect_eq simplicial_chain_def simplicial_chain_simplicial_subdivision subsetD that)
        then obtain m where m: "g ` standard_simplex p ⊆ f ` standard_simplex (Suc p)"
          and geq: "g = oriented_simplex p m"
          using ssf by (auto simp: simplicial_simplex)
        have m_in_gim: "m i ∈ g ` standard_simplex p" if "i ≤ p" for i
        proof 
          show "m i = g (λj. if j = i then 1 else 0)"
            by (simp add: geq oriented_simplex_def that if_distrib cong: if_cong)
          show "(λj. if j = i then 1 else 0) ∈ standard_simplex p"
            by (simp add: oriented_simplex_def that)
        qed
        obtain l where l: "f ` standard_simplex (Suc p) ⊆ S"
          and feq: "f = oriented_simplex (Suc p) l"
          using ssf by (auto simp: simplicial_simplex)
        show ?thesis
        proof (clarsimp simp add: geq simp del: sum.atMost_Suc)
          fix x y
          assume x: "x ∈ standard_simplex (Suc p)" and y: "y ∈ standard_simplex (Suc p)"
          then have x': "(∀i. 0 ≤ x i ∧ x i ≤ 1) ∧ (∀i>Suc p. x i = 0) ∧ (∑i≤Suc p. x i) = 1"
            and y': "(∀i. 0 ≤ y i ∧ y i ≤ 1) ∧ (∀i>Suc p. y i = 0) ∧ (∑i≤Suc p. y i) = 1"
            by (auto simp: standard_simplex_def)
          have "¦(∑j≤Suc p. (if j = 0 then λi. (∑j≤Suc p. l j i) / (2 + real p) else m (j -1)) k * x j) -
                 (∑j≤Suc p. (if j = 0 then λi. (∑j≤Suc p. l j i) / (2 + real p) else m (j -1)) k * y j)¦
                ≤ (1 + real p) * d / (2 + real p)"
          proof -
            have zero: "¦m (s - Suc 0) k - (∑j≤Suc p. l j k) / (2 + real p)¦ ≤ (1 + real p) * d / (2 + real p)"
              if "0 < s" and "s ≤ Suc p" for s
            proof -
              have "m (s - Suc 0) ∈ f ` standard_simplex (Suc p)"
                using m m_in_gim that(2) by auto
              then obtain z where eq: "m (s - Suc 0) = (λi. ∑j≤Suc p. l j i * z j)" and z: "z ∈ standard_simplex (Suc p)"
                using feq unfolding oriented_simplex_def by auto
              show ?thesis
                unfolding eq
              proof (rule convex_sum_bound_le)
                fix i
                assume i: "i ∈ {..Suc p}"
                then have [simp]: "card ({..Suc p} - {i}) = Suc p"
                  by (simp add: card_Suc_Diff1)
                have "(∑j≤Suc p. ¦l i k / (p + 2) - l j k / (p + 2)¦) = (∑j≤Suc p. ¦l i k - l j k¦ / (p + 2))"
                  by (rule sum.cong) (simp_all add: flip: diff_divide_distrib)
                also have "… = (∑j ∈ {..Suc p} - {i}. ¦l i k - l j k¦ / (p + 2))"
                  by (rule sum.mono_neutral_right) auto
                also have "… ≤ (1 + real p) * d / (p + 2)"
                proof (rule sum_bounded_above_divide)
                  fix i' :: "nat"
                  assume i': "i' ∈ {..Suc p} - {i}"
                  have lf: "l r ∈ f ` standard_simplex(Suc p)" if "r ≤ Suc p" for r
                  proof
                    show "l r = f (λj. if j = r then 1 else 0)"
                      using that by (simp add: feq oriented_simplex_def if_distrib cong: if_cong)
                    show "(λj. if j = r then 1 else 0) ∈ standard_simplex (Suc p)"
                      by (auto simp: oriented_simplex_def that)
                  qed
                  show "¦l i k - l i' k¦ / real (p + 2) ≤ (1 + real p) * d / real (p + 2) / real (card ({..Suc p} - {i}))"
                    using i i' lf [of i] lf [of i'] 2
                    by (auto simp: image_iff divide_simps)
                qed auto
                finally have "(∑j≤Suc p. ¦l i k / (p + 2) - l j k / (p + 2)¦) ≤ (1 + real p) * d / (p + 2)" .
                then have "¦∑j≤Suc p. l i k / (p + 2) - l j k / (p + 2)¦ ≤ (1 + real p) * d / (p + 2)"
                  by (rule order_trans [OF sum_abs])
                then show "¦l i k - (∑j≤Suc p. l j k) / (2 + real p)¦ ≤ (1 + real p) * d / (2 + real p)"
                  by (simp add: sum_subtractf sum_divide_distrib del: sum.atMost_Suc)
              qed (use standard_simplex_def z in auto)
            qed
            have nonz: "¦m (s - Suc 0) k - m (r - Suc 0) k¦ ≤ (1 + real p) * d / (2 + real p)" (is "?lhs ≤ ?rhs")
              if "r < s" and "0 < r" and "r ≤ Suc p" and "s ≤ Suc p" for r s
            proof -
              have "?lhs ≤ (p / (Suc p)) * d"
                using m_in_gim [of "r - Suc 0"] m_in_gim [of "s - Suc 0"] that g by fastforce
              also have "… ≤ ?rhs"
                by (simp add: field_simps ‹0 ≤ d›)
              finally show ?thesis .
            qed
            have jj: "j ≤ Suc p ∧ j' ≤ Suc p
                ⟶ ¦(if j' = 0 then λi. (∑j≤Suc p. l j i) / (2 + real p) else m (j' -1)) k -
                     (if j = 0 then λi. (∑j≤Suc p. l j i) / (2 + real p) else m (j -1)) k¦
                     ≤ (1 + real p) * d / (2 + real p)" for j j'
              using ‹0 ≤ d› 
              by (rule_tac a=j and b = "j'" in linorder_less_wlog; force simp: zero nonz simp del: sum.atMost_Suc)
            show ?thesis
              apply (rule convex_sum_bound_le)
              using x' apply blast
              using x' apply blast
              apply (subst abs_minus_commute)
              apply (rule convex_sum_bound_le)
              using y' apply blast
              using y' apply blast
              using jj by blast
          qed
          then show "¦simplex_cone p (Sigp f) (oriented_simplex p m) x k - simplex_cone p (Sigp f) (oriented_simplex p m) y k¦
                ≤ (1 + real p) * d / (real p + 2)"
            apply (simp add: feq Sigp_def simplicial_vertex_oriented_simplex simplex_cone del: sum.atMost_Suc)
            apply (simp add: oriented_simplex_def algebra_simps x y del: sum.atMost_Suc)
            done
        qed
      qed
      show ?thesis
        using Suc.IH [OF 1, where f=g] 2 3 by simp
    qed
    then show ?thesis
      unfolding simplicial_chain_def simplicial_cone_def
      by (simp add: order_trans [OF keys_frag_extend] sub UN_subset_iff)
  qed
  show ?case
    using Suc
    apply (simp del: sum.atMost_Suc)
    apply (drule subsetD [OF keys_frag_extend])
    apply (simp del: sum.atMost_Suc)
    apply clarify (*OBTAIN?*)
    apply (rename_tac FFF)
    using *
    apply (simp add: add.commute Sigp_def subset_iff)
    done
qed (auto simp: standard_simplex_0)


subsection‹Singular subdivision›

definition singular_subdivision
  where "singular_subdivision p ≡
        frag_extend
           (λf. chain_map p f
                  (simplicial_subdivision p
                         (frag_of(restrict id (standard_simplex p)))))"

lemma singular_subdivision_0 [simp]: "singular_subdivision p 0 = 0"
  by (simp add: singular_subdivision_def)

lemma singular_subdivision_add:
   "singular_subdivision p (a + b) = singular_subdivision p a + singular_subdivision p b"
  by (simp add: singular_subdivision_def frag_extend_add)

lemma singular_subdivision_diff:
   "singular_subdivision p (a - b) = singular_subdivision p a - singular_subdivision p b"
  by (simp add: singular_subdivision_def frag_extend_diff)

lemma simplicial_simplex_id [simp]:
   "simplicial_simplex p S (restrict id (standard_simplex p)) ⟷ standard_simplex p ⊆ S"
    (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (simp add: simplicial_simplex_def singular_simplex_def continuous_map_in_subtopology set_mp)
next
  assume R: ?rhs
  then have cm: "continuous_map
                 (subtopology (powertop_real UNIV) (standard_simplex p))
                 (subtopology (powertop_real UNIV) S) id"
    using continuous_map_from_subtopology_mono continuous_map_id by blast
  moreover have "∃l. restrict id (standard_simplex p) = oriented_simplex p l"
    apply (rule_tac x="λi j. if i = j then 1 else 0" in exI)
    apply (force simp: oriented_simplex_def standard_simplex_def if_distrib [of "λu. u * _"] cong: if_cong)
    done
  ultimately show ?lhs
    by (simp add: simplicial_simplex_def singular_simplex_def)
qed

lemma singular_chain_singular_subdivision:
   "singular_chain p X c
        ⟹ singular_chain p X (singular_subdivision p c)"
  unfolding singular_subdivision_def
  apply (rule singular_chain_extend)
  apply (rule singular_chain_chain_map [where X = "subtopology (powertop_real UNIV)
                          (standard_simplex p)"])
  apply (simp add: simplicial_chain_simplicial_subdivision simplicial_imp_singular_chain)
  by (simp add: singular_chain_def singular_simplex_def subset_iff)

lemma naturality_singular_subdivision:
   "singular_chain p X c
    ⟹ singular_subdivision p (chain_map p g c) = chain_map p g (singular_subdivision p c)"
  unfolding singular_chain_def
proof (induction rule: frag_induction)
  case (one f)
  then have "singular_simplex p X f"
    by auto
  have "⟦simplicial_chain p (standard_simplex p) d⟧
    ⟹ chain_map p (simplex_map p g f) d = chain_map p g (chain_map p f d)" for d
    unfolding simplicial_chain_def
  proof (induction rule: frag_induction)
    case (one x)
    then have "simplex_map p (simplex_map p g f) x = simplex_map p g (simplex_map p f x)"
      by (force simp: simplex_map_def restrict_compose_left simplicial_simplex)
    then show ?case
      by auto
  qed (auto simp: chain_map_diff)
  then show ?case
    using simplicial_chain_simplicial_subdivision [of p "standard_simplex p" "frag_of (restrict id (standard_simplex p))"]
    by (simp add: singular_subdivision_def)
next
  case (diff a b)
  then show ?case
    by (simp add: chain_map_diff singular_subdivision_diff)
qed auto

lemma simplicial_chain_chain_map:
  assumes f: "simplicial_simplex q X f" and c: "simplicial_chain p (standard_simplex q) c"
  shows "simplicial_chain p X (chain_map p f c)"
  using c unfolding simplicial_chain_def
proof (induction c rule: frag_induction)
  case (one g)
  have "∃n. simplex_map p (oriented_simplex q l)
                 (oriented_simplex p m) = oriented_simplex p n"
    if m: "singular_simplex p
                (subtopology (powertop_real UNIV) (standard_simplex q)) (oriented_simplex p m)"
    for l m
  proof -
    have "(λi. ∑j≤p. m j i * x j) ∈ standard_simplex q"
      if "x ∈ standard_simplex p" for x
      using that m unfolding oriented_simplex_def singular_simplex_def
      by (auto simp: continuous_map_in_subtopology image_subset_iff)
    then show ?thesis
      unfolding oriented_simplex_def simplex_map_def
      apply (rule_tac x="λj k. (∑i≤q. l i k * m j i)" in exI)
      apply (force simp: sum_distrib_left sum_distrib_right mult.assoc intro: sum.swap)
      done
  qed
  then show ?case
    using f one
    apply (auto simp: simplicial_simplex_def)
    apply (rule singular_simplex_simplex_map
        [where X = "subtopology (powertop_real UNIV) (standard_simplex q)"])
    unfolding singular_simplex_def apply (fastforce simp add:)+
    done
next
  case (diff a b)
  then show ?case
    by (metis chain_map_diff simplicial_chain_def simplicial_chain_diff)
qed auto


lemma singular_subdivision_simplicial_simplex:
   "simplicial_chain p S c
           ⟹ singular_subdivision p c = simplicial_subdivision p c"
proof (induction p arbitrary: S c)
  case 0
  then show ?case
    unfolding simplicial_chain_def
  proof (induction rule: frag_induction)
    case (one x)
    then show ?case
      using singular_simplex_chain_map_id simplicial_imp_singular_simplex
      by (fastforce simp: singular_subdivision_def simplicial_subdivision_def)
  qed (auto simp: singular_subdivision_diff)
next
  case (Suc p)
  show ?case
    using Suc.prems unfolding simplicial_chain_def
  proof (induction rule: frag_induction)
    case (one f)
    then have ssf: "simplicial_simplex (Suc p) S f"
      by (auto simp: simplicial_simplex)
    then have 1: "simplicial_chain p (standard_simplex (Suc p))
                   (simplicial_subdivision p
                     (chain_boundary (Suc p)
                       (frag_of (restrict id (standard_simplex (Suc p))))))"
      by (metis diff_Suc_1 order_refl simplicial_chain_boundary simplicial_chain_of simplicial_chain_simplicial_subdivision simplicial_simplex_id)
    have 2: "(λi. (∑j≤Suc p. simplicial_vertex j (restrict id (standard_simplex (Suc p))) i) / (real p + 2))
                  ∈ standard_simplex (Suc p)"
      by (simp add: simplicial_vertex_def standard_simplex_def del: sum.atMost_Suc)
    have ss_Sp: "(λi. (if i ≤ Suc p then 1 else 0) / (real p + 2)) ∈ standard_simplex (Suc p)"
      by (simp add: standard_simplex_def field_split_simps)
    obtain l where feq: "f = oriented_simplex (Suc p) l"
      using one unfolding simplicial_simplex by blast
    then have 3: "f (λi. (∑j≤Suc p. simplicial_vertex j (restrict id (standard_simplex (Suc p))) i) / (real p + 2))
                = (λi. (∑j≤Suc p. simplicial_vertex j f i) / (real p + 2))"
      unfolding simplicial_vertex_def oriented_simplex_def
      by (simp add: ss_Sp if_distrib [of "λx. _ * x"] sum_divide_distrib del: sum.atMost_Suc cong: if_cong)
    have scp: "singular_chain (Suc p)
                 (subtopology (powertop_real UNIV) (standard_simplex (Suc p)))
                 (frag_of (restrict id (standard_simplex (Suc p))))"
      by (simp add: simplicial_imp_singular_chain)
    have scps: "simplicial_chain p (standard_simplex (Suc p))
                  (chain_boundary (Suc p) (frag_of (restrict id (standard_simplex (Suc p)))))"
      by (metis diff_Suc_1 order_refl simplicial_chain_boundary simplicial_chain_of simplicial_simplex_id)
    have scpf: "simplicial_chain p S
                 (chain_map p f
                   (chain_boundary (Suc p) (frag_of (restrict id (standard_simplex (Suc p))))))"
      using scps simplicial_chain_chain_map ssf by blast
    have 4: "chain_map p f
                (simplicial_subdivision p
                   (chain_boundary (Suc p) (frag_of (restrict id (standard_simplex (Suc p))))))
           = simplicial_subdivision p (chain_boundary (Suc p) (frag_of f))"
      apply (simp add: chain_boundary_chain_map [OF scp] del: chain_map_of
          flip: singular_simplex_chain_map_id [OF simplicial_imp_singular_simplex [OF ssf]])
      by (metis (no_types) scp singular_chain_boundary_alt Suc.IH [OF scps] Suc.IH [OF scpf] naturality_singular_subdivision)
    show ?case
      apply (simp add: singular_subdivision_def del: sum.atMost_Suc)
      apply (simp only: ssf 1 2 3 4 chain_map_simplicial_cone [of "Suc p" S _ p "Suc p"])
      done
  qed (auto simp: frag_extend_diff singular_subdivision_diff)
qed


lemma naturality_simplicial_subdivision:
   "⟦simplicial_chain p (standard_simplex q) c; simplicial_simplex q S g⟧
    ⟹ simplicial_subdivision p (chain_map p g c) = chain_map p g (simplicial_subdivision p c)"
apply (simp flip: singular_subdivision_simplicial_simplex)
  by (metis naturality_singular_subdivision simplicial_chain_chain_map simplicial_imp_singular_chain singular_subdivision_simplicial_simplex)

lemma chain_boundary_singular_subdivision:
   "singular_chain p X c
        ⟹ chain_boundary p (singular_subdivision p c) =
            singular_subdivision (p - Suc 0) (chain_boundary p c)"
  unfolding singular_chain_def
proof (induction rule: frag_induction)
  case (one f)
    then have ssf: "singular_simplex p X f"
      by (auto simp: singular_simplex_def)
    then have scp: "simplicial_chain p (standard_simplex p) (frag_of (restrict id (standard_simplex p)))"
      by simp
    have scp1: "simplicial_chain (p - Suc 0) (standard_simplex p)
                  (chain_boundary p (frag_of (restrict id (standard_simplex p))))"
      using simplicial_chain_boundary by force
    have sgp1: "singular_chain (p - Suc 0)
                   (subtopology (powertop_real UNIV) (standard_simplex p))
                   (chain_boundary p (frag_of (restrict id (standard_simplex p))))"
      using scp1 simplicial_imp_singular_chain by blast
    have scpp: "singular_chain p (subtopology (powertop_real UNIV) (standard_simplex p))
                  (frag_of (restrict id (standard_simplex p)))"
      using scp simplicial_imp_singular_chain by blast
    then show ?case
      unfolding singular_subdivision_def
      using chain_boundary_chain_map [of p "subtopology (powertop_real UNIV)
                              (standard_simplex p)" _ f]
      apply (simp add: simplicial_chain_simplicial_subdivision
          simplicial_imp_singular_chain chain_boundary_simplicial_subdivision [OF scp]
          flip: singular_subdivision_simplicial_simplex [OF scp1] naturality_singular_subdivision [OF sgp1])
      by (metis (full_types)   singular_subdivision_def  chain_boundary_chain_map [OF scpp] singular_simplex_chain_map_id [OF ssf])
qed (auto simp: singular_subdivision_def frag_extend_diff chain_boundary_diff)

lemma singular_subdivision_zero:
  "singular_chain 0 X c ⟹ singular_subdivision 0 c = c"
  unfolding singular_chain_def
proof (induction rule: frag_induction)
  case (one f)
  then have "restrict (f ∘ restrict id (standard_simplex 0)) (standard_simplex 0) = f"
    by (simp add: extensional_restrict restrict_compose_right singular_simplex_def)
  then show ?case
    by (auto simp: singular_subdivision_def simplex_map_def)
qed (auto simp: singular_subdivision_def frag_extend_diff)


primrec subd where
  "subd 0 = (λx. 0)"
| "subd (Suc p) =
      frag_extend
       (λf. simplicial_cone (Suc p) (λi. (∑j≤Suc p. simplicial_vertex j f i) / real (Suc p + 1))
               (simplicial_subdivision (Suc p) (frag_of f) - frag_of f -
                subd p (chain_boundary (Suc p) (frag_of f))))"

lemma subd_0 [simp]: "subd p 0 = 0"
  by (induction p) auto

lemma subd_diff [simp]: "subd p (c1 - c2) = subd p c1 - subd p c2"
  by (induction p) (auto simp: frag_extend_diff)

lemma subd_uminus [simp]: "subd p (-c) = - subd p c"
  by (metis diff_0 subd_0 subd_diff)

lemma subd_power_uminus: "subd p (frag_cmul ((-1) ^ k) c) = frag_cmul ((-1) ^ k) (subd p c)"
  apply (induction k, simp_all)
  by (metis minus_frag_cmul subd_uminus)

lemma subd_power_sum: "subd p (sum f I) = sum (subd p ∘ f) I"
  apply (induction I rule: infinite_finite_induct)
  by auto (metis add_diff_cancel_left' diff_add_cancel subd_diff)

lemma subd: "simplicial_chain p (standard_simplex s) c
     ⟹ (∀r g. simplicial_simplex s (standard_simplex r) g ⟶ chain_map (Suc p) g (subd p c) = subd p (chain_map p g c))
         ∧ simplicial_chain (Suc p) (standard_simplex s) (subd p c)
         ∧ (chain_boundary (Suc p) (subd p c)) + (subd (p - Suc 0) (chain_boundary p c)) = (simplicial_subdivision p c) - c"
proof (induction p arbitrary: c)
  case (Suc p)
  show ?case
    using Suc.prems [unfolded simplicial_chain_def]
  proof (induction rule: frag_induction)
    case (one f)
    then obtain l where l: "(λx i. ∑j≤Suc p. l j i * x j) ` standard_simplex (Suc p) ⊆ standard_simplex s"
                  and feq: "f = oriented_simplex (Suc p) l"
      by (metis (mono_tags) mem_Collect_eq simplicial_simplex simplicial_simplex_oriented_simplex)
    have scf: "simplicial_chain (Suc p) (standard_simplex s) (frag_of f)"
      using one by simp
    have lss: "l i ∈ standard_simplex s" if "i ≤ Suc p" for i
    proof -
      have "(λi'. ∑j≤Suc p. l j i' * (if j = i then 1 else 0)) ∈ standard_simplex s"
        using subsetD [OF l] basis_in_standard_simplex that by blast
      moreover have "(λi'. ∑j≤Suc p. l j i' * (if j = i then 1 else 0)) = l i"
        using that by (simp add: if_distrib [of "λx. _ * x"] del: sum.atMost_Suc cong: if_cong)
      ultimately show ?thesis
        by simp
    qed
    have *: "(⋀i. i ≤ n ⟹ l i ∈ standard_simplex s)
     ⟹ (λi. (∑j≤n. l j i) / (Suc n)) ∈ standard_simplex s" for n
    proof (induction n)
      case (Suc n)
      let ?x = "λi. (1 - inverse (n + 2)) * ((∑j≤n. l j i) / (Suc n)) + inverse (n + 2) * l (Suc n) i"
      have "?x ∈ standard_simplex s"
      proof (rule convex_standard_simplex)
        show "(λi. (∑j≤n. l j i) / real (Suc n)) ∈ standard_simplex s"
          using Suc by simp
      qed (auto simp: lss Suc inverse_le_1_iff)
      moreover have "?x = (λi. (∑j≤Suc n. l j i) / real (Suc (Suc n)))"
        by (force simp: divide_simps)
      ultimately show ?case
        by simp
    qed auto
    have **: "(λi. (∑j≤Suc p. simplicial_vertex j f i) / (2 + real p)) ∈ standard_simplex s"
      using * [of "Suc p"] lss by (simp add: simplicial_vertex_oriented_simplex feq)
    show ?case
    proof (intro conjI impI allI)
      fix r g
      assume g: "simplicial_simplex s (standard_simplex r) g"
      then obtain m where geq: "g = oriented_simplex s m"
        using simplicial_simplex by blast
      have 1: "simplicial_chain (Suc p) (standard_simplex s) (simplicial_subdivision (Suc p) (frag_of f))"
        by (metis mem_Collect_eq one.hyps simplicial_chain_of simplicial_chain_simplicial_subdivision)
      have 2: "(∑j≤Suc p. ∑i≤s. m i k * simplicial_vertex j f i)
             = (∑j≤Suc p. simplicial_vertex j
                                (simplex_map (Suc p) (oriented_simplex s m) f) k)" for k
      proof (rule sum.cong [OF refl])
        fix j
        assume j: "j ∈ {..Suc p}"
        have eq: "simplex_map (Suc p) (oriented_simplex s m) (oriented_simplex (Suc p) l)
                = oriented_simplex (Suc p) (oriented_simplex s m ∘ l)"
        proof (rule simplex_map_oriented_simplex)
          show "simplicial_simplex (Suc p) (standard_simplex s) (oriented_simplex (Suc p) l)"
            using one by (simp add: feq flip: oriented_simplex_def)
          show "simplicial_simplex s (standard_simplex r) (oriented_simplex s m)"
            using g by (simp add: geq)
        qed auto
        show "(∑i≤s. m i k * simplicial_vertex j f i)
            = simplicial_vertex j (simplex_map (Suc p) (oriented_simplex s m) f) k"
          using one j
          apply (simp add: feq eq simplicial_vertex_oriented_simplex simplicial_simplex_oriented_simplex image_subset_iff)
          apply (drule_tac x="(λi. if i = j then 1 else 0)" in bspec)
           apply (auto simp: oriented_simplex_def lss)
          done
      qed
      have 4: "chain_map (Suc p) g (subd p (chain_boundary (Suc p) (frag_of f)))
             = subd p (chain_boundary (Suc p) (frag_of (simplex_map (Suc p) g f)))"
        by (metis (no_types) One_nat_def scf Suc.IH chain_boundary_chain_map chain_map_of diff_Suc_Suc diff_zero g simplicial_chain_boundary simplicial_imp_singular_chain)
      show "chain_map (Suc (Suc p)) g (subd (Suc p) (frag_of f)) = subd (Suc p) (chain_map (Suc p) g (frag_of f))"
        using g
        apply (simp only: subd.simps frag_extend_of)
        apply (subst chain_map_simplicial_cone [of s "standard_simplex r" _ "Suc p" s], assumption)
           apply (intro simplicial_chain_diff)
        using "1" apply auto[1]
        using one.hyps apply auto[1]
        apply (metis Suc.IH diff_Suc_1 mem_Collect_eq one.hyps simplicial_chain_boundary simplicial_chain_of)
        using "**" apply auto[1]
         apply (rule order_refl)
         apply (simp only: chain_map_of frag_extend_of)
        apply (rule arg_cong2 [where f = "simplicial_cone (Suc p)"])
         apply (simp add: geq sum_distrib_left oriented_simplex_def ** del: sum.atMost_Suc flip: sum_divide_distrib)
        using 2  apply (simp only: oriented_simplex_def sum.swap [where A = "{..s}"])
        using naturality_simplicial_subdivision scf apply (fastforce simp add: 4 chain_map_diff)
        done
    next
      have sc: "simplicial_chain (Suc p) (standard_simplex s)
               (simplicial_cone p
                 (λi. (∑j≤Suc p. simplicial_vertex j f i) / (Suc (Suc p)))
                 (simplicial_subdivision p
                   (chain_boundary (Suc p) (frag_of f))))"
          by (metis diff_Suc_1 nat.simps(3) simplicial_subdivision_of scf simplicial_chain_simplicial_subdivision)
      have ff: "simplicial_chain (Suc p) (standard_simplex s) (subd p (chain_boundary (Suc p) (frag_of f)))"
        by (metis (no_types) Suc.IH diff_Suc_1 scf simplicial_chain_boundary)
      show "simplicial_chain (Suc (Suc p)) (standard_simplex s) (subd (Suc p) (frag_of f))"
        using one
        apply (simp only: subd.simps frag_extend_of)
        apply (rule_tac S="standard_simplex s" in simplicial_chain_simplicial_cone)
         apply (intro simplicial_chain_diff ff)
        using sc apply (simp add: algebra_simps)
        using "**" convex_standard_simplex  apply force+
        done
      have "simplicial_chain p (standard_simplex s) (chain_boundary (Suc p) (frag_of f))"
        using scf simplicial_chain_boundary by fastforce
      then have "chain_boundary (Suc p) (simplicial_subdivision (Suc p) (frag_of f) - frag_of f
                                         - subd p (chain_boundary (Suc p) (frag_of f))) = 0"
        apply (simp only: chain_boundary_diff)
        using Suc.IH chain_boundary_boundary [of "Suc p" "subtopology (powertop_real UNIV)
                                (standard_simplex s)" "frag_of f"]
        by (metis One_nat_def add_diff_cancel_left' subd_0 chain_boundary_simplicial_subdivision plus_1_eq_Suc scf simplicial_imp_singular_chain)
      then show "chain_boundary (Suc (Suc p)) (subd (Suc p) (frag_of f))
          + subd (Suc p - Suc 0) (chain_boundary (Suc p) (frag_of f))
          = simplicial_subdivision (Suc p) (frag_of f) - frag_of f"
        apply (simp only: subd.simps frag_extend_of)
        apply (subst chain_boundary_simplicial_cone [of "Suc p" "standard_simplex s"])
         apply (meson ff scf simplicial_chain_diff simplicial_chain_simplicial_subdivision)
        apply (simp add: simplicial_cone_def del: sum.atMost_Suc simplicial_subdivision.simps)
        done
    qed
  next
    case (diff a b)
    then show ?case
      apply safe
        apply (metis chain_map_diff subd_diff)
       apply (metis simplicial_chain_diff subd_diff)
      apply (auto simp:  simplicial_subdivision_diff chain_boundary_diff
          simp del: simplicial_subdivision.simps subd.simps)
      by (metis (no_types, lifting) add_diff_add add_uminus_conv_diff diff_0 diff_diff_add)
  qed auto
qed simp

lemma chain_homotopic_simplicial_subdivision1:
  "⟦simplicial_chain p (standard_simplex q) c; simplicial_simplex q (standard_simplex r) g⟧
       ⟹ chain_map (Suc p) g (subd p c) = subd p (chain_map p g c)"
  by (simp add: subd)

lemma chain_homotopic_simplicial_subdivision2:
  "simplicial_chain p (standard_simplex q) c
       ⟹ simplicial_chain (Suc p) (standard_simplex q) (subd p c)"
  by (simp add: subd)

lemma chain_homotopic_simplicial_subdivision3:
  "simplicial_chain p (standard_simplex q) c
   ⟹ chain_boundary (Suc p) (subd p c) = (simplicial_subdivision p c) - c - subd (p - Suc 0) (chain_boundary p c)"
  by (simp add: subd algebra_simps)

lemma chain_homotopic_simplicial_subdivision:
  "∃h. (∀p. h p 0 = 0) ∧
       (∀p c1 c2. h p (c1-c2) = h p c1 - h p c2) ∧
       (∀p q r g c.
                simplicial_chain p (standard_simplex q) c
                ⟶ simplicial_simplex q (standard_simplex r) g
                ⟶ chain_map (Suc p) g (h p c) = h p (chain_map p g c)) ∧
       (∀p q c. simplicial_chain p (standard_simplex q) c
                ⟶ simplicial_chain (Suc p) (standard_simplex q) (h p c)) ∧
       (∀p q c. simplicial_chain p (standard_simplex q) c
                ⟶ chain_boundary (Suc p) (h p c) + h (p - Suc 0) (chain_boundary p c)
                  = (simplicial_subdivision p c) - c)"
  by (rule_tac x=subd in exI) (fastforce simp: subd)

lemma chain_homotopic_singular_subdivision:
  obtains h where
        "⋀p. h p 0 = 0"
        "⋀p c1 c2. h p (c1-c2) = h p c1 - h p c2"
        "⋀p X c. singular_chain p X c ⟹ singular_chain (Suc p) X (h p c)"
        "⋀p X c. singular_chain p X c
                 ⟹ chain_boundary (Suc p) (h p c) + h (p - Suc 0) (chain_boundary p c) = singular_subdivision p c - c"
proof -
  define k where "k ≡ λp. frag_extend (λf:: (nat ⇒ real) ⇒ 'a. chain_map (Suc p) f (subd p (frag_of(restrict id (standard_simplex p)))))"
  show ?thesis
  proof
    fix p X and c :: "'a chain"
    assume c: "singular_chain p X c"
    have "singular_chain (Suc p) X (k p c) ∧
               chain_boundary (Suc p) (k p c) + k (p - Suc 0) (chain_boundary p c) = singular_subdivision p c - c"
      using c [unfolded singular_chain_def]
    proof (induction rule: frag_induction)
      case (one f)
      let ?X = "subtopology (powertop_real UNIV) (standard_simplex p)"
      show ?case
      proof (simp add: k_def, intro conjI)
        show "singular_chain (Suc p) X (chain_map (Suc p) f (subd p (frag_of (restrict id (standard_simplex p)))))"
        proof (rule singular_chain_chain_map)
          show "singular_chain (Suc p) ?X  (subd p (frag_of (restrict id (standard_simplex p))))"
            by (simp add: chain_homotopic_simplicial_subdivision2 simplicial_imp_singular_chain)
          show "continuous_map ?X X f"
            using one.hyps singular_simplex_def by auto
        qed
      next
        have scp: "singular_chain (Suc p) ?X (subd p (frag_of (restrict id (standard_simplex p))))"
          by (simp add: chain_homotopic_simplicial_subdivision2 simplicial_imp_singular_chain)
        have feqf: "frag_of (simplex_map p f (restrict id (standard_simplex p))) = frag_of f"
          using one.hyps singular_simplex_chain_map_id by auto
        have *: "chain_map p f
                   (subd (p - Suc 0)
                     (∑k≤p. frag_cmul ((-1) ^ k) (frag_of (singular_face p k id))))
              = (∑x≤p. frag_cmul ((-1) ^ x)
                         (chain_map p (singular_face p x f)
                           (subd (p - Suc 0) (frag_of (restrict id (standard_simplex (p - Suc 0)))))))"
                  (is "?lhs = ?rhs")
                  if "p > 0"
        proof -
          have eqc: "subd (p - Suc 0) (frag_of (singular_face p i id))
                   = chain_map p (singular_face p i id)
                                 (subd (p - Suc 0) (frag_of (restrict id (standard_simplex (p - Suc 0)))))"
            if "i ≤ p" for i
          proof -
            have 1: "simplicial_chain (p - Suc 0) (standard_simplex (p - Suc 0))
                       (frag_of (restrict id (standard_simplex (p - Suc 0))))"
              by simp
            have 2: "simplicial_simplex (p - Suc 0) (standard_simplex p) (singular_face p i id)"
              by (metis One_nat_def Suc_leI ‹0 < p› simplicial_simplex_id simplicial_simplex_singular_face singular_face_restrict subsetI that)
            have 3: "simplex_map (p - Suc 0) (singular_face p i id) (restrict id (standard_simplex (p - Suc 0)))
                   = singular_face p i id"
              by (force simp: simplex_map_def singular_face_def)
            show ?thesis
              using chain_homotopic_simplicial_subdivision1 [OF 1 2]
                that ‹p > 0›  by (simp add: 3)
          qed
          have xx: "simplicial_chain p (standard_simplex(p - Suc 0))
                    (subd (p - Suc 0) (frag_of (restrict id (standard_simplex (p - Suc 0)))))"
            by (metis Suc_pred chain_homotopic_simplicial_subdivision2 order_refl simplicial_chain_of simplicial_simplex_id that)
          have yy: "⋀k. k ≤ p ⟹
                 chain_map p f
                  (chain_map p (singular_face p k id) h) = chain_map p (singular_face p k f) h"
            if "simplicial_chain p (standard_simplex(p - Suc 0)) h" for h
            using that unfolding simplicial_chain_def
          proof (induction h rule: frag_induction)
            case (one x)
            then show ?case
                using one
              apply (simp add: chain_map_of singular_simplex_def simplicial_simplex_def, auto)
                apply (rule_tac f=frag_of in arg_cong, rule)
                apply (simp add: simplex_map_def)
                by (simp add: continuous_map_in_subtopology image_subset_iff singular_face_def)
          qed (auto simp: chain_map_diff)
          have "?lhs
                = chain_map p f
                      (∑k≤p. frag_cmul ((-1) ^ k)
                          (chain_map p (singular_face p k id)
                           (subd (p - Suc 0) (frag_of (restrict id (standard_simplex (p - Suc 0)))))))"
            by (simp add: subd_power_sum subd_power_uminus eqc)
          also have "… = ?rhs"
            by (simp add: chain_map_sum xx yy)
          finally show ?thesis .
      qed
        have "chain_map p f
                   (simplicial_subdivision p (frag_of (restrict id (standard_simplex p)))
                   - subd (p - Suc 0) (chain_boundary p (frag_of (restrict id (standard_simplex p)))))
              = singular_subdivision p (frag_of f)
              - frag_extend
                   (λf. chain_map (Suc (p - Suc 0)) f
                         (subd (p - Suc 0) (frag_of (restrict id (standard_simplex (p - Suc 0))))))
                   (chain_boundary p (frag_of f))"
          apply (simp add: singular_subdivision_def chain_map_diff)
          apply (clarsimp simp add: chain_boundary_def)
          apply (simp add: frag_extend_sum frag_extend_cmul *)
          done
        then show "chain_boundary (Suc p) (chain_map (Suc p) f (subd p (frag_of (restrict id (standard_simplex p)))))
                 + frag_extend
                   (λf. chain_map (Suc (p - Suc 0)) f
                         (subd (p - Suc 0) (frag_of (restrict id (standard_simplex (p - Suc 0))))))
                   (chain_boundary p (frag_of f))
                 = singular_subdivision p (frag_of f) - frag_of f"
          by (simp add: chain_boundary_chain_map [OF scp] chain_homotopic_simplicial_subdivision3 [where q=p] chain_map_diff feqf)
      qed
    next
      case (diff a b)
      then show ?case
        apply (simp only: k_def singular_chain_diff chain_boundary_diff frag_extend_diff singular_subdivision_diff)
        by (metis (no_types, lifting) add_diff_add diff_add_cancel)
    qed (auto simp: k_def)
    then show "singular_chain (Suc p) X (k p c)" "chain_boundary (Suc p) (k p c) + k (p - Suc 0) (chain_boundary p c) = singular_subdivision p c - c"
        by auto
  qed (auto simp: k_def frag_extend_diff)
qed


lemma homologous_rel_singular_subdivision:
  assumes "singular_relcycle p X T c"
  shows "homologous_rel p X T (singular_subdivision p c) c"
proof (cases "p = 0")
  case True
  with assms show ?thesis
    by (auto simp: singular_relcycle_def singular_subdivision_zero)
next
  case False
  with assms show ?thesis
    unfolding homologous_rel_def singular_relboundary singular_relcycle
    by (metis One_nat_def Suc_diff_1 chain_homotopic_singular_subdivision gr_zeroI)
qed


subsection‹Excision argument that we keep doing singular subdivision›

lemma singular_subdivision_power_0 [simp]: "(singular_subdivision p ^^ n) 0 = 0"
  by (induction n) auto

lemma singular_subdivision_power_diff:
  "(singular_subdivision p ^^ n) (a - b) = (singular_subdivision p ^^ n) a - (singular_subdivision p ^^ n) b"
  by (induction n) (auto simp: singular_subdivision_diff)

lemma iterated_singular_subdivision:
   "singular_chain p X c
        ⟹ (singular_subdivision p ^^ n) c =
            frag_extend
             (λf. chain_map p f
                       ((simplicial_subdivision p ^^ n)
                         (frag_of(restrict id (standard_simplex p))))) c"
proof (induction n arbitrary: c)
  case 0
  then show ?case
    unfolding singular_chain_def
  proof (induction c rule: frag_induction)
    case (one f)
    then have "restrict f (standard_simplex p) = f"
      by (simp add: extensional_restrict singular_simplex_def)
    then show ?case
      by (auto simp: simplex_map_def cong: restrict_cong)
  qed (auto simp: frag_extend_diff)
next
  case (Suc n)
  show ?case
    using Suc.prems unfolding singular_chain_def
  proof (induction c rule: frag_induction)
    case (one f)
    then have "singular_simplex p X f"
      by simp
    have scp: "simplicial_chain p (standard_simplex p)
                 ((simplicial_subdivision p ^^ n) (frag_of (restrict id (standard_simplex p))))"
    proof (induction n)
      case 0
      then show ?case
        by (metis funpow_0 order_refl simplicial_chain_of simplicial_simplex_id)
    next
      case (Suc n)
      then show ?case
        by (simp add: simplicial_chain_simplicial_subdivision)
    qed
    have scnp: "simplicial_chain p (standard_simplex p)
                  ((simplicial_subdivision p ^^ n) (frag_of (λx∈standard_simplex p. x)))"
    proof (induction n)
      case 0
      then show ?case
        by (metis eq_id_iff funpow_0 order_refl simplicial_chain_of simplicial_simplex_id)
    next
      case (Suc n)
      then show ?case
        by (simp add: simplicial_chain_simplicial_subdivision)
    qed
    have sff: "singular_chain p X (frag_of f)"
      by (simp add: ‹singular_simplex p X f› singular_chain_of)
    then show ?case
      using Suc.IH [OF sff] naturality_singular_subdivision [OF simplicial_imp_singular_chain [OF scp], of f] singular_subdivision_simplicial_simplex [OF scnp]
      by (simp add: singular_chain_of id_def del: restrict_apply)
  qed (auto simp: singular_subdivision_power_diff singular_subdivision_diff frag_extend_diff)
qed


lemma chain_homotopic_iterated_singular_subdivision:
  obtains h where
        "⋀p. h p 0 = (0 :: 'a chain)"
        "⋀p c1 c2. h p (c1-c2) = h p c1 - h p c2"
        "⋀p X c. singular_chain p X c ⟹ singular_chain (Suc p) X (h p c)"
        "⋀p X c. singular_chain p X c
                 ⟹ chain_boundary (Suc p) (h p c) + h (p - Suc 0) (chain_boundary p c)
                   = (singular_subdivision p ^^ n) c - c"
proof (induction n arbitrary: thesis)
  case 0
  show ?case
    by (rule 0 [of "(λp x. 0)"]) auto
next
  case (Suc n)
  then obtain k where k:
        "⋀p. k p 0 = (0 :: 'a chain)"
        "⋀p c1 c2. k p (c1-c2) = k p c1 - k p c2"
        "⋀p X c. singular_chain p X c ⟹ singular_chain (Suc p) X (k p c)"
        "⋀p X c. singular_chain p X c
                 ⟹ chain_boundary (Suc p) (k p c) + k (p - Suc 0) (chain_boundary p c)
                     = (singular_subdivision p ^^ n) c - c"
    by metis
  obtain h where h:
        "⋀p. h p 0 = (0 :: 'a chain)"
        "⋀p c1 c2. h p (c1-c2) = h p c1 - h p c2"
        "⋀p X c. singular_chain p X c ⟹ singular_chain (Suc p) X (h p c)"
        "⋀p X c. singular_chain p X c
                 ⟹ chain_boundary (Suc p) (h p c) + h (p - Suc 0) (chain_boundary p c) = singular_subdivision p c - c"
    by (blast intro: chain_homotopic_singular_subdivision)
  let ?h = "(λp c. singular_subdivision (Suc p) (k p c) + h p c)"
  show ?case
  proof (rule Suc.prems)
    fix p X and c :: "'a chain"
    assume "singular_chain p X c"
    then show "singular_chain (Suc p) X (?h p c)"
      by (simp add: h k singular_chain_add singular_chain_singular_subdivision)
  next
    fix p :: "nat" and X :: "'a topology" and c :: "'a chain"
    assume sc: "singular_chain p X c"
    have f5: "chain_boundary (Suc p) (singular_subdivision (Suc p) (k p c)) = singular_subdivision p (chain_boundary (Suc p) (k p c))"
      using chain_boundary_singular_subdivision k(3) sc by fastforce
    have [simp]: "singular_subdivision (Suc (p - Suc 0)) (k (p - Suc 0) (chain_boundary p c)) =
                  singular_subdivision p (k (p - Suc 0) (chain_boundary p c))"
    proof (cases p)
      case 0
      then show ?thesis
        by (simp add: k chain_boundary_def)
    qed auto
    show "chain_boundary (Suc p) (?h p c) + ?h (p - Suc 0) (chain_boundary p c) = (singular_subdivision p ^^ Suc n) c - c"
      using chain_boundary_singular_subdivision [of "Suc p" X]
      apply (simp add: chain_boundary_add f5 h k algebra_simps)
      apply (smt (verit, ccfv_threshold) add.commute add_diff_eq diff_add_cancel diff_diff_eq2 h(4) k(4) sc singular_subdivision_add)
      done
  qed (auto simp: k h singular_subdivision_diff)
qed

lemma llemma:
  assumes p: "standard_simplex p ⊆ ⋃𝒞"
      and 𝒞: "⋀U. U ∈ 𝒞 ⟹ openin (powertop_real UNIV) U"
  obtains d where "0 < d"
                  "⋀K. ⟦K ⊆ standard_simplex p;
                        ⋀x y i. ⟦i ≤ p; x ∈ K; y ∈ K⟧ ⟹ ¦x i - y i¦ ≤ d⟧
                       ⟹ ∃U. U ∈ 𝒞 ∧ K ⊆ U"
proof -
  have "∃e U. 0 < e ∧ U ∈ 𝒞 ∧ x ∈ U ∧
                (∀y. (∀i≤p. ¦y i - x i¦ ≤ 2 * e) ∧ (∀i>p. y i = 0) ⟶ y ∈ U)"
    if x: "x ∈ standard_simplex p" for x
  proof-
    obtain U where U: "U ∈ 𝒞" "x ∈ U"
      using x p by blast
    then obtain V where finV: "finite {i. V i ≠ UNIV}" and openV: "⋀i. open (V i)"
                  and xV: "x ∈ Pi⇩E UNIV V" and UV: "Pi⇩E UNIV V ⊆ U"
      using 𝒞 unfolding openin_product_topology_alt by force
    have xVi: "x i ∈ V i" for i
      using PiE_mem [OF xV] by simp
    have "⋀i. ∃e>0. ∀x'. ¦x' - x i¦ < e ⟶ x' ∈ V i"
      by (rule openV [unfolded open_real, rule_format, OF xVi])
    then obtain d where d: "⋀i. d i > 0" and dV: "⋀i x'. ¦x' - x i¦ < d i ⟹ x' ∈ V i"
      by metis
    define e where "e ≡ Inf (insert 1 (d ` {i. V i ≠ UNIV})) / 3"
    have ed3: "e ≤ d i / 3" if "V i ≠ UNIV" for i
      using that finV by (auto simp: e_def intro: cInf_le_finite)
    show "∃e U. 0 < e ∧ U ∈ 𝒞 ∧ x ∈ U ∧
                (∀y. (∀i≤p. ¦y i - x i¦ ≤ 2 * e) ∧ (∀i>p. y i = 0) ⟶ y ∈ U)"
    proof (intro exI conjI allI impI)
      show "e > 0"
        using d finV by (simp add: e_def finite_less_Inf_iff)
      fix y assume y: "(∀i≤p. ¦y i - x i¦ ≤ 2 * e) ∧ (∀i>p. y i = 0)"
      have "y ∈ Pi⇩E UNIV V"
      proof
        show "y i ∈ V i" for i
        proof (cases "p < i")
          case True
          then show ?thesis
            by (metis (mono_tags, lifting) y x mem_Collect_eq standard_simplex_def xVi)
        next
          case False show ?thesis
          proof (cases "V i = UNIV")
            case False show ?thesis
            proof (rule dV)
              have "¦y i - x i¦ ≤ 2 * e"
                using y ‹¬ p < i› by simp
              also have "… < d i"
                using ed3 [OF False] ‹e > 0› by simp
              finally show "¦y i - x i¦ < d i" .
            qed
          qed auto
        qed
      qed auto
      with UV show "y ∈ U"
        by blast
    qed (use U in auto)
  qed
  then obtain e U where
      eU: "⋀x. x ∈ standard_simplex p ⟹
                0 < e x ∧ U x ∈ 𝒞 ∧ x ∈ U x"
      and  UI: "⋀x y. ⟦x ∈ standard_simplex p;  ⋀i. i ≤ p ⟹ ¦y i - x i¦ ≤ 2 * e x; ⋀i. i > p ⟹ y i = 0⟧
                       ⟹ y ∈ U x"
    by metis
  define F where "F ≡ λx. Pi⇩E UNIV (λi. if i ≤ p then {x i - e x<..<x i + e x} else UNIV)"
  have "∀S ∈ F ` standard_simplex p. openin (powertop_real UNIV) S"
    by (simp add: F_def openin_PiE_gen)
  moreover have pF: "standard_simplex p ⊆ ⋃(F ` standard_simplex p)"
    by (force simp: F_def PiE_iff eU)
  ultimately have "∃ℱ. finite ℱ ∧ ℱ ⊆ F ` standard_simplex p ∧ standard_simplex p ⊆ ⋃ℱ"
    using compactin_standard_simplex [of p]
    unfolding compactin_def by force
  then obtain S where "finite S" and ssp: "S ⊆ standard_simplex p" "standard_simplex p ⊆ ⋃(F ` S)"
    unfolding ex_finite_subset_image by (auto simp: ex_finite_subset_image)
  then have "S ≠ {}"
    by (auto simp: nonempty_standard_simplex)
  show ?thesis
  proof
    show "Inf (e ` S) > 0"
      using ‹finite S› ‹S ≠ {}› ssp eU by (auto simp: finite_less_Inf_iff)
    fix k :: "(nat ⇒ real) set"
    assume k: "k ⊆ standard_simplex p"
         and kle: "⋀x y i. ⟦i ≤ p; x ∈ k; y ∈ k⟧ ⟹ ¦x i - y i¦ ≤ Inf (e ` S)"
    show "∃U. U ∈ 𝒞 ∧ k ⊆ U"
    proof (cases "k = {}")
      case True
      then show ?thesis
        using ‹S ≠ {}› eU equals0I ssp(1) subset_eq p by auto
    next
      case False
      with k ssp obtain x a where "x ∈ k" "x ∈ standard_simplex p"
                            and a: "a ∈ S" and Fa: "x ∈ F a"
        by blast
      then have le_ea: "⋀i. i ≤ p ⟹ abs (x i - a i) < e a"
        by (simp add: F_def PiE_iff if_distrib abs_diff_less_iff cong: if_cong)
      show ?thesis
      proof (intro exI conjI)
        show "U a ∈ 𝒞"
          using a eU ssp(1) by auto
        show "k ⊆ U a"
        proof clarify
          fix y assume "y ∈ k"
          with k have y: "y ∈ standard_simplex p"
            by blast
          show "y ∈ U a"
          proof (rule UI)
            show "a ∈ standard_simplex p"
              using a ssp(1) by auto
            fix i :: "nat"
            assume "i ≤ p"
            then have "¦x i - y i¦ ≤ e a"
              by (meson kle [OF ‹i ≤ p›] a ‹finite S› ‹x ∈ k› ‹y ∈ k› cInf_le_finite finite_imageI imageI order_trans)
            then show "¦y i - a i¦ ≤ 2 * e a"
              using le_ea [OF ‹i ≤ p›] by linarith
          next
            fix i assume "p < i"
            then show "y i = 0"
              using standard_simplex_def y by auto
          qed
        qed
      qed
    qed
  qed
qed


proposition sufficient_iterated_singular_subdivision_exists:
  assumes 𝒞: "⋀U. U ∈ 𝒞 ⟹ openin X U"
      and X: "topspace X ⊆ ⋃𝒞"
      and p: "singular_chain p X c"
  obtains n where "⋀m f. ⟦n ≤ m; f ∈ Poly_Mapping.keys ((singular_subdivision p ^^ m) c)⟧
                      ⟹ ∃V ∈ 𝒞. f ` (standard_simplex p) ⊆ V"
proof (cases "c = 0")
  case False
  then show ?thesis
  proof (cases "topspace X = {}")
    case True
    show ?thesis
      using p that by (force simp: singular_chain_empty True)
  next
    case False
    show ?thesis
    proof (cases "𝒞 = {}")
      case True
      then show ?thesis
        using False X by blast
    next
      case False
      have "∃e. 0 < e ∧
                (∀K. K ⊆ standard_simplex p ⟶ (∀x y i. x ∈ K ∧ y ∈ K ∧ i ≤ p ⟶ ¦x i - y i¦ ≤ e)
                     ⟶ (∃V. V ∈ 𝒞 ∧ f ` K ⊆ V))"
        if f: "f ∈ Poly_Mapping.keys c" for f
      proof -
        have ssf: "singular_simplex p X f"
          using f p by (auto simp: singular_chain_def)
        then have fp: "⋀x. x ∈ standard_simplex p ⟹ f x ∈ topspace X"
          by (auto simp: singular_simplex_def image_subset_iff dest: continuous_map_image_subset_topspace)
        have "∃T. openin (powertop_real UNIV) T ∧
                    standard_simplex p ∩ f -` V = T ∩ standard_simplex p"
          if V: "V ∈ 𝒞" for V
        proof -
          have "singular_simplex p X f"
            using p f unfolding singular_chain_def by blast
          then have "openin (subtopology (powertop_real UNIV) (standard_simplex p))
                            {x ∈ standard_simplex p. f x ∈ V}"
            using 𝒞 [OF ‹V ∈ 𝒞›] by (simp add: singular_simplex_def continuous_map_def)
          moreover have "standard_simplex p ∩ f -` V = {x ∈ standard_simplex p. f x ∈ V}"
            by blast
          ultimately show ?thesis
            by (simp add: openin_subtopology)
        qed
        then obtain g where gope: "⋀V. V ∈ 𝒞 ⟹ openin (powertop_real UNIV) (g V)"
                and geq: "⋀V. V ∈ 𝒞 ⟹ standard_simplex p ∩ f -` V = g V ∩ standard_simplex p"
          by metis
        obtain d where "0 < d"
              and d: "⋀K. ⟦K ⊆ standard_simplex p; ⋀x y i. ⟦i ≤ p; x ∈ K; y ∈ K⟧ ⟹ ¦x i - y i¦ ≤ d⟧
                       ⟹ ∃U. U ∈ g ` 𝒞 ∧ K ⊆ U"
        proof (rule llemma [of p "g ` 𝒞"])
          show "standard_simplex p ⊆ ⋃(g ` 𝒞)"
            using geq X fp by (fastforce simp add:)
          show "openin (powertop_real UNIV) U" if "U ∈ g ` 𝒞" for U :: "(nat ⇒ real) set"
            using gope that by blast
        qed auto
        show ?thesis
        proof (rule exI, intro allI conjI impI)
          fix K :: "(nat ⇒ real) set"
          assume K: "K ⊆ standard_simplex p"
             and Kd: "∀x y i. x ∈ K ∧ y ∈ K ∧ i ≤ p ⟶ ¦x i - y i¦ ≤ d"
          then have "∃U. U ∈ g ` 𝒞 ∧ K ⊆ U"
            using d [OF K] by auto
          then show "∃V. V ∈ 𝒞 ∧ f ` K ⊆ V"
            using K geq by fastforce
        qed (rule ‹d > 0›)
      qed
      then obtain ψ where epos: "∀f ∈ Poly_Mapping.keys c. 0 < ψ f"
                 and e: "⋀f K. ⟦f ∈ Poly_Mapping.keys c; K ⊆ standard_simplex p;
                                ⋀x y i. x ∈ K ∧ y ∈ K ∧ i ≤ p ⟹ ¦x i - y i¦ ≤ ψ f⟧
                               ⟹ ∃V. V ∈ 𝒞 ∧ f ` K ⊆ V"
        by metis
      obtain d where "0 < d"
               and d: "⋀f K. ⟦f ∈ Poly_Mapping.keys c; K ⊆ standard_simplex p;
                              ⋀x y i. ⟦x ∈ K; y ∈ K; i ≤ p⟧ ⟹ ¦x i - y i¦ ≤ d⟧
                              ⟹ ∃V. V ∈ 𝒞 ∧ f ` K ⊆ V"
      proof
        show "Inf (ψ ` Poly_Mapping.keys c) > 0"
          by (simp add: finite_less_Inf_iff ‹c ≠ 0› epos)
        fix f K
        assume fK: "f ∈ Poly_Mapping.keys c" "K ⊆ standard_simplex p"
          and le: "⋀x y i. ⟦x ∈ K; y ∈ K; i ≤ p⟧ ⟹ ¦x i - y i¦ ≤ Inf (ψ ` Poly_Mapping.keys c)"
        then have lef: "Inf (ψ ` Poly_Mapping.keys c) ≤ ψ f"
          by (auto intro: cInf_le_finite)
        show "∃V. V ∈ 𝒞 ∧ f ` K ⊆ V"
          using le lef by (blast intro: dual_order.trans e [OF fK])
      qed
      let ?d = "λm. (simplicial_subdivision p ^^ m) (frag_of (restrict id (standard_simplex p)))"
      obtain n where n: "(p / (Suc p)) ^ n < d"
        using real_arch_pow_inv ‹0 < d› by fastforce
      show ?thesis
      proof
        fix m h
        assume "n ≤ m" and "h ∈ Poly_Mapping.keys ((singular_subdivision p ^^ m) c)"
        then obtain f where "f ∈ Poly_Mapping.keys c" "h ∈ Poly_Mapping.keys (chain_map p f (?d m))"
          using subsetD [OF keys_frag_extend] iterated_singular_subdivision [OF p, of m] by force
        then obtain g where g: "g ∈ Poly_Mapping.keys (?d m)" and heq: "h = restrict (f ∘ g) (standard_simplex p)"
          using keys_frag_extend by (force simp: chain_map_def simplex_map_def)
        have xx: "simplicial_chain p (standard_simplex p) (?d n) ∧
                  (∀f ∈ Poly_Mapping.keys(?d n). ∀x ∈ standard_simplex p. ∀y ∈ standard_simplex p.
                       ¦f x i - f y i¦ ≤ (p / (Suc p)) ^ n)"
          for n i
        proof (induction n)
          case 0
          have "simplicial_simplex p (standard_simplex p) (λa∈standard_simplex p. a)"
            by (metis eq_id_iff order_refl simplicial_simplex_id)
          moreover have "(∀x∈standard_simplex p. ∀y∈standard_simplex p. ¦x i - y i¦ ≤ 1)"
            unfolding standard_simplex_def
            by (auto simp: abs_if dest!: spec [where x=i])
          ultimately show ?case
            unfolding power_0 funpow_0 by simp
        next
          case (Suc n)
          show ?case
            unfolding power_Suc funpow.simps o_def
          proof (intro conjI ballI)
            show "simplicial_chain p (standard_simplex p) (simplicial_subdivision p (?d n))"
              by (simp add: Suc simplicial_chain_simplicial_subdivision)
            show "¦f x i - f y i¦ ≤ real p / real (Suc p) * (real p / real (Suc p)) ^ n"
              if "f ∈ Poly_Mapping.keys (simplicial_subdivision p (?d n))"
                and "x ∈ standard_simplex p" and "y ∈ standard_simplex p" for f x y
              using Suc that by (blast intro: simplicial_subdivision_shrinks)
          qed
        qed
        have "g ` standard_simplex p ⊆ standard_simplex p"
          using g xx [of m] unfolding simplicial_chain_def simplicial_simplex by auto
        moreover
        have "¦g x i - g y i¦ ≤ d" if "i ≤ p" "x ∈ standard_simplex p" "y ∈ standard_simplex p" for x y i
        proof -
          have "¦g x i - g y i¦ ≤ (p / (Suc p)) ^ m"
            using g xx [of m] that by blast
          also have "… ≤ (p / (Suc p)) ^ n"
            by (auto intro: power_decreasing [OF ‹n ≤ m›])
          finally show ?thesis using n by simp
        qed
        then have "¦x i - y i¦ ≤ d"
          if "x ∈ g ` (standard_simplex p)" "y ∈ g ` (standard_simplex p)" "i ≤ p" for i x y
          using that by blast
        ultimately show "∃V∈𝒞. h ` standard_simplex p ⊆ V"
          using ‹f ∈ Poly_Mapping.keys c› d [of f "g ` standard_simplex p"]
          by (simp add: Bex_def heq image_image)
      qed
    qed
  qed
qed force


lemma small_homologous_rel_relcycle_exists:
  assumes 𝒞: "⋀U. U ∈ 𝒞 ⟹ openin X U"
      and X: "topspace X ⊆ ⋃𝒞"
      and p: "singular_relcycle p X S c"
    obtains c' where "singular_relcycle p X S c'" "homologous_rel p X S c c'"
                      "⋀f. f ∈ Poly_Mapping.keys c' ⟹ ∃V ∈ 𝒞. f ` (standard_simplex p) ⊆ V"
proof -
  have "singular_chain p X c"
       "(chain_boundary p c, 0) ∈ (mod_subset (p - Suc 0) (subtopology X S))"
    using p unfolding singular_relcycle_def by auto
  then obtain n where n: "⋀m f. ⟦n ≤ m; f ∈ Poly_Mapping.keys ((singular_subdivision p ^^ m) c)⟧
                            ⟹ ∃V ∈ 𝒞. f ` (standard_simplex p) ⊆ V"
    by (blast intro: sufficient_iterated_singular_subdivision_exists [OF 𝒞 X])
  let ?c' = "(singular_subdivision p ^^ n) c"
  show ?thesis
  proof
    show "homologous_rel p X S c ?c'"
      apply (induction n, simp_all)
      by (metis p homologous_rel_singular_subdivision homologous_rel_singular_relcycle homologous_rel_trans homologous_rel_sym)
    then show "singular_relcycle p X S ?c'"
      by (metis homologous_rel_singular_relcycle p)
  next
    fix f :: "(nat ⇒ real) ⇒ 'a"
    assume "f ∈ Poly_Mapping.keys ?c'"
    then show "∃V∈𝒞. f ` standard_simplex p ⊆ V"
      by (rule n [OF order_refl])
  qed
qed

lemma excised_chain_exists:
  fixes S :: "'a set"
  assumes "X closure_of U ⊆ X interior_of T" "T ⊆ S" "singular_chain p (subtopology X S) c"
  obtains n d e where "singular_chain p (subtopology X (S - U)) d"
                      "singular_chain p (subtopology X T) e"
                      "(singular_subdivision p ^^ n) c = d + e"
proof -
  have *: "∃n d e. singular_chain p (subtopology X (S - U)) d ∧
                  singular_chain p (subtopology X T) e ∧
                  (singular_subdivision p ^^ n) c = d + e"
    if c: "singular_chain p (subtopology X S) c"
       and X: "X closure_of U ⊆ X interior_of T" "U ⊆ topspace X" and S: "T ⊆ S" "S ⊆ topspace X"
       for p X c S and T U :: "'a set"
  proof -
    obtain n where n: "⋀m f. ⟦n ≤ m; f ∈ Poly_Mapping.keys ((singular_subdivision p ^^ m) c)⟧
                             ⟹ ∃V ∈ {S ∩ X interior_of T, S - X closure_of U}. f ` standard_simplex p ⊆ V"
      apply (rule sufficient_iterated_singular_subdivision_exists
                   [of "{S ∩ X interior_of T, S - X closure_of U}"])
      using X S c
      by (auto simp: topspace_subtopology openin_subtopology_Int2 openin_subtopology_diff_closed)
    let ?c' = "λn. (singular_subdivision p ^^ n) c"
    have "singular_chain p (subtopology X S) (?c' m)" for m
      by (induction m) (auto simp: singular_chain_singular_subdivision c)
    then have scp: "singular_chain p (subtopology X S) (?c' n)" .

    have SS: "Poly_Mapping.keys (?c' n) ⊆ singular_simplex_set p (subtopology X (S - U))
                              ∪ singular_simplex_set p (subtopology X T)"
    proof (clarsimp)
      fix f
      assume f: "f ∈ Poly_Mapping.keys ((singular_subdivision p ^^ n) c)"
         and non: "¬ singular_simplex p (subtopology X T) f"
      show "singular_simplex p (subtopology X (S - U)) f"
        using n [OF order_refl f] scp f non closure_of_subset [OF ‹U ⊆ topspace X›] interior_of_subset [of X T]
        by (fastforce simp: image_subset_iff singular_simplex_subtopology singular_chain_def)
    qed
    show ?thesis
       unfolding singular_chain_def using frag_split [OF SS] by metis
  qed
  have "(subtopology X (topspace X ∩ S)) = (subtopology X S)"
    by (metis subtopology_subtopology subtopology_topspace)
  with assms have c: "singular_chain p (subtopology X (topspace X ∩ S)) c"
    by simp
  have Xsub: "X closure_of (topspace X ∩ U) ⊆ X interior_of (topspace X ∩ T)"
    using assms closure_of_restrict interior_of_restrict by fastforce
  obtain n d e where
    d: "singular_chain p (subtopology X (topspace X ∩ S - topspace X ∩ U)) d"
    and e: "singular_chain p (subtopology X (topspace X ∩ T)) e"
    and de: "(singular_subdivision p ^^ n) c = d + e"
    using *[OF c Xsub, simplified] assms by force
  show thesis
  proof
    show "singular_chain p (subtopology X (S - U)) d"
      by (metis d Diff_Int_distrib inf.cobounded2 singular_chain_mono)
    show "singular_chain p (subtopology X T) e"
      by (metis e inf.cobounded2 singular_chain_mono)
    show "(singular_subdivision p ^^ n) c = d + e"
      by (rule de)
  qed
qed


lemma excised_relcycle_exists:
  fixes S :: "'a set"
  assumes X: "X closure_of U ⊆ X interior_of T" and "T ⊆ S"
      and c: "singular_relcycle p (subtopology X S) T c"
  obtains c' where "singular_relcycle p (subtopology X (S - U)) (T - U) c'"
                   "homologous_rel p (subtopology X S) T c c'"
proof -
  have [simp]: "(S - U) ∩ (T - U) = T - U" "S ∩ T = T"
    using ‹T ⊆ S› by auto
  have scc: "singular_chain p (subtopology X S) c"
    and scp1: "singular_chain (p - Suc 0) (subtopology X T) (chain_boundary p c)"
    using c by (auto simp: singular_relcycle_def mod_subset_def subtopology_subtopology)
  obtain n d e where d: "singular_chain p (subtopology X (S - U)) d"
    and e: "singular_chain p (subtopology X T) e"
    and de: "(singular_subdivision p ^^ n) c = d + e"
    using excised_chain_exists [OF X ‹T ⊆ S› scc] .
  have scSUd: "singular_chain (p - Suc 0) (subtopology X (S - U)) (chain_boundary p d)"
    by (simp add: singular_chain_boundary d)
  have sccn: "singular_chain p (subtopology X S) ((singular_subdivision p ^^ n) c)" for n
    by (induction n) (auto simp: singular_chain_singular_subdivision scc)
  have "singular_chain (p - Suc 0) (subtopology X T) (chain_boundary p ((singular_subdivision p ^^ n) c))"
  proof (induction n)
    case (Suc n)
    then show ?case
      by (simp add: singular_chain_singular_subdivision chain_boundary_singular_subdivision [OF sccn])
  qed (auto simp: scp1)
  then have "singular_chain (p - Suc 0) (subtopology X T) (chain_boundary p ((singular_subdivision p ^^ n) c - e))"
    by (simp add: chain_boundary_diff singular_chain_diff singular_chain_boundary e)
  with de have scTd: "singular_chain (p - Suc 0) (subtopology X T) (chain_boundary p d)"
    by simp
  show thesis
  proof
    have "singular_chain (p - Suc 0) X (chain_boundary p d)"
      using scTd singular_chain_subtopology by blast
    with scSUd scTd have "singular_chain (p - Suc 0) (subtopology X (T - U)) (chain_boundary p d)"
      by (fastforce simp add: singular_chain_subtopology)
    then show "singular_relcycle p (subtopology X (S - U)) (T - U) d"
      by (auto simp: singular_relcycle_def mod_subset_def subtopology_subtopology d)
    have "homologous_rel p (subtopology X S) T (c-0) ((singular_subdivision p ^^ n) c - e)"
    proof (rule homologous_rel_diff)
      show "homologous_rel p (subtopology X S) T c ((singular_subdivision p ^^ n) c)"
      proof (induction n)
        case (Suc n)
        then show ?case
          apply simp
          apply (rule homologous_rel_trans)
          using c homologous_rel_singular_relcycle_1 homologous_rel_singular_subdivision homologous_rel_sym by blast
      qed auto
      show "homologous_rel p (subtopology X S) T 0 e"
        unfolding homologous_rel_def using e
        by (intro singular_relboundary_diff singular_chain_imp_relboundary; simp add: subtopology_subtopology)
    qed
    with de show "homologous_rel p (subtopology X S) T c d"
      by simp
  qed
qed


subsection‹Homotopy invariance›

theorem homotopic_imp_homologous_rel_chain_maps:
  assumes hom: "homotopic_with (λh. h ` T ⊆ V) S U f g" and c: "singular_relcycle p S T c"
  shows "homologous_rel p U V (chain_map p f c) (chain_map p g c)"
proof -
  note sum.atMost_Suc [simp del]
  have contf: "continuous_map S U f" and contg: "continuous_map S U g"
    using homotopic_with_imp_continuous_maps [OF hom] by metis+
  obtain h where conth: "continuous_map (prod_topology (top_of_set {0..1::real}) S) U h"
    and h0: "⋀x. h(0, x) = f x"
    and h1: "⋀x. h(1, x) = g x"
    and hV: "⋀t x. ⟦0 ≤ t; t ≤ 1; x ∈ T⟧ ⟹ h(t,x) ∈ V"
    using hom by (fastforce simp: homotopic_with_def)
  define vv where "vv ≡ λj i. if i = Suc j then 1 else (0::real)"
  define ww where "ww ≡ λj i. if i=0 ∨ i = Suc j then 1 else (0::real)"
  define simp where "simp ≡ λq i. oriented_simplex (Suc q) (λj. if j ≤ i then vv j else ww(j -1))"
  define pr where "pr ≡ λq c. ∑i≤q. frag_cmul ((-1) ^ i)
                                        (frag_of (simplex_map (Suc q) (λz. h(z 0, c(z ∘ Suc))) (simp q i)))"
  have ss_ss: "simplicial_simplex (Suc q) ({x. x 0 ∈ {0..1} ∧ (x ∘ Suc) ∈ standard_simplex q}) (simp q i)"
    if "i ≤ q" for q i
  proof -
    have "(∑j≤Suc q. (if j ≤ i then vv j 0 else ww (j -1) 0) * x j) ∈ {0..1}"
      if "x ∈ standard_simplex (Suc q)" for x
    proof -
      have "(∑j≤Suc q. if j ≤ i then 0 else x j) ≤ sum x {..Suc q}"
        using that unfolding standard_simplex_def
        by (force intro!: sum_mono)
      with ‹i ≤ q› that show ?thesis
        by (simp add: vv_def ww_def standard_simplex_def if_distrib [of "λu. u * _"] sum_nonneg cong: if_cong)
    qed
    moreover
    have "(λk. ∑j≤Suc q. (if j ≤ i then vv j k else ww (j -1) k) * x j) ∘ Suc ∈ standard_simplex q"
      if "x ∈ standard_simplex (Suc q)" for x
    proof -
      have card: "({..q} ∩ {k. Suc k = j}) = {j-1}" if "0 < j" "j ≤ Suc q" for j
        using that by auto
      have eq: "(∑j≤Suc q. ∑k≤q. if j ≤ i then if k = j then x j else 0 else if Suc k = j then x j else 0)
              = (∑j≤Suc q. x j)"
        by (rule sum.cong [OF refl]) (use ‹i ≤ q› in ‹simp add: sum.If_cases card›)
      have "(∑j≤Suc q. if j ≤ i then if k = j then x j else 0 else if Suc k = j then x j else 0)
            ≤ sum x {..Suc q}" for k
        using that unfolding standard_simplex_def
        by (force intro!: sum_mono)
      then show ?thesis
        using ‹i ≤ q› that
        by (simp add: vv_def ww_def standard_simplex_def if_distrib [of "λu. u * _"] sum_nonneg
            sum.swap [where A = "atMost q"] eq cong: if_cong)
    qed
    ultimately show ?thesis
      by (simp add: that simplicial_simplex_oriented_simplex simp_def image_subset_iff if_distribR)
  qed
  obtain prism where prism: "⋀q. prism q 0 = 0"
    "⋀q c. singular_chain q S c ⟹ singular_chain (Suc q) U (prism q c)"
    "⋀q c. singular_chain q (subtopology S T) c
                           ⟹ singular_chain (Suc q) (subtopology U V) (prism q c)"
    "⋀q c. singular_chain q S c
                           ⟹ chain_boundary (Suc q) (prism q c) =
                               chain_map q g c - chain_map q f c - prism (q -1) (chain_boundary q c)"
  proof
    show "(frag_extend ∘ pr) q 0 = 0" for q
      by (simp add: pr_def)
  next
    show "singular_chain (Suc q) U ((frag_extend ∘ pr) q c)"
      if "singular_chain q S c" for q c
      using that [unfolded singular_chain_def]
    proof (induction c rule: frag_induction)
      case (one m)
      show ?case
      proof (simp add: pr_def, intro singular_chain_cmul singular_chain_sum)
        fix i :: "nat"
        assume "i ∈ {..q}"
        define X where "X = subtopology (powertop_real UNIV) {x. x 0 ∈ {0..1} ∧ (x ∘ Suc) ∈ standard_simplex q}"
        show "singular_chain (Suc q) U
                 (frag_of (simplex_map (Suc q) (λz. h (z 0, m (z ∘ Suc))) (simp q i)))"
          unfolding singular_chain_of
        proof (rule singular_simplex_simplex_map)
          show "singular_simplex (Suc q) X (simp q i)"
            unfolding X_def using ‹i ∈ {..q}› simplicial_imp_singular_simplex ss_ss by blast
          have 0: "continuous_map X (top_of_set {0..1}) (λx. x 0)"
            unfolding continuous_map_in_subtopology topspace_subtopology X_def
            by (auto intro: continuous_map_product_projection continuous_map_from_subtopology)
          have 1: "continuous_map X S (m ∘ (λx j. x (Suc j)))"
          proof (rule continuous_map_compose)
            have "continuous_map (powertop_real UNIV) (powertop_real UNIV) (λx j. x (Suc j))"
              by (auto intro: continuous_map_product_projection)
            then show "continuous_map X (subtopology (powertop_real UNIV) (standard_simplex q)) (λx j. x (Suc j))"
              unfolding X_def o_def
              by (auto simp: continuous_map_in_subtopology intro: continuous_map_from_subtopology continuous_map_product_projection)
          qed (use one in ‹simp add: singular_simplex_def›)
          show "continuous_map X U (λz. h (z 0, m (z ∘ Suc)))"
            apply (rule continuous_map_compose [unfolded o_def, OF _ conth])
            using 0 1 by (simp add: continuous_map_pairwise o_def)
        qed
      qed
    next
      case (diff a b)
      then show ?case
        apply (simp add: frag_extend_diff keys_diff)
        using singular_chain_def singular_chain_diff by blast
    qed auto
  next
    show "singular_chain (Suc q) (subtopology U V) ((frag_extend ∘ pr) q c)"
      if "singular_chain q (subtopology S T) c" for q c
      using that [unfolded singular_chain_def]
    proof (induction c rule: frag_induction)
      case (one m)
      show ?case
      proof (simp add: pr_def, intro singular_chain_cmul singular_chain_sum)
        fix i :: "nat"
        assume "i ∈ {..q}"
        define X where "X = subtopology (powertop_real UNIV) {x. x 0 ∈ {0..1} ∧ (x ∘ Suc) ∈ standard_simplex q}"
        show "singular_chain (Suc q) (subtopology U V)
                 (frag_of (simplex_map (Suc q) (λz. h (z 0, m (z ∘ Suc))) (simp q i)))"
          unfolding singular_chain_of
        proof (rule singular_simplex_simplex_map)
          show "singular_simplex (Suc q) X (simp q i)"
            unfolding X_def using ‹i ∈ {..q}› simplicial_imp_singular_simplex ss_ss by blast
          have 0: "continuous_map X (top_of_set {0..1}) (λx. x 0)"
            unfolding continuous_map_in_subtopology topspace_subtopology X_def
            by (auto intro: continuous_map_product_projection continuous_map_from_subtopology)
          have 1: "continuous_map X (subtopology S T) (m ∘ (λx j. x (Suc j)))"
          proof (rule continuous_map_compose)
            have "continuous_map (powertop_real UNIV) (powertop_real UNIV) (λx j. x (Suc j))"
              by (auto intro: continuous_map_product_projection)
            then show "continuous_map X (subtopology (powertop_real UNIV) (standard_simplex q)) (λx j. x (Suc j))"
              unfolding X_def o_def
              by (auto simp: continuous_map_in_subtopology intro: continuous_map_from_subtopology continuous_map_product_projection)
            show "continuous_map (subtopology (powertop_real UNIV) (standard_simplex q)) (subtopology S T) m"
              using one continuous_map_into_fulltopology by (auto simp: singular_simplex_def)
          qed
          have "continuous_map X (subtopology U V) (h ∘ (λz. (z 0, m (z ∘ Suc))))"
          proof (rule continuous_map_compose)
            show "continuous_map X (prod_topology (top_of_set {0..1::real}) (subtopology S T)) (λz. (z 0, m (z ∘ Suc)))"
              using 0 1 by (simp add: continuous_map_pairwise o_def)
            have "continuous_map (subtopology (prod_topology euclideanreal S) ({0..1} × T)) U h"
              by (metis conth continuous_map_from_subtopology subtopology_Times subtopology_topspace)
            with hV show "continuous_map (prod_topology (top_of_set {0..1::real}) (subtopology S T)) (subtopology U V) h"
              by (force simp: topspace_subtopology continuous_map_in_subtopology subtopology_restrict subtopology_Times)
          qed
          then show "continuous_map X (subtopology U V) (λz. h (z 0, m (z ∘ Suc)))"
            by (simp add: o_def)
        qed
      qed
    next
      case (diff a b)
      then show ?case
        by (metis comp_apply frag_extend_diff singular_chain_diff)
    qed auto
  next
    show "chain_boundary (Suc q) ((frag_extend ∘ pr) q c) =
        chain_map q g c - chain_map q f c - (frag_extend ∘ pr) (q -1) (chain_boundary q c)"
      if "singular_chain q S c" for q c
      using that [unfolded singular_chain_def]
    proof (induction c rule: frag_induction)
      case (one m)
      have eq2: "Sigma S T = (λi. (i,i)) ` {i ∈ S. i ∈ T i} ∪ (Sigma S (λi. T i - {i}))" for S :: "nat set" and T
        by force
      have 1: "(∑(i,j)∈(λi. (i, i)) ` {i. i ≤ q ∧ i ≤ Suc q}.
                   frag_cmul (((-1) ^ i) * (-1) ^ j)
                      (frag_of
                        (singular_face (Suc q) j
                          (simplex_map (Suc q) (λz. h (z 0, m (z ∘ Suc))) (simp q i)))))
             + (∑(i,j)∈(λi. (i, i)) ` {i. i ≤ q}.
                     frag_cmul (- ((-1) ^ i * (-1) ^ j))
                        (frag_of
                          (singular_face (Suc q) (Suc j)
                            (simplex_map (Suc q) (λz. h (z 0, m (z ∘ Suc))) (simp q i)))))
             = frag_of (simplex_map q g m) - frag_of (simplex_map q f m)"
      proof -
        have "restrict ((λz. h (z 0, m (z ∘ Suc))) ∘ (simp q 0 ∘ simplical_face 0)) (standard_simplex q)
          = restrict (g ∘ m) (standard_simplex q)"
        proof (rule restrict_ext)
          fix x
          assume x: "x ∈ standard_simplex q"
          have "(∑j≤Suc q. if j = 0 then 0 else x (j - Suc 0)) = (∑j≤q. x j)"
            by (simp add: sum.atMost_Suc_shift)
          with x have "simp q 0 (simplical_face 0 x) 0 = 1"
            apply (simp add: oriented_simplex_def simp_def simplical_face_in_standard_simplex)
            apply (simp add: simplical_face_def if_distrib ww_def standard_simplex_def cong: if_cong)
            done
          moreover
          have "(λn. if n ≤ q then x n else 0) = x"
            using standard_simplex_def x by auto
          then have "(λn. simp q 0 (simplical_face 0 x) (Suc n)) = x"
            unfolding oriented_simplex_def simp_def ww_def using x
            apply (simp add: simplical_face_in_standard_simplex)
            apply (simp add: simplical_face_def if_distrib)
            apply (simp add: if_distribR if_distrib cong: if_cong)
            done
          ultimately show "((λz. h (z 0, m (z ∘ Suc))) ∘ (simp q 0 ∘ simplical_face 0)) x = (g ∘ m) x"
            by (simp add: o_def h1)
        qed
        then have a: "frag_of (singular_face (Suc q) 0 (simplex_map (Suc q) (λz. h (z 0, m (z ∘ Suc))) (simp q 0)))
             = frag_of (simplex_map q g m)"
          by (simp add: singular_face_simplex_map) (simp add: simplex_map_def)
        have "restrict ((λz. h (z 0, m (z ∘ Suc))) ∘ (simp q q ∘ simplical_face (Suc q))) (standard_simplex q)
          = restrict (f ∘ m) (standard_simplex q)"
        proof (rule restrict_ext)
          fix x
          assume x: "x ∈ standard_simplex q"
          then have "simp q q (simplical_face (Suc q) x) 0 = 0"
            unfolding oriented_simplex_def simp_def
            by (simp add: simplical_face_in_standard_simplex sum.atMost_Suc) (simp add: simplical_face_def vv_def)
          moreover have "(λn. simp q q (simplical_face (Suc q) x) (Suc n)) = x"
            unfolding oriented_simplex_def simp_def vv_def using x
            apply (simp add: simplical_face_in_standard_simplex)
            apply (force simp: standard_simplex_def simplical_face_def if_distribR if_distrib [of "λx. x * _"] sum.atMost_Suc cong: if_cong)
            done
          ultimately show "((λz. h (z 0, m (z ∘ Suc))) ∘ (simp q q ∘ simplical_face (Suc q))) x = (f ∘ m) x"
            by (simp add: o_def h0)
        qed
        then have b: "frag_of (singular_face (Suc q) (Suc q)
                     (simplex_map (Suc q) (λz. h (z 0, m (z ∘ Suc))) (simp q q)))
          = frag_of (simplex_map q f m)"
          by (simp add: singular_face_simplex_map) (simp add: simplex_map_def)
        have sfeq: "simplex_map q (λz. h (z 0, m (z ∘ Suc))) (simp q (Suc i) ∘ simplical_face (Suc i))
                = simplex_map q (λz. h (z 0, m (z ∘ Suc))) (simp q i ∘ simplical_face (Suc i))"
          if "i < q" for i
          unfolding simplex_map_def
        proof (rule restrict_ext)
          fix x
          assume "x ∈ standard_simplex q"
          then have "(simp q (Suc i) ∘ simplical_face (Suc i)) x = (simp q i ∘ simplical_face (Suc i)) x"
            unfolding oriented_simplex_def simp_def simplical_face_def
            by (force intro: sum.cong)
          then show "((λz. h (z 0, m (z ∘ Suc))) ∘ (simp q (Suc i) ∘ simplical_face (Suc i))) x
                 = ((λz. h (z 0, m (z ∘ Suc))) ∘ (simp q i ∘ simplical_face (Suc i))) x"
            by simp
        qed
        have eqq: "{i. i ≤ q ∧ i ≤ Suc q} = {..q}"
          by force
        have qeq: "{..q} = insert 0 ((λi. Suc i) ` {i. i < q})" "{i. i ≤ q} = insert q {i. i < q}"
          using le_imp_less_Suc less_Suc_eq_0_disj by auto
        show ?thesis
          using a b
          apply (simp add: sum.reindex inj_on_def eqq)
          apply (simp add: qeq sum.insert_if sum.reindex sum_negf singular_face_simplex_map sfeq)
          done
      qed
      have 2: "(∑(i,j)∈(SIGMA i:{..q}. {0..min (Suc q) i} - {i}).
                     frag_cmul ((-1) ^ i * (-1) ^ j)
                      (frag_of
                        (singular_face (Suc q) j
                          (simplex_map (Suc q) (λz. h (z 0, m (z ∘ Suc))) (simp q i)))))
             + (∑(i,j)∈(SIGMA i:{..q}. {i..q} - {i}).
                 frag_cmul (- ((-1) ^ i * (-1) ^ j))
                  (frag_of
                    (singular_face (Suc q) (Suc j)
                      (simplex_map (Suc q) (λz. h (z 0, m (z ∘ Suc))) (simp q i)))))
             = - frag_extend (pr (q - Suc 0)) (chain_boundary q (frag_of m))"
      proof (cases "q=0")
        case True
        then show ?thesis
          by (simp add: chain_boundary_def flip: sum.Sigma)
      next
        case False
        have eq: "{..q - Suc 0} × {..q} = Sigma {..q - Suc 0} (λi. {0..min q i}) ∪ Sigma {..q} (λi. {i<..q})"
          by force
        have I: "(∑(i,j)∈(SIGMA i:{..q}. {0..min (Suc q) i} - {i}).
                    frag_cmul ((-1) ^ (i + j))
                      (frag_of
                        (singular_face (Suc q) j
                          (simplex_map (Suc q) (λz. h (z 0, m (z ∘ Suc))) (simp q i)))))
               = (∑(i,j)∈(SIGMA i:{..q - Suc 0}. {0..min q i}).
                   frag_cmul (- ((-1) ^ (j + i)))
                    (frag_of
                      (simplex_map q (λz. h (z 0, singular_face q j m (z ∘ Suc)))
                        (simp (q - Suc 0) i))))"
        proof -
          have seq: "simplex_map q (λz. h (z 0, singular_face q j m (z ∘ Suc)))
                       (simp (q - Suc 0) (i - Suc 0))
                   = simplex_map q (λz. h (z 0, m (z ∘ Suc))) (simp q i ∘ simplical_face j)"
            if ij: "i ≤ q" "j ≠ i" "j ≤ i" for i j
            unfolding simplex_map_def
          proof (rule restrict_ext)
            fix x
            assume x: "x ∈ standard_simplex q"
            have "i > 0"
              using that by force
            then have iq: "i - Suc 0 ≤ q - Suc 0"
              using ‹i ≤ q› False by simp
            have q0_eq: "{..Suc q} = insert 0 (Suc ` {..q})"
              by (auto simp: image_def gr0_conv_Suc)
            have α: "simp (q - Suc 0) (i - Suc 0) x 0 = simp q i (simplical_face j x) 0"
              using False x ij
              unfolding oriented_simplex_def simp_def vv_def ww_def
              apply (simp add: simplical_face_in_standard_simplex)
              apply (force simp: simplical_face_def q0_eq sum.reindex intro!: sum.cong)
              done
            have β: "simplical_face j (simp (q - Suc 0) (i - Suc 0) x ∘ Suc) = simp q i (simplical_face j x) ∘ Suc"
            proof
              fix k
              show "simplical_face j (simp (q - Suc 0) (i - Suc 0) x ∘ Suc) k
                  = (simp q i (simplical_face j x) ∘ Suc) k"
                using False x ij
                unfolding oriented_simplex_def simp_def o_def vv_def ww_def
                apply (simp add: simplical_face_in_standard_simplex if_distribR)
                apply (simp add: simplical_face_def if_distrib [of "λu. u * _"] cong: if_cong)
                apply (intro impI conjI)
                 apply (force simp: sum.atMost_Suc intro: sum.cong)
                apply (force simp: q0_eq sum.reindex intro!: sum.cong)
                done
            qed
            have "simp (q - Suc 0) (i - Suc 0) x ∘ Suc ∈ standard_simplex (q - Suc 0)"
              using ss_ss [OF iq] ‹i ≤ q› False ‹i > 0›
              apply (simp add: simplicial_simplex image_subset_iff)
              using ‹x ∈ standard_simplex q› by blast
            then show "((λz. h (z 0, singular_face q j m (z ∘ Suc))) ∘ simp (q - Suc 0) (i - Suc 0)) x
                = ((λz. h (z 0, m (z ∘ Suc))) ∘ (simp q i ∘ simplical_face j)) x"
              by (simp add: singular_face_def α β)
          qed
          have [simp]: "(-1::int) ^ (i + j - Suc 0) = - ((-1) ^ (i + j))" if "i ≠ j" for i j::nat
          proof -
            have "i + j > 0"
              using that by blast
            then show ?thesis
              by (metis (no_types, opaque_lifting) One_nat_def Suc_diff_1 add.inverse_inverse mult.left_neutral mult_minus_left power_Suc)
          qed
          show ?thesis
            apply (rule sum.eq_general_inverses [where h = "λ(a,b). (a-1,b)" and k = "λ(a,b). (Suc a,b)"])
            using False apply (auto simp: singular_face_simplex_map seq add.commute)
            done
        qed
        have *: "singular_face (Suc q) (Suc j) (simplex_map (Suc q) (λz. h (z 0, m (z ∘ Suc))) (simp q i))
               = simplex_map q (λz. h (z 0, singular_face q j m (z ∘ Suc))) (simp (q - Suc 0) i)"
          if ij: "i < j" "j ≤ q" for i j
        proof -
          have iq: "i ≤ q - Suc 0"
            using that by auto
          have sf_eqh: "singular_face (Suc q) (Suc j)
                           (λx. if x ∈ standard_simplex (Suc q)
                                then ((λz. h (z 0, m (z ∘ Suc))) ∘ simp q i) x else undefined) x
                      = h (simp (q - Suc 0) i x 0,
                           singular_face q j m (λxa. simp (q - Suc 0) i x (Suc xa)))"
            if x: "x ∈ standard_simplex q" for x
          proof -
            let ?f = "λk. ∑j≤q. if j ≤ i then if k = j then x j else 0
                               else if Suc k = j then x j else 0"
            have fm: "simplical_face (Suc j) x ∈ standard_simplex (Suc q)"
              using ss_ss [OF iq] that ij
              by (simp add: simplical_face_in_standard_simplex)
            have ss: "?f ∈ standard_simplex (q - Suc 0)"
              unfolding standard_simplex_def
            proof (intro CollectI conjI impI allI)
              fix k
              show "0 ≤ ?f k"
                using that by (simp add: sum_nonneg standard_simplex_def)
              show "?f k ≤ 1"
                using x sum_le_included [of "{..q}" "{..q}" x "id"]
                by (simp add: standard_simplex_def)
              assume k: "q - Suc 0 < k"
              show "?f k = 0"
                by (rule sum.neutral) (use that x iq k standard_simplex_def in auto)
            next
              have "(∑k≤q - Suc 0. ?f k)
                  = (∑(k,j) ∈ ({..q - Suc 0} × {..q}) ∩ {(k,j). if j ≤ i then k = j else Suc k = j}. x j)"
                apply (simp add: sum.Sigma)
                by (rule sum.mono_neutral_cong) (auto simp: split: if_split_asm)
              also have "… = sum x {..q}"
                apply (rule sum.eq_general_inverses
                    [where h = "λ(k,j). if j≤i ∧ k=j ∨ j>i ∧ Suc k = j then j else Suc q"
                      and k = "λj. if j ≤ i then (j,j) else (j - Suc 0, j)"])
                using ij by auto
              also have "… = 1"
                using x by (simp add: standard_simplex_def)
              finally show "(∑k≤q - Suc 0. ?f k) = 1"
                by (simp add: standard_simplex_def)
            qed
            let ?g = "λk. if k ≤ i then 0
                              else if k < Suc j then x k
                                   else if k = Suc j then 0 else x (k - Suc 0)"
            have eq: "{..Suc q} = {..j} ∪ {Suc j} ∪ Suc`{j<..q}" "{..q} = {..j} ∪ {j<..q}"
              using ij image_iff less_Suc_eq_0_disj less_Suc_eq_le
              by (force simp: image_iff)+
            then have "(∑k≤Suc q. ?g k) = (∑k∈{..j} ∪ {Suc j} ∪ Suc`{j<..q}. ?g k)"
              by simp
            also have "… = (∑k∈{..j} ∪ Suc`{j<..q}. ?g k)"
              by (rule sum.mono_neutral_right) auto
            also have "… = (∑k∈{..j}. ?g k) + (∑k∈Suc`{j<..q}. ?g k)"
              by (rule sum.union_disjoint) auto
            also have "… = (∑k∈{..j}. ?g k) + (∑k∈{j<..q}. ?g (Suc k))"
              by (auto simp: sum.reindex)
            also have "… = (∑k∈{..j}. if k ≤ i then 0 else x k)
                           + (∑k∈{j<..q}. if k ≤ i then 0 else x k)"
              by (intro sum.cong arg_cong2 [of concl: "(+)"]) (use ij in auto)
            also have "… = (∑k≤q. if k ≤ i then 0 else x k)"
              unfolding eq by (subst sum.union_disjoint) auto
            finally have "(∑k≤Suc q. ?g k) = (∑k≤q. if k ≤ i then 0 else x k)" .
            then have QQ: "(∑l≤Suc q. if l ≤ i then 0 else simplical_face (Suc j) x l) = (∑j≤q. if j ≤ i then 0 else x j)"
              by (simp add: simplical_face_def cong: if_cong)
            have WW: "(λk. ∑l≤Suc q. if l ≤ i
                                    then if k = l then simplical_face (Suc j) x l else 0
                                    else if Suc k = l then simplical_face (Suc j) x l
                                    else 0)
                = simplical_face j
                   (λk. ∑j≤q. if j ≤ i then if k = j then x j else 0
                                else if Suc k = j then x j else 0)"
            proof -
              have *: "(∑l≤q. if l ≤ i then 0 else if Suc k = l then x (l - Suc 0) else 0)
                    = (∑l≤q. if l ≤ i then if k - Suc 0 = l then x l else 0 else if k = l then x l else 0)"
                (is "?lhs = ?rhs")
                if "k ≠ q" "k > j" for k
              proof (cases "k ≤ q")
                case True
                have "?lhs = sum (λl. x (l - Suc 0)) {Suc k}" "?rhs = sum x {k}"
                  by (rule sum.mono_neutral_cong_right; use True ij that in auto)+
                then show ?thesis
                  by simp
              next
                case False
                have "?lhs = 0" "?rhs = 0"
                  by (rule sum.neutral; use False ij in auto)+
                then show ?thesis
                  by simp
              qed
              show ?thesis
                apply (rule ext)
                unfolding simplical_face_def using ij
                apply (auto simp: sum.atMost_Suc cong: if_cong)
                 apply (force simp flip: ivl_disj_un(2) intro: sum.neutral)
                 apply (auto simp: *)
                done
            qed
            show ?thesis
              using False that iq
              unfolding oriented_simplex_def simp_def vv_def ww_def
              apply (simp add: if_distribR cong: if_cong)
              apply (simp add: simplical_face_def if_distrib [of "λu. u * _"] o_def cong: if_cong)
              apply (simp add: singular_face_def fm ss QQ WW)
              done
          qed
          show ?thesis
            unfolding simplex_map_def restrict_def
            apply (simp add: simplicial_simplex image_subset_iff o_def sf_eqh fun_eq_iff)
            apply (simp add: singular_face_def)
            done
        qed
        have sgeq: "(SIGMA i:{..q}. {i..q} - {i})  = (SIGMA i:{..q}. {i<..q})"
          by force
        have II: "(∑(i,j)∈(SIGMA i:{..q}. {i..q} - {i}).
                     frag_cmul (- ((-1) ^ (i + j)))
                      (frag_of
                        (singular_face (Suc q) (Suc j)
                          (simplex_map (Suc q) (λz. h (z 0, m (z ∘ Suc))) (simp q i))))) =
                  (∑(i,j)∈(SIGMA i:{..q}. {i<..q}).
                     frag_cmul (- ((-1) ^ (j + i)))
                      (frag_of
                        (simplex_map q (λz. h (z 0, singular_face q j m (z ∘ Suc)))
                          (simp (q - Suc 0) i))))"
          by (force simp: * sgeq add.commute intro: sum.cong)
        show ?thesis
          using False
          apply (simp add: chain_boundary_def frag_extend_sum frag_extend_cmul frag_cmul_sum pr_def flip: sum_negf power_add)
          apply (subst sum.swap [where A = "{..q}"])
          apply (simp add: sum.cartesian_product eq sum.union_disjoint disjoint_iff_not_equal I II)
          done
      qed
      have *: "⟦a+b = w; c+d = -z⟧ ⟹ (a + c) + (b+d) = w-z" for a b w c d z :: "'c ⇒⇩0 int"
        by (auto simp: algebra_simps)
      have eq: "{..q} × {..Suc q} =
                Sigma {..q} (λi. {0..min (Suc q) i})
              ∪ Sigma {..q} (λi. {Suc i..Suc q})"
        by force
      show ?case
        apply (subst pr_def)
        apply (simp add: chain_boundary_sum chain_boundary_cmul)
        apply (subst chain_boundary_def)
        apply simp
        apply (simp add: frag_cmul_sum sum.cartesian_product eq sum.union_disjoint disjoint_iff_not_equal
          sum.atLeast_Suc_atMost_Suc_shift del: sum.cl_ivl_Suc min.absorb2 min.absorb4
          flip: comm_monoid_add_class.sum.Sigma)
        apply (simp add: sum.Sigma eq2 [of _ "λi. {_ i.._ i}"]
          del: min.absorb2 min.absorb4)
        apply (simp add: sum.union_disjoint disjoint_iff_not_equal * [OF 1 2])
        done
    next
      case (diff a b)
      then show ?case
        by (simp add: chain_boundary_diff frag_extend_diff chain_map_diff)
    qed auto
  qed
  have *: "singular_chain p (subtopology U V) (prism (p - Suc 0) (chain_boundary p c))"
    if "singular_chain p S c" "singular_chain (p - Suc 0) (subtopology S T) (chain_boundary p c)"
  proof (cases "p")
    case 0 then show ?thesis by (simp add: chain_boundary_def prism)
  next
    case (Suc p')
    with prism that show ?thesis by auto
  qed
  then show ?thesis
    using c
    unfolding singular_relcycle_def homologous_rel_def singular_relboundary_def mod_subset_def
    apply (rule_tac x="- prism p c" in exI)
    by (simp add: chain_boundary_minus prism(2) prism(4) singular_chain_minus)
qed

end