English
There is a dual-order isomorphism between the lattice of nuclei on X and the lattice of sublocales of X.
Русский
Существует дуально-упорядоченное изоморфизм между решёткой нуклеусов на X и решёткой сублокал на X.
LaTeX
$$$(Nucleus\,X)^{\mathrm{op}} \cong_{\mathrm{ord}} Sublocale(X)$$$
Lean4
/-- The nuclei on a frame corresponds exactly to the sublocales on this frame.
The sublocales are ordered dually to the nuclei. -/
def nucleusIsoSublocale : (Nucleus X)ᵒᵈ ≃o Sublocale X
where
toFun n := n.ofDual.toSublocale
invFun s := .toDual s.toNucleus
left_inv := by simp [Function.LeftInverse, Nucleus.ext_iff]
right_inv S := by ext x; simpa using ⟨by simp +contextual [eq_comm], fun hx ↦ ⟨x, by simp [hx]⟩⟩
map_rel_iff' := by simp
