Quelle  Brouwer_Degree.thy

section‹Homology, III: Brouwer Degree›

theory Brouwer_Degree
  imports Homology_Groups "HOL-Algebra.Multiplicative_Group"

begin

subsection‹Reduced Homology›

definition reduced_homology_group :: "int ==> 'a topology ==> 'a chain set monoid"
  where "reduced_homology_group p X ≡
           subgroup_generated (homology_group p X)
             (kernel (homology_group p X) (homology_group p (discrete_topology {()}))
                     (hom_induced p X {} (discrete_topology {()}) {} (λx. ())))"

lemma one_reduced_homology_group: "1🪙reduced_homology_group p X🪙 = 1🪙homology_group p X🪙"
    by (simp add: reduced_homology_group_def)

lemma group_reduced_homology_group [simp]: "group (reduced_homology_group p X)"
    by (simp add: reduced_homology_group_def group.group_subgroup_generated)

lemma carrier_reduced_homology_group:
   "carrier (reduced_homology_group p X) =
    kernel (homology_group p X) (homology_group p (discrete_topology {()}))
           (hom_induced p X {} (discrete_topology {()}) {} (λx. ()))"
    (is "_ = kernel ?G ?H ?h")
proof -
  interpret subgroup "kernel ?G ?H ?h" ?G
  by (simp add: hom_induced_empty_hom group_hom_axioms_def group_hom_def group_hom.subgroup_kernel)
  show ?thesis
    unfolding reduced_homology_group_def
    using carrier_subgroup_generated_subgroup by blast
qed

lemma carrier_reduced_homology_group_subset:
   "carrier (reduced_homology_group p X) ⊆ carrier (homology_group p X)"
  by (simp add: group.carrier_subgroup_generated_subset reduced_homology_group_def)

lemma un_reduced_homology_group:
  assumes "p ≠ 0"
  shows "reduced_homology_group p X = homology_group p X"
proof -
  have "(kernel (homology_group p X) (homology_group p (discrete_topology {()}))
              (hom_induced p X {} (discrete_topology {()}) {} (λx. ())))
      = carrier (homology_group p X)"
  proof (rule group_hom.kernel_to_trivial_group)
    show "group_hom (homology_group p X) (homology_group p (discrete_topology {()}))
         (hom_induced p X {} (discrete_topology {()}) {} (λx. ()))"
      by (auto simp: hom_induced_empty_hom group_hom_def group_hom_axioms_def)
    show "trivial_group (homology_group p (discrete_topology {()}))"
      by (simp add: homology_dimension_axiom [OF _ assms])
  qed
  then show ?thesis
    by (simp add: reduced_homology_group_def group.subgroup_generated_group_carrier)
qed

lemma trivial_reduced_homology_group:
   "p < 0 ==> trivial_group(reduced_homology_group p X)"
  by (simp add: trivial_homology_group un_reduced_homology_group)

lemma hom_induced_reduced_hom:
   "(hom_induced p X {} Y {} f) ∈ hom (reduced_homology_group p X) (reduced_homology_group p Y)"
proof (cases "continuous_map X Y f")
  case True
  have eq: "continuous_map X Y f
         ==> hom_induced p X {} (discrete_topology {()}) {} (λx. ())
           = (hom_induced p Y {} (discrete_topology {()}) {} (λx. ()) ∘ hom_induced p X {} Y {} f)"
    by (simp flip: hom_induced_compose_empty)
  interpret subgroup "kernel (homology_group p X)
                       (homology_group p (discrete_topology {()}))
                         (hom_induced p X {} (discrete_topology {()}) {} (λx. ()))"
                     "homology_group p X"
    by (meson group_hom.subgroup_kernel group_hom_axioms_def group_hom_def group_relative_homology_group hom_induced)
  have sb: "hom_induced p X {} Y {} f ` carrier (homology_group p X) ⊆ carrier (homology_group p Y)"
    using hom_induced_carrier by blast
    show ?thesis
    using True
    unfolding reduced_homology_group_def
    apply (simp add: hom_into_subgroup_eq group_hom.subgroup_kernel hom_induced_empty_hom group.hom_from_subgroup_generated group_hom_def group_hom_axioms_def)
    unfolding kernel_def using eq sb by auto
next
  case False
  then have "hom_induced p X {} Y {} f = (λc. one(reduced_homology_group p Y))"
    by (force simp: hom_induced_default reduced_homology_group_def)
  then show ?thesis
    by (simp add: trivial_hom)
qed


lemma hom_induced_reduced:
   "c ∈ carrier(reduced_homology_group p X)
        ==> hom_induced p X {} Y {} f c ∈ carrier(reduced_homology_group p Y)"
  by (meson hom_in_carrier hom_induced_reduced_hom)

lemma hom_boundary_reduced_hom:
   "hom_boundary p X S
  ∈ hom (relative_homology_group p X S) (reduced_homology_group (p-1) (subtopology X S))"
proof -
  have *: "continuous_map X (discrete_topology {()}) (λx. ())" "(λx. ()) ∈ S → {()}"
    by auto
  interpret group_hom "relative_homology_group p (discrete_topology {()}) {()}"
                      "homology_group (p-1) (discrete_topology {()})"
                      "hom_boundary p (discrete_topology {()}) {()}"
    apply (clarsimp simp: group_hom_def group_hom_axioms_def)
    by (metis UNIV_unit hom_boundary_hom subtopology_UNIV)
  have "hom_boundary p X S `
        carrier (relative_homology_group p X S)
        ⊆ kernel (homology_group (p - 1) (subtopology X S))
            (homology_group (p - 1) (discrete_topology {()}))
            (hom_induced (p - 1) (subtopology X S) {}
              (discrete_topology {()}) {} (λx. ()))"
  proof (clarsimp simp add: kernel_def hom_boundary_carrier)
    fix c
    assume c: "c ∈ carrier (relative_homology_group p X S)"
    have triv: "trivial_group (relative_homology_group p (discrete_topology {()}) {()})"
      by (metis topspace_discrete_topology trivial_relative_homology_group_topspace)
    have "hom_boundary p (discrete_topology {()}) {()}
         (hom_induced p X S (discrete_topology {()}) {()} (λx. ()) c)
       = 1🪙homology_group (p - 1) (discrete_topology {()})🪙"
      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) =
        1🪙homology_group (p - 1) (discrete_topology {()})🪙"
      using naturality_hom_induced [OF *, of p, symmetric] by (simp add: o_def fun_eq_iff)
  qed
  then show ?thesis
    by (simp add: reduced_homology_group_def hom_boundary_hom hom_into_subgroup)
qed


lemma homotopy_equivalence_reduced_homology_group_isomorphisms:
  assumes contf: "continuous_map X Y f" and contg: "continuous_map Y X g"
    and gf: "homotopic_with (λh. True) X X (g ∘ f) id"
    and fg: "homotopic_with (λk. True) Y Y (f ∘ g) id"
  shows "group_isomorphisms (reduced_homology_group p X) (reduced_homology_group p Y)
                               (hom_induced p X {} Y {} f) (hom_induced p Y {} X {} g)"
proof (simp add: hom_induced_reduced_hom group_isomorphisms_def, intro conjI ballI)
  fix a
  assume "a ∈ carrier (reduced_homology_group p X)"
  then have "(hom_induced p Y {} X {} g ∘ hom_induced p X {} Y {} f) a = a"
    apply (simp add: contf contg flip: hom_induced_compose)
    using carrier_reduced_homology_group_subset gf hom_induced_id homology_homotopy_empty by fastforce
  then show "hom_induced p Y {} X {} g (hom_induced p X {} Y {} f a) = a"
    by simp
next
  fix b
  assume "b ∈ carrier (reduced_homology_group p Y)"
  then have "(hom_induced p X {} Y {} f ∘ hom_induced p Y {} X {} g) b = b"
    apply (simp add: contf contg flip: hom_induced_compose)
    using carrier_reduced_homology_group_subset fg hom_induced_id homology_homotopy_empty by fastforce
  then show "hom_induced p X {} Y {} f (hom_induced p Y {} X {} g b) = b"
    by (simp add: carrier_reduced_homology_group)
qed

lemma homotopy_equivalence_reduced_homology_group_isomorphism:
  assumes "continuous_map X Y f" "continuous_map Y X g"
      and "homotopic_with (λh. True) X X (g ∘ f) id" "homotopic_with (λk. True) Y Y (f ∘ g) id"
  shows "(hom_induced p X {} Y {} f)
          ∈ iso (reduced_homology_group p X) (reduced_homology_group p Y)"
proof (rule group_isomorphisms_imp_iso)
  show "group_isomorphisms (reduced_homology_group p X) (reduced_homology_group p Y)
         (hom_induced p X {} Y {} f) (hom_induced p Y {} X {} g)"
    by (simp add: assms homotopy_equivalence_reduced_homology_group_isomorphisms)
qed

lemma homotopy_equivalent_space_imp_isomorphic_reduced_homology_groups:
   "X homotopy_equivalent_space Y
        ==> reduced_homology_group p X ≅ reduced_homology_group p Y"
  unfolding homotopy_equivalent_space_def
  using homotopy_equivalence_reduced_homology_group_isomorphism is_isoI by blast

lemma homeomorphic_space_imp_isomorphic_reduced_homology_groups:
   "X homeomorphic_space Y ==> reduced_homology_group p X ≅ reduced_homology_group p Y"
  by (simp add: homeomorphic_imp_homotopy_equivalent_space homotopy_equivalent_space_imp_isomorphic_reduced_homology_groups)

lemma trivial_reduced_homology_group_empty:
   "topspace X = {} ==> trivial_group(reduced_homology_group p X)"
  by (metis carrier_reduced_homology_group_subset group.trivial_group_alt group_reduced_homology_group trivial_group_def trivial_homology_group_empty)

lemma homology_dimension_reduced:
  assumes "topspace X = {a}"
  shows "trivial_group (reduced_homology_group p X)"
proof -
  have iso: "(hom_induced p X {} (discrete_topology {()}) {} (λx. ()))
           ∈ iso (homology_group p X) (homology_group p (discrete_topology {()}))"
    apply (rule homeomorphic_map_homology_iso)
    apply (force simp: homeomorphic_map_maps homeomorphic_maps_def assms)
    done
  show ?thesis
    unfolding reduced_homology_group_def
    by (rule group.trivial_group_subgroup_generated) (use iso in ‹auto simp: iso_kernel_image›)
qed


lemma trivial_reduced_homology_group_contractible_space:
   "contractible_space X ==> trivial_group (reduced_homology_group p X)"
  apply (simp add: contractible_eq_homotopy_equivalent_singleton_subtopology)
  apply (auto simp: trivial_reduced_homology_group_empty)
  using isomorphic_group_triviality
  by (metis (full_types) group_reduced_homology_group homology_dimension_reduced homotopy_equivalent_space_imp_isomorphic_reduced_homology_groups path_connectedin_def path_connectedin_singleton topspace_subtopology_subset)


