From b6fa3beb29f035598cf0434d919694c5e98091eb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 14 Mar 2022 07:05:51 +0000 Subject: [PATCH] move(topology/sets/*): Move topological types of sets together (#12648) Move * `topology.opens` to `topology.sets.opens` * `topology.compacts` to `topology.sets.closeds` and `topology.sets.compacts` `closeds` and `clopens` go into `topology.sets.closeds` and `compacts`, `nonempty_compacts`, `positive_compacts` and `compact_opens` go into `topology.sets.compacts`. --- .../prime_spectrum/basic.lean | 2 +- src/category_theory/sites/spaces.lean | 3 +- src/measure_theory/measure/content.lean | 3 +- src/order/category/Frame.lean | 2 +- src/topology/alexandroff.lean | 2 +- src/topology/algebra/group.lean | 2 +- src/topology/algebra/open_subgroup.lean | 2 +- src/topology/category/Top/opens.lean | 2 +- src/topology/local_homeomorph.lean | 2 +- src/topology/metric_space/closeds.lean | 4 +- src/topology/metric_space/kuratowski.lean | 2 +- src/topology/sets/closeds.lean | 107 ++++++++++++++++++ src/topology/{ => sets}/compacts.lean | 98 ++-------------- src/topology/{ => sets}/opens.lean | 0 14 files changed, 126 insertions(+), 105 deletions(-) create mode 100644 src/topology/sets/closeds.lean rename src/topology/{ => sets}/compacts.lean (75%) rename src/topology/{ => sets}/opens.lean (100%) diff --git a/src/algebraic_geometry/prime_spectrum/basic.lean b/src/algebraic_geometry/prime_spectrum/basic.lean index d897cbdd38d7d..6ffff5336db71 100644 --- a/src/algebraic_geometry/prime_spectrum/basic.lean +++ b/src/algebraic_geometry/prime_spectrum/basic.lean @@ -9,7 +9,7 @@ import ring_theory.nilpotent import ring_theory.localization.away import ring_theory.ideal.prod import ring_theory.ideal.over -import topology.opens +import topology.sets.opens import topology.sober /-! diff --git a/src/category_theory/sites/spaces.lean b/src/category_theory/sites/spaces.lean index 9d43018441294..cd20ac5cdb426 100644 --- a/src/category_theory/sites/spaces.lean +++ b/src/category_theory/sites/spaces.lean @@ -3,11 +3,10 @@ Copyright (c) 2020 Bhavik Mehta. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Bhavik Mehta -/ - -import topology.opens import category_theory.sites.grothendieck import category_theory.sites.pretopology import category_theory.limits.lattice +import topology.sets.opens /-! # Grothendieck topology on a topological space diff --git a/src/measure_theory/measure/content.lean b/src/measure_theory/measure/content.lean index 11ef4396c58a5..564efc8f0c46e 100644 --- a/src/measure_theory/measure/content.lean +++ b/src/measure_theory/measure/content.lean @@ -5,8 +5,7 @@ Authors: Floris van Doorn -/ import measure_theory.measure.measure_space import measure_theory.measure.regular -import topology.opens -import topology.compacts +import topology.sets.compacts /-! # Contents diff --git a/src/order/category/Frame.lean b/src/order/category/Frame.lean index 251124ca1c7df..eec23ec12ab06 100644 --- a/src/order/category/Frame.lean +++ b/src/order/category/Frame.lean @@ -6,7 +6,7 @@ Authors: Yaël Dillies import order.category.Lattice import order.hom.complete_lattice import topology.category.CompHaus -import topology.opens +import topology.sets.opens /-! # The category of frames diff --git a/src/topology/alexandroff.lean b/src/topology/alexandroff.lean index 2cfaedce9b4e1..085657d93d30c 100644 --- a/src/topology/alexandroff.lean +++ b/src/topology/alexandroff.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Yourong Zang, Yury Kudryashov -/ import topology.separation -import topology.opens +import topology.sets.opens /-! # The Alexandroff Compactification diff --git a/src/topology/algebra/group.lean b/src/topology/algebra/group.lean index 27f5f221b78ce..05cf482092542 100644 --- a/src/topology/algebra/group.lean +++ b/src/topology/algebra/group.lean @@ -6,8 +6,8 @@ Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot import group_theory.quotient_group import order.filter.pointwise import topology.algebra.monoid -import topology.compacts import topology.compact_open +import topology.sets.compacts /-! # Theory of topological groups diff --git a/src/topology/algebra/open_subgroup.lean b/src/topology/algebra/open_subgroup.lean index 33c4db3528acc..145f6a278c965 100644 --- a/src/topology/algebra/open_subgroup.lean +++ b/src/topology/algebra/open_subgroup.lean @@ -3,9 +3,9 @@ Copyright (c) 2019 Johan Commelin All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Johan Commelin -/ -import topology.opens import topology.algebra.ring import topology.algebra.filter_basis +import topology.sets.opens /-! # Open subgroups of a topological groups diff --git a/src/topology/category/Top/opens.lean b/src/topology/category/Top/opens.lean index 1b246724a5f3e..2e2bd928bf36b 100644 --- a/src/topology/category/Top/opens.lean +++ b/src/topology/category/Top/opens.lean @@ -3,10 +3,10 @@ Copyright (c) 2019 Scott Morrison. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison -/ -import topology.opens import category_theory.category.preorder import category_theory.eq_to_hom import topology.category.Top.epi_mono +import topology.sets.opens /-! # The category of open sets in a topological space. diff --git a/src/topology/local_homeomorph.lean b/src/topology/local_homeomorph.lean index dcc3753838f65..805023c7f224c 100644 --- a/src/topology/local_homeomorph.lean +++ b/src/topology/local_homeomorph.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Sébastien Gouëzel -/ import data.equiv.local_equiv -import topology.opens +import topology.sets.opens /-! # Local homeomorphisms diff --git a/src/topology/metric_space/closeds.lean b/src/topology/metric_space/closeds.lean index be57dbe91a451..cd28bf7ef0360 100644 --- a/src/topology/metric_space/closeds.lean +++ b/src/topology/metric_space/closeds.lean @@ -3,9 +3,9 @@ Copyright (c) 2019 Sébastien Gouëzel. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sébastien Gouëzel -/ -import topology.metric_space.hausdorff_distance -import topology.compacts import analysis.specific_limits +import topology.metric_space.hausdorff_distance +import topology.sets.compacts /-! # Closed subsets diff --git a/src/topology/metric_space/kuratowski.lean b/src/topology/metric_space/kuratowski.lean index 4314ab7cfdbd2..b0b5f91c9889c 100644 --- a/src/topology/metric_space/kuratowski.lean +++ b/src/topology/metric_space/kuratowski.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Sébastien Gouëzel -/ import analysis.normed_space.lp_space -import topology.compacts +import topology.sets.compacts /-! # The Kuratowski embedding diff --git a/src/topology/sets/closeds.lean b/src/topology/sets/closeds.lean new file mode 100644 index 0000000000000..0c1f1b10fced6 --- /dev/null +++ b/src/topology/sets/closeds.lean @@ -0,0 +1,107 @@ +/- +Copyright (c) 2020 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn, Yaël Dillies +-/ +import topology.sets.opens + +/-! +# Closed sets + +We define a few types of closed sets in a topological space. + +## Main Definitions + +For a topological space `α`, +* `closeds α`: The type of closed sets. +* `clopens α`: The type of clopen sets. +-/ + +open set + +variables {α β : Type*} [topological_space α] [topological_space β] + +namespace topological_space + +/-! ### Closed sets -/ + +/-- The type of closed subsets of a topological space. -/ +structure closeds (α : Type*) [topological_space α] := +(carrier : set α) +(closed' : is_closed carrier) + +namespace closeds +variables {α} + +instance : set_like (closeds α) α := +{ coe := closeds.carrier, + coe_injective' := λ s t h, by { cases s, cases t, congr' } } + +lemma closed (s : closeds α) : is_closed (s : set α) := s.closed' + +@[ext] protected lemma ext {s t : closeds α} (h : (s : set α) = t) : s = t := set_like.ext' h + +@[simp] lemma coe_mk (s : set α) (h) : (mk s h : set α) = s := rfl + +instance : has_sup (closeds α) := ⟨λ s t, ⟨s ∪ t, s.closed.union t.closed⟩⟩ +instance : has_inf (closeds α) := ⟨λ s t, ⟨s ∩ t, s.closed.inter t.closed⟩⟩ +instance : has_top (closeds α) := ⟨⟨univ, is_closed_univ⟩⟩ +instance : has_bot (closeds α) := ⟨⟨∅, is_closed_empty⟩⟩ + +instance : distrib_lattice (closeds α) := +set_like.coe_injective.distrib_lattice _ (λ _ _, rfl) (λ _ _, rfl) +instance : bounded_order (closeds α) := bounded_order.lift (coe : _ → set α) (λ _ _, id) rfl rfl + +/-- The type of closed sets is inhabited, with default element the empty set. -/ +instance : inhabited (closeds α) := ⟨⊥⟩ + +@[simp] lemma coe_sup (s t : closeds α) : (↑(s ⊔ t) : set α) = s ∪ t := rfl +@[simp] lemma coe_inf (s t : closeds α) : (↑(s ⊓ t) : set α) = s ∩ t := rfl +@[simp] lemma coe_top : (↑(⊤ : closeds α) : set α) = univ := rfl +@[simp] lemma coe_bot : (↑(⊥ : closeds α) : set α) = ∅ := rfl + +end closeds + +/-! ### Clopen sets -/ + +/-- The type of clopen sets of a topological space. -/ +structure clopens (α : Type*) [topological_space α] := +(carrier : set α) +(clopen' : is_clopen carrier) + +namespace clopens + +instance : set_like (clopens α) α := +{ coe := λ s, s.carrier, + coe_injective' := λ s t h, by { cases s, cases t, congr' } } + +lemma clopen (s : clopens α) : is_clopen (s : set α) := s.clopen' + +/-- Reinterpret a compact open as an open. -/ +@[simps] def to_opens (s : clopens α) : opens α := ⟨s, s.clopen.is_open⟩ + +@[ext] protected lemma ext {s t : clopens α} (h : (s : set α) = t) : s = t := set_like.ext' h + +@[simp] lemma coe_mk (s : set α) (h) : (mk s h : set α) = s := rfl + +instance : has_sup (clopens α) := ⟨λ s t, ⟨s ∪ t, s.clopen.union t.clopen⟩⟩ +instance : has_inf (clopens α) := ⟨λ s t, ⟨s ∩ t, s.clopen.inter t.clopen⟩⟩ +instance : has_top (clopens α) := ⟨⟨⊤, is_clopen_univ⟩⟩ +instance : has_bot (clopens α) := ⟨⟨⊥, is_clopen_empty⟩⟩ +instance : has_sdiff (clopens α) := ⟨λ s t, ⟨s \ t, s.clopen.diff t.clopen⟩⟩ +instance : has_compl (clopens α) := ⟨λ s, ⟨sᶜ, s.clopen.compl⟩⟩ + +instance : boolean_algebra (clopens α) := +set_like.coe_injective.boolean_algebra _ (λ _ _, rfl) (λ _ _, rfl) rfl rfl (λ _, rfl) (λ _ _, rfl) + +@[simp] lemma coe_sup (s t : clopens α) : (↑(s ⊔ t) : set α) = s ∪ t := rfl +@[simp] lemma coe_inf (s t : clopens α) : (↑(s ⊓ t) : set α) = s ∩ t := rfl +@[simp] lemma coe_top : (↑(⊤ : clopens α) : set α) = univ := rfl +@[simp] lemma coe_bot : (↑(⊥ : clopens α) : set α) = ∅ := rfl +@[simp] lemma coe_sdiff (s t : clopens α) : (↑(s \ t) : set α) = s \ t := rfl +@[simp] lemma coe_compl (s : clopens α) : (↑sᶜ : set α) = sᶜ := rfl + +instance : inhabited (clopens α) := ⟨⊥⟩ + +end clopens +end topological_space diff --git a/src/topology/compacts.lean b/src/topology/sets/compacts.lean similarity index 75% rename from src/topology/compacts.lean rename to src/topology/sets/compacts.lean index 55792a1bb9f14..2f4afb8f5b0b8 100644 --- a/src/topology/compacts.lean +++ b/src/topology/sets/compacts.lean @@ -3,23 +3,21 @@ Copyright (c) 2020 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn, Yaël Dillies -/ -import topology.opens +import topology.sets.closeds /-! # Compact sets -We define a few types of sets in a topological space. +We define a few types of compact sets in a topological space. ## Main Definitions For a topological space `α`, -- `closeds α`: The type of closed sets. -- `compacts α`: The type of compact sets. -- `nonempty_compacts α`: The type of non-empty compact sets. -- `positive_compacts α`: The type of compact sets with non-empty interior. -- `clopens α`: The type of clopen sets. -- `compact_opens α`: The type of compact open sets. This is a central object of study in the - context of spectral spaces. +* `compacts α`: The type of compact sets. +* `nonempty_compacts α`: The type of non-empty compact sets. +* `positive_compacts α`: The type of compact sets with non-empty interior. +* `compact_opens α`: The type of compact open sets. This is a central object in the study of + spectral spaces. -/ open set @@ -28,45 +26,6 @@ variables {α β : Type*} [topological_space α] [topological_space β] namespace topological_space -/-! ### Closed sets -/ - -/-- The type of closed subsets of a topological space. -/ -structure closeds (α : Type*) [topological_space α] := -(carrier : set α) -(closed' : is_closed carrier) - -namespace closeds -variables {α} - -instance : set_like (closeds α) α := -{ coe := closeds.carrier, - coe_injective' := λ s t h, by { cases s, cases t, congr' } } - -lemma closed (s : closeds α) : is_closed (s : set α) := s.closed' - -@[ext] protected lemma ext {s t : closeds α} (h : (s : set α) = t) : s = t := set_like.ext' h - -@[simp] lemma coe_mk (s : set α) (h) : (mk s h : set α) = s := rfl - -instance : has_sup (closeds α) := ⟨λ s t, ⟨s ∪ t, s.closed.union t.closed⟩⟩ -instance : has_inf (closeds α) := ⟨λ s t, ⟨s ∩ t, s.closed.inter t.closed⟩⟩ -instance : has_top (closeds α) := ⟨⟨univ, is_closed_univ⟩⟩ -instance : has_bot (closeds α) := ⟨⟨∅, is_closed_empty⟩⟩ - -instance : distrib_lattice (closeds α) := -set_like.coe_injective.distrib_lattice _ (λ _ _, rfl) (λ _ _, rfl) -instance : bounded_order (closeds α) := bounded_order.lift (coe : _ → set α) (λ _ _, id) rfl rfl - -/-- The type of closed sets is inhabited, with default element the empty set. -/ -instance : inhabited (closeds α) := ⟨⊥⟩ - -@[simp] lemma coe_sup (s t : closeds α) : (↑(s ⊔ t) : set α) = s ∪ t := rfl -@[simp] lemma coe_inf (s t : closeds α) : (↑(s ⊓ t) : set α) = s ∩ t := rfl -@[simp] lemma coe_top : (↑(⊤ : closeds α) : set α) = univ := rfl -@[simp] lemma coe_bot : (↑(⊥ : closeds α) : set α) = ∅ := rfl - -end closeds - /-! ### Compact sets -/ /-- The type of compact sets of a topological space. -/ @@ -240,49 +199,6 @@ let ⟨s, hs⟩ := exists_compact_subset is_open_univ $ mem_univ (classical.arbi end positive_compacts -/-! ### Clopen sets -/ - -/-- The type of clopen sets of a topological space. -/ -structure clopens (α : Type*) [topological_space α] := -(carrier : set α) -(clopen' : is_clopen carrier) - -namespace clopens - -instance : set_like (clopens α) α := -{ coe := λ s, s.carrier, - coe_injective' := λ s t h, by { cases s, cases t, congr' } } - -lemma clopen (s : clopens α) : is_clopen (s : set α) := s.clopen' - -/-- Reinterpret a compact open as an open. -/ -@[simps] def to_opens (s : clopens α) : opens α := ⟨s, s.clopen.is_open⟩ - -@[ext] protected lemma ext {s t : clopens α} (h : (s : set α) = t) : s = t := set_like.ext' h - -@[simp] lemma coe_mk (s : set α) (h) : (mk s h : set α) = s := rfl - -instance : has_sup (clopens α) := ⟨λ s t, ⟨s ∪ t, s.clopen.union t.clopen⟩⟩ -instance : has_inf (clopens α) := ⟨λ s t, ⟨s ∩ t, s.clopen.inter t.clopen⟩⟩ -instance : has_top (clopens α) := ⟨⟨⊤, is_clopen_univ⟩⟩ -instance : has_bot (clopens α) := ⟨⟨⊥, is_clopen_empty⟩⟩ -instance : has_sdiff (clopens α) := ⟨λ s t, ⟨s \ t, s.clopen.diff t.clopen⟩⟩ -instance : has_compl (clopens α) := ⟨λ s, ⟨sᶜ, s.clopen.compl⟩⟩ - -instance : boolean_algebra (clopens α) := -set_like.coe_injective.boolean_algebra _ (λ _ _, rfl) (λ _ _, rfl) rfl rfl (λ _, rfl) (λ _ _, rfl) - -@[simp] lemma coe_sup (s t : clopens α) : (↑(s ⊔ t) : set α) = s ∪ t := rfl -@[simp] lemma coe_inf (s t : clopens α) : (↑(s ⊓ t) : set α) = s ∩ t := rfl -@[simp] lemma coe_top : (↑(⊤ : clopens α) : set α) = univ := rfl -@[simp] lemma coe_bot : (↑(⊥ : clopens α) : set α) = ∅ := rfl -@[simp] lemma coe_sdiff (s t : clopens α) : (↑(s \ t) : set α) = s \ t := rfl -@[simp] lemma coe_compl (s : clopens α) : (↑sᶜ : set α) = sᶜ := rfl - -instance : inhabited (clopens α) := ⟨⊥⟩ - -end clopens - /-! ### Compact open sets -/ /-- The type of compact open sets of a topological space. This is useful in non Hausdorff contexts, diff --git a/src/topology/opens.lean b/src/topology/sets/opens.lean similarity index 100% rename from src/topology/opens.lean rename to src/topology/sets/opens.lean