mathlib3 documentation

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 #

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

source
def continuous_map.ideal_of_set {X : Type u_1} (R : Type u_2) [topological_space X] [semiring R] [topological_space R] [topological_semiring R] (s : set X) :
ideal C(X, R)

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
source
theorem continuous_map.ideal_of_set_closed {X : Type u_1} (R : Type u_2) [topological_space X] [semiring R] [topological_space R] [topological_semiring R] [locally_compact_space X] [t2_space R] (s : set X) :
is_closed ↑(continuous_map.ideal_of_set R s)
source
theorem continuous_map.mem_ideal_of_set {X : Type u_1} {R : Type u_2} [topological_space X] [semiring R] [topological_space R] [topological_semiring R] {s : set X} {f : C(X, R)} :
f ∈ continuous_map.ideal_of_set R s ↔ ∀ ⦃x : X⦄, x ∈ sᶜ → ⇑f x = 0
source
theorem continuous_map.not_mem_ideal_of_set {X : Type u_1} {R : Type u_2} [topological_space X] [semiring R] [topological_space R] [topological_semiring R] {s : set X} {f : C(X, R)} :
f ∉ continuous_map.ideal_of_set R s ↔ ∃ (x : X) (H : x ∈ sᶜ), ⇑f x ≠ 0
source
def continuous_map.set_of_ideal {X : Type u_1} {R : Type u_2} [topological_space X] [semiring R] [topological_space R] [topological_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
source
theorem continuous_map.not_mem_set_of_ideal {X : Type u_1} {R : Type u_2} [topological_space X] [semiring R] [topological_space R] [topological_semiring R] {I : ideal C(X, R)} {x : X} :
x ∉ continuous_map.set_of_ideal I ↔ ∀ ⦃f : C(X, R)⦄, f ∈ I → ⇑f x = 0
source
theorem continuous_map.mem_set_of_ideal {X : Type u_1} {R : Type u_2} [topological_space X] [semiring R] [topological_space R] [topological_semiring 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
source
theorem continuous_map.set_of_ideal_open {X : Type u_1} {R : Type u_2} [topological_space X] [semiring R] [topological_space R] [topological_semiring R] [t2_space R] (I : ideal C(X, R)) :
is_open (continuous_map.set_of_ideal I)
source
@[simp]
theorem continuous_map.opens_of_ideal_coe {X : Type u_1} {R : Type u_2} [topological_space X] [semiring R] [topological_space R] [topological_semiring R] [t2_space R] (I : ideal C(X, R)) :
↑(continuous_map.opens_of_ideal I) = continuous_map.set_of_ideal I
source
def continuous_map.opens_of_ideal {X : Type u_1} {R : Type u_2} [topological_space X] [semiring R] [topological_space R] [topological_semiring R] [t2_space R] (I : ideal C(X, R)) :
topological_space.opens X

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

Equations
source
@[simp]
theorem continuous_map.set_of_top_eq_univ {X : Type u_1} {R : Type u_2} [topological_space X] [semiring R] [topological_space R] [topological_semiring R] [nontrivial R] :
continuous_map.set_of_ideal ⊤ = set.univ
source
@[simp]
theorem continuous_map.ideal_of_empty_eq_bot {X : Type u_1} {R : Type u_2} [topological_space X] [semiring R] [topological_space R] [topological_semiring R] :
continuous_map.ideal_of_set R ∅ = ⊥
source
@[simp]
theorem continuous_map.mem_ideal_of_set_compl_singleton {X : Type u_1} {R : Type u_2} [topological_space X] [semiring R] [topological_space R] [topological_semiring R] (x : X) (f : C(X, R)) :
f ∈ continuous_map.ideal_of_set R {x}ᶜ ↔ ⇑f x = 0
source
theorem continuous_map.ideal_gc (X : Type u_1) (R : Type u_2) [topological_space X] [semiring R] [topological_space R] [topological_semiring R] :
galois_connection continuous_map.set_of_ideal (continuous_map.ideal_of_set R)
source
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.

source
@[simp]
theorem continuous_map.ideal_of_set_of_ideal_eq_closure {X : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [topological_space X] [compact_space X] [t2_space X] (I : ideal C(X, 𝕜)) :
continuous_map.ideal_of_set 𝕜 (continuous_map.set_of_ideal I) = I.closure
source
theorem continuous_map.ideal_of_set_of_ideal_is_closed {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) :
continuous_map.ideal_of_set 𝕜 (continuous_map.set_of_ideal I) = I
source
@[simp]
theorem continuous_map.set_of_ideal_of_set_eq_interior {X : Type u_1} (𝕜 : Type u_2) [is_R_or_C 𝕜] [topological_space X] [compact_space X] [t2_space X] (s : set X) :
continuous_map.set_of_ideal (continuous_map.ideal_of_set 𝕜 s) = interior s
source
theorem continuous_map.set_of_ideal_of_set_of_is_open {X : Type u_1} (𝕜 : Type u_2) [is_R_or_C 𝕜] [topological_space X] [compact_space X] [t2_space X] {s : set X} (hs : is_open s) :
continuous_map.set_of_ideal (continuous_map.ideal_of_set 𝕜 s) = s
source
@[simp]
theorem continuous_map.ideal_opens_gi_choice (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 : continuous_map.ideal_of_set 𝕜 ↑(continuous_map.opens_of_ideal I) ≤ I) :
(continuous_map.ideal_opens_gi X 𝕜).choice I hI = continuous_map.opens_of_ideal I.closure
source
def continuous_map.ideal_opens_gi (X : Type u_1) (𝕜 : Type u_2) [is_R_or_C 𝕜] [topological_space X] [compact_space X] [t2_space X] :
galois_insertion continuous_map.opens_of_ideal (λ (s : topological_space.opens X), continuous_map.ideal_of_set 𝕜 ↑s)

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

Equations
source
theorem continuous_map.ideal_of_set_is_maximal_iff {X : Type u_1} (𝕜 : Type u_2) [is_R_or_C 𝕜] [topological_space X] [compact_space X] [t2_space X] (s : topological_space.opens X) :
(continuous_map.ideal_of_set 𝕜 ↑s).is_maximal ↔ is_coatom s
source
theorem continuous_map.ideal_of_compl_singleton_is_maximal {X : Type u_1} (𝕜 : Type u_2) [is_R_or_C 𝕜] [topological_space X] [compact_space X] [t2_space X] (x : X) :
(continuous_map.ideal_of_set 𝕜 {x}ᶜ).is_maximal
source
theorem continuous_map.set_of_ideal_eq_compl_singleton {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 : I.is_maximal] :
∃ (x : X), continuous_map.set_of_ideal I = {x}ᶜ
source
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] :
I.is_maximal ↔ ∃ (x : X), continuous_map.ideal_of_set 𝕜 {x}ᶜ = I
source
def weak_dual.character_space.continuous_map_eval (X : Type u_1) (𝕜 : Type u_2) [topological_space X] [locally_compact_space X] [comm_ring 𝕜] [topological_space 𝕜] [topological_ring 𝕜] [nontrivial 𝕜] [no_zero_divisors 𝕜] :
C(X, ↥(weak_dual.character_space 𝕜 C(X, 𝕜)))

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
source
@[simp]
theorem weak_dual.character_space.continuous_map_eval_apply_apply (X : Type u_1) (𝕜 : Type u_2) [topological_space X] [locally_compact_space X] [comm_ring 𝕜] [topological_space 𝕜] [topological_ring 𝕜] [nontrivial 𝕜] [no_zero_divisors 𝕜] (x : X) (f : C(X, 𝕜)) :
⇑(⇑(weak_dual.character_space.continuous_map_eval X 𝕜) x) f = ⇑f x
source
theorem weak_dual.character_space.continuous_map_eval_bijective (X : Type u_1) (𝕜 : Type u_2) [topological_space X] [compact_space X] [t2_space X] [is_R_or_C 𝕜] :
function.bijective ⇑(weak_dual.character_space.continuous_map_eval X 𝕜)
source
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 𝕜] :
X ≃ₜ ↥(weak_dual.character_space 𝕜 C(X, 𝕜))

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

Equations