|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
bisection_nat_sqrt.prf
Sprache: Isabelle
|
|
section\<open>Homology, II: Homology Groups\<close>
theory Homology_Groups
imports Simplices "HOL-Algebra.Exact_Sequence"
begin
subsection\<open>Homology Groups\<close>
text\<open>Now actually connect to group theory and set up homology groups. Note that we define homomogy
groups for all \emph{integers} @{term p}, since this seems to avoid some special-case reasoning,
though they are trivial for @{term"p < 0"}.\<close>
definition chain_group :: "nat \ 'a topology \ 'a chain monoid"
where "chain_group p X \ free_Abelian_group (singular_simplex_set p X)"
lemma carrier_chain_group [simp]: "carrier(chain_group p X) = singular_chain_set p X"
by (auto simp: chain_group_def singular_chain_def free_Abelian_group_def)
lemma one_chain_group [simp]: "one(chain_group p X) = 0"
by (auto simp: chain_group_def free_Abelian_group_def)
lemma mult_chain_group [simp]: "monoid.mult(chain_group p X) = (+)"
by (auto simp: chain_group_def free_Abelian_group_def)
lemma m_inv_chain_group [simp]: "Poly_Mapping.keys a \ singular_simplex_set p X \ inv\<^bsub>chain_group p X\<^esub> a = -a"
unfolding chain_group_def by simp
lemma group_chain_group [simp]: "Group.group (chain_group p X)"
by (simp add: chain_group_def)
lemma abelian_chain_group: "comm_group(chain_group p X)"
by (simp add: free_Abelian_group_def group.group_comm_groupI [OF group_chain_group])
lemma subgroup_singular_relcycle:
"subgroup (singular_relcycle_set p X S) (chain_group p X)"
proof
show "x \\<^bsub>chain_group p X\<^esub> y \ singular_relcycle_set p X S"
if "x \ singular_relcycle_set p X S" and "y \ singular_relcycle_set p X S" for x y
using that by (simp add: singular_relcycle_add)
next
show "inv\<^bsub>chain_group p X\<^esub> x \ singular_relcycle_set p X S"
if "x \ singular_relcycle_set p X S" for x
using that
by clarsimp (metis m_inv_chain_group singular_chain_def singular_relcycle singular_relcycle_minus)
qed (auto simp: singular_relcycle)
definition relcycle_group :: "nat \ 'a topology \ 'a set \ ('a chain) monoid"
where "relcycle_group p X S \
subgroup_generated (chain_group p X) (Collect(singular_relcycle p X S))"
lemma carrier_relcycle_group [simp]:
"carrier (relcycle_group p X S) = singular_relcycle_set p X S"
proof -
have "carrier (chain_group p X) \ singular_relcycle_set p X S = singular_relcycle_set p X S"
using subgroup.subset subgroup_singular_relcycle by blast
moreover have "generate (chain_group p X) (singular_relcycle_set p X S) \ singular_relcycle_set p X S"
by (simp add: group.generate_subgroup_incl group_chain_group subgroup_singular_relcycle)
ultimately show ?thesis
by (auto simp: relcycle_group_def subgroup_generated_def generate.incl)
qed
lemma one_relcycle_group [simp]: "one(relcycle_group p X S) = 0"
by (simp add: relcycle_group_def)
lemma mult_relcycle_group [simp]: "(\\<^bsub>relcycle_group p X S\<^esub>) = (+)"
by (simp add: relcycle_group_def)
lemma abelian_relcycle_group [simp]:
"comm_group(relcycle_group p X S)"
unfolding relcycle_group_def
by (intro group.abelian_subgroup_generated group_chain_group) (auto simp: abelian_chain_group singular_relcycle)
lemma group_relcycle_group [simp]: "group(relcycle_group p X S)"
by (simp add: comm_group.axioms(2))
lemma relcycle_group_restrict [simp]:
"relcycle_group p X (topspace X \ S) = relcycle_group p X S"
by (metis relcycle_group_def singular_relcycle_restrict)
definition relative_homology_group :: "int \ 'a topology \ 'a set \ ('a chain) set monoid"
where
"relative_homology_group p X S \
if p < 0 then singleton_group undefined else
(relcycle_group (nat p) X S) Mod (singular_relboundary_set (nat p) X S)"
abbreviation homology_group
where "homology_group p X \ relative_homology_group p X {}"
lemma relative_homology_group_restrict [simp]:
"relative_homology_group p X (topspace X \ S) = relative_homology_group p X S"
by (simp add: relative_homology_group_def)
lemma nontrivial_relative_homology_group:
fixes p::nat
shows "relative_homology_group p X S
= relcycle_group p X S Mod singular_relboundary_set p X S"
by (simp add: relative_homology_group_def)
lemma singular_relboundary_ss:
"singular_relboundary p X S x \ Poly_Mapping.keys x \ singular_simplex_set p X"
using singular_chain_def singular_relboundary_imp_chain by blast
lemma trivial_relative_homology_group [simp]:
"p < 0 \ trivial_group(relative_homology_group p X S)"
by (simp add: relative_homology_group_def)
lemma subgroup_singular_relboundary:
"subgroup (singular_relboundary_set p X S) (chain_group p X)"
unfolding chain_group_def
proof unfold_locales
show "singular_relboundary_set p X S
\<subseteq> carrier (free_Abelian_group (singular_simplex_set p X))"
using singular_chain_def singular_relboundary_imp_chain by fastforce
next
fix x
assume "x \ singular_relboundary_set p X S"
then show "inv\<^bsub>free_Abelian_group (singular_simplex_set p X)\<^esub> x
\<in> singular_relboundary_set p X S"
by (simp add: singular_relboundary_ss singular_relboundary_minus)
qed (auto simp: free_Abelian_group_def singular_relboundary_add)
lemma subgroup_singular_relboundary_relcycle:
"subgroup (singular_relboundary_set p X S) (relcycle_group p X S)"
unfolding relcycle_group_def
apply (rule group.subgroup_of_subgroup_generated)
by (auto simp: singular_relcycle subgroup_singular_relboundary intro: singular_relboundary_imp_relcycle)
lemma normal_subgroup_singular_relboundary_relcycle:
"(singular_relboundary_set p X S) \ (relcycle_group p X S)"
by (simp add: comm_group.normal_iff_subgroup subgroup_singular_relboundary_relcycle)
lemma group_relative_homology_group [simp]:
"group (relative_homology_group p X S)"
by (simp add: relative_homology_group_def normal.factorgroup_is_group
normal_subgroup_singular_relboundary_relcycle)
lemma right_coset_singular_relboundary:
"r_coset (relcycle_group p X S) (singular_relboundary_set p X S)
= (\<lambda>a. {b. homologous_rel p X S a b})"
using singular_relboundary_minus
by (force simp: r_coset_def homologous_rel_def relcycle_group_def subgroup_generated_def)
lemma carrier_relative_homology_group:
"carrier(relative_homology_group (int p) X S)
= (homologous_rel_set p X S) ` singular_relcycle_set p X S"
by (auto simp: set_eq_iff image_iff relative_homology_group_def FactGroup_def RCOSETS_def right_coset_singular_relboundary)
lemma carrier_relative_homology_group_0:
"carrier(relative_homology_group 0 X S)
= (homologous_rel_set 0 X S) ` singular_relcycle_set 0 X S"
using carrier_relative_homology_group [of 0 X S] by simp
lemma one_relative_homology_group [simp]:
"one(relative_homology_group (int p) X S) = singular_relboundary_set p X S"
by (simp add: relative_homology_group_def FactGroup_def)
lemma mult_relative_homology_group:
"(\\<^bsub>relative_homology_group (int p) X S\<^esub>) = (\R S. (\r\R. \s\S. {r + s}))"
unfolding relcycle_group_def subgroup_generated_def chain_group_def free_Abelian_group_def set_mult_def relative_homology_group_def FactGroup_def
by force
lemma inv_relative_homology_group:
assumes "R \ carrier (relative_homology_group (int p) X S)"
shows "m_inv(relative_homology_group (int p) X S) R = uminus ` R"
proof (rule group.inv_equality [OF group_relative_homology_group _ assms])
obtain c where c: "R = homologous_rel_set p X S c" "singular_relcycle p X S c"
using assms by (auto simp: carrier_relative_homology_group)
have "singular_relboundary p X S (b - a)"
if "a \ R" and "b \ R" for a b
using c that
by clarify (metis homologous_rel_def homologous_rel_eq)
moreover
have "x \ (\x\R. \y\R. {y - x})"
if "singular_relboundary p X S x" for x
using c
by simp (metis diff_eq_eq homologous_rel_def homologous_rel_refl homologous_rel_sym that)
ultimately
have "(\x\R. \xa\R. {xa - x}) = singular_relboundary_set p X S"
by auto
then show "uminus ` R \\<^bsub>relative_homology_group (int p) X S\<^esub> R =
\<one>\<^bsub>relative_homology_group (int p) X S\<^esub>"
by (auto simp: carrier_relative_homology_group mult_relative_homology_group)
have "singular_relcycle p X S (-c)"
using c by (simp add: singular_relcycle_minus)
moreover have "homologous_rel p X S c x \ homologous_rel p X S (-c) (- x)" for x
by (metis homologous_rel_def homologous_rel_sym minus_diff_eq minus_diff_minus)
moreover have "homologous_rel p X S (-c) x \ x \ uminus ` homologous_rel_set p X S c" for x
by (clarsimp simp: image_iff) (metis add.inverse_inverse diff_0 homologous_rel_diff homologous_rel_refl)
ultimately show "uminus ` R \ carrier (relative_homology_group (int p) X S)"
using c by (auto simp: carrier_relative_homology_group)
qed
lemma homologous_rel_eq_relboundary:
"homologous_rel p X S c = singular_relboundary p X S
\<longleftrightarrow> singular_relboundary p X S c" (is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
unfolding homologous_rel_def
by (metis diff_zero singular_relboundary_0)
next
assume R: ?rhs
show ?lhs
unfolding homologous_rel_def
using singular_relboundary_diff R by fastforce
qed
lemma homologous_rel_set_eq_relboundary:
"homologous_rel_set p X S c = singular_relboundary_set p X S \ singular_relboundary p X S c"
by (auto simp flip: homologous_rel_eq_relboundary)
text\<open>Lift the boundary and induced maps to homology groups. We totalize both
quite aggressively to the appropriate group identity in all "undefined"
situations, which makes several of the properties cleaner and simpler.\<close>
lemma homomorphism_chain_boundary:
"chain_boundary p \ hom (relcycle_group p X S) (relcycle_group(p - Suc 0) (subtopology X S) {})"
(is "?h \ hom ?G ?H")
proof (rule homI)
show "\x. x \ carrier ?G \ ?h x \ carrier ?H"
by (auto simp: singular_relcycle_def mod_subset_def chain_boundary_boundary)
qed (simp add: relcycle_group_def subgroup_generated_def chain_boundary_add)
lemma hom_boundary1:
"\d. \p X S.
d p X S \<in> hom (relative_homology_group (int p) X S)
(homology_group (int (p - Suc 0)) (subtopology X S))
\<and> (\<forall>c. singular_relcycle p X S c
\<longrightarrow> d p X S (homologous_rel_set p X S c)
= homologous_rel_set (p - Suc 0) (subtopology X S) {} (chain_boundary p c))"
(is "\d. \p X S. ?\ (d p X S) p X S")
proof ((subst choice_iff [symmetric])+, clarify)
fix p X and S :: "'a set"
define \<theta> where "\<theta> \<equiv> r_coset (relcycle_group(p - Suc 0) (subtopology X S) {})
(singular_relboundary_set (p - Suc 0) (subtopology X S) {}) \<circ> chain_boundary p"
define H where "H \ relative_homology_group (int (p - Suc 0)) (subtopology X S) {}"
define J where "J \ relcycle_group (p - Suc 0) (subtopology X S) {}"
have \<theta>: "\<theta> \<in> hom (relcycle_group p X S) H"
unfolding \<theta>_def
proof (rule hom_compose)
show "chain_boundary p \ hom (relcycle_group p X S) J"
by (simp add: J_def homomorphism_chain_boundary)
show "(#>\<^bsub>relcycle_group (p - Suc 0) (subtopology X S) {}\<^esub>)
(singular_relboundary_set (p - Suc 0) (subtopology X S) {}) \<in> hom J H"
by (simp add: H_def J_def nontrivial_relative_homology_group
normal.r_coset_hom_Mod normal_subgroup_singular_relboundary_relcycle)
qed
have *: "singular_relboundary (p - Suc 0) (subtopology X S) {} (chain_boundary p c)"
if "singular_relboundary p X S c" for c
proof (cases "p=0")
case True
then show ?thesis
by (metis chain_boundary_def singular_relboundary_0)
next
case False
with that have "\d. singular_chain p (subtopology X S) d \ chain_boundary p d = chain_boundary p c"
by (metis add.left_neutral chain_boundary_add chain_boundary_boundary_alt singular_relboundary)
with that False show ?thesis
by (auto simp: singular_boundary)
qed
have \<theta>_eq: "\<theta> x = \<theta> y"
if x: "x \ singular_relcycle_set p X S" and y: "y \ singular_relcycle_set p X S"
and eq: "singular_relboundary_set p X S #>\<^bsub>relcycle_group p X S\<^esub> x
= singular_relboundary_set p X S #>\<^bsub>relcycle_group p X S\<^esub> y" for x y
proof -
have "singular_relboundary p X S (x-y)"
by (metis eq homologous_rel_def homologous_rel_eq mem_Collect_eq right_coset_singular_relboundary)
with * have "(singular_relboundary (p - Suc 0) (subtopology X S) {}) (chain_boundary p (x-y))"
by blast
then show ?thesis
unfolding \<theta>_def comp_def
by (metis chain_boundary_diff homologous_rel_def homologous_rel_eq right_coset_singular_relboundary)
qed
obtain d
where "d \ hom ((relcycle_group p X S) Mod (singular_relboundary_set p X S)) H"
and d: "\u. u \ singular_relcycle_set p X S \ d (homologous_rel_set p X S u) = \ u"
by (metis FactGroup_universal [OF \<theta> normal_subgroup_singular_relboundary_relcycle \<theta>_eq] right_coset_singular_relboundary carrier_relcycle_group)
then have "d \ hom (relative_homology_group p X S) H"
by (simp add: nontrivial_relative_homology_group)
then show "\d. ?\ d p X S"
by (force simp: H_def right_coset_singular_relboundary d \<theta>_def)
qed
lemma hom_boundary2:
"\d. (\p X S.
(d p X S) \<in> hom (relative_homology_group p X S)
(homology_group (p - 1) (subtopology X S)))
\<and> (\<forall>p X S c. singular_relcycle p X S c \<and> Suc 0 \<le> p
\<longrightarrow> d p X S (homologous_rel_set p X S c)
= homologous_rel_set (p - Suc 0) (subtopology X S) {} (chain_boundary p c))"
(is "\d. ?\ d")
proof -
have *: "\f. \(\p. if p \ 0 then \q r t. undefined else f(nat p)) \ \f. \ f" for \
by blast
show ?thesis
apply (rule * [OF ex_forward [OF hom_boundary1]])
apply (simp add: not_le relative_homology_group_def nat_diff_distrib' int_eq_iff nat_diff_distrib flip: nat_1)
by (simp add: hom_def singleton_group_def)
qed
lemma hom_boundary3:
"\d. ((\p X S c. c \ carrier(relative_homology_group p X S)
\<longrightarrow> d p X S c = one(homology_group (p-1) (subtopology X S))) \<and>
(\<forall>p X S.
d p X S \<in> hom (relative_homology_group p X S)
(homology_group (p-1) (subtopology X S))) \<and>
(\<forall>p X S c.
singular_relcycle p X S c \<and> 1 \<le> p
\<longrightarrow> d p X S (homologous_rel_set p X S c)
= homologous_rel_set (p - Suc 0) (subtopology X S) {} (chain_boundary p c)) \<and>
(\<forall>p X S. d p X S = d p X (topspace X \<inter> S))) \<and>
(\<forall>p X S c. d p X S c \<in> carrier(homology_group (p-1) (subtopology X S))) \<and>
(\<forall>p. p \<le> 0 \<longrightarrow> d p = (\<lambda>q r t. undefined))"
(is "\x. ?P x \ ?Q x \ ?R x")
proof -
have "\x. ?Q x \ ?R x"
by (erule all_forward) (force simp: relative_homology_group_def)
moreover have "\x. ?P x \ ?Q x"
proof -
obtain d:: "[int, 'a topology, 'a set, ('a chain) set] \ ('a chain) set"
where 1: "\p X S. d p X S \ hom (relative_homology_group p X S)
(homology_group (p - 1) (subtopology X S))"
and 2: "\n X S c. singular_relcycle n X S c \ Suc 0 \ n
\<Longrightarrow> d n X S (homologous_rel_set n X S c)
= homologous_rel_set (n - Suc 0) (subtopology X S) {} (chain_boundary n c)"
using hom_boundary2 by blast
have 4: "c \ carrier (relative_homology_group p X S) \
d p X (topspace X \<inter> S) c \<in> carrier (relative_homology_group (p-1) (subtopology X S) {})"
for p X S c
using hom_carrier [OF 1 [of p X "topspace X \ S"]]
by (simp add: image_subset_iff subtopology_restrict)
show ?thesis
apply (rule_tac x="\p X S c.
if c \<in> carrier(relative_homology_group p X S)
then d p X (topspace X \<inter> S) c
else one(homology_group (p - 1) (subtopology X S))" in exI)
apply (simp add: Int_left_absorb subtopology_restrict carrier_relative_homology_group
group.is_monoid group.restrict_hom_iff 4 cong: if_cong)
apply (rule conjI)
apply (metis 1 relative_homology_group_restrict subtopology_restrict)
apply (metis 2 homologous_rel_restrict singular_relcycle_def subtopology_restrict)
done
qed
ultimately show ?thesis
by auto
qed
consts hom_boundary :: "[int,'a topology,'a set,'a chain set] \ 'a chain set"
specification (hom_boundary)
hom_boundary:
"((\p X S c. c \ carrier(relative_homology_group p X S)
\<longrightarrow> hom_boundary p X S c = one(homology_group (p-1) (subtopology X (S::'a set)))) \<and>
(\<forall>p X S.
hom_boundary p X S \<in> hom (relative_homology_group p X S)
(homology_group (p-1) (subtopology X (S::'a set)))) \
(\<forall>p X S c.
singular_relcycle p X S c \<and> 1 \<le> p
\<longrightarrow> hom_boundary p X S (homologous_rel_set p X S c)
= homologous_rel_set (p - Suc 0) (subtopology X (S::'a set)) {} (chain_boundary p c)) \
(\<forall>p X S. hom_boundary p X S = hom_boundary p X (topspace X \<inter> (S::'a set)))) \<and>
(\<forall>p X S c. hom_boundary p X S c \<in> carrier(homology_group (p-1) (subtopology X (S::'a set)))) \<and>
(\<forall>p. p \<le> 0 \<longrightarrow> hom_boundary p = (\<lambda>q r. \<lambda>t::'a chain set. undefined))"
by (fact hom_boundary3)
lemma hom_boundary_default:
"c \ carrier(relative_homology_group p X S)
\<Longrightarrow> hom_boundary p X S c = one(homology_group (p-1) (subtopology X S))"
and hom_boundary_hom: "hom_boundary p X S \ hom (relative_homology_group p X S) (homology_group (p-1) (subtopology X S))"
and hom_boundary_restrict [simp]: "hom_boundary p X (topspace X \ S) = hom_boundary p X S"
and hom_boundary_carrier: "hom_boundary p X S c \ carrier(homology_group (p-1) (subtopology X S))"
and hom_boundary_trivial: "p \ 0 \ hom_boundary p = (\q r t. undefined)"
by (metis hom_boundary)+
lemma hom_boundary_chain_boundary:
"\singular_relcycle p X S c; 1 \ p\
\<Longrightarrow> hom_boundary (int p) X S (homologous_rel_set p X S c) =
homologous_rel_set (p - Suc 0) (subtopology X S) {} (chain_boundary p c)"
by (metis hom_boundary)+
lemma hom_chain_map:
"\continuous_map X Y f; f ` S \ T\
\<Longrightarrow> (chain_map p f) \<in> hom (relcycle_group p X S) (relcycle_group p Y T)"
by (force simp: chain_map_add singular_relcycle_chain_map hom_def)
lemma hom_induced1:
"\hom_relmap.
(\<forall>p X S Y T f.
continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T
\<longrightarrow> (hom_relmap p X S Y T f) \<in> hom (relative_homology_group (int p) X S)
(relative_homology_group (int p) Y T)) \<and>
(\<forall>p X S Y T f c.
continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T \<and>
singular_relcycle p X S c
\<longrightarrow> hom_relmap p X S Y T f (homologous_rel_set p X S c) =
homologous_rel_set p Y T (chain_map p f c))"
proof -
have "\y. (y \ hom (relative_homology_group (int p) X S) (relative_homology_group (int p) Y T)) \
(\<forall>c. singular_relcycle p X S c \<longrightarrow>
y (homologous_rel_set p X S c) = homologous_rel_set p Y T (chain_map p f c))"
if contf: "continuous_map X Y f" and fim: "f ` (topspace X \ S) \ T"
for p X S Y T and f :: "'a \ 'b"
proof -
let ?f = "(#>\<^bsub>relcycle_group p Y T\<^esub>) (singular_relboundary_set p Y T) \ chain_map p f"
let ?F = "\x. singular_relboundary_set p X S #>\<^bsub>relcycle_group p X S\<^esub> x"
have 1: "?f \ hom (relcycle_group p X S) (relative_homology_group (int p) Y T)"
apply (rule hom_compose [where H = "relcycle_group p Y T"])
apply (metis contf fim hom_chain_map relcycle_group_restrict)
by (simp add: nontrivial_relative_homology_group normal.r_coset_hom_Mod normal_subgroup_singular_relboundary_relcycle)
have 2: "singular_relboundary_set p X S \ relcycle_group p X S"
using normal_subgroup_singular_relboundary_relcycle by blast
have 3: "?f x = ?f y"
if "singular_relcycle p X S x" "singular_relcycle p X S y" "?F x = ?F y" for x y
proof -
have "singular_relboundary p Y T (chain_map p f (x - y))"
apply (rule singular_relboundary_chain_map [OF _ contf fim])
by (metis homologous_rel_def homologous_rel_eq mem_Collect_eq right_coset_singular_relboundary singular_relboundary_restrict that(3))
then have "singular_relboundary p Y T (chain_map p f x - chain_map p f y)"
by (simp add: chain_map_diff)
with that
show ?thesis
apply (simp add: right_coset_singular_relboundary homologous_rel_set_eq)
apply (simp add: homologous_rel_def)
done
qed
obtain g where "g \ hom (relcycle_group p X S Mod singular_relboundary_set p X S)
(relative_homology_group (int p) Y T)"
"\x. x \ singular_relcycle_set p X S \ g (?F x) = ?f x"
using FactGroup_universal [OF 1 2 3, unfolded carrier_relcycle_group] by blast
then show ?thesis
by (force simp: right_coset_singular_relboundary nontrivial_relative_homology_group)
qed
then show ?thesis
apply (simp flip: all_conj_distrib)
apply ((subst choice_iff [symmetric])+)
apply metis
done
qed
lemma hom_induced2:
"\hom_relmap.
(\<forall>p X S Y T f.
continuous_map X Y f \<and>
f ` (topspace X \<inter> S) \<subseteq> T
\<longrightarrow> (hom_relmap p X S Y T f) \<in> hom (relative_homology_group p X S)
(relative_homology_group p Y T)) \<and>
(\<forall>p X S Y T f c.
continuous_map X Y f \<and>
f ` (topspace X \<inter> S) \<subseteq> T \<and>
singular_relcycle p X S c
\<longrightarrow> hom_relmap p X S Y T f (homologous_rel_set p X S c) =
homologous_rel_set p Y T (chain_map p f c)) \<and>
(\<forall>p. p < 0 \<longrightarrow> hom_relmap p = (\<lambda>X S Y T f c. undefined))"
(is "\d. ?\ d")
proof -
have *: "\f. \(\p. if p < 0 then \X S Y T f c. undefined else f(nat p)) \ \f. \ f" for \
by blast
show ?thesis
apply (rule * [OF ex_forward [OF hom_induced1]])
apply (simp add: not_le relative_homology_group_def nat_diff_distrib' int_eq_iff nat_diff_distrib flip: nat_1)
done
qed
lemma hom_induced3:
"\hom_relmap.
((\<forall>p X S Y T f c.
~(continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T \<and>
c \<in> carrier(relative_homology_group p X S))
\<longrightarrow> hom_relmap p X S Y T f c = one(relative_homology_group p Y T)) \<and>
(\<forall>p X S Y T f.
hom_relmap p X S Y T f \<in> hom (relative_homology_group p X S) (relative_homology_group p Y T)) \<and>
(\<forall>p X S Y T f c.
continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T \<and> singular_relcycle p X S c
\<longrightarrow> hom_relmap p X S Y T f (homologous_rel_set p X S c) =
homologous_rel_set p Y T (chain_map p f c)) \<and>
(\<forall>p X S Y T.
hom_relmap p X S Y T =
hom_relmap p X (topspace X \<inter> S) Y (topspace Y \<inter> T))) \<and>
(\<forall>p X S Y f T c.
hom_relmap p X S Y T f c \<in> carrier(relative_homology_group p Y T)) \<and>
(\<forall>p. p < 0 \<longrightarrow> hom_relmap p = (\<lambda>X S Y T f c. undefined))"
(is "\x. ?P x \ ?Q x \ ?R x")
proof -
have "\x. ?Q x \ ?R x"
by (erule all_forward) (fastforce simp: relative_homology_group_def)
moreover have "\x. ?P x \ ?Q x"
proof -
obtain hom_relmap:: "[int,'a topology,'a set,'b topology,'b set,'a \ 'b,('a chain) set] \ ('b chain) set"
where 1: "\p X S Y T f. \continuous_map X Y f; f ` (topspace X \ S) \ T\ \
hom_relmap p X S Y T f
\<in> hom (relative_homology_group p X S) (relative_homology_group p Y T)"
and 2: "\p X S Y T f c.
\<lbrakk>continuous_map X Y f; f ` (topspace X \<inter> S) \<subseteq> T; singular_relcycle p X S c\<rbrakk>
\<Longrightarrow>
hom_relmap (int p) X S Y T f (homologous_rel_set p X S c) =
homologous_rel_set p Y T (chain_map p f c)"
and 3: "(\p. p < 0 \ hom_relmap p = (\X S Y T f c. undefined))"
using hom_induced2 [where ?'a='a and ?'b='b]
apply clarify
apply (rule_tac hom_relmap=hom_relmap in that, auto)
done
have 4: "\continuous_map X Y f; f ` (topspace X \ S) \ T; c \ carrier (relative_homology_group p X S)\ \
hom_relmap p X (topspace X \<inter> S) Y (topspace Y \<inter> T) f c
\<in> carrier (relative_homology_group p Y T)"
for p X S Y f T c
using hom_carrier [OF 1 [of X Y f "topspace X \ S" "topspace Y \ T" p]]
by (simp add: image_subset_iff subtopology_restrict continuous_map_def)
have inhom: "(\c. if continuous_map X Y f \ f ` (topspace X \ S) \ T \
c \<in> carrier (relative_homology_group p X S)
then hom_relmap p X (topspace X \<inter> S) Y (topspace Y \<inter> T) f c
else \<one>\<^bsub>relative_homology_group p Y T\<^esub>)
\<in> hom (relative_homology_group p X S) (relative_homology_group p Y T)" (is "?h \<in> hom ?GX ?GY")
for p X S Y T f
proof (rule homI)
show "\x. x \ carrier ?GX \ ?h x \ carrier ?GY"
by (auto simp: 4 group.is_monoid)
show "?h (x \\<^bsub>?GX\<^esub> y) = ?h x \\<^bsub>?GY\<^esub>?h y" if "x \ carrier ?GX" "y \ carrier ?GX" for x y
proof (cases "p < 0")
case True
with that show ?thesis
by (simp add: relative_homology_group_def singleton_group_def 3)
next
case False
show ?thesis
proof (cases "continuous_map X Y f")
case True
then have "f ` (topspace X \ S) \ topspace Y"
by (meson IntE continuous_map_def image_subsetI)
then show ?thesis
using True False that
using 1 [of X Y f "topspace X \ S" "topspace Y \ T" p]
by (simp add: 4 continuous_map_image_subset_topspace hom_mult not_less group.is_monoid monoid.m_closed Int_left_absorb)
qed (simp add: group.is_monoid)
qed
qed
have hrel: "\continuous_map X Y f; f ` (topspace X \ S) \ T; singular_relcycle p X S c\
\<Longrightarrow> hom_relmap (int p) X (topspace X \<inter> S) Y (topspace Y \<inter> T)
f (homologous_rel_set p X S c) = homologous_rel_set p Y T (chain_map p f c)"
for p X S Y T f c
using 2 [of X Y f "topspace X \ S" "topspace Y \ T" p c]
by simp (meson IntE continuous_map_def image_subsetI)
show ?thesis
apply (rule_tac x="\p X S Y T f c.
if continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T \<and>
c \<in> carrier(relative_homology_group p X S)
then hom_relmap p X (topspace X \<inter> S) Y (topspace Y \<inter> T) f c
else one(relative_homology_group p Y T)" in exI)
apply (simp add: Int_left_absorb subtopology_restrict carrier_relative_homology_group
group.is_monoid group.restrict_hom_iff 4 inhom hrel cong: if_cong)
apply (force simp: continuous_map_def intro!: ext)
done
qed
ultimately show ?thesis
by auto
qed
consts hom_induced:: "[int,'a topology,'a set,'b topology,'b set,'a \ 'b,('a chain) set] \ ('b chain) set"
specification (hom_induced)
hom_induced:
"((\p X S Y T f c.
~(continuous_map X Y f \<and>
f ` (topspace X \<inter> S) \<subseteq> T \<and>
c \<in> carrier(relative_homology_group p X S))
\<longrightarrow> hom_induced p X (S::'a set) Y (T::'b set) f c =
one(relative_homology_group p Y T)) \<and>
(\<forall>p X S Y T f.
(hom_induced p X (S::'a set) Y (T::'b set) f) \<in> hom (relative_homology_group p X S)
(relative_homology_group p Y T)) \<and>
(\<forall>p X S Y T f c.
continuous_map X Y f \<and>
f ` (topspace X \<inter> S) \<subseteq> T \<and>
singular_relcycle p X S c
\<longrightarrow> hom_induced p X (S::'a set) Y (T::'b set) f (homologous_rel_set p X S c) =
homologous_rel_set p Y T (chain_map p f c)) \<and>
(\<forall>p X S Y T.
hom_induced p X (S::'a set) Y (T::'b set) =
hom_induced p X (topspace X \<inter> S) Y (topspace Y \<inter> T))) \<and>
(\<forall>p X S Y f T c.
hom_induced p X (S::'a set) Y (T::'b set) f c \<in>
carrier(relative_homology_group p Y T)) \<and>
(\<forall>p. p < 0 \<longrightarrow> hom_induced p = (\<lambda>X S Y T. \<lambda>f::'a\<Rightarrow>'b. \<lambda>c. undefined))"
by (fact hom_induced3)
lemma hom_induced_default:
"~(continuous_map X Y f \ f ` (topspace X \ S) \ T \ c \ carrier(relative_homology_group p X S))
\<Longrightarrow> hom_induced p X S Y T f c = one(relative_homology_group p Y T)"
and hom_induced_hom:
"hom_induced p X S Y T f \ hom (relative_homology_group p X S) (relative_homology_group p Y T)"
and hom_induced_restrict [simp]:
"hom_induced p X (topspace X \ S) Y (topspace Y \ T) = hom_induced p X S Y T"
and hom_induced_carrier:
"hom_induced p X S Y T f c \ carrier(relative_homology_group p Y T)"
and hom_induced_trivial: "p < 0 \ hom_induced p = (\X S Y T f c. undefined)"
by (metis hom_induced)+
lemma hom_induced_chain_map_gen:
"\continuous_map X Y f; f ` (topspace X \ S) \ T; singular_relcycle p X S c\
\<Longrightarrow> hom_induced p X S Y T f (homologous_rel_set p X S c) = homologous_rel_set p Y T (chain_map p f c)"
by (metis hom_induced)
lemma hom_induced_chain_map:
"\continuous_map X Y f; f ` S \ T; singular_relcycle p X S c\
\<Longrightarrow> hom_induced p X S Y T f (homologous_rel_set p X S c)
= homologous_rel_set p Y T (chain_map p f c)"
by (meson Int_lower2 hom_induced image_subsetI image_subset_iff subset_iff)
lemma hom_induced_eq:
assumes "\x. x \ topspace X \ f x = g x"
shows "hom_induced p X S Y T f = hom_induced p X S Y T g"
proof -
consider "p < 0" | n where "p = int n"
by (metis int_nat_eq not_less)
then show ?thesis
proof cases
case 1
then show ?thesis
by (simp add: hom_induced_trivial)
next
case 2
have "hom_induced n X S Y T f C = hom_induced n X S Y T g C" for C
proof -
have "continuous_map X Y f \ f ` (topspace X \ S) \ T \ C \ carrier (relative_homology_group n X S)
\<longleftrightarrow> continuous_map X Y g \<and> g ` (topspace X \<inter> S) \<subseteq> T \<and> C \<in> carrier (relative_homology_group n X S)"
(is "?P = ?Q")
by (metis IntD1 assms continuous_map_eq image_cong)
then consider "\ ?P \ \ ?Q" | "?P \ ?Q"
by blast
then show ?thesis
proof cases
case 1
then show ?thesis
by (simp add: hom_induced_default)
next
case 2
have "homologous_rel_set n Y T (chain_map n f c) = homologous_rel_set n Y T (chain_map n g c)"
if "continuous_map X Y f" "f ` (topspace X \ S) \ T"
"continuous_map X Y g" "g ` (topspace X \ S) \ T"
"C = homologous_rel_set n X S c" "singular_relcycle n X S c"
for c
proof -
have "chain_map n f c = chain_map n g c"
using assms chain_map_eq singular_relcycle that by blast
then show ?thesis
by simp
qed
with 2 show ?thesis
by (auto simp: relative_homology_group_def carrier_FactGroup
right_coset_singular_relboundary hom_induced_chain_map_gen)
qed
qed
with 2 show ?thesis
by auto
qed
qed
subsection\<open>Towards the Eilenberg-Steenrod axioms\<close>
text\<open>First prove we get functors into abelian groups with the boundary map
being a natural transformation between them, and prove Eilenberg-Steenrod
axioms (we also prove additivity a bit later on if one counts that). \<close>
(*1. Exact sequence from the inclusions and boundary map
H_{p+1} X --(j')\<longlongrightarrow> H_{p+1}X (A) --(d')\<longlongrightarrow> H_p A --(i')\<longlongrightarrow> H_p X
2. Dimension axiom: H_p X is trivial for one-point X and p =/= 0
3. Homotopy invariance of the induced map
4. Excision: inclusion (X - U,A - U) --(i')\<longlongrightarrow> X (A) induces an isomorphism
when cl U \<subseteq> int A*)
lemma abelian_relative_homology_group [simp]:
"comm_group(relative_homology_group p X S)"
apply (simp add: relative_homology_group_def)
apply (metis comm_group.abelian_FactGroup abelian_relcycle_group subgroup_singular_relboundary_relcycle)
done
lemma abelian_homology_group: "comm_group(homology_group p X)"
by simp
lemma hom_induced_id_gen:
assumes contf: "continuous_map X X f" and feq: "\x. x \ topspace X \ f x = x"
and c: "c \ carrier (relative_homology_group p X S)"
shows "hom_induced p X S X S f c = c"
proof -
consider "p < 0" | n where "p = int n"
by (metis int_nat_eq not_less)
then show ?thesis
proof cases
case 1
with c show ?thesis
by (simp add: hom_induced_trivial relative_homology_group_def)
next
case 2
have cm: "chain_map n f d = d" if "singular_relcycle n X S d" for d
using that assms by (auto simp: chain_map_id_gen singular_relcycle)
have "f ` (topspace X \ S) \ S"
using feq by auto
with 2 c show ?thesis
by (auto simp: nontrivial_relative_homology_group carrier_FactGroup
cm right_coset_singular_relboundary hom_induced_chain_map_gen assms)
qed
qed
lemma hom_induced_id:
"c \ carrier (relative_homology_group p X S) \ hom_induced p X S X S id c = c"
by (rule hom_induced_id_gen) auto
lemma hom_induced_compose:
assumes "continuous_map X Y f" "f ` S \ T" "continuous_map Y Z g" "g ` T \ U"
shows "hom_induced p X S Z U (g \ f) = hom_induced p Y T Z U g \ hom_induced p X S Y T f"
proof -
consider (neg) "p < 0" | (int) n where "p = int n"
by (metis int_nat_eq not_less)
then show ?thesis
proof cases
case int
have gf: "continuous_map X Z (g \ f)"
using assms continuous_map_compose by fastforce
have gfim: "(g \ f) ` S \ U"
unfolding o_def using assms by blast
have sr: "\a. singular_relcycle n X S a \ singular_relcycle n Y T (chain_map n f a)"
by (simp add: assms singular_relcycle_chain_map)
show ?thesis
proof
fix c
show "hom_induced p X S Z U (g \ f) c = (hom_induced p Y T Z U g \ hom_induced p X S Y T f) c"
proof (cases "c \ carrier(relative_homology_group p X S)")
case True
with gfim show ?thesis
unfolding int
by (auto simp: carrier_relative_homology_group gf gfim assms sr chain_map_compose hom_induced_chain_map)
next
case False
then show ?thesis
by (simp add: hom_induced_default hom_one [OF hom_induced_hom])
qed
qed
qed (force simp: hom_induced_trivial)
qed
lemma hom_induced_compose':
assumes "continuous_map X Y f" "f ` S \ T" "continuous_map Y Z g" "g ` T \ U"
shows "hom_induced p Y T Z U g (hom_induced p X S Y T f x) = hom_induced p X S Z U (g \ f) x"
using hom_induced_compose [OF assms] by simp
lemma naturality_hom_induced:
assumes "continuous_map X Y f" "f ` S \ T"
shows "hom_boundary q Y T \ hom_induced q X S Y T f
= hom_induced (q - 1) (subtopology X S) {} (subtopology Y T) {} f \<circ> hom_boundary q X S"
proof (cases "q \ 0")
case False
then obtain p where p1: "p \ Suc 0" and q: "q = int p"
using zero_le_imp_eq_int by force
show ?thesis
proof
fix c
show "(hom_boundary q Y T \ hom_induced q X S Y T f) c =
(hom_induced (q - 1) (subtopology X S) {} (subtopology Y T) {} f \<circ> hom_boundary q X S) c"
proof (cases "c \ carrier(relative_homology_group p X S)")
case True
then obtain a where ceq: "c = homologous_rel_set p X S a" and a: "singular_relcycle p X S a"
by (force simp: carrier_relative_homology_group)
then have sr: "singular_relcycle p Y T (chain_map p f a)"
using assms singular_relcycle_chain_map by fastforce
then have sb: "singular_relcycle (p - Suc 0) (subtopology X S) {} (chain_boundary p a)"
by (metis One_nat_def a chain_boundary_boundary singular_chain_0 singular_relcycle)
have p1_eq: "int p - 1 = int (p - Suc 0)"
using p1 by auto
have cbm: "(chain_boundary p (chain_map p f a))
= (chain_map (p - Suc 0) f (chain_boundary p a))"
using a chain_boundary_chain_map singular_relcycle by blast
have contf: "continuous_map (subtopology X S) (subtopology Y T) f"
using assms
by (auto simp: continuous_map_in_subtopology topspace_subtopology
continuous_map_from_subtopology)
show ?thesis
unfolding q using assms p1 a
apply (simp add: ceq assms hom_induced_chain_map hom_boundary_chain_boundary
hom_boundary_chain_boundary [OF sr] singular_relcycle_def mod_subset_def)
apply (simp add: p1_eq contf sb cbm hom_induced_chain_map)
done
next
case False
with assms show ?thesis
unfolding q o_def using assms
apply (simp add: hom_induced_default hom_boundary_default)
by (metis group_relative_homology_group hom_boundary hom_induced hom_one one_relative_homology_group)
qed
qed
qed (force simp: hom_induced_trivial hom_boundary_trivial)
lemma homology_exactness_axiom_1:
"exact_seq ([homology_group (p-1) (subtopology X S), relative_homology_group p X S, homology_group p X],
[hom_boundary p X S,hom_induced p X {} X S id])"
proof -
consider (neg) "p < 0" | (int) n where "p = int n"
by (metis int_nat_eq not_less)
then have "(hom_induced p X {} X S id) ` carrier (homology_group p X)
= kernel (relative_homology_group p X S) (homology_group (p-1) (subtopology X S))
(hom_boundary p X S)"
proof cases
case neg
then show ?thesis
unfolding kernel_def singleton_group_def relative_homology_group_def
by (auto simp: hom_induced_trivial hom_boundary_trivial)
next
case int
have "hom_induced (int m) X {} X S id ` carrier (relative_homology_group (int m) X {})
= carrier (relative_homology_group (int m) X S) \<inter>
{c. hom_boundary (int m) X S c = \<one>\<^bsub>relative_homology_group (int m - 1) (subtopology X S) {}\<^esub>}" for m
proof (cases m)
case 0
have "hom_induced 0 X {} X S id ` carrier (relative_homology_group 0 X {})
= carrier (relative_homology_group 0 X S)" (is "?lhs = ?rhs")
proof
show "?lhs \ ?rhs"
using hom_induced_hom [of 0 X "{}" X S id]
by (simp add: hom_induced_hom hom_carrier)
show "?rhs \ ?lhs"
apply (clarsimp simp add: image_iff carrier_relative_homology_group [of 0, simplified] singular_relcycle)
apply (force simp: chain_map_id_gen chain_boundary_def singular_relcycle
hom_induced_chain_map [of concl: 0, simplified])
done
qed
with 0 show ?thesis
by (simp add: hom_boundary_trivial relative_homology_group_def [of "-1"] singleton_group_def)
next
case (Suc n)
have "(hom_induced (int (Suc n)) X {} X S id \
homologous_rel_set (Suc n) X {}) ` singular_relcycle_set (Suc n) X {}
= homologous_rel_set (Suc n) X S `
(singular_relcycle_set (Suc n) X S \<inter>
{c. hom_boundary (int (Suc n)) X S (homologous_rel_set (Suc n) X S c)
= singular_relboundary_set n (subtopology X S) {}})"
(is "?lhs = ?rhs")
proof -
have 1: "(\x. x \ A \ x \ B \ x \ C) \ f ` (A \ B) = f ` (A \ C)" for f A B C
by blast
have 2: "\\x. x \ A \ \y. y \ B \ f x = f y; \x. x \ B \ \y. y \ A \ f x = f y\
\<Longrightarrow> f ` A = f ` B" for f A B
by blast
have "?lhs = homologous_rel_set (Suc n) X S ` singular_relcycle_set (Suc n) X {}"
apply (rule image_cong [OF refl])
apply (simp add: o_def hom_induced_chain_map chain_map_ident [of _ X] singular_relcycle
del: of_nat_Suc)
done
also have "\ = homologous_rel_set (Suc n) X S `
(singular_relcycle_set (Suc n) X S \<inter>
{c. singular_relboundary n (subtopology X S) {} (chain_boundary (Suc n) c)})"
proof (rule 2)
fix c
assume "c \ singular_relcycle_set (Suc n) X {}"
then show "\y. y \ singular_relcycle_set (Suc n) X S \
{c. singular_relboundary n (subtopology X S) {} (chain_boundary (Suc n) c)} \<and>
homologous_rel_set (Suc n) X S c = homologous_rel_set (Suc n) X S y"
apply (rule_tac x=c in exI)
by (simp add: singular_boundary) (metis chain_boundary_0 singular_cycle singular_relcycle singular_relcycle_0)
next
fix c
assume c: "c \ singular_relcycle_set (Suc n) X S \
{c. singular_relboundary n (subtopology X S) {} (chain_boundary (Suc n) c)}"
then obtain d where d: "singular_chain (Suc n) (subtopology X S) d"
"chain_boundary (Suc n) d = chain_boundary (Suc n) c"
by (auto simp: singular_boundary)
with c have "c - d \ singular_relcycle_set (Suc n) X {}"
by (auto simp: singular_cycle chain_boundary_diff singular_chain_subtopology singular_relcycle singular_chain_diff)
moreover have "homologous_rel_set (Suc n) X S c = homologous_rel_set (Suc n) X S (c - d)"
proof (simp add: homologous_rel_set_eq)
show "homologous_rel (Suc n) X S c (c - d)"
using d by (simp add: homologous_rel_def singular_chain_imp_relboundary)
qed
ultimately show "\y. y \ singular_relcycle_set (Suc n) X {} \
homologous_rel_set (Suc n) X S c = homologous_rel_set (Suc n) X S y"
by blast
qed
also have "\ = ?rhs"
by (rule 1) (simp add: hom_boundary_chain_boundary homologous_rel_set_eq_relboundary del: of_nat_Suc)
finally show "?lhs = ?rhs" .
qed
with Suc show ?thesis
unfolding carrier_relative_homology_group image_comp id_def by auto
qed
then show ?thesis
by (auto simp: kernel_def int)
qed
then show ?thesis
using hom_boundary_hom hom_induced_hom
by (force simp: group_hom_def group_hom_axioms_def)
qed
lemma homology_exactness_axiom_2:
"exact_seq ([homology_group (p-1) X, homology_group (p-1) (subtopology X S), relative_homology_group p X S],
[hom_induced (p-1) (subtopology X S) {} X {} id, hom_boundary p X S])"
proof -
consider (neg) "p \ 0" | (int) n where "p = int (Suc n)"
by (metis linear not0_implies_Suc of_nat_0 zero_le_imp_eq_int)
then have "kernel (relative_homology_group (p - 1) (subtopology X S) {})
(relative_homology_group (p - 1) X {})
(hom_induced (p - 1) (subtopology X S) {} X {} id)
= hom_boundary p X S ` carrier (relative_homology_group p X S)"
proof cases
case neg
obtain x where "x \ carrier (relative_homology_group p X S)"
using group_relative_homology_group group.is_monoid by blast
with neg show ?thesis
unfolding kernel_def singleton_group_def relative_homology_group_def
by (force simp: hom_induced_trivial hom_boundary_trivial)
next
case int
have "hom_boundary (int (Suc n)) X S ` carrier (relative_homology_group (int (Suc n)) X S)
= carrier (relative_homology_group n (subtopology X S) {}) \<inter>
{c. hom_induced n (subtopology X S) {} X {} id c =
\<one>\<^bsub>relative_homology_group n X {}\<^esub>}"
(is "?lhs = ?rhs")
proof -
have 1: "(\x. x \ A \ x \ B \ x \ C) \ f ` (A \ B) = f ` (A \ C)" for f A B C
by blast
have 2: "(\x. x \ A \ x \ B \ x \ f -` C) \ f ` (A \ B) = f ` A \ C" for f A B C
by blast
have "?lhs = homologous_rel_set n (subtopology X S) {}
` (chain_boundary (Suc n) ` singular_relcycle_set (Suc n) X S)"
unfolding carrier_relative_homology_group image_comp
by (rule image_cong [OF refl]) (simp add: o_def hom_boundary_chain_boundary del: of_nat_Suc)
also have "\ = homologous_rel_set n (subtopology X S) {} `
(singular_relcycle_set n (subtopology X S) {} \<inter> singular_relboundary_set n X {})"
by (force simp: singular_relcycle singular_boundary chain_boundary_boundary_alt)
also have "\ = ?rhs"
unfolding carrier_relative_homology_group vimage_def
apply (rule 2)
apply (auto simp: hom_induced_chain_map chain_map_ident homologous_rel_set_eq_relboundary singular_relcycle)
done
finally show ?thesis .
qed
then show ?thesis
by (auto simp: kernel_def int)
qed
then show ?thesis
using hom_boundary_hom hom_induced_hom
by (force simp: group_hom_def group_hom_axioms_def)
qed
lemma homology_exactness_axiom_3:
"exact_seq ([relative_homology_group p X S, homology_group p X, homology_group p (subtopology X S)],
[hom_induced p X {} X S id, hom_induced p (subtopology X S) {} X {} id])"
proof (cases "p < 0")
case True
then show ?thesis
apply (simp add: relative_homology_group_def hom_induced_trivial group_hom_def group_hom_axioms_def)
apply (auto simp: kernel_def singleton_group_def)
done
next
case False
then obtain n where peq: "p = int n"
by (metis int_ops(1) linorder_neqE_linordered_idom pos_int_cases)
have "hom_induced n (subtopology X S) {} X {} id `
(homologous_rel_set n (subtopology X S) {} `
singular_relcycle_set n (subtopology X S) {})
= {c \<in> homologous_rel_set n X {} ` singular_relcycle_set n X {}.
hom_induced n X {} X S id c = singular_relboundary_set n X S}"
(is "?lhs = ?rhs")
proof -
have 2: "\\x. x \ A \ \y. y \ B \ f x = f y; \x. x \ B \ \y. y \ A \ f x = f y\
\<Longrightarrow> f ` A = f ` B" for f A B
by blast
have "?lhs = homologous_rel_set n X {} ` (singular_relcycle_set n (subtopology X S) {})"
unfolding image_comp o_def
apply (rule image_cong [OF refl])
apply (simp add: hom_induced_chain_map singular_relcycle)
apply (metis chain_map_ident)
done
also have "\ = homologous_rel_set n X {} ` (singular_relcycle_set n X {} \ singular_relboundary_set n X S)"
proof (rule 2)
fix c
assume "c \ singular_relcycle_set n (subtopology X S) {}"
then show "\y. y \ singular_relcycle_set n X {} \ singular_relboundary_set n X S \
homologous_rel_set n X {} c = homologous_rel_set n X {} y"
using singular_chain_imp_relboundary singular_cycle singular_relboundary_imp_chain singular_relcycle by fastforce
next
fix c
assume "c \ singular_relcycle_set n X {} \ singular_relboundary_set n X S"
then obtain d e where c: "singular_relcycle n X {} c" "singular_relboundary n X S c"
and d: "singular_chain n (subtopology X S) d"
and e: "singular_chain (Suc n) X e" "chain_boundary (Suc n) e = c + d"
using singular_relboundary_alt by blast
then have "chain_boundary n (c + d) = 0"
using chain_boundary_boundary_alt by fastforce
then have "chain_boundary n c + chain_boundary n d = 0"
by (metis chain_boundary_add)
with c have "singular_relcycle n (subtopology X S) {} (- d)"
by (metis (no_types) d eq_add_iff singular_cycle singular_relcycle_minus)
moreover have "homologous_rel n X {} c (- d)"
using c
by (metis diff_minus_eq_add e homologous_rel_def singular_boundary)
ultimately
show "\y. y \ singular_relcycle_set n (subtopology X S) {} \
homologous_rel_set n X {} c = homologous_rel_set n X {} y"
by (force simp: homologous_rel_set_eq)
qed
also have "\ = homologous_rel_set n X {} `
(singular_relcycle_set n X {} \<inter> homologous_rel_set n X {} -` {x. hom_induced n X {} X S id x = singular_relboundary_set n X S})"
by (rule 2) (auto simp: hom_induced_chain_map homologous_rel_set_eq_relboundary chain_map_ident [of _ X] singular_cycle cong: conj_cong)
also have "\ = ?rhs"
by blast
finally show ?thesis .
qed
then have "kernel (relative_homology_group p X {}) (relative_homology_group p X S) (hom_induced p X {} X S id)
= hom_induced p (subtopology X S) {} X {} id ` carrier (relative_homology_group p (subtopology X S) {})"
by (simp add: kernel_def carrier_relative_homology_group peq)
then show ?thesis
by (simp add: not_less group_hom_def group_hom_axioms_def hom_induced_hom)
qed
lemma homology_dimension_axiom:
assumes X: "topspace X = {a}" and "p \ 0"
shows "trivial_group(homology_group p X)"
proof (cases "p < 0")
case True
then show ?thesis
by simp
next
case False
then obtain n where peq: "p = int n" "n > 0"
by (metis assms(2) neq0_conv nonneg_int_cases not_less of_nat_0)
have "homologous_rel_set n X {} ` singular_relcycle_set n X {} = {singular_relcycle_set n X {}}"
(is "?lhs = ?rhs")
proof
show "?lhs \ ?rhs"
using peq assms
by (auto simp: image_subset_iff homologous_rel_set_eq_relboundary simp flip: singular_boundary_set_eq_cycle_singleton)
have "singular_relboundary n X {} 0"
by simp
with peq assms
show "?rhs \ ?lhs"
by (auto simp: image_iff simp flip: homologous_rel_eq_relboundary singular_boundary_set_eq_cycle_singleton)
qed
with peq assms show ?thesis
unfolding trivial_group_def
by (simp add: carrier_relative_homology_group singular_boundary_set_eq_cycle_singleton [OF X])
qed
proposition homology_homotopy_axiom:
assumes "homotopic_with (\h. h ` S \ T) X Y f g"
shows "hom_induced p X S Y T f = hom_induced p X S Y T g"
proof (cases "p < 0")
case True
then show ?thesis
by (simp add: hom_induced_trivial)
next
case False
then obtain n where peq: "p = int n"
by (metis int_nat_eq not_le)
have cont: "continuous_map X Y f" "continuous_map X Y g"
using assms homotopic_with_imp_continuous_maps by blast+
have im: "f ` (topspace X \ S) \ T" "g ` (topspace X \ S) \ T"
using homotopic_with_imp_property assms by blast+
show ?thesis
proof
fix c show "hom_induced p X S Y T f c = hom_induced p X S Y T g c"
proof (cases "c \ carrier(relative_homology_group p X S)")
case True
then obtain a where a: "c = homologous_rel_set n X S a" "singular_relcycle n X S a"
unfolding carrier_relative_homology_group peq by auto
then show ?thesis
apply (simp add: peq hom_induced_chain_map_gen cont im homologous_rel_set_eq)
apply (blast intro: assms homotopic_imp_homologous_rel_chain_maps)
done
qed (simp add: hom_induced_default)
qed
qed
proposition homology_excision_axiom:
assumes "X closure_of U \ X interior_of T" "T \ S"
shows
"hom_induced p (subtopology X (S - U)) (T - U) (subtopology X S) T id
\<in> iso (relative_homology_group p (subtopology X (S - U)) (T - U))
(relative_homology_group p (subtopology X S) T)"
proof (cases "p < 0")
case True
then show ?thesis
unfolding iso_def bij_betw_def relative_homology_group_def by (simp add: hom_induced_trivial)
next
case False
then obtain n where peq: "p = int n"
by (metis int_nat_eq not_le)
have cont: "continuous_map (subtopology X (S - U)) (subtopology X S) id"
by (simp add: closure_of_subtopology_mono continuous_map_eq_image_closure_subset)
have TU: "topspace X \ (S - U) \ (T - U) \ T"
by auto
show ?thesis
proof (simp add: iso_def peq carrier_relative_homology_group bij_betw_def hom_induced_hom, intro conjI)
show "inj_on (hom_induced n (subtopology X (S - U)) (T - U) (subtopology X S) T id)
(homologous_rel_set n (subtopology X (S - U)) (T - U) `
singular_relcycle_set n (subtopology X (S - U)) (T - U))"
unfolding inj_on_def
proof (clarsimp simp add: homologous_rel_set_eq)
fix c d
assume c: "singular_relcycle n (subtopology X (S - U)) (T - U) c"
and d: "singular_relcycle n (subtopology X (S - U)) (T - U) d"
and hh: "hom_induced n (subtopology X (S - U)) (T - U) (subtopology X S) T id
(homologous_rel_set n (subtopology X (S - U)) (T - U) c)
= hom_induced n (subtopology X (S - U)) (T - U) (subtopology X S) T id
(homologous_rel_set n (subtopology X (S - U)) (T - U) d)"
then have scc: "singular_chain n (subtopology X (S - U)) c"
and scd: "singular_chain n (subtopology X (S - U)) d"
using singular_relcycle by blast+
have "singular_relboundary n (subtopology X (S - U)) (T - U) c"
if srb: "singular_relboundary n (subtopology X S) T c"
and src: "singular_relcycle n (subtopology X (S - U)) (T - U) c" for c
proof -
have [simp]: "(S - U) \ (T - U) = T - U" "S \ T = T"
using \<open>T \<subseteq> S\<close> by blast+
have c: "singular_chain n (subtopology X (S - U)) c"
"singular_chain (n - Suc 0) (subtopology X (T - U)) (chain_boundary n c)"
using that by (auto simp: singular_relcycle_def mod_subset_def subtopology_subtopology)
obtain d e where d: "singular_chain (Suc n) (subtopology X S) d"
and e: "singular_chain n (subtopology X T) e"
and dce: "chain_boundary (Suc n) d = c + e"
using srb by (auto simp: singular_relboundary_alt subtopology_subtopology)
obtain m f g where f: "singular_chain (Suc n) (subtopology X (S - U)) f"
and g: "singular_chain (Suc n) (subtopology X T) g"
and dfg: "(singular_subdivision (Suc n) ^^ m) d = f + g"
using excised_chain_exists [OF assms d] .
obtain h where
h0: "\p. h p 0 = (0 :: 'a chain)"
and hdiff: "\p c1 c2. h p (c1-c2) = h p c1 - h p c2"
and hSuc: "\p X c. singular_chain p X c \ singular_chain (Suc p) X (h p c)"
and hchain: "\p X c. singular_chain p X c
\<Longrightarrow> chain_boundary (Suc p) (h p c) + h (p - Suc 0) (chain_boundary p c)
= (singular_subdivision p ^^ m) c - c"
using chain_homotopic_iterated_singular_subdivision by blast
have hadd: "\p c1 c2. h p (c1 + c2) = h p c1 + h p c2"
by (metis add_diff_cancel diff_add_cancel hdiff)
define c1 where "c1 \ f - h n c"
define c2 where "c2 \ chain_boundary (Suc n) (h n e) - (chain_boundary (Suc n) g - e)"
show ?thesis
unfolding singular_relboundary_alt
proof (intro exI conjI)
show c1: "singular_chain (Suc n) (subtopology X (S - U)) c1"
by (simp add: \<open>singular_chain n (subtopology X (S - U)) c\<close> c1_def f hSuc singular_chain_diff)
have "chain_boundary (Suc n) (chain_boundary (Suc (Suc n)) (h (Suc n) d) + h n (c+e))
= chain_boundary (Suc n) (f + g - d)"
using hchain [OF d] by (simp add: dce dfg)
then have "chain_boundary (Suc n) (h n (c + e))
= chain_boundary (Suc n) f + chain_boundary (Suc n) g - (c + e)"
using chain_boundary_boundary_alt [of "Suc n" "subtopology X S"]
by (simp add: chain_boundary_add chain_boundary_diff d hSuc dce)
then have "chain_boundary (Suc n) (h n c) + chain_boundary (Suc n) (h n e)
= chain_boundary (Suc n) f + chain_boundary (Suc n) g - (c + e)"
by (simp add: chain_boundary_add hadd)
then have *: "chain_boundary (Suc n) (f - h n c) = c + (chain_boundary (Suc n) (h n e) - (chain_boundary (Suc n) g - e))"
by (simp add: algebra_simps chain_boundary_diff)
then show "chain_boundary (Suc n) c1 = c + c2"
unfolding c1_def c2_def
by (simp add: algebra_simps chain_boundary_diff)
have "singular_chain n (subtopology X (S - U)) c2" "singular_chain n (subtopology X T) c2"
using singular_chain_diff c c1 *
unfolding c1_def c2_def
apply (metis add_diff_cancel_left' singular_chain_boundary_alt)
by (simp add: e g hSuc singular_chain_boundary_alt singular_chain_diff)
then show "singular_chain n (subtopology (subtopology X (S - U)) (T - U)) c2"
by (fastforce simp add: singular_chain_subtopology)
qed
qed
then have "singular_relboundary n (subtopology X S) T (c - d) \
singular_relboundary n (subtopology X (S - U)) (T - U) (c - d)"
using c d singular_relcycle_diff by metis
with hh show "homologous_rel n (subtopology X (S - U)) (T - U) c d"
apply (simp add: hom_induced_chain_map cont c d chain_map_ident [OF scc] chain_map_ident [OF scd])
using homologous_rel_set_eq homologous_rel_def by metis
qed
next
have h: "homologous_rel_set n (subtopology X S) T a
\<in> (\<lambda>x. homologous_rel_set n (subtopology X S) T (chain_map n id x)) `
singular_relcycle_set n (subtopology X (S - U)) (T - U)"
if a: "singular_relcycle n (subtopology X S) T a" for a
proof -
obtain c' where c': "singular_relcycle n (subtopology X (S - U)) (T - U) c'"
"homologous_rel n (subtopology X S) T a c'"
using a by (blast intro: excised_relcycle_exists [OF assms])
then have scc': "singular_chain n (subtopology X S) c'"
using homologous_rel_singular_chain singular_relcycle that by blast
then show ?thesis
apply (rule_tac x="c'" in image_eqI)
apply (auto simp: scc' chain_map_ident [of _ "subtopology X S"] c' homologous_rel_set_eq)
done
qed
show "hom_induced n (subtopology X (S - U)) (T - U) (subtopology X S) T id `
homologous_rel_set n (subtopology X (S - U)) (T - U) `
singular_relcycle_set n (subtopology X (S - U)) (T - U)
= homologous_rel_set n (subtopology X S) T ` singular_relcycle_set n (subtopology X S) T"
apply (simp add: image_comp o_def hom_induced_chain_map_gen cont TU topspace_subtopology
cong: image_cong_simp)
apply (force simp: cont h singular_relcycle_chain_map)
done
qed
qed
subsection\<open>Additivity axiom\<close>
text\<open>Not in the original Eilenberg-Steenrod list but usually included nowadays,
following Milnor's "On Axiomatic Homology Theory".\
lemma iso_chain_group_sum:
assumes disj: "pairwise disjnt \" and UU: "\\ = topspace X"
and subs: "\C T. \compactin X C; path_connectedin X C; T \ \; ~ disjnt C T\ \ C \ T"
shows "(\f. sum' f \) \ iso (sum_group \ (\S. chain_group p (subtopology X S))) (chain_group p X)"
proof -
have pw: "pairwise (\i j. disjnt (singular_simplex_set p (subtopology X i))
(singular_simplex_set p (subtopology X j))) \<U>"
proof
fix S T
assume "S \ \" "T \ \" "S \ T"
then show "disjnt (singular_simplex_set p (subtopology X S))
(singular_simplex_set p (subtopology X T))"
using nonempty_standard_simplex [of p] disj
by (fastforce simp: pairwise_def disjnt_def singular_simplex_subtopology image_subset_iff)
qed
have "\S\\. singular_simplex p (subtopology X S) f"
if f: "singular_simplex p X f" for f
proof -
obtain x where x: "x \ topspace X" "x \ f ` standard_simplex p"
using f nonempty_standard_simplex [of p] continuous_map_image_subset_topspace
unfolding singular_simplex_def by fastforce
then obtain S where "S \ \" "x \ S"
using UU by auto
have "f ` standard_simplex p \ S"
proof (rule subs)
have cont: "continuous_map (subtopology (powertop_real UNIV)
(standard_simplex p)) X f"
using f singular_simplex_def by auto
show "compactin X (f ` standard_simplex p)"
by (simp add: compactin_subtopology compactin_standard_simplex image_compactin [OF _ cont])
show "path_connectedin X (f ` standard_simplex p)"
by (simp add: path_connectedin_subtopology path_connectedin_standard_simplex path_connectedin_continuous_map_image [OF cont])
have "standard_simplex p \ {}"
by (simp add: nonempty_standard_simplex)
then
show "\ disjnt (f ` standard_simplex p) S"
using x \<open>x \<in> S\<close> by (auto simp: disjnt_def)
qed (auto simp: \<open>S \<in> \<U>\<close>)
then show ?thesis
by (meson \<open>S \<in> \<U>\<close> singular_simplex_subtopology that)
qed
then have "(\i\\. singular_simplex_set p (subtopology X i)) = singular_simplex_set p X"
by (auto simp: singular_simplex_subtopology)
then show ?thesis
using iso_free_Abelian_group_sum [OF pw] by (simp add: chain_group_def)
qed
lemma relcycle_group_0_eq_chain_group: "relcycle_group 0 X {} = chain_group 0 X"
apply (rule monoid.equality, simp)
apply (simp_all add: relcycle_group_def chain_group_def)
by (metis chain_boundary_def singular_cycle)
proposition iso_cycle_group_sum:
assumes disj: "pairwise disjnt \" and UU: "\\ = topspace X"
and subs: "\C T. \compactin X C; path_connectedin X C; T \ \; \ disjnt C T\ \ C \ T"
shows "(\f. sum' f \) \ iso (sum_group \ (\T. relcycle_group p (subtopology X T) {}))
(relcycle_group p X {})"
proof (cases "p = 0")
case True
then show ?thesis
by (simp add: relcycle_group_0_eq_chain_group iso_chain_group_sum [OF assms])
next
case False
let ?SG = "(sum_group \ (\T. chain_group p (subtopology X T)))"
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.51Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
|
|
|
|
|
