Quelle Simplices.thy Sprache: Isabelle

section\<open>Homology, I: Simplices\<close>

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

subsection\<open>Standard simplices, all of which are topological subspaces of @{text"R^n"}.      \<close>

type_synonym 'a chain = "((nat \ real) \ 'a) \\<^sub>0 int"

definition standard_simplex :: "nat \ (nat \ real) set" where
  "standard_simplex p \
    {x. (\<forall>i. 0 \<le> x i \<and> x i \<le> 1) \<and> (\<forall>i>p. x i = 0) \<and> (\<Sum>i\<le>p. x i) = 1}"

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 =
              (\<Inter>i. {x. x \<in> topspace ?X \<and> x i \<in> {0..1}}) \<inter>
              (\<Inter>i \<in> {p<..}. {x \<in> topspace ?X. x i \<in> {0}}) \<inter>
              {x \<in> topspace ?X. (\<Sum>i\<le>p. x i) \<in> {1}}"
    by (auto simp: standard_simplex_def topspace_product_topology)
  show ?thesis
    unfolding eq
    by (rule closedin_Int closedin_Inter continuous_map_sum
             continuous_map_product_projection closedin_continuous_map_preimage | force | clarify)+
qed

lemma standard_simplex_01: "standard_simplex p \ UNIV \\<^sub>E {0..1}"
  using standard_simplex_def by auto

lemma compactin_standard_simplex:
   "compactin (powertop_real UNIV) (standard_simplex p)"
proof (rule closed_compactin)
  show "compactin (powertop_real UNIV) (UNIV \\<^sub>E {0..1})"
    by (simp add: compactin_PiE)
  show "standard_simplex p \ UNIV \\<^sub>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 \<le> u; u \<le> 1\<rbrakk>
    \<Longrightarrow> (\<lambda>i. (1 - u) * x i + u * y i) \<in> 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\<open>Face map\<close>

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 {..
    using \<open>k \<le> p\<close> 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))
         = (\<Sum>i < k. x i) + (\<Sum>i \<in> {k..p}. if i = k then 0 else x (i -1))"
    by (simp add: gg)
  consider "k \ p - Suc 0" | "k = p"
    using \<open>k \<le> p\<close> 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 \<open>1 \<le> p\<close> 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\<open>Singular simplices, forcing canonicity outside the intended domain\<close>

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
    \<and> f \<in> 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 \<and> f ` (standard_simplex p) \<subseteq> S"
  by (auto simp: singular_simplex_def continuous_map_in_subtopology)

subsubsection\<open>Singular face\<close>

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
                              (\<lambda>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\<open>Singular chains\<close>

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\
        \<Longrightarrow> 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 \<and> (\<forall>f \<in> Poly_Mapping.keys c. f ` (standard_simplex p) \<subseteq> 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))
        \<Longrightarrow> singular_chain p X (frag_extend f x)"
  by (simp add: frag_extend_def singular_chain_cmul singular_chain_sum)

subsection\<open>Boundary homomorphism for singular chains\<close>

