diff --git a/Mathlib/Topology/Compactness/Compact.lean b/Mathlib/Topology/Compactness/Compact.lean index fb6b6d7acff7d6..0f3ec8410f0389 100644 --- a/Mathlib/Topology/Compactness/Compact.lean +++ b/Mathlib/Topology/Compactness/Compact.lean @@ -1245,3 +1245,8 @@ theorem IsClosed.exists_minimal_nonempty_closed_subset [CompactSpace X] {S : Set rw [← this, compl_compl] end Compact + +/-- +A function satisfies `HasCompactFibers` if all the fibers are compact +-/ +abbrev HasCompactFibers (f : X → Y) : Prop := ∀ y, IsCompact (f ⁻¹' {y}) diff --git a/Mathlib/Topology/Constructible.lean b/Mathlib/Topology/Constructible.lean index fd8072bc572604..70790f3df029d9 100644 --- a/Mathlib/Topology/Constructible.lean +++ b/Mathlib/Topology/Constructible.lean @@ -328,6 +328,12 @@ omit [CompactSpace X] in lemma _root_.IsCompact.isRetrocompact (hU' : IsCompact U) (hU : IsOpen U) : IsRetrocompact U := fun _ hV' hV ↦ hU'.inter_of_isOpen hV' hU hV +omit [QuasiSeparatedSpace X] in +lemma IsOpenEmbedding.isSpectralMap_of_compactSpace {f : X → Y} + (hf : Topology.IsOpenEmbedding f) [QuasiSeparatedSpace Y] : + IsSpectralMap f := ⟨hf.continuous, fun _ hU hU' ↦ IsRetrocompact.isCompact <| + IsRetrocompact.preimage_of_isOpenEmbedding hf <| hU'.isRetrocompact hU⟩ + omit [CompactSpace X] in lemma _root_.IsCompact.isConstructible (hU' : IsCompact U) (hU : IsOpen U) : IsConstructible U := (hU'.isRetrocompact hU).isConstructible hU diff --git a/Mathlib/Topology/Defs/Induced.lean b/Mathlib/Topology/Defs/Induced.lean index c652bd260cf68d..549fda82c78a85 100644 --- a/Mathlib/Topology/Defs/Induced.lean +++ b/Mathlib/Topology/Defs/Induced.lean @@ -108,6 +108,13 @@ protected def equiv (X : Type*) (t : TopologicalSpace X) : WithTopology X t ≃ left_inv _ := rfl right_inv _ := rfl +/-- +Induced map `lift f : WithTopology X → WithTopology Y` by a map `f : X → Y`. +-/ +def map {X Y : Type*} (s : TopologicalSpace X) (t : TopologicalSpace Y) (f : X → Y) : + WithTopology X s → WithTopology Y t := + (WithTopology.equiv Y t).symm ∘ f ∘ WithTopology.equiv X s + end WithTopology namespace Topology diff --git a/Mathlib/Topology/Maps/Proper/Basic.lean b/Mathlib/Topology/Maps/Proper/Basic.lean index 52f33b2efe870b..a34fd3481dd27e 100644 --- a/Mathlib/Topology/Maps/Proper/Basic.lean +++ b/Mathlib/Topology/Maps/Proper/Basic.lean @@ -346,3 +346,6 @@ theorem IsProperMap.universally_closed (Z) [TopologicalSpace Z] (h : IsProperMap IsClosedMap (Prod.map f id : X × Z → Y × Z) := -- `f × id` is proper as a product of proper maps, hence closed. (h.prodMap isProperMap_id).isClosedMap + +lemma IsProperMap.hasCompactFibers {f : X → Y} (hf : IsProperMap f) : HasCompactFibers f := + (isProperMap_iff_isClosedMap_and_compact_fibers.mp hf).2.2 diff --git a/Mathlib/Topology/Spectral/ConstructibleTopology.lean b/Mathlib/Topology/Spectral/ConstructibleTopology.lean index 307c535b393481..d4dec3b758a849 100644 --- a/Mathlib/Topology/Spectral/ConstructibleTopology.lean +++ b/Mathlib/Topology/Spectral/ConstructibleTopology.lean @@ -9,6 +9,7 @@ public import Mathlib.Topology.Spectral.Basic public import Mathlib.Topology.WithTopology public import Mathlib.Topology.JacobsonSpace public import Mathlib.Data.Set.Card +public import Mathlib.Topology.Constructible /-! # Constructible topology @@ -89,12 +90,9 @@ lemma isCompact_sInter_of_subset_constructibleTopologySubbasis [CompactSpace X] is still quasi-compact in the constructible topology. This holds in particular for spectral spaces. -/ @[stacks 0901 "quasi-compactness"] -instance compactSpace_withConstructibleTopology [CompactSpace X] [QuasiSober X] - [PrespectralSpace X] [QuasiSeparatedSpace X] : - CompactSpace (WithConstructibleTopology X) := by - suffices h : @CompactSpace X (constructibleTopology X) from - @Function.Surjective.compactSpace _ _ (constructibleTopology X) _ _ - (WithTopology.continuous_toTopology _) _ (WithTopology.toTopology_surjective _) +instance compactSpace_constructibleTopology [CompactSpace X] + [QuasiSober X] [PrespectralSpace X] [QuasiSeparatedSpace X] : + @CompactSpace X (constructibleTopology X) := by let 𝔅 := constructibleTopologySubbasis X /- It suffices to check that any subset of `𝔅` for which every finite subset has non-empty intersection, has non-empty intersection. We argue by contradiction and by Zorn's @@ -163,3 +161,142 @@ instance compactSpace_withConstructibleTopology [CompactSpace X] [QuasiSober X] · rw [← Set.sInter_union] refine hB.prop.2.1 (_ ∪ F) ?_ <| (hA₁'.sdiff.union hA₂'.sdiff).union hF grind [Set.sdiff_singleton_subset_iff, Set.union_subset_iff] + +/-- If `X` is quasi-separated, quasi-sober, prespectral and quasi-compact, then `X` is still +quasi-compact in the constructible topology. This holds in particular for spectral spaces. -/ +@[stacks 0901 "quasi-compactness"] +instance compactSpace_withConstructibleTopology [CompactSpace X] [QuasiSober X] + [PrespectralSpace X] [QuasiSeparatedSpace X] : + CompactSpace (WithConstructibleTopology X) := + @Function.Surjective.compactSpace _ _ (constructibleTopology X) _ _ + (WithTopology.continuous_toTopology _) compactSpace_constructibleTopology + (WithTopology.toTopology_surjective _) + +/-- If `X` is prespectral, T0 and quasi-sober, then `X` is T2 in the +constructible topology. This holds in particular for spectral spaces. -/ +@[stacks 0901 "Hausdorffness"] +instance t2Space_constructibleTopology [PrespectralSpace X] [T0Space X] + [QuasiSober X] : @T2Space X (constructibleTopology X) := by + simp only [t2Space_iff] + intro x y hxy + wlog h : ∃ (U : Set X), IsOpen U ∧ x ∈ U ∧ y ∉ U + · have o : ∃ (U : Set X), IsOpen U ∧ y ∈ U ∧ x ∉ U := by + obtain ⟨U, hU1, (o | o)⟩ := exists_isOpen_xor_mem (X := X) hxy <;> use U + · simp only [not_exists, not_and, not_not] at h + exact (o.2 (h U hU1 o.1)).elim + obtain ⟨U, V, a, b, c, d, e⟩ := @this X _ _ _ _ y x hxy.symm o + exact ⟨V, U, b, a, d, c, e.symm⟩ + obtain ⟨U, hU1, hU2, hU3⟩ := h + obtain ⟨V, ⟨hVo, hVc⟩, hV, hVU⟩ := + PrespectralSpace.isTopologicalBasis.mem_nhds_iff.mp (hU1.mem_nhds ‹_›) + · exact ⟨V, Vᶜ, + TopologicalSpace.isOpen_generateFrom_of_mem (.inl ⟨hVo, hVc⟩), + TopologicalSpace.isOpen_generateFrom_of_mem + (Or.inr ⟨hVo.isClosed_compl, (compl_compl V).symm ▸ hVc⟩), + hV, Set.mem_compl (fun h ↦ hU3 (hVU h)), disjoint_compl_right⟩ + +/-- If `X` is prespectral, T0 and quasi-sober, then `X` is T2 in the +constructible topology. This holds in particular for spectral spaces. -/ +@[stacks 0901 "Hausdorffness"] +instance t2Space_withConstructibleTopology [PrespectralSpace X] [T0Space X] + [QuasiSober X] : T2Space <| WithConstructibleTopology X := + @T2Space.of_injective_continuous (WithConstructibleTopology X) X _ + (constructibleTopology X) t2Space_constructibleTopology WithTopology.ofTopology + (WithTopology.ofTopology_injective (constructibleTopology X)) + (WithTopology.continuous_ofTopology (constructibleTopology X)) + +/-- +Canonical map from a space `X` to `WithConstructibleTopology X` +-/ +def toConstructibleTopology (X) [TopologicalSpace X] : X ≃ WithConstructibleTopology X := + (WithTopology.equiv X (constructibleTopology X)).symm + +/-- +Canonical map from a space `WithConstructibleTopology X` to `X` +-/ +def WithConstructibleTopology.equiv (X) [TopologicalSpace X] : WithConstructibleTopology X ≃ X := + WithTopology.equiv X (constructibleTopology X) + +variable {Y : Type*} [TopologicalSpace Y] +/-- +Induced map `lift f : WithConstructibleTopology X → WithConstructibleTopology Y` by a map +`f : X → Y` +-/ +def WithConstructibleTopology.map (f : X → Y) : + WithConstructibleTopology X → WithConstructibleTopology Y := + (equiv Y).symm ∘ f ∘ equiv X + +@[simp] +lemma WithConstructibleTopology.map_id (x : WithConstructibleTopology X) : + WithConstructibleTopology.map id x = x := rfl + +@[simp] +lemma WithConstructibleTopology.map_comp {Z : Type*} [TopologicalSpace Z] (f : X → Y) (g : Y → Z) : + WithConstructibleTopology.map (g ∘ f) = + WithConstructibleTopology.map g ∘ WithConstructibleTopology.map f := rfl + +lemma isOpen_ofConstructibleTopology_preimage_iff (s : Set X) : + IsOpen (WithConstructibleTopology.equiv X ⁻¹' s) ↔ IsOpen[constructibleTopology X] s := .rfl + +/-- +The map from `X` with the constructible topology to `X` is continuous if `X` is prespectral. +-/ +lemma WithConstructibleTopology.continuous_equiv [PrespectralSpace X] : + Continuous <| equiv X := by + rw [TopologicalSpace.IsTopologicalBasis.continuous_iff (PrespectralSpace.isBasis_opens X)] + simp only [Set.mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] + intro U hU + rw [isOpen_ofConstructibleTopology_preimage_iff] + exact hU.isOpen_constructibleTopology_of_isOpen U.2 + +lemma WithConstructibleTopology.continuous_constructibleTopology_id [PrespectralSpace X] : + @Continuous X X (constructibleTopology X) _ id := + @Continuous.comp X _ X (constructibleTopology X) _ + _ _ _ continuous_equiv (WithTopology.continuous_toTopology (constructibleTopology X)) + +lemma WithConstructibleTopology.map_continuous_iff (f : X → Y) : + Continuous (WithConstructibleTopology.map f) ↔ + @Continuous X Y (constructibleTopology X) (constructibleTopology Y) f := + WithTopology.map_continuous_iff (constructibleTopology X) (constructibleTopology Y) f + +lemma WithConstructibleTopology.map_continuous {f : X → Y} (hf : IsSpectralMap f) : + Continuous <| WithConstructibleTopology.map f := by + apply (map_continuous_iff f).2 + apply continuous_generateFrom_iff.mpr + intro s hs + obtain ⟨hso, hsc⟩ | ⟨hscl, hsc⟩ := hs + · exact (hf.isCompact_preimage_of_isOpen hso hsc).isOpen_constructibleTopology_of_isOpen + (hso.preimage hf.continuous) + · exact + (hf.isCompact_preimage_of_isOpen hscl.isOpen_compl hsc).isOpen_constructibleTopology_of_isClosed + (hscl.preimage hf.continuous) + +/-- +A spectral map between *quasi-separated* pre-spectral, sober spaces has compact fibers. +Note that any quasi-compact morphism of schemes has compact fibers, although the underlying +topological space of a schemes is not necessarily quasi-separated. +-/ +lemma IsSpectralMap.hasCompactFibers [PrespectralSpace X] [T0Space X] [QuasiSeparatedSpace X] + [QuasiSober X] [PrespectralSpace Y] [T0Space Y] [QuasiSeparatedSpace Y] [QuasiSober Y] + {f : X → Y} (hf : IsSpectralMap f) : HasCompactFibers f := by + intro y + -- Take a compact open neighbourhood U of y (exists since Y is prespectral) + obtain ⟨U, ⟨hUo, hUc⟩, (hyU : y ∈ U), -⟩ := + (PrespectralSpace.isTopologicalBasis (X := Y)).mem_nhds_iff.mp (isOpen_univ.mem_nhds trivial) + have hfUo : IsOpen (f ⁻¹' U) := hUo.preimage hf.continuous + have hfUc : IsCompact (f ⁻¹' U) := hf.isCompact_preimage_of_isOpen hUo hUc + have : CompactSpace (f ⁻¹' U) := isCompact_iff_compactSpace.mp hfUc + have : PrespectralSpace (f ⁻¹' U) := hfUo.isOpenEmbedding_subtypeVal.prespectralSpace + have : QuasiSeparatedSpace (f ⁻¹' U) := hfUo.isOpenEmbedding_subtypeVal.quasiSeparatedSpace + have : QuasiSober (f ⁻¹' U) := hfUo.isOpenEmbedding_subtypeVal.quasiSober + let g := f ∘ (Subtype.val : f ⁻¹' U → X) + have hg : IsSpectralMap g := hf.comp hfUo.isOpenEmbedding_subtypeVal.isSpectralMap_of_compactSpace + have heq : f ⁻¹' {y} = Subtype.val '' (g ⁻¹' {y}) := by grind [Subtype.exists] + rw [heq] + have hg1 := (WithTopology.map_continuous_iff (constructibleTopology (f ⁻¹' U)) + (constructibleTopology Y) g).1 <| WithConstructibleTopology.map_continuous hg + have h := @Continuous.comp (f ⁻¹' U) _ X (constructibleTopology (f ⁻¹' U)) _ _ id _ + continuous_subtype_val WithConstructibleTopology.continuous_constructibleTopology_id + letI := constructibleTopology { x // x ∈ f ⁻¹' U } + letI := constructibleTopology Y + exact (isClosed_singleton.preimage hg1).isCompact.image h diff --git a/Mathlib/Topology/WithTopology.lean b/Mathlib/Topology/WithTopology.lean index 7dd7ce8d8cc117..bcb1cde52311b5 100644 --- a/Mathlib/Topology/WithTopology.lean +++ b/Mathlib/Topology/WithTopology.lean @@ -5,6 +5,7 @@ Authors: Yury Kudryashov, Gemini CLI -/ module +public import Mathlib.Topology.Continuous public import Mathlib.Topology.Defs.Induced /-! @@ -83,6 +84,19 @@ lemma continuous_ofTopology : Continuous[_, t] (ofTopology (t := t)) := /-! ### Set-theoretic lemmas -/ +lemma ofTopology_comp_map_comp_toTopology + {Y : Type*} (s : TopologicalSpace Y) (f : X → Y) : + ofTopology ∘ map t s f ∘ toTopology t = f := by + ext + delta map + simp + +lemma map_continuous_iff {Y : Type*} (s : TopologicalSpace Y) (f : X → Y) : + (Continuous <| WithTopology.map t s f) ↔ @Continuous X Y t s f := + ⟨fun hf => ofTopology_comp_map_comp_toTopology t s f ▸ (continuous_ofTopology s).comp + (hf.comp (continuous_toTopology t)), fun hf => (continuous_toTopology s).comp + (hf.comp (continuous_ofTopology t))⟩ + open Set lemma image_ofTopology (s : Set (WithTopology X t)) : ofTopology '' s = toTopology t ⁻¹' s :=