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)  (ip. 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. (ip. 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::natreal. λ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: "(ip. 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 "(ip. 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 "(ip. if i < p then x i else if i = k then 0 else x (i -1)) = (ip. 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 (iI. 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. (kp. 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 (kp. 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 *: "(xp. ip - 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 (λxstandard_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 = (λxstandard_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 (λxstandard_simplex (p -1). a)"
    have "(kp. frag_cmul ((-1) ^ k) (frag_of (singular_face p k f)))
        = (kp. 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 "(kp. frag_cmul ((-1) ^ k) (frag_of (singular_face p k f)))
                = (if odd p then 0 else frag_of (λxstandard_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 (λxstandard_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  (λxstandard_simplex p. λi. (jp. 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. jp. 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. jp. 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 "(jp. l j k * ?fi j) = (jp. 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 "(jp. l j i * simplical_face k x j)
      = (jp - 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))"
    using feq p singular_face_oriented_simplex by auto
  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. xv. y. (λl. oriented_simplex (Suc x)
                            (λi. if i = 0 then xv else l (i - 1))) =
                  y  oriented_simplex x"
    by (simp add: oriented_simplex_eq flip: choice_iff function_factors_left)
  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. jp. 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 + (jp. 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 "jp" 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 + (jp. l j i * x (Suc j))) = (λi. (1 - (1 - x 0)) * v i + (1 - x 0) * (inverse (1 - x 0) * (jp. 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. (jp. l j i * (x (Suc j) * inverse (1 - x 0))))  S"
        proof (rule S)
          have "x 0 + (jp. x (Suc j)) = sum x {..Suc p}"
            by (metis sum.atMost_Suc_shift)
          with x1 have "(jp. x (Suc j)) = 1 - x 0"
            by simp
          with False show "(jp. 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) * (jp. 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 (λustandard_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)) = (λustandard_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 (λustandard_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 (λustandard_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 (λustandard_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. jp. l j i * x j) i = (jp. g (l j) i * x j)"
    if "x  standard_simplex p" for x i
  proof -
    have ssr: "(λi. jp. 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 "jp" for j
    proof -
      have q: "(λx i. jp. 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. jp. l j i * x j) ` standard_simplex p"
      proof
        show "l j = (λi. jp. l j i * ?x j)"
          using jp 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. jp. l j i * x j) i = (jr. np. m j i * (l n j * x n))"
      by (simp add: geq oriented_simplex_def sum_distrib_left ssr)
    also have "... =  (jp. nr. m n i * (l j n * x j))"
      by (rule sum.swap)
    also have "... = (jp. 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. (jSuc 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. (jp. 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. (jSuc 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) * ((jSuc 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. jSuc 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. jSuc p. l j i * ((1 - u) * inverse (2 + real p) + u * x j))
                   = (λi. (1 - u) * (jSuc p. l j i) / (real p + 2) + u * (jSuc p. l j i * x j))"
      proof
        fix i
        have "(jSuc p. l j i * ((1 - u) * inverse (2 + real p) + u * x j))
            = (jSuc 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) * (jSuc p. l j i) / (real p + 2) + u * (jSuc 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::