lemma image_reduced_homology_group:
  assumes "topspace X ∩ S ≠ {}"
  shows "hom_induced p X {} X S id ` carrier (reduced_homology_group p X)
       = hom_induced p X {} X S id ` carrier (homology_group p X)"
    (is "?h ` carrier ?G = ?h ` carrier ?H")
proof -
  obtain a where a: "a ∈ topspace X" and "a ∈ S"
    using assms by blast
  have [simp]: "A ∩ {x ∈ A. P x} = {x ∈ A. P x}" for A P
    by blast
  interpret comm_group "homology_group p X"
    by (rule abelian_relative_homology_group)
  have *: "∃x'. ?h y = ?h x' ∧
             x' ∈ carrier ?H ∧
             hom_induced p X {} (discrete_topology {()}) {} (λx. ()) x'
           = 1🪙homology_group p (discrete_topology {()})🪙"
    if "y ∈ carrier ?H" for y
  proof -
    let ?f = "hom_induced p (discrete_topology {()}) {} X {} (λx. a)"
    let ?g = "hom_induced p X {} (discrete_topology {()}) {} (λx. ())"
    have bcarr: "?f (?g y) ∈ carrier ?H"
      by (simp add: hom_induced_carrier)
    interpret gh1:
      group_hom "relative_homology_group p X S" "relative_homology_group p (discrete_topology {()}) {()}"
                "hom_induced p X S (discrete_topology {()}) {()} (λx. ())"
      by (meson group_hom_axioms_def group_hom_def hom_induced_hom group_relative_homology_group)
    interpret gh2:
      group_hom "relative_homology_group p (discrete_topology {()}) {()}" "relative_homology_group p X S"
                "hom_induced p (discrete_topology {()}) {()} X S (λx. a)"
      by (meson group_hom_axioms_def group_hom_def hom_induced_hom group_relative_homology_group)
    interpret gh3:
      group_hom "homology_group p X" "relative_homology_group p X S" "?h"
      by (meson group_hom_axioms_def group_hom_def hom_induced_hom group_relative_homology_group)
    interpret gh4:
      group_hom "homology_group p X" "homology_group p (discrete_topology {()})"
                "?g"
      by (meson group_hom_axioms_def group_hom_def hom_induced_hom group_relative_homology_group)
    interpret gh5:
      group_hom "homology_group p (discrete_topology {()})" "homology_group p X"
                "?f"
      by (meson group_hom_axioms_def group_hom_def hom_induced_hom group_relative_homology_group)
    interpret gh6:
      group_hom "homology_group p (discrete_topology {()})" "relative_homology_group p (discrete_topology {()}) {()}"
                "hom_induced p (discrete_topology {()}) {} (discrete_topology {()}) {()} id"
      by (meson group_hom_axioms_def group_hom_def hom_induced_hom group_relative_homology_group)
    show ?thesis
    proof (intro exI conjI)
      have "(?h ∘ ?f ∘ ?g) y
          = (hom_induced p (discrete_topology {()}) {()} X S (λx. a) ∘
             hom_induced p (discrete_topology {()}) {} (discrete_topology {()}) {()} id ∘ ?g) y"
        by (simp add: a ‹a ∈ S› flip: hom_induced_compose)
      also have "… = 1🪙relative_homology_group p X S🪙"
        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)) = 1🪙relative_homology_group p X S🪙"
        by simp
      then show "?h y = ?h (y ⊗🪙?H🪙 inv🪙?H🪙 ?f (?g y))"
        by (simp add: that hom_induced_carrier)
      show "(y ⊗🪙?H🪙 inv🪙?H🪙 ?f (?g y)) ∈ carrier (homology_group p X)"
        by (simp add: hom_induced_carrier that)
      have *: "(?g ∘ hom_induced p X {} X {} (λx. a)) y = hom_induced p X {} (discrete_topology {()}) {} (λa. ()) y"
        by (simp add: a ‹a ∈ S› flip: hom_induced_compose)
      have "?g (y ⊗🪙?H🪙 inv🪙?H🪙 (?f ∘ ?g) y)
          = 1🪙homology_group p (discrete_topology {()})🪙"
        by (simp add: a ‹a ∈ S› that hom_induced_carrier flip: hom_induced_compose * [unfolded o_def])
      then show "?g (y ⊗🪙?H🪙 inv🪙?H🪙 ?f (?g y))
          = 1🪙homology_group p (discrete_topology {()})🪙"
        by simp
    qed
  qed
  show ?thesis
    apply (auto simp: reduced_homology_group_def carrier_subgroup_generated kernel_def image_iff)
     apply (metis (no_types, lifting) generate_in_carrier mem_Collect_eq subsetI)
    apply (force simp: dest: * intro: generate.incl)
    done
qed


lemma homology_exactness_reduced_1:
  assumes "topspace X ∩ S ≠ {}"
  shows  "exact_seq([reduced_homology_group(p - 1) (subtopology X S),
                     relative_homology_group p X S,
                     reduced_homology_group p X],
                    [hom_boundary p X S, hom_induced p X {} X S id])"
    (is "exact_seq ([?G1,?G2,?G3], [?h1,?h2])")
proof -
  have *: "?h2 ` carrier (homology_group p X)
         = kernel ?G2 (homology_group (p - 1) (subtopology X S)) ?h1"
    using homology_exactness_axiom_1 [of p X S] by simp
  have gh: "group_hom ?G3 ?G2 ?h2"
    by (simp add: reduced_homology_group_def group_hom_def group_hom_axioms_def
      group.group_subgroup_generated group.hom_from_subgroup_generated hom_induced_hom)
  show ?thesis
    apply (simp add: hom_boundary_reduced_hom gh * image_reduced_homology_group [OF assms])
    apply (simp add: kernel_def one_reduced_homology_group)
    done
qed


lemma homology_exactness_reduced_2:
   "exact_seq([reduced_homology_group(p - 1) X,
                 reduced_homology_group(p - 1) (subtopology X S),
                 relative_homology_group p X S],
                [hom_induced (p - 1) (subtopology X S) {} X {} id, hom_boundary p X S])"
    (is "exact_seq ([?G1,?G2,?G3], [?h1,?h2])")
  using homology_exactness_axiom_2 [of p X S]
  apply (simp add: group_hom_axioms_def group_hom_def hom_boundary_reduced_hom hom_induced_reduced_hom)
  apply (simp add: reduced_homology_group_def group_hom.subgroup_kernel group_hom_axioms_def group_hom_def hom_induced_hom)
  using hom_boundary_reduced_hom [of p X S]
  apply (auto simp: image_def set_eq_iff)
  by (metis carrier_reduced_homology_group hom_in_carrier set_eq_iff)


lemma homology_exactness_reduced_3:
   "exact_seq([relative_homology_group p X S,
               reduced_homology_group p X,
               reduced_homology_group p (subtopology X S)],
              [hom_induced p X {} X S id, hom_induced p (subtopology X S) {} X {} id])"
    (is "exact_seq ([?G1,?G2,?G3], [?h1,?h2])")
proof -
  have "kernel ?G2 ?G1 ?h1 =
      ?h2 ` carrier ?G3"
  proof -
    obtain U where U:
      "(hom_induced p (subtopology X S) {} X {} id) ` carrier ?G3 ⊆ U"
      "(hom_induced p (subtopology X S) {} X {} id) ` carrier ?G3
       ⊆ (hom_induced p (subtopology X S) {} X {} id) ` carrier (homology_group p (subtopology X S))"
      "U ∩ kernel (homology_group p X) ?G1 (hom_induced p X {} X S id)
     = kernel ?G2 ?G1 (hom_induced p X {} X S id)"
      "U ∩ (hom_induced p (subtopology X S) {} X {} id) ` carrier (homology_group p (subtopology X S))
    ⊆ (hom_induced p (subtopology X S) {} X {} id) ` carrier ?G3"
    proof
      show "?h2 ` carrier ?G3 ⊆ carrier ?G2"
        by (simp add: hom_induced_reduced image_subset_iff)
      show "?h2 ` carrier ?G3 ⊆ ?h2 ` carrier (homology_group p (subtopology X S))"
        by (meson carrier_reduced_homology_group_subset image_mono)
      have "subgroup (kernel (homology_group p X) (homology_group p (discrete_topology {()}))
                             (hom_induced p X {} (discrete_topology {()}) {} (λx. ())))
                     (homology_group p X)"
        by (simp add: group.normal_invE(1) group_hom.normal_kernel group_hom_axioms_def group_hom_def hom_induced_empty_hom)
      then show "carrier ?G2 ∩ kernel (homology_group p X) ?G1 ?h1 = kernel ?G2 ?G1 ?h1"
        unfolding carrier_reduced_homology_group
        by (auto simp: reduced_homology_group_def)
    show "carrier ?G2 ∩ ?h2 ` carrier (homology_group p (subtopology X S))
       ⊆ ?h2 ` carrier ?G3"
      by (force simp: carrier_reduced_homology_group kernel_def hom_induced_compose')
  qed
  with homology_exactness_axiom_3 [of p X S] show ?thesis
    by (fastforce simp add:)
qed
  then show ?thesis
    apply (simp add: group_hom_axioms_def group_hom_def hom_boundary_reduced_hom hom_induced_reduced_hom)
    apply (simp add: group.hom_from_subgroup_generated hom_induced_hom reduced_homology_group_def)
    done
qed


subsection‹More homology properties of deformations, retracts, contractible spaces›

lemma iso_relative_homology_of_contractible:
   "[contractible_space X; topspace X ∩ S ≠ {}]
  ==> hom_boundary p X S
      ∈ iso (relative_homology_group p X S) (reduced_homology_group(p - 1) (subtopology X S))"
  using very_short_exact_sequence
    [of "reduced_homology_group (p - 1) X"
        "reduced_homology_group (p - 1) (subtopology X S)"
        "relative_homology_group p X S"
        "reduced_homology_group p X"
        "hom_induced (p - 1) (subtopology X S) {} X {} id"
        "hom_boundary p X S"
        "hom_induced p X {} X S id"]
  by (meson exact_seq_cons_iff homology_exactness_reduced_1 homology_exactness_reduced_2 trivial_reduced_homology_group_contractible_space)

lemma isomorphic_group_relative_homology_of_contractible:
   "[contractible_space X; topspace X ∩ S ≠ {}]
        ==> relative_homology_group p X S ≅
            reduced_homology_group(p - 1) (subtopology X S)"
  by (meson iso_relative_homology_of_contractible is_isoI)

lemma isomorphic_group_reduced_homology_of_contractible:
   "[contractible_space X; topspace X ∩ S ≠ {}]
        ==> reduced_homology_group p (subtopology X S) ≅ relative_homology_group(p + 1) X S"
  by (metis add.commute add_diff_cancel_left' group.iso_sym group_relative_homology_group isomorphic_group_relative_homology_of_contractible)

lemma iso_reduced_homology_by_contractible:
   "[contractible_space(subtopology X S); topspace X ∩ S ≠ {}]
      ==> (hom_induced p X {} X S id) ∈ iso (reduced_homology_group p X) (relative_homology_group p X S)"
  using very_short_exact_sequence
    [of "reduced_homology_group (p - 1) (subtopology X S)"
        "relative_homology_group p X S"
        "reduced_homology_group p X"
        "reduced_homology_group p (subtopology X S)"
        "hom_boundary p X S"
        "hom_induced p X {} X S id"
        "hom_induced p (subtopology X S) {} X {} id"]
  by (meson exact_seq_cons_iff homology_exactness_reduced_1 homology_exactness_reduced_3 trivial_reduced_homology_group_contractible_space)

lemma isomorphic_reduced_homology_by_contractible:
   "[contractible_space(subtopology X S); topspace X ∩ S ≠ {}]
      ==> reduced_homology_group p X ≅ relative_homology_group p X S"
  using is_isoI iso_reduced_homology_by_contractible by blast

lemma isomorphic_relative_homology_by_contractible:
   "[contractible_space(subtopology X S); topspace X ∩ S ≠ {}]
      ==> relative_homology_group p X S ≅ reduced_homology_group p X"
  using group.iso_sym group_reduced_homology_group isomorphic_reduced_homology_by_contractible by blast

lemma isomorphic_reduced_homology_by_singleton:
   "a ∈ topspace X ==> reduced_homology_group p X ≅ relative_homology_group p X ({a})"
  by (simp add: contractible_space_subtopology_singleton isomorphic_reduced_homology_by_contractible)

lemma isomorphic_relative_homology_by_singleton:
   "a ∈ topspace X ==> relative_homology_group p X ({a}) ≅ reduced_homology_group p X"
  by (simp add: group.iso_sym isomorphic_reduced_homology_by_singleton)

lemma reduced_homology_group_pair:
  assumes "t1_space X" and a: "a ∈ topspace X" and b: "b ∈ topspace X" and "a ≠ b"
  shows "reduced_homology_group p (subtopology X {a,b}) ≅ homology_group p (subtopology X {a})"
        (is  "?lhs ≅ ?rhs")
proof -
  have "?lhs ≅ relative_homology_group p (subtopology X {a,b}) {b}"
    by (simp add: b isomorphic_reduced_homology_by_singleton topspace_subtopology)
  also have "… ≅ ?rhs"
  proof -
    have sub: "subtopology X {a, b} closure_of {b} ⊆ subtopology X {a, b} interior_of {b}"
      by (simp add: assms t1_space_subtopology closure_of_singleton subtopology_eq_discrete_topology_finite discrete_topology_closure_of)
    show ?thesis
      using homology_excision_axiom [OF sub, of "{a,b}" p]
      by (simp add: assms(4) group.iso_sym is_isoI subtopology_subtopology)
  qed
  finally show ?thesis .
qed


lemma deformation_retraction_relative_homology_group_isomorphisms:
   "[retraction_maps X Y r s; r ∈ U → V; s ∈ V → U; homotopic_with (λh. h ` U ⊆ U) X X (s ∘ r) id]
    ==> group_isomorphisms (relative_homology_group p X U) (relative_homology_group p Y V)
             (hom_induced p X U Y V r) (hom_induced p Y V X U s)"
  apply (simp add: retraction_maps_def)
  apply (rule homotopy_equivalence_relative_homology_group_isomorphisms)
       apply (auto simp: image_subset_iff_funcset Pi_iff continuous_map_compose homotopic_with_equal)
  done


lemma deformation_retract_relative_homology_group_isomorphisms:
   "[retraction_maps X Y r id; V ⊆ U; r ∈ U → V; homotopic_with (λh. h ` U ⊆ U) X X r id]
        ==> group_isomorphisms (relative_homology_group p X U) (relative_homology_group p Y V)
             (hom_induced p X U Y V r) (hom_induced p Y V X U id)"
  by (simp add: deformation_retraction_relative_homology_group_isomorphisms
      in_mono)

lemma deformation_retract_relative_homology_group_isomorphism:
   "[retraction_maps X Y r id; V ⊆ U; r ∈ U → V; homotopic_with (λh. h ` U ⊆ U) X X r id]
    ==> (hom_induced p X U Y V r) ∈ iso (relative_homology_group p X U) (relative_homology_group p Y V)"
  by (metis deformation_retract_relative_homology_group_isomorphisms group_isomorphisms_imp_iso)

