English
There is a Galois insertion between the lattice of open sets Opens X and the lattice of ideals of the function algebra C(X, 𝕜), given by s ↦ idealOfSet 𝕜 s and I ↦ opensOfIdeal I.
Русский
Существует вставка Гало между решётками открытых множеств Opens X и идеалов в алгебре функций C(X, 𝕜); карты обмена: s ↦ идеалFromSet 𝕜 s и I ↦ opensOfIdeal I.
LaTeX
$$$\\text{There exists a Galois insertion }\\mathrm{GI}=\\big( opensOfIdeal : Ideal(C(X, 𝕜)) \\to Opens X,\\; s \\mapsto \\mathrm{idealOfSet}(𝕜, s) : Opens X \\to Ideal(C(X, 𝕜)) \\big).$$$
Lean4
/-- The Galois insertion `ContinuousMap.opensOfIdeal : Ideal C(X, 𝕜) → Opens X` and
`fun s ↦ ContinuousMap.idealOfSet ↑s`. -/
@[simps]
def idealOpensGI : GaloisInsertion (opensOfIdeal : Ideal C(X, 𝕜) → Opens X) fun s => idealOfSet 𝕜 s
where
choice I _ := opensOfIdeal I.closure
gc I s := ideal_gc X 𝕜 I s
le_l_u s := (setOfIdeal_ofSet_of_isOpen 𝕜 s.isOpen).ge
choice_eq I
hI :=
congr_arg _ <|
Ideal.ext
(Set.ext_iff.mp
(isClosed_of_closure_subset <| (idealOfSet_ofIdeal_eq_closure I ▸ hI : I.closure ≤ I)).closure_eq)
