# 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

def ContinuousMap.idealOfSet {X : Type u_1} (R : Type u_2) [] [] [] (s : Set X) :

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
• = { carrier := {f : C(X, R) | xs, f x = 0}, add_mem' := , zero_mem' := , smul_mem' := }
Instances For
theorem ContinuousMap.idealOfSet_closed {X : Type u_1} (R : Type u_2) [] [] [] [] (s : Set X) :
theorem ContinuousMap.mem_idealOfSet {X : Type u_1} {R : Type u_2} [] [] [] {s : Set X} {f : C(X, R)} :
∀ ⦃x : X⦄, x sf x = 0
theorem ContinuousMap.not_mem_idealOfSet {X : Type u_1} {R : Type u_2} [] [] [] {s : Set X} {f : C(X, R)} :
f xs, f x 0
def ContinuousMap.setOfIdeal {X : Type u_1} {R : Type u_2} [] [] [] (I : Ideal C(X, R)) :
Set X

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
• = {x : X | fI, f x = 0}
Instances For
theorem ContinuousMap.not_mem_setOfIdeal {X : Type u_1} {R : Type u_2} [] [] [] {I : Ideal C(X, R)} {x : X} :
∀ ⦃f : C(X, R)⦄, f If x = 0
theorem ContinuousMap.mem_setOfIdeal {X : Type u_1} {R : Type u_2} [] [] [] {I : Ideal C(X, R)} {x : X} :
fI, f x 0
theorem ContinuousMap.setOfIdeal_open {X : Type u_1} {R : Type u_2} [] [] [] [] (I : Ideal C(X, R)) :
@[simp]
theorem ContinuousMap.opensOfIdeal_coe {X : Type u_1} {R : Type u_2} [] [] [] [] (I : Ideal C(X, R)) :
def ContinuousMap.opensOfIdeal {X : Type u_1} {R : Type u_2} [] [] [] [] (I : Ideal C(X, R)) :

The open set ContinuousMap.setOfIdeal I realized as a term of opens X.

Equations
• = { carrier := , is_open' := }
Instances For
@[simp]
theorem ContinuousMap.setOfTop_eq_univ {X : Type u_1} {R : Type u_2} [] [] [] [] :
= Set.univ
@[simp]
theorem ContinuousMap.idealOfEmpty_eq_bot {X : Type u_1} {R : Type u_2} [] [] [] :
@[simp]
theorem ContinuousMap.mem_idealOfSet_compl_singleton {X : Type u_1} {R : Type u_2} [] [] [] (x : X) (f : C(X, R)) :
f f x = 0
theorem ContinuousMap.ideal_gc (X : Type u_1) (R : Type u_2) [] [] [] :
GaloisConnection ContinuousMap.setOfIdeal
theorem ContinuousMap.exists_mul_le_one_eqOn_ge {X : Type u_1} [] (f : ) {c : NNReal} (hc : 0 < c) :
∃ (g : ), (∀ (x : X), (g * f) x 1) Set.EqOn ((g * f)) 1 {x : X | c f x}

An auxiliary lemma used in the proof of ContinuousMap.idealOfSet_ofIdeal_eq_closure which may be useful on its own.

@[simp]
theorem ContinuousMap.idealOfSet_ofIdeal_eq_closure {X : Type u_1} {𝕜 : Type u_2} [] [] [] (I : Ideal C(X, 𝕜)) :
= I.closure
theorem ContinuousMap.idealOfSet_ofIdeal_isClosed {X : Type u_1} {𝕜 : Type u_2} [] [] [] {I : Ideal C(X, 𝕜)} (hI : IsClosed I) :
@[simp]
theorem ContinuousMap.setOfIdeal_ofSet_eq_interior {X : Type u_1} (𝕜 : Type u_2) [] [] [] [] (s : Set X) :
theorem ContinuousMap.setOfIdeal_ofSet_of_isOpen {X : Type u_1} (𝕜 : Type u_2) [] [] [] [] {s : Set X} (hs : ) :
@[simp]
theorem ContinuousMap.idealOpensGI_choice (X : Type u_1) (𝕜 : Type u_2) [] [] [] [] (I : Ideal C(X, 𝕜)) :
∀ (x : ), .choice I x = ContinuousMap.opensOfIdeal I.closure
def ContinuousMap.idealOpensGI (X : Type u_1) (𝕜 : Type u_2) [] [] [] [] :
GaloisInsertion ContinuousMap.opensOfIdeal fun (s : ) =>

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
theorem ContinuousMap.idealOfSet_isMaximal_iff {X : Type u_1} (𝕜 : Type u_2) [] [] [] [] (s : ) :
().IsMaximal
theorem ContinuousMap.idealOf_compl_singleton_isMaximal {X : Type u_1} (𝕜 : Type u_2) [] [] [] [] (x : X) :
().IsMaximal
theorem ContinuousMap.setOfIdeal_eq_compl_singleton {X : Type u_1} {𝕜 : Type u_2} [] [] [] [] (I : Ideal C(X, 𝕜)) [hI : I.IsMaximal] :
∃ (x : X),
theorem ContinuousMap.ideal_isMaximal_iff {X : Type u_1} {𝕜 : Type u_2} [] [] [] [] (I : Ideal C(X, 𝕜)) [hI : IsClosed I] :
I.IsMaximal ∃ (x : X), = I
def WeakDual.CharacterSpace.continuousMapEval (X : Type u_1) (𝕜 : Type u_2) [] [] [] [] [] [] :
C(X, ())

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
• = { toFun := fun (x : X) => { toFun := fun (f : C(X, 𝕜)) => f x, map_add' := , map_smul' := , cont := }, , continuous_toFun := }
Instances For
@[simp]
theorem WeakDual.CharacterSpace.continuousMapEval_apply_apply (X : Type u_1) (𝕜 : Type u_2) [] [] [] [] [] [] (x : X) (f : C(X, 𝕜)) :
f = f x
theorem WeakDual.CharacterSpace.continuousMapEval_bijective (X : Type u_1) (𝕜 : Type u_2) [] [] [] [] :
noncomputable def WeakDual.CharacterSpace.homeoEval (X : Type u_1) (𝕜 : Type u_2) [] [] [] [] :
X ≃ₜ ()

This is the natural homeomorphism between a compact Hausdorff space X and the WeakDual.characterSpace 𝕜 C(X, 𝕜).

Equations
• = .homeoOfEquivCompactToT2
Instances For