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

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.

Equations

• One or more equations did not get rendered due to their size.