Theory HOL-Analysis.Homeomorphism
section ‹Homeomorphism Theorems›
theory Homeomorphism
imports Homotopy
begin
lemma homeomorphic_spheres':
fixes a ::"'a::euclidean_space" and b ::"'b::euclidean_space"
assumes "0 < δ" and dimeq: "DIM('a) = DIM('b)"
shows "(sphere a δ) homeomorphic (sphere b δ)"
proof -
obtain f :: "'a⇒'b" and g where "linear f" "linear g"
and fg: "⋀x. norm(f x) = norm x" "⋀y. norm(g y) = norm y" "⋀x. g(f x) = x" "⋀y. f(g y) = y"
by (blast intro: isomorphisms_UNIV_UNIV [OF dimeq])
then have "continuous_on UNIV f" "continuous_on UNIV g"
using linear_continuous_on linear_linear by blast+
then show ?thesis
unfolding homeomorphic_minimal
apply(rule_tac x="λx. b + f(x - a)" in exI)
apply(rule_tac x="λx. a + g(x - b)" in exI)
using assms
apply (force intro: continuous_intros
continuous_on_compose2 [of _ f] continuous_on_compose2 [of _ g] simp: dist_commute dist_norm fg)
done
qed
lemma homeomorphic_spheres_gen:
fixes a :: "'a::euclidean_space" and b :: "'b::euclidean_space"
assumes "0 < r" "0 < s" "DIM('a::euclidean_space) = DIM('b::euclidean_space)"
shows "(sphere a r homeomorphic sphere b s)"
using assms homeomorphic_trans [OF homeomorphic_spheres homeomorphic_spheres'] by auto
subsection ‹Homeomorphism of all convex compact sets with nonempty interior›
proposition
fixes S :: "'a::euclidean_space set"
assumes "compact S" and 0: "0 ∈ rel_interior S"
and star: "⋀x. x ∈ S ⟹ open_segment 0 x ⊆ rel_interior S"
shows starlike_compact_projective1_0:
"S - rel_interior S homeomorphic sphere 0 1 ∩ affine hull S"
(is "?SMINUS homeomorphic ?SPHER")
and starlike_compact_projective2_0:
"S homeomorphic cball 0 1 ∩ affine hull S"
(is "S homeomorphic ?CBALL")
proof -
have starI: "(u *⇩R x) ∈ rel_interior S" if "x ∈ S" "0 ≤ u" "u < 1" for x u
proof (cases "x=0 ∨ u=0")
case True with 0 show ?thesis by force
next
case False with that show ?thesis
by (auto simp: in_segment intro: star [THEN subsetD])
qed
have "0 ∈ S" using assms rel_interior_subset by auto
define proj where "proj ≡ λx::'a. x /⇩R norm x"
have eqI: "x = y" if "proj x = proj y" "norm x = norm y" for x y
using that by (force simp: proj_def)
then have iff_eq: "⋀x y. (proj x = proj y ∧ norm x = norm y) ⟷ x = y"
by blast
have projI: "x ∈ affine hull S ⟹ proj x ∈ affine hull S" for x
by (metis ‹0 ∈ S› affine_hull_span_0 hull_inc span_mul proj_def)
have nproj1 [simp]: "x ≠ 0 ⟹ norm(proj x) = 1" for x
by (simp add: proj_def)
have proj0_iff [simp]: "proj x = 0 ⟷ x = 0" for x
by (simp add: proj_def)
have cont_proj: "continuous_on (UNIV - {0}) proj"
unfolding proj_def by (rule continuous_intros | force)+
have proj_spherI: "⋀x. ⟦x ∈ affine hull S; x ≠ 0⟧ ⟹ proj x ∈ ?SPHER"
by (simp add: projI)
have "bounded S" "closed S"
using ‹compact S› compact_eq_bounded_closed by blast+
have inj_on_proj: "inj_on proj (S - rel_interior S)"
proof
fix x y
assume x: "x ∈ S - rel_interior S"
and y: "y ∈ S - rel_interior S" and eq: "proj x = proj y"
then have xynot: "x ≠ 0" "y ≠ 0" "x ∈ S" "y ∈ S" "x ∉ rel_interior S" "y ∉ rel_interior S"
using 0 by auto
consider "norm x = norm y" | "norm x < norm y" | "norm x > norm y" by linarith
then show "x = y"
proof cases
assume "norm x = norm y"
with iff_eq eq show "x = y" by blast
next
assume *: "norm x < norm y"
have "x /⇩R norm x = norm x *⇩R (x /⇩R norm x) /⇩R norm (norm x *⇩R (x /⇩R norm x))"
by force
then have "proj ((norm x / norm y) *⇩R y) = proj x"
by (metis (no_types) divide_inverse local.proj_def eq scaleR_scaleR)
then have [simp]: "(norm x / norm y) *⇩R y = x"
by (rule eqI) (simp add: ‹y ≠ 0›)
have no: "0 ≤ norm x / norm y" "norm x / norm y < 1"
using * by (auto simp: field_split_simps)
then show "x = y"
using starI [OF ‹y ∈ S› no] xynot by auto
next
assume *: "norm x > norm y"
have "y /⇩R norm y = norm y *⇩R (y /⇩R norm y) /⇩R norm (norm y *⇩R (y /⇩R norm y))"
by force
then have "proj ((norm y / norm x) *⇩R x) = proj y"
by (metis (no_types) divide_inverse local.proj_def eq scaleR_scaleR)
then have [simp]: "(norm y / norm x) *⇩R x = y"
by (rule eqI) (simp add: ‹x ≠ 0›)
have no: "0 ≤ norm y / norm x" "norm y / norm x < 1"
using * by (auto simp: field_split_simps)
then show "x = y"
using starI [OF ‹x ∈ S› no] xynot by auto
qed
qed
have "∃surf. homeomorphism (S - rel_interior S) ?SPHER proj surf"
proof (rule homeomorphism_compact)
show "compact (S - rel_interior S)"
using ‹compact S› compact_rel_boundary by blast
show "continuous_on (S - rel_interior S) proj"
using 0 by (blast intro: continuous_on_subset [OF cont_proj])
show "proj ` (S - rel_interior S) = ?SPHER"
proof
show "proj ` (S - rel_interior S) ⊆ ?SPHER"
using 0 by (force simp: hull_inc projI intro: nproj1)
show "?SPHER ⊆ proj ` (S - rel_interior S)"
proof (clarsimp simp: proj_def)
fix x
assume "x ∈ affine hull S" and nox: "norm x = 1"
then have "x ≠ 0" by auto
obtain d where "0 < d" and dx: "(d *⇩R x) ∈ rel_frontier S"
and ri: "⋀e. ⟦0 ≤ e; e < d⟧ ⟹ (e *⇩R x) ∈ rel_interior S"
using ray_to_rel_frontier [OF ‹bounded S› 0] ‹x ∈ affine hull S› ‹x ≠ 0› by auto
show "x ∈ (λx. x /⇩R norm x) ` (S - rel_interior S)"
proof
show "x = d *⇩R x /⇩R norm (d *⇩R x)"
using ‹0 < d› by (auto simp: nox)
show "d *⇩R x ∈ S - rel_interior S"
using dx ‹closed S› by (auto simp: rel_frontier_def)
qed
qed
qed
qed (rule inj_on_proj)
then obtain surf where surf: "homeomorphism (S - rel_interior S) ?SPHER proj surf"
by blast
then have cont_surf: "continuous_on (proj ` (S - rel_interior S)) surf"
by (auto simp: homeomorphism_def)
have surf_nz: "⋀x. x ∈ ?SPHER ⟹ surf x ≠ 0"
by (metis "0" DiffE homeomorphism_def imageI surf)
have cont_nosp: "continuous_on (?SPHER) (λx. norm x *⇩R ((surf o proj) x))"
proof (intro continuous_intros)
show "continuous_on (sphere 0 1 ∩ affine hull S) proj"
by (rule continuous_on_subset [OF cont_proj], force)
show "continuous_on (proj ` (sphere 0 1 ∩ affine hull S)) surf"
by (intro continuous_on_subset [OF cont_surf]) (force simp: homeomorphism_image1 [OF surf] dest: proj_spherI)
qed
have surfpS: "⋀x. ⟦norm x = 1; x ∈ affine hull S⟧ ⟹ surf (proj x) ∈ S"
by (metis (full_types) DiffE ‹0 ∈ S› homeomorphism_def image_eqI norm_zero proj_spherI real_vector.scale_zero_left scaleR_one surf)
have *: "∃y. norm y = 1 ∧ y ∈ affine hull S ∧ x = surf (proj y)"
if "x ∈ S" "x ∉ rel_interior S" for x
proof -
have "proj x ∈ ?SPHER"
by (metis (full_types) "0" hull_inc proj_spherI that)
moreover have "surf (proj x) = x"
by (metis Diff_iff homeomorphism_def surf that)
ultimately show ?thesis
by (metis ‹⋀x. x ∈ ?SPHER ⟹ surf x ≠ 0› hull_inc inverse_1 local.proj_def norm_sgn projI scaleR_one sgn_div_norm that(1))
qed
have surfp_notin: "⋀x. ⟦norm x = 1; x ∈ affine hull S⟧ ⟹ surf (proj x) ∉ rel_interior S"
by (metis (full_types) DiffE one_neq_zero homeomorphism_def image_eqI norm_zero proj_spherI surf)
have no_sp_im: "(λx. norm x *⇩R surf (proj x)) ` (?SPHER) = S - rel_interior S"
by (auto simp: surfpS image_def Bex_def surfp_notin *)
have inj_spher: "inj_on (λx. norm x *⇩R surf (proj x)) ?SPHER"
proof
fix x y
assume xy: "x ∈ ?SPHER" "y ∈ ?SPHER"
and eq: " norm x *⇩R surf (proj x) = norm y *⇩R surf (proj y)"
then have "norm x = 1" "norm y = 1" "x ∈ affine hull S" "y ∈ affine hull S"
using 0 by auto
with eq show "x = y"
by (simp add: proj_def) (metis surf xy homeomorphism_def)
qed
have co01: "compact ?SPHER"
by (simp add: compact_Int_closed)
show "?SMINUS homeomorphic ?SPHER"
using homeomorphic_def surf by blast
have proj_scaleR: "⋀a x. 0 < a ⟹ proj (a *⇩R x) = proj x"
by (simp add: proj_def)
have cont_sp0: "continuous_on (affine hull S - {0}) (surf o proj)"
proof (rule continuous_on_compose [OF continuous_on_subset [OF cont_proj]])
show "continuous_on (proj ` (affine hull S - {0})) surf"
using homeomorphism_image1 proj_spherI surf by (intro continuous_on_subset [OF cont_surf]) fastforce
qed auto
obtain B where "B>0" and B: "⋀x. x ∈ S ⟹ norm x ≤ B"
by (metis compact_imp_bounded ‹compact S› bounded_pos_less less_eq_real_def)
have cont_nosp: "continuous (at x within ?CBALL) (λx. norm x *⇩R surf (proj x))"
if "norm x ≤ 1" "x ∈ affine hull S" for x
proof (cases "x=0")
case True
have "(norm ⤏ 0) (at 0 within cball 0 1 ∩ affine hull S)"
by (simp add: tendsto_norm_zero eventually_at)
with True show ?thesis
apply (simp add: continuous_within)
apply (rule lim_null_scaleR_bounded [where B=B])
using B ‹0 < B› local.proj_def projI surfpS by (auto simp: eventually_at)
next
case False
then have "∀⇩F x in at x. (x ∈ affine hull S - {0}) = (x ∈ affine hull S)"
by (force simp: False eventually_at)
moreover
have "continuous (at x within affine hull S - {0}) (λx. surf (proj x))"
using cont_sp0 False that by (auto simp add: continuous_on_eq_continuous_within)
ultimately have *: "continuous (at x within affine hull S) (λx. surf (proj x))"
by (simp add: continuous_within Lim_transform_within_set continuous_on_eq_continuous_within)
show ?thesis
by (intro continuous_within_subset [where S = "affine hull S", OF _ Int_lower2] continuous_intros *)
qed
have cont_nosp2: "continuous_on ?CBALL (λx. norm x *⇩R ((surf o proj) x))"
by (simp add: continuous_on_eq_continuous_within cont_nosp)
have "norm y *⇩R surf (proj y) ∈ S" if "y ∈ cball 0 1" and yaff: "y ∈ affine hull S" for y
proof (cases "y=0")
case True then show ?thesis
by (simp add: ‹0 ∈ S›)
next
case False
then have "norm y *⇩R surf (proj y) = norm y *⇩R surf (proj (y /⇩R norm y))"
by (simp add: proj_def)
have "norm y ≤ 1" using that by simp
have "surf (proj (y /⇩R norm y)) ∈ S"
using False local.proj_def nproj1 projI surfpS yaff by blast
then have "surf (proj y) ∈ S"
by (simp add: False proj_def)
then show "norm y *⇩R surf (proj y) ∈ S"
by (metis dual_order.antisym le_less_linear norm_ge_zero rel_interior_subset scaleR_one
starI subset_eq ‹norm y ≤ 1›)
qed
moreover have "x ∈ (λx. norm x *⇩R surf (proj x)) ` (?CBALL)" if "x ∈ S" for x
proof (cases "x=0")
case True with that hull_inc show ?thesis by fastforce
next
case False
then have psp: "proj (surf (proj x)) = proj x"
by (metis homeomorphism_def hull_inc proj_spherI surf that)
have nxx: "norm x *⇩R proj x = x"
by (simp add: False local.proj_def)
have affineI: "(1 / norm (surf (proj x))) *⇩R x ∈ affine hull S"
by (metis ‹0 ∈ S› affine_hull_span_0 hull_inc span_clauses(4) that)
have sproj_nz: "surf (proj x) ≠ 0"
by (metis False proj0_iff psp)
then have "proj x = proj (proj x)"
by (metis False nxx proj_scaleR zero_less_norm_iff)
moreover have scaleproj: "⋀a r. r *⇩R proj a = (r / norm a) *⇩R a"
by (simp add: divide_inverse local.proj_def)
ultimately have "(norm (surf (proj x)) / norm x) *⇩R x ∉ rel_interior S"
by (metis (no_types) sproj_nz divide_self_if hull_inc norm_eq_zero nproj1 projI psp scaleR_one surfp_notin that)
then have "(norm (surf (proj x)) / norm x) ≥ 1"
using starI [OF that] by (meson starI [OF that] le_less_linear norm_ge_zero zero_le_divide_iff)
then have nole: "norm x ≤ norm (surf (proj x))"
by (simp add: le_divide_eq_1)
let ?inx = "x /⇩R norm (surf (proj x))"
show ?thesis
proof
show "x = norm ?inx *⇩R surf (proj ?inx)"
by (simp add: field_simps) (metis inverse_eq_divide nxx positive_imp_inverse_positive proj_scaleR psp scaleproj sproj_nz zero_less_norm_iff)
qed (auto simp: field_split_simps nole affineI)
qed
ultimately have im_cball: "(λx. norm x *⇩R surf (proj x)) ` ?CBALL = S"
by blast
have inj_cball: "inj_on (λx. norm x *⇩R surf (proj x)) ?CBALL"
proof
fix x y
assume "x ∈ ?CBALL" "y ∈ ?CBALL"
and eq: "norm x *⇩R surf (proj x) = norm y *⇩R surf (proj y)"
then have x: "x ∈ affine hull S" and y: "y ∈ affine hull S"
using 0 by auto
show "x = y"
proof (cases "x=0 ∨ y=0")
case True then show "x = y" using eq proj_spherI surf_nz x y by force
next
case False
with x y have speq: "surf (proj x) = surf (proj y)"
by (metis eq homeomorphism_apply2 proj_scaleR proj_spherI surf zero_less_norm_iff)
then have "norm x = norm y"
by (metis ‹x ∈ affine hull S› ‹y ∈ affine hull S› eq proj_spherI real_vector.scale_cancel_right surf_nz)
moreover have "proj x = proj y"
by (metis (no_types) False speq homeomorphism_apply2 proj_spherI surf x y)
ultimately show "x = y"
using eq eqI by blast
qed
qed
have co01: "compact ?CBALL"
by (simp add: compact_Int_closed)
show "S homeomorphic ?CBALL"
using homeomorphic_compact [OF co01 cont_nosp2 [unfolded o_def] im_cball inj_cball] homeomorphic_sym by blast
qed
corollary
fixes S :: "'a::euclidean_space set"
assumes "compact S" and a: "a ∈ rel_interior S"
and star: "⋀x. x ∈ S ⟹ open_segment a x ⊆ rel_interior S"
shows starlike_compact_projective1:
"S - rel_interior S homeomorphic sphere a 1 ∩ affine hull S"
and starlike_compact_projective2:
"S homeomorphic cball a 1 ∩ affine hull S"
proof -
have 1: "compact ((+) (-a) ` S)" by (meson assms compact_translation)
have 2: "0 ∈ rel_interior ((+) (-a) ` S)"
using a rel_interior_translation [of "- a" S] by (simp cong: image_cong_simp)
have 3: "open_segment 0 x ⊆ rel_interior ((+) (-a) ` S)" if "x ∈ ((+) (-a) ` S)" for x
proof -
have "x+a ∈ S" using that by auto
then have "open_segment a (x+a) ⊆ rel_interior S" by (metis star)
then show ?thesis using open_segment_translation [of a 0 x]
using rel_interior_translation [of "- a" S] by (fastforce simp add: ac_simps image_iff cong: image_cong_simp)
qed
have "S - rel_interior S homeomorphic ((+) (-a) ` S) - rel_interior ((+) (-a) ` S)"
by (metis rel_interior_translation translation_diff homeomorphic_translation)
also have "... homeomorphic sphere 0 1 ∩ affine hull ((+) (-a) ` S)"
by (rule starlike_compact_projective1_0 [OF 1 2 3])
also have "... = (+) (-a) ` (sphere a 1 ∩ affine hull S)"
by (metis affine_hull_translation left_minus sphere_translation translation_Int)
also have "... homeomorphic sphere a 1 ∩ affine hull S"
using homeomorphic_translation homeomorphic_sym by blast
finally show "S - rel_interior S homeomorphic sphere a 1 ∩ affine hull S" .
have "S homeomorphic ((+) (-a) ` S)"
by (metis homeomorphic_translation)
also have "... homeomorphic cball 0 1 ∩ affine hull ((+) (-a) ` S)"
by (rule starlike_compact_projective2_0 [OF 1 2 3])
also have "... = (+) (-a) ` (cball a 1 ∩ affine hull S)"
by (metis affine_hull_translation left_minus cball_translation translation_Int)
also have "... homeomorphic cball a 1 ∩ affine hull S"
using homeomorphic_translation homeomorphic_sym by blast
finally show "S homeomorphic cball a 1 ∩ affine hull S" .
qed
corollary starlike_compact_projective_special:
assumes "compact S"
and cb01: "cball (0::'a::euclidean_space) 1 ⊆ S"
and scale: "⋀x u. ⟦x ∈ S; 0 ≤ u; u < 1⟧ ⟹ u *⇩R x ∈ S - frontier S"
shows "S homeomorphic (cball (0::'a::euclidean_space) 1)"
proof -
have "ball 0 1 ⊆ interior S"
using cb01 interior_cball interior_mono by blast
then have 0: "0 ∈ rel_interior S"
by (meson centre_in_ball subsetD interior_subset_rel_interior le_numeral_extra(2) not_le)
have [simp]: "affine hull S = UNIV"
using ‹ball 0 1 ⊆ interior S› by (auto intro!: affine_hull_nonempty_interior)
have star: "open_segment 0 x ⊆ rel_interior S" if "x ∈ S" for x
proof
fix p assume "p ∈ open_segment 0 x"
then obtain u where "x ≠ 0" and u: "0 ≤ u" "u < 1" and p: "u *⇩R x = p"
by (auto simp: in_segment)
then show "p ∈ rel_interior S"
using scale [OF that u] closure_subset frontier_def interior_subset_rel_interior by fastforce
qed
show ?thesis
using starlike_compact_projective2_0 [OF ‹compact S› 0 star] by simp
qed
lemma homeomorphic_convex_lemma:
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
assumes "convex S" "compact S" "convex T" "compact T"
and affeq: "aff_dim S = aff_dim T"
shows "(S - rel_interior S) homeomorphic (T - rel_interior T) ∧
S homeomorphic T"
proof (cases "rel_interior S = {} ∨ rel_interior T = {}")
case True
then show ?thesis
by (metis Diff_empty affeq ‹convex S› ‹convex T› aff_dim_empty homeomorphic_empty rel_interior_eq_empty aff_dim_empty)
next
case False
then obtain a b where a: "a ∈ rel_interior S" and b: "b ∈ rel_interior T" by auto
have starS: "⋀x. x ∈ S ⟹ open_segment a x ⊆ rel_interior S"
using rel_interior_closure_convex_segment
a ‹convex S› closure_subset subsetCE by blast
have starT: "⋀x. x ∈ T ⟹ open_segment b x ⊆ rel_interior T"
using rel_interior_closure_convex_segment
b ‹convex T› closure_subset subsetCE by blast
let ?aS = "(+) (-a) ` S" and ?bT = "(+) (-b) ` T"
have 0: "0 ∈ affine hull ?aS" "0 ∈ affine hull ?bT"
by (metis a b subsetD hull_inc image_eqI left_minus rel_interior_subset)+
have subs: "subspace (span ?aS)" "subspace (span ?bT)"
by (rule subspace_span)+
moreover
have "dim (span ((+) (- a) ` S)) = dim (span ((+) (- b) ` T))"
by (metis 0 aff_dim_translation_eq aff_dim_zero affeq dim_span nat_int)
ultimately obtain f g where "linear f" "linear g"
and fim: "f ` span ?aS = span ?bT"
and gim: "g ` span ?bT = span ?aS"
and fno: "⋀x. x ∈ span ?aS ⟹ norm(f x) = norm x"
and gno: "⋀x. x ∈ span ?bT ⟹ norm(g x) = norm x"
and gf: "⋀x. x ∈ span ?aS ⟹ g(f x) = x"
and fg: "⋀x. x ∈ span ?bT ⟹ f(g x) = x"
by (rule isometries_subspaces) blast
have [simp]: "continuous_on A f" for A
using ‹linear f› linear_conv_bounded_linear linear_continuous_on by blast
have [simp]: "continuous_on B g" for B
using ‹linear g› linear_conv_bounded_linear linear_continuous_on by blast
have eqspanS: "affine hull ?aS = span ?aS"
by (metis a affine_hull_span_0 subsetD hull_inc image_eqI left_minus rel_interior_subset)
have eqspanT: "affine hull ?bT = span ?bT"
by (metis b affine_hull_span_0 subsetD hull_inc image_eqI left_minus rel_interior_subset)
have "S homeomorphic cball a 1 ∩ affine hull S"
by (rule starlike_compact_projective2 [OF ‹compact S› a starS])
also have "... homeomorphic (+) (-a) ` (cball a 1 ∩ affine hull S)"
by (metis homeomorphic_translation)
also have "... = cball 0 1 ∩ (+) (-a) ` (affine hull S)"
by (auto simp: dist_norm)
also have "... = cball 0 1 ∩ span ?aS"
using eqspanS affine_hull_translation by blast
also have "... homeomorphic cball 0 1 ∩ span ?bT"
proof (rule homeomorphicI)
show fim1: "f ` (cball 0 1 ∩ span ?aS) = cball 0 1 ∩ span ?bT"
proof
show "f ` (cball 0 1 ∩ span ?aS) ⊆ cball 0 1 ∩ span ?bT"
using fim fno by auto
show "cball 0 1 ∩ span ?bT ⊆ f ` (cball 0 1 ∩ span ?aS)"
by clarify (metis IntI fg gim gno image_eqI mem_cball_0)
qed
show "g ` (cball 0 1 ∩ span ?bT) = cball 0 1 ∩ span ?aS"
proof
show "g ` (cball 0 1 ∩ span ?bT) ⊆ cball 0 1 ∩ span ?aS"
using gim gno by auto
show "cball 0 1 ∩ span ?aS ⊆ g ` (cball 0 1 ∩ span ?bT)"
by clarify (metis IntI fim1 gf image_eqI)
qed
qed (auto simp: fg gf)
also have "... = cball 0 1 ∩ (+) (-b) ` (affine hull T)"
using eqspanT affine_hull_translation by blast
also have "... = (+) (-b) ` (cball b 1 ∩ affine hull T)"
by (auto simp: dist_norm)
also have "... homeomorphic (cball b 1 ∩ affine hull T)"
by (metis homeomorphic_translation homeomorphic_sym)
also have "... homeomorphic T"
by (metis starlike_compact_projective2 [OF ‹compact T› b starT] homeomorphic_sym)
finally have 1: "S homeomorphic T" .
have "S - rel_interior S homeomorphic sphere a 1 ∩ affine hull S"
by (rule starlike_compact_projective1 [OF ‹compact S› a starS])
also have "... homeomorphic (+) (-a) ` (sphere a 1 ∩ affine hull S)"
by (metis homeomorphic_translation)
also have "... = sphere 0 1 ∩ (+) (-a) ` (affine hull S)"
by (auto simp: dist_norm)
also have "... = sphere 0 1 ∩ span ?aS"
using eqspanS affine_hull_translation by blast
also have "... homeomorphic sphere 0 1 ∩ span ?bT"
proof (rule homeomorphicI)
show fim1: "f ` (sphere 0 1 ∩ span ?aS) = sphere 0 1 ∩ span ?bT"
proof
show "f ` (sphere 0 1 ∩ span ?aS) ⊆ sphere 0 1 ∩ span ?bT"
using fim fno by auto
show "sphere 0 1 ∩ span ?bT ⊆ f ` (sphere 0 1 ∩ span ?aS)"
by clarify (metis IntI fg gim gno image_eqI mem_sphere_0)
qed
show "g ` (sphere 0 1 ∩ span ?bT) = sphere 0 1 ∩ span ?aS"
proof
show "g ` (sphere 0 1 ∩ span ?bT) ⊆ sphere 0 1 ∩ span ?aS"
using gim gno by auto
show "sphere 0 1 ∩ span ?aS ⊆ g ` (sphere 0 1 ∩ span ?bT)"
by clarify (metis IntI fim1 gf image_eqI)
qed
qed (auto simp: fg gf)
also have "... = sphere 0 1 ∩ (+) (-b) ` (affine hull T)"
using eqspanT affine_hull_translation by blast
also have "... = (+) (-b) ` (sphere b 1 ∩ affine hull T)"
by (auto simp: dist_norm)
also have "... homeomorphic (sphere b 1 ∩ affine hull T)"
by (metis homeomorphic_translation homeomorphic_sym)
also have "... homeomorphic T - rel_interior T"
by (metis starlike_compact_projective1 [OF ‹compact T› b starT] homeomorphic_sym)
finally have 2: "S - rel_interior S homeomorphic T - rel_interior T" .
show ?thesis
using 1 2 by blast
qed
lemma homeomorphic_convex_compact_sets:
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
assumes "convex S" "compact S" "convex T" "compact T"
and affeq: "aff_dim S = aff_dim T"
shows "S homeomorphic T"
using homeomorphic_convex_lemma [OF assms] assms
by (auto simp: rel_frontier_def)
lemma homeomorphic_rel_frontiers_convex_bounded_sets:
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
assumes "convex S" "bounded S" "convex T" "bounded T"
and affeq: "aff_dim S = aff_dim T"
shows "rel_frontier S homeomorphic rel_frontier T"
using assms homeomorphic_convex_lemma [of "closure S" "closure T"]
by (simp add: rel_frontier_def convex_rel_interior_closure)
subsection‹Homeomorphisms between punctured spheres and affine sets›
text‹Including the famous stereoscopic projection of the 3-D sphere to the complex plane›
text‹The special case with centre 0 and radius 1›
lemma homeomorphic_punctured_affine_sphere_affine_01:
assumes "b ∈ sphere 0 1" "affine T" "0 ∈ T" "b ∈ T" "affine p"
and affT: "aff_dim T = aff_dim p + 1"
shows "(sphere 0 1 ∩ T) - {b} homeomorphic p"
proof -
have [simp]: "norm b = 1" "b∙b = 1"
using assms by (auto simp: norm_eq_1)
have [simp]: "T ∩ {v. b∙v = 0} ≠ {}"
using ‹0 ∈ T› by auto
have [simp]: "¬ T ⊆ {v. b∙v = 0}"
using ‹norm b = 1› ‹b ∈ T› by auto
define f where "f ≡ λx. 2 *⇩R b + (2 / (1 - b∙x)) *⇩R (x - b)"
define g where "g ≡ λy. b + (4 / (norm y ^ 2 + 4)) *⇩R (y - 2 *⇩R b)"
have fg[simp]: "⋀x. ⟦x ∈ T; b∙x = 0⟧ ⟹ f (g x) = x"
unfolding f_def g_def by (simp add: algebra_simps field_split_simps add_nonneg_eq_0_iff)
have no: "(norm (f x))⇧2 = 4 * (1 + b ∙ x) / (1 - b ∙ x)"
if "norm x = 1" and "b ∙ x ≠ 1" for x
using that sum_sqs_eq [of 1 "b ∙ x"]
apply (simp flip: dot_square_norm add: norm_eq_1 nonzero_eq_divide_eq)
apply (simp add: f_def vector_add_divide_simps inner_simps)
apply (auto simp add: field_split_simps inner_commute)
done
have [simp]: "⋀u::real. 8 + u * (u * 8) = u * 16 ⟷ u=1"
by algebra
have gf[simp]: "⋀x. ⟦norm x = 1; b ∙ x ≠ 1⟧ ⟹ g (f x) = x"
unfolding g_def no by (auto simp: f_def field_split_simps)
have g1: "norm (g x) = 1" if "x ∈ T" and "b ∙ x = 0" for x
using that
apply (simp only: g_def)
apply (rule power2_eq_imp_eq)
apply (simp_all add: dot_square_norm [symmetric] divide_simps vector_add_divide_simps)
apply (simp add: algebra_simps inner_commute)
done
have ne1: "b ∙ g x ≠ 1" if "x ∈ T" and "b ∙ x = 0" for x
using that unfolding g_def
apply (simp_all add: dot_square_norm [symmetric] divide_simps vector_add_divide_simps add_nonneg_eq_0_iff)
apply (auto simp: algebra_simps)
done
have "subspace T"
by (simp add: assms subspace_affine)
have gT: "⋀x. ⟦x ∈ T; b ∙ x = 0⟧ ⟹ g x ∈ T"
unfolding g_def
by (blast intro: ‹subspace T› ‹b ∈ T› subspace_add subspace_mul subspace_diff)
have "f ` {x. norm x = 1 ∧ b∙x ≠ 1} ⊆ {x. b∙x = 0}"
unfolding f_def using ‹norm b = 1› norm_eq_1
by (force simp: field_simps inner_add_right inner_diff_right)
moreover have "f ` T ⊆ T"
unfolding f_def using assms ‹subspace T›
by (auto simp add: inner_add_right inner_diff_right mem_affine_3_minus subspace_mul)
moreover have "{x. b∙x = 0} ∩ T ⊆ f ` ({x. norm x = 1 ∧ b∙x ≠ 1} ∩ T)"
by clarify (metis (mono_tags) IntI ne1 fg gT g1 imageI mem_Collect_eq)
ultimately have imf: "f ` ({x. norm x = 1 ∧ b∙x ≠ 1} ∩ T) = {x. b∙x = 0} ∩ T"
by blast
have no4: "⋀y. b∙y = 0 ⟹ norm ((y∙y + 4) *⇩R b + 4 *⇩R (y - 2 *⇩R b)) = y∙y + 4"
apply (rule power2_eq_imp_eq)
apply (simp_all flip: dot_square_norm)
apply (auto simp: power2_eq_square algebra_simps inner_commute)
done
have [simp]: "⋀x. ⟦norm x = 1; b ∙ x ≠ 1⟧ ⟹ b ∙ f x = 0"
by (simp add: f_def algebra_simps field_split_simps)
have [simp]: "⋀x. ⟦x ∈ T; norm x = 1; b ∙ x ≠ 1⟧ ⟹ f x ∈ T"
unfolding f_def
by (blast intro: ‹subspace T› ‹b ∈ T› subspace_add subspace_mul subspace_diff)
have "g ` {x. b∙x = 0} ⊆ {x. norm x = 1 ∧ b∙x ≠ 1}"
unfolding g_def
apply (clarsimp simp: no4 vector_add_divide_simps divide_simps add_nonneg_eq_0_iff dot_square_norm [symmetric])
apply (auto simp: algebra_simps)
done
moreover have "g ` T ⊆ T"
unfolding g_def
by (blast intro: ‹subspace T› ‹b ∈ T› subspace_add subspace_mul subspace_diff)
moreover have "{x. norm x = 1 ∧ b∙x ≠ 1} ∩ T ⊆ g ` ({x. b∙x = 0} ∩ T)"
by clarify (metis (mono_tags, lifting) IntI gf image_iff imf mem_Collect_eq)
ultimately have img: "g ` ({x. b∙x = 0} ∩ T) = {x. norm x = 1 ∧ b∙x ≠ 1} ∩ T"
by blast
have aff: "affine ({x. b∙x = 0} ∩ T)"
by (blast intro: affine_hyperplane assms)
have contf: "continuous_on ({x. norm x = 1 ∧ b∙x ≠ 1} ∩ T) f"
unfolding f_def by (rule continuous_intros | force)+
have contg: "continuous_on ({x. b∙x = 0} ∩ T) g"
unfolding g_def by (rule continuous_intros | force simp: add_nonneg_eq_0_iff)+
have "(sphere 0 1 ∩ T) - {b} = {x. norm x = 1 ∧ (b∙x ≠ 1)} ∩ T"
using ‹norm b = 1› by (auto simp: norm_eq_1) (metis vector_eq ‹b∙b = 1›)
also have "... homeomorphic {x. b∙x = 0} ∩ T"
by (rule homeomorphicI [OF imf img contf contg]) auto
also have "... homeomorphic p"
proof (rule homeomorphic_affine_sets [OF aff ‹affine p›])
show "aff_dim ({x. b ∙ x = 0} ∩ T) = aff_dim p"
by (simp add: Int_commute aff_dim_affine_Int_hyperplane [OF ‹affine T›] affT)
qed
finally show ?thesis .
qed
theorem homeomorphic_punctured_affine_sphere_affine:
fixes a :: "'a :: euclidean_space"
assumes "0 < r" "b ∈ sphere a r" "affine T" "a ∈ T" "b ∈ T" "affine p"
and aff: "aff_dim T = aff_dim p + 1"
shows "(sphere a r ∩ T) - {b} homeomorphic p"
proof -
have "a ≠ b" using assms by auto
then have inj: "inj (λx::'a. x /⇩R norm (a - b))"
by (simp add: inj_on_def)
have "((sphere a r ∩ T) - {b}) homeomorphic
(+) (-a) ` ((sphere a r ∩ T) - {b})"
by (rule homeomorphic_translation)
also have "... homeomorphic (*⇩R) (inverse r) ` (+) (- a) ` (sphere a r ∩ T - {b})"
by (metis ‹0 < r› homeomorphic_scaling inverse_inverse_eq inverse_zero less_irrefl)
also have "... = sphere 0 1 ∩ ((*⇩R) (inverse r) ` (+) (- a) ` T) - {(b - a) /⇩R r}"
using assms by (auto simp: dist_norm norm_minus_commute divide_simps)
also have "... homeomorphic p"
using assms affine_translation [symmetric, of "- a"] aff_dim_translation_eq [of "- a"]
by (intro homeomorphic_punctured_affine_sphere_affine_01) (auto simp: dist_norm norm_minus_commute affine_scaling inj)
finally show ?thesis .
qed
corollary homeomorphic_punctured_sphere_affine:
fixes a :: "'a :: euclidean_space"
assumes "0 < r" and b: "b ∈ sphere a r"
and "affine T" and affS: "aff_dim T + 1 = DIM('a)"
shows "(sphere a r - {b}) homeomorphic T"
using homeomorphic_punctured_affine_sphere_affine [of r b a UNIV T] assms by auto
corollary homeomorphic_punctured_sphere_hyperplane:
fixes a :: "'a :: euclidean_space"
assumes "0 < r" and b: "b ∈ sphere a r"
and "c ≠ 0"
shows "(sphere a r - {b}) homeomorphic {x::'a. c ∙ x = d}"
using assms
by (intro homeomorphic_punctured_sphere_affine) (auto simp: affine_hyperplane of_nat_diff)
proposition homeomorphic_punctured_sphere_affine_gen:
fixes a :: "'a :: euclidean_space"
assumes "convex S" "bounded S" and a: "a ∈ rel_frontier S"
and "affine T" and affS: "aff_dim S = aff_dim T + 1"
shows "rel_frontier S - {a} homeomorphic T"
proof -
obtain U :: "'a set" where "affine U" "convex U" and affdS: "aff_dim U = aff_dim S"
using choose_affine_subset [OF affine_UNIV aff_dim_geq]
by (meson aff_dim_affine_hull affine_affine_hull affine_imp_convex)
have "S ≠ {}" using assms by auto
then obtain z where "z ∈ U"
by (metis aff_dim_negative_iff equals0I affdS)
then have bne: "ball z 1 ∩ U ≠ {}" by force
then have [simp]: "aff_dim(ball z 1 ∩ U) = aff_dim U"
using aff_dim_convex_Int_open [OF ‹convex U› open_ball]
by (fastforce simp add: Int_commute)
have "rel_frontier S homeomorphic rel_frontier (ball z 1 ∩ U)"
by (rule homeomorphic_rel_frontiers_convex_bounded_sets)
(auto simp: ‹affine U› affine_imp_convex convex_Int affdS assms)
also have "... = sphere z 1 ∩ U"
using convex_affine_rel_frontier_Int [of "ball z 1" U]
by (simp add: ‹affine U› bne)
finally have "rel_frontier S homeomorphic sphere z 1 ∩ U" .
then obtain h k where him: "h ` rel_frontier S = sphere z 1 ∩ U"
and kim: "k ` (sphere z 1 ∩ U) = rel_frontier S"
and hcon: "continuous_on (rel_frontier S) h"
and kcon: "continuous_on (sphere z 1 ∩ U) k"
and kh: "⋀x. x ∈ rel_frontier S ⟹ k(h(x)) = x"
and hk: "⋀y. y ∈ sphere z 1 ∩ U ⟹ h(k(y)) = y"
unfolding homeomorphic_def homeomorphism_def by auto
have "rel_frontier S - {a} homeomorphic (sphere z 1 ∩ U) - {h a}"
proof (rule homeomorphicI)
show h: "h ` (rel_frontier S - {a}) = sphere z 1 ∩ U - {h a}"
using him a kh by auto metis
show "k ` (sphere z 1 ∩ U - {h a}) = rel_frontier S - {a}"
by (force simp: h [symmetric] image_comp o_def kh)
qed (auto intro: continuous_on_subset hcon kcon simp: kh hk)
also have "... homeomorphic T"
by (rule homeomorphic_punctured_affine_sphere_affine)
(use a him in ‹auto simp: affS affdS ‹affine T› ‹affine U› ‹z ∈ U››)
finally show ?thesis .
qed
text‹ When dealing with AR, ANR and ANR later, it's useful to know that every set
is homeomorphic to a closed subset of a convex set, and
if the set is locally compact we can take the convex set to be the universe.›
proposition homeomorphic_closedin_convex:
fixes S :: "'m::euclidean_space set"
assumes "aff_dim S < DIM('n)"
obtains U and T :: "'n::euclidean_space set"
where "convex U" "U ≠ {}" "closedin (top_of_set U) T"
"S homeomorphic T"
proof (cases "S = {}")
case True then show ?thesis
by (rule_tac U=UNIV and T="{}" in that) auto
next
case False
then obtain a where "a ∈ S" by auto
obtain i::'n where i: "i ∈ Basis" "i ≠ 0"
using SOME_Basis Basis_zero by force
have "0 ∈ affine hull ((+) (- a) ` S)"
by (simp add: ‹a ∈ S› hull_inc)
then have "dim ((+) (- a) ` S) = aff_dim ((+) (- a) ` S)"
by (simp add: aff_dim_zero)
also have "... < DIM('n)"
by (simp add: aff_dim_translation_eq_subtract assms cong: image_cong_simp)
finally have dd: "dim ((+) (- a) ` S) < DIM('n)"
by linarith
have span: "span {x. i ∙ x = 0} = {x. i ∙ x = 0}"
using span_eq_iff [symmetric, of "{x. i ∙ x = 0}"] subspace_hyperplane [of i] by simp
have "dim ((+) (- a) ` S) ≤ dim {x. i ∙ x = 0}"
using dd by (simp add: dim_hyperplane [OF ‹i ≠ 0›])
then obtain T where "subspace T" and Tsub: "T ⊆ {x. i ∙ x = 0}"
and dimT: "dim T = dim ((+) (- a) ` S)"
by (rule choose_subspace_of_subspace) (simp add: span)
have "subspace (span ((+) (- a) ` S))"
using subspace_span by blast
then obtain h k where "linear h" "linear k"
and heq: "h ` span ((+) (- a) ` S) = T"
and keq:"k ` T = span ((+) (- a) ` S)"
and hinv [simp]: "⋀x. x ∈ span ((+) (- a) ` S) ⟹ k(h x) = x"
and kinv [simp]: "⋀x. x ∈ T ⟹ h(k x) = x"
by (auto simp: dimT intro: isometries_subspaces [OF _ ‹subspace T›] dimT)
have hcont: "continuous_on A h" and kcont: "continuous_on B k" for A B
using ‹linear h› ‹linear k› linear_continuous_on linear_conv_bounded_linear by blast+
have ihhhh[simp]: "⋀x. x ∈ S ⟹ i ∙ h (x - a) = 0"
using Tsub [THEN subsetD] heq span_superset by fastforce
have "sphere 0 1 - {i} homeomorphic {x. i ∙ x = 0}"
proof (rule homeomorphic_punctured_sphere_affine)
show "affine {x. i ∙ x = 0}"
by (auto simp: affine_hyperplane)
show "aff_dim {x. i ∙ x = 0} + 1 = int DIM('n)"
using i by force
qed (use i in auto)
then obtain f g where fg: "homeomorphism (sphere 0 1 - {i}) {x. i ∙ x = 0} f g"
by (force simp: homeomorphic_def)
show ?thesis
proof
have "h ` (+) (- a) ` S ⊆ T"
using heq span_superset span_linear_image by blast
then have "g ` h ` (+) (- a) ` S ⊆ g ` {x. i ∙ x = 0}"
using Tsub by (simp add: image_mono)
also have "... ⊆ sphere 0 1 - {i}"
by (simp add: fg [unfolded homeomorphism_def])
finally have gh_sub_sph: "(g ∘ h) ` (+) (- a) ` S ⊆ sphere 0 1 - {i}"
by (metis image_comp)
then have gh_sub_cb: "(g ∘ h) ` (+) (- a) ` S ⊆ cball 0 1"
by (metis Diff_subset order_trans sphere_cball)
have [simp]: "⋀u. u ∈ S ⟹ norm (g (h (u - a))) = 1"
using gh_sub_sph [THEN subsetD] by (auto simp: o_def)
show "convex (ball 0 1 ∪ (g ∘ h) ` (+) (- a) ` S)"
by (meson ball_subset_cball convex_intermediate_ball gh_sub_cb sup.bounded_iff sup.cobounded1)
show "closedin (top_of_set (ball 0 1 ∪ (g ∘ h) ` (+) (- a) ` S)) ((g ∘ h) ` (+) (- a) ` S)"
unfolding closedin_closed
by (rule_tac x="sphere 0 1" in exI) auto
have ghcont: "continuous_on ((λx. x - a) ` S) (λx. g (h x))"
by (rule continuous_on_compose2 [OF homeomorphism_cont2 [OF fg] hcont], force)
have kfcont: "continuous_on ((λx. g (h (x - a))) ` S) (λx. k (f x))"
proof (rule continuous_on_compose2 [OF kcont])
show "continuous_on ((λx. g (h (x - a))) ` S) f"
using homeomorphism_cont1 [OF fg] gh_sub_sph by (fastforce intro: continuous_on_subset)
qed auto
have "S homeomorphic (+) (- a) ` S"
by (fact homeomorphic_translation)
also have "… homeomorphic (g ∘ h) ` (+) (- a) ` S"
apply (simp add: homeomorphic_def homeomorphism_def cong: image_cong_simp)
apply (rule_tac x="g ∘ h" in exI)
apply (rule_tac x="k ∘ f" in exI)
apply (auto simp: ghcont kfcont span_base homeomorphism_apply2 [OF fg] image_comp cong: image_cong_simp)
done
finally show "S homeomorphic (g ∘ h) ` (+) (- a) ` S" .
qed auto
qed
subsection‹Locally compact sets in an open set›
text‹ Locally compact sets are closed in an open set and are homeomorphic
to an absolutely closed set if we have one more dimension to play with.›
lemma locally_compact_open_Int_closure:
fixes S :: "'a :: metric_space set"
assumes "locally compact S"
obtains T where "open T" "S = T ∩ closure S"
proof -
have "∀x∈S. ∃T v u. u = S ∩ T ∧ x ∈ u ∧ u ⊆ v ∧ v ⊆ S ∧ open T ∧ compact v"
by (metis assms locally_compact openin_open)
then obtain t v where
tv: "⋀x. x ∈ S
⟹ v x ⊆ S ∧ open (t x) ∧ compact (v x) ∧ (∃u. x ∈ u ∧ u ⊆ v x ∧ u = S ∩ t x)"
by metis
then have o: "open (⋃(t ` S))"
by blast
have "S = ⋃ (v ` S)"
using tv by blast
also have "... = ⋃(t ` S) ∩ closure S"
proof
show "⋃(v ` S) ⊆ ⋃(t ` S) ∩ closure S"
by clarify (meson IntD2 IntI UN_I closure_subset subsetD tv)
have "t x ∩ closure S ⊆ v x" if "x ∈ S" for x
proof -
have "t x ∩ closure S ⊆ closure (t x ∩ S)"
by (simp add: open_Int_closure_subset that tv)
also have "... ⊆ v x"
by (metis Int_commute closure_minimal compact_imp_closed that tv)
finally show ?thesis .
qed
then show "⋃(t ` S) ∩ closure S ⊆ ⋃(v ` S)"
by blast
qed
finally have e: "S = ⋃(t ` S) ∩ closure S" .
show ?thesis
by (rule that [OF o e])
qed
lemma locally_compact_closedin_open:
fixes S :: "'a :: metric_space set"
assumes "locally compact S"
obtains T where "open T" "closedin (top_of_set T) S"
by (metis locally_compact_open_Int_closure [OF assms] closed_closure closedin_closed_Int)
lemma locally_compact_homeomorphism_projection_closed:
assumes "locally compact S"
obtains T and f :: "'a ⇒ 'a :: euclidean_space × 'b :: euclidean_space"
where "closed T" "homeomorphism S T f fst"
proof (cases "closed S")
case True
show ?thesis
proof
show "homeomorphism S (S × {0}) (λx. (x, 0)) fst"
by (auto simp: homeomorphism_def continuous_intros)
qed (use True closed_Times in auto)
next
case False
obtain U where "open U" and US: "U ∩ closure S = S"
by (metis locally_compact_open_Int_closure [OF assms])
with False have Ucomp: "-U ≠ {}"
using closure_eq by auto
have [simp]: "closure (- U) = -U"
by (simp add: ‹open U› closed_Compl)
define f :: "'a ⇒ 'a × 'b" where "f ≡ λx. (x, One /⇩R setdist {x} (- U))"
have "continuous_on U (λx. (x, One /⇩R setdist {x} (- U)))"
proof (intro continuous_intros continuous_on_setdist)
show "∀x∈U. setdist {x} (- U) ≠ 0"
by (simp add: Ucomp setdist_eq_0_sing_1)
qed
then have homU: "homeomorphism U (f`U) f fst"
by (auto simp: f_def homeomorphism_def image_iff continuous_intros)
have cloS: "closedin (top_of_set U) S"
by (metis US closed_closure closedin_closed_Int)
have cont: "isCont ((λx. setdist {x} (- U)) o fst) z" for z :: "'a × 'b"
by (rule continuous_at_compose continuous_intros continuous_at_setdist)+
have setdist1D: "setdist {a} (- U) *⇩R b = One ⟹ setdist {a} (- U) ≠ 0" for a::'a and b::'b
by force
have *: "r *⇩R b = One ⟹ b = (1 / r) *⇩R One" for r and b::'b
by (metis One_non_0 nonzero_divide_eq_eq real_vector.scale_eq_0_iff real_vector.scale_scale scaleR_one)
have "⋀a b::'b. setdist {a} (- U) *⇩R b = One ⟹ (a,b) ∈ (λx. (x, (1 / setdist {x} (- U)) *⇩R One)) ` U"
by (metis (mono_tags, lifting) "*" ComplI image_eqI setdist1D setdist_sing_in_set)
then have "f ` U = (λz. (setdist {fst z} (- U) *⇩R snd z)) -` {One}"
by (auto simp: f_def setdist_eq_0_sing_1 field_simps Ucomp)
then have clfU: "closed (f ` U)"
by (force intro: continuous_intros cont [unfolded o_def] continuous_closed_vimage)
have "closed (f ` S)"
by (metis closedin_closed_trans [OF _ clfU] homeomorphism_imp_closed_map [OF homU cloS])
then show ?thesis
by (metis US homU homeomorphism_of_subsets inf_sup_ord(1) that)
qed
lemma locally_compact_closed_Int_open:
fixes S :: "'a :: euclidean_space set"
shows "locally compact S ⟷ (∃U V. closed U ∧ open V ∧ S = U ∩ V)" (is "?lhs = ?rhs")
proof
show "?lhs ⟹ ?rhs"
by (metis closed_closure inf_commute locally_compact_open_Int_closure)
show "?rhs ⟹ ?lhs"
by (meson closed_imp_locally_compact locally_compact_Int open_imp_locally_compact)
qed
lemma lowerdim_embeddings:
assumes "DIM('a) < DIM('b)"
obtains f :: "'a::euclidean_space*real ⇒ 'b::euclidean_space"
and g :: "'b ⇒ 'a*real"
and j :: 'b
where "linear f" "linear g" "⋀z. g (f z) = z" "j ∈ Basis" "⋀x. f(x,0) ∙ j = 0"
proof -
let ?B = "Basis :: ('a*real) set"
have b01: "(0,1) ∈ ?B"
by (simp add: Basis_prod_def)
have "DIM('a * real) ≤ DIM('b)"
by (simp add: Suc_leI assms)
then obtain basf :: "'a*real ⇒ 'b" where sbf: "basf ` ?B ⊆ Basis" and injbf: "inj_on basf Basis"
by (metis finite_Basis card_le_inj)
define basg:: "'b ⇒ 'a * real" where
"basg ≡ λi. if i ∈ basf ` Basis then inv_into Basis basf i else (0,1)"
have bgf[simp]: "basg (basf i) = i" if "i ∈ Basis" for i
using inv_into_f_f injbf that by (force simp: basg_def)
have sbg: "basg ` Basis ⊆ ?B"
by (force simp: basg_def injbf b01)
define f :: "'a*real ⇒ 'b" where "f ≡ λu. ∑j∈Basis. (u ∙ basg j) *⇩R j"
define g :: "'b ⇒ 'a*real" where "g ≡ λz. (∑i∈Basis. (z ∙ basf i) *⇩R i)"
show ?thesis
proof
show "linear f"
unfolding f_def
by (intro linear_compose_sum linearI ballI) (auto simp: algebra_simps)
show "linear g"
unfolding g_def
by (intro linear_compose_sum linearI ballI) (auto simp: algebra_simps)
have *: "(∑a ∈ Basis. a ∙ basf b * (x ∙ basg a)) = x ∙ b" if "b ∈ Basis" for x b
using sbf that by auto
show gf: "g (f x) = x" for x
proof (rule euclidean_eqI)
show "⋀b. b ∈ Basis ⟹ g (f x) ∙ b = x ∙ b"
using f_def g_def sbf by auto
qed
show "basf(0,1) ∈ Basis"
using b01 sbf by auto
then show "f(x,0) ∙ basf(0,1) = 0" for x
unfolding f_def inner_sum_left
using b01 inner_not_same_Basis
by (fastforce intro: comm_monoid_add_class.sum.neutral)
qed
qed
proposition locally_compact_homeomorphic_closed:
fixes S :: "'a::euclidean_space set"
assumes "locally compact S" and dimlt: "DIM('a) < DIM('b)"
obtains T :: "'b::euclidean_space set" where "closed T" "S homeomorphic T"
proof -
obtain U:: "('a*real)set" and h
where "closed U" and homU: "homeomorphism S U h fst"
using locally_compact_homeomorphism_projection_closed assms by metis
obtain f :: "'a*real ⇒ 'b" and g :: "'b ⇒ 'a*real"
where "linear f" "linear g" and gf [simp]: "⋀z. g (f z) = z"
using lowerdim_embeddings [OF dimlt] by metis
then have "inj f"
by (metis injI)
have gfU: "g ` f ` U = U"
by (simp add: image_comp o_def)
have "S homeomorphic U"
using homU homeomorphic_def by blast
also have "... homeomorphic f ` U"
proof (rule homeomorphicI [OF refl gfU])
show "continuous_on U f"
by (meson ‹inj f› ‹linear f› homeomorphism_cont2 linear_homeomorphism_image)
show "continuous_on (f ` U) g"
using ‹linear g› linear_continuous_on linear_conv_bounded_linear by blast
qed (auto simp: o_def)
finally show ?thesis
using ‹closed U› ‹inj f› ‹linear f› closed_injective_linear_image that by blast
qed
lemma homeomorphic_convex_compact_lemma:
fixes S :: "'a::euclidean_space set"
assumes "convex S"
and "compact S"
and "cball 0 1 ⊆ S"
shows "S homeomorphic (cball (0::'a) 1)"
proof (rule starlike_compact_projective_special[OF assms(2-3)])
fix x u
assume "x ∈ S" and "0 ≤ u" and "u < (1::real)"
have "open (ball (u *⇩R x) (1 - u))"
by (rule open_ball)
moreover have "u *⇩R x ∈ ball (u *⇩R x) (1 - u)"
unfolding centre_in_ball using ‹u < 1› by simp
moreover have "ball (u *⇩R x) (1 - u) ⊆ S"
proof
fix y
assume "y ∈ ball (u *⇩R x) (1 - u)"
then have "dist (u *⇩R x) y < 1 - u"
unfolding mem_ball .
with ‹u < 1› have "inverse (1 - u) *⇩R (y - u *⇩R x) ∈ cball 0 1"
by (simp add: dist_norm inverse_eq_divide norm_minus_commute)
with assms(3) have "inverse (1 - u) *⇩R (y - u *⇩R x) ∈ S" ..
with assms(1) have "(1 - u) *⇩R ((y - u *⇩R x) /⇩R (1 - u)) + u *⇩R x ∈ S"
using ‹x ∈ S› ‹0 ≤ u› ‹u < 1› [THEN less_imp_le] by (rule convexD_alt)
then show "y ∈ S" using ‹u < 1›
by simp
qed
ultimately have "u *⇩R x ∈ interior S" ..
then show "u *⇩R x ∈ S - frontier S"
using frontier_def and interior_subset by auto
qed
proposition homeomorphic_convex_compact_cball:
fixes e :: real
and S :: "'a::euclidean_space set"
assumes S: "convex S" "compact S" "interior S ≠ {}" and "e > 0"
shows "S homeomorphic (cball (b::'a) e)"
proof (rule homeomorphic_trans[OF _ homeomorphic_balls(2)])
obtain a where "a ∈ interior S"
using assms by auto
then show "S homeomorphic cball (0::'a) 1"
by (metis (no_types) aff_dim_cball S compact_cball convex_cball
homeomorphic_convex_lemma interior_rel_interior_gen zero_less_one)
qed (use ‹e>0› in auto)
corollary homeomorphic_convex_compact:
fixes S :: "'a::euclidean_space set"
and T :: "'a set"
assumes "convex S" "compact S" "interior S ≠ {}"
and "convex T" "compact T" "interior T ≠ {}"
shows "S homeomorphic T"
using assms
by (meson zero_less_one homeomorphic_trans homeomorphic_convex_compact_cball homeomorphic_sym)
lemma homeomorphic_closed_intervals:
fixes a :: "'a::euclidean_space" and b and c :: "'a::euclidean_space" and d
assumes "box a b ≠ {}" and "box c d ≠ {}"
shows "(cbox a b) homeomorphic (cbox c d)"
by (simp add: assms homeomorphic_convex_compact)
lemma homeomorphic_closed_intervals_real:
fixes a::real and b and c::real and d
assumes "a<b" and "c<d"
shows "{a..b} homeomorphic {c..d}"
using assms by (auto intro: homeomorphic_convex_compact)
subsection‹Covering spaces and lifting results for them›
definition covering_space
:: "'a::topological_space set ⇒ ('a ⇒ 'b) ⇒ 'b::topological_space set ⇒ bool"
where
"covering_space c p S ≡
continuous_on c p ∧ p ` c = S ∧
(∀x ∈ S. ∃T. x ∈ T ∧ openin (top_of_set S) T ∧
(∃v. ⋃v = c ∩ p -` T ∧
(∀u ∈ v. openin (top_of_set c) u) ∧
pairwise disjnt v ∧
(∀u ∈ v. ∃q. homeomorphism u T p q)))"
lemma covering_spaceI [intro?]:
assumes "continuous_on c p" "p ` c = S"
"⋀x. x ∈ S ⟹ ∃T. x ∈ T ∧ openin (top_of_set S) T ∧
(∃v. ⋃v = c ∩ p -` T ∧ (∀u ∈ v. openin (top_of_set c) u) ∧
pairwise disjnt v ∧ (∀u ∈ v. ∃q. homeomorphism u T p q))"
shows "covering_space c p S"
using assms unfolding covering_space_def by auto
lemma covering_space_imp_continuous: "covering_space c p S ⟹ continuous_on c p"
by (simp add: covering_space_def)
lemma covering_space_imp_surjective: "covering_space c p S ⟹ p ` c = S"
by (simp add: covering_space_def)
lemma homeomorphism_imp_covering_space: "homeomorphism S T f g ⟹ covering_space S f T"
apply (clarsimp simp add: homeomorphism_def covering_space_def)
apply (rule_tac x=T in exI, simp)
apply (rule_tac x="{S}" in exI, auto)
done
lemma covering_space_local_homeomorphism:
assumes "covering_space c p S" "x ∈ c"
obtains T u q where "x ∈ T" "openin (top_of_set c) T"
"p x ∈ u" "openin (top_of_set S) u"
"homeomorphism T u p q"
using assms
by (clarsimp simp add: covering_space_def) (metis IntI UnionE vimage_eq)
lemma covering_space_local_homeomorphism_alt:
assumes p: "covering_space c p S" and "y ∈ S"
obtains x T U q where "p x = y"
"x ∈ T" "openin (top_of_set c) T"
"y ∈ U" "openin (top_of_set S) U"
"homeomorphism T U p q"
proof -
obtain x where "p x = y" "x ∈ c"
using assms covering_space_imp_surjective by blast
show ?thesis
using that ‹p x = y› by (auto intro: covering_space_local_homeomorphism [OF p ‹x ∈ c›])
qed
proposition covering_space_open_map:
fixes S :: "'a :: metric_space set" and T :: "'b :: metric_space set"
assumes p: "covering_space c p S" and T: "openin (top_of_set c) T"
shows "openin (top_of_set S) (p ` T)"
proof -
have pce: "p ` c = S"
and covs:
"⋀x. x ∈ S ⟹
∃X VS. x ∈ X ∧ openin (top_of_set S) X ∧
⋃VS = c ∩ p -` X ∧
(∀u ∈ VS. openin (top_of_set c) u) ∧
pairwise disjnt VS ∧
(∀u ∈ VS. ∃q. homeomorphism u X p q)"
using p by (auto simp: covering_space_def)
have "T ⊆ c" by (metis openin_euclidean_subtopology_iff T)
have "∃X. openin (top_of_set S) X ∧ y ∈ X ∧ X ⊆ p ` T"
if "y ∈ p ` T" for y
proof -
have "y ∈ S" using ‹T ⊆ c› pce that by blast
obtain U VS where "y ∈ U" and U: "openin (top_of_set S) U"
and VS: "⋃VS = c ∩ p -` U"
and openVS: "∀V ∈ VS. openin (top_of_set c) V"
and homVS: "⋀V. V ∈ VS ⟹ ∃q. homeomorphism V U p q"
using covs [OF ‹y ∈ S›] by auto
obtain x where "x ∈ c" "p x ∈ U" "x ∈ T" "p x = y"
using T [unfolded openin_euclidean_subtopology_iff] ‹y ∈ U› ‹y ∈ p ` T› by blast
with VS obtain V where "x ∈ V" "V ∈ VS" by auto
then obtain q where q: "homeomorphism V U p q" using homVS by blast
then have ptV: "p ` (T ∩ V) = U ∩ q -` (T ∩ V)"
using VS ‹V ∈ VS› by (auto simp: homeomorphism_def)
have ocv: "openin (top_of_set c) V"
by (simp add: ‹V ∈ VS› openVS)
have "openin (top_of_set (q ` U)) (T ∩ V)"
using q unfolding homeomorphism_def
by (metis T inf.absorb_iff2 ocv openin_imp_subset openin_subtopology_Int subtopology_subtopology)
then have "openin (top_of_set U) (U ∩ q -` (T ∩ V))"
using continuous_on_open homeomorphism_def q by blast
then have os: "openin (top_of_set S) (U ∩ q -` (T ∩ V))"
using openin_trans [of U] by (simp add: Collect_conj_eq U)
show ?thesis
proof (intro exI conjI)
show "openin (top_of_set S) (p ` (T ∩ V))"
by (simp only: ptV os)
qed (use ‹p x = y› ‹x ∈ V› ‹x ∈ T› in auto)
qed
with openin_subopen show ?thesis by blast
qed
lemma covering_space_lift_unique_gen:
fixes f :: "'a::topological_space ⇒ 'b::topological_space"
fixes g1 :: "'a ⇒ 'c::real_normed_vector"
assumes cov: "covering_space c p S"
and eq: "g1 a = g2 a"
and f: "continuous_on T f" "f ∈ T → S"
and g1: "continuous_on T g1" "g1 ∈ T → c"
and fg1: "⋀x. x ∈ T ⟹ f x = p(g1 x)"
and g2: "continuous_on T g2" "g2 ∈ T → c"
and fg2: "⋀x. x ∈ T ⟹ f x = p(g2 x)"
and u_compt: "U ∈ components T" and "a ∈ U" "x ∈ U"
shows "g1 x = g2 x"
proof -
have "U ⊆ T" by (rule in_components_subset [OF u_compt])
define G12 where "G12 ≡ {x ∈ U. g1 x - g2 x = 0}"
have "connected U" by (rule in_components_connected [OF u_compt])
have contu: "continuous_on U g1" "continuous_on U g2"
using ‹U ⊆ T› continuous_on_subset g1 g2 by blast+
have o12: "openin (top_of_set U) G12"
unfolding G12_def
proof (subst openin_subopen, clarify)
fix z
assume z: "z ∈ U" "g1 z - g2 z = 0"
obtain v w q where "g1 z ∈ v" and ocv: "openin (top_of_set c) v"
and "p (g1 z) ∈ w" and osw: "openin (top_of_set S) w"
and hom: "homeomorphism v w p q"
proof (rule covering_space_local_homeomorphism [OF cov])
show "g1 z ∈ c"
using ‹U ⊆ T› ‹z ∈ U› g1(2) by blast
qed auto
have "g2 z ∈ v" using ‹g1 z ∈ v› z by auto
have gg: "U ∩ g -` v = U ∩ g -` (v ∩ g ` U)" for g
by auto
have "openin (top_of_set (g1 ` U)) (v ∩ g1 ` U)"
using ocv ‹U ⊆ T› g1 by (fastforce simp add: openin_open)
then have 1: "openin (top_of_set U) (U ∩ g1 -` v)"
unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
have "openin (top_of_set (g2 ` U)) (v ∩ g2 ` U)"
using ocv ‹U ⊆ T› g2 by (fastforce simp add: openin_open)
then have 2: "openin (top_of_set U) (U ∩ g2 -` v)"
unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
let ?T = "(U ∩ g1 -` v) ∩ (U ∩ g2 -` v)"
show "∃T. openin (top_of_set U) T ∧ z ∈ T ∧ T ⊆ {z ∈ U. g1 z - g2 z = 0}"
proof (intro exI conjI)
show "openin (top_of_set U) ?T"
using "1" "2" by blast
show "z ∈ ?T"
using z by (simp add: ‹g1 z ∈ v› ‹g2 z ∈ v›)
show "?T ⊆ {z ∈ U. g1 z - g2 z = 0}"
using hom
by (clarsimp simp: homeomorphism_def) (metis ‹U ⊆ T› fg1 fg2 subsetD)
qed
qed
have c12: "closedin (top_of_set U) G12"
unfolding G12_def
by (intro continuous_intros continuous_closedin_preimage_constant contu)
have "G12 = {} ∨ G12 = U"
by (intro connected_clopen [THEN iffD1, rule_format] ‹connected U› conjI o12 c12)
with eq ‹a ∈ U› have "⋀x. x ∈ U ⟹ g1 x - g2 x = 0" by (auto simp: G12_def)
then show ?thesis
using ‹x ∈ U› by force
qed
proposition covering_space_lift_unique:
fixes f :: "'a::topological_space ⇒ 'b::topological_space"
fixes g1 :: "'a ⇒ 'c::real_normed_vector"
assumes "covering_space c p S"
"g1 a = g2 a"
"continuous_on T f" "f ∈ T → S"
"continuous_on T g1" "g1 ∈ T → c" "⋀x. x ∈ T ⟹ f x = p(g1 x)"
"continuous_on T g2" "g2 ∈ T → c" "⋀x. x ∈ T ⟹ f x = p(g2 x)"
"connected T" "a ∈ T" "x ∈ T"
shows "g1 x = g2 x"
using covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv
by blast
lemma covering_space_locally:
fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
assumes loc: "locally φ C" and cov: "covering_space C p S"
and pim: "⋀T. ⟦T ⊆ C; φ T⟧ ⟹ ψ(p ` T)"
shows "locally ψ S"
proof -
have "locally ψ (p ` C)"
proof (rule locally_open_map_image [OF loc])
show "continuous_on C p"
using cov covering_space_imp_continuous by blast
show "⋀T. openin (top_of_set C) T ⟹ openin (top_of_set (p ` C)) (p ` T)"
using cov covering_space_imp_surjective covering_space_open_map by blast
qed (simp add: pim)
then show ?thesis
using covering_space_imp_surjective [OF cov] by metis
qed
proposition covering_space_locally_eq:
fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
assumes cov: "covering_space C p S"
and pim: "⋀T. ⟦T ⊆ C; φ T⟧ ⟹ ψ(p ` T)"
and qim: "⋀q U. ⟦U ⊆ S; continuous_on U q; ψ U⟧ ⟹ φ(q ` U)"
shows "locally ψ S ⟷ locally φ C"
(is "?lhs = ?rhs")
proof
assume L: ?lhs
show ?rhs
proof (rule locallyI)
fix V x
assume V: "openin (top_of_set C) V" and "x ∈ V"
have "p x ∈ p ` C"
by (metis IntE V ‹x ∈ V› imageI openin_open)
then obtain T 𝒱 where "p x ∈ T"
and opeT: "openin (top_of_set S) T"
and veq: "⋃𝒱 = C ∩ p -` T"
and ope: "∀U∈𝒱. openin (top_of_set C) U"
and hom: "∀U∈𝒱. ∃q. homeomorphism U T p q"
using cov unfolding covering_space_def by (blast intro: that)
have "x ∈ ⋃𝒱"
using V veq ‹p x ∈ T› ‹x ∈ V› openin_imp_subset by fastforce
then obtain U where "x ∈ U" "U ∈ 𝒱"
by blast
then obtain q where opeU: "openin (top_of_set C) U" and q: "homeomorphism U T p q"
using ope hom by blast
with V have "openin (top_of_set C) (U ∩ V)"
by blast
then have UV: "openin (top_of_set S) (p ` (U ∩ V))"
using cov covering_space_open_map by blast
obtain W W' where opeW: "openin (top_of_set S) W" and "ψ W'" "p x ∈ W" "W ⊆ W'" and W'sub: "W' ⊆ p ` (U ∩ V)"
using locallyE [OF L UV] ‹x ∈ U› ‹x ∈ V› by blast
then have "W ⊆ T"
by (metis Int_lower1 q homeomorphism_image1 image_Int_subset order_trans)
show "∃U Z. openin (top_of_set C) U ∧
φ Z ∧ x ∈ U ∧ U ⊆ Z ∧ Z ⊆ V"
proof (intro exI conjI)
have "openin (top_of_set T) W"
by (meson opeW opeT openin_imp_subset openin_subset_trans ‹W ⊆ T›)
then have "openin (top_of_set U) (q ` W)"
by (meson homeomorphism_imp_open_map homeomorphism_symD q)
then show "openin (top_of_set C) (q ` W)"
using opeU openin_trans by blast
show "φ (q ` W')"
by (metis (mono_tags, lifting) Int_subset_iff UV W'sub ‹ψ W'› continuous_on_subset dual_order.trans homeomorphism_def image_Int_subset openin_imp_subset q qim)
show "x ∈ q ` W"
by (metis ‹p x ∈ W› ‹x ∈ U› homeomorphism_def imageI q)
show "q ` W ⊆ q ` W'"
using ‹W ⊆ W'› by blast
have "W' ⊆ p ` V"
using W'sub by blast
then show "q ` W' ⊆ V"
using W'sub homeomorphism_apply1 [OF q] by auto
qed
qed
next
assume ?rhs
then show ?lhs
using cov covering_space_locally pim by blast
qed
lemma covering_space_locally_compact_eq:
fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
assumes "covering_space C p S"
shows "locally compact S ⟷ locally compact C"
proof (rule covering_space_locally_eq [OF assms])
show "⋀T. ⟦T ⊆ C; compact T⟧ ⟹ compact (p ` T)"
by (meson assms compact_continuous_image continuous_on_subset covering_space_imp_continuous)
qed (use compact_continuous_image in blast)
lemma covering_space_locally_connected_eq:
fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
assumes "covering_space C p S"
shows "locally connected S ⟷ locally connected C"
proof (rule covering_space_locally_eq [OF assms])
show "⋀T. ⟦T ⊆ C; connected T⟧ ⟹ connected (p ` T)"
by (meson connected_continuous_image assms continuous_on_subset covering_space_imp_continuous)
qed (use connected_continuous_image in blast)
lemma covering_space_locally_path_connected_eq:
fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
assumes "covering_space C p S"
shows "locally path_connected S ⟷ locally path_connected C"
proof (rule covering_space_locally_eq [OF assms])
show "⋀T. ⟦T ⊆ C; path_connected T⟧ ⟹ path_connected (p ` T)"
by (meson path_connected_continuous_image assms continuous_on_subset covering_space_imp_continuous)
qed (use path_connected_continuous_image in blast)
lemma covering_space_locally_compact:
fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
assumes "locally compact C" "covering_space C p S"
shows "locally compact S"
using assms covering_space_locally_compact_eq by blast
lemma covering_space_locally_connected:
fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
assumes "locally connected C" "covering_space C p S"
shows "locally connected S"
using assms covering_space_locally_connected_eq by blast
lemma covering_space_locally_path_connected:
fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
assumes "locally path_connected C" "covering_space C p S"
shows "locally path_connected S"
using assms covering_space_locally_path_connected_eq by blast
proposition covering_space_lift_homotopy:
fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
and h :: "real × 'c::real_normed_vector ⇒ 'b"
assumes cov: "covering_space C p S"
and conth: "continuous_on ({0..1} × U) h"
and him: "h ∈ ({0..1} × U) → S"
and heq: "⋀y. y ∈ U ⟹ h (0,y) = p(f y)"
and contf: "continuous_on U f" and fim: "f ∈ U → C"
obtains k where "continuous_on ({0..1} × U) k"
"k ∈ ({0..1} × U) → C"
"⋀y. y ∈ U ⟹ k(0, y) = f y"
"⋀z. z ∈ {0..1} × U ⟹ h z = p(k z)"
proof -
have "∃V k. openin (top_of_set U) V ∧ y ∈ V ∧
continuous_on ({0..1} × V) k ∧ k ` ({0..1} × V) ⊆ C ∧
(∀z ∈ V. k(0, z) = f z) ∧ (∀z ∈ {0..1} × V. h z = p(k z))"
if "y ∈ U" for y
proof -
obtain UU where UU: "⋀s. s ∈ S ⟹ s ∈ (UU s) ∧ openin (top_of_set S) (UU s) ∧
(∃𝒱. ⋃𝒱 = C ∩ p -` UU s ∧
(∀U ∈ 𝒱. openin (top_of_set C) U) ∧
pairwise disjnt 𝒱 ∧
(∀U ∈ 𝒱. ∃q. homeomorphism U (UU s) p q))"
using cov unfolding covering_space_def by (metis (mono_tags))
then have ope: "⋀s. s ∈ S ⟹ s ∈ (UU s) ∧ openin (top_of_set S) (UU s)"
by blast
have "∃k n i. open k ∧ open n ∧
t ∈ k ∧ y ∈ n ∧ i ∈ S ∧ h ` (({0..1} ∩ k) × (U ∩ n)) ⊆ UU i" if "t ∈ {0..1}" for t
proof -
have hinS: "h (t, y) ∈ S"
using ‹y ∈ U› him that by blast
then have "(t,y) ∈ ({0..1} × U) ∩ h -` UU(h(t, y))"
using ‹y ∈ U› ‹t ∈ {0..1}› by (auto simp: ope)
moreover have ope_01U: "openin (top_of_set ({0..1} × U)) (({0..1} × U) ∩ h -` UU(h(t, y)))"
using hinS ope continuous_on_open_gen [OF him] conth by blast
ultimately obtain V W where opeV: "open V" and "t ∈ {0..1} ∩ V" "t ∈ {0..1} ∩ V"
and opeW: "open W" and "y ∈ U" "y ∈ W"
and VW: "({0..1} ∩ V) × (U ∩ W) ⊆ (({0..1} × U) ∩ h -` UU(h(t, y)))"
by (rule Times_in_interior_subtopology) (auto simp: openin_open)
then show ?thesis
using hinS by blast
qed
then obtain K NN X where
K: "⋀t. t ∈ {0..1} ⟹ open (K t)"
and NN: "⋀t. t ∈ {0..1} ⟹ open (NN t)"
and inUS: "⋀t. t ∈ {0..1} ⟹ t ∈ K t ∧ y ∈ NN t ∧ X t ∈ S"
and him: "⋀t. t ∈ {0..1} ⟹ h ` (({0..1} ∩ K t) × (U ∩ NN t)) ⊆ UU (X t)"
by (metis (mono_tags))
obtain 𝒯 where "𝒯 ⊆ ((λi. K i × NN i)) ` {0..1}" "finite 𝒯" "{0::real..1} × {y} ⊆ ⋃𝒯"
proof (rule compactE)
show "compact ({0::real..1} × {y})"
by (simp add: compact_Times)
show "{0..1} × {y} ⊆ (⋃i∈{0..1}. K i × NN i)"
using K inUS by auto
show "⋀B. B ∈ (λi. K i × NN i) ` {0..1} ⟹ open B"
using K NN by (auto simp: open_Times)
qed blast
then obtain tk where "tk ⊆ {0..1}" "finite tk"
and tk: "{0::real..1} × {y} ⊆ (⋃i ∈ tk. K i × NN i)"
by (metis (no_types, lifting) finite_subset_image)
then have "tk ≠ {}"
by auto
define n where "n = ⋂(NN ` tk)"
have "y ∈ n" "open n"
using inUS NN ‹tk ⊆ {0..1}› ‹finite tk›
by (auto simp: n_def open_INT subset_iff)
obtain δ where "0 < δ" and δ: "⋀T. ⟦T ⊆ {0..1}; diameter T < δ⟧ ⟹ ∃B∈K ` tk. T ⊆ B"
proof (rule Lebesgue_number_lemma [of "{0..1}" "K ` tk"])
show "K ` tk ≠ {}"
using ‹tk ≠ {}› by auto
show "{0..1} ⊆ ⋃(K ` tk)"
using tk by auto
show "⋀B. B ∈ K ` tk ⟹ open B"
using ‹tk ⊆ {0..1}› K by auto
qed auto
obtain N::nat where N: "N > 1 / δ"
using reals_Archimedean2 by blast
then have "N > 0"
using ‹0 < δ› order.asym by force
have *: "∃V k. openin (top_of_set U) V ∧ y ∈ V ∧
continuous_on ({0..of_nat n / N} × V) k ∧
k ` ({0..of_nat n / N} × V) ⊆ C ∧
(∀z∈V. k (0, z) = f z) ∧
(∀z∈{0..of_nat n / N} × V. h z = p (k z))" if "n ≤ N" for n
using that
proof (induction n)
case 0
show ?case
apply (rule_tac x=U in exI)
apply (rule_tac x="f ∘ snd" in exI)
apply (intro conjI ‹y ∈ U› continuous_intros continuous_on_subset [OF contf])
using fim apply (auto simp: heq)
done
next
case (Suc n)
then obtain V k where opeUV: "openin (top_of_set U) V"
and "y ∈ V"
and contk: "continuous_on ({0..n/N} × V) k"
and kim: "k ` ({0..n/N} × V) ⊆ C"
and keq: "⋀z. z ∈ V ⟹ k (0, z) = f z"
and heq: "⋀z. z ∈ {0..n/N} × V ⟹ h z = p (k z)"
using Suc_leD by auto
have "n ≤ N"
using Suc.prems by auto
obtain t where "t ∈ tk" and t: "{n/N .. (1 + real n) / N} ⊆ K t"
proof (rule bexE [OF δ])
show "{n/N .. (1 + real n) / N} ⊆ {0..1}"
using Suc.prems by (auto simp: field_split_simps)
show diameter_less: "diameter {n/N .. (1 + real n) / N} < δ"
using ‹0 < δ› N by (auto simp: field_split_simps)
qed blast
have t01: "t ∈ {0..1}"
using ‹t ∈ tk› ‹tk ⊆ {0..1}› by blast
obtain 𝒱 where 𝒱: "⋃𝒱 = C ∩ p -` UU (X t)"
and opeC: "⋀U. U ∈ 𝒱 ⟹ openin (top_of_set C) U"
and "pairwise disjnt 𝒱"
and homuu: "⋀U. U ∈ 𝒱 ⟹ ∃q. homeomorphism U (UU (X t)) p q"
using inUS [OF t01] UU by meson
have n_div_N_in: "n/N ∈ {n/N .. (1 + real n) / N}"
using N by (auto simp: field_split_simps)
with t have nN_in_kkt: "n/N ∈ K t"
by blast
have "k (n/N, y) ∈ C ∩ p -` UU (X t)"
proof (simp, rule conjI)
show "k (n/N, y) ∈ C"
using ‹y ∈ V› kim keq by force
have "p (k (n/N, y)) = h (n/N, y)"
by (simp add: ‹y ∈ V› heq)
also have "... ∈ h ` (({0..1} ∩ K t) × (U ∩ NN t))"
using ‹y ∈ V› t01 ‹n ≤ N›
by (simp add: nN_in_kkt ‹y ∈ U› inUS field_split_simps)
also have "... ⊆ UU (X t)"
using him t01 by blast
finally show "p (k (n/N, y)) ∈ UU (X t)" .
qed
with 𝒱 have "k (n/N, y) ∈ ⋃𝒱"
by blast
then obtain W where W: "k (n/N, y) ∈ W" and "W ∈ 𝒱"
by blast
then obtain p' where opeC': "openin (top_of_set C) W"
and hom': "homeomorphism W (UU (X t)) p p'"
using homuu opeC by blast
then have "W ⊆ C"
using openin_imp_subset by blast
define W' where "W' = UU(X t)"
have opeVW: "openin (top_of_set V) (V ∩ (k ∘ Pair (n / N)) -` W)"
proof (rule continuous_openin_preimage [OF _ _ opeC'])
show "continuous_on V (k ∘ Pair (n/N))"
by (intro continuous_intros continuous_on_subset [OF contk], auto)
show "(k ∘ Pair (n/N)) ∈ V → C"
using kim by (auto simp: ‹y ∈ V› W)
qed
obtain N' where opeUN': "openin (top_of_set U) N'"
and "y ∈ N'" and kimw: "k ` ({(n/N)} × N') ⊆ W"
proof
show "openin (top_of_set U) (V ∩ (k ∘ Pair (n/N)) -` W)"
using opeUV opeVW openin_trans by blast
qed (use ‹y ∈ V› W in ‹force+›)
obtain Q Q' where opeUQ: "openin (top_of_set U) Q"
and cloUQ': "closedin (top_of_set U) Q'"
and "y ∈ Q" "Q ⊆ Q'"
and Q': "Q' ⊆ (U ∩ NN(t)) ∩ N' ∩ V"
proof -
obtain VO VX where "open VO" "open VX" and VO: "V = U ∩ VO" and VX: "N' = U ∩ VX"
using opeUV opeUN' by (auto simp: openin_open)
then have "open (NN(t) ∩ VO ∩ VX)"
using NN t01 by blast
then obtain e where "e > 0" and e: "cball y e ⊆ NN(t) ∩ VO ∩ VX"
by (metis Int_iff ‹N' = U ∩ VX› ‹V = U ∩ VO› ‹y ∈ N'› ‹y ∈ V› inUS open_contains_cball t01)
show ?thesis
proof
show "openin (top_of_set U) (U ∩ ball y e)"
by blast
show "closedin (top_of_set U) (U ∩ cball y e)"
using e by (auto simp: closedin_closed)
qed (use ‹y ∈ U› ‹e > 0› VO VX e in auto)
qed
then have "y ∈ Q'" "Q ⊆ (U ∩ NN(t)) ∩ N' ∩ V"
by blast+
have neq: "{0..n/N} ∪ {n/N..(1 + real n) / N} = {0..(1 + real n) / N}"
apply (auto simp: field_split_simps)
by (metis not_less of_nat_0_le_iff of_nat_0_less_iff order_trans zero_le_mult_iff)
then have neqQ': "{0..n/N} × Q' ∪ {n/N..(1 + real n) / N} × Q' = {0..(1 + real n) / N} × Q'"
by blast
have cont: "continuous_on ({0..(1 + real n) / N} × Q') (λx. if x ∈ {0..n/N} × Q' then k x else (p' ∘ h) x)"
unfolding neqQ' [symmetric]
proof (rule continuous_on_cases_local, simp_all add: neqQ' del: comp_apply)
have "∃T. closed T ∧ {0..n/N} × Q' = {0..(1+n)/N} × Q' ∩ T"
using n_div_N_in
by (rule_tac x="{0 .. n/N} × UNIV" in exI) (auto simp: closed_Times)
then show "closedin (top_of_set ({0..(1 + real n) / N} × Q')) ({0..n/N} × Q')"
by (simp add: closedin_closed)
have "∃T. closed T ∧ {n/N..(1+n)/N} × Q' = {0..(1+n)/N} × Q' ∩ T"
by (rule_tac x="{n/N..(1+n)/N} × UNIV" in exI) (auto simp: closed_Times order_trans [rotated])
then show "closedin (top_of_set ({0..(1 + real n) / N} × Q')) ({n/N..(1 + real n) / N} × Q')"
by (simp add: closedin_closed)
show "continuous_on ({0..n/N} × Q') k"
using Q' by (auto intro: continuous_on_subset [OF contk])
have "continuous_on ({n/N..(1 + real n) / N} × Q') h"
proof (rule continuous_on_subset [OF conth])
show "{n/N..(1 + real n) / N} × Q' ⊆ {0..1} × U"
proof (clarsimp, intro conjI)
fix a b
assume "b ∈ Q'" and a: "n/N ≤ a" "a ≤ (1 + real n) / N"
have "0 ≤ n/N" "(1 + real n) / N ≤ 1"
using a Suc.prems by (auto simp: divide_simps)
with a show "0 ≤ a" "a ≤ 1"
by linarith+
show "b ∈ U"
using ‹b ∈ Q'› cloUQ' closedin_imp_subset by blast
qed
qed
moreover have "continuous_on (h ` ({n/N..(1 + real n) / N} × Q')) p'"
proof (rule continuous_on_subset [OF homeomorphism_cont2 [OF hom']])
have "h ` ({n/N..(1 + real n) / N} × Q') ⊆ h ` (({0..1} ∩ K t) × (U ∩ NN t))"
proof (rule image_mono)
show "{n/N..(1 + real n) / N} × Q' ⊆ ({0..1} ∩ K t) × (U ∩ NN t)"
proof (clarsimp, intro conjI)
fix a::real and b
assume "b ∈ Q'" "n/N ≤ a" "a ≤ (1 + real n) / N"
show "0 ≤ a"
by (meson ‹n/N ≤ a› divide_nonneg_nonneg of_nat_0_le_iff order_trans)
show "a ≤ 1"
using Suc.prems ‹a ≤ (1 + real n) / N› order_trans by force
show "a ∈ K t"
using ‹a ≤ (1 + real n) / N› ‹n/N ≤ a› t by auto
show "b ∈ U"
using ‹b ∈ Q'› cloUQ' closedin_imp_subset by blast
show "b ∈ NN t"
using Q' ‹b ∈ Q'› by auto
qed
qed
with him show "h ` ({n/N..(1 + real n) / N} × Q') ⊆ UU (X t)"
using t01 by blast
qed
ultimately show "continuous_on ({n/N..(1 + real n) / N} × Q') (p' ∘ h)"
by (rule continuous_on_compose)
have "k (n/N, b) = p' (h (n/N, b))" if "b ∈ Q'" for b
proof -
have "k (n/N, b) ∈ W"
using that Q' kimw by force
then have "k (n/N, b) = p' (p (k (n/N, b)))"
by (simp add: homeomorphism_apply1 [OF hom'])
then show ?thesis
using Q' that by (force simp: heq)
qed
then show "⋀x. x ∈ {n/N..(1 + real n) / N} × Q' ∧
x ∈ {0..n/N} × Q' ⟹ k x = (p' ∘ h) x"
by auto
qed
have h_in_UU: "h (x, y) ∈ UU (X t)" if "y ∈ Q" "¬ x ≤ n/N" "0 ≤ x" "x ≤ (1 + real n) / N" for x y
proof -
have "x ≤ 1"
using Suc.prems that order_trans by force
moreover have "x ∈ K t"
by (meson atLeastAtMost_iff le_less not_le subset_eq t that)
moreover have "y ∈ U"
using ‹y ∈ Q› opeUQ openin_imp_subset by blast
moreover have "y ∈ NN t"
using Q' ‹Q ⊆ Q'› ‹y ∈ Q› by auto
ultimately have "(x, y) ∈ (({0..1} ∩ K t) × (U ∩ NN t))"
using that by auto
then have "h (x, y) ∈ h ` (({0..1} ∩ K t) × (U ∩ NN t))"
by blast
also have "... ⊆ UU (X t)"
by (metis him t01)
finally show ?thesis .
qed
let ?k = "(λx. if x ∈ {0..n/N} × Q' then k x else (p' ∘ h) x)"
show ?case
proof (intro exI conjI)
show "continuous_on ({0..real (Suc n) / N} × Q) ?k"
using ‹Q ⊆ Q'› by (auto intro: continuous_on_subset [OF cont])
have "⋀x y. ⟦x ≤ n/N; y ∈ Q'; 0 ≤ x⟧ ⟹ k (x, y) ∈ C"
using kim Q' by force
moreover have "p' (h (x, y)) ∈ C" if "y ∈ Q" "¬ x ≤ n/N" "0 ≤ x" "x ≤ (1 + real n) / N" for x y
proof (rule ‹W ⊆ C› [THEN subsetD])
show "p' (h (x, y)) ∈ W"
using homeomorphism_image2 [OF hom', symmetric] h_in_UU Q' ‹Q ⊆ Q'› ‹W ⊆ C› that by auto
qed
ultimately show "?k ` ({0..real (Suc n) / N} × Q) ⊆ C"
using Q' ‹Q ⊆ Q'› by force
show "∀z∈Q. ?k (0, z) = f z"
using Q' keq ‹Q ⊆ Q'› by auto
show "∀z ∈ {0..real (Suc n) / N} × Q. h z = p(?k z)"
using ‹Q ⊆ U ∩ NN t ∩ N' ∩ V› heq Q' ‹Q ⊆ Q'›
by (auto simp: homeomorphism_apply2 [OF hom'] dest: h_in_UU)
qed (auto simp: ‹y ∈ Q› opeUQ)
qed
show ?thesis
using *[OF order_refl] N ‹0 < δ› by (simp add: split: if_split_asm)
qed
then obtain V fs where opeV: "⋀y. y ∈ U ⟹ openin (top_of_set U) (V y)"
and V: "⋀y. y ∈ U ⟹ y ∈ V y"
and contfs: "⋀y. y ∈ U ⟹ continuous_on ({0..1} × V y) (fs y)"
and *: "⋀y. y ∈ U ⟹ (fs y) ` ({0..1} × V y) ⊆ C ∧
(∀z ∈ V y. fs y (0, z) = f z) ∧
(∀z ∈ {0..1} × V y. h z = p(fs y z))"
by (metis (mono_tags))
then have VU: "⋀y. y ∈ U ⟹ V y ⊆ U"
by (meson openin_imp_subset)
obtain k where contk: "continuous_on ({0..1} × U) k"
and k: "⋀x i. ⟦i ∈ U; x ∈ {0..1} × U ∩ {0..1} × V i⟧ ⟹ k x = fs i x"
proof (rule pasting_lemma_exists)
let ?X = "top_of_set ({0..1::real} × U)"
show "topspace ?X ⊆ (⋃i∈U. {0..1} × V i)"
using V by force
show "⋀i. i ∈ U ⟹ openin (top_of_set ({0..1} × U)) ({0..1} × V i)"
by (simp add: Abstract_Topology.openin_Times opeV)
show "⋀i. i ∈ U ⟹ continuous_map
(subtopology (top_of_set ({0..1} × U)) ({0..1} × V i)) euclidean (fs i)"
by (metis contfs subtopology_subtopology continuous_map_iff_continuous Times_Int_Times VU inf.absorb_iff2 inf.idem)
show "fs i x = fs j x" if "i ∈ U" "j ∈ U" and x: "x ∈ topspace ?X ∩ {0..1} × V i ∩ {0..1} × V j"
for i j x
proof -
obtain u y where "x = (u, y)" "y ∈ V i" "y ∈ V j" "0 ≤ u" "u ≤ 1"
using x by auto
show ?thesis
proof (rule covering_space_lift_unique [OF cov, of _ "(0,y)" _ "{0..1} × {y}" h])
show "fs i (0, y) = fs j (0, y)"
using*V by (simp add: ‹y ∈ V i› ‹y ∈ V j› that)
show conth_y: "continuous_on ({0..1} × {y}) h"
using VU ‹y ∈ V j› that by (auto intro: continuous_on_subset [OF conth])
show "h ∈ ({0..1} × {y}) → S"
using ‹y ∈ V i› assms(3) VU that by fastforce
show "continuous_on ({0..1} × {y}) (fs i)"
using continuous_on_subset [OF contfs] ‹i ∈ U›
by (simp add: ‹y ∈ V i› subset_iff)
show "fs i ∈ ({0..1} × {y}) → C"
using "*" ‹y ∈ V i› ‹i ∈ U› by fastforce
show "⋀x. x ∈ {0..1} × {y} ⟹ h x = p (fs i x)"
using "*" ‹y ∈ V i› ‹i ∈ U› by blast
show "continuous_on ({0..1} × {y}) (fs j)"
using continuous_on_subset [OF contfs] ‹j ∈ U›
by (simp add: ‹y ∈ V j› subset_iff)
show "fs j ∈ ({0..1} × {y}) → C"
using "*" ‹y ∈ V j› ‹j ∈ U› by fastforce
show "⋀x. x ∈ {0..1} × {y} ⟹ h x = p (fs j x)"
using "*" ‹y ∈ V j› ‹j ∈ U› by blast
show "connected ({0..1::real} × {y})"
using connected_Icc connected_Times connected_sing by blast
show "(0, y) ∈ {0..1::real} × {y}"
by force
show "x ∈ {0..1} × {y}"
using ‹x = (u, y)› x by blast
qed
qed
qed force
show ?thesis
proof
show "k ∈ ({0..1} × U) → C"
using V*k VU by fastforce
show "⋀y. y ∈ U ⟹ k (0, y) = f y"
by (simp add: V*k)
show "⋀z. z ∈ {0..1} × U ⟹ h z = p (k z)"
using V*k by auto
qed (auto simp: contk)
qed
corollary covering_space_lift_homotopy_alt:
fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
and h :: "'c::real_normed_vector × real ⇒ 'b"
assumes cov: "covering_space C p S"
and conth: "continuous_on (U × {0..1}) h"
and him: "h ∈ (U × {0..1}) → S"
and heq: "⋀y. y ∈ U ⟹ h (y,0) = p(f y)"
and contf: "continuous_on U f" and fim: "f ∈ U → C"
obtains k where "continuous_on (U × {0..1}) k"
"k ∈ (U × {0..1}) → C"
"⋀y. y ∈ U ⟹ k(y, 0) = f y"
"⋀z. z ∈ U × {0..1} ⟹ h z = p(k z)"
proof -
have "continuous_on ({0..1} × U) (h ∘ (λz. (snd z, fst z)))"
by (intro continuous_intros continuous_on_subset [OF conth]) auto
then obtain k where contk: "continuous_on ({0..1} × U) k"
and kim: "k ` ({0..1} × U) ⊆ C"
and k0: "⋀y. y ∈ U ⟹ k(0, y) = f y"
and heqp: "⋀z. z ∈ {0..1} × U ⟹ (h ∘ (λz. Pair (snd z) (fst z))) z = p(k z)"
apply (rule covering_space_lift_homotopy [OF cov _ _ _ contf fim])
using him by (auto simp: contf heq)
show ?thesis
proof
show "continuous_on (U × {0..1}) (k ∘ (λz. (snd z, fst z)))"
by (intro continuous_intros continuous_on_subset [OF contk]) auto
qed (use kim heqp in ‹auto simp: k0›)
qed
corollary covering_space_lift_homotopic_function:
fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector" and g:: "'c::real_normed_vector ⇒ 'a"
assumes cov: "covering_space C p S"
and contg: "continuous_on U g"
and gim: "g ∈ U → C"
and pgeq: "⋀y. y ∈ U ⟹ p(g y) = f y"
and hom: "homotopic_with_canon (λx. True) U S f f'"
obtains g' where "continuous_on U g'" "image g' U ⊆ C" "⋀y. y ∈ U ⟹ p(g' y) = f' y"
proof -
obtain h where conth: "continuous_on ({0..1::real} × U) h"
and him: "h ∈ ({0..1} × U) → S"
and h0: "⋀x. h(0, x) = f x"
and h1: "⋀x. h(1, x) = f' x"
using hom by (auto simp: homotopic_with_def)
have "⋀y. y ∈ U ⟹ h (0, y) = p (g y)"
by (simp add: h0 pgeq)
then obtain k where contk: "continuous_on ({0..1} × U) k"
and kim: "k ` ({0..1} × U) ⊆ C"
and k0: "⋀y. y ∈ U ⟹ k(0, y) = g y"
and heq: "⋀z. z ∈ {0..1} × U ⟹ h z = p(k z)"
using covering_space_lift_homotopy [OF cov conth him _ contg gim] by (metis image_subset_iff_funcset)
show ?thesis
proof
show "continuous_on U (k ∘ Pair 1)"
by (meson contk atLeastAtMost_iff continuous_on_o_Pair order_refl zero_le_one)
show "(k ∘ Pair 1) ` U ⊆ C"
using kim by auto
show "⋀y. y ∈ U ⟹ p ((k ∘ Pair 1) y) = f' y"
by (auto simp: h1 heq [symmetric])
qed
qed
corollary covering_space_lift_inessential_function:
fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector" and U :: "'c::real_normed_vector set"
assumes cov: "covering_space C p S"
and hom: "homotopic_with_canon (λx. True) U S f (λx. a)"
obtains g where "continuous_on U g" "g ` U ⊆ C" "⋀y. y ∈ U ⟹ p(g y) = f y"
proof (cases "U = {}")
case True
then show ?thesis
using that continuous_on_empty by blast
next
case False
then obtain b where b: "b ∈ C" "p b = a"
using covering_space_imp_surjective [OF cov] homotopic_with_imp_subset2 [OF hom]
by auto
then have gim: "(λy. b) ∈ U → C"
by blast
show ?thesis
proof (rule covering_space_lift_homotopic_function [OF cov continuous_on_const gim])
show "⋀y. y ∈ U ⟹ p b = a"
using b by auto
qed (use that homotopic_with_symD [OF hom] in auto)
qed
subsection‹ Lifting of general functions to covering space›
proposition covering_space_lift_path_strong:
fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
and f :: "'c::real_normed_vector ⇒ 'b"
assumes cov: "covering_space C p S" and "a ∈ C"
and "path g" and pag: "path_image g ⊆ S" and pas: "pathstart g = p a"
obtains h where "path h" "path_image h ⊆ C" "pathstart h = a"
and "⋀t. t ∈ {0..1} ⟹ p(h t) = g t"
proof -
obtain k:: "real × 'c ⇒ 'a"
where contk: "continuous_on ({0..1} × {undefined}) k"
and kim: "k ` ({0..1} × {undefined}) ⊆ C"
and k0: "k (0, undefined) = a"
and pk: "⋀z. z ∈ {0..1} × {undefined} ⟹ p(k z) = (g ∘ fst) z"
proof (rule covering_space_lift_homotopy [OF cov, of "{undefined}" "g ∘ fst"])
show "continuous_on ({0..1::real} × {undefined::'c}) (g ∘ fst)"
using ‹path g› by (intro continuous_intros) (simp add: path_def)
show "(g ∘ fst) ∈ ({0..1} × {undefined}) → S"
using pag by (auto simp: path_image_def)
show "(g ∘ fst) (0, y) = p a" if "y ∈ {undefined}" for y::'c
by (metis comp_def fst_conv pas pathstart_def)
qed (use assms in auto)
show ?thesis
proof
show "path (k ∘ (λt. Pair t undefined))"
unfolding path_def
by (intro continuous_on_compose continuous_intros continuous_on_subset [OF contk]) auto
show "path_image (k ∘ (λt. (t, undefined))) ⊆ C"
using kim by (auto simp: path_image_def)
show "pathstart (k ∘ (λt. (t, undefined))) = a"
by (auto simp: pathstart_def k0)
show "⋀t. t ∈ {0..1} ⟹ p ((k ∘ (λt. (t, undefined))) t) = g t"
by (auto simp: pk)
qed
qed
corollary covering_space_lift_path:
fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
assumes cov: "covering_space C p S" and "path g" and pig: "path_image g ⊆ S"
obtains h where "path h" "path_image h ⊆ C" "⋀t. t ∈ {0..1} ⟹ p(h t) = g t"
proof -
obtain a where "a ∈ C" "pathstart g = p a"
by (metis pig cov covering_space_imp_surjective imageE pathstart_in_path_image subsetCE)
show ?thesis
using covering_space_lift_path_strong [OF cov ‹a ∈ C› ‹path g› pig]
by (metis ‹pathstart g = p a› that)
qed
proposition covering_space_lift_homotopic_paths:
fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
assumes cov: "covering_space C p S"
and "path g1" and pig1: "path_image g1 ⊆ S"
and "path g2" and pig2: "path_image g2 ⊆ S"
and hom: "homotopic_paths S g1 g2"
and "path h1" and pih1: "path_image h1 ⊆ C" and ph1: "⋀t. t ∈ {0..1} ⟹ p(h1 t) = g1 t"
and "path h2" and pih2: "path_image h2 ⊆ C" and ph2: "⋀t. t ∈ {0..1} ⟹ p(h2 t) = g2 t"
and h1h2: "pathstart h1 = pathstart h2"
shows "homotopic_paths C h1 h2"
proof -
obtain h :: "real × real ⇒ 'b"
where conth: "continuous_on ({0..1} × {0..1}) h"
and him: "h ∈ ({0..1} × {0..1}) → S"
and h0: "⋀x. h (0, x) = g1 x" and h1: "⋀x. h (1, x) = g2 x"
and heq0: "⋀t. t ∈ {0..1} ⟹ h (t, 0) = g1 0"
and heq1: "⋀t. t ∈ {0..1} ⟹ h (t, 1) = g1 1"
using hom by (auto simp: homotopic_paths_def homotopic_with_def pathstart_def pathfinish_def image_subset_iff_funcset)
obtain k where contk: "continuous_on ({0..1} × {0..1}) k"
and kim: "k ∈ ({0..1} × {0..1}) → C"
and kh2: "⋀y. y ∈ {0..1} ⟹ k (y, 0) = h2 0"
and hpk: "⋀z. z ∈ {0..1} × {0..1} ⟹ h z = p (k z)"
proof (rule covering_space_lift_homotopy_alt [OF cov conth him])
show "⋀y. y ∈ {0..1} ⟹ h (y, 0) = p (h2 0)"
by (metis atLeastAtMost_iff h1h2 heq0 order_refl pathstart_def ph1 zero_le_one)
qed (use path_image_def pih2 in ‹fastforce+›)
have contg1: "continuous_on {0..1} g1" and contg2: "continuous_on {0..1} g2"
using ‹path g1› ‹path g2› path_def by blast+
have g1im: "g1 ∈ {0..1} → S" and g2im: "g2 ∈ {0..1} → S"
using path_image_def pig1 pig2 by auto
have conth1: "continuous_on {0..1} h1" and conth2: "continuous_on {0..1} h2"
using ‹path h1› ‹path h2› path_def by blast+
have h1im: "h1 ∈ {0..1} → C" and h2im: "h2 ∈ {0..1} → C"
using path_image_def pih1 pih2 by auto
show ?thesis
unfolding homotopic_paths pathstart_def pathfinish_def
proof (intro exI conjI ballI)
show keqh1: "k(0, x) = h1 x" if "x ∈ {0..1}" for x
proof (rule covering_space_lift_unique [OF cov _ contg1 g1im])
show "k (0,0) = h1 0"
by (metis atLeastAtMost_iff h1h2 kh2 order_refl pathstart_def zero_le_one)
show "continuous_on {0..1} (λa. k (0, a))"
by (intro continuous_intros continuous_on_compose2 [OF contk]) auto
show "⋀x. x ∈ {0..1} ⟹ g1 x = p (k (0, x))"
by (metis atLeastAtMost_iff h0 hpk zero_le_one mem_Sigma_iff order_refl)
qed (use conth1 h1im kim that in ‹auto simp: ph1›)
show "k(1, x) = h2 x" if "x ∈ {0..1}" for x
proof (rule covering_space_lift_unique [OF cov _ contg2 g2im])
show "k (1,0) = h2 0"
by (metis atLeastAtMost_iff kh2 order_refl zero_le_one)
show "continuous_on {0..1} (λa. k (1, a))"
by (intro continuous_intros continuous_on_compose2 [OF contk]) auto
show "⋀x. x ∈ {0..1} ⟹ g2 x = p (k (1, x))"
by (metis atLeastAtMost_iff h1 hpk mem_Sigma_iff order_refl zero_le_one)
qed (use conth2 h2im kim that in ‹auto simp: ph2›)
show "⋀t. t ∈ {0..1} ⟹ (k ∘ Pair t) 0 = h1 0"
by (metis comp_apply h1h2 kh2 pathstart_def)
show "(k ∘ Pair t) 1 = h1 1" if "t ∈ {0..1}" for t
proof (rule covering_space_lift_unique
[OF cov, of "λa. (k ∘ Pair a) 1" 0 "λa. h1 1" "{0..1}" "λx. g1 1"])
show "(k ∘ Pair 0) 1 = h1 1"
using keqh1 by auto
show "continuous_on {0..1} (λa. (k ∘ Pair a) 1)"
by (auto intro!: continuous_intros continuous_on_compose2 [OF contk])
show "⋀x. x ∈ {0..1} ⟹ g1 1 = p ((k ∘ Pair x) 1)"
using heq1 hpk by auto
qed (use contk kim g1im h1im that in ‹auto simp: ph1›)
qed (use contk kim in auto)
qed
corollary covering_space_monodromy:
fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
assumes cov: "covering_space C p S"
and "path g1" and pig1: "path_image g1 ⊆ S"
and "path g2" and pig2: "path_image g2 ⊆ S"
and hom: "homotopic_paths S g1 g2"
and "path h1" and pih1: "path_image h1 ⊆ C" and ph1: "⋀t. t ∈ {0..1} ⟹ p(h1 t) = g1 t"
and "path h2" and pih2: "path_image h2 ⊆ C" and ph2: "⋀t. t ∈ {0..1} ⟹ p(h2 t) = g2 t"
and h1h2: "pathstart h1 = pathstart h2"
shows "pathfinish h1 = pathfinish h2"
using covering_space_lift_homotopic_paths [OF assms] homotopic_paths_imp_pathfinish
by blast
corollary covering_space_lift_homotopic_path:
fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
assumes cov: "covering_space C p S"
and hom: "homotopic_paths S f f'"
and "path g" and pig: "path_image g ⊆ C"
and a: "pathstart g = a" and b: "pathfinish g = b"
and pgeq: "⋀t. t ∈ {0..1} ⟹ p(g t) = f t"
obtains g' where "path g'" "path_image g' ⊆ C"
"pathstart g' = a" "pathfinish g' = b" "⋀t. t ∈ {0..1} ⟹ p(g' t) = f' t"
proof (rule covering_space_lift_path_strong [OF cov, of a f'])
show "a ∈ C"
using a pig by auto
show "path f'" "path_image f' ⊆ S"
using hom homotopic_paths_imp_path homotopic_paths_imp_subset by blast+
show "pathstart f' = p a"
by (metis a atLeastAtMost_iff hom homotopic_paths_imp_pathstart order_refl pathstart_def pgeq zero_le_one)
qed (metis (mono_tags, lifting) assms cov covering_space_monodromy hom homotopic_paths_imp_path homotopic_paths_imp_subset pgeq pig)
proposition covering_space_lift_general:
fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
and f :: "'c::real_normed_vector ⇒ 'b"
assumes cov: "covering_space C p S" and "a ∈ C" "z ∈ U"
and U: "path_connected U" "locally path_connected U"
and contf: "continuous_on U f" and fim: "f ∈ U → S"
and feq: "f z = p a"
and hom: "⋀r. ⟦path r; path_image r ⊆ U; pathstart r = z; pathfinish r = z⟧
⟹ ∃q. path q ∧ path_image q ⊆ C ∧
pathstart q = a ∧ pathfinish q = a ∧
homotopic_paths S (f ∘ r) (p ∘ q)"
obtains g where "continuous_on U g" "g ∈ U → C" "g z = a" "⋀y. y ∈ U ⟹ p(g y) = f y"
proof -
have *: "∃g h. path g ∧ path_image g ⊆ U ∧
pathstart g = z ∧ pathfinish g = y ∧
path h ∧ path_image h ⊆ C ∧ pathstart h = a ∧
(∀t ∈ {0..1}. p(h t) = f(g t))"
if "y ∈ U" for y
proof -
obtain g where "path g" "path_image g ⊆ U" and pastg: "pathstart g = z"
and pafig: "pathfinish g = y"
using U ‹z ∈ U› ‹y ∈ U› by (force simp: path_connected_def)
obtain h where "path h" "path_image h ⊆ C" "pathstart h = a"
and "⋀t. t ∈ {0..1} ⟹ p(h t) = (f ∘ g) t"
proof (rule covering_space_lift_path_strong [OF cov ‹a ∈ C›])
show "path (f ∘ g)"
using ‹path g› ‹path_image g ⊆ U› contf continuous_on_subset path_continuous_image by blast
show "path_image (f ∘ g) ⊆ S"
by (metis ‹path_image g ⊆ U› fim image_mono path_image_compose subset_trans image_subset_iff_funcset)
show "pathstart (f ∘ g) = p a"
by (simp add: feq pastg pathstart_compose)
qed auto
then show ?thesis
by (metis ‹path g› ‹path_image g ⊆ U› comp_apply pafig pastg)
qed
have "∃l. ∀g h. path g ∧ path_image g ⊆ U ∧ pathstart g = z ∧ pathfinish g = y ∧
path h ∧ path_image h ⊆ C ∧ pathstart h = a ∧
(∀t ∈ {0..1}. p(h t) = f(g t)) ⟶ pathfinish h = l" for y
proof -
have "pathfinish h = pathfinish h'"
if g: "path g" "path_image g ⊆ U" "pathstart g = z" "pathfinish g = y"
and h: "path h" "path_image h ⊆ C" "pathstart h = a"
and phg: "⋀t. t ∈ {0..1} ⟹ p(h t) = f(g t)"
and g': "path g'" "path_image g' ⊆ U" "pathstart g' = z" "pathfinish g' = y"
and h': "path h'" "path_image h' ⊆ C" "pathstart h' = a"
and phg': "⋀t. t ∈ {0..1} ⟹ p(h' t) = f(g' t)"
for g h g' h'
proof -
obtain q where "path q" and piq: "path_image q ⊆ C" and pastq: "pathstart q = a" and pafiq: "pathfinish q = a"
and homS: "homotopic_paths S (f ∘ g +++ reversepath g') (p ∘ q)"
using g g' hom [of "g +++ reversepath g'"] by (auto simp: subset_path_image_join)
have papq: "path (p ∘ q)"
using homS homotopic_paths_imp_path by blast
have pipq: "path_image (p ∘ q) ⊆ S"
using homS homotopic_paths_imp_subset by blast
obtain q' where "path q'" "path_image q' ⊆ C"
and "pathstart q' = pathstart q" "pathfinish q' = pathfinish q"
and pq'_eq: "⋀t. t ∈ {0..1} ⟹ p (q' t) = (f ∘ g +++ reversepath g') t"
using covering_space_lift_homotopic_path [OF cov homotopic_paths_sym [OF homS] ‹path q› piq refl refl]
by auto
have "q' t = (h ∘ (*⇩R) 2) t" if "0 ≤ t" "t ≤ 1/2" for t
proof (rule covering_space_lift_unique [OF cov, of q' 0 "h ∘ (*⇩R) 2" "{0..1/2}" "f ∘ g ∘ (*⇩R) 2" t])
show "q' 0 = (h ∘ (*⇩R) 2) 0"
by (metis ‹pathstart q' = pathstart q› comp_def h(3) pastq pathstart_def pth_4(2))
show "continuous_on {0..1/2} (f ∘ g ∘ (*⇩R) 2)"
proof (intro continuous_intros continuous_on_path [OF ‹path g›] continuous_on_subset [OF contf])
show "g ` (*⇩R) 2 ` {0..1/2} ⊆ U"
using g path_image_def by fastforce
qed auto
show "(f ∘ g ∘ (*⇩R) 2) ∈ {0..1/2} → S"
using g(2) fim by (fastforce simp: path_image_def image_subset_iff_funcset)
show "(h ∘ (*⇩R) 2) ∈ {0..1/2} → C"
using h path_image_def by fastforce
show "q' ∈ {0..1/2} → C"
using ‹path_image q' ⊆ C› path_image_def by fastforce
show "⋀x. x ∈ {0..1/2} ⟹ (f ∘ g ∘ (*⇩R) 2) x = p (q' x)"
by (auto simp: joinpaths_def pq'_eq)
show "⋀x. x ∈ {0..1/2} ⟹ (f ∘ g ∘ (*⇩R) 2) x = p ((h ∘ (*⇩R) 2) x)"
by (simp add: phg)
show "continuous_on {0..1/2} q'"
by (simp add: continuous_on_path ‹path q'›)
show "continuous_on {0..1/2} (h ∘ (*⇩R) 2)"
by (intro continuous_intros continuous_on_path [OF ‹path h›]) auto
qed (use that in auto)
moreover have "q' t = (reversepath h' ∘ (λt. 2 *⇩R t - 1)) t" if "1/2 < t" "t ≤ 1" for t
proof (rule covering_space_lift_unique [OF cov, of q' 1 "reversepath h' ∘ (λt. 2 *⇩R t - 1)" "{1/2<..1}" "f ∘ reversepath g' ∘ (λt. 2 *⇩R t - 1)" t])
show "q' 1 = (reversepath h' ∘ (λt. 2 *⇩R t - 1)) 1"
using h' ‹pathfinish q' = pathfinish q› pafiq
by (simp add: pathstart_def pathfinish_def reversepath_def)
show "continuous_on {1/2<..1} (f ∘ reversepath g' ∘ (λt. 2 *⇩R t - 1))"
proof (intro continuous_intros continuous_on_path ‹path g'› continuous_on_subset [OF contf])
show "reversepath g' ` (λt. 2 *⇩R t - 1) ` {1/2<..1} ⊆ U"
using g' by (auto simp: path_image_def reversepath_def)
qed (use g' in auto)
show "(f ∘ reversepath g' ∘ (λt. 2 *⇩R t - 1)) ∈ {1/2<..1} → S"
using g'(2) path_image_def fim by (auto simp: image_subset_iff path_image_def reversepath_def)
show "q' ∈ {1/2<..1} → C"
using ‹path_image q' ⊆ C› path_image_def by fastforce
show "(reversepath h' ∘ (λt. 2 *⇩R t - 1)) ∈ {1/2<..1} → C"
using h' by (simp add: path_image_def reversepath_def subset_eq)
show "⋀x. x ∈ {1/2<..1} ⟹ (f ∘ reversepath g' ∘ (λt. 2 *⇩R t - 1)) x = p (q' x)"
by (auto simp: joinpaths_def pq'_eq)
show "⋀x. x ∈ {1/2<..1} ⟹
(f ∘ reversepath g' ∘ (λt. 2 *⇩R t - 1)) x = p ((reversepath h' ∘ (λt. 2 *⇩R t - 1)) x)"
by (simp add: phg' reversepath_def)
show "continuous_on {1/2<..1} q'"
by (auto intro: continuous_on_path [OF ‹path q'›])
show "continuous_on {1/2<..1} (reversepath h' ∘ (λt. 2 *⇩R t - 1))"
by (intro continuous_intros continuous_on_path ‹path h'›) (use h' in auto)
qed (use that in auto)
ultimately have "q' t = (h +++ reversepath h') t" if "0 ≤ t" "t ≤ 1" for t
using that by (simp add: joinpaths_def)
then have "path(h +++ reversepath h')"
by (auto intro: path_eq [OF ‹path q'›])
then show ?thesis
by (auto simp: ‹path h› ‹path h'›)
qed
then show ?thesis by metis
qed
then obtain l :: "'c ⇒ 'a"
where l: "⋀y g h. ⟦path g; path_image g ⊆ U; pathstart g = z; pathfinish g = y;
path h; path_image h ⊆ C; pathstart h = a;
⋀t. t ∈ {0..1} ⟹ p(h t) = f(g t)⟧ ⟹ pathfinish h = l y"
by metis
show ?thesis
proof
show pleq: "p (l y) = f y" if "y ∈ U" for y
using*[OF ‹y ∈ U›] by (metis l atLeastAtMost_iff order_refl pathfinish_def zero_le_one)
show "l z = a"
using l [of "linepath z z" z "linepath a a"] by (auto simp: assms)
show LC: "l ∈ U → C"
by (clarify dest!: *) (metis (full_types) l pathfinish_in_path_image subsetCE)
have "∃T. openin (top_of_set U) T ∧ y ∈ T ∧ T ⊆ U ∩ l -` X"
if X: "openin (top_of_set C) X" and "y ∈ U" "l y ∈ X" for X y
proof -
have "X ⊆ C"
using X openin_euclidean_subtopology_iff by blast
have "f y ∈ S"
using fim ‹y ∈ U› by blast
then obtain W 𝒱
where WV: "f y ∈ W ∧ openin (top_of_set S) W ∧
(⋃𝒱 = C ∩ p -` W ∧
(∀U ∈ 𝒱. openin (top_of_set C) U) ∧
pairwise disjnt 𝒱 ∧
(∀U ∈ 𝒱. ∃q. homeomorphism U W p q))"
using cov by (force simp: covering_space_def)
then have "l y ∈ ⋃𝒱"
using ‹X ⊆ C› pleq that by auto
then obtain W' where "l y ∈ W'" and "W' ∈ 𝒱"
by blast
with WV obtain p' where opeCW': "openin (top_of_set C) W'"
and homUW': "homeomorphism W' W p p'"
by blast
then have contp': "continuous_on W p'" and p'im: "p' ` W ⊆ W'"
using homUW' homeomorphism_image2 homeomorphism_cont2 by fastforce+
obtain V where "y ∈ V" "y ∈ U" and fimW: "f ` V ⊆ W" "V ⊆ U"
and "path_connected V" and opeUV: "openin (top_of_set U) V"
proof -
have "openin (top_of_set U) (U ∩ f -` W)"
using WV contf continuous_on_open_gen fim by auto
then obtain UO where "openin (top_of_set U) UO ∧ path_connected UO ∧ y ∈ UO ∧ UO ⊆ U ∩ f -` W"
using U WV ‹y ∈ U› unfolding locally_path_connected by (meson IntI vimage_eq)
then show ?thesis
by (meson ‹y ∈ U› image_subset_iff_subset_vimage le_inf_iff that)
qed
have "W' ⊆ C" "W ⊆ S"
using opeCW' WV openin_imp_subset by auto
have p'im: "p' ` W ⊆ W'"
using homUW' homeomorphism_image2 by fastforce
show ?thesis
proof (intro exI conjI)
have "openin (top_of_set S) (W ∩ p' -` (W' ∩ X))"
proof (rule openin_trans)
show "openin (top_of_set W) (W ∩ p' -` (W' ∩ X))"
using X ‹W' ⊆ C›
by (metis continuous_on_open contp' homUW' homeomorphism_image2 inf.assoc inf.orderE openin_open)
show "openin (top_of_set S) W"
using WV by blast
qed
then show "openin (top_of_set U) (V ∩ (U ∩ (f -` (W ∩ (p' -` (W' ∩ X))))))"
by (blast intro: opeUV openin_subtopology_self continuous_openin_preimage [OF contf fim])
have "p' (f y) ∈ X"
using ‹l y ∈ W'› homeomorphism_apply1 [OF homUW'] pleq ‹y ∈ U› ‹l y ∈ X› by fastforce
then show "y ∈ V ∩ (U ∩ f -` (W ∩ p' -` (W' ∩ X)))"
using ‹y ∈ U› ‹y ∈ V› WV p'im by auto
show "V ∩ (U ∩ f -` (W ∩ p' -` (W' ∩ X))) ⊆ U ∩ l -` X"
proof (intro subsetI IntI; clarify)
fix y'
assume y': "y' ∈ V" "y' ∈ U" "f y' ∈ W" "p' (f y') ∈ W'" "p' (f y') ∈ X"
then obtain γ where "path γ" "path_image γ ⊆ V" "pathstart γ = y" "pathfinish γ = y'"
by (meson ‹path_connected V› ‹y ∈ V› path_connected_def)
obtain pp qq where pp: "path pp" "path_image pp ⊆ U" "pathstart pp = z" "pathfinish pp = y"
and qq: "path qq" "path_image qq ⊆ C" "pathstart qq = a"
and pqqeq: "⋀t. t ∈ {0..1} ⟹ p(qq t) = f(pp t)"
using*[OF ‹y ∈ U›] by blast
have finW: "⋀x. ⟦0 ≤ x; x ≤ 1⟧ ⟹ f (γ x) ∈ W"
using ‹path_image γ ⊆ V› by (auto simp: image_subset_iff path_image_def fimW [THEN subsetD])
have "pathfinish (qq +++ (p' ∘ f ∘ γ)) = l y'"
proof (rule l [of "pp +++ γ" y' "qq +++ (p' ∘ f ∘ γ)"])
show "path (pp +++ γ)"
by (simp add: ‹path γ› ‹path pp› ‹pathfinish pp = y› ‹pathstart γ = y›)
show "path_image (pp +++ γ) ⊆ U"
using ‹V ⊆ U› ‹path_image γ ⊆ V› ‹path_image pp ⊆ U› not_in_path_image_join by blast
show "pathstart (pp +++ γ) = z"
by (simp add: ‹pathstart pp = z›)
show "pathfinish (pp +++ γ) = y'"
by (simp add: ‹pathfinish γ = y'›)
have "pathfinish qq = l y"
using ‹path pp› ‹path qq› ‹path_image pp ⊆ U› ‹path_image qq ⊆ C› ‹pathfinish pp = y› ‹pathstart pp = z› ‹pathstart qq = a› l pqqeq by blast
also have "... = p' (f y)"
using ‹l y ∈ W'› homUW' homeomorphism_apply1 pleq that(2) by fastforce
finally have "pathfinish qq = p' (f y)" .
then have paqq: "pathfinish qq = pathstart (p' ∘ f ∘ γ)"
by (simp add: ‹pathstart γ = y› pathstart_compose)
have "continuous_on (path_image γ) (p' ∘ f)"
proof (rule continuous_on_compose)
show "continuous_on (path_image γ) f"
using ‹path_image γ ⊆ V› ‹V ⊆ U› contf continuous_on_subset by blast
show "continuous_on (f ` path_image γ) p'"
proof (rule continuous_on_subset [OF contp'])
show "f ` path_image γ ⊆ W"
by (auto simp: path_image_def pathfinish_def pathstart_def finW)
qed
qed
then show "path (qq +++ (p' ∘ f ∘ γ))"
using ‹path γ› ‹path qq› paqq path_continuous_image path_join_imp by blast
show "path_image (qq +++ (p' ∘ f ∘ γ)) ⊆ C"
proof (rule subset_path_image_join)
show "path_image qq ⊆ C"
by (simp add: ‹path_image qq ⊆ C›)
show "path_image (p' ∘ f ∘ γ) ⊆ C"
by (metis ‹W' ⊆ C› ‹path_image γ ⊆ V› dual_order.trans fimW(1) image_comp image_mono p'im path_image_compose)
qed
show "pathstart (qq +++ (p' ∘ f ∘ γ)) = a"
by (simp add: ‹pathstart qq = a›)
show "p ((qq +++ (p' ∘ f ∘ γ)) ξ) = f ((pp +++ γ) ξ)" if ξ: "ξ ∈ {0..1}" for ξ
proof (simp add: joinpaths_def, safe)
show "p (qq (2*ξ)) = f (pp (2*ξ))" if "ξ*2 ≤ 1"
using ‹ξ ∈ {0..1}› pqqeq that by auto
show "p (p' (f (γ (2*ξ - 1)))) = f (γ (2*ξ - 1))" if "¬ ξ*2 ≤ 1"
using that ξ by (auto intro: homeomorphism_apply2 [OF homUW' finW])
qed
qed
with ‹pathfinish γ = y'› ‹p' (f y') ∈ X› show "y' ∈ l -` X"
unfolding pathfinish_join by (simp add: pathfinish_def)
qed
qed
qed
then show "continuous_on U l"
using vimage_eq openin_subopen continuous_on_open_gen [OF LC]
by (metis IntD1 IntD2 vimage_eq openin_subopen continuous_on_open_gen [OF LC])
qed
qed
corollary covering_space_lift_stronger:
fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
and f :: "'c::real_normed_vector ⇒ 'b"
assumes cov: "covering_space C p S" "a ∈ C" "z ∈ U"
and U: "path_connected U" "locally path_connected U"
and contf: "continuous_on U f" and fim: "f ∈ U → S"
and feq: "f z = p a"
and hom: "⋀r. ⟦path r; path_image r ⊆ U; pathstart r = z; pathfinish r = z⟧
⟹ ∃b. homotopic_paths S (f ∘ r) (linepath b b)"
obtains g where "continuous_on U g" "g ∈ U → C" "g z = a" "⋀y. y ∈ U ⟹ p(g y) = f y"
proof (rule covering_space_lift_general [OF cov U contf fim feq])
fix r
assume "path r" "path_image r ⊆ U" "pathstart r = z" "pathfinish r = z"
then obtain b where b: "homotopic_paths S (f ∘ r) (linepath b b)"
using hom by blast
then have "f (pathstart r) = b"
by (metis homotopic_paths_imp_pathstart pathstart_compose pathstart_linepath)
then have "homotopic_paths S (f ∘ r) (linepath (f z) (f z))"
by (simp add: b ‹pathstart r = z›)
then have "homotopic_paths S (f ∘ r) (p ∘ linepath a a)"
by (simp add: o_def feq linepath_def)
then show "∃q. path q ∧
path_image q ⊆ C ∧
pathstart q = a ∧ pathfinish q = a ∧ homotopic_paths S (f ∘ r) (p ∘ q)"
by (force simp: ‹a ∈ C›)
qed auto
corollary covering_space_lift_strong:
fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
and f :: "'c::real_normed_vector ⇒ 'b"
assumes cov: "covering_space C p S" "a ∈ C" "z ∈ U"
and scU: "simply_connected U" and lpcU: "locally path_connected U"
and contf: "continuous_on U f" and fim: "f ∈ U → S"
and feq: "f z = p a"
obtains g where "continuous_on U g" "g ∈ U → C" "g z = a" "⋀y. y ∈ U ⟹ p(g y) = f y"
proof (rule covering_space_lift_stronger [OF cov _ lpcU contf fim feq])
show "path_connected U"
using scU simply_connected_eq_contractible_loop_some by blast
fix r
assume r: "path r" "path_image r ⊆ U" "pathstart r = z" "pathfinish r = z"
have "linepath (f z) (f z) = f ∘ linepath z z"
by (simp add: o_def linepath_def)
then have "homotopic_paths S (f ∘ r) (linepath (f z) (f z))"
by (metis r contf fim homotopic_paths_continuous_image scU simply_connected_eq_contractible_path)
then show "∃b. homotopic_paths S (f ∘ r) (linepath b b)"
by blast
qed blast
corollary covering_space_lift:
fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
and f :: "'c::real_normed_vector ⇒ 'b"
assumes cov: "covering_space C p S"
and U: "simply_connected U" "locally path_connected U"
and contf: "continuous_on U f" and fim: "f ∈ U → S"
obtains g where "continuous_on U g" "g ∈ U → C" "⋀y. y ∈ U ⟹ p(g y) = f y"
proof (cases "U = {}")
case True
with that show ?thesis by auto
next
case False
then obtain z where "z ∈ U" by blast
then obtain a where "a ∈ C" "f z = p a"
by (metis cov covering_space_imp_surjective fim image_iff Pi_iff)
then show ?thesis
by (metis that covering_space_lift_strong [OF cov _ ‹z ∈ U› U contf fim])
qed
subsection ‹Homeomorphisms of arc images›
lemma homeomorphism_arc:
fixes g :: "real ⇒ 'a::t2_space"
assumes "arc g"
obtains h where "homeomorphism {0..1} (path_image g) g h"
using assms by (force simp: arc_def homeomorphism_compact path_def path_image_def)
lemma homeomorphic_arc_image_interval:
fixes g :: "real ⇒ 'a::t2_space" and a::real
assumes "arc g" "a < b"
shows "(path_image g) homeomorphic {a..b}"
proof -
have "(path_image g) homeomorphic {0..1::real}"
by (meson assms(1) homeomorphic_def homeomorphic_sym homeomorphism_arc)
also have "… homeomorphic {a..b}"
using assms by (force intro: homeomorphic_closed_intervals_real)
finally show ?thesis .
qed
lemma homeomorphic_arc_images:
fixes g :: "real ⇒ 'a::t2_space" and h :: "real ⇒ 'b::t2_space"
assumes "arc g" "arc h"
shows "(path_image g) homeomorphic (path_image h)"
proof -
have "(path_image g) homeomorphic {0..1::real}"
by (meson assms homeomorphic_def homeomorphic_sym homeomorphism_arc)
also have "… homeomorphic (path_image h)"
by (meson assms homeomorphic_def homeomorphism_arc)
finally show ?thesis .
qed
end