closeds and set_like

Stream: general

[Jireh Loreaux]

Currently, docs#closeds (and similarly for docs#opens and others) is a structure built of a set and a proof that it is closed (I think opens may actually be a subtype rather than a structure, but whatever). Then a set_like instance is provided. One downside is that we can only use this to talk about the closed subsets of a topological space.

However, if instead closeds took a set_like instance as a parameter, then we could talk about closed subobjects generally, e.g., we could write closeds (ideal R) to talk about the closed left ideals in a ring which is also a topological space. The current (major) downside to this is that set has no set_like instance, so paradoxically we would lose the ability to talk about the closed subsets of a topological space.

So, what is the word on making set into a set_like instance? Is this a terrible idea? I thought maybe it had been discussed before.

[Yaël Dillies]

Does your idea provide anything beyong basic boilerplate? To me it doesn't seem like you can prove lattice (closeds α) (for your closeds) because you don't know that ↑(a ⊔ b) = ↑a ∪ ↑b and similar (and indeed it might not be the case). So you will end up writing lattice (closeds (set α)), lattice (closeds (ideal α)), etc... separately

[Jireh Loreaux]

I mean, it provides a unified framework, but sure, the lattice operations might be different in different contexts. For closeds you could get a universal inf_semilattice, and then specialize the sup for different types, and for opens the reverse would be true.

[Jireh Loreaux]

Right now I mainly just want to express an order isomorphism opens X ≃o closeds (ideal C(X, 𝕜)), and use it to prove some basic things. But I can't write down the right-hand side as-is, so I expressed it as a subtype, but then I'm missing basic API. And this will only get to be a bigger deal for me as time goes on (closed ideals play a fundamental role in C⋆-algebra theory).

[Yaël Dillies]

Then define closed_ideal! :grinning:

[Jireh Loreaux]

Right, of course I could, but that seems silly when there should be a universal solution to this problem!

[Jireh Loreaux]

especially one that (almost) already exists.

[Yaël Dillies]

My point is that "writing the API for closeds and the API for closed_ideal" is less time than "writing the API for closeds and the API for closeds (set α) and the API for closeds (ideal R)" and less design decisions too.

[Yaël Dillies]

emphasis on the design decisions

[Kyle Miller]

@Jireh Loreaux What did you have in mind for the interface for closed subsets of a topological space with this idea? Would it be closeds (set X)? I'm not sure how you could get closeds X to work.

[Jireh Loreaux]

Yes, it would be closeds (set X), sorry, I mixed usage in my example above.

[Jireh Loreaux]

Certainly design decisions can be time-consuming, but I would prefer to do it right rather than create pockets of things which are half-duplicates across the library. Closed ideals are not the only situation where we care about closed subobjects.

[Adam Topaz]

IMO we should just define closed_ideal because the open analogue is not really useful

[Kyle Miller]

I'm not saying this is a good idea, but there's always this sort of thing to have a global definition closeds:

import topology.sets.closeds

class has_closeds (α : Type*) :=
(closeds : Type*)

export has_closeds (closeds)

instance {α : Type*} [topological_space α] : has_closeds (set α) :=
⟨topological_space.closeds α⟩

[Kyle Miller]

Or another sort of design to bundle a type's is-closed property:

import topology.sets.closeds

class has_is_closed (α : Type*) :=
(is_closed' : α → Prop) -- name conflict with current `is_closed`, hence the '

export has_is_closed (is_closed')

structure closeds (α : Type*) [has_is_closed α] :=
(carrier : α)
(closed' : is_closed' carrier)

instance {α : Type*} [topological_space α] : has_is_closed (set α) :=
⟨is_closed⟩

[Kyle Miller]

@Jireh Loreaux I haven't been able to figure out where you'd need the set_like instance. Could you give some Lean to clarify?

[Yaël Dillies]

It's to state that an ideal is closed. closed eats up a set, not an ideal.

[Jireh Loreaux]

Right now, closeds (ideal R) would mean the type of closed (collections of ideals), assuming that ideal R had a topological_space instance.

[Jireh Loreaux]

@Adam Topaz , this isn't really about open ideals vs closed ideals; it's about closed subobjects in general.

[Jireh Loreaux]

Another option is to just create a new type set_like.closeds which does what I mentioned, and to keep this separate from topological_space.closeds. I'm leaning towards this if there isn't support (or if it isn't a good idea) for making a set_like instance for set.

[Yaël Dillies]

But then you will exactly one use: ideal

[Yaël Dillies]

I'm much more for having at least three examples before abstracting boilerplate away, because you might figure out later that there's little to gain.

[Kyle Miller]

Yaël Dillies said:

But then you will exactly one use: ideal

That seems like a strong statement. What about closed subgroups?

[Yaël Dillies]

I mean now

[Jireh Loreaux]

Yaël, if it were significantly more work to do set_like.closeds vs closed_ideal, then I might agree with you, but this is a trivial abstraction. Moreover, I can already think of other scenarios: as Kyle mentioned, there's closed subgroups, but for my purposes, closed subalgebras and closed star_subalgebras will be important as well. Of course, sometimes we don't want these bundled, but other times we do. For example, there is a natural correspondence between closed left ideals in a C⋆-algebra and hereditary C⋆-algebras.

[Kyle Miller]

Yaël Dillies said:

It's to state that an ideal is closed. closed eats up a set, not an ideal.

I get that -- my thought was that the definitions themselves don't need a set_like instance since you need to supply the is_closed' field. There could then be a property typeclass (I guess what we're calling mixins) that says is_closed' respects the inf structure to support general lemmas.

[Kyle Miller]

It would be nice if there were some general way to deal with the subtype-of-subtype problem. There's something about it that reminds me of monad transformer stacks... We'd like to be able to lift structures that are present in interior subtypes out to the whole stack of subtypes when possible.

[Kyle Miller]

@Jireh Loreaux Regarding set_like for set, I suggest just trying it and seeing if mathlib breaks. I suspect there are some instances that set_like provides that might conflict, however. One solution to this might be to split set_like into two parts, one which is just the injective map to set and the other which, when you create an instance of it, will add all the bells and whistles.

[Eric Rodriguez]

I thought it was tried very recently, and it broke stuff really badly

[Adam Topaz]

I think a more general thing to do is to write some predicate that says a thing is closed with respect to a docs#closure_operator

[Adam Topaz]

I think the map sending an ideal to its closure is such an operator

[Kyle Miller]

That sounds nice and pointless pointfree.

[Jireh Loreaux]

We already have docs#closure_operator.closed, so I guess you mean using this with respect to Kyle's second suggestion above?

[Jireh Loreaux]

So, as far as I can tell, Adam's suggestion would amount to making docs#closure_operator into a class, or maybe a new class with a single field which is a closure_operator in order to provide an API specific to the class separate from the structure closure_operator. While this does seem very appealing, I do wonder about the applicability.

For example, if we had an instance of this class for topological spaces (where the provided closure operator is the usual one) and then have other instances on other types where the closure operator has nothing to do with topological closure, we could easily end up with real diamonds that way.

To me that suggests that we should restrict to topological closure, but then that just leads me back to set_like.closeds. Please let me know if I'm overlooking something or have missed the point.