English
The open-sets to ideals correspondence is established via the prespectral structure.
Русский
Существование связи между открытыми множествами и идеалами через prespectral-структуру.
LaTeX
$$$\\text{OpensEquiv}_{X} : \\mathrm{Opens}(X) \\to \\mathrm{Ideal}(\\mathrm{CompactOpens}(X))$ является изоморфизмом частичной упорядоченности.$$
Lean4
/-- In a prespectral space, the lattice of opens is determined by its lattice of compact opens. -/
def opensEquiv [PrespectralSpace X] : Opens X ≃o Order.Ideal (CompactOpens X)
where
toFun
U :=
⟨⟨{V | (V : Set X) ⊆ U}, fun U₁ U₂ h₁ h₂ ↦ subset_trans (α := Set X) h₁ h₂⟩, ⟨⊥, by simp⟩, fun U₁ h₁ U₂ h₂ ↦
⟨U₁ ⊔ U₂, by aesop, le_sup_left, le_sup_right⟩⟩
invFun I := ⨆ U ∈ I, U.toOpens
left_inv
U := by
apply le_antisymm
· simp only [iSup_le_iff]
exact fun _ ↦ id
· intro x hxU
obtain ⟨V, ⟨h₁, h₂⟩, hxV, hVU⟩ := isTopologicalBasis.exists_subset_of_mem_open hxU U.2
simp only [Opens.mem_iSup, SetLike.mem_coe]
exact ⟨⟨⟨_, h₂⟩, h₁⟩, hVU, hxV⟩
right_inv
I := by
ext U
dsimp
change U.toOpens ≤ _ ↔ _
refine ⟨fun H ↦ ?_, fun h ↦ le_iSup₂ (f := fun U (h : U ∈ I) ↦ U.toOpens) U h⟩
simp only [← SetLike.coe_subset_coe, Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_mk] at H
obtain ⟨s, hsI, hs, hU⟩ := U.isCompact.elim_finite_subcover_image (fun U _ ↦ U.2) H
exact I.lower (a := hs.toFinset.sup fun i ↦ i) (by simpa [← SetLike.coe_subset_coe]) (by simpa)
map_rel_iff'
{U V} := by
change (∀ (W : CompactOpens X), (W : Set X) ⊆ U → (W : Set X) ⊆ V) ↔ U ≤ V
refine ⟨?_, fun H W ↦ (le_trans · H)⟩
intro H x hxU
obtain ⟨W, ⟨h₁, h₂⟩, hxW, hWU⟩ := isTopologicalBasis.exists_subset_of_mem_open hxU U.2
exact H ⟨⟨W, h₂⟩, h₁⟩ hWU hxW