definition chain_boundary :: "nat \ ('a chain) \ 'a chain"
  where "chain_boundary p c \
          (if p = 0 then 0 else
           frag_extend (\<lambda>f. (\<Sum>k\<le>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\
       \<Longrightarrow> 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 (\<Sum>k\<le>p. frag_cmul ((-1) ^ k) (frag_of(singular_face p k f))))"
  by (simp add: chain_boundary_def)

subsection\<open>Factoring out chains in a subtopology for relative homology\<close>

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\<open>Relative cycles $Z_pX (S)$ where $X$ is a topology and $S$ a subset \<close>

definition singular_relcycle :: "nat \ 'a topology \ 'a set \ ('a chain) \ bool"
  where "singular_relcycle \
        \<lambda>p X S c. singular_chain p X c \<and> (chain_boundary p c, 0) \<in> 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 \
    \<lambda>p X S c. singular_chain p X c \<and> 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\
        \<Longrightarrow> 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)\
        \<Longrightarrow> 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\
        \<Longrightarrow> 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\
        \<Longrightarrow> singular_relcycle p (subtopology X S) {} c"
  by (auto simp: singular_cycle elim: singular_chain_mono)

subsection\<open>Relative boundaries $B_p X S$, where $X$ is a topology and $S$ a subset.\<close>

definition singular_relboundary :: "nat \ 'a topology \ 'a set \ ('a chain) \ bool"
  where
  "singular_relboundary p X S \
    \<lambda>c. \<exists>d. singular_chain (Suc p) X d \<and> (chain_boundary (Suc p) d, c) \<in> (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 \
    (\<exists>d e. singular_chain (Suc p) X d \<and> singular_chain p (subtopology X S) e \<and>
           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 \
    (\<exists>d e. singular_chain (Suc p) X d \<and> singular_chain p (subtopology X S) e \<and>
              (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 \
    (\<exists>d. singular_chain (Suc p) X d \<and> 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\
        \<Longrightarrow> 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\<open>The (relative) homology relation\<close>

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'\
        \<Longrightarrow> 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
             \<Longrightarrow> (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\<open>Show that all boundaries are cycles, the key "chain complex" property.\<close>

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 \<le> j" "j \<le> 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 \<open>singular_chain p (subtopology X S) e\<close> 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\<open>Operations induced by a continuous map g between topological spaces\<close>

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\
        \<Longrightarrow> 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;
     \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk>
    \<Longrightarrow> 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;
     \<And>x. x \<in> topspace X \<Longrightarrow> f x = x\<rbrakk>
    \<Longrightarrow> 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\
        \<Longrightarrow> singular_face p k (simplex_map p f c) = simplex_map (p - Suc 0) f (c \<circ> simplical_face k)"
  unfolding simplex_map_def singular_face_def
  by (force simp: simplical_face_in_standard_simplex)

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

definition chain_map :: "nat \ ('b \ 'a) \ (((nat \ real) \ 'b) \\<^sub>0 int) \ 'a chain"
  where "chain_map p g c \ frag_extend (frag_of \ simplex_map p g) c"

lemma singular_chain_chain_map:
   "\singular_chain p X c; continuous_map X X' g\ \ singular_chain p X' (chain_map p g c)"
  unfolding chain_map_def
  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\
    \<Longrightarrow> 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\
    \<Longrightarrow>  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
    by (metis Pi_anti_mono continuous_map_from_subtopology continuous_map_in_subtopology
        openin_imp_subset openin_topspace subsetD)
  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 "\Y. g \ topspace (subtopology Y S) \ T"
      using assms(3) by auto
    then show ?thesis
      by (metis assms(2) continuous_map_from_subtopology continuous_map_into_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\<open>Homology of one-point spaces degenerates except for $p = 0$.\<close>

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 \<open>singular_simplex p X f\<close> 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 \
         (\<exists>b. c = frag_cmul b (frag_of(restrict (\<lambda>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 \<or> odd p then 0
          else frag_extend (\<lambda>f. frag_of(restrict (\<lambda>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)))
        = (\<Sum>k\<le>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 (\<lambda>x\<in>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 \<open>odd p\<close>)
    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\<open>Simplicial chains\<close>

text\<open>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.\<close>

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 \<and>
        (\<exists>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) (\<lambda>x i. \<Sum>j\<le>p. l j i * x j)" for l :: " nat \<Rightarrow> 'a \<Rightarrow> 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)
    \<longleftrightarrow> ((\<lambda>x i. \<Sum>j\<le>p. l j i * x j) ` standard_simplex p \<subseteq> S)"
  by (auto simp: simplicial_simplex oriented_simplex_def)

lemma simplicial_imp_singular_simplex:
   "simplicial_simplex p S f
      \<Longrightarrow> 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
      \<Longrightarrow> 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 \<open>i \<le> p\<close>
      by (simp add: fun_eq_iff oriented_simplex_def split: if_split_asm)
    with \<open>i \<le> p\<close> 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) (\<lambda>j. if j < k then l j else l (Suc j))"
proof -
  have "(\j\p. l j i * simplical_face k x j)
      = (\<Sum>j\<le>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))"
    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\<open>The cone construction on simplicial simplices.\<close>

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) (\<lambda>i. if i = 0 then v else l(i -1))"
proof -
  have *: "\x. \xv. \y. (\l. oriented_simplex (Suc x)
                            (\<lambda>i. if i = 0 then xv else l (i - 1))) =
                  y \<circ> 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\
                 \<Longrightarrow> (\<lambda>i. \<Sum>j\<le>p. l j i * x j) \<in> 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] \<open>a \<in> S\<close> 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 \<open>x 0 < 1\<close> in \<open>auto simp: field_split_simps\<close>)
      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 (\<lambda>u\<in>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 (\<lambda>u\<in>standard_simplex 0. v)"
    by (simp add: assms simplicial_cone_def chain_boundary_of \<open>p = 0\<close> 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
              (\<lambda>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 \<le> p" for x
    using \<open>0 < p\<close> 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)
                     (\<Sum>k = 0..p. frag_cmul ((-1) ^ k) (frag_of (singular_face p k (oriented_simplex p l))))
         = - (\<Sum>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 \<open>p > 0\<close>
    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 (\<lambda>u\<in>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
   \<Longrightarrow> chain_boundary (Suc p) (simplicial_cone p v c) =
       c - (if p = 0 then frag_extend (\<lambda>f. frag_of (\<lambda>u\<in>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 \<open>q \<le> r\<close>]
      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 \<open>j\<le>p\<close> 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 \<open>q \<le> r\<close>] 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 \<open>simplicial_simplex p (standard_simplex q) f\<close> feq by blast
    then have 1: "simplicial_simplex (Suc p) (standard_simplex q)
                      (oriented_simplex (Suc p) (\<lambda>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 \<open>q \<le> r\<close>]
            simplex_map_oriented_simplex [of p q m r S g, OF 0 g \<open>q \<le> r\<close>]
      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\<open>Barycentric subdivision of a linear ("simplicial") simplex's image\<close>

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
      (\<lambda>f. simplicial_cone p
            (\<lambda>i. (\<Sum>j\<le>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)
               (\<lambda>i. (\<Sum>j\<le>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
           \<Longrightarrow> 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"
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Dauer der Verarbeitung: 0.26 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.