Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Brouwer_Degree.thy Sprache: Isabelle

Original von: Isabelle^©

section\<open>Homology, III: Brouwer Degree\<close>

theory Brouwer_Degree
  imports Homology_Groups "HOL-Algebra.Multiplicative_Group"

begin

subsection\<open>Reduced Homology\<close>

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 {()}) {} (\<lambda>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 {()}) {} (\<lambda>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 {()}) {} (\<lambda>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 {()}) {} (\<lambda>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
         \<Longrightarrow> hom_induced p X {} (discrete_topology {()}) {} (\<lambda>x. ())
           = (hom_induced p Y {} (discrete_topology {()}) {} (\<lambda>x. ()) \<circ> 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 {()}) {} (\<lambda>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)
        \<Longrightarrow> hom_induced p X {} Y {} f c \<in> 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
  \<in> 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)
        \<subseteq> kernel (homology_group (p - 1) (subtopology X S))
            (homology_group (p - 1) (discrete_topology {()}))
            (hom_induced (p - 1) (subtopology X S) {}
              (discrete_topology {()}) {} (\<lambda>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 {()}) {()} (\<lambda>x. ()) c)
       = \<one>\<^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) =
        \<one>\<^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)
          \<in> 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
        \<Longrightarrow> reduced_homology_group p X \<cong> 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. ()))
           \<in> 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 \<open>auto simp: iso_kernel_image\<close>)
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 {()}) {} (\<lambda>x. ()) x'
           = \<one>\<^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 (\<lambda>x. a) \<circ>
             hom_induced p (discrete_topology {()}) {} (discrete_topology {()}) {()} id \<circ> ?g) y"
        by (simp add: a \<open>a \<in> S\<close> 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 \<open>a \<in> S\<close> flip: hom_induced_compose)
      have "?g (y \\<^bsub>?H\<^esub> inv\<^bsub>?H\<^esub> (?f \ ?g) y)
          = \<one>\<^bsub>homology_group p (discrete_topology {()})\<^esub>"
        by (simp add: a \<open>a \<in> S\<close> 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))
          = \<one>\<^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
       \<subseteq> (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))
    \<subseteq> (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 {()}) {} (\<lambda>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))
       \<subseteq> ?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\<open>More homology properties of deformations, retracts, contractible spaces\<close>

lemma iso_relative_homology_of_contractible:
   "\contractible_space X; topspace X \ S \ {}\
  \<Longrightarrow> hom_boundary p X S
      \<in> 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 \ {}\
        \<Longrightarrow> relative_homology_group p X S \<cong>
            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 \ {}\
        \<Longrightarrow> reduced_homology_group p (subtopology X S) \<cong> 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 \ {}\
      \<Longrightarrow> (hom_induced p X {} X S id) \<in> 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 \ {}\
      \<Longrightarrow> reduced_homology_group p X \<cong> 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 \ {}\
      \<Longrightarrow> relative_homology_group p X S \<cong> 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\
    \<Longrightarrow> 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\
        \<Longrightarrow> 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\
    \<Longrightarrow> (hom_induced p X U Y V r) \<in> 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\
    \<Longrightarrow> (hom_induced p Y V X U id) \<in> 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\
    \<Longrightarrow> relative_homology_group p X U \<cong> 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\
        \<Longrightarrow> homology_group p X \<cong> 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\
        \<Longrightarrow> relative_homology_group p X U \<cong> 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\
        \<Longrightarrow> homology_group p X \<cong> 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)
   \<in> 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
        \<in> 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
      \<in> carrier (homology_group p X) \<rightarrow> 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)
      \<in> 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)
      \<in> 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)
             \<in> Group.iso (subgroup_generated (homology_group p (subtopology X S)) H \<times>\<times>
                          subgroup_generated (homology_group p (subtopology X S)) K)
                         (homology_group p (subtopology X S))"
    "hom_boundary (p + 1) X S
     \<in> 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
     \<in> 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)
        \<in> Group.iso (subgroup_generated (?pXS) H \<times>\<times> 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)
      \<cong> 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)
     \<in> Group.iso (subgroup_generated (?G) H \<times>\<times> 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 \ {}\
    \<Longrightarrow> homology_group p (subtopology X S) \<cong> 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 \ {}\
        \<Longrightarrow> 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 \<open>T \<subseteq> S\<close>] homology_exactness_triple_3 [OF \<open>T \<subseteq> S\<close>]
    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)
         \<in> 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 \<open>T \<subseteq> S\<close>] homology_exactness_triple_3 [OF \<open>T \<subseteq> S\<close>]
    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
         \<in> 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 \<open>T \<subseteq> S\<close>] homology_exactness_triple_2 [OF \<open>T \<subseteq> S\<close>] 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 \<open>T \<noteq> {}\<close>
      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 \<open>T \<noteq> {}\<close> 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 \<open>T \<noteq> {}\<close>
      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 \<open>T \<noteq> {}\<close> assms group.iso_sym iso_homology_contractible_space_subtopology2)
    finally show ?thesis .
  qed
