mathlib documentation


Ideals of continuous functions #

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.

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 #

Main statements #

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

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.

theorem continuous_map.mem_ideal_of_set {X : Type u_1} {R : Type u_2} [topological_space X] [ring R] [topological_space R] [topological_ring R] {s : set X} {f : C(X, R)} :
f continuous_map.ideal_of_set R s ⦃x : X⦄, x s f x = 0
theorem continuous_map.not_mem_ideal_of_set {X : Type u_1} {R : Type u_2} [topological_space X] [ring R] [topological_space R] [topological_ring R] {s : set X} {f : C(X, R)} :
f continuous_map.ideal_of_set R s (x : X) (H : x s), f x 0

Given an ideal I of C(X, R), construct the set of points for which every function in the ideal vanishes on the complement.

theorem continuous_map.not_mem_set_of_ideal {X : Type u_1} {R : Type u_2} [topological_space X] [ring R] [topological_space R] [topological_ring R] {I : ideal C(X, R)} {x : X} :
x continuous_map.set_of_ideal I ⦃f : C(X, R)⦄, f I f x = 0
theorem continuous_map.mem_set_of_ideal {X : Type u_1} {R : Type u_2} [topological_space X] [ring R] [topological_space R] [topological_ring R] {I : ideal C(X, R)} {x : X} :
x continuous_map.set_of_ideal I (f : C(X, R)) (H : f I), f x 0

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

theorem continuous_map.exists_mul_le_one_eq_on_ge {X : Type u_1} [topological_space X] (f : C(X, nnreal)) {c : nnreal} (hc : 0 < c) :
(g : C(X, nnreal)), ( (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.

theorem continuous_map.ideal_is_maximal_iff {X : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [topological_space X] [compact_space X] [t2_space X] (I : ideal C(X, 𝕜)) [hI : is_closed I] :

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.

noncomputable def weak_dual.character_space.homeo_eval (X : Type u_1) (𝕜 : Type u_2) [topological_space X] [compact_space X] [t2_space X] [is_R_or_C 𝕜] :

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