Constructible topology

In this file we define the constructible topology on a topological space. This is the topology generated by compact open subsets and their complements.

Main definitions and results

• WithConstructibleTopology: X equipped with its constructible topology.
• compactSpace_withConstructibleTopology: If X is quasi-separated, quasi-sober, prespectral and quasi-compact, then X is still quasi-compact in the constructible topology.

TODOs

• If X is a spectral space, show that X is T2 and totally disconnected (@chrisflav).

def constructibleTopologySubbasis (X : Type u_2) [TopologicalSpace X] : Set (Set X)

The subbasis of the constructible topology on a topological space X: It consists of the open and compact sets of X and their complements.

Equations

• constructibleTopologySubbasis X = {s : Set X | IsOpen s ∧ IsCompact s} ∪ {s : Set X | IsClosed s ∧ IsCompact sᶜ}

@[instance_reducible]

def constructibleTopology (X : Type u_2) [TopologicalSpace X] : TopologicalSpace X

The constructible topology on a topological space X has as a subbasis the open and compact sets of X and their complements.

Equations

• constructibleTopology X = TopologicalSpace.generateFrom (constructibleTopologySubbasis X)

@[reducible, inline]

abbrev WithConstructibleTopology (X : Type u_2) [TopologicalSpace X] : Type u_2

A type synonym for X that is equipped with the constructible topology of X.

Equations

• WithConstructibleTopology X = WithTopology X (constructibleTopology X)

@[simp]

theorem empty_mem_constructibleTopologySubbasis (X : Type u_1) [TopologicalSpace X] : ∅ ∈ constructibleTopologySubbasis X

theorem WithConstructibleTopology.isOpen_iff {X : Type u_1} [TopologicalSpace X] {s : Set (WithConstructibleTopology X)} : IsOpen s ↔ IsOpen (WithTopology.toTopology (constructibleTopology X) ⁻¹' s)

theorem WithConstructibleTopology.isClosed_iff {X : Type u_1} [TopologicalSpace X] {s : Set (WithConstructibleTopology X)} : IsClosed s ↔ IsClosed (WithTopology.toTopology (constructibleTopology X) ⁻¹' s)

theorem IsCompact.isOpen_constructibleTopology_of_isOpen {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (ho : IsOpen s) : IsOpen s

theorem IsCompact.isOpen_constructibleTopology_of_isClosed {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsCompact sᶜ) (ho : IsClosed s) : IsOpen s

theorem IsCompact.isClosed_constructibleTopology_of_isOpen {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (ho : IsOpen s) : IsClosed s

theorem IsCompact.isClosed_constructibleTopology_of_isClosed {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsCompact sᶜ) (ho : IsClosed s) : IsClosed s

theorem IsCompact.isClopen_constructibleTopology_of_isOpen {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (ho : IsOpen s) : IsClopen s

theorem IsCompact.isClopen_constructibleTopology_of_isClosed {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsCompact sᶜ) (ho : IsClosed s) : IsClopen s

@[simp]

theorem compl_mem_constructibleTopologySubbasis_iff {X : Type u_1} [TopologicalSpace X] {s : Set X} : sᶜ ∈ constructibleTopologySubbasis X ↔ s ∈ constructibleTopologySubbasis X

theorem compl_image_constructibleTopologySubbasis {X : Type u_1} [TopologicalSpace X] : compl '' constructibleTopologySubbasis X = constructibleTopologySubbasis X

theorem latticeClosure_constructibleTopologySubbasis {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [QuasiSeparatedSpace X] : latticeClosure (constructibleTopologySubbasis X) = {s : Set X | Topology.IsConstructible s}

theorem constructibleTopologySubbasis_subset_isConstructible {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [QuasiSeparatedSpace X] : constructibleTopologySubbasis X ⊆ {s : Set X | Topology.IsConstructible s}

theorem constructibleTopology_eq_generateFrom_isConstructible (X : Type u_1) [TopologicalSpace X] [CompactSpace X] [QuasiSeparatedSpace X] : constructibleTopology X = TopologicalSpace.generateFrom {s : Set X | Topology.IsConstructible s}

theorem isCompact_of_mem_constructibleTopologySubbasis {X : Type u_1} [TopologicalSpace X] [CompactSpace X] {s : Set X} (hs : s ∈ constructibleTopologySubbasis X) : IsCompact s

theorem isCompact_sInter_of_subset_constructibleTopologySubbasis {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [QuasiSeparatedSpace X] {s : Set (Set X)} (hs : s ⊆ constructibleTopologySubbasis X) (hf : s.Finite) : IsCompact (⋂₀ s)

instance compactSpace_withConstructibleTopology {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [QuasiSober X] [PrespectralSpace X] [QuasiSeparatedSpace X] : CompactSpace (WithConstructibleTopology X)

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.