Jacobson spaces

Main results

• JacobsonSpace: The class of jacobson spaces, i.e. spaces such that the set of closed points are dense in every closed subspace.
• jacobsonSpace_iff_locallyClosed: X is a jacobson space iff every locally closed subset contains a closed point of X.
• JacobsonSpace.discreteTopology: If X only has finitely many closed points, then the topology on X is discrete.

References

• https://stacks.math.columbia.edu/tag/005T

def closedPoints (X : Type u_1) [TopologicalSpace X] : Set X

The set of closed points.

Equations

• closedPoints X = {x : X | IsClosed {x}}

@[simp]

theorem mem_closedPoints_iff {X : Type u_1} [TopologicalSpace X] {x : X} : x ∈ closedPoints X ↔ IsClosed {x}

theorem preimage_closedPoints_subset {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Function.Injective f) (hf' : Continuous f) : f ⁻¹' closedPoints Y ⊆ closedPoints X

theorem IsClosedEmbedding.preimage_closedPoints {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) : f ⁻¹' closedPoints Y = closedPoints X

theorem closedPoints_eq_univ {X : Type u_1} [TopologicalSpace X] [T2Space X] : closedPoints X = Set.univ

class JacobsonSpace (X : Type u_1) [TopologicalSpace X] : Prop

The class of jacobson spaces, i.e. spaces such that the set of closed points are dense in every closed subspace.

• closure_inter_closedPoints : ∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z

theorem jacobsonSpace_iff (X : Type u_1) [TopologicalSpace X] : JacobsonSpace X ↔ ∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z

theorem JacobsonSpace.closure_inter_closedPoints {X : Type u_1} : ∀ {inst : TopologicalSpace X} [self : JacobsonSpace X] {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z

theorem closure_closedPoints {X : Type u_1} [TopologicalSpace X] [JacobsonSpace X] : closure (closedPoints X) = Set.univ

theorem jacobsonSpace_iff_locallyClosed {X : Type u_1} [TopologicalSpace X] : JacobsonSpace X ↔ ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty

theorem nonempty_inter_closedPoints {X : Type u_1} [TopologicalSpace X] [JacobsonSpace X] {Z : Set X} (hZ : Z.Nonempty) (hZ' : IsLocallyClosed Z) : (Z ∩ closedPoints X).Nonempty

theorem isClosed_singleton_of_isLocallyClosed_singleton {X : Type u_1} [TopologicalSpace X] [JacobsonSpace X] {x : X} (hx : IsLocallyClosed {x}) : IsClosed {x}

theorem IsOpenEmbedding.preimage_closedPoints {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsOpenEmbedding f) [JacobsonSpace Y] : f ⁻¹' closedPoints Y = closedPoints X

theorem JacobsonSpace.of_isOpenEmbedding {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} [JacobsonSpace Y] (hf : IsOpenEmbedding f) : JacobsonSpace X

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

theorem JacobsonSpace.discreteTopology {X : Type u_1} [TopologicalSpace X] [JacobsonSpace X] (h : (closedPoints X).Finite) : DiscreteTopology X

@[instance 100]

instance instDiscreteTopologyOfFiniteOfJacobsonSpace {X : Type u_1} [TopologicalSpace X] [Finite X] [JacobsonSpace X] : DiscreteTopology X

Equations

• ⋯ = ⋯

@[instance 100]

instance instJacobsonSpaceOfT2Space {X : Type u_1} [TopologicalSpace X] [T2Space X] : JacobsonSpace X

Equations

• ⋯ = ⋯

theorem jacobsonSpace_iff_of_iSup_eq_top {X : Type u_2} [TopologicalSpace X] {ι : Type u_1} {U : ι → TopologicalSpace.Opens X} (hU : iSup U = ⊤) : JacobsonSpace X ↔ ∀ (i : ι), JacobsonSpace ↥(U i)