Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
Simplices.thy
Sprache: Unknown
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 p X S \
\<lambda>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 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"
by (simp add: 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, hide_lams) 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 (simp add: singular_relboundary_def)
lemma singular_boundary_imp_chain:
"singular_relboundary p X {} c \ singular_chain p X c"
by (auto simp: singular_relboundary singular_chain_boundary_alt singular_chain_empty topspace_subtopology)
lemma singular_boundary_mono:
"\T \ S; singular_relboundary p (subtopology X T) {} c\
\<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)
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
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\<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)
then show ?thesis
by (metis (no_types) L extensional_restrict restrict_ext singular_simplex_def)
qed
next
assume ?rhs
with assms show ?lhs
by (auto simp: singular_simplex_def topspace_subtopology)
qed
lemma singular_chain_singleton:
assumes "topspace X = {a}"
shows "singular_chain p X c \
(\<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))"
unfolding feq singular_face_def oriented_simplex_def
apply (simp add: simplical_face_in_standard_simplex [OF p] restrict_compose_left subset_eq)
using sum.zero_middle [OF p, where 'a=real, symmetric] unfolding simplical_face_def o_def
apply (simp add: if_distrib [of "\x. _ * x"] if_distrib [of "\f. f _ * _"] atLeast0AtMost cong: if_cong)
done
ultimately
show ?thesis
using p simplicial_simplex_def singular_simplex_singular_face by blast
qed
lemma simplicial_chain_boundary:
"simplicial_chain p S c \ simplicial_chain (p -1) S (chain_boundary p c)"
unfolding simplicial_chain_def
proof (induction rule: frag_induction)
case (one f)
then have "simplicial_simplex p S f"
by simp
have "simplicial_chain (p - Suc 0) S (frag_of (singular_face p i f))"
if "0 < p" "i \ p" for i
using that one
by (force simp: simplicial_simplex_def singular_simplex_singular_face singular_face_oriented_simplex)
then have "simplicial_chain (p - Suc 0) S (chain_boundary p (frag_of f))"
unfolding chain_boundary_def frag_extend_of
by (auto intro!: simplicial_chain_cmul simplicial_chain_sum)
then show ?case
by (simp add: simplicial_chain_def [symmetric])
next
case (diff a b)
then show ?case
by (metis chain_boundary_diff simplicial_chain_def simplicial_chain_diff)
qed auto
subsection\<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. \y. \v. (\l. oriented_simplex (Suc x) (\i. if i = 0 then v else l (i -1)))
= (y v \<circ> (oriented_simplex x))"
apply (subst choice_iff [symmetric])
by (simp add: oriented_simplex_eq choice_iff [symmetric] function_factors_left [symmetric])
then show ?thesis
unfolding o_def by (metis(no_types))
qed
lemma simplicial_simplex_simplex_cone:
assumes f: "simplicial_simplex p S f"
and T: "\x u. \0 \ u; u \ 1; x \ S\ \ (\i. (1 - u) * v i + u * x i) \ T"
shows "simplicial_simplex (Suc p) T (simplex_cone p v f)"
proof -
obtain l where l: "\x. x \ standard_simplex p \ oriented_simplex p l x \ S"
and feq: "f = oriented_simplex p l"
using f by (auto simp: simplicial_simplex)
have "oriented_simplex p l x \ S" if "x \ standard_simplex p" for x
using f that by (auto simp: simplicial_simplex feq)
then have S: "\x. \\i. 0 \ x i \ x i \ 1; \i. i>p \ x i = 0; sum x {..p} = 1\
\<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"
--> --------------------
--> maximum size reached
--> --------------------
[ Dauer der Verarbeitung: 0.250 Sekunden
(vorverarbeitet)
]
|
|
