Constructible sets #
This file defines constructible sets, which are morally sets in a topological space which we can make out of finite unions and intersections of open and closed sets.
Precisely, constructible sets are the boolean subalgebra generated by open retrocompact sets, where a set is retrocompact if its intersection with every compact open set is compact. In a locally noetherian space, all sets are retrocompact, in which case this boolean subalgebra is simply the one generated by the open sets.
Constructible sets are useful because the image of a constructible set under a finitely presented morphism of schemes is a constructible set (and this is not true at the level of varieties).
Main declarations #
IsRetrocompact: Predicate for a set to be retrocompact, namely to have its intersection with every compact open be compact.IsConstructible: Predicate for a set to be constructible, namely to belong to the boolean subalgebra generated by open retrocompact sets.IsLocallyConstructible: Predicate for a set to be locally constructible, namely to be partitionable along an open cover such that each of its parts is constructible in the respective open subspace.
retrocompact sets #
A retrocompact set is a set whose intersection with every compact open is compact.
Instances For
@[simp]
@[simp]
theorem
IsRetrocompact.union
{X : Type u_2}
[TopologicalSpace X]
{s t : Set X}
(hs : IsRetrocompact s)
(ht : IsRetrocompact t)
:
IsRetrocompact (s ∪ t)
theorem
IsRetrocompact.finsetSup
{X : Type u_2}
[TopologicalSpace X]
{ι : Type u_4}
{s : Finset ι}
{t : ι → Set X}
(ht : ∀ i ∈ s, IsRetrocompact (t i))
:
IsRetrocompact (s.sup t)
theorem
IsRetrocompact.finsetSup'
{X : Type u_2}
[TopologicalSpace X]
{ι : Type u_4}
{s : Finset ι}
{hs : s.Nonempty}
{t : ι → Set X}
(ht : ∀ i ∈ s, IsRetrocompact (t i))
:
IsRetrocompact (s.sup' hs t)
theorem
IsRetrocompact.iUnion
{ι : Sort u_1}
{X : Type u_2}
[TopologicalSpace X]
[Finite ι]
{f : ι → Set X}
(hf : ∀ (i : ι), IsRetrocompact (f i))
:
IsRetrocompact (⋃ (i : ι), f i)
theorem
IsRetrocompact.sUnion
{X : Type u_2}
[TopologicalSpace X]
{S : Set (Set X)}
(hS : S.Finite)
(hS' : ∀ s ∈ S, IsRetrocompact s)
:
IsRetrocompact (⋃₀ S)
theorem
IsRetrocompact.biUnion
{X : Type u_2}
[TopologicalSpace X]
{ι : Type u_4}
{f : ι → Set X}
{t : Set ι}
(ht : t.Finite)
(hf : ∀ i ∈ t, IsRetrocompact (f i))
:
IsRetrocompact (⋃ i ∈ t, f i)
theorem
IsRetrocompact.inter
{X : Type u_2}
[TopologicalSpace X]
{s t : Set X}
[T2Space X]
(hs : IsRetrocompact s)
(ht : IsRetrocompact t)
:
IsRetrocompact (s ∩ t)
theorem
IsRetrocompact.finsetInf
{X : Type u_2}
[TopologicalSpace X]
[T2Space X]
{ι : Type u_4}
{s : Finset ι}
{t : ι → Set X}
(ht : ∀ i ∈ s, IsRetrocompact (t i))
:
IsRetrocompact (s.inf t)
theorem
IsRetrocompact.finsetInf'
{X : Type u_2}
[TopologicalSpace X]
[T2Space X]
{ι : Type u_4}
{s : Finset ι}
{hs : s.Nonempty}
{t : ι → Set X}
(ht : ∀ i ∈ s, IsRetrocompact (t i))
:
IsRetrocompact (s.inf' hs t)
theorem
IsRetrocompact.iInter
{ι : Sort u_1}
{X : Type u_2}
[TopologicalSpace X]
[T2Space X]
[Finite ι]
{f : ι → Set X}
(hf : ∀ (i : ι), IsRetrocompact (f i))
:
IsRetrocompact (⋂ (i : ι), f i)
theorem
IsRetrocompact.sInter
{X : Type u_2}
[TopologicalSpace X]
[T2Space X]
{S : Set (Set X)}
(hS : S.Finite)
(hS' : ∀ s ∈ S, IsRetrocompact s)
:
IsRetrocompact (⋂₀ S)
theorem
IsRetrocompact.biInter
{X : Type u_2}
[TopologicalSpace X]
[T2Space X]
{ι : Type u_4}
{f : ι → Set X}
{t : Set ι}
(ht : t.Finite)
(hf : ∀ i ∈ t, IsRetrocompact (f i))
:
IsRetrocompact (⋂ i ∈ t, f i)
theorem
IsRetrocompact.inter_isOpen
{X : Type u_2}
[TopologicalSpace X]
{s t : Set X}
(hs : IsRetrocompact s)
(ht : IsRetrocompact t)
(htopen : IsOpen t)
:
IsRetrocompact (s ∩ t)
theorem
IsRetrocompact.isOpen_inter
{X : Type u_2}
[TopologicalSpace X]
{s t : Set X}
(hs : IsRetrocompact s)
(ht : IsRetrocompact t)
(hsopen : IsOpen s)
:
IsRetrocompact (s ∩ t)
theorem
IsRetrocompact_iff_isSpectralMap_subtypeVal
{X : Type u_2}
[TopologicalSpace X]
{s : Set X}
:
theorem
IsRetrocompact.image_of_isEmbedding
{X : Type u_2}
{Y : Type u_3}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{s : Set X}
(hs : IsRetrocompact s)
(hfemb : Topology.IsEmbedding f)
(hfcomp : IsRetrocompact (Set.range f))
:
IsRetrocompact (f '' s)
theorem
IsRetrocompact.preimage_of_isOpenEmbedding
{X : Type u_2}
{Y : Type u_3}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{s : Set Y}
(hf : Topology.IsOpenEmbedding f)
(hs : IsRetrocompact s)
:
IsRetrocompact (f ⁻¹' s)
Stacks Tag 005J (Extracted from the proof)
theorem
IsRetrocompact.preimage_of_isClosedEmbedding
{X : Type u_2}
{Y : Type u_3}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{s : Set Y}
(hf : Topology.IsClosedEmbedding f)
(hf' : IsCompact (Set.range f)ᶜ)
(hs : IsRetrocompact s)
:
IsRetrocompact (f ⁻¹' s)
Stacks Tag 09YE (Extracted from the proof)
Constructible sets #
A constructible set is a set that can be written as the finite union/finite intersection/complement of open retrocompact sets.
In other words, constructible sets form the boolean subalgebra generated by open retrocompact sets.
Equations
- Topology.IsConstructible s = (s ∈ BooleanSubalgebra.closure {U : Set X | IsOpen U ∧ IsRetrocompact U})
Instances For
@[simp]
@[simp]
theorem
Topology.IsConstructible.union
{X : Type u_2}
[TopologicalSpace X]
{s t : Set X}
:
IsConstructible s → IsConstructible t → IsConstructible (s ∪ t)
theorem
Topology.IsConstructible.inter
{X : Type u_2}
[TopologicalSpace X]
{s t : Set X}
:
IsConstructible s → IsConstructible t → IsConstructible (s ∩ t)
theorem
Topology.IsConstructible.sdiff
{X : Type u_2}
[TopologicalSpace X]
{s t : Set X}
:
IsConstructible s → IsConstructible t → IsConstructible (s \ t)
theorem
Topology.IsConstructible.himp
{X : Type u_2}
[TopologicalSpace X]
{s t : Set X}
:
IsConstructible s → IsConstructible t → IsConstructible (s ⇨ t)
@[simp]
Alias of the forward direction of Topology.isConstructible_compl.
Alias of the reverse direction of Topology.isConstructible_compl.
theorem
Topology.IsConstructible.iUnion
{ι : Sort u_1}
{X : Type u_2}
[TopologicalSpace X]
[Finite ι]
{f : ι → Set X}
(hf : ∀ (i : ι), IsConstructible (f i))
:
IsConstructible (⋃ (i : ι), f i)
theorem
Topology.IsConstructible.iInter
{ι : Sort u_1}
{X : Type u_2}
[TopologicalSpace X]
[Finite ι]
{f : ι → Set X}
(hf : ∀ (i : ι), IsConstructible (f i))
:
IsConstructible (⋂ (i : ι), f i)
theorem
Topology.IsConstructible.sUnion
{X : Type u_2}
[TopologicalSpace X]
{S : Set (Set X)}
(hS : S.Finite)
(hS' : ∀ s ∈ S, IsConstructible s)
:
IsConstructible (⋃₀ S)
theorem
Topology.IsConstructible.sInter
{X : Type u_2}
[TopologicalSpace X]
{S : Set (Set X)}
(hS : S.Finite)
(hS' : ∀ s ∈ S, IsConstructible s)
:
IsConstructible (⋂₀ S)
theorem
Topology.IsConstructible.biUnion
{X : Type u_2}
[TopologicalSpace X]
{ι : Type u_4}
{f : ι → Set X}
{t : Set ι}
(ht : t.Finite)
(hf : ∀ i ∈ t, IsConstructible (f i))
:
IsConstructible (⋃ i ∈ t, f i)
theorem
Topology.IsConstructible.biInter
{X : Type u_2}
[TopologicalSpace X]
{ι : Type u_4}
{f : ι → Set X}
{t : Set ι}
(ht : t.Finite)
(hf : ∀ i ∈ t, IsConstructible (f i))
:
IsConstructible (⋂ i ∈ t, f i)
theorem
IsRetrocompact.isConstructible
{X : Type u_2}
[TopologicalSpace X]
{U : Set X}
(hUopen : IsOpen U)
(hUcomp : IsRetrocompact U)
:
theorem
Topology.IsConstructible.empty_union_induction
{X : Type u_2}
[TopologicalSpace X]
{p : (s : Set X) → IsConstructible s → Prop}
(open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen U) (hUcomp : IsRetrocompact U), p U ⋯)
(union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), p s hs → p t ht → p (s ∪ t) ⋯)
(compl : ∀ (s : Set X) (hs : IsConstructible s), p s hs → p sᶜ ⋯)
{s : Set X}
(hs : IsConstructible s)
:
p s hs
An induction principle for constructible sets. If p holds for all open retrocompact
sets, and is preserved under union and complement, then p holds for all constructible sets.
theorem
Topology.IsConstructible.preimage
{X : Type u_2}
{Y : Type u_3}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{s : Set Y}
(hfcont : Continuous f)
(hf : ∀ (s : Set Y), IsRetrocompact s → IsRetrocompact (f ⁻¹' s))
(hs : IsConstructible s)
:
IsConstructible (f ⁻¹' s)
If f is continuous and is such that preimages of retrocompact sets are retrocompact, then
preimages of constructible sets are constructible.
theorem
Topology.IsConstructible.preimage_of_isOpenEmbedding
{X : Type u_2}
{Y : Type u_3}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{s : Set Y}
(hf : IsOpenEmbedding f)
(hs : IsConstructible s)
:
IsConstructible (f ⁻¹' s)
theorem
Topology.IsConstructible.preimage_of_isClosedEmbedding
{X : Type u_2}
{Y : Type u_3}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{s : Set Y}
(hf : IsClosedEmbedding f)
(hf' : IsCompact (Set.range f)ᶜ)
(hs : IsConstructible s)
:
IsConstructible (f ⁻¹' s)
theorem
Topology.IsConstructible.image_of_isOpenEmbedding
{X : Type u_2}
{Y : Type u_3}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{s : Set X}
(hfopen : IsOpenEmbedding f)
(hfcomp : IsRetrocompact (Set.range f))
(hs : IsConstructible s)
:
IsConstructible (f '' s)
theorem
Topology.IsConstructible.image_of_isClosedEmbedding
{X : Type u_2}
{Y : Type u_3}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{s : Set X}
(hf : IsClosedEmbedding f)
(hfcomp : IsRetrocompact (Set.range f)ᶜ)
(hs : IsConstructible s)
:
IsConstructible (f '' s)
theorem
Topology.isConstructible_preimage_iff_of_isOpenEmbedding
{X : Type u_2}
{Y : Type u_3}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{s : Set Y}
(hf : IsOpenEmbedding f)
(hfcomp : IsRetrocompact (Set.range f))
(hsf : s ⊆ Set.range f)
:
theorem
IsRetrocompact.isCompact
{X : Type u_2}
[TopologicalSpace X]
{s : Set X}
[CompactSpace X]
(hs : IsRetrocompact s)
:
theorem
TopologicalSpace.IsTopologicalBasis.isRetrocompact_iff_isCompact'
{X : Type u_2}
[TopologicalSpace X]
{U : Set X}
[CompactSpace X]
{B : Set (Set X)}
[QuasiSeparatedSpace X]
(basis : IsTopologicalBasis B)
(isCompact_basis : ∀ U ∈ B, IsCompact U)
(hU : IsOpen U)
:
Variant of TopologicalSpace.IsTopologicalBasis.isRetrocompact_iff_isCompact for a
non-indexed topological basis.
Stacks Tag 0069 (Iff form of (2). Note that Stacks doesn't define quasi-separated spaces.)
theorem
TopologicalSpace.IsTopologicalBasis.isRetrocompact_iff_isCompact
{ι : Sort u_1}
{X : Type u_2}
[TopologicalSpace X]
{U : Set X}
[CompactSpace X]
{b : ι → Set X}
[QuasiSeparatedSpace X]
(basis : IsTopologicalBasis (Set.range b))
(isCompact_basis : ∀ (i : ι), IsCompact (b i))
(hU : IsOpen U)
:
Stacks Tag 0069 (Iff form of (2). Note that Stacks doesn't define quasi-separated spaces.)
theorem
TopologicalSpace.IsTopologicalBasis.isRetrocompact'
{X : Type u_2}
[TopologicalSpace X]
{U : Set X}
[CompactSpace X]
{B : Set (Set X)}
[QuasiSeparatedSpace X]
(basis : IsTopologicalBasis B)
(isCompact_basis : ∀ U ∈ B, IsCompact U)
(hU : U ∈ B)
:
Variant of TopologicalSpace.IsTopologicalBasis.isRetrocompact for a non-indexed topological
basis.
theorem
TopologicalSpace.IsTopologicalBasis.isRetrocompact
{ι : Sort u_1}
{X : Type u_2}
[TopologicalSpace X]
[CompactSpace X]
{b : ι → Set X}
[QuasiSeparatedSpace X]
(basis : IsTopologicalBasis (Set.range b))
(isCompact_basis : ∀ (i : ι), IsCompact (b i))
(i : ι)
:
IsRetrocompact (b i)
theorem
TopologicalSpace.IsTopologicalBasis.isConstructible'
{X : Type u_2}
[TopologicalSpace X]
{U : Set X}
[CompactSpace X]
{B : Set (Set X)}
[QuasiSeparatedSpace X]
(basis : IsTopologicalBasis B)
(isCompact_basis : ∀ U ∈ B, IsCompact U)
(hU : U ∈ B)
:
Variant of TopologicalSpace.IsTopologicalBasis.isConstructible for a non-indexed topological
basis.
theorem
TopologicalSpace.IsTopologicalBasis.isConstructible
{ι : Sort u_1}
{X : Type u_2}
[TopologicalSpace X]
[CompactSpace X]
{b : ι → Set X}
[QuasiSeparatedSpace X]
(basis : IsTopologicalBasis (Set.range b))
(isCompact_basis : ∀ (i : ι), IsCompact (b i))
(i : ι)
:
Topology.IsConstructible (b i)
theorem
Topology.IsConstructible.induction_of_isTopologicalBasis
{X : Type u_2}
[TopologicalSpace X]
[CompactSpace X]
{P : (s : Set X) → IsConstructible s → Prop}
[QuasiSeparatedSpace X]
{ι : Type u_4}
[Nonempty ι]
(b : ι → Set X)
(basis : TopologicalSpace.IsTopologicalBasis (Set.range b))
(isCompact_basis : ∀ (i : ι), IsCompact (b i))
(sdiff : ∀ (i : ι) (s : Set ι) (hs : s.Finite), P (b i \ ⋃ j ∈ s, b j) ⋯)
(union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), P s hs → P t ht → P (s ∪ t) ⋯)
(s : Set X)
(hs : IsConstructible s)
:
P s hs
Locally constructible sets #
A set in a topological space is locally constructible, if every point has a neighborhood on which the set is constructible.
Equations
- Topology.IsLocallyConstructible s = ∀ (x : X), ∃ U ∈ nhds x, IsOpen U ∧ Topology.IsConstructible (Subtype.val ⁻¹' s)
Instances For
theorem
Topology.IsConstructible.isLocallyConstructible
{X : Type u_2}
[TopologicalSpace X]
{s : Set X}
(hs : IsConstructible s)
:
theorem
IsRetrocompact.isLocallyConstructible
{X : Type u_2}
[TopologicalSpace X]
{U : Set X}
(hUopen : IsOpen U)
(hUcomp : IsRetrocompact U)
:
@[simp]
@[simp]
theorem
Topology.IsLocallyConstructible.inter
{X : Type u_2}
[TopologicalSpace X]
{s t : Set X}
(hs : IsLocallyConstructible s)
(ht : IsLocallyConstructible t)
:
IsLocallyConstructible (s ∩ t)
theorem
Topology.IsLocallyConstructible.finsetInf
{X : Type u_2}
[TopologicalSpace X]
{ι : Type u_4}
{s : Finset ι}
{t : ι → Set X}
(ht : ∀ i ∈ s, IsLocallyConstructible (t i))
:
IsLocallyConstructible (s.inf t)
theorem
Topology.IsLocallyConstructible.finsetInf'
{X : Type u_2}
[TopologicalSpace X]
{ι : Type u_4}
{s : Finset ι}
{hs : s.Nonempty}
{t : ι → Set X}
(ht : ∀ i ∈ s, IsLocallyConstructible (t i))
:
IsLocallyConstructible (s.inf' hs t)
theorem
Topology.IsLocallyConstructible.iInter
{ι : Sort u_1}
{X : Type u_2}
[TopologicalSpace X]
[Finite ι]
{f : ι → Set X}
(hf : ∀ (i : ι), IsLocallyConstructible (f i))
:
IsLocallyConstructible (⋂ (i : ι), f i)
theorem
Topology.IsLocallyConstructible.sInter
{X : Type u_2}
[TopologicalSpace X]
{S : Set (Set X)}
(hS : S.Finite)
(hS' : ∀ s ∈ S, IsLocallyConstructible s)
: