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 #

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

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.

Instances For
    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 sf 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)} :
    fContinuousMap.idealOfSet R s xs, 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.

    Instances For
      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} :
      xContinuousMap.setOfIdeal I ∀ ⦃f : C(X, R)⦄, f If 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 fI, f x 0

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

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

        theorem ContinuousMap.idealOpensGI_choice (X : Type u_1) (𝕜 : Type u_2) [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X] (I : Ideal C(X, 𝕜)) :
        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.

        • One or more equations did not get rendered due to their size.
        Instances For
          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

          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.

          Instances For
            noncomputable def WeakDual.CharacterSpace.homeoEval (X : Type u_1) (𝕜 : Type u_2) [TopologicalSpace X] [CompactSpace X] [T2Space X] [RCLike 𝕜] :

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

            Instances For