Exact source: Mathlib/Topology/Homeomorph/Lemmas.lean
Pinned GitHub source · Raw UTF-8 source
Back to Finite-dimensionality transfers across a sphere isometry
1/-2Copyright (c) 2019 Reid Barton. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Johannes Hölzl, Patrick Massot, Sébastien Gouëzel, Zhouhang Zhou, Reid Barton5-/6module78public import Mathlib.Logic.Equiv.Fin.Basic9public import Mathlib.Topology.Connected.LocallyConnected10public import Mathlib.Topology.DenseEmbedding11public import Mathlib.Topology.Connected.TotallyDisconnected12public import Mathlib.Topology.Baire.Lemmas1314/-!15# Further properties of homeomorphisms1617This file proves further properties of homeomorphisms between topological spaces.18Pretty much every topological property is preserved under homeomorphisms.1920-/2122@[expose] public section2324assert_not_exists Module MonoidWithZero2526open Filter Function Set Topology2728variable {X Y W Z : Type*}2930section3132variable [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z]33 {X' Y' : Type*} [TopologicalSpace X'] [TopologicalSpace Y']3435namespace Homeomorph3637protected theorem secondCountableTopology [SecondCountableTopology Y]38 (h : X ≃ₜ Y) : SecondCountableTopology X :=39 h.isInducing.secondCountableTopology4041protected theorem baireSpace [BaireSpace X] (f : X ≃ₜ Y) : BaireSpace Y :=42 f.isOpenQuotientMap.baireSpace4344/-- If `h : X → Y` is a homeomorphism, `h(s)` is compact iff `s` is. -/45@[simp]46theorem isCompact_image {s : Set X} (h : X ≃ₜ Y) : IsCompact (h '' s) ↔ IsCompact s :=47 h.isEmbedding.isCompact_iff.symm4849/-- If `h : X → Y` is a homeomorphism, `h⁻¹(s)` is compact iff `s` is. -/50@[simp]51theorem isCompact_preimage {s : Set Y} (h : X ≃ₜ Y) : IsCompact (h ⁻¹' s) ↔ IsCompact s := by52 rw [← image_symm]; exact h.symm.isCompact_image5354/-- If `h : X → Y` is a homeomorphism, `s` is σ-compact iff `h(s)` is. -/55@[simp]56theorem isSigmaCompact_image {s : Set X} (h : X ≃ₜ Y) :57 IsSigmaCompact (h '' s) ↔ IsSigmaCompact s :=58 h.isEmbedding.isSigmaCompact_iff.symm5960/-- If `h : X → Y` is a homeomorphism, `h⁻¹(s)` is σ-compact iff `s` is. -/61@[simp]62theorem isSigmaCompact_preimage {s : Set Y} (h : X ≃ₜ Y) :63 IsSigmaCompact (h ⁻¹' s) ↔ IsSigmaCompact s := by64 rw [← image_symm]; exact h.symm.isSigmaCompact_image6566@[simp]67theorem isPreconnected_image {s : Set X} (h : X ≃ₜ Y) :68 IsPreconnected (h '' s) ↔ IsPreconnected s :=69 ⟨fun hs ↦ by simpa only [image_symm, preimage_image]70 using hs.image _ h.symm.continuous.continuousOn,71 fun hs ↦ hs.image _ h.continuous.continuousOn⟩7273@[simp]74theorem isPreconnected_preimage {s : Set Y} (h : X ≃ₜ Y) :75 IsPreconnected (h ⁻¹' s) ↔ IsPreconnected s := by76 rw [← image_symm, isPreconnected_image]7778@[simp]79theorem isConnected_image {s : Set X} (h : X ≃ₜ Y) :80 IsConnected (h '' s) ↔ IsConnected s :=81 image_nonempty.and h.isPreconnected_image8283@[simp]84theorem isConnected_preimage {s : Set Y} (h : X ≃ₜ Y) :85 IsConnected (h ⁻¹' s) ↔ IsConnected s := by86 rw [← image_symm, isConnected_image]8788theorem image_connectedComponentIn {s : Set X} (h : X ≃ₜ Y) {x : X} (hx : x ∈ s) :89 h '' connectedComponentIn s x = connectedComponentIn (h '' s) (h x) := by90 refine (h.continuous.image_connectedComponentIn_subset hx).antisymm ?_91 have := h.symm.continuous.image_connectedComponentIn_subset (mem_image_of_mem h hx)92 rwa [image_subset_iff, h.preimage_symm, h.image_symm, h.preimage_image, h.symm_apply_apply]93 at this9495@[simp]96theorem comap_cocompact (h : X ≃ₜ Y) : comap h (cocompact Y) = cocompact X :=97 (comap_cocompact_le h.continuous).antisymm <|98 (hasBasis_cocompact.le_basis_iff (hasBasis_cocompact.comap h)).2 fun K hK =>99 ⟨h ⁻¹' K, h.isCompact_preimage.2 hK, Subset.rfl⟩100101@[simp]102theorem map_cocompact (h : X ≃ₜ Y) : map h (cocompact X) = cocompact Y := by103 rw [← h.comap_cocompact, map_comap_of_surjective h.surjective]104105protected theorem compactSpace [CompactSpace X] (h : X ≃ₜ Y) : CompactSpace Y where106 isCompact_univ := h.symm.isCompact_preimage.2 isCompact_univ107108theorem isDenseEmbedding (h : X ≃ₜ Y) : IsDenseEmbedding h :=109 { h.isEmbedding with dense := h.surjective.denseRange }110111protected lemma totallyDisconnectedSpace (h : X ≃ₜ Y) [tdc : TotallyDisconnectedSpace X] :112 TotallyDisconnectedSpace Y :=113 (totallyDisconnectedSpace_iff Y).mpr114 (h.range_coe ▸ ((IsEmbedding.isTotallyDisconnected_range h.isEmbedding).mpr tdc))115116@[simp]117theorem map_punctured_nhds_eq (h : X ≃ₜ Y) (x : X) : map h (𝓝[≠] x) = 𝓝[≠] (h x) := by118 convert! h.isEmbedding.map_nhdsWithin_eq ({ x }ᶜ) x119 rw [h.image_compl, Set.image_singleton]120121@[simp]122theorem comap_coclosedCompact (h : X ≃ₜ Y) : comap h (coclosedCompact Y) = coclosedCompact X :=123 (hasBasis_coclosedCompact.comap h).eq_of_same_basis <| by124 simpa [comp_def] using hasBasis_coclosedCompact.comp_surjective h.injective.preimage_surjective125126@[simp]127theorem map_coclosedCompact (h : X ≃ₜ Y) : map h (coclosedCompact X) = coclosedCompact Y := by128 rw [← h.comap_coclosedCompact, map_comap_of_surjective h.surjective]129130/-- If the codomain of a homeomorphism is a locally connected space, then the domain is also131a locally connected space. -/132theorem locallyConnectedSpace [i : LocallyConnectedSpace Y] (h : X ≃ₜ Y) :133 LocallyConnectedSpace X := by134 have : ∀ x, (𝓝 x).HasBasis (fun s ↦ IsOpen s ∧ h x ∈ s ∧ IsConnected s)135 (h.symm '' ·) := fun x ↦ by136 rw [← h.symm_map_nhds_eq]137 exact (i.1 _).map _138 refine locallyConnectedSpace_of_connected_bases _ _ this fun _ _ hs ↦ ?_139 exact hs.2.2.2.image _ h.symm.continuous.continuousOn140141/-- The codomain of a homeomorphism is a locally compact space if and only if142the domain is a locally compact space. -/143theorem locallyCompactSpace_iff (h : X ≃ₜ Y) :144 LocallyCompactSpace X ↔ LocallyCompactSpace Y := by145 exact ⟨fun _ => h.symm.isOpenEmbedding.locallyCompactSpace,146 fun _ => h.isClosedEmbedding.locallyCompactSpace⟩147148@[simp]149theorem comp_continuousOn_iff (h : X ≃ₜ Y) (f : Z → X) (s : Set Z) :150 ContinuousOn (h ∘ f) s ↔ ContinuousOn f s :=151 h.isInducing.continuousOn_iff.symm152153theorem comp_continuousWithinAt_iff (h : X ≃ₜ Y) (f : Z → X) (s : Set Z) (z : Z) :154 ContinuousWithinAt f s z ↔ ContinuousWithinAt (h ∘ f) s z :=155 h.isInducing.continuousWithinAt_iff156157set_option backward.defeqAttrib.useBackward true in158/-- A homeomorphism `h : X ≃ₜ Y` lifts to a homeomorphism between subtypes corresponding to159predicates `p : X → Prop` and `q : Y → Prop` so long as `p = q ∘ h`. -/160@[simps!]161def subtype {p : X → Prop} {q : Y → Prop} (h : X ≃ₜ Y) (h_iff : ∀ x, p x ↔ q (h x)) :162 {x // p x} ≃ₜ {y // q y} where163 __ := h.subtypeEquiv h_iff164165@[simp]166lemma subtype_toEquiv {p : X → Prop} {q : Y → Prop} (h : X ≃ₜ Y) (h_iff : ∀ x, p x ↔ q (h x)) :167 (h.subtype h_iff).toEquiv = h.toEquiv.subtypeEquiv h_iff :=168 rfl169170/-- A homeomorphism `h : X ≃ₜ Y` lifts to a homeomorphism between sets `s : Set X` and `t : Set Y`171whenever `h` maps `s` onto `t`. -/172abbrev sets {s : Set X} {t : Set Y} (h : X ≃ₜ Y) (h_eq : s = h ⁻¹' t) : s ≃ₜ t :=173 h.subtype <| Set.ext_iff.mp h_eq174175set_option backward.defeqAttrib.useBackward true in176/-- If two sets are equal, then they are homeomorphic. -/177def setCongr {s t : Set X} (h : s = t) : s ≃ₜ t where178 toEquiv := Equiv.setCongr h179180section prod181182variable (X Y W Z)183184/-- `X × {*}` is homeomorphic to `X`. -/185@[simps! symm_apply_snd]186def prodUnique [Unique Y] :187 X × Y ≃ₜ X where188 toEquiv := Equiv.prodUnique X Y189190@[simp] theorem coe_prodUnique [Unique Y] : ⇑(prodUnique X Y) = Prod.fst := rfl191192/-- `X × {*}` is homeomorphic to `X`. -/193@[simps! symm_apply_snd]194def uniqueProd (X Y : Type*) [TopologicalSpace X] [TopologicalSpace Y] [Unique X] :195 X × Y ≃ₜ Y :=196 (prodComm _ _).trans (prodUnique Y X)197198@[simp] theorem coe_uniqueProd [Unique X] : ⇑(uniqueProd X Y) = Prod.snd := rfl199200set_option backward.defeqAttrib.useBackward true in201/-- The product over `S ⊕ T` of a family of topological spaces202is homeomorphic to the product of (the product over `S`) and (the product over `T`).203204This is `Equiv.sumPiEquivProdPi` as a `Homeomorph`.205-/206def sumPiEquivProdPi (S T : Type*) (A : S ⊕ T → Type*)207 [∀ st, TopologicalSpace (A st)] :208 (Π (st : S ⊕ T), A st) ≃ₜ (Π (s : S), A (.inl s)) × (Π (t : T), A (.inr t)) where209 __ := Equiv.sumPiEquivProdPi _210 continuous_invFun := continuous_pi <| by rintro (s | t) <;> dsimp <;> fun_prop211212/-- The product `Π t : α, f t` of a family of topological spaces is homeomorphic to the213space `f ⬝` when `α` only contains `⬝`.214215This is `Equiv.piUnique` as a `Homeomorph`.216-/217@[simps! -fullyApplied]218def piUnique {α : Type*} [Unique α] (f : α → Type*) [∀ x, TopologicalSpace (f x)] :219 (Π t, f t) ≃ₜ f default :=220 (Equiv.piUnique f).toHomeomorphOfContinuousOpen (continuous_apply default) (isOpenMap_eval _)221222end prod223224/-- `Equiv.piCongrLeft` as a homeomorphism: this is the natural homeomorphism225`Π i, Y (e i) ≃ₜ Π j, Y j` obtained from a bijection `ι ≃ ι'`. -/226@[simps +simpRhs toEquiv, simps! -isSimp apply]227def piCongrLeft {ι ι' : Type*} {Y : ι' → Type*} [∀ j, TopologicalSpace (Y j)]228 (e : ι ≃ ι') : (∀ i, Y (e i)) ≃ₜ ∀ j, Y j where229 continuous_toFun := continuous_pi <| e.forall_congr_right.mp fun i ↦ by230 simpa only [Equiv.toFun_as_coe, Equiv.piCongrLeft_apply_apply] using continuous_apply i231 continuous_invFun := Pi.continuous_precomp' e232 toEquiv := Equiv.piCongrLeft _ e233234@[simp]235lemma piCongrLeft_refl {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] :236 piCongrLeft (.refl ι) = .refl (∀ i, X i) :=237 rfl238239@[simp]240lemma piCongrLeft_symm_apply {ι ι' : Type*} {Y : ι' → Type*} [∀ j, TopologicalSpace (Y j)]241 (e : ι ≃ ι') : ⇑(piCongrLeft (Y := Y) e).symm = (· <| e ·) :=242 rfl243244@[simp]245lemma piCongrLeft_apply_apply {ι ι' : Type*} {Y : ι' → Type*} [∀ j, TopologicalSpace (Y j)]246 (e : ι ≃ ι') (x : ∀ i, Y (e i)) (i : ι) : piCongrLeft e x (e i) = x i :=247 Equiv.piCongrLeft_apply_apply ..248249set_option backward.defeqAttrib.useBackward true in250/-- `Equiv.piCongrRight` as a homeomorphism: this is the natural homeomorphism251`Π i, Y₁ i ≃ₜ Π j, Y₂ i` obtained from homeomorphisms `Y₁ i ≃ₜ Y₂ i` for each `i`. -/252@[simps! apply toEquiv]253def piCongrRight {ι : Type*} {Y₁ Y₂ : ι → Type*} [∀ i, TopologicalSpace (Y₁ i)]254 [∀ i, TopologicalSpace (Y₂ i)] (F : ∀ i, Y₁ i ≃ₜ Y₂ i) : (∀ i, Y₁ i) ≃ₜ ∀ i, Y₂ i where255 toEquiv := Equiv.piCongrRight fun i => (F i).toEquiv256257@[simp]258theorem piCongrRight_symm {ι : Type*} {Y₁ Y₂ : ι → Type*} [∀ i, TopologicalSpace (Y₁ i)]259 [∀ i, TopologicalSpace (Y₂ i)] (F : ∀ i, Y₁ i ≃ₜ Y₂ i) :260 (piCongrRight F).symm = piCongrRight fun i => (F i).symm :=261 rfl262263/-- `Equiv.piCongr` as a homeomorphism: this is the natural homeomorphism264`Π i₁, Y₁ i ≃ₜ Π i₂, Y₂ i₂` obtained from a bijection `ι₁ ≃ ι₂` and homeomorphisms265`Y₁ i₁ ≃ₜ Y₂ (e i₁)` for each `i₁ : ι₁`. -/266@[simps! apply toEquiv]267def piCongr {ι₁ ι₂ : Type*} {Y₁ : ι₁ → Type*} {Y₂ : ι₂ → Type*}268 [∀ i₁, TopologicalSpace (Y₁ i₁)] [∀ i₂, TopologicalSpace (Y₂ i₂)]269 (e : ι₁ ≃ ι₂) (F : ∀ i₁, Y₁ i₁ ≃ₜ Y₂ (e i₁)) : (∀ i₁, Y₁ i₁) ≃ₜ ∀ i₂, Y₂ i₂ :=270 (Homeomorph.piCongrRight F).trans (Homeomorph.piCongrLeft e)271272/-- `ULift X` is homeomorphic to `X`. -/273def ulift.{u, v} {X : Type v} [TopologicalSpace X] : ULift.{u, v} X ≃ₜ X where274 toEquiv := Equiv.ulift275276/-- The natural homeomorphism `(ι ⊕ ι' → X) ≃ₜ (ι → X) × (ι' → X)`.277`Equiv.sumArrowEquivProdArrow` as a homeomorphism. -/278@[simps!]279def sumArrowHomeomorphProdArrow {ι ι' : Type*} : (ι ⊕ ι' → X) ≃ₜ (ι → X) × (ι' → X) where280 toEquiv := Equiv.sumArrowEquivProdArrow _ _ _281 continuous_toFun := by282 dsimp [Equiv.sumArrowEquivProdArrow]283 fun_prop284 continuous_invFun := continuous_pi fun i ↦ match i with285 | .inl i => by apply (continuous_apply _).comp' continuous_fst286 | .inr i => by apply (continuous_apply _).comp' continuous_snd287288private theorem _root_.Fin.appendEquiv_eq_homeomorph (m n : ℕ) : Fin.appendEquiv m n =289 (sumArrowHomeomorphProdArrow.symm.trans290 (piCongrLeft (Y := fun _ ↦ X) finSumFinEquiv)).toEquiv := by291 apply Equiv.symm_bijective.injective292 ext x i <;> simp293294@[fun_prop]295theorem _root_.Fin.continuous_append (m n : ℕ) :296 Continuous fun (p : (Fin m → X) × (Fin n → X)) ↦ Fin.append p.1 p.2 := by297 suffices Continuous (Fin.appendEquiv m n) by exact this298 rw [Fin.appendEquiv_eq_homeomorph]299 exact Homeomorph.continuous_toFun _300301/-- The natural homeomorphism between `(Fin m → X) × (Fin n → X)` and `Fin (m + n) → X`.302`Fin.appendEquiv` as a homeomorphism -/303@[simps!]304def _root_.Fin.appendHomeomorph (m n : ℕ) : (Fin m → X) × (Fin n → X) ≃ₜ (Fin (m + n) → X) where305 toEquiv := Fin.appendEquiv m n306307@[simp]308theorem _root_.Fin.appendHomeomorph_toEquiv (m n : ℕ) :309 (Fin.appendHomeomorph (X := X) m n).toEquiv = Fin.appendEquiv m n :=310 rfl311312section Distrib313314variable {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)]315316/-- `(Σ i, X i) × Y` is homeomorphic to `Σ i, (X i × Y)`. -/317@[simps! apply symm_apply toEquiv]318def sigmaProdDistrib : (Σ i, X i) × Y ≃ₜ Σ i, X i × Y :=319 Homeomorph.symm <|320 (Equiv.sigmaProdDistrib X Y).symm.toHomeomorphOfContinuousOpen321 (continuous_sigma fun _ => continuous_sigmaMk.fst'.prodMk continuous_snd)322 (isOpenMap_sigma.2 fun _ => isOpenMap_sigmaMk.prodMap IsOpenMap.id)323324end Distrib325326set_option backward.defeqAttrib.useBackward true in327/-- If `ι` has a unique element, then `ι → X` is homeomorphic to `X`. -/328@[simps! -fullyApplied]329def funUnique (ι X : Type*) [Unique ι] [TopologicalSpace X] : (ι → X) ≃ₜ X where330 toEquiv := Equiv.funUnique ι X331332/-- Homeomorphism between dependent functions `Π i : Fin 2, X i` and `X 0 × X 1`. -/333@[simps! -fullyApplied]334def piFinTwo.{u} (X : Fin 2 → Type u) [∀ i, TopologicalSpace (X i)] : (∀ i, X i) ≃ₜ X 0 × X 1 where335 toEquiv := piFinTwoEquiv X336337/-- Homeomorphism between `X² = Fin 2 → X` and `X × X`. -/338@[simps! -fullyApplied]339def finTwoArrow : (Fin 2 → X) ≃ₜ X × X :=340 { piFinTwo fun _ => X with toEquiv := finTwoArrowEquiv X }341342/-- A subset of a topological space is homeomorphic to its image under a homeomorphism.343-/344@[simps!]345def image (e : X ≃ₜ Y) (s : Set X) : s ≃ₜ e '' s where346 -- TODO: by continuity!347 continuous_toFun := e.continuous.continuousOn.mapsToRestrict (mapsTo_image _ _)348 continuous_invFun := (e.symm.continuous.comp continuous_subtype_val).codRestrict _349 toEquiv := e.toEquiv.image s350351/-- `Set.univ X` is homeomorphic to `X`. -/352@[simps! -fullyApplied]353def Set.univ (X : Type*) [TopologicalSpace X] : (univ : Set X) ≃ₜ X where354 toEquiv := Equiv.Set.univ X355356/-- `s ×ˢ t` is homeomorphic to `s × t`. -/357@[simps!]358def Set.prod (s : Set X) (t : Set Y) : ↥(s ×ˢ t) ≃ₜ s × t where359 toEquiv := Equiv.Set.prod s t360 continuous_toFun :=361 (continuous_subtype_val.fst.subtype_mk _).prodMk (continuous_subtype_val.snd.subtype_mk _)362 continuous_invFun :=363 (continuous_subtype_val.fst'.prodMk continuous_subtype_val.snd').subtype_mk _364365section366367variable {ι : Type*}368369/-- The topological space `Π i, Y i` can be split as a product by separating the indices in ι370 depending on whether they satisfy a predicate p or not. -/371@[simps!]372def piEquivPiSubtypeProd (p : ι → Prop) (Y : ι → Type*) [∀ i, TopologicalSpace (Y i)]373 [DecidablePred p] : (∀ i, Y i) ≃ₜ (∀ i : { x // p x }, Y i) × ∀ i : { x // ¬p x }, Y i where374 toEquiv := Equiv.piEquivPiSubtypeProd p Y375 continuous_invFun :=376 continuous_pi fun j => by377 dsimp only [Equiv.piEquivPiSubtypeProd]; split_ifs378 exacts [(continuous_apply _).comp continuous_fst, (continuous_apply _).comp continuous_snd]379380variable [DecidableEq ι] (i : ι)381382/-- A product of topological spaces can be split as the binary product of one of the spaces and383 the product of all the remaining spaces. -/384@[simps!]385def piSplitAt (Y : ι → Type*) [∀ j, TopologicalSpace (Y j)] :386 (∀ j, Y j) ≃ₜ Y i × ∀ j : { j // j ≠ i }, Y j where387 toEquiv := Equiv.piSplitAt i Y388 continuous_invFun :=389 continuous_pi fun j => by390 dsimp only [Equiv.piSplitAt]391 split_ifs with h392 · subst h393 exact continuous_fst394 · exact (continuous_apply _).comp continuous_snd395396variable (Y)397398/-- A product of copies of a topological space can be split as the binary product of one copy and399 the product of all the remaining copies. -/400@[simps!]401def funSplitAt : (ι → Y) ≃ₜ Y × ({ j // j ≠ i } → Y) :=402 piSplitAt i _403404end405406end Homeomorph407408namespace Topology.IsEmbedding409410/-- Homeomorphism given an embedding. -/411@[simps! apply_coe]412noncomputable def toHomeomorph {f : X → Y} (hf : IsEmbedding f) :413 X ≃ₜ Set.range f :=414 Equiv.ofInjective f hf.injective |>.toHomeomorphOfIsInducing <|415 IsInducing.subtypeVal.of_comp_iff.mp hf.toIsInducing416417@[simp]418lemma toHomeomorph_symm_apply {f : X → Y} (hf : IsEmbedding f) (x : X) :419 hf.toHomeomorph.symm ⟨f x, by simp⟩ = x :=420 hf.toHomeomorph.injective (by ext; simp)421422/-- A surjective embedding is a homeomorphism. -/423@[simps! apply]424noncomputable def toHomeomorphOfSurjective {f : X → Y}425 (hf : IsEmbedding f) (hsurj : Function.Surjective f) : X ≃ₜ Y :=426 Equiv.ofBijective f ⟨hf.injective, hsurj⟩ |>.toHomeomorphOfIsInducing hf.toIsInducing427428/-- A set is homeomorphic to its image under any embedding. -/429noncomputable def homeomorphImage {f : X → Y} (hf : IsEmbedding f) (s : Set X) : s ≃ₜ f '' s :=430 (hf.comp .subtypeVal).toHomeomorph.trans <| .setCongr <| by simp [Set.range_comp]431432/-- An embedding restricts to a homeomorphism between the preimage and any subset of its range. -/433noncomputable def homeomorphOfSubsetRange {f : X → Y} (hf : IsEmbedding f)434 {s : Set Y} (hs : s ⊆ Set.range f) : (f ⁻¹' s) ≃ₜ s :=435 hf.homeomorphImage (f ⁻¹' s) |>.trans <| .setCongr <| Set.image_preimage_eq_of_subset hs436437@[simp]438theorem homeomorphOfSubsetRange_apply_coe {f : X → Y} (hf : IsEmbedding f)439 {s : Set Y} (hs : s ⊆ Set.range f) (x : f ⁻¹' s) :440 ↑(hf.homeomorphOfSubsetRange hs x) = f ↑x := rfl441442end Topology.IsEmbedding443444lemma Topology.IsEmbedding.uliftMap {f : X → Y} (hf : IsEmbedding f) :445 IsEmbedding (ULift.map f) :=446 .comp Homeomorph.ulift.symm.isEmbedding (.comp hf <| Homeomorph.ulift.isEmbedding)447448lemma Topology.IsOpenEmbedding.uliftMap {f : X → Y} (hf : IsOpenEmbedding f) :449 IsOpenEmbedding (ULift.map f) :=450 .comp Homeomorph.ulift.symm.isOpenEmbedding (.comp hf <| Homeomorph.ulift.isOpenEmbedding)451452lemma Topology.IsClosedEmbedding.uliftMap {f : X → Y} (hf : IsClosedEmbedding f) :453 IsClosedEmbedding (ULift.map f) :=454 .comp Homeomorph.ulift.symm.isClosedEmbedding (.comp hf <| Homeomorph.ulift.isClosedEmbedding)455456end457458namespace Continuous459460variable [TopologicalSpace X] [TopologicalSpace Y]461462theorem continuous_symm_of_equiv_compact_to_t2 [CompactSpace X] [T2Space Y] {f : X ≃ Y}463 (hf : Continuous f) : Continuous f.symm := by464 rw [continuous_iff_isClosed]465 intro C hC466 have hC' : IsClosed (f '' C) := (hC.isCompact.image hf).isClosed467 rwa [Equiv.image_eq_preimage_symm] at hC'468469/-- Continuous equivalences from a compact space to a T2 space are homeomorphisms.470471This is not true when T2 is weakened to T1472(see `Continuous.homeoOfEquivCompactToT2.t1_counterexample`). -/473@[simps toEquiv]474def homeoOfEquivCompactToT2 [CompactSpace X] [T2Space Y] {f : X ≃ Y} (hf : Continuous f) : X ≃ₜ Y :=475 { f with476 continuous_toFun := hf477 continuous_invFun := hf.continuous_symm_of_equiv_compact_to_t2 }478479end Continuous480481variable [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]482 {W : Type*} [TopologicalSpace W] {f : X → Y}483484namespace IsHomeomorph485variable (hf : IsHomeomorph f)486include hf487488protected lemma isClosedMap : IsClosedMap f := (hf.homeomorph f).isClosedMap489lemma isInducing : IsInducing f := (hf.homeomorph f).isInducing490lemma isQuotientMap : IsQuotientMap f := (hf.homeomorph f).isQuotientMap491lemma isEmbedding : IsEmbedding f := (hf.homeomorph f).isEmbedding492lemma isOpenEmbedding : IsOpenEmbedding f := (hf.homeomorph f).isOpenEmbedding493lemma isClosedEmbedding : IsClosedEmbedding f := (hf.homeomorph f).isClosedEmbedding494lemma isDenseEmbedding : IsDenseEmbedding f := (hf.homeomorph f).isDenseEmbedding495496end IsHomeomorph497498/-- A map is a homeomorphism iff it is the map underlying a bundled homeomorphism `h : X ≃ₜ Y`. -/499lemma isHomeomorph_iff_exists_homeomorph : IsHomeomorph f ↔ ∃ h : X ≃ₜ Y, h = f :=500 ⟨fun hf => ⟨hf.homeomorph f, rfl⟩, fun ⟨h, h'⟩ => h' ▸ h.isHomeomorph⟩501502/-- A map is a homeomorphism iff it is continuous and has a continuous inverse. -/503lemma isHomeomorph_iff_exists_inverse : IsHomeomorph f ↔ Continuous f ∧ ∃ g : Y → X,504 LeftInverse g f ∧ RightInverse g f ∧ Continuous g := by505 refine ⟨fun hf ↦ ⟨hf.continuous, ?_⟩, fun ⟨hf, g, hg⟩ ↦ ?_⟩506 · let h := hf.homeomorph f507 exact ⟨h.symm, h.left_inv, h.right_inv, h.continuous_invFun⟩508 · exact (Homeomorph.mk ⟨f, g, hg.1, hg.2.1⟩ hf hg.2.2).isHomeomorph509510/-- An equivalence between topological spaces is a homeomorphism iff it is continuous in both511directions. -/512theorem Equiv.isHomeomorph_iff (e : X ≃ Y) :513 IsHomeomorph e ↔ Continuous e ∧ Continuous e.symm := by514 rw [e.continuous_symm_iff]515 exact ⟨fun h ↦ ⟨h.continuous, h.isOpenMap⟩, fun ⟨hc, ho⟩ ↦ ⟨hc, ho, e.bijective⟩⟩516517/-- A map is a homeomorphism iff it is a surjective embedding. -/518lemma isHomeomorph_iff_isEmbedding_surjective : IsHomeomorph f ↔ IsEmbedding f ∧ Surjective f where519 mp hf := ⟨hf.isEmbedding, hf.surjective⟩520 mpr h := ⟨h.1.continuous, ((isOpenEmbedding_iff f).2 ⟨h.1, h.2.range_eq ▸ isOpen_univ⟩).isOpenMap,521 h.1.injective, h.2⟩522523/-- A map is a homeomorphism iff it is a quotient map and injective. -/524lemma isHomeomorph_iff_isQuotientMap_injective {f : X → Y} :525 IsHomeomorph f ↔ IsQuotientMap f ∧ Injective f := by526 refine ⟨fun h ↦ ⟨h.isQuotientMap, h.injective⟩,527 fun h ↦ ⟨h.1.continuous, fun s hs ↦ ?_, h.2, h.1.surjective⟩⟩528 rwa [← h.1.isOpen_preimage, Set.preimage_image_eq _ h.2]529530/-- A map is a homeomorphism iff it is continuous, closed and bijective. -/531lemma isHomeomorph_iff_continuous_isClosedMap_bijective : IsHomeomorph f ↔532 Continuous f ∧ IsClosedMap f ∧ Function.Bijective f :=533 ⟨fun hf => ⟨hf.continuous, hf.isClosedMap, hf.bijective⟩, fun ⟨hf, hf', hf''⟩ =>534 ⟨hf, fun _ hu => isClosed_compl_iff.1 (image_compl_eq hf'' ▸ hf' _ hu.isClosed_compl), hf''⟩⟩535536/-- A map from a compact space to a T2 space is a homeomorphism iff it is continuous and537 bijective. -/538lemma isHomeomorph_iff_continuous_bijective [CompactSpace X] [T2Space Y] :539 IsHomeomorph f ↔ Continuous f ∧ Bijective f := by540 rw [isHomeomorph_iff_continuous_isClosedMap_bijective]541 refine and_congr_right fun hf ↦ ?_542 rw [eq_true hf.isClosedMap, true_and]543544lemma IsHomeomorph.sumMap {g : Z → W} (hf : IsHomeomorph f) (hg : IsHomeomorph g) :545 IsHomeomorph (Sum.map f g) := ⟨hf.1.sumMap hg.1, hf.2.sumMap hg.2, hf.3.sumMap hg.3⟩546547lemma IsHomeomorph.prodMap {g : Z → W} (hf : IsHomeomorph f) (hg : IsHomeomorph g) :548 IsHomeomorph (Prod.map f g) := ⟨hf.1.prodMap hg.1, hf.2.prodMap hg.2, hf.3.prodMap hg.3⟩549550lemma IsHomeomorph.sigmaMap {ι κ : Type*} {X : ι → Type*} {Y : κ → Type*}551 [∀ i, TopologicalSpace (X i)] [∀ i, TopologicalSpace (Y i)] {f : ι → κ}552 (hf : Bijective f) {g : (i : ι) → X i → Y (f i)} (hg : ∀ i, IsHomeomorph (g i)) :553 IsHomeomorph (Sigma.map f g) := by554 simp_rw [isHomeomorph_iff_isEmbedding_surjective] at hg ⊢555 exact ⟨(isEmbedding_sigmaMap hf.1).2 fun i ↦ (hg i).1, hf.2.sigma_map fun i ↦ (hg i).2⟩556557lemma IsHomeomorph.pi_map {ι : Type*} {X Y : ι → Type*} [∀ i, TopologicalSpace (X i)]558 [∀ i, TopologicalSpace (Y i)] {f : (i : ι) → X i → Y i} (h : ∀ i, IsHomeomorph (f i)) :559 IsHomeomorph (fun (x : ∀ i, X i) i ↦ f i (x i)) :=560 (Homeomorph.piCongrRight fun i ↦ (h i).homeomorph (f i)).isHomeomorph561562/-- A bijection between discrete topological spaces induces a homeomorphism. -/563def Homeomorph.ofDiscrete [DiscreteTopology X] [DiscreteTopology Y] (f : X ≃ Y) : X ≃ₜ Y where564 toEquiv := f565566theorem Equiv.isHomeomorph_of_discrete [DiscreteTopology X] [DiscreteTopology Y]567 (f : X ≃ Y) : IsHomeomorph f :=568 (Homeomorph.ofDiscrete f).isHomeomorph569570section571572/-- If `f : X → Y` is coinducing and has connected fibers, it induces a homeomorphism on `π₀`. -/573noncomputable def Topology.IsCoinducing.connectedComponentsHomeomorph {f : X → Y}574 (hf : IsCoinducing f) (hf' : ∀ y, IsConnected (f ⁻¹' {y})) :575 ConnectedComponents X ≃ₜ ConnectedComponents Y :=576 IsHomeomorph.homeomorph hf.continuous.connectedComponentsMap <| by577 have hbij := hf.connectedComponentsMap_bijective hf'578 exact ⟨hf.continuous.connectedComponentsMap_continuous,579 hf.connectedComponentsMap.isOpenMap_of_injective hbij.injective, hbij⟩580581variable {f : X → Y} (hf : Topology.IsCoinducing f) (hf' : ∀ y, IsConnected (f ⁻¹' {y}))582583@[simp]584lemma Topology.IsCoinducing.connectedComponentsHomeomorph_mk (x : X) :585 hf.connectedComponentsHomeomorph hf' (.mk x) = .mk (f x) :=586 rfl587588@[simp]589lemma Topology.IsCoinducing.connectedComponentsHomeomorph_symm_mk_apply (x : X) :590 (hf.connectedComponentsHomeomorph hf').symm (.mk (f x)) = .mk x :=591 (hf.connectedComponentsHomeomorph hf').injective (by simp)592593end