lemma deformation_retract_relative_homology_group_isomorphism_id:
   "[retraction_maps X Y r id; V ⊆ U; r ∈ U → V; homotopic_with (λh. h ` U ⊆ U) X X r id]
    ==> (hom_induced p Y V X U id) ∈ iso (relative_homology_group p Y V) (relative_homology_group p X U)"
  by (metis deformation_retract_relative_homology_group_isomorphisms group_isomorphisms_imp_iso group_isomorphisms_sym)

lemma deformation_retraction_imp_isomorphic_relative_homology_groups:
   "[retraction_maps X Y r s; r ∈ U → V; s ` V ⊆ U; homotopic_with (λh. h ` U ⊆ U) X X (s ∘ r) id]
    ==> relative_homology_group p X U ≅ relative_homology_group p Y V"
  by (blast intro: is_isoI group_isomorphisms_imp_iso deformation_retraction_relative_homology_group_isomorphisms)

lemma deformation_retraction_imp_isomorphic_homology_groups:
   "[retraction_maps X Y r s; homotopic_with (λh. True) X X (s ∘ r) id]
        ==> homology_group p X ≅ homology_group p Y"
  by (simp add: deformation_retraction_imp_homotopy_equivalent_space homotopy_equivalent_space_imp_isomorphic_homology_groups)

lemma deformation_retract_imp_isomorphic_relative_homology_groups:
   "[retraction_maps X X' r id; V ⊆ U; r ∈ U → V; homotopic_with (λh. h ` U ⊆ U) X X r id]
        ==> relative_homology_group p X U ≅ relative_homology_group p X' V"
  by (simp add: deformation_retraction_imp_isomorphic_relative_homology_groups)

lemma deformation_retract_imp_isomorphic_homology_groups:
   "[retraction_maps X X' r id; homotopic_with (λh. True) X X r id]
        ==> homology_group p X ≅ homology_group p X'"
  by (simp add: deformation_retraction_imp_isomorphic_homology_groups)


lemma epi_hom_induced_inclusion:
  assumes "homotopic_with (λx. True) X X id f" and "f ∈ topspace X → S"
  shows "(hom_induced p (subtopology X S) {} X {} id)
   ∈ epi (homology_group p (subtopology X S)) (homology_group p X)"
