# Commit 2022-10-08 00:38 54f74fc8

View on Github โ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.