Prespectral spaces

In this file, we define prespectral spaces as spaces whose lattice of compact opens forms a basis.

class PrespectralSpace (X : Type u_3) [TopologicalSpace X] : Prop

A space is prespectral if the lattice of compact opens forms a basis.

• isTopologicalBasis : TopologicalSpace.IsTopologicalBasis {U : Set X | IsOpen U ∧ IsCompact U}

theorem prespectralSpace_iff (X : Type u_3) [TopologicalSpace X] : PrespectralSpace X ↔ TopologicalSpace.IsTopologicalBasis {U : Set X | IsOpen U ∧ IsCompact U}

theorem PrespectralSpace.of_isTopologicalBasis {X : Type u_1} [TopologicalSpace X] {B : Set (Set X)} (basis : TopologicalSpace.IsTopologicalBasis B) (isCompact_basis : ∀ U ∈ B, IsCompact U) : PrespectralSpace X

A space is prespectral if it has a basis consisting of compact opens.

theorem PrespectralSpace.of_isTopologicalBasis' {X : Type u_1} [TopologicalSpace X] {ι : Type u_3} {b : ι → Set X} (basis : TopologicalSpace.IsTopologicalBasis (Set.range b)) (isCompact_basis : ∀ (i : ι), IsCompact (b i)) : PrespectralSpace X

A space is prespectral if it has a basis consisting of compact opens. This is the variant with an indexed basis instead.

@[instance 100]

instance instPrespectralSpaceOfNoetherianSpace {X : Type u_1} [TopologicalSpace X] [TopologicalSpace.NoetherianSpace X] : PrespectralSpace X

@[instance 100]

instance instLocallyCompactSpaceOfPrespectralSpace {X : Type u_1} [TopologicalSpace X] [PrespectralSpace X] : LocallyCompactSpace X

@[instance 100]

instance instTotallySeparatedSpaceOfT2SpaceOfPrespectralSpace {X : Type u_1} [TopologicalSpace X] [T2Space X] [PrespectralSpace X] : TotallySeparatedSpace X

theorem PrespectralSpace.of_isOpenCover {X : Type u_1} [TopologicalSpace X] {ι : Type u_3} {U : ι → TopologicalSpace.Opens X} (hU : TopologicalSpace.IsOpenCover U) [∀ (i : ι), PrespectralSpace ↥(U i)] : PrespectralSpace X

theorem PrespectralSpace.of_isInducing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [PrespectralSpace Y] (f : X → Y) (hf : Topology.IsInducing f) (hf' : IsSpectralMap f) : PrespectralSpace X

theorem PrespectralSpace.of_isClosedEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [PrespectralSpace Y] (f : X → Y) (hf : Topology.IsClosedEmbedding f) : PrespectralSpace X

theorem Topology.IsOpenEmbedding.prespectralSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [PrespectralSpace Y] {f : X → Y} (hf : IsOpenEmbedding f) : PrespectralSpace X

Let f : X → Y be an open embedding of topological spaces. If Y is a prespectral space (i.e., the quasi-compact opens of Y form a basis), then X is also a prespectral space.

instance PrespectralSpace.sigma {ι : Type u_3} (X : ι → Type u_4) [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), PrespectralSpace (X i)] : PrespectralSpace ((i : ι) × X i)

theorem PrespectralSpace.isBasis_opens (X : Type u_1) [TopologicalSpace X] [PrespectralSpace X] : TopologicalSpace.Opens.IsBasis {U : TopologicalSpace.Opens X | IsCompact ↑U}

def PrespectralSpace.opensEquiv {X : Type u_1} [TopologicalSpace X] [PrespectralSpace X] : TopologicalSpace.Opens X ≃o Order.Ideal (TopologicalSpace.CompactOpens X)

In a prespectral space, the lattice of opens is determined by its lattice of compact opens.

theorem IsOpenMap.exists_opens_image_eq_of_prespectralSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [PrespectralSpace X] {f : X → Y} (hfc : Continuous f) (h : IsOpenMap f) {U : Set Y} (hs : U ⊆ Set.range f) (hU : IsOpen U) (hc : IsCompact U) : ∃ (V : TopologicalSpace.Opens X), IsCompact V.carrier ∧ f '' ↑V = U

If X has a basis of compact opens and f : X → S is open, every compact open of S is the image of a compact open of X.

theorem PrespectralSpace.exists_isCompact_and_isOpen_between {X : Type u_1} [TopologicalSpace X] [PrespectralSpace X] {K U : Set X} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) : ∃ (W : Set X), IsCompact W ∧ IsOpen W ∧ K ⊆ W ∧ W ⊆ U

theorem PrespectralSpace.exists_isClosed_of_not_isPreirreducible {X : Type u_1} [TopologicalSpace X] [PrespectralSpace X] (Z : Set X) (hZ : ¬IsPreirreducible Z) : ∃ (A : Set X) (B : Set X), IsClosed A ∧ IsClosed B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty