Zulip Chat Archive

Stream: general

Topic: ideals of continuous maps


Jireh Loreaux (Sep 22 2022 at 18:53):

I have implemented (locally, there is no branch or PR yet) the Galois connection between sets of topological space X and ideals of C(X, R) where R is a topological ring; here the maps are, for s : set X take the ideal of all functions which are zero on this set, and for I : ideal C(X, R) take the intersections of the zero sets of all functions in the ideal are zero.

In case R is is_R_or_C R, and X is compact Hausdorff, then this can actually be upgraded to a Galois correspondence between closed sets and closed ideals, which I have also implemented in an unbundled fashion. The questions is: should I also implement a bundled version of this Galois correspondence between the types closeds X and { I : ideal C(X, R) // is_closed (I : set C(X, R)) }?

Jireh Loreaux (Sep 22 2022 at 19:28):

@Heather Macbeth, @Frédéric Dupuis , @Oliver Nash

Frédéric Dupuis (Sep 22 2022 at 19:51):

My take is that if you don't have a use case in mind for the bundled version, then don't worry about it for now. We can always add it later.

Jireh Loreaux (Sep 22 2022 at 19:59):

Well, here is one possibility, but I haven't actually tried it yet: if we have an actual order_iso here (between (closeds X)ᵒᵈ and the subtype of closed ideals), shouldn't we be able to prove more easily that the ideal correspondning to {x} is maximal, and vice versa that every maximal ideal arises in this way?

Jireh Loreaux (Sep 22 2022 at 20:22):

Another issue: should I implement all this in terms of open sets instead? closed sets has always felt to me more natural, but I could possibly be convinced to go the other way.

Kevin Buzzard (Sep 22 2022 at 21:37):

Given that we don't have contravariant functors I would implement it in the covariant way

Jireh Loreaux (Sep 22 2022 at 22:15):

Just the order isomorphism, or everything?

Kevin Buzzard (Sep 23 2022 at 10:28):

Heh, I don't know really, I just think having ops makes stuff less readable, but it's probably not a strong argument for making the decision.

Jireh Loreaux (Sep 23 2022 at 14:34):

To see how it would play out, I just did it last night. I think I agree with you that it's better via open sets.


Last updated: Dec 20 2023 at 11:08 UTC