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ᶜ}

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)

def 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 = X

@[implicit_reducible]

instance instTopologicalSpaceWithConstructibleTopology {X : Type u_1} [TopologicalSpace X] : TopologicalSpace (WithConstructibleTopology X)

Equations

• instTopologicalSpaceWithConstructibleTopology = constructibleTopology X

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

@[simp]

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

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.