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) [TopologicalSpace X] [Semiring R] [TopologicalSpace R] [TopologicalSemiring 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

• ContinuousMap.idealOfSet R s = { carrier := {f : C(X, R) | ∀ x ∈ sᶜ, f x = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem ContinuousMap.idealOfSet_closed {X : Type u_1} (R : Type u_2) [TopologicalSpace X] [Semiring R] [TopologicalSpace R] [TopologicalSemiring R] [T2Space R] (s : Set X) : IsClosed ↑(ContinuousMap.idealOfSet R s)

theorem ContinuousMap.mem_idealOfSet {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [Semiring R] [TopologicalSpace R] [TopologicalSemiring R] {s : Set X} {f : C(X, R)} : f ∈ ContinuousMap.idealOfSet R s ↔ ∀ ⦃x : X⦄, x ∈ sᶜ → f x = 0

theorem ContinuousMap.not_mem_idealOfSet {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [Semiring R] [TopologicalSpace R] [TopologicalSemiring R] {s : Set X} {f : C(X, R)} : f ∉ ContinuousMap.idealOfSet R s ↔ ∃ x ∈ sᶜ, f x ≠ 0

def ContinuousMap.setOfIdeal {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [Semiring R] [TopologicalSpace R] [TopologicalSemiring 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

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

theorem ContinuousMap.not_mem_setOfIdeal {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [Semiring R] [TopologicalSpace R] [TopologicalSemiring R] {I : Ideal C(X, R)} {x : X} : x ∉ ContinuousMap.setOfIdeal I ↔ ∀ ⦃f : C(X, R)⦄, f ∈ I → f x = 0

theorem ContinuousMap.mem_setOfIdeal {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [Semiring R] [TopologicalSpace R] [TopologicalSemiring R] {I : Ideal C(X, R)} {x : X} : x ∈ ContinuousMap.setOfIdeal I ↔ ∃ f ∈ I, f x ≠ 0

theorem ContinuousMap.setOfIdeal_open {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [Semiring R] [TopologicalSpace R] [TopologicalSemiring R] [T2Space R] (I : Ideal C(X, R)) : IsOpen (ContinuousMap.setOfIdeal I)

def ContinuousMap.opensOfIdeal {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [Semiring R] [TopologicalSpace R] [TopologicalSemiring R] [T2Space R] (I : Ideal C(X, R)) : TopologicalSpace.Opens X

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

Equations

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

@[simp]

theorem ContinuousMap.opensOfIdeal_coe {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [Semiring R] [TopologicalSpace R] [TopologicalSemiring R] [T2Space R] (I : Ideal C(X, R)) : ↑(ContinuousMap.opensOfIdeal I) = ContinuousMap.setOfIdeal I

@[simp]

theorem ContinuousMap.setOfTop_eq_univ {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [Semiring R] [TopologicalSpace R] [TopologicalSemiring R] [Nontrivial R] : ContinuousMap.setOfIdeal ⊤ = Set.univ

@[simp]

theorem ContinuousMap.idealOfEmpty_eq_bot {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [Semiring R] [TopologicalSpace R] [TopologicalSemiring R] : ContinuousMap.idealOfSet R ∅ = ⊥

@[simp]

theorem ContinuousMap.mem_idealOfSet_compl_singleton {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [Semiring R] [TopologicalSpace R] [TopologicalSemiring R] (x : X) (f : C(X, R)) : f ∈ ContinuousMap.idealOfSet R {x}ᶜ ↔ f x = 0

theorem ContinuousMap.ideal_gc (X : Type u_1) (R : Type u_2) [TopologicalSpace X] [Semiring R] [TopologicalSpace R] [TopologicalSemiring R] : GaloisConnection ContinuousMap.setOfIdeal (ContinuousMap.idealOfSet R)

theorem ContinuousMap.exists_mul_le_one_eqOn_ge {X : Type u_1} [TopologicalSpace X] (f : C(X, NNReal)) {c : NNReal} (hc : 0 < c) : ∃ (g : C(X, NNReal)), (∀ (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} [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X] (I : Ideal C(X, 𝕜)) : ContinuousMap.idealOfSet 𝕜 (ContinuousMap.setOfIdeal I) = I.closure

theorem ContinuousMap.idealOfSet_ofIdeal_isClosed {X : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X] {I : Ideal C(X, 𝕜)} (hI : IsClosed ↑I) : ContinuousMap.idealOfSet 𝕜 (ContinuousMap.setOfIdeal I) = I

@[simp]

theorem ContinuousMap.setOfIdeal_ofSet_eq_interior {X : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X] (s : Set X) : ContinuousMap.setOfIdeal (ContinuousMap.idealOfSet 𝕜 s) = interior s

theorem ContinuousMap.setOfIdeal_ofSet_of_isOpen {X : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X] {s : Set X} (hs : IsOpen s) : ContinuousMap.setOfIdeal (ContinuousMap.idealOfSet 𝕜 s) = s

def ContinuousMap.idealOpensGI (X : Type u_1) (𝕜 : Type u_2) [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X] : GaloisInsertion ContinuousMap.opensOfIdeal fun (s : TopologicalSpace.Opens X) => ContinuousMap.idealOfSet 𝕜 ↑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.

@[simp]

theorem ContinuousMap.idealOpensGI_choice (X : Type u_1) (𝕜 : Type u_2) [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X] (I : Ideal C(X, 𝕜)) (x✝ : ContinuousMap.idealOfSet 𝕜 ↑(ContinuousMap.opensOfIdeal I) ≤ I) : (ContinuousMap.idealOpensGI X 𝕜).choice I x✝ = ContinuousMap.opensOfIdeal I.closure

theorem ContinuousMap.idealOfSet_isMaximal_iff {X : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X] (s : TopologicalSpace.Opens X) : (ContinuousMap.idealOfSet 𝕜 ↑s).IsMaximal ↔ IsCoatom s

theorem ContinuousMap.idealOf_compl_singleton_isMaximal {X : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X] (x : X) : (ContinuousMap.idealOfSet 𝕜 {x}ᶜ).IsMaximal

theorem ContinuousMap.setOfIdeal_eq_compl_singleton {X : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X] (I : Ideal C(X, 𝕜)) [hI : I.IsMaximal] : ∃ (x : X), ContinuousMap.setOfIdeal I = {x}ᶜ

theorem ContinuousMap.ideal_isMaximal_iff {X : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X] (I : Ideal C(X, 𝕜)) [hI : IsClosed ↑I] : I.IsMaximal ↔ ∃ (x : X), ContinuousMap.idealOfSet 𝕜 {x}ᶜ = I

def WeakDual.CharacterSpace.continuousMapEval (X : Type u_1) (𝕜 : Type u_2) [TopologicalSpace X] [CommRing 𝕜] [TopologicalSpace 𝕜] [TopologicalRing 𝕜] [Nontrivial 𝕜] [NoZeroDivisors 𝕜] : C(X, ↑(WeakDual.characterSpace 𝕜 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

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

@[simp]

theorem WeakDual.CharacterSpace.continuousMapEval_apply_apply (X : Type u_1) (𝕜 : Type u_2) [TopologicalSpace X] [CommRing 𝕜] [TopologicalSpace 𝕜] [TopologicalRing 𝕜] [Nontrivial 𝕜] [NoZeroDivisors 𝕜] (x : X) (f : C(X, 𝕜)) : ((WeakDual.CharacterSpace.continuousMapEval X 𝕜) x) f = f x

theorem WeakDual.CharacterSpace.continuousMapEval_bijective (X : Type u_1) (𝕜 : Type u_2) [TopologicalSpace X] [CompactSpace X] [T2Space X] [RCLike 𝕜] : Function.Bijective ⇑(WeakDual.CharacterSpace.continuousMapEval X 𝕜)

noncomputable def WeakDual.CharacterSpace.homeoEval (X : Type u_1) (𝕜 : Type u_2) [TopologicalSpace X] [CompactSpace X] [T2Space X] [RCLike 𝕜] : X ≃ₜ ↑(WeakDual.characterSpace 𝕜 C(X, 𝕜))

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

Equations

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