English
The closed irreducible subsets of a sober space are in bijective correspondence with the points of the space.
Русский
Замкнутые неразложимые подмножества собственного пространства образуют биекцию с точками пространства.
LaTeX
$$$\\text{IrrClos}(\\alpha) \\cong_o \\alpha$,\\; C \\mapsto \\text{genericPoint}(C),\\; x \\mapsto \\overline{\\{x\\}}.$$$
Lean4
/-- The closed irreducible subsets of a sober space bijects with the points of the space. -/
noncomputable def irreducibleSetEquivPoints [QuasiSober α] [T0Space α] : TopologicalSpace.IrreducibleCloseds α ≃o α
where
toFun s := s.2.genericPoint
invFun x := ⟨closure ({ x } : Set α), isIrreducible_singleton.closure, isClosed_closure⟩
left_inv
s := by
refine TopologicalSpace.IrreducibleCloseds.ext ?_
simp only [IsIrreducible.genericPoint_closure_eq, TopologicalSpace.IrreducibleCloseds.coe_mk,
closure_eq_iff_isClosed.mpr s.3]
rfl
right_inv
x :=
isIrreducible_singleton.closure.isGenericPoint_genericPoint_closure.eq
(by rw [closure_closure]; exact isGenericPoint_closure)
map_rel_iff' := by
rintro ⟨s, hs, hs'⟩ ⟨t, ht, ht'⟩
refine specializes_iff_closure_subset.trans ?_
simp
rfl
