Quelle Invariance_of_Domain.thy Sprache: Isabelle

section\<open>Invariance of Domain\<close>

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

begin

subsection\<open>Degree invariance mod 2 for map between pairs\<close>

theorem Borsuk_odd_mapping_degree_step:
  assumes cmf: "continuous_map (nsphere n) (nsphere n) f"
    and f: "\u. u \ topspace(nsphere n) \ (f \ (\x i. -x i)) u = ((\x i. -x i) \ f) u"
    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::nat\real. \i. -x i"
  define upper where "upper \ \n. {x::nat\real. x n \ 0}"
  define lower where "lower \ \n. {x::nat\real. x n \ 0}"
  define equator where "equator \ \n. {x::nat\real. 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)
  then have [simp]: "id \ equator n \ upper n"
    by force
  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 cmf continuous_map_from_subtopology continuous_map_in_subtopology equ(1)
        fim subtopology_restrict 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}
      \<in> Group.iso (relative_homology_group n
                     (subtopology (nsphere n) {x. x n \<le> 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 \<le> 0}) {x. x n = 0})
                          (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))
                          (hom_boundary n (subtopology (nsphere n) {x. x n \<le> 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 \<le> 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}
            \<in> iso (relative_homology_group n (subtopology (nsphere n) {x. x n \<ge> 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 \<ge> 0}) {x. x n = 0})
                          (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))
                          (hom_boundary n (subtopology (nsphere n) {x. x n \<ge> 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 \<ge> 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
      \<in> iso (reduced_homology_group n (nsphere n))
            (?rhgn {x. x n \<ge> 0})"
    using iso_reduced_homology_group_upper_hemisphere [of n n n] by auto
  then have "carrier(?rhgn {x. x n \ 0})
          \<subseteq> (hom_induced n (nsphere n) {} (nsphere n) {x. x n \<ge> 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
      \<in> iso (reduced_homology_group n (nsphere n))
            (?rhgn {x. x n \<le> 0})"
    using iso_reduced_homology_group_lower_hemisphere [of n n n] by auto
  then have "carrier(?rhgn {x. x n \ 0})
          \<subseteq> (hom_induced n (nsphere n) {} (nsphere n) {x. x n \<le> 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
          \<otimes>\<^bsub>?rhgn (equator n)\<^esub>
            hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id y)
        \<in> Group.iso
            (relative_homology_group n (lsphere n) (equator n) \<times>\<times>
             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
        \<in> Group.iso (relative_homology_group n (lsphere n) (equator n))
            (?rhgn (upper n))"
      unfolding 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
        \<in> Group.iso (relative_homology_group n (usphere n) (equator n))
            (?rhgn (lower n))"
      unfolding 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))
             \<subseteq> (\<lambda>(x, y).
            hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id x
          \<otimes>\<^bsub>?rhgn (equator n)\<^esub>
            hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id y)
               ` carrier (relative_homology_group n (lsphere n) (equator n) \<times>\<times>
             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 [^]\<^bsub>?rhgn (equator n)\<^esub> a\<otimes>\<^bsub>?rhgn (equator n)\<^esub> un [^]\<^bsub>?rhgn (equator n)\<^esub> 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
                \<otimes>\<^bsub>?rhgn (equator n)\<^esub>
                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 [^]\<^bsub>relative_homology_group n (lsphere n) (equator n)\<^esub> 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 [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub> 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 [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub> b)
        = hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id
           zn [^]\<^bsub>relative_homology_group n (nsphere n) (equator n)\<^esub> 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 [^]\<^bsub>?rhgn (equator n)\<^esub> a \<otimes>\<^bsub>?rhgn (equator n)\<^esub> un [^]\<^bsub>?rhgn (equator n)\<^esub> b"
        using a ae b be eq local.up_def un_def by auto
    qed
  qed
  have "(hom_boundary n (nsphere n) (equator n)
       \<circ> 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)
       \<circ> 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
           \<circ> hom_boundary n (nsphere n) (equator n)) up
        = (hom_boundary n (nsphere n) (equator n) \<circ>
           ?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 [^]\<^bsub>relative_homology_group n (nsphere n) (equator n)\<^esub>
                        a \<otimes>\<^bsub>relative_homology_group n (nsphere n) (equator n)\<^esub>
                        un [^]\<^bsub>relative_homology_group n (nsphere n) (equator n)\<^esub> b)"
      by (simp add: o_def up_ab)
    also have "\ = z [^]\<^bsub>reduced_homology_group (int n - 1) (nsphere (n - Suc 0))\<^esub> (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 [^]\<^bsub>reduced_homology_group (int n - 1) (nsphere (n - Suc 0))\<^esub> (a + b)"
      by (simp add: up_z)
  qed
  define u where "u \ up \\<^bsub>?rhgn (equator n)\<^esub> inv\<^bsub>?rhgn (equator n)\<^esub> un"
  have ucarr: "u \ carrier (?rhgn (equator n))"
    by (simp add: u_def uncarr upcarr)
  then have "u [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 n f = u [^]\<^bsub>?rhgn (equator n)\<^esub> (a - b)
             \<longleftrightarrow> (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 [^]\<^bsub>?rhgn (equator n)\<^esub> d = singular_relboundary_set n (nsphere n) (equator n)"
    then have "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id u [^]\<^bsub>?rhgn (upper n)\<^esub> d
               = \<one>\<^bsub>?rhgn (upper n)\<^esub>"
      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 \<circ>
          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 = \\<^bsub>?rhgn (upper n)\<^esub>"
      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 [^]\<^bsub>?rhgn (upper n)\<^esub> d) = \\<^bsub>?rhgn (upper n)\<^esub>"
      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 \<open>0 < d\<close> wpcarr by blast
  qed
  ultimately have iff: "u [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 n f = u [^]\<^bsub>?rhgn (equator n)\<^esub> (a - b)
                   \<longleftrightarrow> Brouwer_degree2 n f = a - b"
    by auto
  have "u [^]\<^bsub>?rhgn (equator n)\<^esub> 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
               = \<one>\<^bsub>reduced_homology_group (int n - 1) (subtopology (nsphere n) (equator n))\<^esub>"
      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 [^]\<^bsub>?rhgn (equator n)\<^esub> 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) \<inter> equator n) id v)"
      using fimeq by (simp add: hom_induced_compose' cmf Pi_iff)
    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 [^]\<^bsub>?rhgn (equator n)\<^esub> 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 \<circ> 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 [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub> 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 [^]\<^bsub>homology_group (int n - 1) (nsphere (n - Suc 0))\<^esub> 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 \<circ>
              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 [^]\<^bsub>homology_group (int n - 1) (nsphere (n - Suc 0))\<^esub> Brouwer_degree2 (n - Suc 0) neg)"
          by (metis "*" comp_apply zp_z)
        also have "\ = ?hb (zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub>
          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 [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub>
          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 [^]\<^bsub>?rhgn (equator n)\<^esub> 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 [^]\<^bsub>?rhgn (equator n)\<^esub> a \\<^bsub>?rhgn (equator n)\<^esub> up [^]\<^bsub>?rhgn (equator n)\<^esub> 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"
      using cm_neg continuous_map_image_subset_topspace equator_def
      by fastforce
    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 \<circ> hom_induced n (nsphere n) ?TE (nsphere n) ?TE f"
      using neg_im fimeq cm_neg cmf fneg
      apply (simp flip: hom_induced_compose del: hom_induced_restrict)
      using fneg by (auto intro: hom_induced_eq)
    have "(un [^]\<^bsub>?rhgn (equator n)\<^esub> a) \\<^bsub>?rhgn (equator n)\<^esub> (up [^]\<^bsub>?rhgn (equator n)\<^esub> b)
        = un [^]\<^bsub>?rhgn (equator n)\<^esub> (Brouwer_degree2 (n - 1) neg * a * Brouwer_degree2 (n - 1) neg)
          \<otimes>\<^bsub>?rhgn (equator n)\<^esub>
          up [^]\<^bsub>?rhgn (equator n)\<^esub> (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 [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - 1) neg) [^]\<^bsub>?rhgn (equator n)\<^esub> a \\<^bsub>?rhgn (equator n)\<^esub>
           (up [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - 1) neg) [^]\<^bsub>?rhgn (equator n)\<^esub> b) [^]\<^bsub>?rhgn (equator n)\<^esub>
          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) [^]\<^bsub>?rhgn (equator n)\<^esub> 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 [^]\<^bsub>?rhgn (equator n)\<^esub> a) \\<^bsub>?rhgn (equator n)\<^esub> (up [^]\<^bsub>?rhgn (equator n)\<^esub> b)
             = ?hi_ee neg (?hi_ee f up) [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg" .
    have "un = ?hi_ee neg up [^]\<^bsub>?rhgn (equator n)\<^esub> 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) [^]\<^bsub>?rhgn (equator n)\<^esub> (Brouwer_degree2 (n - Suc 0) neg))
                 = un [^]\<^bsub>?rhgn (equator n)\<^esub> a \<otimes>\<^bsub>?rhgn (equator n)\<^esub> up [^]\<^bsub>?rhgn (equator n)\<^esub> 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 [^]\<^bsub>?rhgn (equator n)\<^esub> (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 \<open>General Jordan-Brouwer separation theorem and invariance of dimension\<close>

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)
      \<cong> 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)
           \<cong> relative_homology_group (p + 1) (Euclidean_space (Suc n)) (topspace(Euclidean_space (Suc n)) - {x \<in> 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 \<in> U \<and> 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 \<in> 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 (\<lambda>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 (\<lambda>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)
      define h where "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 unfolding h_def
        by clarsimp (metis squashableD [OF \<open>squashable t V\<close>] convex_bound_le diff_ge_0_iff_ge eq_diff_eq' le_cases less_eq_real_def segment_bound_lemma)
      have "\x y i. \\k\Suc n. y k = 0; Suc n \ i\ \ ret ((1 - x) * t + x * y n) y i = 0"
        by (simp add: ret_def)
      then have "h \ {0..1} \ ({x. \i\Suc n. x i = 0} \ U) \ {x. \i\Suc n. x i = 0} \ U"
        using  squashableD [OF \<open>squashable t U\<close>]  segment_bound_lemma
        apply (clarsimp simp: h_def Pi_iff)
        by (metis convex_bound_le eq_diff_eq ge_iff_diff_ge_0 linorder_le_cases)
      moreover
      have "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (powertop_real UNIV)
                           ({x. \<forall>i\<ge>Suc n. x i = 0} \<inter> U))) (powertop_real UNIV) h"
        apply (auto simp: h_def 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)
      ultimately show "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (Euclidean_space (Suc n)) U))
                           (subtopology (Euclidean_space (Suc n)) U) h"
        by (simp add: continuous_map_in_subtopology Euclidean_space_def subtopology_subtopology)
    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. \i\Suc n. x i = 0} \ {x \ hi. x n = 1} = {x. \i\Suc 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 \<open>squashable 1 hi\<close> \<open>squashable 1 UNIV\<close>] eq by simp
        show "retraction_maps (subtopology (Euclidean_space (Suc n)) hi) (?ST 1) (ret 1) id"
          using rm_ret [OF \<open>squashable 1 hi\<close>] 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. \i\Suc n. x i = 0} \ {x. x n = 0} = {x. \i\n. 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 \<open>squashable 0 UNIV\<close>] 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}
                            \<inter> (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}
                                \<inter> (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 \<union> hi)) - hi)
                   \<subseteq> subtopology (Euclidean_space (Suc n)) (lo \<union> 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)
             \<longleftrightarrow> 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. \i\n. 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)
                \<cong> 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' \<equiv> {x \<in> topspace(Euclidean_space(Suc n)). (\<lambda>i. if i < n then x i else 0) \<in> 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')
           \<cong> relative_homology_group (p + 1) (Euclidean_space (Suc n)) (topspace(Euclidean_space (Suc n)) - {x \<in> 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
                (\<lambda>x. if k \<le> n then x k else 0)" for k
          by (simp add: continuous_map_from_subtopology [OF cm])
        moreover have "\i\n. (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)
            \<cong> relative_homology_group (p + m + 1) (Euclidean_space (Suc (m + n))) (topspace (Euclidean_space (Suc (m + n))) - S)"
      by (metis \<open>closedin (Euclidean_space (m + n)) S\<close>)
    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' \<equiv> \<lambda>(x,y). (x,(\<lambda>i. y i - f' x i))"
  define q  where "q \ \(x,y). (x,(\i. y i + g' x i))"
  define q' where "q' \<equiv> \<lambda>(x,y). (x,(\<lambda>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)) (\<lambda>(x,y). (y,x)) (\<lambda>(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)
          \<cong> 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)
        \<cong> 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)
        \<cong> 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)
               \<cong> 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 \<open>x \<in> S\<close> 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 \<open>fastforce+\<close>)
    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]: "\i\n. a i = 0"
      using Tsub \<open>a \<in> S\<close> assms(1) topspace_Euclidean_space by auto
    have [simp]: "\i\n. 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 \<open>a \<in> S\<close> \<open>b \<in> T\<close> \<open>S \<subseteq> T\<close> show ?thesis
        by force
    next
      case False
      then show ?thesis
        using subsetD [OF \<open>S \<subseteq> T\<close> S] \<open>a \<in> S\<close> \<open>b \<in> T\<close> 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
--> --------------------

--> maximum size reached

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

quality96%

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.