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.

@[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 Topology.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] [T1Space X] : closedPoints X = Set.univ

theorem Set.Finite.isDiscrete_of_subset_closedPoints {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : s.Finite) (hs' : s ⊆ closedPoints X) : IsDiscrete s

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 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 JacobsonSpace.closure_inter_closedPoints_eq_closure {X : Type u_1} [TopologicalSpace X] [JacobsonSpace X] {S : Set X} (hS : IsLocallyClosed S) : closure (S ∩ closedPoints X) = closure S

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

theorem Topology.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 : Topology.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 : Topology.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

@[instance 100]

instance instJacobsonSpaceOfT1Space {X : Type u_1} [TopologicalSpace X] [T1Space X] : JacobsonSpace X

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

theorem subsingleton_image_closure_of_finite_of_isPreirreducible {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} [JacobsonSpace X] {S : Set X} (hS : IsLocallyClosed S) (hS' : IsPreirreducible S) (hf₁ : Continuous f) (hf₂ : IsClosedMap f) (hfS : (f '' S).Finite) : (f '' closure S).Subsingleton