# mathlib3documentation

topology.continuous_function.ideals

# Ideals of continuous functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 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.

When R = 𝕜 with is_R_or_C 𝕜 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 continuous_map.ideal_opens_gi. 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 character_space 𝕜 C(X, 𝕜) given by point evaluation, which is herein called weak_dual.character_space.continuous_map_eval. Again, when X is compact Hausdorff and is_R_or_C 𝕜, 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 weak_dual.character_space.homeo_eval.

## Main definitions #

• continuous_map.ideal_of_set: ideal of functions which vanish on the complement of a set.
• continuous_map.set_of_ideal: complement of the set on which all functions in the ideal vanish.
• continuous_map.opens_of_ideal: continuous_map.set_of_ideal as a term of opens X.
• continuous_map.ideal_opens_gi: The Galois insertion continuous_map.opens_of_ideal and λ s, continuous_map.ideal_of_set ↑s.
• weak_dual.character_space.continuous_map_eval: the natural continuous map from a locally compact topological space X to the character_space 𝕜 C(X, 𝕜) which sends x : X to point evaluation at x, with modest hypothesis on 𝕜.
• weak_dual.character_space.homeo_eval: this is weak_dual.character_space.continuous_map_eval upgraded to a homeomorphism when X is compact Hausdorff and is_R_or_C 𝕜.

## Main statements #

• continuous_map.ideal_of_set_of_ideal_eq_closure: when X is compact Hausdorff and is_R_or_C 𝕜, ideal_of_set 𝕜 (set_of_ideal I) = I.closure for any ideal I : ideal C(X, 𝕜).
• continuous_map.set_of_ideal_of_set_eq_interior: when X is compact Hausdorff and is_R_or_C 𝕜, set_of_ideal (ideal_of_set 𝕜 s) = interior s for any s : set X.
• continuous_map.ideal_is_maximal_iff: when X is compact Hausdorff and is_R_or_C 𝕜, a closed ideal of C(X, 𝕜) is maximal if and only if it is ideal_of_set 𝕜 {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 continuous_map.ideal_opens_gi.

## Tags #

ideal, continuous function, compact, Hausdorff

def continuous_map.ideal_of_set {X : Type u_1} (R : Type u_2) [semiring R] (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
theorem continuous_map.ideal_of_set_closed {X : Type u_1} (R : Type u_2) [semiring R] [t2_space R] (s : set X) :
theorem continuous_map.mem_ideal_of_set {X : Type u_1} {R : Type u_2} [semiring R] {s : set X} {f : C(X, R)} :
⦃x : X⦄, x s f x = 0
theorem continuous_map.not_mem_ideal_of_set {X : Type u_1} {R : Type u_2} [semiring R] {s : set X} {f : C(X, R)} :
(x : X) (H : x s), f x 0
def continuous_map.set_of_ideal {X : Type u_1} {R : Type u_2} [semiring R] (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
theorem continuous_map.not_mem_set_of_ideal {X : Type u_1} {R : Type u_2} [semiring R] {I : ideal C(X, R)} {x : X} :
⦃f : C(X, R)⦄, f I f x = 0
theorem continuous_map.mem_set_of_ideal {X : Type u_1} {R : Type u_2} [semiring R] {I : ideal C(X, R)} {x : X} :
(f : C(X, R)) (H : f I), f x 0
theorem continuous_map.set_of_ideal_open {X : Type u_1} {R : Type u_2} [semiring R] [t2_space R] (I : ideal C(X, R)) :
@[simp]
theorem continuous_map.opens_of_ideal_coe {X : Type u_1} {R : Type u_2} [semiring R] [t2_space R] (I : ideal C(X, R)) :
def continuous_map.opens_of_ideal {X : Type u_1} {R : Type u_2} [semiring R] [t2_space R] (I : ideal C(X, R)) :

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

Equations
@[simp]
theorem continuous_map.set_of_top_eq_univ {X : Type u_1} {R : Type u_2} [semiring R] [nontrivial R] :
@[simp]
theorem continuous_map.ideal_of_empty_eq_bot {X : Type u_1} {R : Type u_2} [semiring R]  :
@[simp]
theorem continuous_map.mem_ideal_of_set_compl_singleton {X : Type u_1} {R : Type u_2} [semiring R] (x : X) (f : C(X, R)) :
f x = 0
theorem continuous_map.ideal_gc (X : Type u_1) (R : Type u_2) [semiring R]  :
theorem continuous_map.exists_mul_le_one_eq_on_ge {X : Type u_1} (f : C(X, nnreal)) {c : nnreal} (hc : 0 < c) :
(g : , ( (x : X), (g * f) x 1) set.eq_on (g * f) 1 {x : X | c f x}

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

@[simp]
theorem continuous_map.ideal_of_set_of_ideal_eq_closure {X : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [t2_space X] (I : ideal C(X, 𝕜)) :
theorem continuous_map.ideal_of_set_of_ideal_is_closed {X : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [t2_space X] {I : ideal C(X, 𝕜)} (hI : is_closed I) :
@[simp]
theorem continuous_map.set_of_ideal_of_set_eq_interior {X : Type u_1} (𝕜 : Type u_2) [is_R_or_C 𝕜] [t2_space X] (s : set X) :
theorem continuous_map.set_of_ideal_of_set_of_is_open {X : Type u_1} (𝕜 : Type u_2) [is_R_or_C 𝕜] [t2_space X] {s : set X} (hs : is_open s) :
@[simp]
theorem continuous_map.ideal_opens_gi_choice (X : Type u_1) (𝕜 : Type u_2) [is_R_or_C 𝕜] [t2_space X] (I : ideal C(X, 𝕜))  :
def continuous_map.ideal_opens_gi (X : Type u_1) (𝕜 : Type u_2) [is_R_or_C 𝕜] [t2_space X] :

The Galois insertion continuous_map.opens_of_ideal : ideal C(X, 𝕜) → opens X and λ s, continuous_map.ideal_of_set ↑s.

Equations
theorem continuous_map.ideal_of_compl_singleton_is_maximal {X : Type u_1} (𝕜 : Type u_2) [is_R_or_C 𝕜] [t2_space X] (x : X) :
theorem continuous_map.set_of_ideal_eq_compl_singleton {X : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [t2_space X] (I : ideal C(X, 𝕜)) [hI : I.is_maximal] :
(x : X),
theorem continuous_map.ideal_is_maximal_iff {X : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [t2_space X] (I : ideal C(X, 𝕜)) [hI : is_closed I] :
I.is_maximal (x : X),
def weak_dual.character_space.continuous_map_eval (X : Type u_1) (𝕜 : Type u_2) [comm_ring 𝕜] [nontrivial 𝕜]  :

The natural continuous map from a locally compact topological space X to the character_space 𝕜 C(X, 𝕜) which sends x : X to point evaluation at x.

Equations
@[simp]
theorem weak_dual.character_space.continuous_map_eval_apply_apply (X : Type u_1) (𝕜 : Type u_2) [comm_ring 𝕜] [nontrivial 𝕜] (x : X) (f : C(X, 𝕜)) :
= f x
noncomputable def weak_dual.character_space.homeo_eval (X : Type u_1) (𝕜 : Type u_2) [t2_space X] [is_R_or_C 𝕜] :

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

Equations