# HG changeset patch # User paulson # Date 1554840348 -3600 # Node ID c4f2cac288d27da17567dbc75ef8b96504695efe # Parent a93e6472ac9c3b050c966f29bc951aee44f1c4e4# Parent e8f4ce87012b82dc229541ff0da60b6981f60593 merged diff -r a93e6472ac9c -r c4f2cac288d2 src/HOL/Algebra/Group.thy --- a/src/HOL/Algebra/Group.thy Tue Apr 09 16:59:00 2019 +0000 +++ b/src/HOL/Algebra/Group.thy Tue Apr 09 21:05:48 2019 +0100 @@ -913,6 +913,9 @@ "\h \ hom G H; bij_betw h (carrier G) (carrier H)\ \ h \ iso G H" by (auto simp: iso_def) +lemma is_isoI: "h \ iso G H \ G \ H" + using is_iso_def by auto + lemma epi_iff_subset: "f \ epi G G' \ f \ hom G G' \ carrier G' \ f ` carrier G" by (auto simp: epi_def hom_def) diff -r a93e6472ac9c -r c4f2cac288d2 src/HOL/Homology/Brouwer_Degree.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Homology/Brouwer_Degree.thy Tue Apr 09 21:05:48 2019 +0100 @@ -0,0 +1,1687 @@ +section\Homology, III: Brouwer Degree\ + +theory Brouwer_Degree + imports Homology_Groups + +begin + +lemma Eps_cong: + assumes "\x. P x = Q x" + shows "Eps P = Eps Q" + using ext[of P Q, OF assms] by simp + +subsection\Reduced Homology\ + +definition reduced_homology_group :: "int \ 'a topology \ 'a chain set monoid" + where "reduced_homology_group p X \ + subgroup_generated (homology_group p X) + (kernel (homology_group p X) (homology_group p (discrete_topology {()})) + (hom_induced p X {} (discrete_topology {()}) {} (\x. ())))" + +lemma one_reduced_homology_group: "\\<^bsub>reduced_homology_group p X\<^esub> = \\<^bsub>homology_group p X\<^esub>" + by (simp add: reduced_homology_group_def) + +lemma group_reduced_homology_group [simp]: "group (reduced_homology_group p X)" + by (simp add: reduced_homology_group_def group.group_subgroup_generated) + +lemma carrier_reduced_homology_group: + "carrier (reduced_homology_group p X) = + kernel (homology_group p X) (homology_group p (discrete_topology {()})) + (hom_induced p X {} (discrete_topology {()}) {} (\x. ()))" + (is "_ = kernel ?G ?H ?h") +proof - + interpret subgroup "kernel ?G ?H ?h" ?G + by (simp add: hom_induced_empty_hom group_hom_axioms_def group_hom_def group_hom.subgroup_kernel) + show ?thesis + unfolding reduced_homology_group_def + using carrier_subgroup_generated_subgroup by blast +qed + +lemma carrier_reduced_homology_group_subset: + "carrier (reduced_homology_group p X) \ carrier (homology_group p X)" + by (simp add: group.carrier_subgroup_generated_subset reduced_homology_group_def) + +lemma un_reduced_homology_group: + assumes "p \ 0" + shows "reduced_homology_group p X = homology_group p X" +proof - + have "(kernel (homology_group p X) (homology_group p (discrete_topology {()})) + (hom_induced p X {} (discrete_topology {()}) {} (\x. ()))) + = carrier (homology_group p X)" + proof (rule group_hom.kernel_to_trivial_group) + show "group_hom (homology_group p X) (homology_group p (discrete_topology {()})) + (hom_induced p X {} (discrete_topology {()}) {} (\x. ()))" + by (auto simp: hom_induced_empty_hom group_hom_def group_hom_axioms_def) + show "trivial_group (homology_group p (discrete_topology {()}))" + by (simp add: homology_dimension_axiom [OF _ assms]) + qed + then show ?thesis + by (simp add: reduced_homology_group_def group.subgroup_generated_group_carrier) +qed + +lemma trivial_reduced_homology_group: + "p < 0 \ trivial_group(reduced_homology_group p X)" + by (simp add: trivial_homology_group un_reduced_homology_group) + +lemma hom_induced_reduced_hom: + "(hom_induced p X {} Y {} f) \ hom (reduced_homology_group p X) (reduced_homology_group p Y)" +proof (cases "continuous_map X Y f") + case True + have eq: "continuous_map X Y f + \ hom_induced p X {} (discrete_topology {()}) {} (\x. ()) + = (hom_induced p Y {} (discrete_topology {()}) {} (\x. ()) \ hom_induced p X {} Y {} f)" + by (simp flip: hom_induced_compose_empty) + interpret subgroup "kernel (homology_group p X) + (homology_group p (discrete_topology {()})) + (hom_induced p X {} (discrete_topology {()}) {} (\x. ()))" + "homology_group p X" + by (meson group_hom.subgroup_kernel group_hom_axioms_def group_hom_def group_relative_homology_group hom_induced) + have sb: "hom_induced p X {} Y {} f ` carrier (homology_group p X) \ carrier (homology_group p Y)" + using hom_induced_carrier by blast + show ?thesis + using True + unfolding reduced_homology_group_def + apply (simp add: hom_into_subgroup_eq group_hom.subgroup_kernel hom_induced_empty_hom group.hom_from_subgroup_generated group_hom_def group_hom_axioms_def) + unfolding kernel_def using eq sb by auto +next + case False + then have "hom_induced p X {} Y {} f = (\c. one(reduced_homology_group p Y))" + by (force simp: hom_induced_default reduced_homology_group_def) + then show ?thesis + by (simp add: trivial_hom) +qed + + +lemma hom_induced_reduced: + "c \ carrier(reduced_homology_group p X) + \ hom_induced p X {} Y {} f c \ carrier(reduced_homology_group p Y)" + by (meson hom_in_carrier hom_induced_reduced_hom) + +lemma hom_boundary_reduced_hom: + "hom_boundary p X S + \ hom (relative_homology_group p X S) (reduced_homology_group (p-1) (subtopology X S))" +proof - + have *: "continuous_map X (discrete_topology {()}) (\x. ())" "(\x. ()) ` S \ {()}" + by auto + interpret group_hom "relative_homology_group p (discrete_topology {()}) {()}" + "homology_group (p-1) (discrete_topology {()})" + "hom_boundary p (discrete_topology {()}) {()}" + apply (clarsimp simp: group_hom_def group_hom_axioms_def) + by (metis UNIV_unit hom_boundary_hom subtopology_UNIV) + have "hom_boundary p X S ` + carrier (relative_homology_group p X S) + \ kernel (homology_group (p - 1) (subtopology X S)) + (homology_group (p - 1) (discrete_topology {()})) + (hom_induced (p - 1) (subtopology X S) {} + (discrete_topology {()}) {} (\x. ()))" + proof (clarsimp simp add: kernel_def hom_boundary_carrier) + fix c + assume c: "c \ carrier (relative_homology_group p X S)" + have triv: "trivial_group (relative_homology_group p (discrete_topology {()}) {()})" + by (metis topspace_discrete_topology trivial_relative_homology_group_topspace) + have "hom_boundary p (discrete_topology {()}) {()} + (hom_induced p X S (discrete_topology {()}) {()} (\x. ()) c) + = \\<^bsub>homology_group (p - 1) (discrete_topology {()})\<^esub>" + by (metis hom_induced_carrier local.hom_one singletonD triv trivial_group_def) + then show "hom_induced (p - 1) (subtopology X S) {} (discrete_topology {()}) {} (\x. ()) (hom_boundary p X S c) = + \\<^bsub>homology_group (p - 1) (discrete_topology {()})\<^esub>" + using naturality_hom_induced [OF *, of p, symmetric] by (simp add: o_def fun_eq_iff) + qed + then show ?thesis + by (simp add: reduced_homology_group_def hom_boundary_hom hom_into_subgroup) +qed + + +lemma homotopy_equivalence_reduced_homology_group_isomorphisms: + assumes contf: "continuous_map X Y f" and contg: "continuous_map Y X g" + and gf: "homotopic_with (\h. True) X X (g \ f) id" + and fg: "homotopic_with (\k. True) Y Y (f \ g) id" + shows "group_isomorphisms (reduced_homology_group p X) (reduced_homology_group p Y) + (hom_induced p X {} Y {} f) (hom_induced p Y {} X {} g)" +proof (simp add: hom_induced_reduced_hom group_isomorphisms_def, intro conjI ballI) + fix a + assume "a \ carrier (reduced_homology_group p X)" + then have "(hom_induced p Y {} X {} g \ hom_induced p X {} Y {} f) a = a" + apply (simp add: contf contg flip: hom_induced_compose) + using carrier_reduced_homology_group_subset gf hom_induced_id homology_homotopy_empty by fastforce + then show "hom_induced p Y {} X {} g (hom_induced p X {} Y {} f a) = a" + by simp +next + fix b + assume "b \ carrier (reduced_homology_group p Y)" + then have "(hom_induced p X {} Y {} f \ hom_induced p Y {} X {} g) b = b" + apply (simp add: contf contg flip: hom_induced_compose) + using carrier_reduced_homology_group_subset fg hom_induced_id homology_homotopy_empty by fastforce + then show "hom_induced p X {} Y {} f (hom_induced p Y {} X {} g b) = b" + by (simp add: carrier_reduced_homology_group) +qed + +lemma homotopy_equivalence_reduced_homology_group_isomorphism: + assumes "continuous_map X Y f" "continuous_map Y X g" + and "homotopic_with (\h. True) X X (g \ f) id" "homotopic_with (\k. True) Y Y (f \ g) id" + shows "(hom_induced p X {} Y {} f) + \ iso (reduced_homology_group p X) (reduced_homology_group p Y)" +proof (rule group_isomorphisms_imp_iso) + show "group_isomorphisms (reduced_homology_group p X) (reduced_homology_group p Y) + (hom_induced p X {} Y {} f) (hom_induced p Y {} X {} g)" + by (simp add: assms homotopy_equivalence_reduced_homology_group_isomorphisms) +qed + +lemma homotopy_equivalent_space_imp_isomorphic_reduced_homology_groups: + "X homotopy_equivalent_space Y + \ reduced_homology_group p X \ reduced_homology_group p Y" + unfolding homotopy_equivalent_space_def + using homotopy_equivalence_reduced_homology_group_isomorphism is_isoI by blast + +lemma homeomorphic_space_imp_isomorphic_reduced_homology_groups: + "X homeomorphic_space Y \ reduced_homology_group p X \ reduced_homology_group p Y" + by (simp add: homeomorphic_imp_homotopy_equivalent_space homotopy_equivalent_space_imp_isomorphic_reduced_homology_groups) + +lemma trivial_reduced_homology_group_empty: + "topspace X = {} \ trivial_group(reduced_homology_group p X)" + by (metis carrier_reduced_homology_group_subset group.trivial_group_alt group_reduced_homology_group trivial_group_def trivial_homology_group_empty) + +lemma homology_dimension_reduced: + assumes "topspace X = {a}" + shows "trivial_group (reduced_homology_group p X)" +proof - + have iso: "(hom_induced p X {} (discrete_topology {()}) {} (\x. ())) + \ iso (homology_group p X) (homology_group p (discrete_topology {()}))" + apply (rule homeomorphic_map_homology_iso) + apply (force simp: homeomorphic_map_maps homeomorphic_maps_def assms) + done + show ?thesis + unfolding reduced_homology_group_def + by (rule group.trivial_group_subgroup_generated) (use iso in \auto simp: iso_kernel_image\) +qed + + +lemma trivial_reduced_homology_group_contractible_space: + "contractible_space X \ trivial_group (reduced_homology_group p X)" + apply (simp add: contractible_eq_homotopy_equivalent_singleton_subtopology) + apply (auto simp: trivial_reduced_homology_group_empty) + using isomorphic_group_triviality + by (metis (full_types) group_reduced_homology_group homology_dimension_reduced homotopy_equivalent_space_imp_isomorphic_reduced_homology_groups path_connectedin_def path_connectedin_singleton topspace_subtopology_subset) + + +lemma image_reduced_homology_group: + assumes "topspace X \ S \ {}" + shows "hom_induced p X {} X S id ` carrier (reduced_homology_group p X) + = hom_induced p X {} X S id ` carrier (homology_group p X)" + (is "?h ` carrier ?G = ?h ` carrier ?H") +proof - + obtain a where a: "a \ topspace X" and "a \ S" + using assms by blast + have [simp]: "A \ {x \ A. P x} = {x \ A. P x}" for A P + by blast + interpret comm_group "homology_group p X" + by (rule abelian_relative_homology_group) + have *: "\x'. ?h y = ?h x' \ + x' \ carrier ?H \ + hom_induced p X {} (discrete_topology {()}) {} (\x. ()) x' + = \\<^bsub>homology_group p (discrete_topology {()})\<^esub>" + if "y \ carrier ?H" for y + proof - + let ?f = "hom_induced p (discrete_topology {()}) {} X {} (\x. a)" + let ?g = "hom_induced p X {} (discrete_topology {()}) {} (\x. ())" + have bcarr: "?f (?g y) \ carrier ?H" + by (simp add: hom_induced_carrier) + interpret gh1: + group_hom "relative_homology_group p X S" "relative_homology_group p (discrete_topology {()}) {()}" + "hom_induced p X S (discrete_topology {()}) {()} (\x. ())" + by (meson group_hom_axioms_def group_hom_def hom_induced_hom group_relative_homology_group) + interpret gh2: + group_hom "relative_homology_group p (discrete_topology {()}) {()}" "relative_homology_group p X S" + "hom_induced p (discrete_topology {()}) {()} X S (\x. a)" + by (meson group_hom_axioms_def group_hom_def hom_induced_hom group_relative_homology_group) + interpret gh3: + group_hom "homology_group p X" "relative_homology_group p X S" "?h" + by (meson group_hom_axioms_def group_hom_def hom_induced_hom group_relative_homology_group) + interpret gh4: + group_hom "homology_group p X" "homology_group p (discrete_topology {()})" + "?g" + by (meson group_hom_axioms_def group_hom_def hom_induced_hom group_relative_homology_group) + interpret gh5: + group_hom "homology_group p (discrete_topology {()})" "homology_group p X" + "?f" + by (meson group_hom_axioms_def group_hom_def hom_induced_hom group_relative_homology_group) + interpret gh6: + group_hom "homology_group p (discrete_topology {()})" "relative_homology_group p (discrete_topology {()}) {()}" + "hom_induced p (discrete_topology {()}) {} (discrete_topology {()}) {()} id" + by (meson group_hom_axioms_def group_hom_def hom_induced_hom group_relative_homology_group) + show ?thesis + proof (intro exI conjI) + have "(?h \ ?f \ ?g) y + = (hom_induced p (discrete_topology {()}) {()} X S (\x. a) \ + hom_induced p (discrete_topology {()}) {} (discrete_topology {()}) {()} id \ ?g) y" + by (simp add: a \a \ S\ flip: hom_induced_compose) + also have "\ = \\<^bsub>relative_homology_group p X S\<^esub>" + using trivial_relative_homology_group_topspace [of p "discrete_topology {()}"] + apply simp + by (metis (full_types) empty_iff gh1.H.one_closed gh1.H.trivial_group gh2.hom_one hom_induced_carrier insert_iff) + finally have "?h (?f (?g y)) = \\<^bsub>relative_homology_group p X S\<^esub>" + by simp + then show "?h y = ?h (y \\<^bsub>?H\<^esub> inv\<^bsub>?H\<^esub> ?f (?g y))" + by (simp add: that hom_induced_carrier) + show "(y \\<^bsub>?H\<^esub> inv\<^bsub>?H\<^esub> ?f (?g y)) \ carrier (homology_group p X)" + by (simp add: hom_induced_carrier that) + have *: "(?g \ hom_induced p X {} X {} (\x. a)) y = hom_induced p X {} (discrete_topology {()}) {} (\a. ()) y" + by (simp add: a \a \ S\ flip: hom_induced_compose) + have "?g (y \\<^bsub>?H\<^esub> inv\<^bsub>?H\<^esub> (?f \ ?g) y) + = \\<^bsub>homology_group p (discrete_topology {()})\<^esub>" + by (simp add: a \a \ S\ that hom_induced_carrier flip: hom_induced_compose * [unfolded o_def]) + then show "?g (y \\<^bsub>?H\<^esub> inv\<^bsub>?H\<^esub> ?f (?g y)) + = \\<^bsub>homology_group p (discrete_topology {()})\<^esub>" + by simp + qed + qed + show ?thesis + apply (auto simp: reduced_homology_group_def carrier_subgroup_generated kernel_def image_iff) + apply (metis (no_types, lifting) generate_in_carrier mem_Collect_eq subsetI) + apply (force simp: dest: * intro: generate.incl) + done +qed + + +lemma homology_exactness_reduced_1: + assumes "topspace X \ S \ {}" + shows "exact_seq([reduced_homology_group(p - 1) (subtopology X S), + relative_homology_group p X S, + reduced_homology_group p X], + [hom_boundary p X S, hom_induced p X {} X S id])" + (is "exact_seq ([?G1,?G2,?G3], [?h1,?h2])") +proof - + have *: "?h2 ` carrier (homology_group p X) + = kernel ?G2 (homology_group (p - 1) (subtopology X S)) ?h1" + using homology_exactness_axiom_1 [of p X S] by simp + have gh: "group_hom ?G3 ?G2 ?h2" + by (simp add: reduced_homology_group_def group_hom_def group_hom_axioms_def + group.group_subgroup_generated group.hom_from_subgroup_generated hom_induced_hom) + show ?thesis + apply (simp add: hom_boundary_reduced_hom gh * image_reduced_homology_group [OF assms]) + apply (simp add: kernel_def one_reduced_homology_group) + done +qed + + +lemma homology_exactness_reduced_2: + "exact_seq([reduced_homology_group(p - 1) X, + reduced_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])" + (is "exact_seq ([?G1,?G2,?G3], [?h1,?h2])") + using homology_exactness_axiom_2 [of p X S] + apply (simp add: group_hom_axioms_def group_hom_def hom_boundary_reduced_hom hom_induced_reduced_hom) + apply (simp add: reduced_homology_group_def group_hom.subgroup_kernel group_hom_axioms_def group_hom_def hom_induced_hom) + using hom_boundary_reduced_hom [of p X S] + apply (auto simp: image_def set_eq_iff) + by (metis carrier_reduced_homology_group hom_in_carrier set_eq_iff) + + +lemma homology_exactness_reduced_3: + "exact_seq([relative_homology_group p X S, + reduced_homology_group p X, + reduced_homology_group p (subtopology X S)], + [hom_induced p X {} X S id, hom_induced p (subtopology X S) {} X {} id])" + (is "exact_seq ([?G1,?G2,?G3], [?h1,?h2])") +proof - + have "kernel ?G2 ?G1 ?h1 = + ?h2 ` carrier ?G3" + proof - + obtain U where U: + "(hom_induced p (subtopology X S) {} X {} id) ` carrier ?G3 \ U" + "(hom_induced p (subtopology X S) {} X {} id) ` carrier ?G3 + \ (hom_induced p (subtopology X S) {} X {} id) ` carrier (homology_group p (subtopology X S))" + "U \ kernel (homology_group p X) ?G1 (hom_induced p X {} X S id) + = kernel ?G2 ?G1 (hom_induced p X {} X S id)" + "U \ (hom_induced p (subtopology X S) {} X {} id) ` carrier (homology_group p (subtopology X S)) + \ (hom_induced p (subtopology X S) {} X {} id) ` carrier ?G3" + proof + show "?h2 ` carrier ?G3 \ carrier ?G2" + by (simp add: hom_induced_reduced image_subset_iff) + show "?h2 ` carrier ?G3 \ ?h2 ` carrier (homology_group p (subtopology X S))" + by (meson carrier_reduced_homology_group_subset image_mono) + have "subgroup (kernel (homology_group p X) (homology_group p (discrete_topology {()})) + (hom_induced p X {} (discrete_topology {()}) {} (\x. ()))) + (homology_group p X)" + by (simp add: group.normal_invE(1) group_hom.normal_kernel group_hom_axioms_def group_hom_def hom_induced_empty_hom) + then show "carrier ?G2 \ kernel (homology_group p X) ?G1 ?h1 = kernel ?G2 ?G1 ?h1" + unfolding carrier_reduced_homology_group + by (auto simp: reduced_homology_group_def) + show "carrier ?G2 \ ?h2 ` carrier (homology_group p (subtopology X S)) + \ ?h2 ` carrier ?G3" + by (force simp: carrier_reduced_homology_group kernel_def hom_induced_compose') + qed + with homology_exactness_axiom_3 [of p X S] show ?thesis + by (fastforce simp add:) +qed + then show ?thesis + apply (simp add: group_hom_axioms_def group_hom_def hom_boundary_reduced_hom hom_induced_reduced_hom) + apply (simp add: group.hom_from_subgroup_generated hom_induced_hom reduced_homology_group_def) + done +qed + + +subsection\More homology properties of deformations, retracts, contractible spaces\ + +lemma iso_relative_homology_of_contractible: + "\contractible_space X; topspace X \ S \ {}\ + \ hom_boundary p X S + \ iso (relative_homology_group p X S) (reduced_homology_group(p - 1) (subtopology X S))" + using very_short_exact_sequence + [of "reduced_homology_group (p - 1) X" + "reduced_homology_group (p - 1) (subtopology X S)" + "relative_homology_group p X S" + "reduced_homology_group p X" + "hom_induced (p - 1) (subtopology X S) {} X {} id" + "hom_boundary p X S" + "hom_induced p X {} X S id"] + by (meson exact_seq_cons_iff homology_exactness_reduced_1 homology_exactness_reduced_2 trivial_reduced_homology_group_contractible_space) + +lemma isomorphic_group_relative_homology_of_contractible: + "\contractible_space X; topspace X \ S \ {}\ + \ relative_homology_group p X S \ + reduced_homology_group(p - 1) (subtopology X S)" + by (meson iso_relative_homology_of_contractible is_isoI) + +lemma isomorphic_group_reduced_homology_of_contractible: + "\contractible_space X; topspace X \ S \ {}\ + \ reduced_homology_group p (subtopology X S) \ relative_homology_group(p + 1) X S" + by (metis add.commute add_diff_cancel_left' group.iso_sym group_relative_homology_group isomorphic_group_relative_homology_of_contractible) + +lemma iso_reduced_homology_by_contractible: + "\contractible_space(subtopology X S); topspace X \ S \ {}\ + \ (hom_induced p X {} X S id) \ iso (reduced_homology_group p X) (relative_homology_group p X S)" + using very_short_exact_sequence + [of "reduced_homology_group (p - 1) (subtopology X S)" + "relative_homology_group p X S" + "reduced_homology_group p X" + "reduced_homology_group p (subtopology X S)" + "hom_boundary p X S" + "hom_induced p X {} X S id" + "hom_induced p (subtopology X S) {} X {} id"] + by (meson exact_seq_cons_iff homology_exactness_reduced_1 homology_exactness_reduced_3 trivial_reduced_homology_group_contractible_space) + +lemma isomorphic_reduced_homology_by_contractible: + "\contractible_space(subtopology X S); topspace X \ S \ {}\ + \ reduced_homology_group p X \ relative_homology_group p X S" + using is_isoI iso_reduced_homology_by_contractible by blast + +lemma isomorphic_relative_homology_by_contractible: + "\contractible_space(subtopology X S); topspace X \ S \ {}\ + \ relative_homology_group p X S \ reduced_homology_group p X" + using group.iso_sym group_reduced_homology_group isomorphic_reduced_homology_by_contractible by blast + +lemma isomorphic_reduced_homology_by_singleton: + "a \ topspace X \ reduced_homology_group p X \ relative_homology_group p X ({a})" + by (simp add: contractible_space_subtopology_singleton isomorphic_reduced_homology_by_contractible) + +lemma isomorphic_relative_homology_by_singleton: + "a \ topspace X \ relative_homology_group p X ({a}) \ reduced_homology_group p X" + by (simp add: group.iso_sym isomorphic_reduced_homology_by_singleton) + +lemma reduced_homology_group_pair: + assumes "t1_space X" and a: "a \ topspace X" and b: "b \ topspace X" and "a \ b" + shows "reduced_homology_group p (subtopology X {a,b}) \ homology_group p (subtopology X {a})" + (is "?lhs \ ?rhs") +proof - + have "?lhs \ relative_homology_group p (subtopology X {a,b}) {b}" + by (simp add: b isomorphic_reduced_homology_by_singleton topspace_subtopology) + also have "\ \ ?rhs" + proof - + have sub: "subtopology X {a, b} closure_of {b} \ subtopology X {a, b} interior_of {b}" + by (simp add: assms t1_space_subtopology closure_of_singleton subtopology_eq_discrete_topology_finite discrete_topology_closure_of) + show ?thesis + using homology_excision_axiom [OF sub, of "{a,b}" p] + by (simp add: assms(4) group.iso_sym is_isoI subtopology_subtopology) + qed + finally show ?thesis . +qed + + +lemma deformation_retraction_relative_homology_group_isomorphisms: + "\retraction_maps X Y r s; r ` U \ V; s ` V \ U; homotopic_with (\h. h ` U \ U) X X (s \ r) id\ + \ group_isomorphisms (relative_homology_group p X U) (relative_homology_group p Y V) + (hom_induced p X U Y V r) (hom_induced p Y V X U s)" + apply (simp add: retraction_maps_def) + apply (rule homotopy_equivalence_relative_homology_group_isomorphisms) + apply (auto simp: image_subset_iff continuous_map_compose homotopic_with_equal) + done + + +lemma deformation_retract_relative_homology_group_isomorphisms: + "\retraction_maps X Y r id; V \ U; r ` U \ V; homotopic_with (\h. h ` U \ U) X X r id\ + \ group_isomorphisms (relative_homology_group p X U) (relative_homology_group p Y V) + (hom_induced p X U Y V r) (hom_induced p Y V X U id)" + by (simp add: deformation_retraction_relative_homology_group_isomorphisms) + +lemma deformation_retract_relative_homology_group_isomorphism: + "\retraction_maps X Y r id; V \ U; r ` U \ V; homotopic_with (\h. h ` U \ U) X X r id\ + \ (hom_induced p X U Y V r) \ iso (relative_homology_group p X U) (relative_homology_group p Y V)" + by (metis deformation_retract_relative_homology_group_isomorphisms group_isomorphisms_imp_iso) + +lemma deformation_retract_relative_homology_group_isomorphism_id: + "\retraction_maps X Y r id; V \ U; r ` U \ V; homotopic_with (\h. h ` U \ U) X X r id\ + \ (hom_induced p Y V X U id) \ iso (relative_homology_group p Y V) (relative_homology_group p X U)" + by (metis deformation_retract_relative_homology_group_isomorphisms group_isomorphisms_imp_iso group_isomorphisms_sym) + +lemma deformation_retraction_imp_isomorphic_relative_homology_groups: + "\retraction_maps X Y r s; r ` U \ V; s ` V \ U; homotopic_with (\h. h ` U \ U) X X (s \ r) id\ + \ relative_homology_group p X U \ relative_homology_group p Y V" + by (blast intro: is_isoI group_isomorphisms_imp_iso deformation_retraction_relative_homology_group_isomorphisms) + +lemma deformation_retraction_imp_isomorphic_homology_groups: + "\retraction_maps X Y r s; homotopic_with (\h. True) X X (s \ r) id\ + \ homology_group p X \ homology_group p Y" + by (simp add: deformation_retraction_imp_homotopy_equivalent_space homotopy_equivalent_space_imp_isomorphic_homology_groups) + +lemma deformation_retract_imp_isomorphic_relative_homology_groups: + "\retraction_maps X X' r id; V \ U; r ` U \ V; homotopic_with (\h. h ` U \ U) X X r id\ + \ relative_homology_group p X U \ relative_homology_group p X' V" + by (simp add: deformation_retraction_imp_isomorphic_relative_homology_groups) + +lemma deformation_retract_imp_isomorphic_homology_groups: + "\retraction_maps X X' r id; homotopic_with (\h. True) X X r id\ + \ homology_group p X \ homology_group p X'" + by (simp add: deformation_retraction_imp_isomorphic_homology_groups) + + +lemma epi_hom_induced_inclusion: + assumes "homotopic_with (\x. True) X X id f" and "f ` (topspace X) \ S" + shows "(hom_induced p (subtopology X S) {} X {} id) + \ epi (homology_group p (subtopology X S)) (homology_group p X)" +proof (rule epi_right_invertible) + show "hom_induced p (subtopology X S) {} X {} id + \ hom (homology_group p (subtopology X S)) (homology_group p X)" + by (simp add: hom_induced_empty_hom) + show "hom_induced p X {} (subtopology X S) {} f + \ carrier (homology_group p X) \ carrier (homology_group p (subtopology X S))" + by (simp add: hom_induced_carrier) + fix x + assume "x \ carrier (homology_group p X)" + then show "hom_induced p (subtopology X S) {} X {} id (hom_induced p X {} (subtopology X S) {} f x) = x" + by (metis assms continuous_map_id_subt continuous_map_in_subtopology hom_induced_compose' hom_induced_id homology_homotopy_empty homotopic_with_imp_continuous_maps image_empty order_refl) +qed + + +lemma trivial_homomorphism_hom_induced_relativization: + assumes "homotopic_with (\x. True) X X id f" and "f ` (topspace X) \ S" + shows "trivial_homomorphism (homology_group p X) (relative_homology_group p X S) + (hom_induced p X {} X S id)" +proof - + have "(hom_induced p (subtopology X S) {} X {} id) + \ epi (homology_group p (subtopology X S)) (homology_group p X)" + by (metis assms epi_hom_induced_inclusion) + then show ?thesis + using homology_exactness_axiom_3 [of p X S] homology_exactness_axiom_1 [of p X S] + by (simp add: epi_def group.trivial_homomorphism_image group_hom.trivial_hom_iff) +qed + + +lemma mon_hom_boundary_inclusion: + assumes "homotopic_with (\x. True) X X id f" and "f ` (topspace X) \ S" + shows "(hom_boundary p X S) \ mon + (relative_homology_group p X S) (homology_group (p - 1) (subtopology X S))" +proof - + have "(hom_induced p (subtopology X S) {} X {} id) + \ epi (homology_group p (subtopology X S)) (homology_group p X)" + by (metis assms epi_hom_induced_inclusion) + then show ?thesis + using homology_exactness_axiom_3 [of p X S] homology_exactness_axiom_1 [of p X S] + apply (simp add: mon_def epi_def hom_boundary_hom) + by (metis (no_types, hide_lams) group_hom.trivial_hom_iff group_hom.trivial_ker_imp_inj group_hom_axioms_def group_hom_def group_relative_homology_group hom_boundary_hom) +qed + +lemma short_exact_sequence_hom_induced_relativization: + assumes "homotopic_with (\x. True) X X id f" and "f ` (topspace X) \ S" + shows "short_exact_sequence (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)" + unfolding short_exact_sequence_iff + by (intro conjI homology_exactness_axiom_2 epi_hom_induced_inclusion [OF assms] mon_hom_boundary_inclusion [OF assms]) + + +lemma group_isomorphisms_homology_group_prod_deformation: + fixes p::int + assumes "homotopic_with (\x. True) X X id f" and "f ` (topspace X) \ S" + obtains H K where + "subgroup H (homology_group p (subtopology X S))" + "subgroup K (homology_group p (subtopology X S))" + "(\(x, y). x \\<^bsub>homology_group p (subtopology X S)\<^esub> y) + \ Group.iso (subgroup_generated (homology_group p (subtopology X S)) H \\ + subgroup_generated (homology_group p (subtopology X S)) K) + (homology_group p (subtopology X S))" + "hom_boundary (p + 1) X S + \ Group.iso (relative_homology_group (p + 1) X S) + (subgroup_generated (homology_group p (subtopology X S)) H)" + "hom_induced p (subtopology X S) {} X {} id + \ Group.iso + (subgroup_generated (homology_group p (subtopology X S)) K) + (homology_group p X)" +proof - + let ?rhs = "relative_homology_group (p + 1) X S" + let ?pXS = "homology_group p (subtopology X S)" + let ?pX = "homology_group p X" + let ?hb = "hom_boundary (p + 1) X S" + let ?hi = "hom_induced p (subtopology X S) {} X {} id" + have x: "short_exact_sequence (?pX) ?pXS ?rhs ?hi ?hb" + using short_exact_sequence_hom_induced_relativization [OF assms, of "p + 1"] by simp + have contf: "continuous_map X (subtopology X S) f" + by (meson assms continuous_map_in_subtopology homotopic_with_imp_continuous_maps) + obtain H K where HK: "H \ ?pXS" "subgroup K ?pXS" "H \ K \ {one ?pXS}" "set_mult ?pXS H K = carrier ?pXS" + and iso: "?hb \ iso ?rhs (subgroup_generated ?pXS H)" "?hi \ iso (subgroup_generated ?pXS K) ?pX" + apply (rule splitting_lemma_right [OF x, where g' = "hom_induced p X {} (subtopology X S) {} f"]) + apply (simp add: hom_induced_empty_hom) + apply (simp add: contf hom_induced_compose') + apply (metis (full_types) assms(1) hom_induced_id homology_homotopy_empty) + apply blast + done + show ?thesis + proof + show "subgroup H ?pXS" + using HK(1) normal_imp_subgroup by blast + then show "(\(x, y). x \\<^bsub>?pXS\<^esub> y) + \ Group.iso (subgroup_generated (?pXS) H \\ subgroup_generated (?pXS) K) (?pXS)" + by (meson HK abelian_relative_homology_group group_disjoint_sum.iso_group_mul group_disjoint_sum_def group_relative_homology_group) + show "subgroup K ?pXS" + by (rule HK) + show "hom_boundary (p + 1) X S \ Group.iso ?rhs (subgroup_generated (?pXS) H)" + using iso int_ops(4) by presburger + show "hom_induced p (subtopology X S) {} X {} id \ Group.iso (subgroup_generated (?pXS) K) (?pX)" + by (simp add: iso(2)) + qed +qed + +lemma iso_homology_group_prod_deformation: + assumes "homotopic_with (\x. True) X X id f" and "f ` (topspace X) \ S" + shows "homology_group p (subtopology X S) + \ DirProd (homology_group p X) (relative_homology_group(p + 1) X S)" + (is "?G \ DirProd ?H ?R") +proof - + obtain H K where HK: + "(\(x, y). x \\<^bsub>?G\<^esub> y) + \ Group.iso (subgroup_generated (?G) H \\ subgroup_generated (?G) K) (?G)" + "hom_boundary (p + 1) X S \ Group.iso (?R) (subgroup_generated (?G) H)" + "hom_induced p (subtopology X S) {} X {} id \ Group.iso (subgroup_generated (?G) K) (?H)" + by (blast intro: group_isomorphisms_homology_group_prod_deformation [OF assms]) + have "?G \ DirProd (subgroup_generated (?G) H) (subgroup_generated (?G) K)" + by (meson DirProd_group HK(1) group.group_subgroup_generated group.iso_sym group_relative_homology_group is_isoI) + also have "\ \ DirProd ?R ?H" + by (meson HK group.DirProd_iso_trans group.group_subgroup_generated group.iso_sym group_relative_homology_group is_isoI) + also have "\ \ DirProd ?H ?R" + by (simp add: DirProd_commute_iso) + finally show ?thesis . +qed + + + +lemma iso_homology_contractible_space_subtopology1: + assumes "contractible_space X" "S \ topspace X" "S \ {}" + shows "homology_group 0 (subtopology X S) \ DirProd integer_group (relative_homology_group(1) X S)" +proof - + obtain f where "homotopic_with (\x. True) X X id f" and "f ` (topspace X) \ S" + using assms contractible_space_alt by fastforce + then have "homology_group 0 (subtopology X S) \ homology_group 0 X \\ relative_homology_group 1 X S" + using iso_homology_group_prod_deformation [of X _ S 0] by auto + also have "\ \ integer_group \\ relative_homology_group 1 X S" + using assms contractible_imp_path_connected_space group.DirProd_iso_trans group_relative_homology_group iso_refl isomorphic_integer_zeroth_homology_group by blast + finally show ?thesis . +qed + +lemma iso_homology_contractible_space_subtopology2: + "\contractible_space X; S \ topspace X; p \ 0; S \ {}\ + \ homology_group p (subtopology X S) \ relative_homology_group (p + 1) X S" + by (metis (no_types, hide_lams) add.commute isomorphic_group_reduced_homology_of_contractible topspace_subtopology topspace_subtopology_subset un_reduced_homology_group) + +lemma trivial_relative_homology_group_contractible_spaces: + "\contractible_space X; contractible_space(subtopology X S); topspace X \ S \ {}\ + \ trivial_group(relative_homology_group p X S)" + using group_reduced_homology_group group_relative_homology_group isomorphic_group_triviality isomorphic_relative_homology_by_contractible trivial_reduced_homology_group_contractible_space by blast + +lemma trivial_relative_homology_group_alt: + assumes contf: "continuous_map X (subtopology X S) f" and hom: "homotopic_with (\k. k ` S \ S) X X f id" + shows "trivial_group (relative_homology_group p X S)" +proof (rule trivial_relative_homology_group_gen [OF contf]) + show "homotopic_with (\h. True) (subtopology X S) (subtopology X S) f id" + using hom unfolding homotopic_with_def + apply (rule ex_forward) + apply (auto simp: prod_topology_subtopology continuous_map_in_subtopology continuous_map_from_subtopology image_subset_iff topspace_subtopology) + done + show "homotopic_with (\k. True) X X f id" + using assms by (force simp: homotopic_with_def) +qed + + +lemma iso_hom_induced_relativization_contractible: + assumes "contractible_space(subtopology X S)" "contractible_space(subtopology X T)" "T \ S" "topspace X \ T \ {}" + shows "(hom_induced p X T X S id) \ iso (relative_homology_group p X T) (relative_homology_group p X S)" +proof (rule very_short_exact_sequence) + show "exact_seq + ([relative_homology_group(p - 1) (subtopology X S) T, relative_homology_group p X S, relative_homology_group p X T, relative_homology_group p (subtopology X S) T], + [hom_relboundary p X S T, hom_induced p X T X S id, hom_induced p (subtopology X S) T X T id])" + using homology_exactness_triple_1 [OF \T \ S\] homology_exactness_triple_3 [OF \T \ S\] + by fastforce + show "trivial_group (relative_homology_group p (subtopology X S) T)" "trivial_group (relative_homology_group(p - 1) (subtopology X S) T)" + using assms + by (force simp: inf.absorb_iff2 subtopology_subtopology topspace_subtopology intro!: trivial_relative_homology_group_contractible_spaces)+ +qed + +corollary isomorphic_relative_homology_groups_relativization_contractible: + assumes "contractible_space(subtopology X S)" "contractible_space(subtopology X T)" "T \ S" "topspace X \ T \ {}" + shows "relative_homology_group p X T \ relative_homology_group p X S" + by (rule is_isoI) (rule iso_hom_induced_relativization_contractible [OF assms]) + +lemma iso_hom_induced_inclusion_contractible: + assumes "contractible_space X" "contractible_space(subtopology X S)" "T \ S" "topspace X \ S \ {}" + shows "(hom_induced p (subtopology X S) T X T id) + \ iso (relative_homology_group p (subtopology X S) T) (relative_homology_group p X T)" +proof (rule very_short_exact_sequence) + show "exact_seq + ([relative_homology_group p X S, relative_homology_group p X T, + relative_homology_group p (subtopology X S) T, relative_homology_group (p+1) X S], + [hom_induced p X T X S id, hom_induced p (subtopology X S) T X T id, hom_relboundary (p+1) X S T])" + using homology_exactness_triple_2 [OF \T \ S\] homology_exactness_triple_3 [OF \T \ S\] + by (metis add_diff_cancel_left' diff_add_cancel exact_seq_cons_iff) + show "trivial_group (relative_homology_group (p+1) X S)" "trivial_group (relative_homology_group p X S)" + using assms + by (auto simp: subtopology_subtopology topspace_subtopology intro!: trivial_relative_homology_group_contractible_spaces) +qed + +corollary isomorphic_relative_homology_groups_inclusion_contractible: + assumes "contractible_space X" "contractible_space(subtopology X S)" "T \ S" "topspace X \ S \ {}" + shows "relative_homology_group p (subtopology X S) T \ relative_homology_group p X T" + by (rule is_isoI) (rule iso_hom_induced_inclusion_contractible [OF assms]) + +lemma iso_hom_relboundary_contractible: + assumes "contractible_space X" "contractible_space(subtopology X T)" "T \ S" "topspace X \ T \ {}" + shows "hom_relboundary p X S T + \ iso (relative_homology_group p X S) (relative_homology_group (p - 1) (subtopology X S) T)" +proof (rule very_short_exact_sequence) + show "exact_seq + ([relative_homology_group (p - 1) X T, relative_homology_group (p - 1) (subtopology X S) T, relative_homology_group p X S, relative_homology_group p X T], + [hom_induced (p - 1) (subtopology X S) T X T id, hom_relboundary p X S T, hom_induced p X T X S id])" + using homology_exactness_triple_1 [OF \T \ S\] homology_exactness_triple_2 [OF \T \ S\] by simp + show "trivial_group (relative_homology_group p X T)" "trivial_group (relative_homology_group (p - 1) X T)" + using assms + by (auto simp: subtopology_subtopology topspace_subtopology intro!: trivial_relative_homology_group_contractible_spaces) +qed + +corollary isomorphic_relative_homology_groups_relboundary_contractible: + assumes "contractible_space X" "contractible_space(subtopology X T)" "T \ S" "topspace X \ T \ {}" + shows "relative_homology_group p X S \ relative_homology_group (p - 1) (subtopology X S) T" + by (rule is_isoI) (rule iso_hom_relboundary_contractible [OF assms]) + +lemma isomorphic_relative_contractible_space_imp_homology_groups: + assumes "contractible_space X" "contractible_space Y" "S \ topspace X" "T \ topspace Y" + and ST: "S = {} \ T = {}" + and iso: "\p. relative_homology_group p X S \ relative_homology_group p Y T" + shows "homology_group p (subtopology X S) \ homology_group p (subtopology Y T)" +proof (cases "T = {}") + case True + have "homology_group p (subtopology X {}) \ homology_group p (subtopology Y {})" + by (simp add: homeomorphic_empty_space_eq homeomorphic_space_imp_isomorphic_homology_groups) + then show ?thesis + using ST True by blast +next + case False + show ?thesis + proof (cases "p = 0") + case True + have "homology_group p (subtopology X S) \ integer_group \\ relative_homology_group 1 X S" + using assms True \T \ {}\ + by (simp add: iso_homology_contractible_space_subtopology1) + also have "\ \ integer_group \\ relative_homology_group 1 Y T" + by (simp add: assms group.DirProd_iso_trans iso_refl) + also have "\ \ homology_group p (subtopology Y T)" + by (simp add: True \T \ {}\ assms group.iso_sym iso_homology_contractible_space_subtopology1) + finally show ?thesis . + next + case False + have "homology_group p (subtopology X S) \ relative_homology_group (p+1) X S" + using assms False \T \ {}\ + by (simp add: iso_homology_contractible_space_subtopology2) + also have "\ \ relative_homology_group (p+1) Y T" + by (simp add: assms) + also have "\ \ homology_group p (subtopology Y T)" + by (simp add: False \T \ {}\ assms group.iso_sym iso_homology_contractible_space_subtopology2) + finally show ?thesis . + qed +qed + + +subsection\Homology groups of spheres\ + +lemma iso_reduced_homology_group_lower_hemisphere: + assumes "k \ n" + shows "hom_induced p (nsphere n) {} (nsphere n) {x. x k \ 0} id + \ iso (reduced_homology_group p (nsphere n)) (relative_homology_group p (nsphere n) {x. x k \ 0})" +proof (rule iso_reduced_homology_by_contractible) + show "contractible_space (subtopology (nsphere n) {x. x k \ 0})" + by (simp add: assms contractible_space_lower_hemisphere) + have "(\i. if i = k then -1 else 0) \ topspace (nsphere n) \ {x. x k \ 0}" + using assms by (simp add: nsphere if_distrib [of "\x. x ^ 2"] cong: if_cong) + then show "topspace (nsphere n) \ {x. x k \ 0} \ {}" + by blast +qed + + +lemma topspace_nsphere_1: + assumes "x \ topspace (nsphere n)" shows "(x k)\<^sup>2 \ 1" +proof (cases "k \ n") + case True + have "(\i \ {..n} - {k}. (x i)\<^sup>2) = (\i\n. (x i)\<^sup>2) - (x k)\<^sup>2" + using \k \ n\ by (simp add: sum_diff) + then show ?thesis + using assms + apply (simp add: nsphere) + by (metis diff_ge_0_iff_ge sum_nonneg zero_le_power2) +next + case False + then show ?thesis + using assms by (simp add: nsphere) +qed + +lemma topspace_nsphere_1_eq_0: + fixes x :: "nat \ real" + assumes x: "x \ topspace (nsphere n)" and xk: "(x k)\<^sup>2 = 1" and "i \ k" + shows "x i = 0" +proof (cases "i \ n") + case True + have "k \ n" + using x + by (simp add: nsphere) (metis not_less xk zero_neq_one zero_power2) + have "(\i \ {..n} - {k}. (x i)\<^sup>2) = (\i\n. (x i)\<^sup>2) - (x k)\<^sup>2" + using \k \ n\ by (simp add: sum_diff) + also have "\ = 0" + using assms by (simp add: nsphere) + finally have "\i\{..n} - {k}. (x i)\<^sup>2 = 0" + by (simp add: sum_nonneg_eq_0_iff) + then show ?thesis + using True \i \ k\ by auto +next + case False + with x show ?thesis + by (simp add: nsphere) +qed + + +proposition iso_relative_homology_group_upper_hemisphere: + "(hom_induced p (subtopology (nsphere n) {x. x k \ 0}) {x. x k = 0} (nsphere n) {x. x k \ 0} id) + \ iso (relative_homology_group p (subtopology (nsphere n) {x. x k \ 0}) {x. x k = 0}) + (relative_homology_group p (nsphere n) {x. x k \ 0})" (is "?h \ iso ?G ?H") +proof - + have "topspace (nsphere n) \ {x. x k < - 1 / 2} \ {x \ topspace (nsphere n). x k \ {y. y \ - 1 / 2}}" + by force + moreover have "closedin (nsphere n) {x \ topspace (nsphere n). x k \ {y. y \ - 1 / 2}}" + apply (rule closedin_continuous_map_preimage [OF continuous_map_nsphere_projection]) + using closed_Collect_le [of id "\x::real. -1/2"] apply simp + done + ultimately have "nsphere n closure_of {x. x k < -1/2} \ {x \ topspace (nsphere n). x k \ {y. y \ -1/2}}" + by (metis (no_types, lifting) closure_of_eq closure_of_mono closure_of_restrict) + also have "\ \ {x \ topspace (nsphere n). x k \ {y. y < 0}}" + by force + also have "\ \ nsphere n interior_of {x. x k \ 0}" + proof (rule interior_of_maximal) + show "{x \ topspace (nsphere n). x k \ {y. y < 0}} \ {x. x k \ 0}" + by force + show "openin (nsphere n) {x \ topspace (nsphere n). x k \ {y. y < 0}}" + apply (rule openin_continuous_map_preimage [OF continuous_map_nsphere_projection]) + using open_Collect_less [of id "\x::real. 0"] apply simp + done + qed + finally have nn: "nsphere n closure_of {x. x k < -1/2} \ nsphere n interior_of {x. x k \ 0}" . + have [simp]: "{x::nat\real. x k \ 0} - {x. x k < - (1/2)} = {x. -1/2 \ x k \ x k \ 0}" + "UNIV - {x::nat\real. x k < a} = {x. a \ x k}" for a + by auto + let ?T01 = "top_of_set {0..1::real}" + let ?X12 = "subtopology (nsphere n) {x. -1/2 \ x k}" + have 1: "hom_induced p ?X12 {x. -1/2 \ x k \ x k \ 0} (nsphere n) {x. x k \ 0} id + \ iso (relative_homology_group p ?X12 {x. -1/2 \ x k \ x k \ 0}) + ?H" + using homology_excision_axiom [OF nn subset_UNIV, of p] by simp + define h where "h \ \(T,x). let y = max (x k) (-T) in + (\i. if i = k then y else sqrt(1 - y ^ 2) / sqrt(1 - x k ^ 2) * x i)" + have h: "h(T,x) = x" if "0 \ T" "T \ 1" "(\i\n. (x i)\<^sup>2) = 1" and 0: "\i>n. x i = 0" "-T \ x k" for T x + using that by (force simp: nsphere h_def Let_def max_def intro!: topspace_nsphere_1_eq_0) + have "continuous_map (prod_topology ?T01 ?X12) euclideanreal (\x. h x i)" for i + proof - + show ?thesis + proof (rule continuous_map_eq) + show "continuous_map (prod_topology ?T01 ?X12) + euclideanreal (\(T, x). if 0 \ x k then x i else h (T, x) i)" + unfolding case_prod_unfold + proof (rule continuous_map_cases_le) + show "continuous_map (prod_topology ?T01 ?X12) euclideanreal (\x. snd x k)" + apply (subst continuous_map_of_snd [unfolded o_def]) + by (simp add: continuous_map_from_subtopology continuous_map_nsphere_projection) + next + show "continuous_map (subtopology (prod_topology ?T01 ?X12) {p \ topspace (prod_topology ?T01 ?X12). 0 \ snd p k}) + euclideanreal (\x. snd x i)" + apply (rule continuous_map_from_subtopology) + apply (subst continuous_map_of_snd [unfolded o_def]) + by (simp add: continuous_map_from_subtopology continuous_map_nsphere_projection) + next + note fst = continuous_map_into_fulltopology [OF continuous_map_subtopology_fst] + have snd: "continuous_map (subtopology (prod_topology ?T01 (subtopology (nsphere n) T)) S) euclideanreal (\x. snd x k)" for k S T + apply (simp add: nsphere) + apply (rule continuous_map_from_subtopology) + apply (subst continuous_map_of_snd [unfolded o_def]) + using continuous_map_from_subtopology continuous_map_nsphere_projection nsphere by fastforce + show "continuous_map (subtopology (prod_topology ?T01 ?X12) {p \ topspace (prod_topology ?T01 ?X12). snd p k \ 0}) + euclideanreal (\x. h (fst x, snd x) i)" + apply (simp add: h_def case_prod_unfold Let_def) + apply (intro conjI impI fst snd continuous_intros) + apply (auto simp: nsphere power2_eq_1_iff) + done + qed (auto simp: nsphere h) + qed (auto simp: nsphere h) + qed + moreover + have "h ` ({0..1} \ (topspace (nsphere n) \ {x. - (1/2) \ x k})) + \ {x. (\i\n. (x i)\<^sup>2) = 1 \ (\i>n. x i = 0)}" + proof - + have "(\i\n. (h (T,x) i)\<^sup>2) = 1" + if x: "x \ topspace (nsphere n)" and xk: "- (1/2) \ x k" and T: "0 \ T" "T \ 1" for T x + proof (cases "-T \ x k ") + case True + then show ?thesis + using that by (auto simp: nsphere h) + next + case False + with x \0 \ T\ have "k \ n" + apply (simp add: nsphere) + by (metis neg_le_0_iff_le not_le) + have "1 - (x k)\<^sup>2 \ 0" + using topspace_nsphere_1 x by auto + with False T \k \ n\ + have "(\i\n. (h (T,x) i)\<^sup>2) = T\<^sup>2 + (1 - T\<^sup>2) * (\i\{..n} - {k}. (x i)\<^sup>2 / (1 - (x k)\<^sup>2))" + unfolding h_def Let_def max_def + by (simp add: not_le square_le_1 power_mult_distrib power_divide if_distrib [of "\x. x ^ 2"] + sum.delta_remove sum_distrib_left) + also have "\ = 1" + using x False xk \0 \ T\ + by (simp add: nsphere sum_diff not_le \k \ n\ power2_eq_1_iff flip: sum_divide_distrib) + finally show ?thesis . + qed + moreover + have "h (T,x) i = 0" + if "x \ topspace (nsphere n)" "- (1/2) \ x k" and "n < i" "0 \ T" "T \ 1" + for T x i + proof (cases "-T \ x k ") + case False + then show ?thesis + using that by (auto simp: nsphere h_def Let_def not_le max_def) + qed (use that in \auto simp: nsphere h\) + ultimately show ?thesis + by auto + qed + ultimately + have cmh: "continuous_map (prod_topology ?T01 ?X12) (nsphere n) h" + by (subst (2) nsphere) (simp add: continuous_map_in_subtopology continuous_map_componentwise_UNIV) + have "hom_induced p (subtopology (nsphere n) {x. 0 \ x k}) + (topspace (subtopology (nsphere n) {x. 0 \ x k}) \ {x. x k = 0}) ?X12 + (topspace ?X12 \ {x. - 1/2 \ x k \ x k \ 0}) id + \ iso (relative_homology_group p (subtopology (nsphere n) {x. 0 \ x k}) + (topspace (subtopology (nsphere n) {x. 0 \ x k}) \ {x. x k = 0})) + (relative_homology_group p ?X12 (topspace ?X12 \ {x. - 1/2 \ x k \ x k \ 0}))" + proof (rule deformation_retract_relative_homology_group_isomorphism_id) + show "retraction_maps ?X12 (subtopology (nsphere n) {x. 0 \ x k}) (h \ (\x. (0,x))) id" + unfolding retraction_maps_def + proof (intro conjI ballI) + show "continuous_map ?X12 (subtopology (nsphere n) {x. 0 \ x k}) (h \ Pair 0)" + apply (simp add: continuous_map_in_subtopology) + apply (intro conjI continuous_map_compose [OF _ cmh] continuous_intros) + apply (auto simp: h_def Let_def) + done + show "continuous_map (subtopology (nsphere n) {x. 0 \ x k}) ?X12 id" + by (simp add: continuous_map_in_subtopology) (auto simp: nsphere) + qed (simp add: nsphere h) + next + have h0: "\xa. \xa \ topspace (nsphere n); - (1/2) \ xa k; xa k \ 0\ \ h (0, xa) k = 0" + by (simp add: h_def Let_def) + show "(h \ (\x. (0,x))) ` (topspace ?X12 \ {x. - 1 / 2 \ x k \ x k \ 0}) + \ topspace (subtopology (nsphere n) {x. 0 \ x k}) \ {x. x k = 0}" + apply (auto simp: h0) + apply (rule subsetD [OF continuous_map_image_subset_topspace [OF cmh]]) + apply (force simp: nsphere) + done + have hin: "\t x. \x \ topspace (nsphere n); - (1/2) \ x k; 0 \ t; t \ 1\ \ h (t,x) \ topspace (nsphere n)" + apply (rule subsetD [OF continuous_map_image_subset_topspace [OF cmh]]) + apply (force simp: nsphere) + done + have h1: "\x. \x \ topspace (nsphere n); - (1/2) \ x k\ \ h (1, x) = x" + by (simp add: h nsphere) + have "continuous_map (prod_topology ?T01 ?X12) (nsphere n) h" + using cmh by force + then show "homotopic_with + (\h. h ` (topspace ?X12 \ {x. - 1 / 2 \ x k \ x k \ 0}) \ topspace ?X12 \ {x. - 1 / 2 \ x k \ x k \ 0}) + ?X12 ?X12 (h \ (\x. (0,x))) id" + apply (subst homotopic_with, force) + apply (rule_tac x=h in exI) + apply (auto simp: hin h1 continuous_map_in_subtopology) + apply (auto simp: h_def Let_def max_def) + done + qed auto + then have 2: "hom_induced p (subtopology (nsphere n) {x. 0 \ x k}) {x. x k = 0} + ?X12 {x. - 1/2 \ x k \ x k \ 0} id + \ Group.iso + (relative_homology_group p (subtopology (nsphere n) {x. 0 \ x k}) {x. x k = 0}) + (relative_homology_group p ?X12 {x. - 1/2 \ x k \ x k \ 0})" + by (metis hom_induced_restrict relative_homology_group_restrict topspace_subtopology) + show ?thesis + using iso_set_trans [OF 2 1] + by (simp add: subset_iff continuous_map_in_subtopology flip: hom_induced_compose) +qed + + +corollary iso_upper_hemisphere_reduced_homology_group: + "(hom_boundary (1 + p) (subtopology (nsphere (Suc n)) {x. x(Suc n) \ 0}) {x. x(Suc n) = 0}) + \ iso (relative_homology_group (1 + p) (subtopology (nsphere (Suc n)) {x. x(Suc n) \ 0}) {x. x(Suc n) = 0}) + (reduced_homology_group p (nsphere n))" +proof - + have "{x. 0 \ x (Suc n)} \ {x. x (Suc n) = 0} = {x. x (Suc n) = (0::real)}" + by auto + then have n: "nsphere n = subtopology (subtopology (nsphere (Suc n)) {x. x(Suc n) \ 0}) {x. x(Suc n) = 0}" + by (simp add: subtopology_nsphere_equator subtopology_subtopology) + have ne: "(\i. if i = n then 1 else 0) \ topspace (subtopology (nsphere (Suc n)) {x. 0 \ x (Suc n)}) \ {x. x (Suc n) = 0}" + by (simp add: nsphere if_distrib [of "\x. x ^ 2"] cong: if_cong) + show ?thesis + unfolding n + apply (rule iso_relative_homology_of_contractible [where p = "1 + p", simplified]) + using contractible_space_upper_hemisphere ne apply blast+ + done +qed + +corollary iso_reduced_homology_group_upper_hemisphere: + assumes "k \ n" + shows "hom_induced p (nsphere n) {} (nsphere n) {x. x k \ 0} id + \ iso (reduced_homology_group p (nsphere n)) (relative_homology_group p (nsphere n) {x. x k \ 0})" +proof (rule iso_reduced_homology_by_contractible [OF contractible_space_upper_hemisphere [OF assms]]) + have "(\i. if i = k then 1 else 0) \ topspace (nsphere n) \ {x. 0 \ x k}" + using assms by (simp add: nsphere if_distrib [of "\x. x ^ 2"] cong: if_cong) + then show "topspace (nsphere n) \ {x. 0 \ x k} \ {}" + by blast +qed + + +lemma iso_relative_homology_group_lower_hemisphere: + "hom_induced p (subtopology (nsphere n) {x. x k \ 0}) {x. x k = 0} (nsphere n) {x. x k \ 0} id + \ iso (relative_homology_group p (subtopology (nsphere n) {x. x k \ 0}) {x. x k = 0}) + (relative_homology_group p (nsphere n) {x. x k \ 0})" (is "?k \ iso ?G ?H") +proof - + define r where "r \ \x i. if i = k then -x i else (x i::real)" + then have [simp]: "r \ r = id" + by force + have cmr: "continuous_map (subtopology (nsphere n) S) (nsphere n) r" for S + using continuous_map_nsphere_reflection [of n k] + by (simp add: continuous_map_from_subtopology r_def) + let ?f = "hom_induced p (subtopology (nsphere n) {x. x k \ 0}) {x. x k = 0} + (subtopology (nsphere n) {x. x k \ 0}) {x. x k = 0} r" + let ?g = "hom_induced p (subtopology (nsphere n) {x. x k \ 0}) {x. x k = 0} (nsphere n) {x. x k \ 0} id" + let ?h = "hom_induced p (nsphere n) {x. x k \ 0} (nsphere n) {x. x k \ 0} r" + obtain f h where + f: "f \ iso ?G (relative_homology_group p (subtopology (nsphere n) {x. x k \ 0}) {x. x k = 0})" + and h: "h \ iso (relative_homology_group p (nsphere n) {x. x k \ 0}) ?H" + and eq: "h \ ?g \ f = ?k" + proof + have hmr: "homeomorphic_map (nsphere n) (nsphere n) r" + unfolding homeomorphic_map_maps + by (metis \r \ r = id\ cmr homeomorphic_maps_involution pointfree_idE subtopology_topspace) + then have hmrs: "homeomorphic_map (subtopology (nsphere n) {x. x k \ 0}) (subtopology (nsphere n) {x. x k \ 0}) r" + by (simp add: homeomorphic_map_subtopologies_alt r_def) + have rimeq: "r ` (topspace (subtopology (nsphere n) {x. x k \ 0}) \ {x. x k = 0}) + = topspace (subtopology (nsphere n) {x. 0 \ x k}) \ {x. x k = 0}" + using continuous_map_eq_topcontinuous_at continuous_map_nsphere_reflection topcontinuous_at_atin + by (fastforce simp: r_def) + show "?f \ iso ?G (relative_homology_group p (subtopology (nsphere n) {x. x k \ 0}) {x. x k = 0})" + using homeomorphic_map_relative_homology_iso [OF hmrs Int_lower1 rimeq] + by (metis hom_induced_restrict relative_homology_group_restrict) + have rimeq: "r ` (topspace (nsphere n) \ {x. x k \ 0}) = topspace (nsphere n) \ {x. 0 \ x k}" + by (metis hmrs homeomorphic_imp_surjective_map topspace_subtopology) + show "?h \ Group.iso (relative_homology_group p (nsphere n) {x. x k \ 0}) ?H" + using homeomorphic_map_relative_homology_iso [OF hmr Int_lower1 rimeq] by simp + have [simp]: "\x. x k = 0 \ r x k = 0" + by (auto simp: r_def) + have "?h \ ?g \ ?f + = hom_induced p (subtopology (nsphere n) {x. 0 \ x k}) {x. x k = 0} (nsphere n) {x. 0 \ x k} r \ + hom_induced p (subtopology (nsphere n) {x. x k \ 0}) {x. x k = 0} (subtopology (nsphere n) {x. 0 \ x k}) {x. x k = 0} r" + apply (subst hom_induced_compose [symmetric]) + using continuous_map_nsphere_reflection apply (force simp: r_def)+ + done + also have "\ = ?k" + apply (subst hom_induced_compose [symmetric]) + apply (simp_all add: image_subset_iff cmr) + using hmrs homeomorphic_imp_continuous_map apply blast + done + finally show "?h \ ?g \ ?f = ?k" . + qed + with iso_relative_homology_group_upper_hemisphere [of p n k] + have "h \ hom_induced p (subtopology (nsphere n) {f. 0 \ f k}) {f. f k = 0} (nsphere n) {f. f k \ 0} id \ f + \ Group.iso ?G (relative_homology_group p (nsphere n) {f. 0 \ f k})" + using f h iso_set_trans by blast + then show ?thesis + by (simp add: eq) +qed + + +lemma iso_lower_hemisphere_reduced_homology_group: + "hom_boundary (1 + p) (subtopology (nsphere (Suc n)) {x. x(Suc n) \ 0}) {x. x(Suc n) = 0} + \ iso (relative_homology_group (1 + p) (subtopology (nsphere (Suc n)) {x. x(Suc n) \ 0}) + {x. x(Suc n) = 0}) + (reduced_homology_group p (nsphere n))" +proof - + have "{x. (\i\n. (x i)\<^sup>2) = 1 \ (\i>n. x i = 0)} = + ({x. (\i\n. (x i)\<^sup>2) + (x (Suc n))\<^sup>2 = 1 \ (\i>Suc n. x i = 0)} \ {x. x (Suc n) \ 0} \ + {x. x (Suc n) = (0::real)})" + by (force simp: dest: Suc_lessI) + then have n: "nsphere n = subtopology (subtopology (nsphere (Suc n)) {x. x(Suc n) \ 0}) {x. x(Suc n) = 0}" + by (simp add: nsphere subtopology_subtopology) + have ne: "(\i. if i = n then 1 else 0) \ topspace (subtopology (nsphere (Suc n)) {x. x (Suc n) \ 0}) \ {x. x (Suc n) = 0}" + by (simp add: nsphere if_distrib [of "\x. x ^ 2"] cong: if_cong) + show ?thesis + unfolding n + apply (rule iso_relative_homology_of_contractible [where p = "1 + p", simplified]) + using contractible_space_lower_hemisphere ne apply blast+ + done +qed + +lemma isomorphism_sym: + "\f \ iso G1 G2; \x. x \ carrier G1 \ r'(f x) = f(r x); + \x. x \ carrier G1 \ r x \ carrier G1; group G1; group G2\ + \ \f \ iso G2 G1. \x \ carrier G2. r(f x) = f(r' x)" + apply (clarsimp simp add: group.iso_iff_group_isomorphisms Bex_def) + by (metis (full_types) group_isomorphisms_def group_isomorphisms_sym hom_in_carrier) + +lemma isomorphism_trans: + "\\f \ iso G1 G2. \x \ carrier G1. r2(f x) = f(r1 x); \f \ iso G2 G3. \x \ carrier G2. r3(f x) = f(r2 x)\ + \ \f \ iso G1 G3. \x \ carrier G1. r3(f x) = f(r1 x)" + apply clarify + apply (rename_tac g f) + apply (rule_tac x="f \ g" in bexI) + apply (metis iso_iff comp_apply hom_in_carrier) + using iso_set_trans by blast + +lemma reduced_homology_group_nsphere_step: + "\f \ iso(reduced_homology_group p (nsphere n)) + (reduced_homology_group (1 + p) (nsphere (Suc n))). + \c \ carrier(reduced_homology_group p (nsphere n)). + hom_induced (1 + p) (nsphere(Suc n)) {} (nsphere(Suc n)) {} + (\x i. if i = 0 then -x i else x i) (f c) + = f (hom_induced p (nsphere n) {} (nsphere n) {} (\x i. if i = 0 then -x i else x i) c)" +proof - + define r where "r \ \x::nat\real. \i. if i = 0 then -x i else x i" + have cmr: "continuous_map (nsphere n) (nsphere n) r" for n + unfolding r_def by (rule continuous_map_nsphere_reflection) + have rsub: "r ` {x. 0 \ x (Suc n)} \ {x. 0 \ x (Suc n)}" "r ` {x. x (Suc n) \ 0} \ {x. x (Suc n) \ 0}" "r ` {x. x (Suc n) = 0} \ {x. x (Suc n) = 0}" + by (force simp: r_def)+ + let ?sub = "subtopology (nsphere (Suc n)) {x. x (Suc n) \ 0}" + let ?G2 = "relative_homology_group (1 + p) ?sub {x. x (Suc n) = 0}" + let ?r2 = "hom_induced (1 + p) ?sub {x. x (Suc n) = 0} ?sub {x. x (Suc n) = 0} r" + let ?j = "\p n. hom_induced p (nsphere n) {} (nsphere n) {} r" + show ?thesis + unfolding r_def [symmetric] + proof (rule isomorphism_trans) + let ?f = "hom_boundary (1 + p) ?sub {x. x (Suc n) = 0}" + show "\f\Group.iso (reduced_homology_group p (nsphere n)) ?G2. + \c\carrier (reduced_homology_group p (nsphere n)). ?r2 (f c) = f (?j p n c)" + proof (rule isomorphism_sym) + show "?f \ Group.iso ?G2 (reduced_homology_group p (nsphere n))" + using iso_upper_hemisphere_reduced_homology_group + by (metis add.commute) + next + fix c + assume "c \ carrier ?G2" + have cmrs: "continuous_map ?sub ?sub r" + by (metis (mono_tags, lifting) IntE cmr continuous_map_from_subtopology continuous_map_in_subtopology image_subset_iff rsub(1) topspace_subtopology) + have "hom_induced p (nsphere n) {} (nsphere n) {} r \ hom_boundary (1 + p) ?sub {x. x (Suc n) = 0} + = hom_boundary (1 + p) ?sub {x. x (Suc n) = 0} \ + hom_induced (1 + p) ?sub {x. x (Suc n) = 0} ?sub {x. x (Suc n) = 0} r" + using naturality_hom_induced [OF cmrs rsub(3), symmetric, of "1+p", simplified] + by (simp add: subtopology_subtopology subtopology_nsphere_equator flip: Collect_conj_eq cong: rev_conj_cong) + then show "?j p n (?f c) = ?f (hom_induced (1 + p) ?sub {x. x (Suc n) = 0} ?sub {x. x (Suc n) = 0} r c)" + by (metis comp_def) + next + fix c + assume "c \ carrier ?G2" + show "hom_induced (1 + p) ?sub {x. x (Suc n) = 0} ?sub {x. x (Suc n) = 0} r c \ carrier ?G2" + using hom_induced_carrier by blast + qed auto + next + let ?H2 = "relative_homology_group (1 + p) (nsphere (Suc n)) {x. x (Suc n) \ 0}" + let ?s2 = "hom_induced (1 + p) (nsphere (Suc n)) {x. x (Suc n) \ 0} (nsphere (Suc n)) {x. x (Suc n) \ 0} r" + show "\f\Group.iso ?G2 (reduced_homology_group (1 + p) (nsphere (Suc n))). \c\carrier ?G2. ?j (1 + p) (Suc n) (f c) + = f (?r2 c)" + proof (rule isomorphism_trans) + show "\f\Group.iso ?G2 ?H2. + \c\carrier ?G2. + ?s2 (f c) = f (hom_induced (1 + p) ?sub {x. x (Suc n) = 0} ?sub {x. x (Suc n) = 0} r c)" + proof (intro ballI bexI) + fix c + assume "c \ carrier (relative_homology_group (1 + p) ?sub {x. x (Suc n) = 0})" + show "?s2 (hom_induced (1 + p) ?sub {x. x (Suc n) = 0} (nsphere (Suc n)) {x. x (Suc n) \ 0} id c) + = hom_induced (1 + p) ?sub {x. x (Suc n) = 0} (nsphere (Suc n)) {x. x (Suc n) \ 0} id (?r2 c)" + apply (simp add: rsub hom_induced_compose' Collect_mono_iff cmr) + apply (subst hom_induced_compose') + apply (simp_all add: continuous_map_in_subtopology continuous_map_from_subtopology [OF cmr] rsub) + apply (auto simp: r_def) + done + qed (simp add: iso_relative_homology_group_upper_hemisphere) + next + let ?h = "hom_induced (1 + p) (nsphere(Suc n)) {} (nsphere (Suc n)) {x. x(Suc n) \ 0} id" + show "\f\Group.iso ?H2 (reduced_homology_group (1 + p) (nsphere (Suc n))). + \c\carrier ?H2. ?j (1 + p) (Suc n) (f c) = f (?s2 c)" + proof (rule isomorphism_sym) + show "?h \ Group.iso (reduced_homology_group (1 + p) (nsphere (Suc n))) + (relative_homology_group (1 + p) (nsphere (Suc n)) {x. x (Suc n) \ 0})" + using iso_reduced_homology_group_lower_hemisphere by blast + next + fix c + assume "c \ carrier (reduced_homology_group (1 + p) (nsphere (Suc n)))" + show "?s2 (?h c) = ?h (?j (1 + p) (Suc n) c)" + by (simp add: hom_induced_compose' cmr rsub) + next + fix c + assume "c \ carrier (reduced_homology_group (1 + p) (nsphere (Suc n)))" + then show "hom_induced (1 + p) (nsphere (Suc n)) {} (nsphere (Suc n)) {} r c + \ carrier (reduced_homology_group (1 + p) (nsphere (Suc n)))" + by (simp add: hom_induced_reduced) + qed auto + qed + qed +qed + + +lemma reduced_homology_group_nsphere_aux: + "if p = int n then reduced_homology_group n (nsphere n) \ integer_group + else trivial_group(reduced_homology_group p (nsphere n))" +proof (induction n arbitrary: p) + case 0 + let ?a = "\i::nat. if i = 0 then 1 else (0::real)" + let ?b = "\i::nat. if i = 0 then -1 else (0::real)" + have st: "subtopology (powertop_real UNIV) {?a, ?b} = nsphere 0" + proof - + have "{?a, ?b} = {x. (x 0)\<^sup>2 = 1 \ (\i>0. x i = 0)}" + using power2_eq_iff by fastforce + then show ?thesis + by (simp add: nsphere) + qed + have *: "reduced_homology_group p (subtopology (powertop_real UNIV) {?a, ?b}) \ + homology_group p (subtopology (powertop_real UNIV) {?a})" + apply (rule reduced_homology_group_pair) + apply (simp_all add: fun_eq_iff) + apply (simp add: open_fun_def separation_t1 t1_space_def) + done + have "reduced_homology_group 0 (nsphere 0) \ integer_group" if "p=0" + proof - + have "reduced_homology_group 0 (nsphere 0) \ homology_group 0 (top_of_set {?a})" if "p=0" + by (metis * euclidean_product_topology st that) + also have "\ \ integer_group" + by (simp add: homology_coefficients) + finally show ?thesis + using that by blast + qed + moreover have "trivial_group (reduced_homology_group p (nsphere 0))" if "p\0" + using * that homology_dimension_axiom [of "subtopology (powertop_real UNIV) {?a}" ?a p] + using isomorphic_group_triviality st by force + ultimately show ?case + by auto +next + case (Suc n) + have eq: "reduced_homology_group (int n) (nsphere n) \ integer_group" if "p-1 = n" + by (simp add: Suc.IH) + have neq: "trivial_group (reduced_homology_group (p-1) (nsphere n))" if "p-1 \ n" + by (simp add: Suc.IH that) + have iso: "reduced_homology_group p (nsphere (Suc n)) \ reduced_homology_group (p-1) (nsphere n)" + using reduced_homology_group_nsphere_step [of "p-1" n] group.iso_sym [OF _ is_isoI] group_reduced_homology_group + by fastforce + then show ?case + using eq iso_trans iso isomorphic_group_triviality neq + by (metis (no_types, hide_lams) add.commute add_left_cancel diff_add_cancel group_reduced_homology_group of_nat_Suc) +qed + + +lemma reduced_homology_group_nsphere: + "reduced_homology_group n (nsphere n) \ integer_group" + "p \ n \ trivial_group(reduced_homology_group p (nsphere n))" + using reduced_homology_group_nsphere_aux by auto + +lemma cyclic_reduced_homology_group_nsphere: + "cyclic_group(reduced_homology_group p (nsphere n))" + by (metis reduced_homology_group_nsphere trivial_imp_cyclic_group cyclic_integer_group + group_integer_group group_reduced_homology_group isomorphic_group_cyclicity) + +lemma trivial_reduced_homology_group_nsphere: + "trivial_group(reduced_homology_group p (nsphere n)) \ (p \ n)" + using group_integer_group isomorphic_group_triviality nontrivial_integer_group reduced_homology_group_nsphere(1) reduced_homology_group_nsphere(2) trivial_group_def by blast + +lemma non_contractible_space_nsphere: "\ (contractible_space(nsphere n))" + proof (clarsimp simp add: contractible_eq_homotopy_equivalent_singleton_subtopology) + fix a :: "nat \ real" + assume a: "a \ topspace (nsphere n)" + and he: "nsphere n homotopy_equivalent_space subtopology (nsphere n) {a}" + have "trivial_group (reduced_homology_group (int n) (subtopology (nsphere n) {a}))" + by (simp add: a homology_dimension_reduced [where a=a]) + then show "False" + using isomorphic_group_triviality [OF homotopy_equivalent_space_imp_isomorphic_reduced_homology_groups [OF he, of n]] + by (simp add: trivial_reduced_homology_group_nsphere) +qed + + +subsection\Brouwer degree of a Map\ + +definition Brouwer_degree2 :: "nat \ ((nat \ real) \ nat \ real) \ int" + where + "Brouwer_degree2 p f \ + @d::int. \x \ carrier(reduced_homology_group p (nsphere p)). + hom_induced p (nsphere p) {} (nsphere p) {} f x = pow (reduced_homology_group p (nsphere p)) x d" + +lemma Brouwer_degree2_eq: + "(\x. x \ topspace(nsphere p) \ f x = g x) \ Brouwer_degree2 p f = Brouwer_degree2 p g" + unfolding Brouwer_degree2_def Ball_def + apply (intro Eps_cong all_cong) + by (metis (mono_tags, lifting) hom_induced_eq) + +lemma Brouwer_degree2: + assumes "x \ carrier(reduced_homology_group p (nsphere p))" + shows "hom_induced p (nsphere p) {} (nsphere p) {} f x + = pow (reduced_homology_group p (nsphere p)) x (Brouwer_degree2 p f)" + (is "?h x = pow ?G x _") +proof (cases "continuous_map(nsphere p) (nsphere p) f") + case True + interpret group ?G + by simp + interpret group_hom ?G ?G ?h + using hom_induced_reduced_hom group_hom_axioms_def group_hom_def is_group by blast + obtain a where a: "a \ carrier ?G" + and aeq: "subgroup_generated ?G {a} = ?G" + using cyclic_reduced_homology_group_nsphere [of p p] by (auto simp: cyclic_group_def) + then have carra: "carrier (subgroup_generated ?G {a}) = range (\n::int. pow ?G a n)" + using carrier_subgroup_generated_by_singleton by blast + moreover have "?h a \ carrier (subgroup_generated ?G {a})" + by (simp add: a aeq hom_induced_reduced) + ultimately obtain d::int where d: "?h a = pow ?G a d" + by auto + have *: "hom_induced (int p) (nsphere p) {} (nsphere p) {} f x = x [^]\<^bsub>?G\<^esub> d" + if x: "x \ carrier ?G" for x + proof - + obtain n::int where xeq: "x = pow ?G a n" + using carra x aeq by moura + show ?thesis + by (simp add: xeq a d hom_int_pow int_pow_pow mult.commute) + qed + show ?thesis + unfolding Brouwer_degree2_def + apply (rule someI2 [where a=d]) + using assms * apply blast+ + done +next + case False + show ?thesis + unfolding Brouwer_degree2_def + by (rule someI2 [where a=0]) (simp_all add: hom_induced_default False one_reduced_homology_group assms) +qed + + + +lemma Brouwer_degree2_iff: + assumes f: "continuous_map (nsphere p) (nsphere p) f" + and x: "x \ carrier(reduced_homology_group p (nsphere p))" + shows "(hom_induced (int p) (nsphere p) {} (nsphere p) {} f x = + x [^]\<^bsub>reduced_homology_group (int p) (nsphere p)\<^esub> d) + \ (x = \\<^bsub>reduced_homology_group (int p) (nsphere p)\<^esub> \ Brouwer_degree2 p f = d)" + (is "(?h x = x [^]\<^bsub>?G\<^esub> d) \ _") +proof - + interpret group "?G" + by simp + obtain a where a: "a \ carrier ?G" + and aeq: "subgroup_generated ?G {a} = ?G" + using cyclic_reduced_homology_group_nsphere [of p p] by (auto simp: cyclic_group_def) + then obtain i::int where i: "x = (a [^]\<^bsub>?G\<^esub> i)" + using carrier_subgroup_generated_by_singleton x by fastforce + then have "a [^]\<^bsub>?G\<^esub> i \ carrier ?G" + using x by blast + have [simp]: "ord a = 0" + by (simp add: a aeq iso_finite [OF reduced_homology_group_nsphere(1)] flip: infinite_cyclic_subgroup_order) + show ?thesis + by (auto simp: Brouwer_degree2 int_pow_eq_id x i a int_pow_pow int_pow_eq) +qed + + +lemma Brouwer_degree2_unique: + assumes f: "continuous_map (nsphere p) (nsphere p) f" + and hi: "\x. x \ carrier(reduced_homology_group p (nsphere p)) + \ hom_induced p (nsphere p) {} (nsphere p) {} f x = pow (reduced_homology_group p (nsphere p)) x d" + (is "\x. x \ carrier ?G \ ?h x = _") + shows "Brouwer_degree2 p f = d" +proof - + obtain a where a: "a \ carrier ?G" + and aeq: "subgroup_generated ?G {a} = ?G" + using cyclic_reduced_homology_group_nsphere [of p p] by (auto simp: cyclic_group_def) + show ?thesis + using hi [OF a] + apply (simp add: Brouwer_degree2 a) + by (metis Brouwer_degree2_iff a aeq f group.trivial_group_subgroup_generated group_reduced_homology_group subsetI trivial_reduced_homology_group_nsphere) +qed + +lemma Brouwer_degree2_unique_generator: + assumes f: "continuous_map (nsphere p) (nsphere p) f" + and eq: "subgroup_generated (reduced_homology_group p (nsphere p)) {a} + = reduced_homology_group p (nsphere p)" + and hi: "hom_induced p (nsphere p) {} (nsphere p) {} f a = pow (reduced_homology_group p (nsphere p)) a d" + (is "?h a = pow ?G a _") + shows "Brouwer_degree2 p f = d" +proof (cases "a \ carrier ?G") + case True + then show ?thesis + by (metis Brouwer_degree2_iff hi eq f group.trivial_group_subgroup_generated group_reduced_homology_group + subset_singleton_iff trivial_reduced_homology_group_nsphere) +next + case False + then show ?thesis + using trivial_reduced_homology_group_nsphere [of p p] + by (metis group.trivial_group_subgroup_generated_eq disjoint_insert(1) eq group_reduced_homology_group inf_bot_right subset_singleton_iff) +qed + +lemma Brouwer_degree2_homotopic: + assumes "homotopic_with (\x. True) (nsphere p) (nsphere p) f g" + shows "Brouwer_degree2 p f = Brouwer_degree2 p g" +proof - + have "continuous_map (nsphere p) (nsphere p) f" + using homotopic_with_imp_continuous_maps [OF assms] by auto + show ?thesis + using Brouwer_degree2_def assms homology_homotopy_empty by fastforce +qed + +lemma Brouwer_degree2_id [simp]: "Brouwer_degree2 p id = 1" +proof (rule Brouwer_degree2_unique) + fix x + assume x: "x \ carrier (reduced_homology_group (int p) (nsphere p))" + then have "x \ carrier (homology_group (int p) (nsphere p))" + using carrier_reduced_homology_group_subset by blast + then show "hom_induced (int p) (nsphere p) {} (nsphere p) {} id x = + x [^]\<^bsub>reduced_homology_group (int p) (nsphere p)\<^esub> (1::int)" + by (simp add: hom_induced_id group.int_pow_1 x) +qed auto + +lemma Brouwer_degree2_compose: + assumes f: "continuous_map (nsphere p) (nsphere p) f" and g: "continuous_map (nsphere p) (nsphere p) g" + shows "Brouwer_degree2 p (g \ f) = Brouwer_degree2 p g * Brouwer_degree2 p f" +proof (rule Brouwer_degree2_unique) + show "continuous_map (nsphere p) (nsphere p) (g \ f)" + by (meson continuous_map_compose f g) +next + fix x + assume x: "x \ carrier (reduced_homology_group (int p) (nsphere p))" + have "hom_induced (int p) (nsphere p) {} (nsphere p) {} (g \ f) = + hom_induced (int p) (nsphere p) {} (nsphere p) {} g \ + hom_induced (int p) (nsphere p) {} (nsphere p) {} f" + by (blast intro: hom_induced_compose [OF f _ g]) + with x show "hom_induced (int p) (nsphere p) {} (nsphere p) {} (g \ f) x = + x [^]\<^bsub>reduced_homology_group (int p) (nsphere p)\<^esub> (Brouwer_degree2 p g * Brouwer_degree2 p f)" + by (simp add: mult.commute hom_induced_reduced flip: Brouwer_degree2 group.int_pow_pow) +qed + +lemma Brouwer_degree2_homotopy_equivalence: + assumes f: "continuous_map (nsphere p) (nsphere p) f" and g: "continuous_map (nsphere p) (nsphere p) g" + and hom: "homotopic_with (\x. True) (nsphere p) (nsphere p) (f \ g) id" + obtains "\Brouwer_degree2 p f\ = 1" "\Brouwer_degree2 p g\ = 1" "Brouwer_degree2 p g = Brouwer_degree2 p f" + using Brouwer_degree2_homotopic [OF hom] Brouwer_degree2_compose f g zmult_eq_1_iff by auto + +lemma Brouwer_degree2_homeomorphic_maps: + assumes "homeomorphic_maps (nsphere p) (nsphere p) f g" + obtains "\Brouwer_degree2 p f\ = 1" "\Brouwer_degree2 p g\ = 1" "Brouwer_degree2 p g = Brouwer_degree2 p f" + using assms + by (auto simp: homeomorphic_maps_def homotopic_with_equal continuous_map_compose intro: Brouwer_degree2_homotopy_equivalence) + + +lemma Brouwer_degree2_retraction_map: + assumes "retraction_map (nsphere p) (nsphere p) f" + shows "\Brouwer_degree2 p f\ = 1" +proof - + obtain g where g: "retraction_maps (nsphere p) (nsphere p) f g" + using assms by (auto simp: retraction_map_def) + show ?thesis + proof (rule Brouwer_degree2_homotopy_equivalence) + show "homotopic_with (\x. True) (nsphere p) (nsphere p) (f \ g) id" + using g apply (auto simp: retraction_maps_def) + by (simp add: homotopic_with_equal continuous_map_compose) + show "continuous_map (nsphere p) (nsphere p) f" "continuous_map (nsphere p) (nsphere p) g" + using g retraction_maps_def by blast+ + qed +qed + +lemma Brouwer_degree2_section_map: + assumes "section_map (nsphere p) (nsphere p) f" + shows "\Brouwer_degree2 p f\ = 1" +proof - + obtain g where g: "retraction_maps (nsphere p) (nsphere p) g f" + using assms by (auto simp: section_map_def) + show ?thesis + proof (rule Brouwer_degree2_homotopy_equivalence) + show "homotopic_with (\x. True) (nsphere p) (nsphere p) (g \ f) id" + using g apply (auto simp: retraction_maps_def) + by (simp add: homotopic_with_equal continuous_map_compose) + show "continuous_map (nsphere p) (nsphere p) g" "continuous_map (nsphere p) (nsphere p) f" + using g retraction_maps_def by blast+ + qed +qed + +lemma Brouwer_degree2_homeomorphic_map: + "homeomorphic_map (nsphere p) (nsphere p) f \ \Brouwer_degree2 p f\ = 1" + using Brouwer_degree2_retraction_map section_and_retraction_eq_homeomorphic_map by blast + + +lemma Brouwer_degree2_nullhomotopic: + assumes "homotopic_with (\x. True) (nsphere p) (nsphere p) f (\x. a)" + shows "Brouwer_degree2 p f = 0" +proof - + have contf: "continuous_map (nsphere p) (nsphere p) f" + and contc: "continuous_map (nsphere p) (nsphere p) (\x. a)" + using homotopic_with_imp_continuous_maps [OF assms] by metis+ + have "Brouwer_degree2 p f = Brouwer_degree2 p (\x. a)" + using Brouwer_degree2_homotopic [OF assms] . + moreover + let ?G = "reduced_homology_group (int p) (nsphere p)" + interpret group ?G + by simp + have "Brouwer_degree2 p (\x. a) = 0" + proof (rule Brouwer_degree2_unique [OF contc]) + fix c + assume c: "c \ carrier ?G" + have "continuous_map (nsphere p) (subtopology (nsphere p) {a}) (\f. a)" + using contc continuous_map_in_subtopology by blast + then have he: "hom_induced p (nsphere p) {} (nsphere p) {} (\x. a) + = hom_induced p (subtopology (nsphere p) {a}) {} (nsphere p) {} id \ + hom_induced p (nsphere p) {} (subtopology (nsphere p) {a}) {} (\x. a)" + by (metis continuous_map_id_subt hom_induced_compose id_comp image_empty order_refl) + have 1: "hom_induced p (nsphere p) {} (subtopology (nsphere p) {a}) {} (\x. a) c = + \\<^bsub>reduced_homology_group (int p) (subtopology (nsphere p) {a})\<^esub>" + using c trivial_reduced_homology_group_contractible_space [of "subtopology (nsphere p) {a}" p] + by (simp add: hom_induced_reduced contractible_space_subtopology_singleton trivial_group_subset group.trivial_group_subset subset_iff) + show "hom_induced (int p) (nsphere p) {} (nsphere p) {} (\x. a) c = + c [^]\<^bsub>?G\<^esub> (0::int)" + apply (simp add: he 1) + using hom_induced_reduced_hom group_hom.hom_one group_hom_axioms_def group_hom_def group_reduced_homology_group by blast + qed + ultimately show ?thesis + by metis +qed + + +lemma Brouwer_degree2_const: "Brouwer_degree2 p (\x. a) = 0" +proof (cases "continuous_map(nsphere p) (nsphere p) (\x. a)") + case True + then show ?thesis + by (auto intro: Brouwer_degree2_nullhomotopic [where a=a]) +next + case False + let ?G = "reduced_homology_group (int p) (nsphere p)" + let ?H = "homology_group (int p) (nsphere p)" + interpret group ?G + by simp + have eq1: "\\<^bsub>?H\<^esub> = \\<^bsub>?G\<^esub>" + by (simp add: one_reduced_homology_group) + have *: "\x\carrier ?G. hom_induced (int p) (nsphere p) {} (nsphere p) {} (\x. a) x = \\<^bsub>?H\<^esub>" + by (metis False hom_induced_default one_relative_homology_group) + obtain c where c: "c \ carrier ?G" and ceq: "subgroup_generated ?G {c} = ?G" + using cyclic_reduced_homology_group_nsphere [of p p] by (force simp: cyclic_group_def) + have [simp]: "ord c = 0" + by (simp add: c ceq iso_finite [OF reduced_homology_group_nsphere(1)] flip: infinite_cyclic_subgroup_order) + show ?thesis + unfolding Brouwer_degree2_def + proof (rule some_equality) + fix d :: "int" + assume "\x\carrier ?G. hom_induced (int p) (nsphere p) {} (nsphere p) {} (\x. a) x = x [^]\<^bsub>?G\<^esub> d" + then have "c [^]\<^bsub>?G\<^esub> d = \\<^bsub>?H\<^esub>" + using "*" c by blast + then have "int (ord c) dvd d" + using c eq1 int_pow_eq_id by auto + then show "d = 0" + by (simp add: * del: one_relative_homology_group) + qed (use "*" eq1 in force) +qed + + +corollary Brouwer_degree2_nonsurjective: + "\continuous_map(nsphere p) (nsphere p) f; f ` topspace (nsphere p) \ topspace (nsphere p)\ + \ Brouwer_degree2 p f = 0" + by (meson Brouwer_degree2_nullhomotopic nullhomotopic_nonsurjective_sphere_map) + + +proposition Brouwer_degree2_reflection: + "Brouwer_degree2 p (\x i. if i = 0 then -x i else x i) = -1" (is "Brouwer_degree2 _ ?r = -1") +proof (induction p) + case 0 + let ?G = "homology_group 0 (nsphere 0)" + let ?D = "homology_group 0 (discrete_topology {()})" + interpret group ?G + by simp + define r where "r \ \x::nat\real. \i. if i = 0 then -x i else x i" + then have [simp]: "r \ r = id" + by force + have cmr: "continuous_map (nsphere 0) (nsphere 0) r" + by (simp add: r_def continuous_map_nsphere_reflection) + have *: "hom_induced 0 (nsphere 0) {} (nsphere 0) {} r c = inv\<^bsub>?G\<^esub> c" + if "c \ carrier(reduced_homology_group 0 (nsphere 0))" for c + proof - + have c: "c \ carrier ?G" + and ceq: "hom_induced 0 (nsphere 0) {} (discrete_topology {()}) {} (\x. ()) c = \\<^bsub>?D\<^esub>" + using that by (auto simp: carrier_reduced_homology_group kernel_def) + define pp::"nat\real" where "pp \ \i. if i = 0 then 1 else 0" + define nn::"nat\real" where "nn \ \i. if i = 0 then -1 else 0" + have topn0: "topspace(nsphere 0) = {pp,nn}" + by (auto simp: nsphere pp_def nn_def fun_eq_iff power2_eq_1_iff split: if_split_asm) + have "t1_space (nsphere 0)" + unfolding nsphere + apply (rule t1_space_subtopology) + by (metis (full_types) open_fun_def t1_space t1_space_def) + then have dtn0: "discrete_topology {pp,nn} = nsphere 0" + using finite_t1_space_imp_discrete_topology [OF topn0] by auto + have "pp \ nn" + by (auto simp: pp_def nn_def fun_eq_iff) + have [simp]: "r pp = nn" "r nn = pp" + by (auto simp: r_def pp_def nn_def fun_eq_iff) + have iso: "(\(a,b). hom_induced 0 (subtopology (nsphere 0) {pp}) {} (nsphere 0) {} id a + \\<^bsub>?G\<^esub> hom_induced 0 (subtopology (nsphere 0) {nn}) {} (nsphere 0) {} id b) + \ iso (homology_group 0 (subtopology (nsphere 0) {pp}) \\ homology_group 0 (subtopology (nsphere 0) {nn})) + ?G" (is "?f \ iso (?P \\ ?N) ?G") + apply (rule homology_additivity_explicit) + using dtn0 \pp \ nn\ by (auto simp: discrete_topology_unique) + then have fim: "?f ` carrier(?P \\ ?N) = carrier ?G" + by (simp add: iso_def bij_betw_def) + obtain d d' where d: "d \ carrier ?P" and d': "d' \ carrier ?N" and eqc: "?f(d,d') = c" + using c by (force simp flip: fim) + let ?h = "\xx. hom_induced 0 (subtopology (nsphere 0) {xx}) {} (discrete_topology {()}) {} (\x. ())" + have "retraction_map (subtopology (nsphere 0) {pp}) (subtopology (nsphere 0) {nn}) r" + apply (simp add: retraction_map_def retraction_maps_def continuous_map_in_subtopology continuous_map_from_subtopology cmr image_subset_iff) + apply (rule_tac x=r in exI) + apply (force simp: retraction_map_def retraction_maps_def continuous_map_in_subtopology continuous_map_from_subtopology cmr) + done + then have "carrier ?N = (hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere 0) {nn}) {} r) ` carrier ?P" + by (rule surj_hom_induced_retraction_map) + then obtain e where e: "e \ carrier ?P" and eqd': "hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere 0) {nn}) {} r e = d'" + using d' by auto + have "section_map (subtopology (nsphere 0) {pp}) (discrete_topology {()}) (\x. ())" + by (force simp: section_map_def retraction_maps_def topn0) + then have "?h pp \ mon ?P ?D" + by (rule mon_hom_induced_section_map) + then have one: "x = one ?P" + if "?h pp x = \\<^bsub>?D\<^esub>" "x \ carrier ?P" for x + using that by (simp add: mon_iff_hom_one) + interpret hpd: group_hom ?P ?D "?h pp" + using hom_induced_empty_hom by (simp add: hom_induced_empty_hom group_hom_axioms_def group_hom_def) + interpret hgd: group_hom ?G ?D "hom_induced 0 (nsphere 0) {} (discrete_topology {()}) {} (\x. ())" + using hom_induced_empty_hom by (simp add: hom_induced_empty_hom group_hom_axioms_def group_hom_def) + interpret hpg: group_hom ?P ?G "hom_induced 0 (subtopology (nsphere 0) {pp}) {} (nsphere 0) {} r" + using hom_induced_empty_hom by (simp add: hom_induced_empty_hom group_hom_axioms_def group_hom_def) + interpret hgg: group_hom ?G ?G "hom_induced 0 (nsphere 0) {} (nsphere 0) {} r" + using hom_induced_empty_hom by (simp add: hom_induced_empty_hom group_hom_axioms_def group_hom_def) + have "?h pp d = + (hom_induced 0 (nsphere 0) {} (discrete_topology {()}) {} (\x. ()) + \ hom_induced 0 (subtopology (nsphere 0) {pp}) {} (nsphere 0) {} id) d" + by (simp flip: hom_induced_compose_empty) + moreover + have "?h pp = ?h nn \ hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere 0) {nn}) {} r" + by (simp add: cmr continuous_map_from_subtopology continuous_map_in_subtopology image_subset_iff flip: hom_induced_compose_empty) + then have "?h pp e = + (hom_induced 0 (nsphere 0) {} (discrete_topology {()}) {} (\x. ()) + \ hom_induced 0 (subtopology (nsphere 0) {nn}) {} (nsphere 0) {} id) d'" + by (simp flip: hom_induced_compose_empty eqd') + ultimately have "?h pp (d \\<^bsub>?P\<^esub> e) = hom_induced 0 (nsphere 0) {} (discrete_topology {()}) {} (\x. ()) (?f(d,d'))" + by (simp add: d e hom_induced_carrier) + then have "?h pp (d \\<^bsub>?P\<^esub> e) = \\<^bsub>?D\<^esub>" + using ceq eqc by simp + then have inv_p: "inv\<^bsub>?P\<^esub> d = e" + by (metis (no_types, lifting) Group.group_def d e group.inv_equality group.r_inv group_relative_homology_group one monoid.m_closed) + have cmr_pn: "continuous_map (subtopology (nsphere 0) {pp}) (subtopology (nsphere 0) {nn}) r" + by (simp add: cmr continuous_map_from_subtopology continuous_map_in_subtopology image_subset_iff) + then have "hom_induced 0 (subtopology (nsphere 0) {pp}) {} (nsphere 0) {} (id \ r) = + hom_induced 0 (subtopology (nsphere 0) {nn}) {} (nsphere 0) {} id \ + hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere 0) {nn}) {} r" + using hom_induced_compose_empty continuous_map_id_subt by blast + then have "inv\<^bsub>?G\<^esub> hom_induced 0 (subtopology (nsphere 0) {pp}) {} (nsphere 0) {} r d = + hom_induced 0 (subtopology (nsphere 0) {nn}) {} (nsphere 0) {} id d'" + apply (simp add: flip: inv_p eqd') + using d hpg.hom_inv by auto + then have c: "c = (hom_induced 0 (subtopology (nsphere 0) {pp}) {} (nsphere 0) {} id d) + \\<^bsub>?G\<^esub> inv\<^bsub>?G\<^esub> (hom_induced 0 (subtopology (nsphere 0) {pp}) {} (nsphere 0) {} r d)" + by (simp flip: eqc) + have "hom_induced 0 (nsphere 0) {} (nsphere 0) {} r \ + hom_induced 0 (subtopology (nsphere 0) {pp}) {} (nsphere 0) {} id = + hom_induced 0 (subtopology (nsphere 0) {pp}) {} (nsphere 0) {} r" + by (metis cmr comp_id continuous_map_id_subt hom_induced_compose_empty) + moreover + have "hom_induced 0 (nsphere 0) {} (nsphere 0) {} r \ + hom_induced 0 (subtopology (nsphere 0) {pp}) {} (nsphere 0) {} r = + hom_induced 0 (subtopology (nsphere 0) {pp}) {} (nsphere 0) {} id" + by (metis \r \ r = id\ cmr continuous_map_from_subtopology hom_induced_compose_empty) + ultimately show ?thesis + by (metis inv_p c comp_def d e hgg.hom_inv hgg.hom_mult hom_induced_carrier hpd.G.inv_inv hpg.hom_inv inv_mult_group) + qed + show ?case + unfolding r_def [symmetric] + using Brouwer_degree2_unique [OF cmr] + by (auto simp: * group.int_pow_neg group.int_pow_1 reduced_homology_group_def intro!: Brouwer_degree2_unique [OF cmr]) +next + case (Suc p) + let ?G = "reduced_homology_group (int p) (nsphere p)" + let ?G1 = "reduced_homology_group (1 + int p) (nsphere (Suc p))" + obtain f g where fg: "group_isomorphisms ?G ?G1 f g" + and *: "\c\carrier ?G. + hom_induced (1 + int p) (nsphere (Suc p)) {} (nsphere (Suc p)) {} ?r (f c) = + f (hom_induced p (nsphere p) {} (nsphere p) {} ?r c)" + using reduced_homology_group_nsphere_step + by (meson group.iso_iff_group_isomorphisms group_reduced_homology_group) + then have eq: "carrier ?G1 = f ` carrier ?G" + by (fastforce simp add: iso_iff dest: group_isomorphisms_imp_iso) + interpret group_hom ?G ?G1 f + by (meson fg group_hom_axioms_def group_hom_def group_isomorphisms_def group_reduced_homology_group) + have homf: "f \ hom ?G ?G1" + using fg group_isomorphisms_def by blast + have "hom_induced (1 + int p) (nsphere (Suc p)) {} (nsphere (Suc p)) {} ?r (f y) = f y [^]\<^bsub>?G1\<^esub> (-1::int)" + if "y \ carrier ?G" for y + by (simp add: that * Brouwer_degree2 Suc hom_int_pow) + then show ?case + by (fastforce simp: eq intro: Brouwer_degree2_unique [OF continuous_map_nsphere_reflection]) +qed + +end diff -r a93e6472ac9c -r c4f2cac288d2 src/HOL/Homology/Homology.thy --- a/src/HOL/Homology/Homology.thy Tue Apr 09 16:59:00 2019 +0000 +++ b/src/HOL/Homology/Homology.thy Tue Apr 09 21:05:48 2019 +0100 @@ -1,6 +1,5 @@ theory Homology - imports - Simplices + imports Brouwer_Degree begin end diff -r a93e6472ac9c -r c4f2cac288d2 src/HOL/Homology/Homology_Groups.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Homology/Homology_Groups.thy Tue Apr 09 21:05:48 2019 +0100 @@ -0,0 +1,2569 @@ +section\Homology, II: Homology Groups\ + +theory Homology_Groups + imports Simplices "HOL-Algebra.Exact_Sequence" + +begin +subsection\Homology Groups\ + +text\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"}.\ + +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 + \ 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 + \ 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) + = (\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 = + \\<^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 + \ 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\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.\ + +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 \ hom (relative_homology_group (int p) X S) + (homology_group (int (p - Suc 0)) (subtopology X S)) + \ (\c. singular_relcycle p X S c + \ 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 \ where "\ \ r_coset (relcycle_group(p - Suc 0) (subtopology X S) {}) + (singular_relboundary_set (p - Suc 0) (subtopology X S) {}) \ 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 \: "\ \ hom (relcycle_group p X S) H" + unfolding \_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) {}) \ 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 \_eq: "\ x = \ 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 \_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 \ normal_subgroup_singular_relboundary_relcycle \_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 \_def) +qed + +lemma hom_boundary2: + "\d. (\p X S. + (d p X S) \ hom (relative_homology_group p X S) + (homology_group (p - 1) (subtopology X S))) + \ (\p X S c. singular_relcycle p X S c \ Suc 0 \ p + \ 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) + \ d p X S c = one(homology_group (p-1) (subtopology X S))) \ + (\p X S. + d p X S \ hom (relative_homology_group p X S) + (homology_group (p-1) (subtopology X S))) \ + (\p X S c. + singular_relcycle p X S c \ 1 \ p + \ d p X S (homologous_rel_set p X S c) + = homologous_rel_set (p - Suc 0) (subtopology X S) {} (chain_boundary p c)) \ + (\p X S. d p X S = d p X (topspace X \ S))) \ + (\p X S c. d p X S c \ carrier(homology_group (p-1) (subtopology X S))) \ + (\p. p \ 0 \ d p = (\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 + \ 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 \ S) c \ 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 \ carrier(relative_homology_group p X S) + then d p X (topspace X \ 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) + \ hom_boundary p X S c = one(homology_group (p-1) (subtopology X (S::'a set)))) \ + (\p X S. + hom_boundary p X S \ hom (relative_homology_group p X S) + (homology_group (p-1) (subtopology X (S::'a set)))) \ + (\p X S c. + singular_relcycle p X S c \ 1 \ p + \ 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)) \ + (\p X S. hom_boundary p X S = hom_boundary p X (topspace X \ (S::'a set)))) \ + (\p X S c. hom_boundary p X S c \ carrier(homology_group (p-1) (subtopology X (S::'a set)))) \ + (\p. p \ 0 \ hom_boundary p = (\q r. \t::'a chain set. undefined))" + by (fact hom_boundary3) + +lemma hom_boundary_default: + "c \ carrier(relative_homology_group p X S) + \ 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\ + \ 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\ + \ (chain_map p f) \ 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. + (\p X S Y T f. + continuous_map X Y f \ f ` (topspace X \ S) \ T + \ (hom_relmap p X S Y T f) \ hom (relative_homology_group (int p) X S) + (relative_homology_group (int p) Y T)) \ + (\p X S Y T f c. + continuous_map X Y f \ f ` (topspace X \ S) \ T \ + singular_relcycle p X S c + \ 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)) \ + (\c. singular_relcycle p X S c \ + 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. + (\p X S Y T f. + continuous_map X Y f \ + f ` (topspace X \ S) \ T + \ (hom_relmap p X S Y T f) \ hom (relative_homology_group p X S) + (relative_homology_group p Y T)) \ + (\p X S Y T f c. + continuous_map X Y f \ + f ` (topspace X \ S) \ T \ + singular_relcycle p X S c + \ 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)) \ + (\p. p < 0 \ hom_relmap p = (\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. + ((\p X S Y T f c. + ~(continuous_map X Y f \ f ` (topspace X \ S) \ T \ + c \ carrier(relative_homology_group p X S)) + \ hom_relmap p X S Y T f c = one(relative_homology_group p Y T)) \ + (\p X S Y T f. + hom_relmap p X S Y T f \ hom (relative_homology_group p X S) (relative_homology_group p Y T)) \ + (\p X S Y T f c. + continuous_map X Y f \ f ` (topspace X \ S) \ T \ singular_relcycle p X S c + \ 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)) \ + (\p X S Y T. + hom_relmap p X S Y T = + hom_relmap p X (topspace X \ S) Y (topspace Y \ T))) \ + (\p X S Y f T c. + hom_relmap p X S Y T f c \ carrier(relative_homology_group p Y T)) \ + (\p. p < 0 \ hom_relmap p = (\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 + \ hom (relative_homology_group p X S) (relative_homology_group p Y T)" + and 2: "\p X S Y T f c. + \continuous_map X Y f; f ` (topspace X \ S) \ T; singular_relcycle p X S c\ + \ + 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 \ S) Y (topspace Y \ T) f c + \ 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 \ carrier (relative_homology_group p X S) + then hom_relmap p X (topspace X \ S) Y (topspace Y \ T) f c + else \\<^bsub>relative_homology_group p Y T\<^esub>) + \ hom (relative_homology_group p X S) (relative_homology_group p Y T)" (is "?h \ 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\ + \ hom_relmap (int p) X (topspace X \ S) Y (topspace Y \ 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 \ f ` (topspace X \ S) \ T \ + c \ carrier(relative_homology_group p X S) + then hom_relmap p X (topspace X \ S) Y (topspace Y \ 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 \ + f ` (topspace X \ S) \ T \ + c \ carrier(relative_homology_group p X S)) + \ hom_induced p X (S::'a set) Y (T::'b set) f c = + one(relative_homology_group p Y T)) \ + (\p X S Y T f. + (hom_induced p X (S::'a set) Y (T::'b set) f) \ hom (relative_homology_group p X S) + (relative_homology_group p Y T)) \ + (\p X S Y T f c. + continuous_map X Y f \ + f ` (topspace X \ S) \ T \ + singular_relcycle p X S c + \ 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)) \ + (\p X S Y T. + hom_induced p X (S::'a set) Y (T::'b set) = + hom_induced p X (topspace X \ S) Y (topspace Y \ T))) \ + (\p X S Y f T c. + hom_induced p X (S::'a set) Y (T::'b set) f c \ + carrier(relative_homology_group p Y T)) \ + (\p. p < 0 \ hom_induced p = (\X S Y T. \f::'a\'b. \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)) + \ 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\ + \ 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\ + \ 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) + \ continuous_map X Y g \ g ` (topspace X \ S) \ T \ C \ 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\Towards the Eilenberg-Steenrod axioms\ + +text\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). \ +(*1. Exact sequence from the inclusions and boundary map + H_{p+1} X --(j')\ H_{p+1}X (A) --(d')\ H_p A --(i')\ 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')\ X (A) induces an isomorphism +when cl U \ 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 \ 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 \ 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) \ + {c. hom_boundary (int m) X S c = \\<^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 \ + {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\ + \ 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 \ + {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)} \ + 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) {}) \ + {c. hom_induced n (subtopology X S) {} X {} id c = + \\<^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) {} \ 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 \ 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\ + \ 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 {} \ 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 + \ 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 \T \ S\ 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 + \ 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: \singular_chain n (subtopology X (S - U)) c\ 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 + \ (\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\Additivity axiom\ + +text\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))) \" + 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 \x \ S\ by (auto simp: disjnt_def) + qed (auto simp: \S \ \\) + then show ?thesis + by (meson \S \ \\ 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)))" + let ?PI = "(\\<^sub>E T\\. singular_relcycle_set p (subtopology X T) {})" + have "(\f. sum' f \) \ Group.iso (subgroup_generated ?SG (carrier ?SG \ ?PI)) + (subgroup_generated (chain_group p X) (singular_relcycle_set p X {}))" + proof (rule group_hom.iso_between_subgroups) + have iso: "(\f. sum' f \) \ Group.iso ?SG (chain_group p X)" + by (auto simp: assms iso_chain_group_sum) + then show "group_hom ?SG (chain_group p X) (\f. sum' f \)" + by (auto simp: iso_imp_homomorphism group_hom_def group_hom_axioms_def) + have B: "sum' f \ \ singular_relcycle_set p X {} \ f \ (carrier ?SG \ ?PI)" + if "f \ (carrier ?SG)" for f + proof - + have f: "\S. S \ \ \ singular_chain p (subtopology X S) (f S)" + "f \ extensional \" "finite {i \ \. f i \ 0}" + using that by (auto simp: carrier_sum_group PiE_def Pi_def) + then have rfin: "finite {S \ \. restrict (chain_boundary p \ f) \ S \ 0}" + by (auto elim: rev_finite_subset) + have "chain_boundary p ((\x | x \ \ \ f x \ 0. f x)) = 0 + \ (\S \ \. chain_boundary p (f S) = 0)" (is "?cb = 0 \ ?rhs") + proof + assume "?cb = 0" + moreover have "?cb = sum' (\S. chain_boundary p (f S)) \" + unfolding sum.G_def using rfin f + by (force simp: chain_boundary_sum intro: sum.mono_neutral_right cong: conj_cong) + ultimately have eq0: "sum' (\S. chain_boundary p (f S)) \ = 0" + by simp + have "(\f. sum' f \) \ hom (sum_group \ (\S. chain_group (p - Suc 0) (subtopology X S))) + (chain_group (p - Suc 0) X)" + and inj: "inj_on (\f. sum' f \) (carrier (sum_group \ (\S. chain_group (p - Suc 0) (subtopology X S))))" + using iso_chain_group_sum [OF assms, of "p-1"] by (auto simp: iso_def bij_betw_def) + then have eq: "\f \ (\\<^sub>E i\\. singular_chain_set (p - Suc 0) (subtopology X i)); + finite {S \ \. f S \ 0}; sum' f \ = 0; S \ \\ \ f S = 0" for f S + apply (simp add: group_hom_def group_hom_axioms_def group_hom.inj_on_one_iff [of _ "chain_group (p-1) X"]) + apply (auto simp: carrier_sum_group fun_eq_iff that) + done + show ?rhs + proof clarify + fix S assume "S \ \" + then show "chain_boundary p (f S) = 0" + using eq [of "restrict (chain_boundary p \ f) \" S] rfin f eq0 + by (simp add: singular_chain_boundary cong: conj_cong) + qed + next + assume ?rhs + then show "?cb = 0" + by (force simp: chain_boundary_sum intro: sum.mono_neutral_right) + qed + moreover + have "(\S. S \ \ \ singular_chain p (subtopology X S) (f S)) + \ singular_chain p X (\x | x \ \ \ f x \ 0. f x)" + by (metis (no_types, lifting) mem_Collect_eq singular_chain_subtopology singular_chain_sum) + ultimately show ?thesis + using f by (auto simp: carrier_sum_group sum.G_def singular_cycle PiE_iff) + qed + have "singular_relcycle_set p X {} \ carrier (chain_group p X)" + using subgroup.subset subgroup_singular_relcycle by blast + then show "(\f. sum' f \) ` (carrier ?SG \ ?PI) = singular_relcycle_set p X {}" + using iso B + apply (auto simp: iso_def bij_betw_def) + apply (force simp: singular_relcycle) + done + qed (auto simp: assms iso_chain_group_sum) + then show ?thesis + by (simp add: relcycle_group_def sum_group_subgroup_generated subgroup_singular_relcycle) +qed + + +proposition homology_additivity_axiom_gen: + 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 "(\x. gfinprod (homology_group p X) + (\V. hom_induced p (subtopology X V) {} X {} id (x V)) \) + \ iso (sum_group \ (\S. homology_group p (subtopology X S))) (homology_group p X)" + (is "?h \ iso ?SG ?HG") +proof (cases "p < 0") + case True + then have [simp]: "gfinprod (singleton_group undefined) (\v. undefined) \ = undefined" + by (metis Pi_I carrier_singleton_group comm_group_def comm_monoid.gfinprod_closed singletonD singleton_abelian_group) + show ?thesis + using True + apply (simp add: iso_def relative_homology_group_def hom_induced_trivial carrier_sum_group) + apply (auto simp: singleton_group_def bij_betw_def inj_on_def fun_eq_iff) + done +next + case False + then obtain n where peq: "p = int n" + by (metis int_ops(1) linorder_neqE_linordered_idom pos_int_cases) + interpret comm_group "homology_group p X" + by (rule abelian_homology_group) + show ?thesis + proof (simp add: iso_def bij_betw_def, intro conjI) + show "?h \ hom ?SG ?HG" + by (rule hom_group_sum) (simp_all add: hom_induced_hom) + then interpret group_hom ?SG ?HG ?h + by (simp add: group_hom_def group_hom_axioms_def) + have carrSG: "carrier ?SG + = (\x. \S\\. homologous_rel_set n (subtopology X S) {} (x S)) + ` (carrier (sum_group \ (\S. relcycle_group n (subtopology X S) {})))" (is "?lhs = ?rhs") + proof + show "?lhs \ ?rhs" + proof (clarsimp simp: carrier_sum_group carrier_relative_homology_group peq) + fix z + assume z: "z \ (\\<^sub>E S\\. homologous_rel_set n (subtopology X S) {} ` singular_relcycle_set n (subtopology X S) {})" + and fin: "finite {S \ \. z S \ singular_relboundary_set n (subtopology X S) {}}" + then obtain c where c: "\S\\. singular_relcycle n (subtopology X S) {} (c S) + \ z S = homologous_rel_set n (subtopology X S) {} (c S)" + by (simp add: PiE_def Pi_def image_def) metis + let ?f = "\S\\. if singular_relboundary n (subtopology X S) {} (c S) then 0 else c S" + have "z = (\S\\. homologous_rel_set n (subtopology X S) {} (?f S))" + apply (simp_all add: c fun_eq_iff PiE_arb [OF z]) + apply (metis homologous_rel_eq_relboundary singular_boundary singular_relboundary_0) + done + moreover have "?f \ (\\<^sub>E i\\. singular_relcycle_set n (subtopology X i) {})" + by (simp add: c fun_eq_iff PiE_arb [OF z]) + moreover have "finite {i \ \. ?f i \ 0}" + apply (rule finite_subset [OF _ fin]) + using z apply (clarsimp simp: PiE_def Pi_def image_def) + by (metis c homologous_rel_set_eq_relboundary singular_boundary) + ultimately + show "z \ (\x. \S\\. homologous_rel_set n (subtopology X S) {} (x S)) ` + {x \ \\<^sub>E i\\. singular_relcycle_set n (subtopology X i) {}. finite {i \ \. x i \ 0}}" + by blast + qed + show "?rhs \ ?lhs" + by (force simp: peq carrier_sum_group carrier_relative_homology_group homologous_rel_set_eq_relboundary + elim: rev_finite_subset) + qed + have gf: "gfinprod (homology_group p X) + (\V. hom_induced n (subtopology X V) {} X {} id + ((\S\\. homologous_rel_set n (subtopology X S) {} (z S)) V)) \ + = homologous_rel_set n X {} (sum' z \)" (is "?lhs = ?rhs") + if z: "z \ carrier (sum_group \ (\S. relcycle_group n (subtopology X S) {}))" for z + proof - + have hom_pi: "(\S. homologous_rel_set n X {} (z S)) \ \ \ carrier (homology_group p X)" + apply (rule Pi_I) + using z + apply (force simp: peq carrier_sum_group carrier_relative_homology_group singular_chain_subtopology singular_cycle) + done + have fin: "finite {S \ \. z S \ 0}" + using that by (force simp: carrier_sum_group) + have "?lhs = gfinprod (homology_group p X) (\S. homologous_rel_set n X {} (z S)) \" + apply (rule gfinprod_cong [OF refl Pi_I]) + apply (simp add: hom_induced_carrier peq) + using that + apply (auto simp: peq simp_implies_def carrier_sum_group PiE_def Pi_def chain_map_ident singular_cycle hom_induced_chain_map) + done + also have "\ = gfinprod (homology_group p X) + (\S. homologous_rel_set n X {} (z S)) {S \ \. z S \ 0}" + apply (rule gfinprod_mono_neutral_cong_right, simp_all add: hom_pi) + apply (simp add: relative_homology_group_def peq) + apply (metis homologous_rel_eq_relboundary singular_relboundary_0) + done + also have "\ = ?rhs" + proof - + have "gfinprod (homology_group p X) (\S. homologous_rel_set n X {} (z S)) \ + = homologous_rel_set n X {} (sum z \)" + if "finite \" "\ \ {S \ \. z S \ 0}" for \ + using that + proof (induction \) + case empty + have "\\<^bsub>homology_group p X\<^esub> = homologous_rel_set n X {} 0" + apply (simp add: relative_homology_group_def peq) + by (metis diff_zero homologous_rel_def homologous_rel_sym) + then show ?case + by simp + next + case (insert S \) + with z have pi: "(\S. homologous_rel_set n X {} (z S)) \ \ \ carrier (homology_group p X)" + "homologous_rel_set n X {} (z S) \ carrier (homology_group p X)" + by (force simp: peq carrier_sum_group carrier_relative_homology_group singular_chain_subtopology singular_cycle)+ + have hom: "homologous_rel_set n X {} (z S) \ carrier (homology_group p X)" + using insert z + by (force simp: peq carrier_sum_group carrier_relative_homology_group singular_chain_subtopology singular_cycle) + show ?case + using insert z + proof (simp add: pi) + show "homologous_rel_set n X {} (z S) \\<^bsub>homology_group p X\<^esub> homologous_rel_set n X {} (sum z \) + = homologous_rel_set n X {} (z S + sum z \)" + using insert z apply (auto simp: peq homologous_rel_add mult_relative_homology_group) + by (metis (no_types, lifting) diff_add_cancel diff_diff_eq2 homologous_rel_def homologous_rel_refl) + qed + qed + with fin show ?thesis + by (simp add: sum.G_def) + qed + finally show ?thesis . + qed + show "inj_on ?h (carrier ?SG)" + proof (clarsimp simp add: inj_on_one_iff) + fix x + assume x: "x \ carrier (sum_group \ (\S. homology_group p (subtopology X S)))" + and 1: "gfinprod (homology_group p X) (\V. hom_induced p (subtopology X V) {} X {} id (x V)) \ + = \\<^bsub>homology_group p X\<^esub>" + have feq: "(\S\\. homologous_rel_set n (subtopology X S) {} (z S)) + = (\S\\. \\<^bsub>homology_group p (subtopology X S)\<^esub>)" + if z: "z \ carrier (sum_group \ (\S. relcycle_group n (subtopology X S) {}))" + and eq: "homologous_rel_set n X {} (sum' z \) = \\<^bsub>homology_group p X\<^esub>" for z + proof - + have "z \ (\\<^sub>E S\\. singular_relcycle_set n (subtopology X S) {})" "finite {S \ \. z S \ 0}" + using z by (auto simp: carrier_sum_group) + have "singular_relboundary n X {} (sum' z \)" + using eq singular_chain_imp_relboundary by (auto simp: relative_homology_group_def peq) + then obtain d where scd: "singular_chain (Suc n) X d" and cbd: "chain_boundary (Suc n) d = sum' z \" + by (auto simp: singular_boundary) + have *: "\d. singular_chain (Suc n) (subtopology X S) d \ chain_boundary (Suc n) d = z S" + if "S \ \" for S + proof - + have inj': "inj_on (\f. sum' f \) {x \ \\<^sub>E S\\. singular_chain_set (Suc n) (subtopology X S). finite {S \ \. x S \ 0}}" + using iso_chain_group_sum [OF assms, of "Suc n"] + by (simp add: iso_iff_mon_epi mon_def carrier_sum_group) + obtain w where w: "w \ (\\<^sub>E S\\. singular_chain_set (Suc n) (subtopology X S))" + and finw: "finite {S \ \. w S \ 0}" + and deq: "d = sum' w \" + using iso_chain_group_sum [OF assms, of "Suc n"] scd + by (auto simp: iso_iff_mon_epi epi_def carrier_sum_group set_eq_iff) + with \S \ \\ have scwS: "singular_chain (Suc n) (subtopology X S) (w S)" + by blast + have "inj_on (\f. sum' f \) {x \ \\<^sub>E S\\. singular_chain_set n (subtopology X S). finite {S \ \. x S \ 0}}" + using iso_chain_group_sum [OF assms, of n] + by (simp add: iso_iff_mon_epi mon_def carrier_sum_group) + then have "(\S\\. chain_boundary (Suc n) (w S)) = z" + proof (rule inj_onD) + have "sum' (\S\\. chain_boundary (Suc n) (w S)) \ = sum' (chain_boundary (Suc n) \ w) {S \ \. w S \ 0}" + by (auto simp: o_def intro: sum.mono_neutral_right') + also have "\ = chain_boundary (Suc n) d" + by (auto simp: sum.G_def deq chain_boundary_sum finw intro: finite_subset [OF _ finw] sum.mono_neutral_left) + finally show "sum' (\S\\. chain_boundary (Suc n) (w S)) \ = sum' z \" + by (simp add: cbd) + show "(\S\\. chain_boundary (Suc n) (w S)) \ {x \ \\<^sub>E S\\. singular_chain_set n (subtopology X S). finite {S \ \. x S \ 0}}" + using w by (auto simp: PiE_iff singular_chain_boundary_alt cong: rev_conj_cong intro: finite_subset [OF _ finw]) + show "z \ {x \ \\<^sub>E S\\. singular_chain_set n (subtopology X S). finite {S \ \. x S \ 0}}" + using z by (simp_all add: carrier_sum_group PiE_iff singular_cycle) + qed + with \S \ \\ scwS show ?thesis + by force + qed + show ?thesis + apply (rule restrict_ext) + using that * + apply (simp add: singular_boundary relative_homology_group_def homologous_rel_set_eq_relboundary peq) + done + qed + show "x = (\S\\. \\<^bsub>homology_group p (subtopology X S)\<^esub>)" + using x 1 carrSG gf + by (auto simp: peq feq) + qed + show "?h ` carrier ?SG = carrier ?HG" + proof safe + fix A + assume "A \ carrier (homology_group p X)" + then obtain y where y: "singular_relcycle n X {} y" and xeq: "A = homologous_rel_set n X {} y" + by (auto simp: peq carrier_relative_homology_group) + then obtain x where "x \ carrier (sum_group \ (\T. relcycle_group n (subtopology X T) {}))" + "y = sum' x \" + using iso_cycle_group_sum [OF assms, of n] that by (force simp: iso_iff_mon_epi epi_def) + then show "A \ (\x. gfinprod (homology_group p X) (\V. hom_induced p (subtopology X V) {} X {} id (x V)) \) ` + carrier (sum_group \ (\S. homology_group p (subtopology X S)))" + apply (simp add: carrSG image_comp o_def xeq) + apply (simp add: hom_induced_carrier peq flip: gf cong: gfinprod_cong) + done + qed auto + qed +qed + + +corollary homology_additivity_axiom: + assumes disj: "pairwise disjnt \" and UU: "\\ = topspace X" + and ope: "\v. v \ \ \ openin X v" + shows "(\x. gfinprod (homology_group p X) + (\v. hom_induced p (subtopology X v) {} X {} id (x v)) \) + \ iso (sum_group \ (\S. homology_group p (subtopology X S))) (homology_group p X)" +proof (rule homology_additivity_axiom_gen [OF disj UU]) + fix C T + assume + "compactin X C" and + "path_connectedin X C" and + "T \ \" and + "\ disjnt C T" + then have "C \ topspace X" + and *: "\B. \openin X T; T \ B \ C = {}; C \ T \ B; openin X B\ \ B \ C = {}" + apply (auto simp: connectedin disjnt_def dest!: path_connectedin_imp_connectedin, blast) + done + have "C \ Union \" + using \C \ topspace X\ UU by blast + moreover have "\ (\ - {T}) \ C = {}" + proof (rule *) + show "T \ \ (\ - {T}) \ C = {}" + using \T \ \\ disj disjointD by fastforce + show "C \ T \ \ (\ - {T})" + using \C \ \ \\ by fastforce + qed (auto simp: \T \ \\ ope) + ultimately show "C \ T" + by blast +qed + + +subsection\Special properties of singular homology\ + +text\In particular: the zeroth homology group is isomorphic to the free abelian group +generated by the path components. So, the "coefficient group" is the integers.\ + +lemma iso_integer_zeroth_homology_group_aux: + assumes X: "path_connected_space X" and f: "singular_simplex 0 X f" and f': "singular_simplex 0 X f'" + shows "homologous_rel 0 X {} (frag_of f) (frag_of f')" +proof - + let ?p = "\j. if j = 0 then 1 else 0" + have "f ?p \ topspace X" "f' ?p \ topspace X" + using assms by (auto simp: singular_simplex_def continuous_map_def) + then obtain g where g: "pathin X g" + and g0: "g 0 = f ?p" + and g1: "g 1 = f' ?p" + using assms by (force simp: path_connected_space_def) + then have contg: "continuous_map (subtopology euclideanreal {0..1}) X g" + by (simp add: pathin_def) + have "singular_chain (Suc 0) X (frag_of (restrict (g \ (\x. x 0)) (standard_simplex 1)))" + proof - + have "continuous_map (subtopology (powertop_real UNIV) (standard_simplex (Suc 0))) + (top_of_set {0..1}) (\x. x 0)" + apply (auto simp: continuous_map_in_subtopology g) + apply (metis (mono_tags) UNIV_I continuous_map_from_subtopology continuous_map_product_projection) + apply (simp_all add: standard_simplex_def) + done + moreover have "continuous_map (top_of_set {0..1}) X g" + using contg by blast + ultimately show ?thesis + by (force simp: singular_chain_of chain_boundary_of singular_simplex_def continuous_map_compose) + qed + moreover + have "chain_boundary (Suc 0) (frag_of (restrict (g \ (\x. x 0)) (standard_simplex 1))) = + frag_of f - frag_of f'" + proof - + have "singular_face (Suc 0) 0 (g \ (\x. x 0)) = f" + "singular_face (Suc 0) (Suc 0) (g \ (\x. x 0)) = f'" + using assms + by (auto simp: singular_face_def singular_simplex_def extensional_def simplical_face_def standard_simplex_0 g0 g1) + then show ?thesis + by (simp add: singular_chain_of chain_boundary_of) + qed + ultimately + show ?thesis + by (auto simp: homologous_rel_def singular_boundary) +qed + + +proposition iso_integer_zeroth_homology_group: + assumes X: "path_connected_space X" and f: "singular_simplex 0 X f" + shows "pow (homology_group 0 X) (homologous_rel_set 0 X {} (frag_of f)) + \ iso integer_group (homology_group 0 X)" (is "pow ?H ?q \ iso _ ?H") +proof - + have srf: "singular_relcycle 0 X {} (frag_of f)" + by (simp add: chain_boundary_def f singular_chain_of singular_cycle) + then have qcarr: "?q \ carrier ?H" + by (simp add: carrier_relative_homology_group_0) + have 1: "homologous_rel_set 0 X {} a \ range (\n. homologous_rel_set 0 X {} (frag_cmul n (frag_of f)))" + if "singular_relcycle 0 X {} a" for a + proof - + have "singular_chain 0 X d \ + homologous_rel_set 0 X {} d \ range (\n. homologous_rel_set 0 X {} (frag_cmul n (frag_of f)))" for d + unfolding singular_chain_def + proof (induction d rule: frag_induction) + case zero + then show ?case + by (metis frag_cmul_zero rangeI) + next + case (one x) + then have "\i. homologous_rel_set 0 X {} (frag_cmul i (frag_of f)) + = homologous_rel_set 0 X {} (frag_of x)" + by (metis (no_types) iso_integer_zeroth_homology_group_aux [OF X] f frag_cmul_one homologous_rel_eq mem_Collect_eq) + with one show ?case + by auto + next + case (diff a b) + then obtain c d where + "homologous_rel 0 X {} (a - b) (frag_cmul c (frag_of f) - frag_cmul d (frag_of f))" + using homologous_rel_diff by (fastforce simp add: homologous_rel_set_eq) + then show ?case + by (rule_tac x="c-d" in image_eqI) (auto simp: homologous_rel_set_eq frag_cmul_diff_distrib) + qed + with that show ?thesis + unfolding singular_relcycle_def by blast + qed + have 2: "n = 0" + if "homologous_rel_set 0 X {} (frag_cmul n (frag_of f)) = \\<^bsub>relative_homology_group 0 X {}\<^esub>" + for n + proof - + have "singular_chain (Suc 0) X d + \ frag_extend (\x. frag_of f) (chain_boundary (Suc 0) d) = 0" for d + unfolding singular_chain_def + proof (induction d rule: frag_induction) + case (one x) + then show ?case + by (simp add: frag_extend_diff chain_boundary_of) + next + case (diff a b) + then show ?case + by (simp add: chain_boundary_diff frag_extend_diff) + qed auto + with that show ?thesis + by (force simp: singular_boundary relative_homology_group_def homologous_rel_set_eq_relboundary frag_extend_cmul) + qed + interpret GH : group_hom integer_group ?H "([^]\<^bsub>?H\<^esub>) ?q" + by (simp add: group_hom_def group_hom_axioms_def qcarr group.hom_integer_group_pow) + have eq: "pow ?H ?q = (\n. homologous_rel_set 0 X {} (frag_cmul n (frag_of f)))" + proof + fix n + have "frag_of f + \ carrier (subgroup_generated + (free_Abelian_group (singular_simplex_set 0 X)) (singular_relcycle_set 0 X {}))" + by (metis carrier_relcycle_group chain_group_def mem_Collect_eq relcycle_group_def srf) + then have ff: "frag_of f [^]\<^bsub>relcycle_group 0 X {}\<^esub> n = frag_cmul n (frag_of f)" + by (simp add: relcycle_group_def chain_group_def group.int_pow_subgroup_generated f) + show "pow ?H ?q n = homologous_rel_set 0 X {} (frag_cmul n (frag_of f))" + apply (rule subst [OF right_coset_singular_relboundary]) + apply (simp add: relative_homology_group_def) + apply (simp add: srf ff normal.FactGroup_int_pow normal_subgroup_singular_relboundary_relcycle) + done + qed + show ?thesis + apply (subst GH.iso_iff) + apply (simp add: eq) + apply (auto simp: carrier_relative_homology_group_0 1 2) + done +qed + + +corollary isomorphic_integer_zeroth_homology_group: + assumes X: "path_connected_space X" "topspace X \ {}" + shows "homology_group 0 X \ integer_group" +proof - + obtain a where a: "a \ topspace X" + using assms by auto + have "singular_simplex 0 X (restrict (\x. a) (standard_simplex 0))" + by (simp add: singular_simplex_def a) + then show ?thesis + using X group.iso_sym group_integer_group is_isoI iso_integer_zeroth_homology_group by blast +qed + + +corollary homology_coefficients: + "topspace X = {a} \ homology_group 0 X \ integer_group" + using isomorphic_integer_zeroth_homology_group path_connectedin_topspace by fastforce + +proposition zeroth_homology_group: + "homology_group 0 X \ free_Abelian_group (path_components_of X)" +proof - + obtain h where h: "h \ iso (sum_group (path_components_of X) (\S. homology_group 0 (subtopology X S))) + (homology_group 0 X)" + proof (rule that [OF homology_additivity_axiom_gen]) + show "disjoint (path_components_of X)" + by (simp add: pairwise_disjoint_path_components_of) + show "\(path_components_of X) = topspace X" + by (rule Union_path_components_of) + next + fix C T + assume "path_connectedin X C" "T \ path_components_of X" "\ disjnt C T" + then show "C \ T" + by (metis path_components_of_maximal disjnt_sym)+ + qed + have "homology_group 0 X \ sum_group (path_components_of X) (\S. homology_group 0 (subtopology X S))" + by (rule group.iso_sym) (use h is_iso_def in auto) + also have "\ \ sum_group (path_components_of X) (\i. integer_group)" + proof (rule iso_sum_groupI) + show "homology_group 0 (subtopology X i) \ integer_group" if "i \ path_components_of X" for i + by (metis that isomorphic_integer_zeroth_homology_group nonempty_path_components_of + path_connectedin_def path_connectedin_path_components_of topspace_subtopology_subset) + qed auto + also have "\ \ free_Abelian_group (path_components_of X)" + using path_connectedin_path_components_of nonempty_path_components_of + by (simp add: isomorphic_sum_integer_group path_connectedin_def) + finally show ?thesis . +qed + + +lemma isomorphic_homology_imp_path_components: + assumes "homology_group 0 X \ homology_group 0 Y" + shows "path_components_of X \ path_components_of Y" +proof - + have "free_Abelian_group (path_components_of X) \ homology_group 0 X" + by (rule group.iso_sym) (auto simp: zeroth_homology_group) + also have "\ \ homology_group 0 Y" + by (rule assms) + also have "\ \ free_Abelian_group (path_components_of Y)" + by (rule zeroth_homology_group) + finally have "free_Abelian_group (path_components_of X) \ free_Abelian_group (path_components_of Y)" . + then show ?thesis + by (simp add: isomorphic_free_Abelian_groups) +qed + + +lemma isomorphic_homology_imp_path_connectedness: + assumes "homology_group 0 X \ homology_group 0 Y" + shows "path_connected_space X \ path_connected_space Y" +proof - + obtain h where h: "bij_betw h (path_components_of X) (path_components_of Y)" + using assms isomorphic_homology_imp_path_components eqpoll_def by blast + have 1: "path_components_of X \ {a} \ path_components_of Y \ {h a}" for a + using h unfolding bij_betw_def by blast + have 2: "path_components_of Y \ {a} + \ path_components_of X \ {inv_into (path_components_of X) h a}" for a + using h [THEN bij_betw_inv_into] unfolding bij_betw_def by blast + show ?thesis + unfolding path_connected_space_iff_components_subset_singleton + by (blast intro: dest: 1 2) +qed + + +subsection\More basic properties of homology groups, deduced from the E-S axioms\ + +lemma trivial_homology_group: + "p < 0 \ trivial_group(homology_group p X)" + by simp + +lemma hom_induced_empty_hom: + "(hom_induced p X {} X' {} f) \ hom (homology_group p X) (homology_group p X')" + by (simp add: hom_induced_hom) + +lemma hom_induced_compose_empty: + "\continuous_map X Y f; continuous_map Y Z g\ + \ hom_induced p X {} Z {} (g \ f) = hom_induced p Y {} Z {} g \ hom_induced p X {} Y {} f" + by (simp add: hom_induced_compose) + +lemma homology_homotopy_empty: + "homotopic_with (\h. True) X Y f g \ hom_induced p X {} Y {} f = hom_induced p X {} Y {} g" + by (simp add: homology_homotopy_axiom) + +lemma homotopy_equivalence_relative_homology_group_isomorphisms: + assumes contf: "continuous_map X Y f" and fim: "f ` S \ T" + and contg: "continuous_map Y X g" and gim: "g ` T \ S" + and gf: "homotopic_with (\h. h ` S \ S) X X (g \ f) id" + and fg: "homotopic_with (\k. k ` T \ T) Y Y (f \ g) id" + shows "group_isomorphisms (relative_homology_group p X S) (relative_homology_group p Y T) + (hom_induced p X S Y T f) (hom_induced p Y T X S g)" + unfolding group_isomorphisms_def +proof (intro conjI ballI) + fix x + assume x: "x \ carrier (relative_homology_group p X S)" + then show "hom_induced p Y T X S g (hom_induced p X S Y T f x) = x" + using homology_homotopy_axiom [OF gf, of p] + apply (simp add: hom_induced_compose [OF contf fim contg gim]) + apply (metis comp_apply hom_induced_id) + done +next + fix y + assume "y \ carrier (relative_homology_group p Y T)" + then show "hom_induced p X S Y T f (hom_induced p Y T X S g y) = y" + using homology_homotopy_axiom [OF fg, of p] + apply (simp add: hom_induced_compose [OF contg gim contf fim]) + apply (metis comp_apply hom_induced_id) + done +qed (auto simp: hom_induced_hom) + + +lemma homotopy_equivalence_relative_homology_group_isomorphism: + assumes "continuous_map X Y f" and fim: "f ` S \ T" + and "continuous_map Y X g" and gim: "g ` T \ S" + and "homotopic_with (\h. h ` S \ S) X X (g \ f) id" + and "homotopic_with (\k. k ` T \ T) Y Y (f \ g) id" + shows "(hom_induced p X S Y T f) \ iso (relative_homology_group p X S) (relative_homology_group p Y T)" + using homotopy_equivalence_relative_homology_group_isomorphisms [OF assms] group_isomorphisms_imp_iso + by metis + +lemma homotopy_equivalence_homology_group_isomorphism: + assumes "continuous_map X Y f" + and "continuous_map Y X g" + and "homotopic_with (\h. True) X X (g \ f) id" + and "homotopic_with (\k. True) Y Y (f \ g) id" + shows "(hom_induced p X {} Y {} f) \ iso (homology_group p X) (homology_group p Y)" + apply (rule homotopy_equivalence_relative_homology_group_isomorphism) + using assms by auto + +lemma homotopy_equivalent_space_imp_isomorphic_relative_homology_groups: + assumes "continuous_map X Y f" and fim: "f ` S \ T" + and "continuous_map Y X g" and gim: "g ` T \ S" + and "homotopic_with (\h. h ` S \ S) X X (g \ f) id" + and "homotopic_with (\k. k ` T \ T) Y Y (f \ g) id" + shows "relative_homology_group p X S \ relative_homology_group p Y T" + using homotopy_equivalence_relative_homology_group_isomorphism [OF assms] + unfolding is_iso_def by blast + +lemma homotopy_equivalent_space_imp_isomorphic_homology_groups: + "X homotopy_equivalent_space Y \ homology_group p X \ homology_group p Y" + unfolding homotopy_equivalent_space_def + by (auto intro: homotopy_equivalent_space_imp_isomorphic_relative_homology_groups) + +lemma homeomorphic_space_imp_isomorphic_homology_groups: + "X homeomorphic_space Y \ homology_group p X \ homology_group p Y" + by (simp add: homeomorphic_imp_homotopy_equivalent_space homotopy_equivalent_space_imp_isomorphic_homology_groups) + +lemma trivial_relative_homology_group_gen: + assumes "continuous_map X (subtopology X S) f" + "homotopic_with (\h. True) (subtopology X S) (subtopology X S) f id" + "homotopic_with (\k. True) X X f id" + shows "trivial_group(relative_homology_group p X S)" +proof (rule exact_seq_imp_triviality) + show "exact_seq ([homology_group (p-1) X, + homology_group (p-1) (subtopology X S), + relative_homology_group p X S, homology_group p X, homology_group p (subtopology X S)], + [hom_induced (p-1) (subtopology X S) {} X {} id, + hom_boundary p X S, + hom_induced p X {} X S id, + hom_induced p (subtopology X S) {} X {} id])" + using homology_exactness_axiom_1 homology_exactness_axiom_2 homology_exactness_axiom_3 + by (metis exact_seq_cons_iff) +next + show "hom_induced p (subtopology X S) {} X {} id + \ iso (homology_group p (subtopology X S)) (homology_group p X)" + "hom_induced (p - 1) (subtopology X S) {} X {} id + \ iso (homology_group (p - 1) (subtopology X S)) (homology_group (p - 1) X)" + using assms + by (auto intro: homotopy_equivalence_relative_homology_group_isomorphism) +qed + + +lemma trivial_relative_homology_group_topspace: + "trivial_group(relative_homology_group p X (topspace X))" + by (rule trivial_relative_homology_group_gen [where f=id]) auto + +lemma trivial_relative_homology_group_empty: + "topspace X = {} \ trivial_group(relative_homology_group p X S)" + by (metis Int_absorb2 empty_subsetI relative_homology_group_restrict trivial_relative_homology_group_topspace) + +lemma trivial_homology_group_empty: + "topspace X = {} \ trivial_group(homology_group p X)" + by (simp add: trivial_relative_homology_group_empty) + +lemma homeomorphic_maps_relative_homology_group_isomorphisms: + assumes "homeomorphic_maps X Y f g" and im: "f ` S \ T" "g ` T \ S" + shows "group_isomorphisms (relative_homology_group p X S) (relative_homology_group p Y T) + (hom_induced p X S Y T f) (hom_induced p Y T X S g)" +proof - + have fg: "continuous_map X Y f" "continuous_map Y X g" + "(\x\topspace X. g (f x) = x)" "(\y\topspace Y. f (g y) = y)" + using assms by (simp_all add: homeomorphic_maps_def) + have "group_isomorphisms + (relative_homology_group p X (topspace X \ S)) + (relative_homology_group p Y (topspace Y \ T)) + (hom_induced p X (topspace X \ S) Y (topspace Y \ T) f) + (hom_induced p Y (topspace Y \ T) X (topspace X \ S) g)" + proof (rule homotopy_equivalence_relative_homology_group_isomorphisms) + show "homotopic_with (\h. h ` (topspace X \ S) \ topspace X \ S) X X (g \ f) id" + using fg im by (auto intro: homotopic_with_equal continuous_map_compose) + next + show "homotopic_with (\k. k ` (topspace Y \ T) \ topspace Y \ T) Y Y (f \ g) id" + using fg im by (auto intro: homotopic_with_equal continuous_map_compose) + qed (use im fg in \auto simp: continuous_map_def\) + then show ?thesis + by simp +qed + +lemma homeomorphic_map_relative_homology_iso: + assumes f: "homeomorphic_map X Y f" and S: "S \ topspace X" "f ` S = T" + shows "(hom_induced p X S Y T f) \ iso (relative_homology_group p X S) (relative_homology_group p Y T)" +proof - + obtain g where g: "homeomorphic_maps X Y f g" + using homeomorphic_map_maps f by metis + then have "group_isomorphisms (relative_homology_group p X S) (relative_homology_group p Y T) + (hom_induced p X S Y T f) (hom_induced p Y T X S g)" + using S g by (auto simp: homeomorphic_maps_def intro!: homeomorphic_maps_relative_homology_group_isomorphisms) + then show ?thesis + by (rule group_isomorphisms_imp_iso) +qed + +lemma inj_on_hom_induced_section_map: + assumes "section_map X Y f" + shows "inj_on (hom_induced p X {} Y {} f) (carrier (homology_group p X))" +proof - + obtain g where cont: "continuous_map X Y f" "continuous_map Y X g" + and gf: "\x. x \ topspace X \ g (f x) = x" + using assms by (auto simp: section_map_def retraction_maps_def) + show ?thesis + proof (rule inj_on_inverseI) + fix x + assume x: "x \ carrier (homology_group p X)" + have "continuous_map X X (\x. g (f x))" + by (metis (no_types, lifting) continuous_map_eq continuous_map_id gf id_apply) + with x show "hom_induced p Y {} X {} g (hom_induced p X {} Y {} f x) = x" + using hom_induced_compose_empty [OF cont, symmetric] + apply (simp add: o_def fun_eq_iff) + apply (rule hom_induced_id_gen) + apply (auto simp: gf) + done + qed +qed + +corollary mon_hom_induced_section_map: + assumes "section_map X Y f" + shows "(hom_induced p X {} Y {} f) \ mon (homology_group p X) (homology_group p Y)" + by (simp add: hom_induced_empty_hom inj_on_hom_induced_section_map [OF assms] mon_def) + +lemma surj_hom_induced_retraction_map: + assumes "retraction_map X Y f" + shows "carrier (homology_group p Y) = (hom_induced p X {} Y {} f) ` carrier (homology_group p X)" + (is "?lhs = ?rhs") +proof - + obtain g where cont: "continuous_map Y X g" "continuous_map X Y f" + and fg: "\x. x \ topspace Y \ f (g x) = x" + using assms by (auto simp: retraction_map_def retraction_maps_def) + have "x = hom_induced p X {} Y {} f (hom_induced p Y {} X {} g x)" + if x: "x \ carrier (homology_group p Y)" for x + proof - + have "continuous_map Y Y (\x. f (g x))" + by (metis (no_types, lifting) continuous_map_eq continuous_map_id fg id_apply) + with x show ?thesis + using hom_induced_compose_empty [OF cont, symmetric] + apply (simp add: o_def fun_eq_iff) + apply (rule hom_induced_id_gen [symmetric]) + apply (auto simp: fg) + done + qed + moreover + have "(hom_induced p Y {} X {} g x) \ carrier (homology_group p X)" + if "x \ carrier (homology_group p Y)" for x + by (metis hom_induced) + ultimately have "?lhs \ ?rhs" + by auto + moreover have "?rhs \ ?lhs" + using hom_induced_hom [of p X "{}" Y "{}" f] + by (simp add: hom_def flip: image_subset_iff_funcset) + ultimately show ?thesis + by auto +qed + + +corollary epi_hom_induced_retraction_map: + assumes "retraction_map X Y f" + shows "(hom_induced p X {} Y {} f) \ epi (homology_group p X) (homology_group p Y)" + using assms epi_iff_subset hom_induced_empty_hom surj_hom_induced_retraction_map by fastforce + + +lemma homeomorphic_map_homology_iso: + assumes "homeomorphic_map X Y f" + shows "(hom_induced p X {} Y {} f) \ iso (homology_group p X) (homology_group p Y)" + using assms + apply (simp add: iso_def bij_betw_def flip: section_and_retraction_eq_homeomorphic_map) + by (metis inj_on_hom_induced_section_map surj_hom_induced_retraction_map hom_induced_hom) + +(*See also hom_hom_induced_inclusion*) +lemma inj_on_hom_induced_inclusion: + assumes "S = {} \ S retract_of_space X" + shows "inj_on (hom_induced p (subtopology X S) {} X {} id) (carrier (homology_group p (subtopology X S)))" + using assms +proof + assume "S = {}" + then have "trivial_group(homology_group p (subtopology X S))" + by (auto simp: topspace_subtopology intro: trivial_homology_group_empty) + then show ?thesis + by (auto simp: inj_on_def trivial_group_def) +next + assume "S retract_of_space X" + then show ?thesis + by (simp add: retract_of_space_section_map inj_on_hom_induced_section_map) +qed + +lemma trivial_homomorphism_hom_boundary_inclusion: + assumes "S = {} \ S retract_of_space X" + shows "trivial_homomorphism + (relative_homology_group p X S) (homology_group (p-1) (subtopology X S)) + (hom_boundary p X S)" + apply (rule iffD1 [OF exact_seq_mon_eq_triviality inj_on_hom_induced_inclusion [OF assms]]) + apply (rule exact_seq.intros) + apply (rule homology_exactness_axiom_1 [of p]) + using homology_exactness_axiom_2 [of p] + by auto + +lemma epi_hom_induced_relativization: + assumes "S = {} \ S retract_of_space X" + shows "(hom_induced p X {} X S id) ` carrier (homology_group p X) = carrier (relative_homology_group p X S)" + apply (rule iffD2 [OF exact_seq_epi_eq_triviality trivial_homomorphism_hom_boundary_inclusion]) + apply (rule exact_seq.intros) + apply (rule homology_exactness_axiom_1 [of p]) + using homology_exactness_axiom_2 [of p] apply (auto simp: assms) + done + +(*different in HOL Light because we don't need short_exact_sequence*) +lemmas short_exact_sequence_hom_induced_inclusion = homology_exactness_axiom_3 + +lemma group_isomorphisms_homology_group_prod_retract: + assumes "S = {} \ S retract_of_space X" + obtains \ \ where + "subgroup \ (homology_group p X)" + "subgroup \ (homology_group p X)" + "(\(x, y). x \\<^bsub>homology_group p X\<^esub> y) + \ iso (DirProd (subgroup_generated (homology_group p X) \) (subgroup_generated (homology_group p X) \)) + (homology_group p X)" + "(hom_induced p (subtopology X S) {} X {} id) + \ iso (homology_group p (subtopology X S)) (subgroup_generated (homology_group p X) \)" + "(hom_induced p X {} X S id) + \ iso (subgroup_generated (homology_group p X) \) (relative_homology_group p X S)" + using assms +proof + assume "S = {}" + show thesis + proof (rule splitting_lemma_left [OF homology_exactness_axiom_3 [of p]]) + let ?f = "\x. one(homology_group p (subtopology X {}))" + show "?f \ hom (homology_group p X) (homology_group p (subtopology X {}))" + by (simp add: trivial_hom) + have tg: "trivial_group (homology_group p (subtopology X {}))" + by (auto simp: topspace_subtopology trivial_homology_group_empty) + then have [simp]: "carrier (homology_group p (subtopology X {})) = {one (homology_group p (subtopology X {}))}" + by (auto simp: trivial_group_def) + then show "?f (hom_induced p (subtopology X {}) {} X {} id x) = x" + if "x \ carrier (homology_group p (subtopology X {}))" for x + using that by auto + show "inj_on (hom_induced p (subtopology X {}) {} X {} id) + (carrier (homology_group p (subtopology X {})))" + by auto + show "hom_induced p X {} X {} id ` carrier (homology_group p X) = carrier (homology_group p X)" + by (metis epi_hom_induced_relativization) + next + fix \ \ + assume *: "\ \ homology_group p X" "\ \ homology_group p X" + "\ \ \ \ {\\<^bsub>homology_group p X\<^esub>}" + "hom_induced p (subtopology X {}) {} X {} id + \ Group.iso (homology_group p (subtopology X {})) (subgroup_generated (homology_group p X) \)" + "hom_induced p X {} X {} id + \ Group.iso (subgroup_generated (homology_group p X) \) (relative_homology_group p X {})" + "\ <#>\<^bsub>homology_group p X\<^esub> \ = carrier (homology_group p X)" + show thesis + proof (rule that) + show "(\(x, y). x \\<^bsub>homology_group p X\<^esub> y) + \ iso (subgroup_generated (homology_group p X) \ \\ subgroup_generated (homology_group p X) \) + (homology_group p X)" + using * by (simp add: group_disjoint_sum.iso_group_mul normal_def group_disjoint_sum_def) + qed (use \S = {}\ * in \auto simp: normal_def\) + qed +next + assume "S retract_of_space X" + then obtain r where "S \ topspace X" and r: "continuous_map X (subtopology X S) r" + and req: "\x \ S. r x = x" + by (auto simp: retract_of_space_def) + show thesis + proof (rule splitting_lemma_left [OF homology_exactness_axiom_3 [of p]]) + let ?f = "hom_induced p X {} (subtopology X S) {} r" + show "?f \ hom (homology_group p X) (homology_group p (subtopology X S))" + by (simp add: hom_induced_empty_hom) + show eqx: "?f (hom_induced p (subtopology X S) {} X {} id x) = x" + if "x \ carrier (homology_group p (subtopology X S))" for x + proof - + have "hom_induced p (subtopology X S) {} (subtopology X S) {} r x = x" + by (metis \S \ topspace X\ continuous_map_from_subtopology hom_induced_id_gen inf.absorb_iff2 r req that topspace_subtopology) + then show ?thesis + by (simp add: r hom_induced_compose [unfolded o_def fun_eq_iff, rule_format, symmetric]) + qed + then show "inj_on (hom_induced p (subtopology X S) {} X {} id) + (carrier (homology_group p (subtopology X S)))" + unfolding inj_on_def by metis + show "hom_induced p X {} X S id ` carrier (homology_group p X) = carrier (relative_homology_group p X S)" + by (simp add: \S retract_of_space X\ epi_hom_induced_relativization) + next + fix \ \ + assume *: "\ \ homology_group p X" "\ \ homology_group p X" + "\ \ \ \ {\\<^bsub>homology_group p X\<^esub>}" + "\ <#>\<^bsub>homology_group p X\<^esub> \ = carrier (homology_group p X)" + "hom_induced p (subtopology X S) {} X {} id + \ Group.iso (homology_group p (subtopology X S)) (subgroup_generated (homology_group p X) \)" + "hom_induced p X {} X S id + \ Group.iso (subgroup_generated (homology_group p X) \) (relative_homology_group p X S)" + show "thesis" + proof (rule that) + show "(\(x, y). x \\<^bsub>homology_group p X\<^esub> y) + \ iso (subgroup_generated (homology_group p X) \ \\ subgroup_generated (homology_group p X) \) + (homology_group p X)" + using * + by (simp add: group_disjoint_sum.iso_group_mul normal_def group_disjoint_sum_def) + qed (use * in \auto simp: normal_def\) + qed +qed + + + +lemma isomorphic_group_homology_group_prod_retract: + assumes "S = {} \ S retract_of_space X" + shows "homology_group p X \ homology_group p (subtopology X S) \\ relative_homology_group p X S" + (is "?lhs \ ?rhs") +proof - + obtain \ \ where + "subgroup \ (homology_group p X)" + "subgroup \ (homology_group p X)" + and 1: "(\(x, y). x \\<^bsub>homology_group p X\<^esub> y) + \ iso (DirProd (subgroup_generated (homology_group p X) \) (subgroup_generated (homology_group p X) \)) + (homology_group p X)" + "(hom_induced p (subtopology X S) {} X {} id) + \ iso (homology_group p (subtopology X S)) (subgroup_generated (homology_group p X) \)" + "(hom_induced p X {} X S id) + \ iso (subgroup_generated (homology_group p X) \) (relative_homology_group p X S)" + using group_isomorphisms_homology_group_prod_retract [OF assms] by blast + have "?lhs \ subgroup_generated (homology_group p X) \ \\ subgroup_generated (homology_group p X) \" + by (meson DirProd_group 1 abelian_homology_group comm_group_def group.abelian_subgroup_generated group.iso_sym is_isoI) + also have "\ \ ?rhs" + by (meson "1"(2) "1"(3) abelian_homology_group comm_group_def group.DirProd_iso_trans group.abelian_subgroup_generated group.iso_sym is_isoI) + finally show ?thesis . +qed + + +lemma homology_additivity_explicit: + assumes "openin X S" "openin X T" "disjnt S T" and SUT: "S \ T = topspace X" + shows "(\(a,b).(hom_induced p (subtopology X S) {} X {} id a) + \\<^bsub>homology_group p X\<^esub> + (hom_induced p (subtopology X T) {} X {} id b)) + \ iso (DirProd (homology_group p (subtopology X S)) (homology_group p (subtopology X T))) + (homology_group p X)" +proof - + have "closedin X S" "closedin X T" + using assms Un_commute disjnt_sym + by (metis Diff_cancel Diff_triv Un_Diff disjnt_def openin_closedin_eq sup_bot.right_neutral)+ + with \openin X S\ \openin X T\ have SS: "X closure_of S \ X interior_of S" and TT: "X closure_of T \ X interior_of T" + by (simp_all add: closure_of_closedin interior_of_openin) + have [simp]: "S \ T - T = S" "S \ T - S = T" + using \disjnt S T\ + by (auto simp: Diff_triv Un_Diff disjnt_def) + let ?f = "hom_induced p X {} X T id" + let ?g = "hom_induced p X {} X S id" + let ?h = "hom_induced p (subtopology X S) {} X T id" + let ?i = "hom_induced p (subtopology X S) {} X {} id" + let ?j = "hom_induced p (subtopology X T) {} X {} id" + let ?k = "hom_induced p (subtopology X T) {} X S id" + let ?A = "homology_group p (subtopology X S)" + let ?B = "homology_group p (subtopology X T)" + let ?C = "relative_homology_group p X T" + let ?D = "relative_homology_group p X S" + let ?G = "homology_group p X" + have h: "?h \ iso ?A ?C" and k: "?k \ iso ?B ?D" + using homology_excision_axiom [OF TT, of "S \ T" p] + using homology_excision_axiom [OF SS, of "S \ T" p] + by auto (simp_all add: SUT) + have 1: "\x. (hom_induced p X {} X T id \ hom_induced p (subtopology X S) {} X {} id) x + = hom_induced p (subtopology X S) {} X T id x" + by (simp flip: hom_induced_compose) + have 2: "\x. (hom_induced p X {} X S id \ hom_induced p (subtopology X T) {} X {} id) x + = hom_induced p (subtopology X T) {} X S id x" + by (simp flip: hom_induced_compose) + show ?thesis + using exact_sequence_sum_lemma + [OF abelian_homology_group h k homology_exactness_axiom_3 homology_exactness_axiom_3] 1 2 + by auto +qed + + +subsection\Generalize exact homology sequence to triples\ + +definition hom_relboundary :: "[int,'a topology,'a set,'a set,'a chain set] \ 'a chain set" + where + "hom_relboundary p X S T = + hom_induced (p - 1) (subtopology X S) {} (subtopology X S) T id \ + hom_boundary p X S" + +lemma group_homomorphism_hom_relboundary: + "hom_relboundary p X S T + \ hom (relative_homology_group p X S) (relative_homology_group (p - 1) (subtopology X S) T)" + unfolding hom_relboundary_def + proof (rule hom_compose) + show "hom_boundary p X S \ hom (relative_homology_group p X S) (homology_group(p - 1) (subtopology X S))" + by (simp add: hom_boundary_hom) + show "hom_induced (p - 1) (subtopology X S) {} (subtopology X S) T id + \ hom (homology_group(p - 1) (subtopology X S)) (relative_homology_group (p - 1) (subtopology X S) T)" + by (simp add: hom_induced_hom) +qed + +lemma hom_relboundary: + "hom_relboundary p X S T c \ carrier (relative_homology_group (p - 1) (subtopology X S) T)" + by (simp add: hom_relboundary_def hom_induced_carrier) + +lemma hom_relboundary_empty: "hom_relboundary p X S {} = hom_boundary p X S" + apply (simp add: hom_relboundary_def o_def) + apply (subst hom_induced_id) + apply (metis hom_boundary_carrier, auto) + done + +lemma naturality_hom_induced_relboundary: + assumes "continuous_map X Y f" "f ` S \ U" "f ` T \ V" + shows "hom_relboundary p Y U V \ + hom_induced p X S Y (U) f = + hom_induced (p - 1) (subtopology X S) T (subtopology Y U) V f \ + hom_relboundary p X S T" +proof - + have [simp]: "continuous_map (subtopology X S) (subtopology Y U) f" + using assms continuous_map_from_subtopology continuous_map_in_subtopology topspace_subtopology by fastforce + have "hom_induced (p - 1) (subtopology Y U) {} (subtopology Y U) V id \ + hom_induced (p - 1) (subtopology X S) {} (subtopology Y U) {} f + = hom_induced (p - 1) (subtopology X S) T (subtopology Y U) V f \ + hom_induced (p - 1) (subtopology X S) {} (subtopology X S) T id" + using assms by (simp flip: hom_induced_compose) + then show ?thesis + apply (simp add: hom_relboundary_def comp_assoc naturality_hom_induced assms) + apply (simp flip: comp_assoc) + done +qed + +proposition homology_exactness_triple_1: + assumes "T \ S" + shows "exact_seq ([relative_homology_group(p - 1) (subtopology X S) T, + relative_homology_group p X S, + relative_homology_group p X T], + [hom_relboundary p X S T, hom_induced p X T X S id])" + (is "exact_seq ([?G1,?G2,?G3], [?h1,?h2])") +proof - + have iTS: "id ` T \ S" and [simp]: "S \ T = T" + using assms by auto + have "?h2 B \ kernel ?G2 ?G1 ?h1" for B + proof - + have "hom_boundary p X T B \ carrier (relative_homology_group (p - 1) (subtopology X T) {})" + by (metis (no_types) hom_boundary) + then have *: "hom_induced (p - 1) (subtopology X S) {} (subtopology X S) T id + (hom_induced (p - 1) (subtopology X T) {} (subtopology X S) {} id + (hom_boundary p X T B)) + = \\<^bsub>?G1\<^esub>" + using homology_exactness_axiom_3 [of "p-1" "subtopology X S" T] + by (auto simp: subtopology_subtopology kernel_def) + show ?thesis + apply (simp add: kernel_def hom_induced_carrier hom_relboundary_def flip: *) + by (metis comp_def naturality_hom_induced [OF continuous_map_id iTS]) + qed + moreover have "B \ ?h2 ` carrier ?G3" if "B \ kernel ?G2 ?G1 ?h1" for B + proof - + have Bcarr: "B \ carrier ?G2" + and Beq: "?h1 B = \\<^bsub>?G1\<^esub>" + using that by (auto simp: kernel_def) + have "\A' \ carrier (homology_group (p - 1) (subtopology X T)). hom_induced (p - 1) (subtopology X T) {} (subtopology X S) {} id A' = A" + if "A \ carrier (homology_group (p - 1) (subtopology X S))" + "hom_induced (p - 1) (subtopology X S) {} (subtopology X S) T id A = + \\<^bsub>?G1\<^esub>" for A + using homology_exactness_axiom_3 [of "p-1" "subtopology X S" T] that + by (simp add: kernel_def subtopology_subtopology image_iff set_eq_iff) meson + then obtain C where Ccarr: "C \ carrier (homology_group (p - 1) (subtopology X T))" + and Ceq: "hom_induced (p - 1) (subtopology X T) {} (subtopology X S) {} id C = hom_boundary p X S B" + using Beq by (simp add: hom_relboundary_def) (metis hom_boundary_carrier) + let ?hi_XT = "hom_induced (p - 1) (subtopology X T) {} X {} id" + have "?hi_XT + = hom_induced (p - 1) (subtopology X S) {} X {} id + \ (hom_induced (p - 1) (subtopology X T) {} (subtopology X S) {} id)" + by (metis assms comp_id continuous_map_id_subt hom_induced_compose_empty inf.absorb_iff2 subtopology_subtopology) + then have "?hi_XT C + = hom_induced (p - 1) (subtopology X S) {} X {} id (hom_boundary p X S B)" + by (simp add: Ceq) + also have eq: "\ = \\<^bsub>homology_group (p - 1) X\<^esub>" + using homology_exactness_axiom_2 [of p X S] Bcarr by (auto simp: kernel_def) + finally have "?hi_XT C = \\<^bsub>homology_group (p - 1) X\<^esub>" . + then obtain D where Dcarr: "D \ carrier ?G3" and Deq: "hom_boundary p X T D = C" + using homology_exactness_axiom_2 [of p X T] Ccarr + by (auto simp: kernel_def image_iff set_eq_iff) meson + interpret hb: group_hom "?G2" "homology_group (p-1) (subtopology X S)" + "hom_boundary p X S" + using hom_boundary_hom group_hom_axioms_def group_hom_def by fastforce + let ?A = "B \\<^bsub>?G2\<^esub> inv\<^bsub>?G2\<^esub> ?h2 D" + have "\A' \ carrier (homology_group p X). hom_induced p X {} X S id A' = A" + if "A \ carrier ?G2" + "hom_boundary p X S A = one (homology_group (p - 1) (subtopology X S))" for A + using that homology_exactness_axiom_1 [of p X S] + by (simp add: kernel_def subtopology_subtopology image_iff set_eq_iff) meson + moreover + have "?A \ carrier ?G2" + by (simp add: Bcarr abelian_relative_homology_group comm_groupE(1) hom_induced_carrier) + moreover have "hom_boundary p X S (?h2 D) = hom_boundary p X S B" + by (metis (mono_tags, lifting) Ceq Deq comp_eq_dest continuous_map_id iTS naturality_hom_induced) + then have "hom_boundary p X S ?A = one (homology_group (p - 1) (subtopology X S))" + by (simp add: hom_induced_carrier Bcarr) + ultimately obtain W where Wcarr: "W \ carrier (homology_group p X)" + and Weq: "hom_induced p X {} X S id W = ?A" + by blast + let ?W = "D \\<^bsub>?G3\<^esub> hom_induced p X {} X T id W" + show ?thesis + proof + interpret comm_group "?G2" + by (rule abelian_relative_homology_group) + have "B = (?h2 \ hom_induced p X {} X T id) W \\<^bsub>?G2\<^esub> ?h2 D" + apply (simp add: hom_induced_compose [symmetric] assms) + by (metis Bcarr Weq hb.G.inv_solve_right hom_induced_carrier) + then have "B \\<^bsub>?G2\<^esub> inv\<^bsub>?G2\<^esub> ?h2 D + = ?h2 (hom_induced p X {} X T id W)" + by (simp add: hb.G.m_assoc hom_induced_carrier) + then show "B = ?h2 ?W" + apply (simp add: Dcarr hom_induced_carrier hom_mult [OF hom_induced_hom]) + by (metis Bcarr hb.G.inv_solve_right hom_induced_carrier m_comm) + show "?W \ carrier ?G3" + by (simp add: Dcarr abelian_relative_homology_group comm_groupE(1) hom_induced_carrier) + qed + qed + ultimately show ?thesis + by (auto simp: group_hom_def group_hom_axioms_def hom_induced_hom group_homomorphism_hom_relboundary) +qed + + +proposition homology_exactness_triple_2: + assumes "T \ S" + shows "exact_seq ([relative_homology_group(p - 1) X T, + relative_homology_group(p - 1) (subtopology X S) T, + relative_homology_group p X S], + [hom_induced (p - 1) (subtopology X S) T X T id, hom_relboundary p X S T])" + (is "exact_seq ([?G1,?G2,?G3], [?h1,?h2])") +proof - + let ?H2 = "homology_group (p - 1) (subtopology X S)" + have iTS: "id ` T \ S" and [simp]: "S \ T = T" + using assms by auto + have "?h2 C \ kernel ?G2 ?G1 ?h1" for C + proof - + have "?h1 (?h2 C) + = (hom_induced (p - 1) X {} X T id \ hom_induced (p - 1) (subtopology X S) {} X {} id \ hom_boundary p X S) C" + unfolding hom_relboundary_def + by (metis (no_types, lifting) comp_apply continuous_map_id continuous_map_id_subt empty_subsetI hom_induced_compose id_apply image_empty image_id order_refl) + also have "\ = \\<^bsub>?G1\<^esub>" + proof - + have *: "hom_boundary p X S C \ carrier ?H2" + by (simp add: hom_boundary_carrier) + moreover have "hom_boundary p X S C \ hom_boundary p X S ` carrier ?G3" + using homology_exactness_axiom_2 [of p X S] * + apply (simp add: kernel_def set_eq_iff) + by (metis group_relative_homology_group hom_boundary_default hom_one image_eqI) + ultimately + have 1: "hom_induced (p - 1) (subtopology X S) {} X {} id (hom_boundary p X S C) + = \\<^bsub>homology_group (p - 1) X\<^esub>" + using homology_exactness_axiom_2 [of p X S] by (simp add: kernel_def) blast + show ?thesis + by (simp add: 1 hom_one [OF hom_induced_hom]) + qed + finally have "?h1 (?h2 C) = \\<^bsub>?G1\<^esub>" . + then show ?thesis + by (simp add: kernel_def hom_relboundary_def hom_induced_carrier) + qed + moreover have "x \ ?h2 ` carrier ?G3" if "x \ kernel ?G2 ?G1 ?h1" for x + proof - + let ?homX = "hom_induced (p - 1) (subtopology X S) {} X {} id" + let ?homXS = "hom_induced (p - 1) (subtopology X S) {} (subtopology X S) T id" + have "x \ carrier (relative_homology_group (p - 1) (subtopology X S) T)" + using that by (simp add: kernel_def) + moreover + have "hom_boundary (p-1) X T \ hom_induced (p-1) (subtopology X S) T X T id = hom_boundary (p-1) (subtopology X S) T" + by (metis Int_lower2 \S \ T = T\ continuous_map_id_subt hom_relboundary_def hom_relboundary_empty id_apply image_id naturality_hom_induced subtopology_subtopology) + then have "hom_boundary (p - 1) (subtopology X S) T x = \\<^bsub>homology_group (p - 2) (subtopology (subtopology X S) T)\<^esub>" + using naturality_hom_induced [of "subtopology X S" X id T T "p-1"] that + hom_one [OF hom_boundary_hom group_relative_homology_group group_relative_homology_group, of "p-1" X T] + apply (simp add: kernel_def subtopology_subtopology) + by (metis comp_apply) + ultimately + obtain y where ycarr: "y \ carrier ?H2" + and yeq: "?homXS y = x" + using homology_exactness_axiom_1 [of "p-1" "subtopology X S" T] + by (simp add: kernel_def image_def set_eq_iff) meson + have "?homX y \ carrier (homology_group (p - 1) X)" + by (simp add: hom_induced_carrier) + moreover + have "(hom_induced (p - 1) X {} X T id \ ?homX) y = \\<^bsub>relative_homology_group (p - 1) X T\<^esub>" + apply (simp flip: hom_induced_compose) + using hom_induced_compose [of "subtopology X S" "subtopology X S" id "{}" T X id T "p-1"] + apply simp + by (metis (mono_tags, lifting) kernel_def mem_Collect_eq that yeq) + then have "hom_induced (p - 1) X {} X T id (?homX y) = \\<^bsub>relative_homology_group (p - 1) X T\<^esub>" + by simp + ultimately obtain z where zcarr: "z \ carrier (homology_group (p - 1) (subtopology X T))" + and zeq: "hom_induced (p - 1) (subtopology X T) {} X {} id z = ?homX y" + using homology_exactness_axiom_3 [of "p-1" X T] + by (auto simp: kernel_def dest!: equalityD1 [of "Collect _"]) + have *: "\t. \t \ carrier ?H2; + hom_induced (p - 1) (subtopology X S) {} X {} id t = \\<^bsub>homology_group (p - 1) X\<^esub>\ + \ t \ hom_boundary p X S ` carrier ?G3" + using homology_exactness_axiom_2 [of p X S] + by (auto simp: kernel_def dest!: equalityD1 [of "Collect _"]) + interpret comm_group "?H2" + by (rule abelian_relative_homology_group) + interpret gh: group_hom ?H2 "homology_group (p - 1) X" "hom_induced (p-1) (subtopology X S) {} X {} id" + by (meson group_hom_axioms_def group_hom_def group_relative_homology_group hom_induced) + let ?yz = "y \\<^bsub>?H2\<^esub> inv\<^bsub>?H2\<^esub> hom_induced (p - 1) (subtopology X T) {} (subtopology X S) {} id z" + have yzcarr: "?yz \ carrier ?H2" + by (simp add: hom_induced_carrier ycarr) + have yzeq: "hom_induced (p - 1) (subtopology X S) {} X {} id ?yz = \\<^bsub>homology_group (p - 1) X\<^esub>" + apply (simp add: hom_induced_carrier ycarr gh.inv_solve_right') + by (metis assms continuous_map_id_subt hom_induced_compose_empty inf.absorb_iff2 o_apply o_id subtopology_subtopology zeq) + obtain w where wcarr: "w \ carrier ?G3" and weq: "hom_boundary p X S w = ?yz" + using * [OF yzcarr yzeq] by blast + interpret gh2: group_hom ?H2 ?G2 ?homXS + by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom) + have "?homXS (hom_induced (p - 1) (subtopology X T) {} (subtopology X S) {} id z) + = \\<^bsub>relative_homology_group (p - 1) (subtopology X S) T\<^esub>" + using homology_exactness_axiom_3 [of "p-1" "subtopology X S" T] zcarr + by (auto simp: kernel_def subtopology_subtopology) + then show ?thesis + apply (rule_tac x=w in image_eqI) + apply (simp_all add: hom_relboundary_def weq wcarr) + by (metis gh2.hom_inv gh2.hom_mult gh2.inv_one gh2.r_one group.inv_closed group_l_invI hom_induced_carrier l_inv_ex ycarr yeq) + qed + ultimately show ?thesis + by (auto simp: group_hom_axioms_def group_hom_def group_homomorphism_hom_relboundary hom_induced_hom) +qed + +proposition homology_exactness_triple_3: + assumes "T \ S" + shows "exact_seq ([relative_homology_group p X S, + relative_homology_group p X T, + relative_homology_group p (subtopology X S) T], + [hom_induced p X T X S id, hom_induced p (subtopology X S) T X T id])" + (is "exact_seq ([?G1,?G2,?G3], [?h1,?h2])") +proof - + have iTS: "id ` T \ S" and [simp]: "S \ T = T" + using assms by auto + have 1: "?h2 x \ kernel ?G2 ?G1 ?h1" for x + proof - + have "?h1 (?h2 x) + = (hom_induced p (subtopology X S) S X S id \ + hom_induced p (subtopology X S) T (subtopology X S) S id) x" + by (metis comp_eq_dest_lhs continuous_map_id continuous_map_id_subt hom_induced_compose iTS id_apply image_subsetI) + also have "\ = \\<^bsub>relative_homology_group p X S\<^esub>" + proof - + have "trivial_group (relative_homology_group p (subtopology X S) S)" + using trivial_relative_homology_group_topspace [of p "subtopology X S"] + by (metis inf_right_idem relative_homology_group_restrict topspace_subtopology) + then have 1: "hom_induced p (subtopology X S) T (subtopology X S) S id x + = \\<^bsub>relative_homology_group p (subtopology X S) S\<^esub>" + using hom_induced_carrier by (fastforce simp add: trivial_group_def) + show ?thesis + by (simp add: 1 hom_one [OF hom_induced_hom]) + qed + finally have "?h1 (?h2 x) = \\<^bsub>relative_homology_group p X S\<^esub>" . + then show ?thesis + by (simp add: hom_induced_carrier kernel_def) + qed + moreover have "x \ ?h2 ` carrier ?G3" if x: "x \ kernel ?G2 ?G1 ?h1" for x + proof - + have xcarr: "x \ carrier ?G2" + using that by (auto simp: kernel_def) + interpret G2: comm_group "?G2" + by (rule abelian_relative_homology_group) + let ?b = "hom_boundary p X T x" + have bcarr: "?b \ carrier(homology_group(p - 1) (subtopology X T))" + by (simp add: hom_boundary_carrier) + have "hom_boundary p X S (hom_induced p X T X S id x) + = hom_induced (p - 1) (subtopology X T) {} (subtopology X S) {} id + (hom_boundary p X T x)" + using naturality_hom_induced [of X X id T S p] by (simp add: assms o_def) meson + with bcarr have "hom_boundary p X T x \ hom_boundary p (subtopology X S) T ` carrier ?G3" + using homology_exactness_axiom_2 [of p "subtopology X S" T] x + apply (simp add: kernel_def set_eq_iff subtopology_subtopology) + by (metis group_relative_homology_group hom_boundary_hom hom_one set_eq_iff) + then obtain u where ucarr: "u \ carrier ?G3" + and ueq: "hom_boundary p X T x = hom_boundary p (subtopology X S) T u" + by (auto simp: kernel_def set_eq_iff subtopology_subtopology hom_boundary_carrier) + define y where "y = x \\<^bsub>?G2\<^esub> inv\<^bsub>?G2\<^esub> ?h2 u" + have ycarr: "y \ carrier ?G2" + using x by (simp add: y_def kernel_def hom_induced_carrier) + interpret hb: group_hom ?G2 "homology_group (p-1) (subtopology X T)" "hom_boundary p X T" + by (simp add: group_hom_axioms_def group_hom_def hom_boundary_hom) + have yyy: "hom_boundary p X T y = \\<^bsub>homology_group (p - 1) (subtopology X T)\<^esub>" + apply (simp add: y_def bcarr xcarr hom_induced_carrier hom_boundary_carrier hb.inv_solve_right') + using naturality_hom_induced [of concl: p X T "subtopology X S" T id] + apply (simp add: o_def fun_eq_iff subtopology_subtopology) + by (metis hom_boundary_carrier hom_induced_id ueq) + then have "y \ hom_induced p X {} X T id ` carrier (homology_group p X)" + using homology_exactness_axiom_1 [of p X T] x ycarr by (auto simp: kernel_def) + then obtain z where zcarr: "z \ carrier (homology_group p X)" + and zeq: "hom_induced p X {} X T id z = y" + by auto + interpret gh1: group_hom ?G2 ?G1 ?h1 + by (meson group_hom_axioms_def group_hom_def group_relative_homology_group hom_induced) + + have "hom_induced p X {} X S id z = (hom_induced p X T X S id \ hom_induced p X {} X T id) z" + by (simp add: assms flip: hom_induced_compose) + also have "\ = \\<^bsub>relative_homology_group p X S\<^esub>" + using x 1 by (simp add: kernel_def zeq y_def) + finally have "hom_induced p X {} X S id z = \\<^bsub>relative_homology_group p X S\<^esub>" . + then have "z \ hom_induced p (subtopology X S) {} X {} id ` + carrier (homology_group p (subtopology X S))" + using homology_exactness_axiom_3 [of p X S] zcarr by (auto simp: kernel_def) + then obtain w where wcarr: "w \ carrier (homology_group p (subtopology X S))" + and weq: "hom_induced p (subtopology X S) {} X {} id w = z" + by blast + let ?u = "hom_induced p (subtopology X S) {} (subtopology X S) T id w \\<^bsub>?G3\<^esub> u" + show ?thesis + proof + have *: "x = z \\<^bsub>?G2\<^esub> u" + if "z = x \\<^bsub>?G2\<^esub> inv\<^bsub>?G2\<^esub> u" "z \ carrier ?G2" "u \ carrier ?G2" for z u + using that by (simp add: group.inv_solve_right xcarr) + have eq: "?h2 \ hom_induced p (subtopology X S) {} (subtopology X S) T id + = hom_induced p X {} X T id \ hom_induced p (subtopology X S) {} X {} id" + by (simp flip: hom_induced_compose) + show "x = hom_induced p (subtopology X S) T X T id ?u" + apply (simp add: hom_mult [OF hom_induced_hom] hom_induced_carrier ucarr) + apply (rule *) + using eq apply (simp_all add: fun_eq_iff hom_induced_carrier flip: y_def zeq weq) + done + show "?u \ carrier (relative_homology_group p (subtopology X S) T)" + by (simp add: abelian_relative_homology_group comm_groupE(1) hom_induced_carrier ucarr) + qed + qed + ultimately show ?thesis + by (auto simp: group_hom_axioms_def group_hom_def hom_induced_hom) +qed + +end + + diff -r a93e6472ac9c -r c4f2cac288d2 src/HOL/Homology/Simplices.thy --- a/src/HOL/Homology/Simplices.thy Tue Apr 09 16:59:00 2019 +0000 +++ b/src/HOL/Homology/Simplices.thy Tue Apr 09 21:05:48 2019 +0100 @@ -4,6 +4,7 @@ imports "HOL-Analysis.Abstract_Euclidean_Space" "HOL-Algebra.Free_Abelian_Groups" begin + subsection\Standard simplices, all of which are topological subspaces of @{text"R^n"}. \ type_synonym 'a chain = "((nat \ real) \ 'a) \\<^sub>0 int" @@ -2781,5 +2782,501 @@ qed qed + +subsection\Homotopy invariance\ + +theorem homotopic_imp_homologous_rel_chain_maps: + assumes hom: "homotopic_with (\h. h ` T \ V) S U f g" and c: "singular_relcycle p S T c" + shows "homologous_rel p U V (chain_map p f c) (chain_map p g c)" +proof - + note sum_atMost_Suc [simp del] + have contf: "continuous_map S U f" and contg: "continuous_map S U g" + using homotopic_with_imp_continuous_maps [OF hom] by metis+ + obtain h where conth: "continuous_map (prod_topology (top_of_set {0..1::real}) S) U h" + and h0: "\x. h(0, x) = f x" + and h1: "\x. h(1, x) = g x" + and hV: "\t x. \0 \ t; t \ 1; x \ T\ \ h(t,x) \ V" + using hom by (fastforce simp: homotopic_with_def) + define vv where "vv \ \j i. if i = Suc j then 1 else (0::real)" + define ww where "ww \ \j i. if i=0 \ i = Suc j then 1 else (0::real)" + define simp where "simp \ \q i. oriented_simplex (Suc q) (\j. if j \ i then vv j else ww(j -1))" + define pr where "pr \ \q c. \i\q. frag_cmul ((-1) ^ i) + (frag_of (simplex_map (Suc q) (\z. h(z 0, c(z \ Suc))) (simp q i)))" + have ss_ss: "simplicial_simplex (Suc q) ({x. x 0 \ {0..1} \ (x \ Suc) \ standard_simplex q}) (simp q i)" + if "i \ q" for q i + proof - + have "(\j\Suc q. (if j \ i then vv j 0 else ww (j -1) 0) * x j) \ {0..1}" + if "x \ standard_simplex (Suc q)" for x + proof - + have "(\j\Suc q. if j \ i then 0 else x j) \ sum x {..Suc q}" + using that unfolding standard_simplex_def + by (force intro!: sum_mono) + with \i \ q\ that show ?thesis + by (simp add: vv_def ww_def standard_simplex_def if_distrib [of "\u. u * _"] sum_nonneg cong: if_cong) + qed + moreover + have "(\k. \j\Suc q. (if j \ i then vv j k else ww (j -1) k) * x j) \ Suc \ standard_simplex q" + if "x \ standard_simplex (Suc q)" for x + proof - + have card: "({..q} \ {k. Suc k = j}) = {j-1}" if "0 < j" "j \ Suc q" for j + using that by auto + have eq: "(\j\Suc q. \k\q. if j \ i then if k = j then x j else 0 else if Suc k = j then x j else 0) + = (\j\Suc q. x j)" + by (rule sum.cong [OF refl]) (use \i \ q\ in \simp add: sum.If_cases card\) + have "(\j\Suc q. if j \ i then if k = j then x j else 0 else if Suc k = j then x j else 0) + \ sum x {..Suc q}" for k + using that unfolding standard_simplex_def + by (force intro!: sum_mono) + then show ?thesis + using \i \ q\ that + by (simp add: vv_def ww_def standard_simplex_def if_distrib [of "\u. u * _"] sum_nonneg + sum.swap [where A = "atMost q"] eq cong: if_cong) + qed + ultimately show ?thesis + by (simp add: that simplicial_simplex_oriented_simplex simp_def image_subset_iff if_distribR) + qed + obtain prism where prism: "\q. prism q 0 = 0" + "\q c. singular_chain q S c \ singular_chain (Suc q) U (prism q c)" + "\q c. singular_chain q (subtopology S T) c + \ singular_chain (Suc q) (subtopology U V) (prism q c)" + "\q c. singular_chain q S c + \ chain_boundary (Suc q) (prism q c) = + chain_map q g c - chain_map q f c - prism (q -1) (chain_boundary q c)" + proof + show "(frag_extend \ pr) q 0 = 0" for q + by (simp add: pr_def) + next + show "singular_chain (Suc q) U ((frag_extend \ pr) q c)" + if "singular_chain q S c" for q c + using that [unfolded singular_chain_def] + proof (induction c rule: frag_induction) + case (one m) + show ?case + proof (simp add: pr_def, intro singular_chain_cmul singular_chain_sum) + fix i :: "nat" + assume "i \ {..q}" + define X where "X = subtopology (powertop_real UNIV) {x. x 0 \ {0..1} \ (x \ Suc) \ standard_simplex q}" + show "singular_chain (Suc q) U + (frag_of (simplex_map (Suc q) (\z. h (z 0, m (z \ Suc))) (simp q i)))" + unfolding singular_chain_of + proof (rule singular_simplex_simplex_map) + show "singular_simplex (Suc q) X (simp q i)" + unfolding X_def using \i \ {..q}\ simplicial_imp_singular_simplex ss_ss by blast + have 0: "continuous_map X (top_of_set {0..1}) (\x. x 0)" + unfolding continuous_map_in_subtopology topspace_subtopology X_def + by (auto intro: continuous_map_product_projection continuous_map_from_subtopology) + have 1: "continuous_map X S (m \ (\x j. x (Suc j)))" + proof (rule continuous_map_compose) + have "continuous_map (powertop_real UNIV) (powertop_real UNIV) (\x j. x (Suc j))" + by (auto intro: continuous_map_product_projection) + then show "continuous_map X (subtopology (powertop_real UNIV) (standard_simplex q)) (\x j. x (Suc j))" + unfolding X_def o_def + by (auto simp: continuous_map_in_subtopology intro: continuous_map_from_subtopology continuous_map_product_projection) + qed (use one in \simp add: singular_simplex_def\) + show "continuous_map X U (\z. h (z 0, m (z \ Suc)))" + apply (rule continuous_map_compose [unfolded o_def, OF _ conth]) + using 0 1 by (simp add: continuous_map_pairwise o_def) + qed + qed + next + case (diff a b) + then show ?case + apply (simp add: frag_extend_diff keys_diff) + using singular_chain_def singular_chain_diff by blast + qed auto + next + show "singular_chain (Suc q) (subtopology U V) ((frag_extend \ pr) q c)" + if "singular_chain q (subtopology S T) c" for q c + using that [unfolded singular_chain_def] + proof (induction c rule: frag_induction) + case (one m) + show ?case + proof (simp add: pr_def, intro singular_chain_cmul singular_chain_sum) + fix i :: "nat" + assume "i \ {..q}" + define X where "X = subtopology (powertop_real UNIV) {x. x 0 \ {0..1} \ (x \ Suc) \ standard_simplex q}" + show "singular_chain (Suc q) (subtopology U V) + (frag_of (simplex_map (Suc q) (\z. h (z 0, m (z \ Suc))) (simp q i)))" + unfolding singular_chain_of + proof (rule singular_simplex_simplex_map) + show "singular_simplex (Suc q) X (simp q i)" + unfolding X_def using \i \ {..q}\ simplicial_imp_singular_simplex ss_ss by blast + have 0: "continuous_map X (top_of_set {0..1}) (\x. x 0)" + unfolding continuous_map_in_subtopology topspace_subtopology X_def + by (auto intro: continuous_map_product_projection continuous_map_from_subtopology) + have 1: "continuous_map X (subtopology S T) (m \ (\x j. x (Suc j)))" + proof (rule continuous_map_compose) + have "continuous_map (powertop_real UNIV) (powertop_real UNIV) (\x j. x (Suc j))" + by (auto intro: continuous_map_product_projection) + then show "continuous_map X (subtopology (powertop_real UNIV) (standard_simplex q)) (\x j. x (Suc j))" + unfolding X_def o_def + by (auto simp: continuous_map_in_subtopology intro: continuous_map_from_subtopology continuous_map_product_projection) + show "continuous_map (subtopology (powertop_real UNIV) (standard_simplex q)) (subtopology S T) m" + using one continuous_map_into_fulltopology by (auto simp: singular_simplex_def) + qed + have "continuous_map X (subtopology U V) (h \ (\z. (z 0, m (z \ Suc))))" + proof (rule continuous_map_compose) + show "continuous_map X (prod_topology (top_of_set {0..1::real}) (subtopology S T)) (\z. (z 0, m (z \ Suc)))" + using 0 1 by (simp add: continuous_map_pairwise o_def) + have "continuous_map (subtopology (prod_topology euclideanreal S) ({0..1} \ T)) U h" + by (metis conth continuous_map_from_subtopology subtopology_Times subtopology_topspace) + with hV show "continuous_map (prod_topology (top_of_set {0..1::real}) (subtopology S T)) (subtopology U V) h" + by (force simp: topspace_subtopology continuous_map_in_subtopology subtopology_restrict subtopology_Times) + qed + then show "continuous_map X (subtopology U V) (\z. h (z 0, m (z \ Suc)))" + by (simp add: o_def) + qed + qed + next + case (diff a b) + then show ?case + by (metis comp_apply frag_extend_diff singular_chain_diff) + qed auto + next + show "chain_boundary (Suc q) ((frag_extend \ pr) q c) = + chain_map q g c - chain_map q f c - (frag_extend \ pr) (q -1) (chain_boundary q c)" + if "singular_chain q S c" for q c + using that [unfolded singular_chain_def] + proof (induction c rule: frag_induction) + case (one m) + have eq2: "Sigma S T = (\i. (i,i)) ` {i \ S. i \ T i} \ (Sigma S (\i. T i - {i}))" for S :: "nat set" and T + by force + have 1: "(\(i,j)\(\i. (i, i)) ` {i. i \ q \ i \ Suc q}. + frag_cmul (((-1) ^ i) * (-1) ^ j) + (frag_of + (singular_face (Suc q) j + (simplex_map (Suc q) (\z. h (z 0, m (z \ Suc))) (simp q i))))) + + (\(i,j)\(\i. (i, i)) ` {i. i \ q}. + frag_cmul (- ((-1) ^ i * (-1) ^ j)) + (frag_of + (singular_face (Suc q) (Suc j) + (simplex_map (Suc q) (\z. h (z 0, m (z \ Suc))) (simp q i))))) + = frag_of (simplex_map q g m) - frag_of (simplex_map q f m)" + proof - + have "restrict ((\z. h (z 0, m (z \ Suc))) \ (simp q 0 \ simplical_face 0)) (standard_simplex q) + = restrict (g \ m) (standard_simplex q)" + proof (rule restrict_ext) + fix x + assume x: "x \ standard_simplex q" + have "(\j\Suc q. if j = 0 then 0 else x (j - Suc 0)) = (\j\q. x j)" + by (simp add: sum_atMost_Suc_shift) + with x have "simp q 0 (simplical_face 0 x) 0 = 1" + apply (simp add: oriented_simplex_def simp_def simplical_face_in_standard_simplex) + apply (simp add: simplical_face_def if_distrib ww_def standard_simplex_def cong: if_cong) + done + moreover + have "(\n. if n \ q then x n else 0) = x" + using standard_simplex_def x by auto + then have "(\n. simp q 0 (simplical_face 0 x) (Suc n)) = x" + unfolding oriented_simplex_def simp_def ww_def using x + apply (simp add: simplical_face_in_standard_simplex) + apply (simp add: simplical_face_def if_distrib) + apply (simp add: if_distribR if_distrib cong: if_cong) + done + ultimately show "((\z. h (z 0, m (z \ Suc))) \ (simp q 0 \ simplical_face 0)) x = (g \ m) x" + by (simp add: o_def h1) + qed + then have a: "frag_of (singular_face (Suc q) 0 (simplex_map (Suc q) (\z. h (z 0, m (z \ Suc))) (simp q 0))) + = frag_of (simplex_map q g m)" + by (simp add: singular_face_simplex_map) (simp add: simplex_map_def) + have "restrict ((\z. h (z 0, m (z \ Suc))) \ (simp q q \ simplical_face (Suc q))) (standard_simplex q) + = restrict (f \ m) (standard_simplex q)" + proof (rule restrict_ext) + fix x + assume x: "x \ standard_simplex q" + then have "simp q q (simplical_face (Suc q) x) 0 = 0" + unfolding oriented_simplex_def simp_def + by (simp add: simplical_face_in_standard_simplex sum_atMost_Suc) (simp add: simplical_face_def vv_def) + moreover have "(\n. simp q q (simplical_face (Suc q) x) (Suc n)) = x" + unfolding oriented_simplex_def simp_def vv_def using x + apply (simp add: simplical_face_in_standard_simplex) + apply (force simp: standard_simplex_def simplical_face_def if_distribR if_distrib [of "\x. x * _"] sum_atMost_Suc cong: if_cong) + done + ultimately show "((\z. h (z 0, m (z \ Suc))) \ (simp q q \ simplical_face (Suc q))) x = (f \ m) x" + by (simp add: o_def h0) + qed + then have b: "frag_of (singular_face (Suc q) (Suc q) + (simplex_map (Suc q) (\z. h (z 0, m (z \ Suc))) (simp q q))) + = frag_of (simplex_map q f m)" + by (simp add: singular_face_simplex_map) (simp add: simplex_map_def) + have sfeq: "simplex_map q (\z. h (z 0, m (z \ Suc))) (simp q (Suc i) \ simplical_face (Suc i)) + = simplex_map q (\z. h (z 0, m (z \ Suc))) (simp q i \ simplical_face (Suc i))" + if "i < q" for i + unfolding simplex_map_def + proof (rule restrict_ext) + fix x + assume "x \ standard_simplex q" + then have "(simp q (Suc i) \ simplical_face (Suc i)) x = (simp q i \ simplical_face (Suc i)) x" + unfolding oriented_simplex_def simp_def simplical_face_def + by (force intro: sum.cong) + then show "((\z. h (z 0, m (z \ Suc))) \ (simp q (Suc i) \ simplical_face (Suc i))) x + = ((\z. h (z 0, m (z \ Suc))) \ (simp q i \ simplical_face (Suc i))) x" + by simp + qed + have eqq: "{i. i \ q \ i \ Suc q} = {..q}" + by force + have qeq: "{..q} = insert 0 ((\i. Suc i) ` {i. i < q})" "{i. i \ q} = insert q {i. i < q}" + using le_imp_less_Suc less_Suc_eq_0_disj by auto + show ?thesis + using a b + apply (simp add: sum.reindex inj_on_def eqq) + apply (simp add: qeq sum.insert_if sum.reindex sum_negf singular_face_simplex_map sfeq) + done + qed + have 2: "(\(i,j)\(SIGMA i:{..q}. {0..min (Suc q) i} - {i}). + frag_cmul ((-1) ^ i * (-1) ^ j) + (frag_of + (singular_face (Suc q) j + (simplex_map (Suc q) (\z. h (z 0, m (z \ Suc))) (simp q i))))) + + (\(i,j)\(SIGMA i:{..q}. {i..q} - {i}). + frag_cmul (- ((-1) ^ i * (-1) ^ j)) + (frag_of + (singular_face (Suc q) (Suc j) + (simplex_map (Suc q) (\z. h (z 0, m (z \ Suc))) (simp q i))))) + = - frag_extend (pr (q - Suc 0)) (chain_boundary q (frag_of m))" + proof (cases "q=0") + case True + then show ?thesis + by (simp add: chain_boundary_def flip: sum.Sigma) + next + case False + have eq: "{..q - Suc 0} \ {..q} = Sigma {..q - Suc 0} (\i. {0..min q i}) \ Sigma {..q} (\i. {i<..q})" + by force + have I: "(\(i,j)\(SIGMA i:{..q}. {0..min (Suc q) i} - {i}). + frag_cmul ((-1) ^ (i + j)) + (frag_of + (singular_face (Suc q) j + (simplex_map (Suc q) (\z. h (z 0, m (z \ Suc))) (simp q i))))) + = (\(i,j)\(SIGMA i:{..q - Suc 0}. {0..min q i}). + frag_cmul (- ((-1) ^ (j + i))) + (frag_of + (simplex_map q (\z. h (z 0, singular_face q j m (z \ Suc))) + (simp (q - Suc 0) i))))" + proof - + have seq: "simplex_map q (\z. h (z 0, singular_face q j m (z \ Suc))) + (simp (q - Suc 0) (i - Suc 0)) + = simplex_map q (\z. h (z 0, m (z \ Suc))) (simp q i \ simplical_face j)" + if ij: "i \ q" "j \ i" "j \ i" for i j + unfolding simplex_map_def + proof (rule restrict_ext) + fix x + assume x: "x \ standard_simplex q" + have "i > 0" + using that by force + then have iq: "i - Suc 0 \ q - Suc 0" + using \i \ q\ False by simp + have q0_eq: "{..Suc q} = insert 0 (Suc ` {..q})" + by (auto simp: image_def gr0_conv_Suc) + have \: "simp (q - Suc 0) (i - Suc 0) x 0 = simp q i (simplical_face j x) 0" + using False x ij + unfolding oriented_simplex_def simp_def vv_def ww_def + apply (simp add: simplical_face_in_standard_simplex) + apply (force simp: simplical_face_def q0_eq sum.reindex intro!: sum.cong) + done + have \: "simplical_face j (simp (q - Suc 0) (i - Suc 0) x \ Suc) = simp q i (simplical_face j x) \ Suc" + proof + fix k + show "simplical_face j (simp (q - Suc 0) (i - Suc 0) x \ Suc) k + = (simp q i (simplical_face j x) \ Suc) k" + using False x ij + unfolding oriented_simplex_def simp_def o_def vv_def ww_def + apply (simp add: simplical_face_in_standard_simplex if_distribR) + apply (simp add: simplical_face_def if_distrib [of "\u. u * _"] cong: if_cong) + apply (intro impI conjI) + apply (force simp: sum_atMost_Suc intro: sum.cong) + apply (force simp: q0_eq sum.reindex intro!: sum.cong) + done + qed + have "simp (q - Suc 0) (i - Suc 0) x \ Suc \ standard_simplex (q - Suc 0)" + using ss_ss [OF iq] \i \ q\ False \i > 0\ + apply (simp add: simplicial_simplex image_subset_iff) + using \x \ standard_simplex q\ by blast + then show "((\z. h (z 0, singular_face q j m (z \ Suc))) \ simp (q - Suc 0) (i - Suc 0)) x + = ((\z. h (z 0, m (z \ Suc))) \ (simp q i \ simplical_face j)) x" + by (simp add: singular_face_def \ \) + qed + have [simp]: "(-1::int) ^ (i + j - Suc 0) = - ((-1) ^ (i + j))" if "i \ j" for i j::nat + proof - + have "i + j > 0" + using that by blast + then show ?thesis + by (metis (no_types, hide_lams) One_nat_def Suc_diff_1 add.inverse_inverse mult.left_neutral mult_minus_left power_Suc) + qed + show ?thesis + apply (rule sum.eq_general_inverses [where h = "\(a,b). (a-1,b)" and k = "\(a,b). (Suc a,b)"]) + using False apply (auto simp: singular_face_simplex_map seq add.commute) + done + qed + have *: "singular_face (Suc q) (Suc j) (simplex_map (Suc q) (\z. h (z 0, m (z \ Suc))) (simp q i)) + = simplex_map q (\z. h (z 0, singular_face q j m (z \ Suc))) (simp (q - Suc 0) i)" + if ij: "i < j" "j \ q" for i j + proof - + have iq: "i \ q - Suc 0" + using that by auto + have sf_eqh: "singular_face (Suc q) (Suc j) + (\x. if x \ standard_simplex (Suc q) + then ((\z. h (z 0, m (z \ Suc))) \ simp q i) x else undefined) x + = h (simp (q - Suc 0) i x 0, + singular_face q j m (\xa. simp (q - Suc 0) i x (Suc xa)))" + if x: "x \ standard_simplex q" for x + proof - + let ?f = "\k. \j\q. if j \ i then if k = j then x j else 0 + else if Suc k = j then x j else 0" + have fm: "simplical_face (Suc j) x \ standard_simplex (Suc q)" + using ss_ss [OF iq] that ij + by (simp add: simplical_face_in_standard_simplex) + have ss: "?f \ standard_simplex (q - Suc 0)" + unfolding standard_simplex_def + proof (intro CollectI conjI impI allI) + fix k + show "0 \ ?f k" + using that by (simp add: sum_nonneg standard_simplex_def) + show "?f k \ 1" + using x sum_le_included [of "{..q}" "{..q}" x "id"] + by (simp add: standard_simplex_def) + assume k: "q - Suc 0 < k" + show "?f k = 0" + by (rule sum.neutral) (use that x iq k standard_simplex_def in auto) + next + have "(\k\q - Suc 0. ?f k) + = (\(k,j) \ ({..q - Suc 0} \ {..q}) \ {(k,j). if j \ i then k = j else Suc k = j}. x j)" + apply (simp add: sum.Sigma) + by (rule sum.mono_neutral_cong) (auto simp: split: if_split_asm) + also have "\ = sum x {..q}" + apply (rule sum.eq_general_inverses + [where h = "\(k,j). if j\i \ k=j \ j>i \ Suc k = j then j else Suc q" + and k = "\j. if j \ i then (j,j) else (j - Suc 0, j)"]) + using ij by auto + also have "\ = 1" + using x by (simp add: standard_simplex_def) + finally show "(\k\q - Suc 0. ?f k) = 1" + by (simp add: standard_simplex_def) + qed + let ?g = "\k. if k \ i then 0 + else if k < Suc j then x k + else if k = Suc j then 0 else x (k - Suc 0)" + have eq: "{..Suc q} = {..j} \ {Suc j} \ Suc`{j<..q}" "{..q} = {..j} \ {j<..q}" + using ij image_iff less_Suc_eq_0_disj less_Suc_eq_le + by (force simp: image_iff)+ + then have "(\k\Suc q. ?g k) = (\k\{..j} \ {Suc j} \ Suc`{j<..q}. ?g k)" + by simp + also have "\ = (\k\{..j} \ Suc`{j<..q}. ?g k)" + by (rule sum.mono_neutral_right) auto + also have "\ = (\k\{..j}. ?g k) + (\k\Suc`{j<..q}. ?g k)" + by (rule sum.union_disjoint) auto + also have "\ = (\k\{..j}. ?g k) + (\k\{j<..q}. ?g (Suc k))" + by (auto simp: sum.reindex) + also have "\ = (\k\{..j}. if k \ i then 0 else x k) + + (\k\{j<..q}. if k \ i then 0 else x k)" + by (intro sum.cong arg_cong2 [of concl: "(+)"]) (use ij in auto) + also have "\ = (\k\q. if k \ i then 0 else x k)" + unfolding eq by (subst sum.union_disjoint) auto + finally have "(\k\Suc q. ?g k) = (\k\q. if k \ i then 0 else x k)" . + then have QQ: "(\l\Suc q. if l \ i then 0 else simplical_face (Suc j) x l) = (\j\q. if j \ i then 0 else x j)" + by (simp add: simplical_face_def cong: if_cong) + have WW: "(\k. \l\Suc q. if l \ i + then if k = l then simplical_face (Suc j) x l else 0 + else if Suc k = l then simplical_face (Suc j) x l + else 0) + = simplical_face j + (\k. \j\q. if j \ i then if k = j then x j else 0 + else if Suc k = j then x j else 0)" + proof - + have *: "(\l\q. if l \ i then 0 else if Suc k = l then x (l - Suc 0) else 0) + = (\l\q. if l \ i then if k - Suc 0 = l then x l else 0 else if k = l then x l else 0)" + (is "?lhs = ?rhs") + if "k \ q" "k > j" for k + proof (cases "k \ q") + case True + have "?lhs = sum (\l. x (l - Suc 0)) {Suc k}" "?rhs = sum x {k}" + by (rule sum.mono_neutral_cong_right; use True ij that in auto)+ + then show ?thesis + by simp + next + case False + have "?lhs = 0" "?rhs = 0" + by (rule sum.neutral; use False ij in auto)+ + then show ?thesis + by simp + qed + show ?thesis + apply (rule ext) + unfolding simplical_face_def using ij + apply (auto simp: sum_atMost_Suc cong: if_cong) + apply (force simp flip: ivl_disj_un(2) intro: sum.neutral) + apply (auto simp: *) + done + qed + show ?thesis + using False that iq + unfolding oriented_simplex_def simp_def vv_def ww_def + apply (simp add: if_distribR cong: if_cong) + apply (simp add: simplical_face_def if_distrib [of "\u. u * _"] o_def cong: if_cong) + apply (simp add: singular_face_def fm ss QQ WW) + done + qed + show ?thesis + unfolding simplex_map_def restrict_def + apply (rule ext) + apply (simp add: simplicial_simplex image_subset_iff o_def sf_eqh) + apply (simp add: singular_face_def) + done + qed + have sgeq: "(SIGMA i:{..q}. {i..q} - {i}) = (SIGMA i:{..q}. {i<..q})" + by force + have II: "(\(i,j)\(SIGMA i:{..q}. {i..q} - {i}). + frag_cmul (- ((-1) ^ (i + j))) + (frag_of + (singular_face (Suc q) (Suc j) + (simplex_map (Suc q) (\z. h (z 0, m (z \ Suc))) (simp q i))))) = + (\(i,j)\(SIGMA i:{..q}. {i<..q}). + frag_cmul (- ((-1) ^ (j + i))) + (frag_of + (simplex_map q (\z. h (z 0, singular_face q j m (z \ Suc))) + (simp (q - Suc 0) i))))" + by (force simp: * sgeq add.commute intro: sum.cong) + show ?thesis + using False + apply (simp add: chain_boundary_def frag_extend_sum frag_extend_cmul frag_cmul_sum pr_def flip: sum_negf power_add) + apply (subst sum.swap [where A = "{..q}"]) + apply (simp add: sum.cartesian_product eq sum.union_disjoint disjoint_iff_not_equal I II) + done + qed + have *: "\a+b = w; c+d = -z\ \ (a + c) + (b+d) = w-z" for a b w c d z :: "'c \\<^sub>0 int" + by (auto simp: algebra_simps) + have eq: "{..q} \ {..Suc q} = + Sigma {..q} (\i. {0..min (Suc q) i}) + \ Sigma {..q} (\i. {Suc i..Suc q})" + by force + show ?case + apply (subst pr_def) + apply (simp add: chain_boundary_sum chain_boundary_cmul) + apply (subst chain_boundary_def) + apply (simp add: frag_cmul_sum sum.cartesian_product eq sum.union_disjoint disjoint_iff_not_equal + sum.atLeast_Suc_atMost_Suc_shift del: sum_cl_ivl_Suc flip: comm_monoid_add_class.sum.Sigma) + apply (simp add: comm_monoid_add_class.sum.Sigma eq2 [of _ "\i. {_ i.._ i}"]) + apply (simp add: sum.union_disjoint disjoint_iff_not_equal * [OF 1 2]) + done + next + case (diff a b) + then show ?case + by (simp add: chain_boundary_diff frag_extend_diff chain_map_diff) + qed auto + qed + have *: "singular_chain p (subtopology U V) (prism (p - Suc 0) (chain_boundary p c))" + if "singular_chain p S c" "singular_chain (p - Suc 0) (subtopology S T) (chain_boundary p c)" + proof (cases "p") + case 0 then show ?thesis by (simp add: chain_boundary_def prism) + next + case (Suc p') + with prism that show ?thesis by auto + qed + then show ?thesis + using c + unfolding singular_relcycle_def homologous_rel_def singular_relboundary_def mod_subset_def + apply (rule_tac x="- prism p c" in exI) + by (simp add: chain_boundary_minus prism(2) prism(4) singular_chain_minus) +qed + end