# Ideals of continuous functions #

For a topological semiring `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 `ContinuousMap.setOfIdeal`

and
`ContinuousMap.idealOfSet`

. As long as `R`

is Hausdorff, `ContinuousMap.setOfIdeal I`

is open,
and if, in addition, `X`

is locally compact, then `ContinuousMap.setOfIdeal s`

is closed.

When `R = 𝕜`

with `RCLike 𝕜`

and `X`

is compact Hausdorff, then this Galois connection can be
improved to a true Galois correspondence (i.e., order isomorphism) between the type `opens X`

and
the subtype of closed ideals of `C(X, 𝕜)`

. Because we do not have a bundled type of closed ideals,
we simply register this as a Galois insertion between `Ideal C(X, 𝕜)`

and `opens X`

, which is
`ContinuousMap.idealOpensGI`

. Consequently, the maximal ideals of `C(X, 𝕜)`

are precisely those
ideals corresponding to (complements of) singletons in `X`

.

In addition, when `X`

is locally compact and `𝕜`

is a nontrivial topological integral domain, then
there is a natural continuous map from `X`

to `WeakDual.characterSpace 𝕜 C(X, 𝕜)`

given by point
evaluation, which is herein called `WeakDual.CharacterSpace.continuousMapEval`

. Again, when `X`

is
compact Hausdorff and `RCLike 𝕜`

, more can be obtained. In particular, in that context this map is
bijective, and since the domain is compact and the codomain is Hausdorff, it is a homeomorphism,
herein called `WeakDual.CharacterSpace.homeoEval`

.

## Main definitions #

`ContinuousMap.idealOfSet`

: ideal of functions which vanish on the complement of a set.`ContinuousMap.setOfIdeal`

: complement of the set on which all functions in the ideal vanish.`ContinuousMap.opensOfIdeal`

:`ContinuousMap.setOfIdeal`

as a term of`opens X`

.`ContinuousMap.idealOpensGI`

: The Galois insertion`ContinuousMap.opensOfIdeal`

and`fun s ↦ ContinuousMap.idealOfSet ↑s`

.`WeakDual.CharacterSpace.continuousMapEval`

: the natural continuous map from a locally compact topological space`X`

to the`WeakDual.characterSpace 𝕜 C(X, 𝕜)`

which sends`x : X`

to point evaluation at`x`

, with modest hypothesis on`𝕜`

.`WeakDual.CharacterSpace.homeoEval`

: this is`WeakDual.CharacterSpace.continuousMapEval`

upgraded to a homeomorphism when`X`

is compact Hausdorff and`RCLike 𝕜`

.

## Main statements #

`ContinuousMap.idealOfSet_ofIdeal_eq_closure`

: when`X`

is compact Hausdorff and`RCLike 𝕜`

,`idealOfSet 𝕜 (setOfIdeal I) = I.closure`

for any ideal`I : Ideal C(X, 𝕜)`

.`ContinuousMap.setOfIdeal_ofSet_eq_interior`

: when`X`

is compact Hausdorff and`RCLike 𝕜`

,`setOfIdeal (idealOfSet 𝕜 s) = interior s`

for any`s : Set X`

.`ContinuousMap.ideal_isMaximal_iff`

: when`X`

is compact Hausdorff and`RCLike 𝕜`

, a closed ideal of`C(X, 𝕜)`

is maximal if and only if it is`idealOfSet 𝕜 {x}ᶜ`

for some`x : X`

.

## Implementation details #

Because there does not currently exist a bundled type of closed ideals, we don't provide the actual
order isomorphism described above, and instead we only consider the Galois insertion
`ContinuousMap.idealOpensGI`

.

## Tags #

ideal, continuous function, compact, Hausdorff

Given a topological ring `R`

and `s : Set X`

, construct the ideal in `C(X, R)`

of functions
which vanish on the complement of `s`

.

## Equations

## Instances For

Given an ideal `I`

of `C(X, R)`

, construct the set of points for which every function in the
ideal vanishes on the complement.

## Equations

- ContinuousMap.setOfIdeal I = {x : X | ∀ f ∈ I, f x = 0}ᶜ

## Instances For

The open set `ContinuousMap.setOfIdeal I`

realized as a term of `opens X`

.

## Equations

- ContinuousMap.opensOfIdeal I = { carrier := ContinuousMap.setOfIdeal I, is_open' := ⋯ }

## Instances For

An auxiliary lemma used in the proof of `ContinuousMap.idealOfSet_ofIdeal_eq_closure`

which may
be useful on its own.

The Galois insertion `ContinuousMap.opensOfIdeal : Ideal C(X, 𝕜) → Opens X`

and
`fun s ↦ ContinuousMap.idealOfSet ↑s`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

The natural continuous map from a locally compact topological space `X`

to the
`WeakDual.characterSpace 𝕜 C(X, 𝕜)`

which sends `x : X`

to point evaluation at `x`

.

## Equations

- WeakDual.CharacterSpace.continuousMapEval X 𝕜 = { toFun := fun (x : X) => ⟨{ toFun := fun (f : C(X, 𝕜)) => f x, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }, ⋯⟩, continuous_toFun := ⋯ }

## Instances For

This is the natural homeomorphism between a compact Hausdorff space `X`

and the
`WeakDual.characterSpace 𝕜 C(X, 𝕜)`

.

## Equations

- WeakDual.CharacterSpace.homeoEval X 𝕜 = ⋯.homeoOfEquivCompactToT2