Alexandrov topologies

Stream: Is there code for X?

[Adam Topaz]

We have docs#AlexandrovDiscrete but I can't seem to find the following:

1. given any partial order on a type X, the upper sets form a (alexandrov) topology on X.
2. the specialization partial order associated to the topology of (1) is the original partial order.
3. Any alexandrov topological space arises in this way.

Do we have such things in mathlib?

[Adam Topaz]

We do have isOpen_iff_forall_specializes which essentially says that the specialization order determines the topology and vice-versa, but I still don't know how to talk about a poset as a topological space.

[Junyan Xu]

The "upper" topology in mathlib seems to be coarser than what you describe according to Topology.IsUpper.isUpperSet_of_isOpen

[Adam Topaz]

Ok, I guess I'm looking for docs#Topology.IsUpperSet

[Adam Topaz]

and yes I agree that "IsUpper" doesn't coincide with this.

[Adam Topaz]

and the synonym WithUpperSet is my (1).

[Yaël Dillies]

Are you looking for docs#alexDiscEquivPreord ?

[Yaël Dillies]

Adam Topaz said:

I still don't know how to talk about a poset as a topological space.

This is docs#WithUpperSet

[Yaël Dillies]

Sorry, I'm blind. You already found it

[Adam Topaz]

Yes, thanks!

[Yaël Dillies]

The thing we're missing is that T1 Alexandrov discrete <=> partial order. I didn't do it, but it should be easy from what we have

[Adam Topaz]

@Yaël Dillies do you know off the top of your head where I can find the lemma that says that, given Topology.IsUpperSet X, that the preorder on X agrees with the specialization order coming from the topology?

[Yaël Dillies]

We don't have it, pretty sure

[Adam Topaz]

ok, thanks.

[Yaël Dillies]

Maybe @Christopher Hoskin has it on a branch, but in any case it should be easy to prove

[Adam Topaz]

I mean, we do have Topology.WithUpperSet.toUpperSet_specializes_toUpperSet

[Adam Topaz]

Indeed it is easy:

example (x y : X) : x ⤳ y ↔ y ≤ x := by
  simp only [specializes_iff_closure_subset,
    Topology.IsUpperSet.closure_singleton, Set.Iic_subset_Iic]

[Adam Topaz]

It turns out that I didn’t need the lemma for my application, but I added it anyway: #21263