Theory Invariance_of_Domain

section‹Invariance of Domain›

theory Invariance_of_Domain
  imports Brouwer_Degree "HOL-Analysis.Continuous_Extension" "HOL-Analysis.Homeomorphism"

begin

subsection‹Degree invariance mod 2 for map between pairs›

theorem Borsuk_odd_mapping_degree_step:
  assumes cmf: "continuous_map (nsphere n) (nsphere n) f"
    and f: "x. x  topspace(nsphere n)  (f  (λx i. -x i)) x = ((λx i. -x i)  f) x"
    and fim: "f ` (topspace(nsphere(n - Suc 0)))  topspace(nsphere(n - Suc 0))"
  shows "even (Brouwer_degree2 n f - Brouwer_degree2 (n - Suc 0) f)"
proof (cases "n = 0")
  case False
  define neg where "neg  λx::natreal. λi. -x i"
  define upper where "upper  λn. {x::natreal. x n  0}"
  define lower where "lower  λn. {x::natreal. x n  0}"
  define equator where "equator  λn. {x::natreal. x n = 0}"
  define usphere where "usphere  λn. subtopology (nsphere n) (upper n)"
  define lsphere where "lsphere  λn. subtopology (nsphere n) (lower n)"
  have [simp]: "neg x i = -x i" for x i
    by (force simp: neg_def)
  have equator_upper: "equator n  upper n"
    by (force simp: equator_def upper_def)
  have upper_usphere: "subtopology (nsphere n) (upper n) = usphere n"
    by (simp add: usphere_def)
  let ?rhgn = "relative_homology_group n (nsphere n)"
  let ?hi_ee = "hom_induced n (nsphere n) (equator n) (nsphere n) (equator n)"
  interpret GE: comm_group "?rhgn (equator n)"
    by simp
  interpret HB: group_hom "?rhgn (equator n)"
                          "homology_group (int n - 1) (subtopology (nsphere n) (equator n))"
                          "hom_boundary n (nsphere n) (equator n)"
    by (simp add: group_hom_axioms_def group_hom_def hom_boundary_hom)
  interpret HIU: group_hom "?rhgn (equator n)"
                           "?rhgn (upper n)"
                           "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id"
    by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom)
  have subt_eq: "subtopology (nsphere n) {x. x n = 0} = nsphere (n - Suc 0)"
    by (metis False Suc_pred le_zero_eq not_le subtopology_nsphere_equator)
  then have equ: "subtopology (nsphere n) (equator n) = nsphere(n - Suc 0)"
    "subtopology (lsphere n) (equator n) = nsphere(n - Suc 0)"
    "subtopology (usphere n) (equator n) = nsphere(n - Suc 0)"
    using False by (auto simp: lsphere_def usphere_def equator_def lower_def upper_def subtopology_subtopology simp flip: Collect_conj_eq cong: rev_conj_cong)
  have cmr: "continuous_map (nsphere(n - Suc 0)) (nsphere(n - Suc 0)) f"
    by (metis (no_types, lifting) IntE cmf fim continuous_map_from_subtopology continuous_map_in_subtopology equ(1) image_subset_iff topspace_subtopology)

  have "f x n = 0" if "x  topspace (nsphere n)" "x n = 0" for x
  proof -
    have "x  topspace (nsphere (n - Suc 0))"
      by (simp add: that topspace_nsphere_minus1)
    moreover have "topspace (nsphere n)  {f. f n = 0} = topspace (nsphere (n - Suc 0))"
      by (metis subt_eq topspace_subtopology)
    ultimately show ?thesis
      using fim by auto
  qed
  then have fimeq: "f ` (topspace (nsphere n)  equator n)  topspace (nsphere n)  equator n"
    using fim cmf by (auto simp: equator_def continuous_map_def image_subset_iff)
  have "k. continuous_map (powertop_real UNIV) euclideanreal (λx. - x k)"
    by (metis UNIV_I continuous_map_product_projection continuous_map_minus)
  then have cm_neg: "continuous_map (nsphere m) (nsphere m) neg" for m
    by (force simp: nsphere continuous_map_in_subtopology neg_def continuous_map_componentwise_UNIV intro: continuous_map_from_subtopology)
  then have cm_neg_lu: "continuous_map (lsphere n) (usphere n) neg"
      by (auto simp: lsphere_def usphere_def lower_def upper_def continuous_map_from_subtopology continuous_map_in_subtopology)
  have neg_in_top_iff: "neg x  topspace(nsphere m)  x  topspace(nsphere m)" for m x
    by (simp add: nsphere_def neg_def topspace_Euclidean_space)
  obtain z where zcarr: "z  carrier (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))"
    and zeq: "subgroup_generated (reduced_homology_group (int n - 1) (nsphere (n - Suc 0))) {z}
              = reduced_homology_group (int n - 1) (nsphere (n - Suc 0))"
    using cyclic_reduced_homology_group_nsphere [of "int n - 1" "n - Suc 0"] by (auto simp: cyclic_group_def)
  have "hom_boundary n (subtopology (nsphere n) {x. x n  0}) {x. x n = 0}
       Group.iso (relative_homology_group n
                     (subtopology (nsphere n) {x. x n  0}) {x. x n = 0})
                  (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))"
    using iso_lower_hemisphere_reduced_homology_group [of "int n - 1" "n - Suc 0"] False by simp
  then obtain gp where g: "group_isomorphisms
                          (relative_homology_group n (subtopology (nsphere n) {x. x n  0}) {x. x n = 0})
                          (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))
                          (hom_boundary n (subtopology (nsphere n) {x. x n  0}) {x. x n = 0})
                          gp"
    by (auto simp: group.iso_iff_group_isomorphisms)
  then interpret gp: group_hom "reduced_homology_group (int n - 1) (nsphere (n - Suc 0))"
    "relative_homology_group n (subtopology (nsphere n) {x. x n  0}) {x. x n = 0}" gp
    by (simp add: group_hom_axioms_def group_hom_def group_isomorphisms_def)
  obtain zp where zpcarr: "zp  carrier(relative_homology_group n (lsphere n) (equator n))"
    and zp_z: "hom_boundary n (lsphere n) (equator n) zp = z"
    and zp_sg: "subgroup_generated (relative_homology_group n (lsphere n) (equator n)) {zp}
                = relative_homology_group n (lsphere n) (equator n)"
  proof
    show "gp z  carrier (relative_homology_group n (lsphere n) (equator n))"
      "hom_boundary n (lsphere n) (equator n) (gp z) = z"
      using g zcarr by (auto simp: lsphere_def equator_def lower_def group_isomorphisms_def)
    have giso: "gp  Group.iso (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))
                     (relative_homology_group n (subtopology (nsphere n) {x. x n  0}) {x. x n = 0})"
      by (metis (mono_tags, lifting) g group_isomorphisms_imp_iso group_isomorphisms_sym)
    show "subgroup_generated (relative_homology_group n (lsphere n) (equator n)) {gp z} =
        relative_homology_group n (lsphere n) (equator n)"
      apply (rule monoid.equality)
      using giso gp.subgroup_generated_by_image [of "{z}"] zcarr
      by (auto simp: lsphere_def equator_def lower_def zeq gp.iso_iff)
  qed
  have hb_iso: "hom_boundary n (subtopology (nsphere n) {x. x n  0}) {x. x n = 0}
             iso (relative_homology_group n (subtopology (nsphere n) {x. x n  0}) {x. x n = 0})
                  (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))"
    using iso_upper_hemisphere_reduced_homology_group [of "int n - 1" "n - Suc 0"] False by simp
  then obtain gn where g: "group_isomorphisms
                          (relative_homology_group n (subtopology (nsphere n) {x. x n  0}) {x. x n = 0})
                          (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))
                          (hom_boundary n (subtopology (nsphere n) {x. x n  0}) {x. x n = 0})
                          gn"
    by (auto simp: group.iso_iff_group_isomorphisms)
  then interpret gn: group_hom "reduced_homology_group (int n - 1) (nsphere (n - Suc 0))"
    "relative_homology_group n (subtopology (nsphere n) {x. x n  0}) {x. x n = 0}" gn
    by (simp add: group_hom_axioms_def group_hom_def group_isomorphisms_def)
  obtain zn where zncarr: "zn  carrier(relative_homology_group n (usphere n) (equator n))"
    and zn_z: "hom_boundary n (usphere n) (equator n) zn = z"
    and zn_sg: "subgroup_generated (relative_homology_group n (usphere n) (equator n)) {zn}
                 = relative_homology_group n (usphere n) (equator n)"
  proof
    show "gn z  carrier (relative_homology_group n (usphere n) (equator n))"
      "hom_boundary n (usphere n) (equator n) (gn z) = z"
      using g zcarr by (auto simp: usphere_def equator_def upper_def group_isomorphisms_def)
    have giso: "gn  Group.iso (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))
                     (relative_homology_group n (subtopology (nsphere n) {x. x n  0}) {x. x n = 0})"
      by (metis (mono_tags, lifting) g group_isomorphisms_imp_iso group_isomorphisms_sym)
    show "subgroup_generated (relative_homology_group n (usphere n) (equator n)) {gn z} =
        relative_homology_group n (usphere n) (equator n)"
      apply (rule monoid.equality)
      using giso gn.subgroup_generated_by_image [of "{z}"] zcarr
      by (auto simp: usphere_def equator_def upper_def zeq gn.iso_iff)
  qed
  let ?hi_lu = "hom_induced n (lsphere n) (equator n) (nsphere n) (upper n) id"
  interpret gh_lu: group_hom "relative_homology_group n (lsphere n) (equator n)" "?rhgn (upper n)" ?hi_lu
    by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom)
  interpret gh_eef: group_hom "?rhgn (equator n)" "?rhgn (equator n)" "?hi_ee f"
    by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom)
  define wp where "wp  ?hi_lu zp"
  then have wpcarr: "wp  carrier(?rhgn (upper n))"
    by (simp add: hom_induced_carrier)
  have "hom_induced n (nsphere n) {} (nsphere n) {x. x n  0} id
       iso (reduced_homology_group n (nsphere n))
            (?rhgn {x. x n  0})"
    using iso_reduced_homology_group_upper_hemisphere [of n n n] by auto
  then have "carrier(?rhgn {x. x n  0})
           (hom_induced n (nsphere n) {} (nsphere n) {x. x n  0} id)
                         ` carrier(reduced_homology_group n (nsphere n))"
    by (simp add: iso_iff)
  then obtain vp where vpcarr: "vp  carrier(reduced_homology_group n (nsphere n))"
    and eqwp: "hom_induced n (nsphere n) {} (nsphere n) (upper n) id vp = wp"
    using wpcarr by (auto simp: upper_def)
  define wn where "wn  hom_induced n (usphere n) (equator n) (nsphere n) (lower n) id zn"
  then have wncarr: "wn  carrier(?rhgn (lower n))"
    by (simp add: hom_induced_carrier)
  have "hom_induced n (nsphere n) {} (nsphere n) {x. x n  0} id
       iso (reduced_homology_group n (nsphere n))
            (?rhgn {x. x n  0})"
    using iso_reduced_homology_group_lower_hemisphere [of n n n] by auto
  then have "carrier(?rhgn {x. x n  0})
           (hom_induced n (nsphere n) {} (nsphere n) {x. x n  0} id)
                         ` carrier(reduced_homology_group n (nsphere n))"
    by (simp add: iso_iff)
  then obtain vn where vpcarr: "vn  carrier(reduced_homology_group n (nsphere n))"
    and eqwp: "hom_induced n (nsphere n) {} (nsphere n) (lower n) id vn = wn"
    using wncarr by (auto simp: lower_def)
  define up where "up  hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id zp"
  then have upcarr: "up  carrier(?rhgn (equator n))"
    by (simp add: hom_induced_carrier)
  define un where "un  hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id zn"
  then have uncarr: "un  carrier(?rhgn (equator n))"
    by (simp add: hom_induced_carrier)
  have *: "(λ(x, y).
            hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id x
          ?rhgn (equator n)hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id y)
         Group.iso
            (relative_homology_group n (lsphere n) (equator n) ××
             relative_homology_group n (usphere n) (equator n))
            (?rhgn (equator n))"
  proof (rule conjunct1 [OF exact_sequence_sum_lemma [OF abelian_relative_homology_group]])
    show "hom_induced n (lsphere n) (equator n) (nsphere n) (upper n) id
         Group.iso (relative_homology_group n (lsphere n) (equator n))
            (?rhgn (upper n))"
      apply (simp add: lsphere_def usphere_def equator_def lower_def upper_def)
      using iso_relative_homology_group_lower_hemisphere by blast
    show "hom_induced n (usphere n) (equator n) (nsphere n) (lower n) id
         Group.iso (relative_homology_group n (usphere n) (equator n))
            (?rhgn (lower n))"
      apply (simp_all add: lsphere_def usphere_def equator_def lower_def upper_def)
      using iso_relative_homology_group_upper_hemisphere by blast+
    show "exact_seq
         ([?rhgn (lower n),
           ?rhgn (equator n),
           relative_homology_group n (lsphere n) (equator n)],
          [hom_induced n (nsphere n) (equator n) (nsphere n) (lower n) id,
           hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id])"
      unfolding lsphere_def usphere_def equator_def lower_def upper_def
      by (rule homology_exactness_triple_3) force
    show "exact_seq
         ([?rhgn (upper n),
           ?rhgn (equator n),
           relative_homology_group n (usphere n) (equator n)],
          [hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id,
           hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id])"
      unfolding lsphere_def usphere_def equator_def lower_def upper_def
      by (rule homology_exactness_triple_3) force
  next
    fix x
    assume "x  carrier (relative_homology_group n (lsphere n) (equator n))"
    show "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id
         (hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id x) =
        hom_induced n (lsphere n) (equator n) (nsphere n) (upper n) id x"
      by (simp add: hom_induced_compose' subset_iff lsphere_def usphere_def equator_def lower_def upper_def)
  next
    fix x
    assume "x  carrier (relative_homology_group n (usphere n) (equator n))"
    show "hom_induced n (nsphere n) (equator n) (nsphere n) (lower n) id
         (hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id x) =
        hom_induced n (usphere n) (equator n) (nsphere n) (lower n) id x"
      by (simp add: hom_induced_compose' subset_iff lsphere_def usphere_def equator_def lower_def upper_def)
  qed
  then have sb: "carrier (?rhgn (equator n))
              (λ(x, y).
            hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id x
          ?rhgn (equator n)hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id y)
               ` carrier (relative_homology_group n (lsphere n) (equator n) ××
             relative_homology_group n (usphere n) (equator n))"
    by (simp add: iso_iff)
  obtain a b::int
    where up_ab: "?hi_ee f up
             = up [^]?rhgn (equator n)a?rhgn (equator n)un [^]?rhgn (equator n)b"
  proof -
    have hiupcarr: "?hi_ee f up  carrier(?rhgn (equator n))"
      by (simp add: hom_induced_carrier)
    obtain u v where u: "u  carrier (relative_homology_group n (lsphere n) (equator n))"
      and v: "v  carrier (relative_homology_group n (usphere n) (equator n))"
      and eq: "?hi_ee f up =
                hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id u
                ?rhgn (equator n)hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id v"
      using subsetD [OF sb hiupcarr] by auto
    have "u  carrier (subgroup_generated (relative_homology_group n (lsphere n) (equator n)) {zp})"
      by (simp_all add: u zp_sg)
    then obtain a::int where a: "u = zp [^]relative_homology_group n (lsphere n) (equator n)a"
      by (metis group.carrier_subgroup_generated_by_singleton group_relative_homology_group rangeE zpcarr)
    have ae: "hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id
            (pow (relative_homology_group n (lsphere n) (equator n)) zp a)
          = pow (?rhgn (equator n)) (hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id zp) a"
      by (meson group_hom.hom_int_pow group_hom_axioms_def group_hom_def group_relative_homology_group hom_induced zpcarr)
    have "v  carrier (subgroup_generated (relative_homology_group n (usphere n) (equator n)) {zn})"
      by (simp_all add: v zn_sg)
    then obtain b::int where b: "v = zn [^]relative_homology_group n (usphere n) (equator n)b"
      by (metis group.carrier_subgroup_generated_by_singleton group_relative_homology_group rangeE zncarr)
    have be: "hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id
           (zn [^]relative_homology_group n (usphere n) (equator n)b)
        = hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id
           zn [^]relative_homology_group n (nsphere n) (equator n)b"
      by (meson group_hom.hom_int_pow group_hom_axioms_def group_hom_def group_relative_homology_group hom_induced zncarr)
    show thesis
    proof
      show "?hi_ee f up
         = up [^]?rhgn (equator n)a ?rhgn (equator n)un [^]?rhgn (equator n)b"
        using a ae b be eq local.up_def un_def by auto
    qed
  qed
  have "(hom_boundary n (nsphere n) (equator n)
        hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id) zp = z"
    using zp_z equ apply (simp add: lsphere_def naturality_hom_induced)
    by (metis hom_boundary_carrier hom_induced_id)
  then have up_z: "hom_boundary n (nsphere n) (equator n) up = z"
    by (simp add: up_def)
  have "(hom_boundary n (nsphere n) (equator n)
        hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id) zn = z"
    using zn_z equ apply (simp add: usphere_def naturality_hom_induced)
    by (metis hom_boundary_carrier hom_induced_id)
  then have un_z: "hom_boundary n (nsphere n) (equator n) un = z"
    by (simp add: un_def)
  have Bd_ab: "Brouwer_degree2 (n - Suc 0) f = a + b"
  proof (rule Brouwer_degree2_unique_generator; use False int_ops in simp_all)
    show "continuous_map (nsphere (n - Suc 0)) (nsphere (n - Suc 0)) f"
      using cmr by auto
    show "subgroup_generated (reduced_homology_group (int n - 1) (nsphere (n - Suc 0))) {z} =
        reduced_homology_group (int n - 1) (nsphere (n - Suc 0))"
      using zeq by blast
    have "(hom_induced (int n - 1) (nsphere (n - Suc 0)) {} (nsphere (n - Suc 0)) {} f
            hom_boundary n (nsphere n) (equator n)) up
        = (hom_boundary n (nsphere n) (equator n) 
           ?hi_ee f) up"
      using naturality_hom_induced [OF cmf fimeq, of n, symmetric]
      by (simp add: subtopology_restrict equ fun_eq_iff)
    also have " = hom_boundary n (nsphere n) (equator n)
                       (up [^]relative_homology_group n (nsphere n) (equator n)a relative_homology_group n (nsphere n) (equator n)un [^]relative_homology_group n (nsphere n) (equator n)b)"
      by (simp add: o_def up_ab)
    also have " = z [^]reduced_homology_group (int n - 1) (nsphere (n - Suc 0))(a + b)"
      using zcarr
      apply (simp add: HB.hom_int_pow reduced_homology_group_def group.int_pow_subgroup_generated upcarr uncarr)
      by (metis equ(1) group.int_pow_mult group_relative_homology_group hom_boundary_carrier un_z up_z)
  finally show "hom_induced (int n - 1) (nsphere (n - Suc 0)) {} (nsphere (n - Suc 0)) {} f z =
        z [^]reduced_homology_group (int n - 1) (nsphere (n - Suc 0))(a + b)"
      by (simp add: up_z)
  qed
  define u where "u  up ?rhgn (equator n)inv?rhgn (equator n)un"
  have ucarr: "u  carrier (?rhgn (equator n))"
    by (simp add: u_def uncarr upcarr)
  then have "u [^]?rhgn (equator n)Brouwer_degree2 n f = u [^]?rhgn (equator n)(a - b)
              (GE.ord u) dvd a - b - Brouwer_degree2 n f"
    by (simp add: GE.int_pow_eq)
  moreover
  have "GE.ord u = 0"
  proof (clarsimp simp add: GE.ord_eq_0 ucarr)
    fix d :: nat
    assume "0 < d"
      and "u [^]?rhgn (equator n)d = singular_relboundary_set n (nsphere n) (equator n)"
    then have "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id u [^]?rhgn (upper n)d
               = 𝟭?rhgn (upper n)⇙"
      by (metis HIU.hom_one HIU.hom_nat_pow one_relative_homology_group ucarr)
    moreover
    have "?hi_lu
        = hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id 
          hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id"
      by (simp add: lsphere_def image_subset_iff equator_upper flip: hom_induced_compose)
    then have p: "wp = hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id up"
      by (simp add: local.up_def wp_def)
    have n: "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id un = 𝟭?rhgn (upper n)⇙"
      using homology_exactness_triple_3 [OF equator_upper, of n "nsphere n"]
      using un_def zncarr by (auto simp: upper_usphere kernel_def)
    have "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id u = wp"
      unfolding u_def
      using p n HIU.inv_one HIU.r_one uncarr upcarr by auto
    ultimately have "(wp [^]?rhgn (upper n)d) = 𝟭?rhgn (upper n)⇙"
      by simp
    moreover have "infinite (carrier (subgroup_generated (?rhgn (upper n)) {wp}))"
    proof -
      have "?rhgn (upper n)  reduced_homology_group n (nsphere n)"
        unfolding upper_def
        using iso_reduced_homology_group_upper_hemisphere [of n n n]
        by (blast intro: group.iso_sym group_reduced_homology_group is_isoI)
      also have "  integer_group"
        by (simp add: reduced_homology_group_nsphere)
      finally have iso: "?rhgn (upper n)  integer_group" .
      have "carrier (subgroup_generated (?rhgn (upper n)) {wp}) = carrier (?rhgn (upper n))"
        using gh_lu.subgroup_generated_by_image [of "{zp}"] zpcarr HIU.carrier_subgroup_generated_subset
          gh_lu.iso_iff iso_relative_homology_group_lower_hemisphere zp_sg
        by (auto simp: lower_def lsphere_def upper_def equator_def wp_def)
      then show ?thesis
        using infinite_UNIV_int iso_finite [OF iso] by simp
    qed
    ultimately show False
      using HIU.finite_cyclic_subgroup 0 < d wpcarr by blast
  qed
  ultimately have iff: "u [^]?rhgn (equator n)Brouwer_degree2 n f = u [^]?rhgn (equator n)(a - b)
                    Brouwer_degree2 n f = a - b"
    by auto
  have "u [^]?rhgn (equator n)Brouwer_degree2 n f = ?hi_ee f u"
  proof -
    have ne: "topspace (nsphere n)  equator n  {}"
      using False equator_def in_topspace_nsphere by fastforce
    have eq1: "hom_boundary n (nsphere n) (equator n) u
               = 𝟭reduced_homology_group (int n - 1) (subtopology (nsphere n) (equator n))⇙"
      using one_reduced_homology_group u_def un_z uncarr up_z upcarr by force
    then have uhom: "u  hom_induced n (nsphere n) {} (nsphere n) (equator n) id `
                         carrier (reduced_homology_group (int n) (nsphere n))"
      using homology_exactness_reduced_1 [OF ne, of n] eq1 ucarr by (auto simp: kernel_def)
    then obtain v where vcarr: "v  carrier (reduced_homology_group (int n) (nsphere n))"
                  and ueq: "u = hom_induced n (nsphere n) {} (nsphere n) (equator n) id v"
      by blast
    interpret GH_hi: group_hom "homology_group n (nsphere n)"
                        "?rhgn (equator n)"
                        "hom_induced n (nsphere n) {} (nsphere n) (equator n) id"
      by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom)
    have poweq: "pow (homology_group n (nsphere n)) x i = pow (reduced_homology_group n (nsphere n)) x i"
      for x and i::int
      by (simp add: False un_reduced_homology_group)
    have vcarr': "v  carrier (homology_group n (nsphere n))"
      using carrier_reduced_homology_group_subset vcarr by blast
    have "u [^]?rhgn (equator n)Brouwer_degree2 n f
          = hom_induced n (nsphere n) {} (nsphere n) (equator n) f v"
      using vcarr vcarr'
      by (simp add: ueq poweq hom_induced_compose' cmf flip: GH_hi.hom_int_pow Brouwer_degree2)
    also have " = hom_induced n (nsphere n) (topspace(nsphere n)  equator n) (nsphere n) (equator n) f
                     (hom_induced n (nsphere n) {} (nsphere n) (topspace(nsphere n)  equator n) id v)"
      using fimeq by (simp add: hom_induced_compose' cmf)
    also have " = ?hi_ee f u"
      by (metis hom_induced inf.left_idem ueq)
    finally show ?thesis .
  qed
  moreover
  interpret gh_een: group_hom "?rhgn (equator n)" "?rhgn (equator n)" "?hi_ee neg"
    by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom)
  have hi_up_eq_un: "?hi_ee neg up = un [^]?rhgn (equator n)Brouwer_degree2 (n - Suc 0) neg"
  proof -
    have "?hi_ee neg (hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id zp)
         = hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) (neg  id) zp"
      by (intro hom_induced_compose') (auto simp: lsphere_def equator_def cm_neg)
    also have " = hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id
            (hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg zp)"
      by (subst hom_induced_compose' [OF cm_neg_lu]) (auto simp: usphere_def equator_def)
    also have "hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg zp
             = zn [^]relative_homology_group n (usphere n) (equator n)Brouwer_degree2 (n - Suc 0) neg"
    proof -
      let ?hb = "hom_boundary n (usphere n) (equator n)"
      have eq: "subtopology (nsphere n) {x. x n  0} = usphere n  {x. x n = 0} = equator n"
        by (auto simp: usphere_def upper_def equator_def)
      with hb_iso have inj: "inj_on (?hb) (carrier (relative_homology_group n (usphere n) (equator n)))"
        by (simp add: iso_iff)
      interpret hb_hom: group_hom "relative_homology_group n (usphere n) (equator n)"
                                  "reduced_homology_group (int n - 1) (nsphere (n - Suc 0))"
                                  "?hb"
        using hb_iso iso_iff eq group_hom_axioms_def group_hom_def by fastforce
      show ?thesis
      proof (rule inj_onD [OF inj])
        have *: "hom_induced (int n - 1) (nsphere (n - Suc 0)) {} (nsphere (n - Suc 0)) {} neg z
                 = z [^]homology_group (int n - 1) (nsphere (n - Suc 0))Brouwer_degree2 (n - Suc 0) neg"
          using Brouwer_degree2 [of z "n - Suc 0" neg] False zcarr
          by (simp add: int_ops group.int_pow_subgroup_generated reduced_homology_group_def)
        have "?hb 
              hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg
            = hom_induced (int n - 1) (nsphere (n - Suc 0)) {} (nsphere (n - Suc 0)) {} neg 
              hom_boundary n (lsphere n) (equator n)"
          apply (subst naturality_hom_induced [OF cm_neg_lu])
           apply (force simp: equator_def neg_def)
          by (simp add: equ)
        then have "?hb
                    (hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg zp)
            = (z [^]homology_group (int n - 1) (nsphere (n - Suc 0))Brouwer_degree2 (n - Suc 0) neg)"
          by (metis "*" comp_apply zp_z)
        also have " = ?hb (zn [^]relative_homology_group n (usphere n) (equator n)Brouwer_degree2 (n - Suc 0) neg)"
          by (metis group.int_pow_subgroup_generated group_relative_homology_group hb_hom.hom_int_pow reduced_homology_group_def zcarr zn_z zncarr)
        finally show "?hb (hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg zp) =
        ?hb (zn [^]relative_homology_group n (usphere n) (equator n)Brouwer_degree2 (n - Suc 0) neg)" by simp
      qed (auto simp: hom_induced_carrier group.int_pow_closed zncarr)
    qed
    finally show ?thesis
      by (metis (no_types, lifting) group_hom.hom_int_pow group_hom_axioms_def group_hom_def group_relative_homology_group hom_induced local.up_def un_def zncarr)
  qed
  have "continuous_map (nsphere (n - Suc 0)) (nsphere (n - Suc 0)) neg"
    using cm_neg by blast
  then have "homeomorphic_map (nsphere (n - Suc 0)) (nsphere (n - Suc 0)) neg"
    apply (auto simp: homeomorphic_map_maps homeomorphic_maps_def)
    apply (rule_tac x=neg in exI, auto)
    done
  then have Brouwer_degree2_21: "Brouwer_degree2 (n - Suc 0) neg ^ 2 = 1"
    using Brouwer_degree2_homeomorphic_map power2_eq_1_iff by force
  have hi_un_eq_up: "?hi_ee neg un = up [^]?rhgn (equator n)Brouwer_degree2 (n - Suc 0) neg" (is "?f un = ?y")
  proof -
    have [simp]: "neg  neg = id"
      by force
    have "?f (?f ?y) = ?y"
      apply (subst hom_induced_compose' [OF cm_neg _ cm_neg])
       apply(force simp: equator_def)
      apply (simp add: upcarr hom_induced_id_gen)
      done
    moreover have "?f ?y = un"
      using upcarr apply (simp only: gh_een.hom_int_pow hi_up_eq_un)
      by (metis (no_types, lifting) Brouwer_degree2_21 GE.group_l_invI GE.l_inv_ex group.int_pow_1 group.int_pow_pow power2_eq_1_iff uncarr zmult_eq_1_iff)
    ultimately show "?f un = ?y"
      by simp
  qed
  have "?hi_ee f un = un [^]?rhgn (equator n)a ?rhgn (equator n)up [^]?rhgn (equator n)b"
  proof -
    let ?TE = "topspace (nsphere n)  equator n"
    have fneg: "(f  neg) x = (neg  f) x" if "x  topspace (nsphere n)" for x
      using f [OF that] by (force simp: neg_def)
    have neg_im: "neg ` (topspace (nsphere n)  equator n)  topspace (nsphere n)  equator n"
      by (metis cm_neg continuous_map_image_subset_topspace equ(1) topspace_subtopology)
    have 1: "hom_induced n (nsphere n) ?TE (nsphere n) ?TE f  hom_induced n (nsphere n) ?TE (nsphere n) ?TE neg
           = hom_induced n (nsphere n) ?TE (nsphere n) ?TE neg  hom_induced n (nsphere n) ?TE (nsphere n) ?TE f"
      using neg_im fimeq cm_neg cmf
      apply (simp add: flip: hom_induced_compose del: hom_induced_restrict)
      using fneg by (auto intro: hom_induced_eq)
    have "(un [^]?rhgn (equator n)a) ?rhgn (equator n)(up [^]?rhgn (equator n)b)
        = un [^]?rhgn (equator n)(Brouwer_degree2 (n - 1) neg * a * Brouwer_degree2 (n - 1) neg)
          ?rhgn (equator n)up [^]?rhgn (equator n)(Brouwer_degree2 (n - 1) neg * b * Brouwer_degree2 (n - 1) neg)"
    proof -
      have "Brouwer_degree2 (n - Suc 0) neg = 1  Brouwer_degree2 (n - Suc 0) neg = - 1"
        using Brouwer_degree2_21 power2_eq_1_iff by blast
      then show ?thesis
        by fastforce
    qed
    also have " = ((un [^]?rhgn (equator n)Brouwer_degree2 (n - 1) neg) [^]?rhgn (equator n)a ?rhgn (equator n)(up [^]?rhgn (equator n)Brouwer_degree2 (n - 1) neg) [^]?rhgn (equator n)b) [^]?rhgn (equator n)Brouwer_degree2 (n - 1) neg"
      by (simp add: GE.int_pow_distrib GE.int_pow_pow uncarr upcarr)
    also have " = ?hi_ee neg (?hi_ee f up) [^]?rhgn (equator n)Brouwer_degree2 (n - Suc 0) neg"
      by (simp add: gh_een.hom_int_pow hi_un_eq_up hi_up_eq_un uncarr up_ab upcarr)
    finally have 2: "(un [^]?rhgn (equator n)a) ?rhgn (equator n)(up [^]?rhgn (equator n)b)
             = ?hi_ee neg (?hi_ee f up) [^]?rhgn (equator n)Brouwer_degree2 (n - Suc 0) neg" .
    have "un = ?hi_ee neg up [^]?rhgn (equator n)Brouwer_degree2 (n - Suc 0) neg"
      by (metis (no_types, opaque_lifting) Brouwer_degree2_21 GE.int_pow_1 GE.int_pow_pow hi_up_eq_un power2_eq_1_iff uncarr zmult_eq_1_iff)
    moreover have "?hi_ee f ((?hi_ee neg up) [^]?rhgn (equator n)(Brouwer_degree2 (n - Suc 0) neg))
                 = un [^]?rhgn (equator n)a ?rhgn (equator n)up [^]?rhgn (equator n)b"
      using 1 2 by (simp add: hom_induced_carrier gh_eef.hom_int_pow fun_eq_iff)
    ultimately show ?thesis
      by blast
  qed
  then have "?hi_ee f u = u [^]?rhgn (equator n)(a - b)"
    by (simp add: u_def upcarr uncarr up_ab GE.int_pow_diff GE.m_ac GE.int_pow_distrib GE.int_pow_inv GE.inv_mult_group)
  ultimately
  have "Brouwer_degree2 n f = a - b"
    using iff by blast
  with Bd_ab show ?thesis
    by simp
qed simp


subsection ‹General Jordan-Brouwer separation theorem and invariance of dimension›

proposition relative_homology_group_Euclidean_complement_step:
  assumes "closedin (Euclidean_space n) S"
  shows "relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - S)
       relative_homology_group (p + k) (Euclidean_space (n+k)) (topspace(Euclidean_space (n+k)) - S)"
proof -
  have *: "relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - S)
            relative_homology_group (p + 1) (Euclidean_space (Suc n)) (topspace(Euclidean_space (Suc n)) - {x  S. x n = 0})"
    (is "?lhs  ?rhs")
    if clo: "closedin (Euclidean_space (Suc n)) S" and cong: "x y. x  S; i. i  n  x i = y i  y  S"
      for p n S
  proof -
    have Ssub: "S  topspace (Euclidean_space (Suc n))"
      by (meson clo closedin_def)
    define lo where "lo  {x  topspace(Euclidean_space (Suc n)). x n < (if x  S then 0 else 1)}"
    define hi where "hi = {x  topspace(Euclidean_space (Suc n)). x n > (if x  S then 0 else -1)}"
    have lo_hi_Int: "lo  hi = {x  topspace(Euclidean_space (Suc n)) - S. x n  {-1<..<1}}"
      by (auto simp: hi_def lo_def)
    have lo_hi_Un: "lo  hi = topspace(Euclidean_space (Suc n)) - {x  S. x n = 0}"
      by (auto simp: hi_def lo_def)
    define ret where "ret  λc::real. λx i. if i = n then c else x i"
    have cm_ret: "continuous_map (powertop_real UNIV) (powertop_real UNIV) (ret t)" for t
      by (auto simp: ret_def continuous_map_componentwise_UNIV intro: continuous_map_product_projection)
    let ?ST = "λt. subtopology (Euclidean_space (Suc n)) {x. x n = t}"
    define squashable where
      "squashable  λt S. x t'. x  S  (x n  t'  t'  t  t  t'  t'  x n)  ret t' x  S"
    have squashable: "squashable t (topspace(Euclidean_space(Suc n)))" for t
      by (simp add: squashable_def topspace_Euclidean_space ret_def)
    have squashableD: "squashable t S; x  S; x n  t'  t'  t  t  t'  t'  x n  ret t' x  S" for x t' t S
      by (auto simp: squashable_def)
    have "squashable 1 hi"
      by (force simp: squashable_def hi_def ret_def topspace_Euclidean_space intro: cong)
    have "squashable t UNIV" for t
      by (force simp: squashable_def hi_def ret_def topspace_Euclidean_space intro: cong)
    have squashable_0_lohi: "squashable 0 (lo  hi)"
      using Ssub
      by (auto simp: squashable_def hi_def lo_def ret_def topspace_Euclidean_space intro: cong)
    have rm_ret: "retraction_maps (subtopology (Euclidean_space (Suc n)) U)
                                  (subtopology (Euclidean_space (Suc n)) {x. x  U  x n = t})
                                  (ret t) id"
      if "squashable t U" for t U
      unfolding retraction_maps_def
    proof (intro conjI ballI)
      show "continuous_map (subtopology (Euclidean_space (Suc n)) U)
             (subtopology (Euclidean_space (Suc n)) {x  U. x n = t}) (ret t)"
        apply (simp add: cm_ret continuous_map_in_subtopology continuous_map_from_subtopology Euclidean_space_def)
        using that by (fastforce simp: squashable_def ret_def)
    next
      show "continuous_map (subtopology (Euclidean_space (Suc n)) {x  U. x n = t})
                           (subtopology (Euclidean_space (Suc n)) U) id"
        using continuous_map_in_subtopology by fastforce
      show "ret t (id x) = x"
        if "x  topspace (subtopology (Euclidean_space (Suc n)) {x  U. x n = t})" for x
        using that by (simp add: topspace_Euclidean_space ret_def fun_eq_iff)
    qed
    have cm_snd: "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (powertop_real UNIV) S))
                              euclideanreal (λx. snd x k)" for k::nat and S
      using continuous_map_componentwise_UNIV continuous_map_into_fulltopology continuous_map_snd by fastforce
    have cm_fstsnd: "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (powertop_real UNIV) S))
                              euclideanreal (λx. fst x * snd x k)" for k::nat and S
      by (intro continuous_intros continuous_map_into_fulltopology [OF continuous_map_fst] cm_snd)
    have hw_sub: "homotopic_with (λk. k ` V  V) (subtopology (Euclidean_space (Suc n)) U)
                                 (subtopology (Euclidean_space (Suc n)) U) (ret t) id"
      if "squashable t U" "squashable t V" for U V t
      unfolding homotopic_with_def
    proof (intro exI conjI allI ballI)
      let ?h = "λ(z,x). ret ((1 - z) * t + z * x n) x"
      show "(λx. ?h (u, x)) ` V  V" if "u  {0..1}" for u
        using that
        by clarsimp (metis squashableD [OF squashable t V] convex_bound_le diff_ge_0_iff_ge eq_diff_eq' le_cases less_eq_real_def segment_bound_lemma)
      have 1: "?h ` ({0..1} × ({x. iSuc n. x i = 0}  U))  U"
        by clarsimp (metis squashableD [OF squashable t U] convex_bound_le diff_ge_0_iff_ge eq_diff_eq' le_cases less_eq_real_def segment_bound_lemma)
      show "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (Euclidean_space (Suc n)) U))
                           (subtopology (Euclidean_space (Suc n)) U) ?h"
        apply (simp add: continuous_map_in_subtopology Euclidean_space_def subtopology_subtopology 1)
        apply (auto simp: case_prod_unfold ret_def continuous_map_componentwise_UNIV)
         apply (intro continuous_map_into_fulltopology [OF continuous_map_fst] cm_snd continuous_intros)
        by (auto simp: cm_snd)
    qed (auto simp: ret_def)
    have cs_hi: "contractible_space(subtopology (Euclidean_space(Suc n)) hi)"
    proof -
      have "homotopic_with (λx. True) (?ST 1) (?ST 1) id (λx. (λi. if i = n then 1 else 0))"
        apply (subst homotopic_with_sym)
        apply (simp add: homotopic_with)
        apply (rule_tac x="(λ(z,x) i. if i=n then 1 else z * x i)" in exI)
        apply (auto simp: Euclidean_space_def subtopology_subtopology continuous_map_in_subtopology case_prod_unfold continuous_map_componentwise_UNIV cm_fstsnd)
        done
      then have "contractible_space (?ST 1)"
        unfolding contractible_space_def by metis
      moreover have "?thesis = contractible_space (?ST 1)"
      proof (intro deformation_retract_imp_homotopy_equivalent_space homotopy_equivalent_space_contractibility)
        have "{x. iSuc n. x i = 0}  {x  hi. x n = 1} = {x. iSuc n. x i = 0}  {x. x n = 1}"
          by (auto simp: hi_def topspace_Euclidean_space)
        then have eq: "subtopology (Euclidean_space (Suc n)) {x. x  hi  x n = 1} = ?ST 1"
          by (simp add: Euclidean_space_def subtopology_subtopology)
        show "homotopic_with (λx. True) (subtopology (Euclidean_space (Suc n)) hi) (subtopology (Euclidean_space (Suc n)) hi) (ret 1) id"
          using hw_sub [OF squashable 1 hi squashable 1 UNIV] eq by simp
        show "retraction_maps (subtopology (Euclidean_space (Suc n)) hi) (?ST 1) (ret 1) id"
          using rm_ret [OF squashable 1 hi] eq by simp
      qed
      ultimately show ?thesis by metis
    qed
    have "?lhs  relative_homology_group p (Euclidean_space (Suc n)) (lo  hi)"
    proof (rule group.iso_sym [OF _ deformation_retract_imp_isomorphic_relative_homology_groups])
      have "{x. iSuc n. x i = 0}  {x. x n = 0} = {x. in. x i = (0::real)}"
        by auto (metis le_less_Suc_eq not_le)
      then have "?ST 0 = Euclidean_space n"
        by (simp add: Euclidean_space_def subtopology_subtopology)
      then show "retraction_maps (Euclidean_space (Suc n)) (Euclidean_space n) (ret 0) id"
        using rm_ret [OF squashable 0 UNIV] by auto
      then have "ret 0 x  topspace (Euclidean_space n)"
        if "x  topspace (Euclidean_space (Suc n))" "-1 < x n" "x n < 1" for x
        using that by (metis continuous_map_image_subset_topspace image_subset_iff retraction_maps_def)
      then show "(ret 0) ` (lo  hi)  topspace (Euclidean_space n) - S"
        by (auto simp: local.cong ret_def hi_def lo_def)
      show "homotopic_with (λh. h ` (lo  hi)  lo  hi) (Euclidean_space (Suc n)) (Euclidean_space (Suc n)) (ret 0) id"
        using hw_sub [OF squashable squashable_0_lohi] by simp
    qed (auto simp: lo_def hi_def Euclidean_space_def)
    also have "  relative_homology_group p (subtopology (Euclidean_space (Suc n)) hi) (lo  hi)"
    proof (rule group.iso_sym [OF _ isomorphic_relative_homology_groups_inclusion_contractible])
      show "contractible_space (subtopology (Euclidean_space (Suc n)) hi)"
        by (simp add: cs_hi)
      show "topspace (Euclidean_space (Suc n))  hi  {}"
        apply (simp add: hi_def topspace_Euclidean_space set_eq_iff)
        apply (rule_tac x="λi. if i = n then 1 else 0" in exI, auto)
        done
    qed auto
    also have "  relative_homology_group p (subtopology (Euclidean_space (Suc n)) (lo  hi)) lo"
    proof -
      have oo: "openin (Euclidean_space (Suc n)) {x  topspace (Euclidean_space (Suc n)). x n  A}"
        if "open A" for A
      proof (rule openin_continuous_map_preimage)
        show "continuous_map (Euclidean_space (Suc n)) euclideanreal (λx. x n)"
        proof -
          have "n f. continuous_map (product_topology f UNIV) (f (n::nat)) (λf. f n::real)"
            by (simp add: continuous_map_product_projection)
          then show ?thesis
            using Euclidean_space_def continuous_map_from_subtopology
            by (metis (mono_tags))
        qed
      qed (auto intro: that)
      have "openin (Euclidean_space(Suc n)) lo"
        apply (simp add: openin_subopen [of _ lo])
        apply (simp add: lo_def, safe)
         apply (force intro: oo [of "lessThan 0", simplified] open_Collect_less)
        apply (rule_tac x="{x  topspace(Euclidean_space(Suc n)). x n < 1}
                             (topspace(Euclidean_space(Suc n)) - S)" in exI)
        using clo apply (force intro: oo [of "lessThan 1", simplified] open_Collect_less)
        done
      moreover have "openin (Euclidean_space(Suc n)) hi"
        apply (simp add: openin_subopen [of _ hi])
        apply (simp add: hi_def, safe)
         apply (force intro: oo [of "greaterThan 0", simplified] open_Collect_less)
        apply (rule_tac x="{x  topspace(Euclidean_space(Suc n)). x n > -1}
                                 (topspace(Euclidean_space(Suc n)) - S)" in exI)
        using clo apply (force intro: oo [of "greaterThan (-1)", simplified] open_Collect_less)
        done
      ultimately
      have *: "subtopology (Euclidean_space (Suc n)) (lo  hi) closure_of
                   (topspace (subtopology (Euclidean_space (Suc n)) (lo  hi)) - hi)
                    subtopology (Euclidean_space (Suc n)) (lo  hi) interior_of lo"
        by (metis (no_types, lifting) Diff_idemp Diff_subset_conv Un_commute Un_upper2 closure_of_interior_of interior_of_closure_of interior_of_complement interior_of_eq lo_hi_Un openin_Un openin_open_subtopology topspace_subtopology_subset)
      have eq: "((lo  hi)  (lo  hi - (topspace (Euclidean_space (Suc n))  (lo  hi) - hi))) = hi"
        "(lo - (topspace (Euclidean_space (Suc n))  (lo  hi) - hi)) = lo  hi"
        by (auto simp: lo_def hi_def Euclidean_space_def)
      show ?thesis
        using homology_excision_axiom [OF *, of "lo  hi" p]
        by (force simp: subtopology_subtopology eq is_iso_def)
    qed
    also have "  relative_homology_group (p + 1 - 1) (subtopology (Euclidean_space (Suc n)) (lo  hi)) lo"
      by simp
    also have "  relative_homology_group (p + 1) (Euclidean_space (Suc n)) (lo  hi)"
    proof (rule group.iso_sym [OF _ isomorphic_relative_homology_groups_relboundary_contractible])
      have proj: "continuous_map (powertop_real UNIV) euclideanreal (λf. f n)"
        by (metis UNIV_I continuous_map_product_projection)
      have hilo: "x. x  hi  (λi. if i = n then - x i else x i)  lo"
                 "x. x  lo  (λi. if i = n then - x i else x i)  hi"
        using local.cong
        by (auto simp: hi_def lo_def topspace_Euclidean_space split: if_split_asm)
      have "subtopology (Euclidean_space (Suc n)) hi homeomorphic_space subtopology (Euclidean_space (Suc n)) lo"
        unfolding homeomorphic_space_def
        apply (rule_tac x="λx i. if i = n then -(x i) else x i" in exI)+
        using proj
        apply (auto simp: homeomorphic_maps_def Euclidean_space_def continuous_map_in_subtopology
                          hilo continuous_map_componentwise_UNIV continuous_map_from_subtopology continuous_map_minus
                    intro: continuous_map_from_subtopology continuous_map_product_projection)
        done
      then have "contractible_space(subtopology (Euclidean_space(Suc n)) hi)
              contractible_space (subtopology (Euclidean_space (Suc n)) lo)"
        by (rule homeomorphic_space_contractibility)
      then show "contractible_space (subtopology (Euclidean_space (Suc n)) lo)"
        using cs_hi by auto
      show "topspace (Euclidean_space (Suc n))  lo  {}"
        apply (simp add: lo_def Euclidean_space_def set_eq_iff)
        apply (rule_tac x="λi. if i = n then -1 else 0" in exI, auto)
        done
    qed auto
    also have "  ?rhs"
      by (simp flip: lo_hi_Un)
    finally show ?thesis .
  qed
  show ?thesis
  proof (induction k)
    case (Suc m)
    with assms obtain T where cloT: "closedin (powertop_real UNIV) T"
                         and SeqT: "S = T  {x. in. x i = 0}"
      by (auto simp: Euclidean_space_def closedin_subtopology)
    then have "closedin (Euclidean_space (m + n)) S"
      apply (simp add: Euclidean_space_def closedin_subtopology)
      apply (rule_tac x="T  topspace(Euclidean_space n)" in exI)
      using closedin_Euclidean_space topspace_Euclidean_space by force
    moreover have "relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - S)
                 relative_homology_group (p + 1) (Euclidean_space (Suc n)) (topspace (Euclidean_space (Suc n)) - S)"
      if "closedin (Euclidean_space n) S" for p n
    proof -
      define S' where "S'  {x  topspace(Euclidean_space(Suc n)). (λi. if i < n then x i else 0)  S}"
      have Ssub_n: "S  topspace (Euclidean_space n)"
        by (meson that closedin_def)
      have "relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - S')
            relative_homology_group (p + 1) (Euclidean_space (Suc n)) (topspace(Euclidean_space (Suc n)) - {x  S'. x n = 0})"
      proof (rule *)
        have cm: "continuous_map (powertop_real UNIV) euclideanreal (λf. f u)" for u
          by (metis UNIV_I continuous_map_product_projection)
        have "continuous_map (subtopology (powertop_real UNIV) {x. i>n. x i = 0}) euclideanreal
                (λx. if k  n then x k else 0)" for k
          by (simp add: continuous_map_from_subtopology [OF cm])
        moreover have "in. (if i < n then x i else 0) = 0"
          if "x  topspace (subtopology (powertop_real UNIV) {x. i>n. x i = 0})" for x
          using that by simp
        ultimately have "continuous_map (Euclidean_space (Suc n)) (Euclidean_space n) (λx i. if i < n then x i else 0)"
          by (simp add: Euclidean_space_def continuous_map_in_subtopology continuous_map_componentwise_UNIV
                        continuous_map_from_subtopology [OF cm] image_subset_iff)
        then show "closedin (Euclidean_space (Suc n)) S'"
          unfolding S'_def using that by (rule closedin_continuous_map_preimage)
      next
        fix x y
        assume xy: "i. i  n  x i = y i" "x  S'"
        then have "(λi. if i < n then x i else 0) = (λi. if i < n then y i else 0)"
          by (simp add: S'_def Euclidean_space_def fun_eq_iff)
        with xy show "y  S'"
          by (simp add: S'_def Euclidean_space_def)
      qed
      moreover
      have abs_eq: "(λi. if i < n then x i else 0) = x" if "i. i  n  x i = 0" for x :: "nat  real" and n
        using that by auto
      then have "topspace (Euclidean_space n) - S' = topspace (Euclidean_space n) - S"
        by (simp add: S'_def Euclidean_space_def set_eq_iff cong: conj_cong)
      moreover
      have "topspace (Euclidean_space (Suc n)) - {x  S'. x n = 0} = topspace (Euclidean_space (Suc n)) - S"
        using Ssub_n
        apply (auto simp: S'_def subset_iff Euclidean_space_def set_eq_iff abs_eq  cong: conj_cong)
        by (metis abs_eq le_antisym not_less_eq_eq)
      ultimately show ?thesis
        by simp
    qed
    ultimately have "relative_homology_group (p + m)(Euclidean_space (m + n))(topspace (Euclidean_space (m + n)) - S)
             relative_homology_group (p + m + 1) (Euclidean_space (Suc (m + n))) (topspace (Euclidean_space (Suc (m + n))) - S)"
      by (metis closedin (Euclidean_space (m + n)) S)
    then show ?case
      using Suc.IH iso_trans by (force simp: algebra_simps)
  qed (simp add: iso_refl)
qed

lemma iso_Euclidean_complements_lemma1:
  assumes S: "closedin (Euclidean_space m) S" and cmf: "continuous_map(subtopology (Euclidean_space m) S) (Euclidean_space n) f"
  obtains g where "continuous_map (Euclidean_space m) (Euclidean_space n) g"
                  "x. x  S  g x = f x"
proof -
  have cont: "continuous_on (topspace (Euclidean_space m)  S) (λx. f x i)" for i
    by (metis (no_types) continuous_on_product_then_coordinatewise
            cm_Euclidean_space_iff_continuous_on cmf topspace_subtopology)
  have "f ` (topspace (Euclidean_space m)  S)  topspace (Euclidean_space n)"
    using cmf continuous_map_image_subset_topspace by fastforce
  then
  have "g. continuous_on (topspace (Euclidean_space m)) g  (x  S. g x = f x i)" for i
    using S Tietze_unbounded [OF cont [of i]]
    by (metis closedin_Euclidean_space_iff closedin_closed_Int topspace_subtopology topspace_subtopology_subset)
  then obtain g where cmg: "i. continuous_map (Euclidean_space m) euclideanreal (g i)"
    and gf: "i x. x  S  g i x = f x i"
    unfolding continuous_map_Euclidean_space_iff by metis
  let ?GG = "λx i. if i < n then g i x else 0"
  show thesis
  proof
    show "continuous_map (Euclidean_space m) (Euclidean_space n) ?GG"
      unfolding Euclidean_space_def [of n]
      by (auto simp: continuous_map_in_subtopology continuous_map_componentwise cmg)
    show "?GG x = f x" if "x  S" for x
    proof -
      have "S  topspace (Euclidean_space m)"
        by (meson S closedin_def)
      then have "f x  topspace (Euclidean_space n)"
        using cmf that unfolding continuous_map_def topspace_subtopology by blast
      then show ?thesis
        by (force simp: topspace_Euclidean_space gf that)
    qed
  qed
qed


lemma iso_Euclidean_complements_lemma2:
  assumes S: "closedin (Euclidean_space m) S"
      and T: "closedin (Euclidean_space n) T"
      and hom: "homeomorphic_map (subtopology (Euclidean_space m) S) (subtopology (Euclidean_space n) T) f"
  obtains g where "homeomorphic_map (prod_topology (Euclidean_space m) (Euclidean_space n))
                                    (prod_topology (Euclidean_space n) (Euclidean_space m)) g"
                  "x. x  S  g(x,(λi. 0)) = (f x,(λi. 0))"
proof -
  obtain g where cmf: "continuous_map (subtopology (Euclidean_space m) S) (subtopology (Euclidean_space n) T) f"
           and cmg: "continuous_map (subtopology (Euclidean_space n) T) (subtopology (Euclidean_space m) S) g"
           and gf: "x. x  S  g (f x) = x"
           and fg: "y. y  T  f (g y) = y"
    using hom S T closedin_subset unfolding homeomorphic_map_maps homeomorphic_maps_def
    by fastforce
  obtain f' where cmf': "continuous_map (Euclidean_space m) (Euclidean_space n) f'"
             and f'f: "x. x  S  f' x = f x"
    using iso_Euclidean_complements_lemma1 S cmf continuous_map_into_fulltopology by metis
  obtain g' where cmg': "continuous_map (Euclidean_space n) (Euclidean_space m) g'"
             and g'g: "x. x  T  g' x = g x"
    using iso_Euclidean_complements_lemma1 T cmg continuous_map_into_fulltopology by metis
  define p  where "p  λ(x,y). (x,(λi. y i + f' x i))"
  define p' where "p'  λ(x,y). (x,(λi. y i - f' x i))"
  define q  where "q  λ(x,y). (x,(λi. y i + g' x i))"
  define q' where "q'  λ(x,y). (x,(λi. y i - g' x i))"
  have "homeomorphic_maps (prod_topology (Euclidean_space m) (Euclidean_space n))
                          (prod_topology (Euclidean_space m) (Euclidean_space n))
                          p p'"
       "homeomorphic_maps (prod_topology (Euclidean_space n) (Euclidean_space m))
                          (prod_topology (Euclidean_space n) (Euclidean_space m))
                          q q'"
       "homeomorphic_maps (prod_topology (Euclidean_space m) (Euclidean_space n))
                          (prod_topology (Euclidean_space n) (Euclidean_space m)) (λ(x,y). (y,x)) (λ(x,y). (y,x))"
    apply (simp_all add: p_def p'_def q_def q'_def homeomorphic_maps_def continuous_map_pairwise)
    apply (force simp: case_prod_unfold continuous_map_of_fst [unfolded o_def] cmf' cmg' intro: continuous_intros)+
    done
  then have "homeomorphic_maps (prod_topology (Euclidean_space m) (Euclidean_space n))
                          (prod_topology (Euclidean_space n) (Euclidean_space m))
                          (q'  (λ(x,y). (y,x))  p) (p'  ((λ(x,y). (y,x))  q))"
    using homeomorphic_maps_compose homeomorphic_maps_sym by (metis (no_types, lifting))
  moreover
  have "x. x  S  (q'  (λ(x,y). (y,x))  p) (x, λi. 0) = (f x, λi. 0)"
    apply (simp add: q'_def p_def f'f)
    apply (simp add: fun_eq_iff)
    by (metis S T closedin_subset g'g gf hom homeomorphic_imp_surjective_map image_eqI topspace_subtopology_subset)
  ultimately
  show thesis
    using homeomorphic_map_maps that by blast
qed


proposition isomorphic_relative_homology_groups_Euclidean_complements:
  assumes S: "closedin (Euclidean_space n) S" and T: "closedin (Euclidean_space n) T"
   and hom: "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)"
   shows "relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - S)
           relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - T)"
proof -
  have subST: "S  topspace(Euclidean_space n)" "T  topspace(Euclidean_space n)"
    by (meson S T closedin_def)+
  have "relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - S)
         relative_homology_group (p + int n) (Euclidean_space (n + n)) (topspace (Euclidean_space (n + n)) - S)"
    using relative_homology_group_Euclidean_complement_step [OF S] by blast
  moreover have "relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - T)
         relative_homology_group (p + int n) (Euclidean_space (n + n)) (topspace (Euclidean_space (n + n)) - T)"
    using relative_homology_group_Euclidean_complement_step [OF T] by blast
  moreover have "relative_homology_group (p + int n) (Euclidean_space (n + n)) (topspace (Euclidean_space (n + n)) - S)
                relative_homology_group (p + int n) (Euclidean_space (n + n)) (topspace (Euclidean_space (n + n)) - T)"
  proof -
    obtain f where f: "homeomorphic_map (subtopology (Euclidean_space n) S)
                                        (subtopology (Euclidean_space n) T) f"
      using hom unfolding homeomorphic_space by blast
    obtain g where g: "homeomorphic_map (prod_topology (Euclidean_space n) (Euclidean_space n))
                                        (prod_topology (Euclidean_space n) (Euclidean_space n)) g"
              and gf: "x. x  S  g(x,(λi. 0)) = (f x,(λi. 0))"
      using S T f iso_Euclidean_complements_lemma2 by blast
    define h where "h  λx::nat real. ((λi. if i < n then x i else 0), (λj. if j < n then x(n + j) else 0))"
    define k where "k  λ(x,y) i. if i < 2 * n then if i < n then x i else y(i - n) else (0::real)"
    have hk: "homeomorphic_maps (Euclidean_space(2 * n)) (prod_topology (Euclidean_space n) (Euclidean_space n)) h k"
      unfolding homeomorphic_maps_def
    proof safe
      show "continuous_map (Euclidean_space (2 * n))
                           (prod_topology (Euclidean_space n) (Euclidean_space n)) h"
        apply (simp add: h_def continuous_map_pairwise o_def continuous_map_componentwise_Euclidean_space)
        unfolding Euclidean_space_def
        by (metis (mono_tags) UNIV_I continuous_map_from_subtopology continuous_map_product_projection)
      have "continuous_map (prod_topology (Euclidean_space n) (Euclidean_space n)) euclideanreal (λp. fst p i)" for i
        using Euclidean_space_def continuous_map_into_fulltopology continuous_map_fst by fastforce
      moreover
      have "continuous_map (prod_topology (Euclidean_space n) (Euclidean_space n)) euclideanreal (λp. snd p (i - n))" for i
        using Euclidean_space_def continuous_map_into_fulltopology continuous_map_snd by fastforce
      ultimately
      show "continuous_map (prod_topology (Euclidean_space n) (Euclidean_space n))
                           (Euclidean_space (2 * n)) k"
        by (simp add: k_def continuous_map_pairwise o_def continuous_map_componentwise_Euclidean_space case_prod_unfold)
    qed (auto simp: k_def h_def fun_eq_iff topspace_Euclidean_space)
    define kgh where "kgh  k  g  h"
    let ?i = "hom_induced (p + n) (Euclidean_space(2 * n)) (topspace(Euclidean_space(2 * n)) - S)
                                 (Euclidean_space(2 * n)) (topspace(Euclidean_space(2 * n)) - T) kgh"
    have "?i  iso (relative_homology_group (p + int n) (Euclidean_space (2 * n))
                    (topspace (Euclidean_space (2 * n)) - S))
                   (relative_homology_group (p + int n) (Euclidean_space (2 * n))
                    (topspace (Euclidean_space (2 * n)) - T))"
    proof (rule homeomorphic_map_relative_homology_iso)
      show hm: "homeomorphic_map (Euclidean_space (2 * n)) (Euclidean_space (2 * n)) kgh"
        unfolding kgh_def by (meson hk g homeomorphic_map_maps homeomorphic_maps_compose homeomorphic_maps_sym)
      have Teq: "T = f ` S"
        using f homeomorphic_imp_surjective_map subST(1) subST(2) topspace_subtopology_subset by blast
      have khf: "x. x  S  k(h(f x)) = f x"
        by (metis (no_types, lifting) Teq hk homeomorphic_maps_def image_subset_iff le_add1 mult_2 subST(2) subsetD subset_Euclidean_space)
      have gh: "g(h x) = h(f x)" if "x  S" for x
      proof -
        have [simp]: "(λi. if i < n then x i else 0) = x"
          using subST(1) that topspace_Euclidean_space by (auto simp: fun_eq_iff)
        have "f x  topspace(Euclidean_space n)"
          using Teq subST(2) that by blast
        moreover have "(λj. if j < n then x (n + j) else 0) = (λj. 0::real)"
          using Euclidean_space_def subST(1) that by force
        ultimately show ?thesis
          by (simp add: topspace_Euclidean_space h_def gf x  S fun_eq_iff)
      qed
      have *: "S  U; T  U; kgh ` U = U; inj_on kgh U; kgh ` S = T  kgh ` (U - S) = U - T" for U
        unfolding inj_on_def set_eq_iff by blast
      show "kgh ` (topspace (Euclidean_space (2 * n)) - S) = topspace (Euclidean_space (2 * n)) - T"
      proof (rule *)
        show "kgh ` topspace (Euclidean_space (2 * n)) = topspace (Euclidean_space (2 * n))"
          by (simp add: hm homeomorphic_imp_surjective_map)
        show "inj_on kgh (topspace (Euclidean_space (2 * n)))"
          using hm homeomorphic_map_def by auto
        show "kgh ` S = T"
          by (simp add: Teq kgh_def gh khf)
      qed (use subST topspace_Euclidean_space in fastforce+)
    qed auto
    then show ?thesis
      by (simp add: is_isoI mult_2)
  qed
  ultimately show ?thesis
    by (meson group.iso_sym iso_trans group_relative_homology_group)
qed

lemma lemma_iod:
  assumes "S  T" "S  {}" and Tsub: "T  topspace(Euclidean_space n)"
      and S: "a b u. a  S; b  T; 0 < u; u < 1  (λi. (1 - u) * a i + u * b i)  S"
    shows "path_connectedin (Euclidean_space n) T"
proof -
  obtain a where "a  S"
    using assms by blast
  have "path_component_of (subtopology (Euclidean_space n) T) a b" if "b  T" for b
    unfolding path_component_of_def
  proof (intro exI conjI)
    have [simp]: "in. a i = 0"
      using Tsub a  S assms(1) topspace_Euclidean_space by auto
    have [simp]: "in. b i = 0"
      using Tsub that topspace_Euclidean_space by auto
    have inT: "(λi. (1 - x) * a i + x * b i)  T" if "0  x" "x  1" for x
    proof (cases "x = 0  x = 1")
      case True
      with a  S b  T S  T show ?thesis
        by force
    next
      case False
      then show ?thesis
        using subsetD [OF S  T S] a  S b  T that by auto
    qed
    have "continuous_on {0..1} (λx. (1 - x) * a k + x * b k)" for k
      by (intro continuous_intros)
    then show "pathin (subtopology (Euclidean_space n) T) (λt i. (1 - t) * a i + t * b i)"
      apply (simp add: Euclidean_space_def subtopology_subtopology pathin_subtopology)
      apply (simp add: pathin_def continuous_map_componentwise_UNIV inT)
      done
  qed auto
  then have "path_connected_space (subtopology (Euclidean_space n) T)"
    by (metis Tsub path_component_of_equiv path_connected_space_iff_path_component topspace_subtopology_subset)
  then show ?thesis
    by (simp add: Tsub path_connectedin_def)
qed


lemma invariance_of_dimension_closedin_Euclidean_space:
  assumes "closedin (Euclidean_space n) S"
  shows "subtopology (Euclidean_space n) S homeomorphic_space Euclidean_space n
          S = topspace(Euclidean_space n)"
         (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  have Ssub: "S  topspace (Euclidean_space n)"
    by (meson assms closedin_def)
  moreover have False if "a  S" and "a  topspace (Euclidean_space n)" for a
  proof -
    have cl_n: "closedin (Euclidean_space (Suc n)) (topspace(Euclidean_space n))"
      using Euclidean_space_def closedin_Euclidean_space closedin_subtopology by fastforce
    then have sub: "subtopology (Euclidean_space(Suc n)) (topspace(Euclidean_space n)) = Euclidean_space n"
      by (metis (no_types, lifting) Euclidean_space_def closedin_subset subtopology_subtopology topspace_Euclidean_space topspace_subtopology topspace_subtopology_subset)
    then have cl_S: "closedin (Euclidean_space(Suc n)) S"
      using cl_n assms closedin_closed_subtopology by fastforce
    have sub_SucS: "subtopology (Euclidean_space (Suc n)) S = subtopology (Euclidean_space n) S"
      by (metis Ssub sub subtopology_subtopology topspace_subtopology topspace_subtopology_subset)
    have non0: "{y. x::natreal. (iSuc n. x i = 0)  (in. x i  0)  y = x n} = -{0}"
    proof safe
      show "False" if "iSuc n. f i = 0" "0 = f n" "n  i" "f i  0" for f::"natreal" and i
        by (metis that le_antisym not_less_eq_eq)
      show "f::natreal. (iSuc n. f i = 0)  (in. f i  0)  a = f n" if "a  0" for a
        by (rule_tac x="(λi. 0)(n:= a)" in exI) (force simp: that)
    qed
    have "homology_group 0 (subtopology (Euclidean_space (Suc n)) (topspace (Euclidean_space (Suc n)) - S))
           homology_group 0 (subtopology (Euclidean_space (Suc n)) (topspace (Euclidean_space (Suc n)) - topspace (Euclidean_space n)))"
    proof (rule isomorphic_relative_contractible_space_imp_homology_groups)
      show "(topspace (Euclidean_space (Suc n)) - S = {}) =
            (topspace (Euclidean_space (Suc n)) - topspace (Euclidean_space n) = {})"
        using cl_n closedin_subset that by auto
    next
      fix p
      show "relative_homology_group p (Euclidean_space (Suc n))
         (topspace (Euclidean_space (Suc n)) - S) 
        relat