Commit 2022-10-08 00:38 54f74fc8

feat(topology/continuous_function/ideals): construct the Galois correspondence between closed ideals in C(X, 𝕜) and open sets in X (#16677) For a topological ring R and a topological space X there is a Galois connection between ideal C(X, R) and set X given by sending each I : ideal C(X, R) to {x : X | ∀ f ∈ I, f x = 0}ᶜ and mapping s : set X to the ideal with carrier {f : C(X, R) | ∀ x ∈ sᶜ, f x = 0}, and we call these maps continuous_map.set_of_ideal and continuous_map.ideal_of_set. As long as R is Hausdorff, continuous_map.set_of_ideal I is open, and if, in addition, X is locally compact, then continuous_map.set_of_ideal s is closed.