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 ofX
.JacobsonSpace.discreteTopology
: IfX
only has finitely many closed points, then the topology onX
is discrete.
References #
@[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
theorem
jacobsonSpace_iff
(X : Type u_1)
[TopologicalSpace X]
:
JacobsonSpace X ↔ ∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z
The class of jacobson spaces, i.e. spaces such that the set of closed points are dense in every closed subspace.
Instances
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)
:
theorem
JacobsonSpace.of_isClosedEmbedding
{X : Type u_2}
{Y : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
[JacobsonSpace Y]
(hf : IsClosedEmbedding f)
:
theorem
JacobsonSpace.discreteTopology
{X : Type u_1}
[TopologicalSpace X]
[JacobsonSpace X]
(h : (closedPoints X).Finite)
:
@[instance 100]
instance
instDiscreteTopologyOfFiniteOfJacobsonSpace
{X : Type u_1}
[TopologicalSpace X]
[Finite X]
[JacobsonSpace X]
:
Equations
- ⋯ = ⋯
@[instance 100]
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)