# HG changeset patch # User paulson # Date 1713116383 -3600 # Node ID 2ff4cc7fa70a19bce04cc2febcb73257f30f212c # Parent c111785fd6407c8a6e96ce8b3532748ef763eabc More tidying and removal of "apply" diff -r c111785fd640 -r 2ff4cc7fa70a src/HOL/Homology/Homology_Groups.thy --- a/src/HOL/Homology/Homology_Groups.thy Fri Apr 12 22:19:27 2024 +0100 +++ b/src/HOL/Homology/Homology_Groups.thy Sun Apr 14 18:39:43 2024 +0100 @@ -124,8 +124,7 @@ 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) + by (simp add: Collect_mono group.subgroup_of_subgroup_generated singular_relboundary_imp_relcycle subgroup_singular_relboundary) lemma normal_subgroup_singular_relboundary_relcycle: "(singular_relboundary_set p X S) \ (relcycle_group p X S)" @@ -288,7 +287,7 @@ 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))) + (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))" @@ -323,7 +322,7 @@ 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))" + (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)" @@ -337,13 +336,10 @@ 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) + 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 + by (metis "1" "2" homologous_rel_restrict relative_homology_group_restrict singular_relcycle_def subtopology_restrict) qed ultimately show ?thesis by auto @@ -408,25 +404,24 @@ 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 "chain_map p f \ hom (relcycle_group p X S) (relcycle_group p Y T)" + by (metis contf fim hom_chain_map relcycle_group_restrict) + then have 1: "?f \ hom (relcycle_group p X S) (relative_homology_group (int p) Y T)" + by (simp add: hom_compose normal.r_coset_hom_Mod normal_subgroup_singular_relboundary_relcycle relative_homology_group_def) 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)) + have "homologous_rel p X S x y" + by (metis (no_types) homologous_rel_set_eq right_coset_singular_relboundary that(3)) + then have "singular_relboundary p Y T (chain_map p f (x - y))" + using singular_relboundary_chain_map [OF _ contf fim] by (simp add: homologous_rel_def) 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 + by (metis comp_apply homologous_rel_def homologous_rel_set_eq right_coset_singular_relboundary) 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)" @@ -501,9 +496,7 @@ 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 + by (metis (mono_tags, lifting)) 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)" @@ -676,9 +669,7 @@ 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 + by (simp add: comm_group.abelian_FactGroup relative_homology_group_def subgroup_singular_relboundary_relcycle) lemma abelian_homology_group: "comm_group(homology_group p X)" by simp @@ -783,10 +774,7 @@ 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 + by (simp add: cbm ceq contf hom_boundary_chain_boundary hom_induced_chain_map p1_eq sb sr) next case False with assms show ?thesis @@ -850,10 +838,8 @@ \ 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 + using hom_induced_chain_map chain_map_ident [of _ X] singular_relcycle + by (smt (verit) bot.extremum comp_apply continuous_map_id image_cong image_empty mem_Collect_eq) 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)})" @@ -861,10 +847,9 @@ 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) + {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" + using singular_cycle singular_relcycle by (fastforce simp: singular_boundary) next fix c assume c: "c \ singular_relcycle_set (Suc n) X S \ @@ -905,9 +890,9 @@ 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) + 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 @@ -937,9 +922,7 @@ 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 + by (intro 2) (auto simp: hom_induced_chain_map chain_map_ident homologous_rel_set_eq_relboundary singular_relcycle) finally show ?thesis . qed then show ?thesis @@ -957,9 +940,8 @@ 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 + unfolding relative_homology_group_def + by (simp add: group_hom.kernel_to_trivial_group group_hom_axioms_def group_hom_def hom_induced_trivial) next case False then obtain n where peq: "p = int n" @@ -975,11 +957,7 @@ \ 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 + by (smt (verit) chain_map_ident continuous_map_id_subt empty_subsetI hom_induced_chain_map image_cong image_empty image_image mem_Collect_eq singular_relcycle) also have "\ = homologous_rel_set n X {} ` (singular_relcycle_set n X {} \ singular_relboundary_set n X S)" proof (rule 2) fix c @@ -1074,10 +1052,8 @@ 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 + with assms homotopic_imp_homologous_rel_chain_maps show ?thesis + by (force simp add: peq hom_induced_chain_map_gen cont im homologous_rel_set_eq) qed (simp add: hom_induced_default) qed qed @@ -1166,11 +1142,10 @@ 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" + obtain "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) + by (metis add_diff_cancel_left' e g hSuc singular_chain_boundary_alt) then show "singular_chain n (subtopology (subtopology X (S - U)) (T - U)) c2" by (fastforce simp add: singular_chain_subtopology) qed @@ -1194,18 +1169,21 @@ 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 + using scc' chain_map_ident [of _ "subtopology X S"] c' homologous_rel_set_eq + by fastforce qed + have "(\x. homologous_rel_set n (subtopology X S) T (chain_map n id x)) ` + 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" + by (force simp: cont h singular_relcycle_chain_map) + then 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 + by (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 @@ -1263,10 +1241,10 @@ 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) - +proof (rule monoid.equality) + show "carrier (relcycle_group 0 X {}) = carrier (chain_group 0 X)" + by (simp add: Collect_mono chain_boundary_def singular_cycle subset_antisym) +qed (simp_all add: relcycle_group_def chain_group_def) proposition iso_cycle_group_sum: assumes disj: "pairwise disjnt \" and UU: "\\ = topspace X" @@ -1336,10 +1314,8 @@ 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 + using iso B unfolding Group.iso_def + by (smt (verit, del_insts) Int_iff bij_betw_def image_iff mem_Collect_eq subset_antisym subset_iff) qed (auto simp: assms iso_chain_group_sum) then show ?thesis by (simp add: relcycle_group_def sum_group_subgroup_generated subgroup_singular_relcycle) @@ -1388,15 +1364,11 @@ 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 + by (smt (verit) PiE_restrict c homologous_rel_eq_relboundary restrict_apply restrict_ext singular_relboundary_0 z) 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) + using z c by (intro finite_subset [OF _ fin]) auto 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}}" @@ -1413,24 +1385,26 @@ 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 + by (intro Pi_I) (force simp: peq carrier_sum_group carrier_relative_homology_group singular_chain_subtopology singular_cycle) 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 + proof (rule gfinprod_cong [OF refl Pi_I]) + fix i + show "i \ \ =simp=> hom_induced (int n) (subtopology X i) {} X {} id ((\S\\. homologous_rel_set n (subtopology X S) {} (z S)) i) + = homologous_rel_set n X {} (z i)" + using that + by (auto simp: peq simp_implies_def carrier_sum_group PiE_def Pi_def chain_map_ident singular_cycle hom_induced_chain_map) + qed (simp add: hom_induced_carrier peq) 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 + proof - + have "homologous_rel_set n X {} 0 = singular_relboundary_set n X {}" + by (metis homologous_rel_eq_relboundary singular_relboundary_0) + with hom_pi peq show ?thesis + by (intro gfinprod_mono_neutral_cong_right) auto + qed also have "\ = ?rhs" proof - have "gfinprod (homology_group p X) (\S. homologous_rel_set n X {} (z S)) \ @@ -1440,8 +1414,7 @@ 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) + by (metis homologous_rel_eq_relboundary one_relative_homology_group peq singular_relboundary_0) then show ?case by simp next @@ -1455,10 +1428,13 @@ show ?case using insert z proof (simp add: pi) + have "\x. homologous_rel n X {} (z S + sum z \) x + \ \u v. homologous_rel n X {} (z S) u \ homologous_rel n X {} (sum z \) v \ x = u + v" + by (metis (no_types, lifting) diff_add_cancel diff_diff_eq2 homologous_rel_def homologous_rel_refl) + with insert z 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) + using insert z by (auto simp: peq homologous_rel_add mult_relative_homology_group) qed qed with fin show ?thesis @@ -1516,10 +1492,8 @@ 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 + by (force intro!: restrict_ext simp add: singular_boundary relative_homology_group_def homologous_rel_set_eq_relboundary peq) qed show "x = (\S\\. \\<^bsub>homology_group p (subtopology X S)\<^esub>)" using x 1 carrSG gf @@ -1557,12 +1531,10 @@ "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 + then have *: "\B. \openin X T; T \ B \ C = {}; C \ T \ B; openin X B\ \ B \ C = {}" + by (meson connectedin disjnt_def disjnt_sym path_connectedin_imp_connectedin) have "C \ Union \" - using \C \ topspace X\ UU by blast + by (simp add: UU \compactin X C\ compactin_subset_topspace) moreover have "\ (\ - {T}) \ C = {}" proof (rule *) show "T \ \ (\ - {T}) \ C = {}" @@ -1596,11 +1568,12 @@ 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 + euclideanreal (\x. x 0)" + by (metis (mono_tags) UNIV_I continuous_map_from_subtopology continuous_map_product_projection) + then have "continuous_map (subtopology (powertop_real UNIV) (standard_simplex (Suc 0))) + (top_of_set {0..1}) (\x. x 0)" + unfolding continuous_map_in_subtopology g + by (auto simp: continuous_map_in_subtopology standard_simplex_def g) moreover have "continuous_map (top_of_set {0..1}) X g" using contg by blast ultimately show ?thesis @@ -1692,9 +1665,7 @@ 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 + by (simp add: ff normal.FactGroup_int_pow normal_subgroup_singular_relboundary_relcycle relative_homology_group_def srf) qed show ?thesis apply (subst GH.iso_iff) @@ -1817,17 +1788,13 @@ 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 + by (simp add: contf contg fim gim hom_induced_compose' hom_induced_id) 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 + by (simp add: contf contg fim gim hom_induced_compose' hom_induced_id) qed (auto simp: hom_induced_hom) @@ -1846,8 +1813,7 @@ 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 + using assms by (intro homotopy_equivalence_relative_homology_group_isomorphism) auto lemma homotopy_equivalent_space_imp_isomorphic_relative_homology_groups: assumes "continuous_map X Y f" and fim: "f ` S \ T" @@ -1885,8 +1851,8 @@ 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)" + "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 @@ -1956,10 +1922,7 @@ 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 + by (metis comp_apply cont continuous_map_compose gf hom_induced_id_gen) qed qed @@ -1983,10 +1946,7 @@ 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 + by (metis comp_def cont continuous_map_compose fg hom_induced_id_gen) qed moreover have "(hom_induced p Y {} X {} g x) \ carrier (homology_group p X)" @@ -2011,9 +1971,7 @@ 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) + using assms by (simp add: homeomorphic_map_relative_homology_iso) (*See also hom_hom_induced_inclusion*) lemma inj_on_hom_induced_inclusion: @@ -2037,20 +1995,14 @@ 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 + using exact_seq_mon_eq_triviality inj_on_hom_induced_inclusion [OF assms] + by (metis exact_seq_cons_iff homology_exactness_axiom_1 homology_exactness_axiom_2) 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 + using exact_seq_epi_eq_triviality trivial_homomorphism_hom_boundary_inclusion + by (metis assms exact_seq_cons_iff homology_exactness_axiom_1 homology_exactness_axiom_2) (*different in HOL Light because we don't need short_exact_sequence*) lemmas short_exact_sequence_hom_induced_inclusion = homology_exactness_axiom_3 @@ -2222,54 +2174,49 @@ 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_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)" + \ 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))" + 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)" + 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)" + "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 + by (simp add: ext hom_boundary_carrier hom_induced_id hom_relboundary_def) 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_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" + 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 + with assms show ?thesis + by (metis (no_types, lifting) fun.map_comp hom_relboundary_def naturality_hom_induced) qed proposition homology_exactness_triple_1: assumes "T \ S" - shows "exact_seq ([relative_homology_group(p - 1) (subtopology X S) T, + 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])" @@ -2279,43 +2226,43 @@ 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) {})" + 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 + 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]) + using naturality_hom_induced [OF continuous_map_id iTS] + by (smt (verit, best) * comp_apply hom_induced_carrier hom_relboundary_def kernel_def mem_Collect_eq) 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 = + 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" + 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" + 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)" + = 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)" + = 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>" + 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>" . + 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 @@ -2325,7 +2272,7 @@ 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 + "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 @@ -2333,7 +2280,7 @@ 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))" + 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" @@ -2343,17 +2290,14 @@ 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) + have "hom_induced p X T X S id (hom_induced p X {} X T id W) = hom_induced p X {} X S id W" + by (simp add: assms hom_induced_compose') + then have "B = (?h2 \ hom_induced p X {} X T id) W \\<^bsub>?G2\<^esub> ?h2 D" + by (simp add: Bcarr Weq 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) + by (metis hom_mult [OF hom_induced_hom] Dcarr comp_apply hom_induced_carrier m_comm) show "?W \ carrier ?G3" - by (simp add: Dcarr abelian_relative_homology_group comm_groupE(1) hom_induced_carrier) + by (simp add: Dcarr comm_groupE(1) hom_induced_carrier) qed qed ultimately show ?thesis @@ -2363,19 +2307,19 @@ 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, + 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])" + [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)" + 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" + = (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>" @@ -2387,8 +2331,8 @@ 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>" + 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]) @@ -2399,58 +2343,60 @@ 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)" + 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>" + 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) + by (smt (verit) assms comp_apply inf.absorb_iff2 kernel_def mem_Collect_eq subtopology_subtopology) 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)" + 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>" + have "(hom_induced (p-1) X {} X T id \ ?homX) y = \\<^bsub>relative_homology_group (p-1) X T\<^esub>" + using that + apply (simp add: kernel_def flip: hom_induced_compose) + using hom_induced_compose [of "subtopology X S" "subtopology X S" id "{}" T X id T "p-1"] yeq + by auto + 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" + 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>\ + 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" + 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" + 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') + have "hom_induced (p-1) (subtopology X S) {} X {} id y = + hom_induced (p-1) (subtopology X S) {} X {} id + (hom_induced (p-1) (subtopology X T) {} (subtopology X S) {} id z)" by (metis assms continuous_map_id_subt hom_induced_compose_empty inf.absorb_iff2 o_apply o_id subtopology_subtopology zeq) + then have yzeq: "hom_induced (p-1) (subtopology X S) {} X {} id ?yz = \\<^bsub>homology_group (p-1) X\<^esub>" + by (simp add: hom_induced_carrier ycarr gh.inv_solve_right') 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>" + 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 @@ -2500,10 +2446,10 @@ 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))" + 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_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" @@ -2518,11 +2464,11 @@ 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>" + 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) + by (smt (verit, best) \S \ T = T\ bcarr comp_eq_dest continuous_map_id_subt hom_induced_id id_apply + image_subset_iff subtopology_subtopology 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)" @@ -2552,10 +2498,8 @@ = 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 + using hom_mult [OF hom_induced_hom] hom_induced_carrier * + by (smt (verit, best) comp_eq_dest eq ucarr weq y_def zeq) 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 diff -r c111785fd640 -r 2ff4cc7fa70a src/HOL/Homology/Simplices.thy --- a/src/HOL/Homology/Simplices.thy Fri Apr 12 22:19:27 2024 +0100 +++ b/src/HOL/Homology/Simplices.thy Sun Apr 14 18:39:43 2024 +0100 @@ -1133,11 +1133,7 @@ using assms by (force simp: simplicial_simplex_def) moreover have "singular_face p k f = oriented_simplex (p - Suc 0) (\i. if i < k then m i else m (Suc i))" - unfolding feq singular_face_def oriented_simplex_def - apply (simp add: simplical_face_in_standard_simplex [OF p] restrict_compose_left subset_eq) - using sum.zero_middle [OF p, where 'a=real, symmetric] unfolding simplical_face_def o_def - apply (simp add: if_distrib [of "\x. _ * x"] if_distrib [of "\f. f _ * _"] atLeast0AtMost cong: if_cong) - done + using feq p singular_face_oriented_simplex by auto ultimately show ?thesis using p simplicial_simplex_def singular_simplex_singular_face by blast @@ -1174,10 +1170,10 @@ "\p v l. simplex_cone p v (oriented_simplex p l) = oriented_simplex (Suc p) (\i. if i = 0 then v else l(i -1))" proof - - have *: "\x. \y. \v. (\l. oriented_simplex (Suc x) (\i. if i = 0 then v else l (i -1))) - = (y v \ (oriented_simplex x))" - apply (subst choice_iff [symmetric]) - by (simp add: oriented_simplex_eq choice_iff [symmetric] function_factors_left [symmetric]) + have *: "\x. \xv. \y. (\l. oriented_simplex (Suc x) + (\i. if i = 0 then xv else l (i - 1))) = + y \ oriented_simplex x" + by (simp add: oriented_simplex_eq flip: choice_iff function_factors_left) then show ?thesis unfolding o_def by (metis(no_types)) qed @@ -1528,12 +1524,12 @@ proof (induction p arbitrary: d c f x y) case (Suc p) define Sigp where "Sigp \ \f:: (nat \ real) \ nat \ real. \i. (\j\Suc p. simplicial_vertex j f i) / real (p + 2)" - let ?CB = "\f. chain_boundary (Suc p) (frag_of f)" + define CB where "CB \ \f::(nat \ real) \ nat \ real. chain_boundary (Suc p) (frag_of f)" have *: "Poly_Mapping.keys (simplicial_cone p (Sigp f) - (simplicial_subdivision p (?CB f))) + (simplicial_subdivision p (CB f))) \ {f. \x\standard_simplex (Suc p). \y\standard_simplex (Suc p). - \f x k - f y k\ \ real (Suc p) / (real p + 2) * d}" (is "?lhs \ ?rhs") + \f x k - f y k\ \ Suc p / (real p + 2) * d}" (is "?lhs \ ?rhs") if f: "f \ Poly_Mapping.keys c" for f proof - have ssf: "simplicial_simplex (Suc p) S f" @@ -1541,22 +1537,24 @@ have 2: "\x y. \x \ standard_simplex (Suc p); y \ standard_simplex (Suc p)\ \ \f x k - f y k\ \ d" by (meson Suc.prems(2) f subsetD le_Suc_eq order_refl standard_simplex_mono) have sub: "Poly_Mapping.keys ((frag_of \ simplex_cone p (Sigp f)) g) \ ?rhs" - if "g \ Poly_Mapping.keys (simplicial_subdivision p (?CB f))" for g + if "g \ Poly_Mapping.keys (simplicial_subdivision p (CB f))" for g proof - - have 1: "simplicial_chain p S (?CB f)" + have 1: "simplicial_chain p S (CB f)" + unfolding CB_def using ssf simplicial_chain_boundary simplicial_chain_of by fastforce have "simplicial_chain (Suc p) (f ` standard_simplex(Suc p)) (frag_of f)" by (metis simplicial_chain_of simplicial_simplex ssf subset_refl) - then have sc_sub: "Poly_Mapping.keys (?CB f) + then have sc_sub: "Poly_Mapping.keys (CB f) \ Collect (simplicial_simplex p (f ` standard_simplex (Suc p)))" - by (metis diff_Suc_1 simplicial_chain_boundary simplicial_chain_def) - have led: "\h x y. \h \ Poly_Mapping.keys (chain_boundary (Suc p) (frag_of f)); + by (metis diff_Suc_1 simplicial_chain_boundary simplicial_chain_def CB_def) + have led: "\h x y. \h \ Poly_Mapping.keys (CB f); x \ standard_simplex p; y \ standard_simplex p\ \ \h x k - h y k\ \ d" using Suc.prems(2) f sc_sub by (simp add: simplicial_simplex subset_iff image_iff) metis - have "\f' x y. \f' \ Poly_Mapping.keys (simplicial_subdivision p (?CB f)); x \ standard_simplex p; y \ standard_simplex p\ + have "\f' x y. \f' \ Poly_Mapping.keys (simplicial_subdivision p (CB f)); + x \ standard_simplex p; y \ standard_simplex p\ \ \f' x k - f' y k\ \ (p / (Suc p)) * d" - by (blast intro: led Suc.IH [of "chain_boundary (Suc p) (frag_of f)", OF 1]) + by (blast intro: led Suc.IH [of "CB f", OF 1]) then have g: "\x y. \x \ standard_simplex p; y \ standard_simplex p\ \ \g x k - g y k\ \ (p / (Suc p)) * d" using that by blast have "d \ 0" @@ -1668,16 +1666,16 @@ unfolding simplicial_chain_def simplicial_cone_def by (simp add: order_trans [OF keys_frag_extend] sub UN_subset_iff) qed - show ?case - using Suc - apply (simp del: sum.atMost_Suc) - apply (drule subsetD [OF keys_frag_extend]) - apply (simp del: sum.atMost_Suc) - apply clarify (*OBTAIN?*) - apply (rename_tac FFF) - using * - apply (simp add: add.commute Sigp_def subset_iff) - done + obtain ff where "ff \ Poly_Mapping.keys c" + "f \ Poly_Mapping.keys + (simplicial_cone p + (\i. (\j\Suc p. simplicial_vertex j ff i) / + (real p + 2)) + (simplicial_subdivision p (CB ff)))" + using Suc.prems(3) subsetD [OF keys_frag_extend] + by (force simp: CB_def simp del: sum.atMost_Suc) + then show ?case + using Suc * by (simp add: add.commute Sigp_def subset_iff) qed (auto simp: standard_simplex_0) @@ -1715,22 +1713,27 @@ (subtopology (powertop_real UNIV) S) id" using continuous_map_from_subtopology_mono continuous_map_id by blast moreover have "\l. restrict id (standard_simplex p) = oriented_simplex p l" - apply (rule_tac x="\i j. if i = j then 1 else 0" in exI) - apply (force simp: oriented_simplex_def standard_simplex_def if_distrib [of "\u. u * _"] cong: if_cong) - done + proof + show "restrict id (standard_simplex p) = oriented_simplex p (\i j. if i = j then 1 else 0)" + by (force simp: oriented_simplex_def standard_simplex_def if_distrib [of "\u. u * _"] cong: if_cong) + qed ultimately show ?lhs by (simp add: simplicial_simplex_def singular_simplex_def) qed lemma singular_chain_singular_subdivision: - "singular_chain p X c - \ singular_chain p X (singular_subdivision p c)" + assumes "singular_chain p X c" + shows "singular_chain p X (singular_subdivision p c)" unfolding singular_subdivision_def - apply (rule singular_chain_extend) - apply (rule singular_chain_chain_map [where X = "subtopology (powertop_real UNIV) - (standard_simplex p)"]) - apply (simp add: simplicial_chain_simplicial_subdivision simplicial_imp_singular_chain) - by (simp add: singular_chain_def singular_simplex_def subset_iff) +proof (rule singular_chain_extend) + fix ca + assume "ca \ Poly_Mapping.keys c" + with assms have "singular_simplex p X ca" + by (simp add: singular_chain_def subset_iff) + then show "singular_chain p X (chain_map p ca (simplicial_subdivision p (frag_of (restrict id (standard_simplex p)))))" + unfolding singular_simplex_def + by (metis order_refl simplicial_chain_of simplicial_chain_simplicial_subdivision simplicial_imp_singular_chain simplicial_simplex_id singular_chain_chain_map) +qed lemma naturality_singular_subdivision: "singular_chain p X c @@ -1783,11 +1786,8 @@ qed then show ?case using f one - apply (auto simp: simplicial_simplex_def) - apply (rule singular_simplex_simplex_map - [where X = "subtopology (powertop_real UNIV) (standard_simplex q)"]) - unfolding singular_simplex_def apply (fastforce simp add:)+ - done + apply (simp add: simplicial_simplex_def) + using singular_simplex_def singular_simplex_simplex_map by blast next case (diff a b) then show ?case @@ -1847,9 +1847,15 @@ (simplicial_subdivision p (chain_boundary (Suc p) (frag_of (restrict id (standard_simplex (Suc p)))))) = simplicial_subdivision p (chain_boundary (Suc p) (frag_of f))" - apply (simp add: chain_boundary_chain_map [OF scp] del: chain_map_of - flip: singular_simplex_chain_map_id [OF simplicial_imp_singular_simplex [OF ssf]]) - by (metis (no_types) scp singular_chain_boundary_alt Suc.IH [OF scps] Suc.IH [OF scpf] naturality_singular_subdivision) + proof - + have "singular_simplex (Suc p) (subtopology (powertop_real UNIV) S) f" + using simplicial_simplex_def ssf by blast + then have "chain_map (Suc p) f (frag_of (restrict id (standard_simplex (Suc p)))) = frag_of f" + using singular_simplex_chain_map_id by blast + then show ?thesis + by (metis (no_types) Suc.IH chain_boundary_chain_map diff_Suc_Suc diff_zero + naturality_singular_subdivision scp scpf scps simplicial_imp_singular_chain) + qed show ?case apply (simp add: singular_subdivision_def del: sum.atMost_Suc) apply (simp only: ssf 1 2 3 4 chain_map_simplicial_cone [of "Suc p" S _ p "Suc p"]) @@ -1861,8 +1867,8 @@ lemma naturality_simplicial_subdivision: "\simplicial_chain p (standard_simplex q) c; simplicial_simplex q S g\ \ simplicial_subdivision p (chain_map p g c) = chain_map p g (simplicial_subdivision p c)" -apply (simp flip: singular_subdivision_simplicial_simplex) - by (metis naturality_singular_subdivision simplicial_chain_chain_map simplicial_imp_singular_chain singular_subdivision_simplicial_simplex) + by (metis naturality_singular_subdivision simplicial_chain_chain_map simplicial_imp_singular_chain + singular_subdivision_simplicial_simplex) lemma chain_boundary_singular_subdivision: "singular_chain p X c @@ -1925,12 +1931,21 @@ by (metis diff_0 subd_0 subd_diff) lemma subd_power_uminus: "subd p (frag_cmul ((-1) ^ k) c) = frag_cmul ((-1) ^ k) (subd p c)" - apply (induction k, simp_all) - by (metis minus_frag_cmul subd_uminus) +proof (induction k) + case 0 + then show ?case by simp +next + case (Suc k) + then show ?case + by (metis frag_cmul_cmul frag_cmul_minus_one power_Suc subd_uminus) +qed lemma subd_power_sum: "subd p (sum f I) = sum (subd p \ f) I" - apply (induction I rule: infinite_finite_induct) - by auto (metis add_diff_cancel_left' diff_add_cancel subd_diff) +proof (induction I rule: infinite_finite_induct) + case (insert i I) + then show ?case + by (metis (no_types, lifting) comp_apply diff_minus_eq_add subd_diff subd_uminus sum.insert) +qed auto lemma subd: "simplicial_chain p (standard_simplex s) c \ (\r g. simplicial_simplex s (standard_simplex r) g \ chain_map (Suc p) g (subd p c) = subd p (chain_map p g c)) @@ -2007,16 +2022,13 @@ = subd p (chain_boundary (Suc p) (frag_of (simplex_map (Suc p) g f)))" by (metis (no_types) One_nat_def scf Suc.IH chain_boundary_chain_map chain_map_of diff_Suc_Suc diff_zero g simplicial_chain_boundary simplicial_imp_singular_chain) show "chain_map (Suc (Suc p)) g (subd (Suc p) (frag_of f)) = subd (Suc p) (chain_map (Suc p) g (frag_of f))" - using g - apply (simp only: subd.simps frag_extend_of) + unfolding subd.simps frag_extend_of + using g apply (subst chain_map_simplicial_cone [of s "standard_simplex r" _ "Suc p" s], assumption) - apply (intro simplicial_chain_diff) - using "1" apply auto[1] - using one.hyps apply auto[1] - apply (metis Suc.IH diff_Suc_1 mem_Collect_eq one.hyps simplicial_chain_boundary simplicial_chain_of) + apply (metis "1" Suc.IH diff_Suc_1 scf simplicial_chain_boundary simplicial_chain_diff) using "**" apply auto[1] apply (rule order_refl) - apply (simp only: chain_map_of frag_extend_of) + unfolding chain_map_of frag_extend_of apply (rule arg_cong2 [where f = "simplicial_cone (Suc p)"]) apply (simp add: geq sum_distrib_left oriented_simplex_def ** del: sum.atMost_Suc flip: sum_divide_distrib) using 2 apply (simp only: oriented_simplex_def sum.swap [where A = "{..s}"]) @@ -2033,26 +2045,27 @@ by (metis (no_types) Suc.IH diff_Suc_1 scf simplicial_chain_boundary) show "simplicial_chain (Suc (Suc p)) (standard_simplex s) (subd (Suc p) (frag_of f))" using one - apply (simp only: subd.simps frag_extend_of) + unfolding subd.simps frag_extend_of apply (rule_tac S="standard_simplex s" in simplicial_chain_simplicial_cone) - apply (intro simplicial_chain_diff ff) - using sc apply (simp add: algebra_simps) - using "**" convex_standard_simplex apply force+ - done + apply (meson ff scf simplicial_chain_diff simplicial_chain_simplicial_subdivision) + using "**" convex_standard_simplex by force have "simplicial_chain p (standard_simplex s) (chain_boundary (Suc p) (frag_of f))" using scf simplicial_chain_boundary by fastforce then have "chain_boundary (Suc p) (simplicial_subdivision (Suc p) (frag_of f) - frag_of f - subd p (chain_boundary (Suc p) (frag_of f))) = 0" - apply (simp only: chain_boundary_diff) - using Suc.IH chain_boundary_boundary [of "Suc p" "subtopology (powertop_real UNIV) - (standard_simplex s)" "frag_of f"] - by (metis One_nat_def add_diff_cancel_left' subd_0 chain_boundary_simplicial_subdivision plus_1_eq_Suc scf simplicial_imp_singular_chain) - then show "chain_boundary (Suc (Suc p)) (subd (Suc p) (frag_of f)) + unfolding chain_boundary_diff + using Suc.IH chain_boundary_boundary + by (metis One_nat_def add_diff_cancel_left' chain_boundary_simplicial_subdivision diff_Suc_1 scf + simplicial_imp_singular_chain subd_0) + moreover have "simplicial_chain (Suc p) (standard_simplex s) + (simplicial_subdivision (Suc p) (frag_of f) - frag_of f - + subd p (chain_boundary (Suc p) (frag_of f)))" + by (meson ff scf simplicial_chain_diff simplicial_chain_simplicial_subdivision) + ultimately show "chain_boundary (Suc (Suc p)) (subd (Suc p) (frag_of f)) + subd (Suc p - Suc 0) (chain_boundary (Suc p) (frag_of f)) = simplicial_subdivision (Suc p) (frag_of f) - frag_of f" - apply (simp only: subd.simps frag_extend_of) - apply (subst chain_boundary_simplicial_cone [of "Suc p" "standard_simplex s"]) - apply (meson ff scf simplicial_chain_diff simplicial_chain_simplicial_subdivision) + unfolding subd.simps frag_extend_of + apply (simp add: chain_boundary_simplicial_cone ) apply (simp add: simplicial_cone_def del: sum.atMost_Suc simplicial_subdivision.simps) done qed @@ -2062,9 +2075,7 @@ apply safe apply (metis chain_map_diff subd_diff) apply (metis simplicial_chain_diff subd_diff) - apply (auto simp: simplicial_subdivision_diff chain_boundary_diff - simp del: simplicial_subdivision.simps subd.simps) - by (metis (no_types, lifting) add_diff_add add_uminus_conv_diff diff_0 diff_diff_add) + by (smt (verit, ccfv_threshold) add_diff_add chain_boundary_diff diff_add_cancel simplicial_subdivision_diff subd_diff) qed auto qed simp @@ -2169,9 +2180,9 @@ then show ?case using one apply (simp add: chain_map_of singular_simplex_def simplicial_simplex_def, auto) - apply (rule_tac f=frag_of in arg_cong, rule) - apply (simp add: simplex_map_def) - by (simp add: continuous_map_in_subtopology image_subset_iff singular_face_def) + apply (rule arg_cong [where f=frag_of]) + by (auto simp: image_subset_iff simplex_map_def simplicial_simplex singular_face_def) + qed (auto simp: chain_map_diff) have "?lhs = chain_map p f @@ -2347,8 +2358,7 @@ show "chain_boundary (Suc p) (?h p c) + ?h (p - Suc 0) (chain_boundary p c) = (singular_subdivision p ^^ Suc n) c - c" using chain_boundary_singular_subdivision [of "Suc p" X] apply (simp add: chain_boundary_add f5 h k algebra_simps) - apply (smt (verit, ccfv_threshold) add.commute add_diff_eq diff_add_cancel diff_diff_eq2 h(4) k(4) sc singular_subdivision_add) - done + by (smt (verit, del_insts) add.commute add.left_commute diff_add_cancel h(4) k(4) sc singular_subdivision_add) qed (auto simp: k h singular_subdivision_diff) qed @@ -2642,8 +2652,14 @@ show ?thesis proof show "homologous_rel p X S c ?c'" - apply (induction n, simp_all) - by (metis p homologous_rel_singular_subdivision homologous_rel_singular_relcycle homologous_rel_trans homologous_rel_sym) + proof (induction n) + case 0 + then show ?case by auto + next + case (Suc n) + then show ?case + by simp (metis homologous_rel_eq p homologous_rel_singular_subdivision homologous_rel_singular_relcycle) + qed then show "singular_relcycle p X S ?c'" by (metis homologous_rel_singular_relcycle p) next @@ -2760,8 +2776,7 @@ case (Suc n) then show ?case apply simp - apply (rule homologous_rel_trans) - using c homologous_rel_singular_relcycle_1 homologous_rel_singular_subdivision homologous_rel_sym by blast + by (metis c homologous_rel_eq homologous_rel_singular_relcycle_1 homologous_rel_singular_subdivision) qed auto show "homologous_rel p (subtopology X S) T 0 e" unfolding homologous_rel_def using e @@ -2871,8 +2886,7 @@ 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 + by (simp add: frag_extend_diff singular_chain_diff) qed auto next show "singular_chain (Suc q) (subtopology U V) ((frag_extend \ pr) q c)" @@ -3079,8 +3093,7 @@ 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 + by (simp add: image_subset_iff simplicial_simplex x) 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 \ \) @@ -3189,19 +3202,18 @@ then show ?thesis by simp qed + have xq: "x q = (\j\q. if j \ i then if q - Suc 0 = j then x j else 0 + else if q = j then x j else 0)" if "q\j" + using ij that + by (force simp flip: ivl_disj_un(2) intro: sum.neutral) 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 + using ij unfolding simplical_face_def + by (intro ext) (auto simp: * sum.atMost_Suc xq cong: if_cong) 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: if_distribR 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