qed

subsection\<open>Homology groups of spheres\<close>

lemma iso_reduced_homology_group_lower_hemisphere:
  assumes "k \ n"
  shows "hom_induced p (nsphere n) {} (nsphere n) {x. x k \ 0} id
      \<in> iso (reduced_homology_group p (nsphere n)) (relative_homology_group p (nsphere n) {x. x k \<le> 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 \<open>k \<le> n\<close> 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 \<open>k \<le> n\<close> 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 \<open>i \<noteq> k\<close> 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)
  \<in> iso (relative_homology_group p (subtopology (nsphere n) {x. x k \<ge> 0}) {x. x k = 0})
        (relative_homology_group p (nsphere n) {x. x k \<le> 0})" (is "?h \<in> 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
         \<in> iso (relative_homology_group p ?X12 {x. -1/2 \<le> x k \<and> x k \<le> 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
                               (\<lambda>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 (\<lambda>(T, x). if 0 \<le> 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 (\<lambda>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 (\<lambda>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}))
     \<subseteq> {x. (\<Sum>i\<le>n. (x i)\<^sup>2) = 1 \<and> (\<forall>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 \<open>0 \<le> T\<close> have "k \<le> 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 \<open>k \<le> n\<close>
      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 \<open>0 \<le> T\<close>
        by (simp add: nsphere sum_diff not_le \<open>k \<le> n\<close> 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 \<open>auto simp: nsphere h\<close>)
    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 \<le> x k}) \<inter> {x. x k = 0}) ?X12
             (topspace ?X12 \<inter> {x. - 1/2 \<le> x k \<and> x k \<le> 0}) id
            \<in> iso (relative_homology_group p (subtopology (nsphere n) {x. 0 \<le> x k})
                       (topspace (subtopology (nsphere n) {x. 0 \<le> x k}) \<inter> {x. x k = 0}))
                (relative_homology_group p ?X12 (topspace ?X12 \<inter> {x. - 1/2 \<le> x k \<and> x k \<le> 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})
        \<subseteq> topspace (subtopology (nsphere n) {x. 0 \<le> x k}) \<inter> {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
                 (\<lambda>h. h ` (topspace ?X12 \<inter> {x. - 1 / 2 \<le> x k \<and> x k \<le> 0}) \<subseteq> topspace ?X12 \<inter> {x. - 1 / 2 \<le> x k \<and> x k \<le> 0})
                 ?X12 ?X12 (h \<circ> (\<lambda>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 \<le> x k \<and> x k \<le> 0} id
            \<in> Group.iso
                (relative_homology_group p (subtopology (nsphere n) {x. 0 \<le> x k}) {x. x k = 0})
                (relative_homology_group p ?X12 {x. - 1/2 \<le> x k \<and> x k \<le> 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})
  \<in> iso (relative_homology_group (1 + p) (subtopology (nsphere (Suc n)) {x. x(Suc n) \<ge> 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
      \<in> iso (reduced_homology_group p (nsphere n)) (relative_homology_group p (nsphere n) {x. x k \<ge> 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
  \<in> iso (relative_homology_group p (subtopology (nsphere n) {x. x k \<le> 0}) {x. x k = 0})
        (relative_homology_group p (nsphere n) {x. x k \<ge> 0})" (is "?k \<in> 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 \<ge> 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 \<open>r \<circ> r = id\<close> 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 \<le> x k}) \<inter> {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 \<le> x k}) {x. x k = 0} (nsphere n) {x. 0 \<le> x k} r \<circ>
          hom_induced p (subtopology (nsphere n) {x. x k \<le> 0}) {x. x k = 0} (subtopology (nsphere n) {x. 0 \<le> 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
  \<in> Group.iso ?G (relative_homology_group p (nsphere n) {f. 0 \<le> 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}
  \<in> iso (relative_homology_group (1 + p) (subtopology (nsphere (Suc n)) {x. x(Suc n) \<le> 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. (\<Sum>i\<le>n. (x i)\<^sup>2) + (x (Suc n))\<^sup>2 = 1 \<and> (\<forall>i>Suc n. x i = 0)} \<inter> {x. x (Suc n) \<le> 0} \<inter>
        {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);
     \<And>x. x \<in> carrier G1 \<Longrightarrow> r x \<in> carrier G1; group G1; group G2\<rbrakk>
      \<Longrightarrow> \<exists>f \<in> iso G2 G1. \<forall>x \<in> 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)\
   \<Longrightarrow> \<exists>f \<in> iso G1 G3. \<forall>x \<in> 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))).
        \<forall>c \<in> carrier(reduced_homology_group p (nsphere n)).
             hom_induced (1 + p) (nsphere(Suc n)) {} (nsphere(Suc n)) {}
                         (\<lambda>x i. if i = 0 then -x i else x i) (f c)
           = f (hom_induced p (nsphere n) {} (nsphere n) {} (\<lambda>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.
           \<forall>c\<in>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} \<circ>
            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)
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.22 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.