ideals of continuous maps

Stream: general

[Jireh Loreaux]

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]

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

[Frédéric Dupuis]

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]

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]

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]

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

[Jireh Loreaux]

Just the order isomorphism, or everything?

[Kevin Buzzard]

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]

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.