Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: 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: "\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::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)
  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 cmr continuous_map_def by fastforce
  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))"
      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
        \<in> 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))
             \<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 \ {}"
      by (metis equ(1) nonempty_nsphere topspace_subtopology)
    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)
    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"
      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 \<circ> 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 [^]\<^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, hide_lams) 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)
      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 \<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 1: "?h ` ({0..1} \ ({x. \i\Suc n. x i = 0} \ U)) \ U"
        by clarsimp (metis squashableD [OF \<open>squashable t U\<close>] 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. \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 (simp add: continuous_map_def 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
  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
         \<longleftrightarrow> S = topspace(Euclidean_space n)"
         (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  have Ssub: "S \ topspace (Euclidean_space n)"
    by (meson assms closedin_def)
--> --------------------

--> maximum size reached

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

[ zur Elbe Produktseite wechseln0.55Quellennavigators  Analyse erneut starten  ]

                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....

Besucherstatistik

Besucherstatistik