proof (rule epi_right_invertible)
  show "hom_induced p (subtopology X S) {} X {} id
        ∈ hom (homology_group p (subtopology X S)) (homology_group p X)"
    by (simp add: hom_induced_empty_hom)
  show "hom_induced p X {} (subtopology X S) {} f
      ∈ carrier (homology_group p X) → carrier (homology_group p (subtopology X S))"
    by (simp add: hom_induced_carrier)
  fix x
  assume x: "x ∈ carrier (homology_group p X)"
  show "hom_induced p (subtopology X S) {} X {} id (hom_induced p X {} (subtopology X S) {} f x) = x"
  proof (subst hom_induced_compose')
    show "continuous_map X (subtopology X S) f"
      by (meson assms continuous_map_into_subtopology
          homotopic_with_imp_continuous_maps)
    show "hom_induced p X {} X {} (id ∘ f) x = x"
      by (metis assms(1) hom_induced_id homology_homotopy_empty id_comp x)
  qed (use assms in auto)
qed


lemma trivial_homomorphism_hom_induced_relativization:
  assumes "homotopic_with (λx. True) X X id f" and "f ∈ topspace X → S"
  shows "trivial_homomorphism (homology_group p X) (relative_homology_group p X S)
              (hom_induced p X {} X S id)"
proof -
  have "(hom_induced p (subtopology X S) {} X {} id)
      ∈ epi (homology_group p (subtopology X S)) (homology_group p X)"
    by (metis assms epi_hom_induced_inclusion)
  then show ?thesis
    using homology_exactness_axiom_3 [of p X S] homology_exactness_axiom_1 [of p X S]
    by (simp add: epi_def group.trivial_homomorphism_image group_hom.trivial_hom_iff)
qed


lemma mon_hom_boundary_inclusion:
  assumes "homotopic_with (λx. True) X X id f" and "f ∈ topspace X → S"
  shows "(hom_boundary p X S) ∈ mon
             (relative_homology_group p X S) (homology_group (p - 1) (subtopology X S))"
proof -
  have "(hom_induced p (subtopology X S) {} X {} id)
      ∈ epi (homology_group p (subtopology X S)) (homology_group p X)"
    by (metis assms epi_hom_induced_inclusion)
  then show ?thesis
    using homology_exactness_axiom_3 [of p X S] homology_exactness_axiom_1 [of p X S]
    apply (simp add: mon_def epi_def hom_boundary_hom)
    by (metis (no_types, opaque_lifting) 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 ⊗🪙homology_group p (subtopology X S)🪙 y)
             ∈ Group.iso (subgroup_generated (homology_group p (subtopology X S)) H ××
                          subgroup_generated (homology_group p (subtopology X S)) K)
                         (homology_group p (subtopology X S))"
    "hom_boundary (p + 1) X S
     ∈ Group.iso (relative_homology_group (p + 1) X S)
         (subgroup_generated (homology_group p (subtopology X S)) H)"
    "hom_induced p (subtopology X S) {} X {} id
     ∈ Group.iso
         (subgroup_generated (homology_group p (subtopology X S)) K)
         (homology_group p X)"
proof -
  let ?rhs = "relative_homology_group (p + 1) X S"
  let ?pXS = "homology_group p (subtopology X S)"
  let ?pX = "homology_group p X"
  let ?hb = "hom_boundary (p + 1) X S"
  let ?hi = "hom_induced p (subtopology X S) {} X {} id"
  have x: "short_exact_sequence (?pX) ?pXS ?rhs ?hi ?hb"
    using short_exact_sequence_hom_induced_relativization [OF assms, of "p + 1"] by simp
  have contf: "continuous_map X (subtopology X S) f"
    by (metis assms continuous_map_into_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"
  proof (rule splitting_lemma_right [OF x, where g' = "hom_induced p X {} (subtopology X S) {} f"])
    show "hom_induced p X {} (subtopology X S) {} f ∈ hom (homology_group p X) (homology_group p (subtopology X S))"
      using hom_induced_empty_hom by blast
  next
    fix z 
    assume "z ∈ carrier (homology_group p X)"
    then show "hom_induced p (subtopology X S) {} X {} id (hom_induced p X {} (subtopology X S) {} f z) = z"
      using assms(1) contf hom_induced_id homology_homotopy_empty
      by (fastforce simp add: hom_induced_compose')
  qed blast
  show ?thesis
  proof
    show "subgroup H ?pXS"
      using HK(1) normal_imp_subgroup by blast
    then show "(λ(x, y). x ⊗🪙?pXS🪙 y)
        ∈ Group.iso (subgroup_generated (?pXS) H ×× subgroup_generated (?pXS) K) (?pXS)"
      by (meson HK abelian_relative_homology_group group_disjoint_sum.iso_group_mul group_disjoint_sum_def group_relative_homology_group)
    show "subgroup K ?pXS"
      by (rule HK)
    show "hom_boundary (p + 1) X S ∈ Group.iso ?rhs (subgroup_generated (?pXS) H)"
      using iso int_ops(4) by presburger
    show "hom_induced p (subtopology X S) {} X {} id ∈ Group.iso (subgroup_generated (?pXS) K) (?pX)"
      by (simp add: iso(2))
  qed
qed

lemma iso_homology_group_prod_deformation:
  assumes "homotopic_with (λx. True) X X id f" and "f ∈ topspace X → S"
  shows "homology_group p (subtopology X S)
      ≅ DirProd (homology_group p X) (relative_homology_group(p + 1) X S)"
    (is "?G ≅ DirProd ?H ?R")
proof -
  obtain H K where HK:
    "(λ(x, y). x ⊗🪙?G🪙 y)
     ∈ Group.iso (subgroup_generated (?G) H ×× subgroup_generated (?G) K) (?G)"
    "hom_boundary (p + 1) X S ∈ Group.iso (?R) (subgroup_generated (?G) H)"
    "hom_induced p (subtopology X S) {} X {} id ∈ Group.iso (subgroup_generated (?G) K) (?H)"
    by (blast intro: group_isomorphisms_homology_group_prod_deformation [OF assms])
  have "?G ≅ DirProd (subgroup_generated (?G) H) (subgroup_generated (?G) K)"
    by (meson DirProd_group HK(1) group.group_subgroup_generated group.iso_sym group_relative_homology_group is_isoI)
  also have "… ≅ DirProd ?R ?H"
    by (meson HK group.DirProd_iso_trans group.group_subgroup_generated group.iso_sym group_relative_homology_group is_isoI)
  also have "… ≅ DirProd ?H ?R"
    by (simp add: DirProd_commute_iso)
  finally show ?thesis .
qed



lemma iso_homology_contractible_space_subtopology1:
  assumes "contractible_space X" "S ⊆ topspace X" "S ≠ {}"
  shows  "homology_group 0 (subtopology X S) ≅ DirProd integer_group (relative_homology_group(1) X S)"
proof -
  obtain f where  "homotopic_with (λx. True) X X id f" and "f ∈ topspace X → S"
    using assms contractible_space_alt by fastforce
  then have "homology_group 0 (subtopology X S) ≅ homology_group 0 X ×× relative_homology_group 1 X S"
    using iso_homology_group_prod_deformation [of X _ S 0] by auto
  also have "… ≅ integer_group ×× relative_homology_group 1 X S"
    using assms contractible_imp_path_connected_space group.DirProd_iso_trans group_relative_homology_group iso_refl isomorphic_integer_zeroth_homology_group by blast
  finally show ?thesis .
qed

lemma iso_homology_contractible_space_subtopology2:
  "[contractible_space X; S ⊆ topspace X; p ≠ 0; S ≠ {}]
    ==> homology_group p (subtopology X S) ≅ relative_homology_group (p + 1) X S"
  by (metis (no_types, opaque_lifting) add.commute isomorphic_group_reduced_homology_of_contractible topspace_subtopology topspace_subtopology_subset un_reduced_homology_group)

lemma trivial_relative_homology_group_contractible_spaces:
   "[contractible_space X; contractible_space(subtopology X S); topspace X ∩ S ≠ {}]
        ==> trivial_group(relative_homology_group p X S)"
  using group_reduced_homology_group group_relative_homology_group isomorphic_group_triviality isomorphic_relative_homology_by_contractible trivial_reduced_homology_group_contractible_space by blast

lemma trivial_relative_homology_group_alt:
  assumes contf: "continuous_map X (subtopology X S) f" and hom: "homotopic_with (λk. k ` S ⊆ S) X X f id"
  shows "trivial_group (relative_homology_group p X S)"
proof (rule trivial_relative_homology_group_gen [OF contf])
  show "homotopic_with (λh. True) (subtopology X S) (subtopology X S) f id"
    using hom unfolding homotopic_with_def
    apply (rule ex_forward)
    apply (auto simp: prod_topology_subtopology continuous_map_in_subtopology continuous_map_from_subtopology image_subset_iff topspace_subtopology)
    done
  show "homotopic_with (λk. True) X X f id"
    using assms by (force simp: homotopic_with_def)
qed


lemma iso_hom_induced_relativization_contractible:
  assumes "contractible_space(subtopology X S)" "contractible_space(subtopology X T)" "T ⊆ S" "topspace X ∩ T ≠ {}"
  shows "(hom_induced p X T X S id) ∈ iso (relative_homology_group p X T) (relative_homology_group p X S)"
proof (rule very_short_exact_sequence)
  show "exact_seq
         ([relative_homology_group(p - 1) (subtopology X S) T, relative_homology_group p X S, relative_homology_group p X T, relative_homology_group p (subtopology X S) T],
          [hom_relboundary p X S T, hom_induced p X T X S id, hom_induced p (subtopology X S) T X T id])"
    using homology_exactness_triple_1 [OF ‹T ⊆ S›] homology_exactness_triple_3 [OF ‹T ⊆ S›]
    by fastforce
  show "trivial_group (relative_homology_group p (subtopology X S) T)" "trivial_group (relative_homology_group(p - 1) (subtopology X S) T)"
    using assms
    by (force simp: inf.absorb_iff2 subtopology_subtopology topspace_subtopology intro!: trivial_relative_homology_group_contractible_spaces)+
qed

corollary isomorphic_relative_homology_groups_relativization_contractible:
  assumes "contractible_space(subtopology X S)" "contractible_space(subtopology X T)" "T ⊆ S" "topspace X ∩ T ≠ {}"
  shows "relative_homology_group p X T ≅ relative_homology_group p X S"
  by (rule is_isoI) (rule iso_hom_induced_relativization_contractible [OF assms])

lemma iso_hom_induced_inclusion_contractible:
  assumes "contractible_space X" "contractible_space(subtopology X S)" "T ⊆ S" "topspace X ∩ S ≠ {}"
  shows "(hom_induced p (subtopology X S) T X T id)
         ∈ iso (relative_homology_group p (subtopology X S) T) (relative_homology_group p X T)"
proof (rule very_short_exact_sequence)
  show "exact_seq
         ([relative_homology_group p X S, relative_homology_group p X T,
           relative_homology_group p (subtopology X S) T, relative_homology_group (p+1) X S],
          [hom_induced p X T X S id, hom_induced p (subtopology X S) T X T id, hom_relboundary (p+1) X S T])"
    using homology_exactness_triple_2 [OF ‹T ⊆ S›] homology_exactness_triple_3 [OF ‹T ⊆ S›]
    by (metis add_diff_cancel_left' diff_add_cancel exact_seq_cons_iff)
  show "trivial_group (relative_homology_group (p+1) X S)" "trivial_group (relative_homology_group p X S)"
    using assms
    by (auto simp: subtopology_subtopology topspace_subtopology intro!: trivial_relative_homology_group_contractible_spaces)
qed

corollary isomorphic_relative_homology_groups_inclusion_contractible:
  assumes "contractible_space X" "contractible_space(subtopology X S)" "T ⊆ S" "topspace X ∩ S ≠ {}"
  shows "relative_homology_group p (subtopology X S) T ≅ relative_homology_group p X T"
  by (rule is_isoI) (rule iso_hom_induced_inclusion_contractible [OF assms])

lemma iso_hom_relboundary_contractible:
  assumes "contractible_space X" "contractible_space(subtopology X T)" "T ⊆ S" "topspace X ∩ T ≠ {}"
  shows "hom_relboundary p X S T
         ∈ iso (relative_homology_group p X S) (relative_homology_group (p - 1) (subtopology X S) T)"
proof (rule very_short_exact_sequence)
  show "exact_seq
         ([relative_homology_group (p - 1) X T, relative_homology_group (p - 1) (subtopology X S) T, relative_homology_group p X S, relative_homology_group p X T],
          [hom_induced (p - 1) (subtopology X S) T X T id, hom_relboundary p X S T, hom_induced p X T X S id])"
    using homology_exactness_triple_1 [OF ‹T ⊆ S›] homology_exactness_triple_2 [OF ‹T ⊆ S›] by simp
  show "trivial_group (relative_homology_group p X T)" "trivial_group (relative_homology_group (p - 1) X T)"
    using assms
    by (auto simp: subtopology_subtopology topspace_subtopology intro!: trivial_relative_homology_group_contractible_spaces)
qed

corollary isomorphic_relative_homology_groups_relboundary_contractible:
  assumes "contractible_space X" "contractible_space(subtopology X T)" "T ⊆ S" "topspace X ∩ T ≠ {}"
  shows "relative_homology_group p X S ≅ relative_homology_group (p - 1) (subtopology X S) T"
  by (rule is_isoI) (rule iso_hom_relboundary_contractible [OF assms])

lemma isomorphic_relative_contractible_space_imp_homology_groups:
  assumes "contractible_space X" "contractible_space Y" "S ⊆ topspace X" "T ⊆ topspace Y"
     and ST: "S = {} ⟷ T = {}"
     and iso: "∧p. relative_homology_group p X S ≅ relative_homology_group p Y T"
  shows "homology_group p (subtopology X S) ≅ homology_group p (subtopology Y T)"
proof (cases "T = {}")
  case True
  have "homology_group p (subtopology X {}) ≅ homology_group p (subtopology Y {})"
    by (simp add: homeomorphic_empty_space_eq homeomorphic_space_imp_isomorphic_homology_groups)
  then show ?thesis
    using ST True by blast
next
  case False
  show ?thesis
  proof (cases "p = 0")
    case True
    have "homology_group p (subtopology X S) ≅ integer_group ×× relative_homology_group 1 X S"
      using assms True ‹T ≠ {}›
      by (simp add: iso_homology_contractible_space_subtopology1)
    also have "… ≅ integer_group ×× relative_homology_group 1 Y T"
      by (simp add: assms group.DirProd_iso_trans iso_refl)
    also have "… ≅ homology_group p (subtopology Y T)"
      by (simp add: True ‹T ≠ {}› assms group.iso_sym iso_homology_contractible_space_subtopology1)
    finally show ?thesis .
  next
    case False
    have "homology_group p (subtopology X S) ≅ relative_homology_group (p+1) X S"
      using assms False ‹T ≠ {}›
      by (simp add: iso_homology_contractible_space_subtopology2)
    also have "… ≅ relative_homology_group (p+1) Y T"
      by (simp add: assms)
    also have "… ≅ homology_group p (subtopology Y T)"
      by (simp add: False ‹T ≠ {}› assms group.iso_sym iso_homology_contractible_space_subtopology2)
    finally show ?thesis .
  qed
qed


subsection‹Homology groups of spheres›

lemma iso_reduced_homology_group_lower_hemisphere:
  assumes "k ≤ n"
  shows "hom_induced p (nsphere n) {} (nsphere n) {x. x k ≤ 0} id
      ∈ iso (reduced_homology_group p (nsphere n)) (relative_homology_group p (nsphere n) {x. x k ≤ 0})"
proof (rule iso_reduced_homology_by_contractible)
  show "contractible_space (subtopology (nsphere n) {x. x k ≤ 0})"
    by (simp add: assms contractible_space_lower_hemisphere)
  have "(λi. if i = k then -1 else 0) ∈ topspace (nsphere n) ∩ {x. x k ≤ 0}"
    using assms by (simp add: nsphere if_distrib [of "λx. x ^ 2"] cong: if_cong)
  then show "topspace (nsphere n) ∩ {x. x k ≤ 0} ≠ {}"
    by blast
qed


lemma topspace_nsphere_1:
  assumes "x ∈ topspace (nsphere n)" shows "(x k)🪙2 ≤ 1"
proof (cases "k ≤ n")
  case True
  have "(∑i ∈ {..n} - {k}. (x i)🪙2) = (∑i≤n. (x i)🪙2) - (x k)🪙2"
    using ‹k ≤ n› by (simp add: sum_diff)
  then show ?thesis
    using assms
    apply (simp add: nsphere)
    by (metis diff_ge_0_iff_ge sum_nonneg zero_le_power2)
next
  case False
  then show ?thesis
    using assms by (simp add: nsphere)
qed

lemma topspace_nsphere_1_eq_0:
  fixes x :: "nat ==> real"
  assumes x: "x ∈ topspace (nsphere n)" and xk: "(x k)🪙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)🪙2) = (∑i≤n. (x i)🪙2) - (x k)🪙2"
    using ‹k ≤ n› by (simp add: sum_diff)
  also have "… = 0"
    using assms by (simp add: nsphere)
  finally have "∀i∈{..n} - {k}. (x i)🪙2 = 0"
    by (simp add: sum_nonneg_eq_0_iff)
  then show ?thesis
    using True ‹i ≠ k› by auto
next
  case False
  with x show ?thesis
    by (simp add: nsphere)
qed


proposition iso_relative_homology_group_upper_hemisphere:
   "(hom_induced p (subtopology (nsphere n) {x. x k ≥ 0}) {x. x k = 0} (nsphere n) {x. x k ≤ 0} id)
  ∈ iso (relative_homology_group p (subtopology (nsphere n) {x. x k ≥ 0}) {x. x k = 0})
        (relative_homology_group p (nsphere n) {x. x k ≤ 0})" (is "?h ∈ iso ?G ?H")
proof -
  have "topspace (nsphere n) ∩ {x. x k < - 1 / 2} ⊆ {x ∈ topspace (nsphere n). x k ∈ {y. y ≤ - 1 / 2}}"
    by force
  moreover have "closedin (nsphere n) {x ∈ topspace (nsphere n). x k ∈ {y. y ≤ - 1 / 2}}"
    apply (rule closedin_continuous_map_preimage [OF continuous_map_nsphere_projection])
    using closed_Collect_le [of id "λx::real. -1/2"] apply simp
    done
  ultimately have "nsphere n closure_of {x. x k < -1/2} ⊆ {x ∈ topspace (nsphere n). x k ∈ {y. y ≤ -1/2}}"
    by (metis (no_types, lifting) closure_of_eq closure_of_mono closure_of_restrict)
  also have "… ⊆ {x ∈ topspace (nsphere n). x k ∈ {y. y < 0}}"
    by force
  also have "… ⊆ nsphere n interior_of {x. x k ≤ 0}"
  proof (rule interior_of_maximal)
    show "{x ∈ topspace (nsphere n). x k ∈ {y. y < 0}} ⊆ {x. x k ≤ 0}"
      by force
    show "openin (nsphere n) {x ∈ topspace (nsphere n). x k ∈ {y. y < 0}}"
      apply (rule openin_continuous_map_preimage [OF continuous_map_nsphere_projection])
      using open_Collect_less [of id "λx::real. 0"] apply simp
      done
  qed
  finally have nn: "nsphere n closure_of {x. x k < -1/2} ⊆ nsphere n interior_of {x. x k ≤ 0}" .
  have [simp]: "{x::nat==>real. x k ≤ 0} - {x. x k < - (1/2)} = {x. -1/2 ≤ x k ∧ x k ≤ 0}"
               "UNIV - {x::nat==>real. x k < a} = {x. a ≤ x k}" for a
    by auto
  let ?T01 = "top_of_set {0..1::real}"
  let ?X12 = "subtopology (nsphere n) {x. -1/2 ≤ x k}"
  have 1: "hom_induced p ?X12 {x. -1/2 ≤ x k ∧ x k ≤ 0} (nsphere n) {x. x k ≤ 0} id
         ∈ iso (relative_homology_group p ?X12 {x. -1/2 ≤ x k ∧ x k ≤ 0})
               ?H"
    using homology_excision_axiom [OF nn subset_UNIV, of p] by simp
  define h where "h ≡ λ(T,x). let y = max (x k) (-T) in
                               (λi. if i = k then y else sqrt(1 - y ^ 2) / sqrt(1 - x k ^ 2) * x i)"
  have h: "h(T,x) = x" if "0 ≤ T" "T ≤ 1" "(∑i≤n. (x i)🪙2) = 1" and 0: "∀i>n. x i = 0" "-T ≤ x k" for T x
    using that by (force simp: nsphere h_def Let_def max_def intro!: topspace_nsphere_1_eq_0)
  have "continuous_map (prod_topology ?T01 ?X12) euclideanreal (λx. h x i)" for i
  proof -
    show ?thesis
    proof (rule continuous_map_eq)
      show "continuous_map (prod_topology ?T01 ?X12)
         euclideanreal (λ(T, x). if 0 ≤ x k then x i else h (T, x) i)"
        unfolding case_prod_unfold
      proof (rule continuous_map_cases_le)
        show "continuous_map (prod_topology ?T01 ?X12) euclideanreal (λx. snd x k)"
          apply (subst continuous_map_of_snd [unfolded o_def])
          by (simp add: continuous_map_from_subtopology continuous_map_nsphere_projection)
      next
        show "continuous_map (subtopology (prod_topology ?T01 ?X12) {p ∈ topspace (prod_topology ?T01 ?X12). 0 ≤ snd p k})
         euclideanreal (λx. snd x i)"
          apply (rule continuous_map_from_subtopology)
          apply (subst continuous_map_of_snd [unfolded o_def])
          by (simp add: continuous_map_from_subtopology continuous_map_nsphere_projection)
      next
        note fst = continuous_map_into_fulltopology [OF continuous_map_subtopology_fst]
        have snd: "continuous_map (subtopology (prod_topology ?T01 (subtopology (nsphere n) T)) S) euclideanreal (λx. snd x k)" for k S T
          apply (simp add: nsphere)
          apply (rule continuous_map_from_subtopology)
          apply (subst continuous_map_of_snd [unfolded o_def])
          using continuous_map_from_subtopology continuous_map_nsphere_projection nsphere by fastforce
        show "continuous_map (subtopology (prod_topology ?T01 ?X12) {p ∈ topspace (prod_topology ?T01 ?X12). snd p k ≤ 0})
         euclideanreal (λx. h (fst x, snd x) i)"
          apply (simp add: h_def case_prod_unfold Let_def)
          apply (intro conjI impI fst snd continuous_intros)
          apply (auto simp: nsphere power2_eq_1_iff)
          done
      qed (auto simp: nsphere h)
    qed (auto simp: nsphere h)
  qed
  moreover
  have "h ` ({0..1} × (topspace (nsphere n) ∩ {x. - (1/2) ≤ x k}))
     ⊆ {x. (∑i≤n. (x i)🪙2) = 1 ∧ (∀i>n. x i = 0)}"
  proof -
    have "(∑i≤n. (h (T,x) i)🪙2) = 1"
      if x: "x ∈ topspace (nsphere n)" and xk: "- (1/2) ≤ x k" and T: "0 ≤ T" "T ≤ 1" for T x
    proof (cases "-T ≤ x k ")
      case True
      then show ?thesis
        using that by (auto simp: nsphere h)
    next
      case False
      with x ‹0 ≤ T› have "k ≤ n"
        apply (simp add: nsphere)
        by (metis neg_le_0_iff_le not_le)
      have "1 - (x k)🪙2 ≥ 0"
        using topspace_nsphere_1 x by auto
      with False T ‹k ≤ n›
      have "(∑i≤n. (h (T,x) i)🪙2) = T🪙2 + (1 - T🪙2) * (∑i∈{..n} - {k}. (x i)🪙2 / (1 - (x k)🪙2))"
        unfolding h_def Let_def max_def
        by (simp add: not_le square_le_1 power_mult_distrib power_divide if_distrib [of "λx. x ^ 2"]
              sum.delta_remove sum_distrib_left)
      also have "… = 1"
        using x False xk ‹0 ≤ T›
        by (simp add: nsphere sum_diff not_le ‹k ≤ n› power2_eq_1_iff flip: sum_divide_distrib)
      finally show ?thesis .
    qed
    moreover
    have "h (T,x) i = 0"
      if "x ∈ topspace (nsphere n)" "- (1/2) ≤ x k" and "n < i" "0 ≤ T" "T ≤ 1"
      for T x i
    proof (cases "-T ≤ x k ")
      case False
      then show ?thesis
        using that by (auto simp: nsphere h_def Let_def not_le max_def)
    qed (use that in ‹auto simp: nsphere h›)
    ultimately show ?thesis
      by auto
  qed
  ultimately
  have cmh: "continuous_map (prod_topology ?T01 ?X12) (nsphere n) h"
  proof (subst (2) nsphere) 
  qed (fastforce simp add: continuous_map_in_subtopology continuous_map_componentwise_UNIV)
  have "hom_induced p (subtopology (nsphere n) {x. 0 ≤ x k})
             (topspace (subtopology (nsphere n) {x. 0 ≤ x k}) ∩ {x. x k = 0}) ?X12
             (topspace ?X12 ∩ {x. - 1/2 ≤ x k ∧ x k ≤ 0}) id
            ∈ iso (relative_homology_group p (subtopology (nsphere n) {x. 0 ≤ x k})
                       (topspace (subtopology (nsphere n) {x. 0 ≤ x k}) ∩ {x. x k = 0}))
                (relative_homology_group p ?X12 (topspace ?X12 ∩ {x. - 1/2 ≤ x k ∧ x k ≤ 0}))"
  proof (rule deformation_retract_relative_homology_group_isomorphism_id)
    show "retraction_maps ?X12 (subtopology (nsphere n) {x. 0 ≤ x k}) (h ∘ (λx. (0,x))) id"
      unfolding retraction_maps_def
    proof (intro conjI ballI)
      show "continuous_map ?X12 (subtopology (nsphere n) {x. 0 ≤ x k}) (h ∘ Pair 0)"
        apply (simp add: continuous_map_in_subtopology)
        apply (intro conjI continuous_map_compose [OF _ cmh] continuous_intros)
          apply (auto simp: h_def Let_def)
        done
      show "continuous_map (subtopology (nsphere n) {x. 0 ≤ x k}) ?X12 id"
        by (simp add: continuous_map_in_subtopology)
    qed (simp add: nsphere h)
  next
    have h0: "∧xa. [xa ∈ topspace (nsphere n); - (1/2) ≤ xa k; xa k ≤ 0] ==> h (0, xa) k = 0"
      by (simp add: h_def Let_def)
    show "(h ∘ (λx. (0,x))) ∈ (topspace ?X12 ∩ {x. - 1 / 2 ≤ x k ∧ x k ≤ 0})
        → topspace (subtopology (nsphere n) {x. 0 ≤ x k}) ∩ {x. x k = 0}"
      apply (auto simp: h0)
      apply (rule subsetD [OF continuous_map_image_subset_topspace [OF cmh]])
      apply (force simp: nsphere)
      done
    have hin: "∧t x. [x ∈ topspace (nsphere n); - (1/2) ≤ x k; 0 ≤ t; t ≤ 1] ==> h (t,x) ∈ topspace (nsphere n)"
      apply (rule subsetD [OF continuous_map_image_subset_topspace [OF cmh]])
      apply (force simp: nsphere)
      done
    have h1: "∧x. [x ∈ topspace (nsphere n); - (1/2) ≤ x k] ==> h (1, x) = x"
      by (simp add: h nsphere)
    have "continuous_map (prod_topology ?T01 ?X12) (nsphere n) h"
      using cmh by force
    then show "homotopic_with
                 (λh. h ` (topspace ?X12 ∩ {x. - 1 / 2 ≤ x k ∧ x k ≤ 0}) ⊆ topspace ?X12 ∩ {x. - 1 / 2 ≤ x k ∧ x k ≤ 0})
                 ?X12 ?X12 (h ∘ (λx. (0,x))) id"
      apply (subst homotopic_with, force)
      apply (rule_tac x=h in exI)
      apply (auto simp: hin h1 continuous_map_in_subtopology)
         apply (auto simp: h_def Let_def max_def)
      done
  qed auto
  then have 2: "hom_induced p (subtopology (nsphere n) {x. 0 ≤ x k}) {x. x k = 0}
             ?X12 {x. - 1/2 ≤ x k ∧ x k ≤ 0} id
            ∈ Group.iso
                (relative_homology_group p (subtopology (nsphere n) {x. 0 ≤ x k}) {x. x k = 0})
                (relative_homology_group p ?X12 {x. - 1/2 ≤ x k ∧ x k ≤ 0})"
    by (metis hom_induced_restrict relative_homology_group_restrict topspace_subtopology)
  show ?thesis
    using iso_set_trans [OF 2 1]
    by (simp add: subset_iff continuous_map_in_subtopology flip: hom_induced_compose)
qed


corollary iso_upper_hemisphere_reduced_homology_group:
   "(hom_boundary (1 + p) (subtopology (nsphere (Suc n)) {x. x(Suc n) ≥ 0}) {x. x(Suc n) = 0})
  ∈ iso (relative_homology_group (1 + p) (subtopology (nsphere (Suc n)) {x. x(Suc n) ≥ 0}) {x. x(Suc n) = 0})
        (reduced_homology_group p (nsphere n))"
proof -
  have "{x. 0 ≤ x (Suc n)} ∩ {x. x (Suc n) = 0} = {x. x (Suc n) = (0::real)}"
    by auto
  then have n: "nsphere n = subtopology (subtopology (nsphere (Suc n)) {x. x(Suc n) ≥ 0}) {x. x(Suc n) = 0}"
    by (simp add: subtopology_nsphere_equator subtopology_subtopology)
  have ne: "(λi. if i = n then 1 else 0) ∈ topspace (subtopology (nsphere (Suc n)) {x. 0 ≤ x (Suc n)}) ∩ {x. x (Suc n) = 0}"
    by (simp add: nsphere if_distrib [of "λx. x ^ 2"] cong: if_cong)
  show ?thesis
    unfolding n
    using iso_relative_homology_of_contractible [where p = "1 + p", simplified]
    by (metis contractible_space_upper_hemisphere dual_order.refl empty_iff ne)
qed

corollary iso_reduced_homology_group_upper_hemisphere:
  assumes "k ≤ n"
  shows "hom_induced p (nsphere n) {} (nsphere n) {x. x k ≥ 0} id
      ∈ iso (reduced_homology_group p (nsphere n)) (relative_homology_group p (nsphere n) {x. x k ≥ 0})"
proof (rule iso_reduced_homology_by_contractible [OF contractible_space_upper_hemisphere [OF assms]])
  have "(λi. if i = k then 1 else 0) ∈ topspace (nsphere n) ∩ {x. 0 ≤ x k}"
    using assms by (simp add: nsphere if_distrib [of "λx. x ^ 2"] cong: if_cong)
  then show "topspace (nsphere n) ∩ {x. 0 ≤ x k} ≠ {}"
    by blast
qed


lemma iso_relative_homology_group_lower_hemisphere:
  "hom_induced p (subtopology (nsphere n) {x. x k ≤ 0}) {x. x k = 0} (nsphere n) {x. x k ≥ 0} id
  ∈ iso (relative_homology_group p (subtopology (nsphere n) {x. x k ≤ 0}) {x. x k = 0})
        (relative_homology_group p (nsphere n) {x. x k ≥ 0})" (is "?k ∈ iso ?G ?H")
proof -
  define r where "r ≡ λx i. if i = k then -x i else (x i::real)"
  then have [simp]: "r ∘ r = id"
    by force
  have cmr: "continuous_map (subtopology (nsphere n) S) (nsphere n) r" for S
    using continuous_map_nsphere_reflection [of n k]
    by (simp add: continuous_map_from_subtopology r_def)
  let ?f = "hom_induced p (subtopology (nsphere n) {x. x k ≤ 0}) {x. x k = 0}
                          (subtopology (nsphere n) {x. x k ≥ 0}) {x. x k = 0} r"
  let ?g = "hom_induced p (subtopology (nsphere n) {x. x k ≥ 0}) {x. x k = 0} (nsphere n) {x. x k ≤ 0} id"
  let ?h = "hom_induced p (nsphere n) {x. x k ≤ 0} (nsphere n) {x. x k ≥ 0} r"
  obtain f h where
        f: "f ∈ iso ?G (relative_homology_group p (subtopology (nsphere n) {x. x k ≥ 0}) {x. x k = 0})"
    and h: "h ∈ iso (relative_homology_group p (nsphere n) {x. x k ≤ 0}) ?H"
    and eq: "h ∘ ?g ∘ f = ?k"
  proof
    have hmr: "homeomorphic_map (nsphere n) (nsphere n) r"
      unfolding homeomorphic_map_maps
      by (metis ‹r ∘ r = id› cmr homeomorphic_maps_involution pointfree_idE subtopology_topspace)
    then have hmrs: "homeomorphic_map (subtopology (nsphere n) {x. x k ≤ 0}) (subtopology (nsphere n) {x. x k ≥ 0}) r"
      by (simp add: homeomorphic_map_subtopologies_alt r_def)
    have rimeq: "r ` (topspace (subtopology (nsphere n) {x. x k ≤ 0}) ∩ {x. x k = 0})
               = topspace (subtopology (nsphere n) {x. 0 ≤ x k}) ∩ {x. x k = 0}"
      using continuous_map_eq_topcontinuous_at continuous_map_nsphere_reflection topcontinuous_at_atin
      by (fastforce simp: r_def Pi_iff)
    show "?f ∈ iso ?G (relative_homology_group p (subtopology (nsphere n) {x. x k ≥ 0}) {x. x k = 0})"
      using homeomorphic_map_relative_homology_iso [OF hmrs Int_lower1 rimeq]
      by (metis hom_induced_restrict relative_homology_group_restrict)
    have rimeq: "r ` (topspace (nsphere n) ∩ {x. x k ≤ 0}) = topspace (nsphere n) ∩ {x. 0 ≤ x k}"
      by (metis hmrs homeomorphic_imp_surjective_map topspace_subtopology)
    show "?h ∈ Group.iso (relative_homology_group p (nsphere n) {x. x k ≤ 0}) ?H"
      using homeomorphic_map_relative_homology_iso [OF hmr Int_lower1 rimeq] by simp
    have [simp]: "∧x. x k = 0 ==> r x k = 0"
      by (auto simp: r_def)
    have "?h ∘ ?g ∘ ?f
        = hom_induced p (subtopology (nsphere n) {x. 0 ≤ x k}) {x. x k = 0} (nsphere n) {x. 0 ≤ x k} r ∘
          hom_induced p (subtopology (nsphere n) {x. x k ≤ 0}) {x. x k = 0} (subtopology (nsphere n) {x. 0 ≤ x k}) {x. x k = 0} r"
      apply (subst hom_induced_compose [symmetric])
      using continuous_map_nsphere_reflection apply (force simp: r_def)+
      done
    also have "… = ?k"
      apply (subst hom_induced_compose [symmetric])
          apply (simp_all add: image_subset_iff cmr)
      using hmrs homeomorphic_imp_continuous_map apply blast
      done
    finally show "?h ∘ ?g ∘ ?f = ?k" .
  qed
  with iso_relative_homology_group_upper_hemisphere [of p n k]
  have "h ∘ hom_induced p (subtopology (nsphere n) {f. 0 ≤ f k}) {f. f k = 0} (nsphere n) {f. f k ≤ 0} id ∘ f
  ∈ Group.iso ?G (relative_homology_group p (nsphere n) {f. 0 ≤ f k})"
    using f h iso_set_trans by blast
  then show ?thesis
    by (simp add: eq)
qed


lemma iso_lower_hemisphere_reduced_homology_group:
   "hom_boundary (1 + p) (subtopology (nsphere (Suc n)) {x. x(Suc n) ≤ 0}) {x. x(Suc n) = 0}
  ∈ iso (relative_homology_group (1 + p) (subtopology (nsphere (Suc n)) {x. x(Suc n) ≤ 0})
                        {x. x(Suc n) = 0})
        (reduced_homology_group p (nsphere n))"
proof -
  have "{x. (∑i≤n. (x i)🪙2) = 1 ∧ (∀i>n. x i = 0)} =
       ({x. (∑i≤n. (x i)🪙2) + (x (Suc n))🪙2 = 1 ∧ (∀i>Suc n. x i = 0)} ∩ {x. x (Suc n) ≤ 0} ∩
        {x. x (Suc n) = (0::real)})"
    by (force simp: dest: Suc_lessI)
  then have n: "nsphere n = subtopology (subtopology (nsphere (Suc n)) {x. x(Suc n) ≤ 0}) {x. x(Suc n) = 0}"
    by (simp add: nsphere subtopology_subtopology)
  have ne: "(λi. if i = n then 1 else 0) ∈ topspace (subtopology (nsphere (Suc n)) {x. x (Suc n) ≤ 0}) ∩ {x. x (Suc n) = 0}"
    by (simp add: nsphere if_distrib [of "λx. x ^ 2"] cong: if_cong)
  show ?thesis
    unfolding n
    apply (rule iso_relative_homology_of_contractible [where p = "1 + p", simplified])
    using contractible_space_lower_hemisphere ne apply blast+
    done
qed

lemma isomorphism_sym:
  "[f ∈ iso G1 G2; ∧x. x ∈ carrier G1 ==> r'(f x) = f(r x);
     ∧x. x ∈ carrier G1 ==> r x ∈ carrier G1; group G1; group G2]
      ==> ∃f ∈ iso G2 G1. ∀x ∈ carrier G2. r(f x) = f(r' x)"
  apply (clarsimp simp add: group.iso_iff_group_isomorphisms Bex_def)
  by (metis (full_types) group_isomorphisms_def group_isomorphisms_sym hom_in_carrier)

lemma isomorphism_trans:
  "[∃f ∈ iso G1 G2. ∀x ∈ carrier G1. r2(f x) = f(r1 x); ∃f ∈ iso G2 G3. ∀x ∈ carrier G2. r3(f x) = f(r2 x)]
   ==> ∃f ∈ iso G1 G3. ∀x ∈ carrier G1. r3(f x) = f(r1 x)"
  apply clarify
  by (smt (verit, ccfv_threshold) Group.iso_iff hom_in_carrier iso_set_trans
      o_apply)

lemma reduced_homology_group_nsphere_step:
   "∃f ∈ iso(reduced_homology_group p (nsphere n))
            (reduced_homology_group (1 + p) (nsphere (Suc n))).
        ∀c ∈ carrier(reduced_homology_group p (nsphere n)).
             hom_induced (1 + p) (nsphere(Suc n)) {} (nsphere(Suc n)) {}
                         (λx i. if i = 0 then -x i else x i) (f c)
           = f (hom_induced p (nsphere n) {} (nsphere n) {} (λx i. if i = 0 then -x i else x i) c)"
proof -
  define r where "r ≡ λx::nat==>real. λi. if i = 0 then -x i else x i"
  have cmr: "continuous_map (nsphere n) (nsphere n) r" for n
    unfolding r_def by (rule continuous_map_nsphere_reflection)
  have rsub: "r ∈ {x. 0 ≤ x (Suc n)} → {x. 0 ≤ x (Suc n)}" 
             "r ∈ {x. x (Suc n) ≤ 0} → {x. x (Suc n) ≤ 0}" 
             "r ∈ {x. x (Suc n) = 0} → {x. x (Suc n) = 0}"
    by (force simp: r_def)+
  let ?sub = "subtopology (nsphere (Suc n)) {x. x (Suc n) ≥ 0}"
  let ?G2 = "relative_homology_group (1 + p) ?sub {x. x (Suc n) = 0}"
  let ?r2 = "hom_induced (1 + p) ?sub {x. x (Suc n) = 0} ?sub {x. x (Suc n) = 0} r"
  let ?j = "λp n. hom_induced p (nsphere n) {} (nsphere n) {} r"
  show ?thesis
    unfolding r_def [symmetric]
  proof (rule isomorphism_trans)
    let ?f = "hom_boundary (1 + p) ?sub {x. x (Suc n) = 0}"
    show "∃f∈Group.iso (reduced_homology_group p (nsphere n)) ?G2.
           ∀c∈carrier (reduced_homology_group p (nsphere n)). ?r2 (f c) = f (?j p n c)"
    proof (rule isomorphism_sym)
      show "?f ∈ Group.iso ?G2 (reduced_homology_group p (nsphere n))"
        using iso_upper_hemisphere_reduced_homology_group
        by (metis add.commute)
    next
      fix c
      assume "c ∈ carrier ?G2"
      have cmrs: "continuous_map ?sub ?sub r"
        by (metis (no_types, lifting) IntE Pi_iff cmr continuous_map_from_subtopology
            continuous_map_into_subtopology rsub(1) topspace_subtopology)
      have "hom_induced p (nsphere n) {} (nsphere n) {} r ∘ hom_boundary (1 + p) ?sub {x. x (Suc n) = 0}
          = hom_boundary (1 + p) ?sub {x. x (Suc n) = 0} ∘
            hom_induced (1 + p) ?sub {x. x (Suc n) = 0} ?sub {x. x (Suc n) = 0} r"
        using naturality_hom_induced [OF cmrs rsub(3), symmetric, of "1+p", simplified]
        by (simp add: Pi_iff subtopology_subtopology subtopology_nsphere_equator flip: Collect_conj_eq cong: rev_conj_cong)
      then show "?j p n (?f c) = ?f (hom_induced (1 + p) ?sub {x. x (Suc n) = 0} ?sub {x. x (Suc n) = 0} r c)"
        by (metis comp_def)
    next
      fix c
      assume "c ∈ carrier ?G2"
      show "hom_induced (1 + p) ?sub {x. x (Suc n) = 0} ?sub {x. x (Suc n) = 0} r c ∈ carrier ?G2"
        using hom_induced_carrier by blast
    qed auto
  next
    let ?H2 = "relative_homology_group (1 + p) (nsphere (Suc n)) {x. x (Suc n) ≤ 0}"
    let ?s2 = "hom_induced (1 + p) (nsphere (Suc n)) {x. x (Suc n) ≤ 0} (nsphere (Suc n)) {x. x (Suc n) ≤ 0} r"
    show "∃f∈Group.iso ?G2 (reduced_homology_group (1 + p) (nsphere (Suc n))). ∀c∈carrier ?G2. ?j (1 + p) (Suc n) (f c)
            = f (?r2 c)"
    proof (rule isomorphism_trans)
      show "∃f∈Group.iso ?G2 ?H2.
                 ∀c∈carrier ?G2.
                    ?s2 (f c) = f (hom_induced (1 + p) ?sub {x. x (Suc n) = 0} ?sub {x. x (Suc n) = 0} r c)"
      proof (intro ballI bexI)
        fix c
        assume "c ∈ carrier (relative_homology_group (1 + p) ?sub {x. x (Suc n) = 0})"
        show "?s2 (hom_induced (1 + p) ?sub {x. x (Suc n) = 0} (nsphere (Suc n)) {x. x (Suc n) ≤ 0} id c)
            = hom_induced (1 + p) ?sub {x. x (Suc n) = 0} (nsphere (Suc n)) {x. x (Suc n) ≤ 0} id (?r2 c)"
          apply (simp add: rsub hom_induced_compose' Collect_mono_iff cmr)
          apply (subst hom_induced_compose')
              apply (simp_all add: continuous_map_in_subtopology continuous_map_from_subtopology [OF cmr] rsub)
           apply (auto simp: r_def)
          done
      qed (simp add: iso_relative_homology_group_upper_hemisphere)
    next
      let ?h = "hom_induced (1 + p) (nsphere(Suc n)) {} (nsphere (Suc n)) {x. x(Suc n) ≤ 0} id"
      show "∃f∈Group.iso ?H2 (reduced_homology_group (1 + p) (nsphere (Suc n))).
               ∀c∈carrier ?H2. ?j (1 + p) (Suc n) (f c) = f (?s2 c)"
      proof (rule isomorphism_sym)
        show "?h ∈ Group.iso (reduced_homology_group (1 + p) (nsphere (Suc n)))
               (relative_homology_group (1 + p) (nsphere (Suc n)) {x. x (Suc n) ≤ 0})"
          using iso_reduced_homology_group_lower_hemisphere by blast
      next
        fix c
        assume "c ∈ carrier (reduced_homology_group (1 + p) (nsphere (Suc n)))"
        show "?s2 (?h c) = ?h (?j (1 + p) (Suc n) c)"
          by (simp add: hom_induced_compose' cmr rsub)
      next
        fix c
        assume "c ∈ carrier (reduced_homology_group (1 + p) (nsphere (Suc n)))"
        then show "hom_induced (1 + p) (nsphere (Suc n)) {} (nsphere (Suc n)) {} r c
        ∈ carrier (reduced_homology_group (1 + p) (nsphere (Suc n)))"
          by (simp add: hom_induced_reduced)
      qed auto
    qed
  qed
qed


lemma reduced_homology_group_nsphere_aux:
  "if p = int n then reduced_homology_group n (nsphere n) ≅ integer_group
                     else trivial_group(reduced_homology_group p (nsphere n))"
proof (induction n arbitrary: p)
  case 0
  let ?a = "λi::nat. if i = 0 then 1 else (0::real)"
  let ?b = "λi::nat. if i = 0 then -1 else (0::real)"
  have st: "subtopology (powertop_real UNIV) {?a, ?b} = nsphere 0"
  proof -
    have "{?a, ?b} = {x. (x 0)🪙2 = 1 ∧ (∀i>0. x i = 0)}"
      using power2_eq_iff by fastforce
    then show ?thesis
      by (simp add: nsphere)
  qed
  have "t1_space (powertop_real UNIV)"
    using t1_space_euclidean t1_space_product_topology by blast
  then have *: "reduced_homology_group p (subtopology (powertop_real UNIV) {?a, ?b}) ≅
        homology_group p (subtopology (powertop_real UNIV) {?a})"
    by (intro reduced_homology_group_pair) (auto simp: fun_eq_iff)
  have "reduced_homology_group 0 (nsphere 0) ≅ integer_group" if "p=0"
  proof -
    have "reduced_homology_group 0 (nsphere 0) ≅ homology_group 0 (top_of_set {?a})" if "p=0"
      by (metis * euclidean_product_topology st that)
    also have "… ≅ integer_group"
      by (simp add: homology_coefficients)
    finally show ?thesis
      using that by blast
  qed
  moreover have "trivial_group (reduced_homology_group p (nsphere 0))" if "p≠0"
    using * that homology_dimension_axiom [of "subtopology (powertop_real UNIV) {?a}" ?a p]
    using isomorphic_group_triviality st by force
  ultimately show ?case
    by auto
next
  case (Suc n)
  have eq: "reduced_homology_group (int n) (nsphere n) ≅ integer_group" if "p-1 = n"
    by (simp add: Suc.IH)
  have neq: "trivial_group (reduced_homology_group (p-1) (nsphere n))" if "p-1 ≠ n"
    by (simp add: Suc.IH that)
  have iso: "reduced_homology_group p (nsphere (Suc n)) ≅ reduced_homology_group (p-1) (nsphere n)"
    using reduced_homology_group_nsphere_step [of "p-1" n]  group.iso_sym [OF _ is_isoI] group_reduced_homology_group
    by fastforce
  then show ?case
    using eq iso_trans iso isomorphic_group_triviality neq
    by (metis (no_types, opaque_lifting) add.commute add_left_cancel diff_add_cancel group_reduced_homology_group of_nat_Suc)
qed


lemma reduced_homology_group_nsphere:
  "reduced_homology_group n (nsphere n) ≅ integer_group"
  "p ≠ n ==> trivial_group(reduced_homology_group p (nsphere n))"
  using reduced_homology_group_nsphere_aux by auto

lemma cyclic_reduced_homology_group_nsphere:
   "cyclic_group(reduced_homology_group p (nsphere n))"
  by (metis reduced_homology_group_nsphere trivial_imp_cyclic_group cyclic_integer_group
      group_integer_group group_reduced_homology_group isomorphic_group_cyclicity)

lemma trivial_reduced_homology_group_nsphere:
   "trivial_group(reduced_homology_group p (nsphere n)) ⟷ (p ≠ n)"
  using group_integer_group isomorphic_group_triviality nontrivial_integer_group reduced_homology_group_nsphere(1) reduced_homology_group_nsphere(2) trivial_group_def by blast

lemma non_contractible_space_nsphere: "¬ (contractible_space(nsphere n))"
  proof (clarsimp simp add: contractible_eq_homotopy_equivalent_singleton_subtopology)
  fix a :: "nat ==> real"
  assume a: "a ∈ topspace (nsphere n)"
    and he: "nsphere n homotopy_equivalent_space subtopology (nsphere n) {a}"
  have "trivial_group (reduced_homology_group (int n) (subtopology (nsphere n) {a}))"
    by (simp add: a homology_dimension_reduced [where a=a])
  then show "False"
    using isomorphic_group_triviality [OF homotopy_equivalent_space_imp_isomorphic_reduced_homology_groups [OF he, of n]]
    by (simp add: trivial_reduced_homology_group_nsphere)
qed


subsection‹Brouwer degree of a Map›

definition Brouwer_degree2 :: "nat ==> ((nat ==> real) ==> nat ==> real) ==> int"
  where
 "Brouwer_degree2 p f ≡
    @d::int. ∀x ∈ carrier(reduced_homology_group p (nsphere p)).
                hom_induced p (nsphere p) {} (nsphere p) {} f x = pow (reduced_homology_group p (nsphere p)) x d"

lemma Brouwer_degree2_eq:
   "(∧x. x ∈ topspace(nsphere p) ==> f x = g x) ==> Brouwer_degree2 p f = Brouwer_degree2 p g"
  unfolding Brouwer_degree2_def Ball_def
  apply (intro Eps_cong all_cong)
  by (metis (mono_tags, lifting) hom_induced_eq)

lemma Brouwer_degree2:
  assumes "x ∈ carrier(reduced_homology_group p (nsphere p))"
  shows "hom_induced p (nsphere p) {} (nsphere p) {} f x
       = pow (reduced_homology_group p (nsphere p)) x (Brouwer_degree2 p f)"
       (is "?h x = pow ?G x _")
proof (cases "continuous_map(nsphere p) (nsphere p) f")
  case True
  interpret group ?G
    by simp
  interpret group_hom ?G ?G ?h
    using hom_induced_reduced_hom group_hom_axioms_def group_hom_def is_group by blast
  obtain a where a: "a ∈ carrier ?G"
    and aeq: "subgroup_generated ?G {a} = ?G"
    using cyclic_reduced_homology_group_nsphere [of p p] by (auto simp: cyclic_group_def)
  then have carra: "carrier (subgroup_generated ?G {a}) = range (λn::int. pow ?G a n)"
    using carrier_subgroup_generated_by_singleton by blast
  moreover have "?h a ∈ carrier (subgroup_generated ?G {a})"
    by (simp add: a aeq hom_induced_reduced)
  ultimately obtain d::int where d: "?h a = pow ?G a d"
    by auto
  have *: "hom_induced (int p) (nsphere p) {} (nsphere p) {} f x = x [^]🪙?G🪙 d"
    if x: "x ∈ carrier ?G" for x
  proof -
    obtain n::int where xeq: "x = pow ?G a n"
      using carra x aeq by auto
    show ?thesis
      by (simp add: xeq a d hom_int_pow int_pow_pow mult.commute)
  qed
  show ?thesis
    unfolding Brouwer_degree2_def
    apply (rule someI2 [where a=d])
    using assms * apply blast+
    done
next
  case False
  show ?thesis
    unfolding Brouwer_degree2_def
    by (rule someI2 [where a=0]) (simp_all add: hom_induced_default False one_reduced_homology_group assms)
qed



lemma Brouwer_degree2_iff:
  assumes f: "continuous_map (nsphere p) (nsphere p) f"
    and x: "x ∈ carrier(reduced_homology_group p (nsphere p))"
  shows "(hom_induced (int p) (nsphere p) {} (nsphere p) {} f x =
         x [^]🪙reduced_homology_group (int p) (nsphere p)🪙 d)
    ⟷ (x = 1🪙reduced_homology_group (int p) (nsphere p)🪙 ∨ Brouwer_degree2 p f = d)"
    (is  "(?h x = x [^]🪙?G🪙 d) ⟷ _")
proof -
  interpret group "?G"
    by simp
  obtain a where a: "a ∈ carrier ?G"
    and aeq: "subgroup_generated ?G {a} = ?G"
    using cyclic_reduced_homology_group_nsphere [of p p] by (auto simp: cyclic_group_def)
  then obtain i::int where i: "x = (a [^]🪙?G🪙 i)"
    using carrier_subgroup_generated_by_singleton x by fastforce
  then have "a [^]🪙?G🪙 i ∈ carrier ?G"
    using x by blast
  have [simp]: "ord a = 0"
    by (simp add: a aeq iso_finite [OF reduced_homology_group_nsphere(1)] flip: infinite_cyclic_subgroup_order)
  show ?thesis
    by (auto simp: Brouwer_degree2 int_pow_eq_id x i a int_pow_pow int_pow_eq)
qed


lemma Brouwer_degree2_unique:
  assumes f: "continuous_map (nsphere p) (nsphere p) f"
    and hi: "∧x. x ∈ carrier(reduced_homology_group p (nsphere p))
               ==> hom_induced p (nsphere p) {} (nsphere p) {} f x = pow (reduced_homology_group p (nsphere p)) x d"
          (is "∧x. x ∈ carrier ?G ==> ?h x = _")
  shows "Brouwer_degree2 p f = d"
proof -
  obtain a where a: "a ∈ carrier ?G"
    and aeq: "subgroup_generated ?G {a} = ?G"
    using cyclic_reduced_homology_group_nsphere [of p p] by (auto simp: cyclic_group_def)
  show ?thesis
    using hi [OF a] unfolding Brouwer_degree2 a
    by (metis Brouwer_degree2_iff a aeq f group.trivial_group_subgroup_generated
        group_reduced_homology_group subsetI trivial_reduced_homology_group_nsphere)
qed

lemma Brouwer_degree2_unique_generator:
  assumes f: "continuous_map (nsphere p) (nsphere p) f"
    and eq: "subgroup_generated (reduced_homology_group p (nsphere p)) {a}
           = reduced_homology_group p (nsphere p)"
    and hi: "hom_induced p (nsphere p) {} (nsphere p) {} f a = pow (reduced_homology_group p (nsphere p)) a d"
          (is "?h a = pow ?G a _")
  shows "Brouwer_degree2 p f = d"
proof (cases "a ∈ carrier ?G")
  case True
  then show ?thesis
    by (metis Brouwer_degree2_iff hi eq f group.trivial_group_subgroup_generated group_reduced_homology_group
              subset_singleton_iff trivial_reduced_homology_group_nsphere)
next
  case False
  then show ?thesis
    using trivial_reduced_homology_group_nsphere [of p p]
    by (metis group.trivial_group_subgroup_generated_eq disjoint_insert(1) eq group_reduced_homology_group inf_bot_right subset_singleton_iff)
qed

lemma Brouwer_degree2_homotopic:
  assumes "homotopic_with (λx. True) (nsphere p) (nsphere p) f g"
  shows "Brouwer_degree2 p f = Brouwer_degree2 p g"
proof -
  have "continuous_map (nsphere p) (nsphere p) f"
    using homotopic_with_imp_continuous_maps [OF assms] by auto
  show ?thesis
    using Brouwer_degree2_def assms homology_homotopy_empty by fastforce
qed

lemma Brouwer_degree2_id [simp]: "Brouwer_degree2 p id = 1"
proof (rule Brouwer_degree2_unique)
  fix x
  assume x: "x ∈ carrier (reduced_homology_group (int p) (nsphere p))"
  then have "x ∈ carrier (homology_group (int p) (nsphere p))"
    using carrier_reduced_homology_group_subset by blast
  then show "hom_induced (int p) (nsphere p) {} (nsphere p) {} id x =
        x [^]🪙reduced_homology_group (int p) (nsphere p)🪙 (1::int)"
    by (simp add: hom_induced_id group.int_pow_1 x)
qed auto

lemma Brouwer_degree2_compose:
  assumes f: "continuous_map (nsphere p) (nsphere p) f" and g: "continuous_map (nsphere p) (nsphere p) g"
  shows "Brouwer_degree2 p (g ∘ f) = Brouwer_degree2 p g * Brouwer_degree2 p f"
proof (rule Brouwer_degree2_unique)
  show "continuous_map (nsphere p) (nsphere p) (g ∘ f)"
    by (meson continuous_map_compose f g)
next
  fix x
  assume x: "x ∈ carrier (reduced_homology_group (int p) (nsphere p))"
  have "hom_induced (int p) (nsphere p) {} (nsphere p) {} (g ∘ f) =
             hom_induced (int p) (nsphere p) {} (nsphere p) {} g ∘
             hom_induced (int p) (nsphere p) {} (nsphere p) {} f"
    by (blast intro: hom_induced_compose [OF f _ g])
  with x show "hom_induced (int p) (nsphere p) {} (nsphere p) {} (g ∘ f) x =
        x [^]🪙reduced_homology_group (int p) (nsphere p)🪙 (Brouwer_degree2 p g * Brouwer_degree2 p f)"
    by (simp add: mult.commute hom_induced_reduced flip: Brouwer_degree2 group.int_pow_pow)
qed

lemma Brouwer_degree2_homotopy_equivalence:
  assumes f: "continuous_map (nsphere p) (nsphere p) f" and g: "continuous_map (nsphere p) (nsphere p) g"
    and hom: "homotopic_with (λx. True) (nsphere p) (nsphere p) (f ∘ g) id"
  obtains "∣Brouwer_degree2 p f∣ = 1" "∣Brouwer_degree2 p g∣ = 1" "Brouwer_degree2 p g = Brouwer_degree2 p f"
  using Brouwer_degree2_homotopic [OF hom] Brouwer_degree2_compose f g zmult_eq_1_iff by auto

lemma Brouwer_degree2_homeomorphic_maps:
  assumes "homeomorphic_maps (nsphere p) (nsphere p) f g"
  obtains "∣Brouwer_degree2 p f∣ = 1" "∣Brouwer_degree2 p g∣ = 1" "Brouwer_degree2 p g = Brouwer_degree2 p f"
  using assms
  by (auto simp: homeomorphic_maps_def homotopic_with_equal continuous_map_compose intro: Brouwer_degree2_homotopy_equivalence)


lemma Brouwer_degree2_retraction_map:
  assumes "retraction_map (nsphere p) (nsphere p) f"
  shows "∣Brouwer_degree2 p f∣ = 1"
proof -
  obtain g where g: "retraction_maps (nsphere p) (nsphere p) f g"
    using assms by (auto simp: retraction_map_def)
  show ?thesis
  proof (rule Brouwer_degree2_homotopy_equivalence)
    show "homotopic_with (λx. True) (nsphere p) (nsphere p) (f ∘ g) id"
      using g apply (auto simp: retraction_maps_def)
      by (simp add: homotopic_with_equal continuous_map_compose)
    show "continuous_map (nsphere p) (nsphere p) f" "continuous_map (nsphere p) (nsphere p) g"
      using g retraction_maps_def by blast+
  qed
qed

lemma Brouwer_degree2_section_map:
  assumes "section_map (nsphere p) (nsphere p) f"
  shows "∣Brouwer_degree2 p f∣ = 1"
proof -
  obtain g where g: "retraction_maps (nsphere p) (nsphere p) g f"
    using assms by (auto simp: section_map_def)
  show ?thesis
  proof (rule Brouwer_degree2_homotopy_equivalence)
    show "homotopic_with (λx. True) (nsphere p) (nsphere p) (g ∘ f) id"
      using g apply (auto simp: retraction_maps_def)
      by (simp add: homotopic_with_equal continuous_map_compose)
    show "continuous_map (nsphere p) (nsphere p) g" "continuous_map (nsphere p) (nsphere p) f"
      using g retraction_maps_def by blast+
  qed
qed

lemma Brouwer_degree2_homeomorphic_map:
   "homeomorphic_map (nsphere p) (nsphere p) f ==> ∣Brouwer_degree2 p f∣ = 1"
  using Brouwer_degree2_retraction_map section_and_retraction_eq_homeomorphic_map by blast


lemma Brouwer_degree2_nullhomotopic:
  assumes "homotopic_with (λx. True) (nsphere p) (nsphere p) f (λx. a)"
  shows "Brouwer_degree2 p f = 0"
proof -
  have contf: "continuous_map (nsphere p) (nsphere p) f"
   and contc: "continuous_map (nsphere p) (nsphere p) (λx. a)"
    using homotopic_with_imp_continuous_maps [OF assms] by metis+
  have "Brouwer_degree2 p f = Brouwer_degree2 p (λx. a)"
    using Brouwer_degree2_homotopic [OF assms] .
  moreover
  let ?G = "reduced_homology_group (int p) (nsphere p)"
  interpret group ?G
    by simp
  have "Brouwer_degree2 p (λx. a) = 0"
  proof (rule Brouwer_degree2_unique [OF contc])
    fix c
    assume c: "c ∈ carrier ?G"
    have "continuous_map (nsphere p) (subtopology (nsphere p) {a}) (λf. a)"
      using contc continuous_map_in_subtopology by blast
    then have he: "hom_induced p (nsphere p) {} (nsphere p) {} (λx. a)
                 = hom_induced p (subtopology (nsphere p) {a}) {} (nsphere p) {} id ∘
                   hom_induced p (nsphere p) {} (subtopology (nsphere p) {a}) {} (λx. a)"
      by (metis continuous_map_id_subt fun.map_id hom_induced_compose_empty)
    have 1: "hom_induced p (nsphere p) {} (subtopology (nsphere p) {a}) {} (λx. a) c =
             1🪙reduced_homology_group (int p) (subtopology (nsphere p) {a})🪙"
      using c trivial_reduced_homology_group_contractible_space [of "subtopology (nsphere p) {a}" p]
      by (simp add: hom_induced_reduced contractible_space_subtopology_singleton trivial_group_subset group.trivial_group_subset subset_iff)
    show "hom_induced (int p) (nsphere p) {} (nsphere p) {} (λx. a) c =
        c [^]🪙?G🪙 (0::int)"
      apply (simp add: he 1)
      using hom_induced_reduced_hom group_hom.hom_one group_hom_axioms_def group_hom_def group_reduced_homology_group by blast
  qed
  ultimately show ?thesis
    by metis
qed


lemma Brouwer_degree2_const: "Brouwer_degree2 p (λx. a) = 0"
proof (cases "continuous_map(nsphere p) (nsphere p) (λx. a)")
  case True
  then show ?thesis
    by (auto intro: Brouwer_degree2_nullhomotopic [where a=a])
next
  case False
  let ?G = "reduced_homology_group (int p) (nsphere p)"
  let ?H = "homology_group (int p) (nsphere p)"
  interpret group ?G
    by simp
  have eq1: "1🪙?H🪙 = 1🪙?G🪙"
    by (simp add: one_reduced_homology_group)
  have *: "∀x∈carrier ?G. hom_induced (int p) (nsphere p) {} (nsphere p) {} (λx. a) x = 1🪙?H🪙"
    by (metis False hom_induced_default one_relative_homology_group)
  obtain c where c: "c ∈ carrier ?G" and ceq: "subgroup_generated ?G {c} = ?G"
    using cyclic_reduced_homology_group_nsphere [of p p] by (force simp: cyclic_group_def)
  have [simp]: "ord c = 0"
    by (simp add: c ceq iso_finite [OF reduced_homology_group_nsphere(1)] flip: infinite_cyclic_subgroup_order)
  show ?thesis
    unfolding Brouwer_degree2_def
  proof (rule some_equality)
    fix d :: "int"
    assume "∀x∈carrier ?G. hom_induced (int p) (nsphere p) {} (nsphere p) {} (λx. a) x = x [^]🪙?G🪙 d"
    then have "c [^]🪙?G🪙 d = 1🪙?H🪙"
      using "*" c by blast
    then have "int (ord c) dvd d"
      using c eq1 int_pow_eq_id by auto
    then show "d = 0"
      by (simp add: * del: one_relative_homology_group)
  qed (use "*" eq1 in force)
qed


corollary Brouwer_degree2_nonsurjective:
   "[continuous_map(nsphere p) (nsphere p) f; f ` topspace (nsphere p) ≠ topspace (nsphere p)]
    ==> Brouwer_degree2 p f = 0"
  by (meson Brouwer_degree2_nullhomotopic nullhomotopic_nonsurjective_sphere_map)


proposition Brouwer_degree2_reflection:
  "Brouwer_degree2 p (λx i. if i = 0 then -x i else x i) = -1" (is "Brouwer_degree2 _ ?r = -1")
proof (induction p)
  case 0
  let ?G = "homology_group 0 (nsphere 0)"
  let ?D = "homology_group 0 (discrete_topology {()})"
  interpret group ?G
    by simp
  define r where "r ≡ λx::nat==>real. λi. if i = 0 then -x i else x i"
  then have [simp]: "r ∘ r = id"
    by force
  have cmr: "continuous_map (nsphere 0) (nsphere 0) r"
    by (simp add: r_def continuous_map_nsphere_reflection)
  have *: "hom_induced 0 (nsphere 0) {} (nsphere 0) {} r c = inv🪙?G🪙 c"
    if "c ∈ carrier(reduced_homology_group 0 (nsphere 0))" for c
  proof -
    have c: "c ∈ carrier ?G"
      and ceq: "hom_induced 0 (nsphere 0) {} (discrete_topology {()}) {} (λx. ()) c = 1🪙?D🪙"
      using that by (auto simp: carrier_reduced_homology_group kernel_def)
    define pp::"nat==>real" where "pp ≡ λi. if i = 0 then 1 else 0"
    define nn::"nat==>real" where "nn ≡ λi. if i = 0 then -1 else 0"
    have topn0: "topspace(nsphere 0) = {pp,nn}"
      by (auto simp: nsphere pp_def nn_def fun_eq_iff power2_eq_1_iff split: if_split_asm)
    have "t1_space (nsphere 0)"
      unfolding nsphere
      apply (rule t1_space_subtopology)
      by (metis (full_types) open_fun_def t1_space t1_space_def)
    then have dtn0: "discrete_topology {pp,nn} = nsphere 0"
      using finite_t1_space_imp_discrete_topology [OF topn0] by auto
    have "pp ≠ nn"
      by (auto simp: pp_def nn_def fun_eq_iff)
    have [simp]: "r pp = nn" "r nn = pp"
      by (auto simp: r_def pp_def nn_def fun_eq_iff)
    have iso: "(λ(a,b). hom_induced 0 (subtopology (nsphere 0) {pp}) {} (nsphere 0) {} id a
                  ⊗🪙?G🪙 hom_induced 0 (subtopology (nsphere 0) {nn}) {} (nsphere 0) {} id b)
            ∈ iso (homology_group 0 (subtopology (nsphere 0) {pp}) ×× homology_group 0 (subtopology (nsphere 0) {nn}))
                  ?G" (is "?f ∈ iso (?P ×× ?N) ?G")
      apply (rule homology_additivity_explicit)
      using dtn0 ‹pp ≠ nn› by (auto simp: discrete_topology_unique)
    then have fim: "?f ` carrier(?P ×× ?N) = carrier ?G"
      by (simp add: iso_def bij_betw_def)
    obtain d d' where d: "d ∈ carrier ?P" and d': "d' ∈ carrier ?N" and eqc: "?f(d,d') = c"
      using c by (force simp flip: fim)
    let ?h = "λxx. hom_induced 0 (subtopology (nsphere 0) {xx}) {} (discrete_topology {()}) {} (λx. ())"
    have "continuous_map (subtopology (nsphere 0) {nn}) (nsphere 0) r"
      using cmr continuous_map_from_subtopology by blast
    then have "retraction_map (subtopology (nsphere 0) {pp}) (subtopology (nsphere 0) {nn}) r"
      apply (simp add: retraction_map_def retraction_maps_def continuous_map_in_subtopology)
      using ‹r nn = pp› ‹r pp = nn› cmr continuous_map_from_subtopology
      by blast
    then have "carrier ?N = (hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere 0) {nn}) {} r) ` carrier ?P"
      by (rule surj_hom_induced_retraction_map)
    then obtain e where e: "e ∈ carrier ?P" and eqd': "hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere 0) {nn}) {} r e = d'"
      using d' by auto
    have "section_map (subtopology (nsphere 0) {pp}) (discrete_topology {()}) (λx. ())"
      by (force simp: section_map_def retraction_maps_def topn0)
    then have "?h pp ∈ mon ?P ?D"
      by (rule mon_hom_induced_section_map)
    then have one: "x = one ?P"
      if "?h pp x = 1🪙?D🪙" "x ∈ carrier ?P" for x
      using that by (simp add: mon_iff_hom_one)
    interpret hpd: group_hom ?P ?D "?h pp"
      using hom_induced_empty_hom by (simp add: hom_induced_empty_hom group_hom_axioms_def group_hom_def)
    interpret hgd: group_hom ?G ?D "hom_induced 0 (nsphere 0) {} (discrete_topology {()}) {} (λx. ())"
      using hom_induced_empty_hom by (simp add: hom_induced_empty_hom group_hom_axioms_def group_hom_def)
    interpret hpg: group_hom ?P ?G "hom_induced 0 (subtopology (nsphere 0) {pp}) {} (nsphere 0) {} r"
      using hom_induced_empty_hom by (simp add: hom_induced_empty_hom group_hom_axioms_def group_hom_def)
    interpret hgg: group_hom ?G ?G "hom_induced 0 (nsphere 0) {} (nsphere 0) {} r"
      using hom_induced_empty_hom by (simp add: hom_induced_empty_hom group_hom_axioms_def group_hom_def)
    have "?h pp d =
          (hom_induced 0 (nsphere 0) {} (discrete_topology {()}) {} (λx. ())
           ∘ hom_induced 0 (subtopology (nsphere 0) {pp}) {} (nsphere 0) {} id) d"
      by (simp flip: hom_induced_compose_empty)
    moreover
    have "?h pp = ?h nn ∘ hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere 0) {nn}) {} r"
      by (simp add: cmr continuous_map_from_subtopology continuous_map_in_subtopology image_subset_iff flip: hom_induced_compose_empty)
    then have "?h pp e =
               (hom_induced 0 (nsphere 0) {} (discrete_topology {()}) {} (λx. ())
                ∘ hom_induced 0 (subtopology (nsphere 0) {nn}) {} (nsphere 0) {} id) d'"
      by (simp flip: hom_induced_compose_empty eqd')
    ultimately have "?h pp (d ⊗🪙?P🪙 e) = hom_induced 0 (nsphere 0) {} (discrete_topology {()}) {} (λx. ()) (?f(d,d'))"
      by (simp add: d e hom_induced_carrier)
    then have "?h pp (d ⊗🪙?P🪙 e) = 1🪙?D🪙"
      using ceq eqc by simp
    then have inv_p: "inv🪙?P🪙 d = e"
      by (metis (no_types, lifting) Group.group_def d e group.inv_equality group.r_inv group_relative_homology_group one monoid.m_closed)
    have cmr_pn: "continuous_map (subtopology (nsphere 0) {pp}) (subtopology (nsphere 0) {nn}) r"
      by (simp add: cmr continuous_map_from_subtopology continuous_map_in_subtopology image_subset_iff)
    then have "hom_induced 0 (subtopology (nsphere 0) {pp}) {} (nsphere 0) {} (id ∘ r) =
               hom_induced 0 (subtopology (nsphere 0) {nn}) {} (nsphere 0) {} id ∘
               hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere 0) {nn}) {} r"
      using hom_induced_compose_empty continuous_map_id_subt by blast
    then have "inv🪙?G🪙 hom_induced 0 (subtopology (nsphere 0) {pp}) {} (nsphere 0) {} r d =
                  hom_induced 0 (subtopology (nsphere 0) {nn}) {} (nsphere 0) {} id d'"
      apply (simp add: flip: inv_p eqd')
      using d hpg.hom_inv by auto
    then have c: "c = (hom_induced 0 (subtopology (nsphere 0) {pp}) {} (nsphere 0) {} id d)
                       ⊗🪙?G🪙 inv🪙?G🪙 (hom_induced 0 (subtopology (nsphere 0) {pp}) {} (nsphere 0) {} r d)"
      by (simp flip: eqc)
    have "hom_induced 0 (nsphere 0) {} (nsphere 0) {} r ∘
          hom_induced 0 (subtopology (nsphere 0) {pp}) {} (nsphere 0) {} id =
          hom_induced 0 (subtopology (nsphere 0) {pp}) {} (nsphere 0) {} r"
      by (metis cmr comp_id continuous_map_id_subt hom_induced_compose_empty)
    moreover
    have "hom_induced 0 (nsphere 0) {} (nsphere 0) {} r ∘
          hom_induced 0 (subtopology (nsphere 0) {pp}) {} (nsphere 0) {} r =
          hom_induced 0 (subtopology (nsphere 0) {pp}) {} (nsphere 0) {} id"
      by (metis ‹r ∘ r = id› cmr continuous_map_from_subtopology hom_induced_compose_empty)
    ultimately show ?thesis
      by (metis inv_p c comp_def d e hgg.hom_inv hgg.hom_mult hom_induced_carrier hpd.G.inv_inv hpg.hom_inv inv_mult_group)
  qed
  show ?case
    unfolding r_def [symmetric]
    using Brouwer_degree2_unique [OF cmr]
    by (auto simp: * group.int_pow_neg group.int_pow_1 reduced_homology_group_def intro!: Brouwer_degree2_unique [OF cmr])
next
  case (Suc p)
  let ?G = "reduced_homology_group (int p) (nsphere p)"
  let ?G1 = "reduced_homology_group (1 + int p) (nsphere (Suc p))"
  obtain f g where fg: "group_isomorphisms ?G ?G1 f g"
    and *: "∀c∈carrier ?G.
           hom_induced (1 + int p) (nsphere (Suc p)) {} (nsphere (Suc p)) {} ?r (f c) =
           f (hom_induced p (nsphere p) {} (nsphere p) {} ?r c)"
    using reduced_homology_group_nsphere_step
    by (meson group.iso_iff_group_isomorphisms group_reduced_homology_group)
  then have eq: "carrier ?G1 = f ` carrier ?G"
    by (fastforce simp add: iso_iff dest: group_isomorphisms_imp_iso)
  interpret group_hom ?G ?G1 f
    by (meson fg group_hom_axioms_def group_hom_def group_isomorphisms_def group_reduced_homology_group)
  have homf: "f ∈ hom ?G ?G1"
    using fg group_isomorphisms_def by blast
  have "hom_induced (1 + int p) (nsphere (Suc p)) {} (nsphere (Suc p)) {} ?r (f y) = f y [^]🪙?G1🪙 (-1::int)"
    if "y ∈ carrier ?G" for y
    by (simp add: that * Brouwer_degree2 Suc hom_int_pow)
  then show ?case
    by (fastforce simp: eq intro: Brouwer_degree2_unique [OF continuous_map_nsphere_reflection])
qed

end