# Theory Invariance_of_Domain

```section‹Invariance of Domain›

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

begin

subsection‹Degree invariance mod 2 for map between pairs›

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

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

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

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

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

proposition isomorphic_relative_homology_groups_Euclidean_complements:
assumes S: "closedin (Euclidean_space n) S" and T: "closedin (Euclidean_space n) T"
and hom: "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)"
shows "relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - S)
≅ relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - T)"
proof -
have subST: "S ⊆ topspace(Euclidean_space n)" "T ⊆ topspace(Euclidean_space n)"
by (meson S T closedin_def)+
have "relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - S)
≅ relative_homology_group (p + int n) (Euclidean_space (n + n)) (topspace (Euclidean_space (n + n)) - S)"
using relative_homology_group_Euclidean_complement_step [OF S] by blast
moreover have "relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - T)
≅ relative_homology_group (p + int n) (Euclidean_space (n + n)) (topspace (Euclidean_space (n + n)) - T)"
using relative_homology_group_Euclidean_complement_step [OF T] by blast
moreover have "relative_homology_group (p + int n) (Euclidean_space (n + n)) (topspace (Euclidean_space (n + n)) - S)
≅ relative_homology_group (p + int n) (Euclidean_space (n + n)) (topspace (Euclidean_space (n + n)) - T)"
proof -
obtain f where f: "homeomorphic_map (subtopology (Euclidean_space n) S)
(subtopology (Euclidean_space n) T) f"
using hom unfolding homeomorphic_space by blast
obtain g where g: "homeomorphic_map (prod_topology (Euclidean_space n) (Euclidean_space n))
(prod_topology (Euclidean_space n) (Euclidean_space n)) g"
and gf: "⋀x. x ∈ S ⟹ g(x,(λi. 0)) = (f x,(λi. 0))"
using S T f iso_Euclidean_complements_lemma2 by blast
define h where "h ≡ λx::nat ⇒real. ((λi. if i < n then x i else 0), (λj. if j < n then x(n + j) else 0))"
define k where "k ≡ λ(x,y) i. if i < 2 * n then if i < n then x i else y(i - n) else (0::real)"
have hk: "homeomorphic_maps (Euclidean_space(2 * n)) (prod_topology (Euclidean_space n) (Euclidean_space n)) h k"
unfolding homeomorphic_maps_def
proof safe
show "continuous_map (Euclidean_space (2 * n))
(prod_topology (Euclidean_space n) (Euclidean_space n)) h"
apply (simp add: h_def continuous_map_pairwise o_def continuous_map_componentwise_Euclidean_space)
unfolding Euclidean_space_def
by (metis (mono_tags) UNIV_I continuous_map_from_subtopology continuous_map_product_projection)
have "continuous_map (prod_topology (Euclidean_space n) (Euclidean_space n)) euclideanreal (λp. fst p i)" for i
using Euclidean_space_def continuous_map_into_fulltopology continuous_map_fst by fastforce
moreover
have "continuous_map (prod_topology (Euclidean_space n) (Euclidean_space n)) euclideanreal (λp. snd p (i - n))" for i
using Euclidean_space_def continuous_map_into_fulltopology continuous_map_snd by fastforce
ultimately
show "continuous_map (prod_topology (Euclidean_space n) (Euclidean_space n))
(Euclidean_space (2 * n)) k"
by (simp add: k_def continuous_map_pairwise o_def continuous_map_componentwise_Euclidean_space case_prod_unfold)
qed (auto simp: k_def h_def fun_eq_iff topspace_Euclidean_space)
define kgh where "kgh ≡ k ∘ g ∘ h"
let ?i = "hom_induced (p + n) (Euclidean_space(2 * n)) (topspace(Euclidean_space(2 * n)) - S)
(Euclidean_space(2 * n)) (topspace(Euclidean_space(2 * n)) - T) kgh"
have "?i ∈ iso (relative_homology_group (p + int n) (Euclidean_space (2 * n))
(topspace (Euclidean_space (2 * n)) - S))
(relative_homology_group (p + int n) (Euclidean_space (2 * n))
(topspace (Euclidean_space (2 * n)) - T))"
proof (rule homeomorphic_map_relative_homology_iso)
show hm: "homeomorphic_map (Euclidean_space (2 * n)) (Euclidean_space (2 * n)) kgh"
unfolding kgh_def by (meson hk g homeomorphic_map_maps homeomorphic_maps_compose homeomorphic_maps_sym)
have Teq: "T = f ` S"
using f homeomorphic_imp_surjective_map subST(1) subST(2) topspace_subtopology_subset by blast
have khf: "⋀x. x ∈ S ⟹ k(h(f x)) = f x"
by (metis (no_types, lifting) Teq hk homeomorphic_maps_def image_subset_iff le_add1 mult_2 subST(2) subsetD subset_Euclidean_space)
have gh: "g(h x) = h(f x)" if "x ∈ S" for x
proof -
have [simp]: "(λi. if i < n then x i else 0) = x"
using subST(1) that topspace_Euclidean_space by (auto simp: fun_eq_iff)
have "f x ∈ topspace(Euclidean_space n)"
using Teq subST(2) that by blast
moreover have "(λj. if j < n then x (n + j) else 0) = (λj. 0::real)"
using Euclidean_space_def subST(1) that by force
ultimately show ?thesis
by (simp add: topspace_Euclidean_space h_def gf ‹x ∈ S› fun_eq_iff)
qed
have *: "⟦S ⊆ U; T ⊆ U; kgh ` U = U; inj_on kgh U; kgh ` S = T⟧ ⟹ kgh ` (U - S) = U - T" for U
unfolding inj_on_def set_eq_iff by blast
show "kgh ` (topspace (Euclidean_space (2 * n)) - S) = topspace (Euclidean_space (2 * n)) - T"
proof (rule *)
show "kgh ` topspace (Euclidean_space (2 * n)) = topspace (Euclidean_space (2 * n))"
show "inj_on kgh (topspace (Euclidean_space (2 * n)))"
using hm homeomorphic_map_def by auto
show "kgh ` S = T"
by (simp add: Teq kgh_def gh khf)
qed (use subST topspace_Euclidean_space in ‹fastforce+›)
qed auto
then show ?thesis
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 ‹a ∈ S› 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 ‹a ∈ S› ‹b ∈ T› ‹S ⊆ T› show ?thesis
by force
next
case False
then show ?thesis
using subsetD [OF ‹S ⊆ T› S] ‹a ∈ S› ‹b ∈ T› that by auto
qed
have "continuous_on {0..1} (λx. (1 - x) * a k + x * b k)" for k
by (intro continuous_intros)
then show "pathin (subtopology (Euclidean_space n) T) (λt i. (1 - t) * a i + t * b i)"
apply (simp add: Euclidean_space_def subtopology_subtopology pathin_subtopology)
apply (simp add: pathin_def continuous_map_componentwise_UNIV inT)
done
qed auto
then have "path_connected_space (subtopology (Euclidean_space n) T)"
by (metis Tsub path_component_of_equiv path_connected_space_iff_path_component topspace_subtopology_subset)
then show ?thesis
qed

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