Multiple topologies?

Stream: maths

[Christopher Hoskin]

I'm trying - and in some cases succeeding - to prove results about the relationships between various well known topologies on a lattice:

https://github.com/leanprover-community/mathlib4/blob/mans0954/lawson-topology/Mathlib/Topology/Order/LawsonTopology.lean#L168

However, it's all starting to look a bit weird and unlike other things I've seen in Mathlib e.g.:

variable [CompleteLattice α]
  (S :TopologicalSpace α) (l : TopologicalSpace α) (L : TopologicalSpace α)
  [@ScottTopology α S _]  [@LawsonTopology α L _] [@LowerTopology α l _]

-- Scott open iff UpperSet and STopology open

open Topology

lemma LawsonOpen_iff_ScottOpen (s : Set α) (h : IsUpperSet s) :
  IsOpen[L] s ↔ IsOpen[S] s := by
  constructor
  . intro hs
    rw [@ScottTopology.isOpen_iff_upper_and_Scott_Hausdorff_Open α _ S]
    constructor
    . exact h
    . exact fun d d₁ d₂ d₃ => (@LawsonOpen_implies_ScottHausdorffOpen' _ _ l S _ _ _ _ s)
        hs d d₁ d₂ d₃
  . apply TopologicalSpace.le_def.mp (Scott_le_Lawson _ _)

Before I go much further down this route, it would be useful to know if I'm going about this the right way or not?

Thanks!

CC @Yaël Dillies @Eric Wieser

[Yaël Dillies]

Sorry, am unavailable for the next week. But you know what I'm going to say: use type synonyms and translation functions.

[Eric Wieser]

I think there might be precedent for this kind of thing in our topology files

[Christopher Hoskin]

Okay, but I'm still wondering what to do about ordering topologies? Which of the following is "correct" or should I provide both?

lemma Scott_Hausdorff_le_Lower' [Preorder α] : @ScottHausdorffTopology α ≤ @LowerTopology' α :=
  fun _ s h => ScottHausdorffTopology.Lower_IsOpen s
    (@LowerTopology.isLowerSet_of_isOpen (WithLowerTopology α) _ _  _ s h)

lemma Scott_Hausdorff_le_Lower [Preorder α] [TopologicalSpace α] [LowerTopology α] :
ScottHausdorffTopology ≤  ‹TopologicalSpace α› :=
  fun _ h => ScottHausdorffTopology.Lower_IsOpen _ (LowerTopology.isLowerSet_of_isOpen h)

I don't see a way of formulating this statement using WithLowerTopology α since the topology is of type TopologicalSpace (WithLowerTopology α ) and therefore not directly comparable with an element of TopologicalSpace α?

Christopher

[Yaël Dillies]

I would state it as continuous (toScottHausdorff \comp toLower\-1)

[Yaël Dillies]

(deleted)

[Yaël Dillies]

If you can't figure it out, I can do it all in a week from now.

[Yury G. Kudryashov]

Another option is to consider two distinct types with an OrderIso between them.

[Christopher Hoskin]

Lean looks happy with this:

lemma ScottLawsonCont' [Preorder α] : Continuous (WithScottTopology.toScott ∘ WithLawsonTopology.ofLawson : WithLawsonTopology α → _) := sorry

Ultimately I want to get to a position where I can figure these things out by myself, so I don't have to keep bothering other people.

Thanks for the suggestions.

[Christopher Hoskin]

So the rule is, if the result is a property intrinsic to the topology (e.g. a separation property) use the mixin class, and if it's about the relationship between multiple topologies, use the type synonyms?

[Yury G. Kudryashov]

You can formulate your result without type synonyms using something like (not sure about names)

example {X Y : Type _} [Preorder X] [Preorder Y] [TopologicalSpace X] [TopologicalSpace Y]
    [IsLawsonTopology X] [IsScottTopology Y] (e : OrderIso X Y) : Continuous e :=

[Yury G. Kudryashov]

The rule is: if you want more than 1 topology on the same space, then most of the time it's better to use type synonyms.

[Yury G. Kudryashov]

What's good about the way of formulating the lemma with two separate spaces: if (I didn't check for these two topologies) the statement holds with weaker assumptions on e (e.g., an order embedding, or even a monotone map), then you can prove this more precise statement, then get the version with type synonyms for free.

[Christopher Hoskin]

Sorry for the long delay in replying - I've been trying to figure this out when I have a moment.

I've been wondering what to do when the statement of a result uses only one topology, but the proof depends on a stronger or weaker topology?

This is what I've come up with: https://github.com/leanprover-community/mathlib4/pull/2508/files#diff-983e16dd03108ad09234625f776ad94cfb58b1f6ee4762bf7519306fd90a2b46R293-R313

lemma closure_singleton (a : α) : closure {a} = Iic a := by
  rw [le_antisymm_iff]
  constructor
  . apply closure_minimal
    rw [singleton_subset_iff, mem_Iic]
    rw [isClosed_iff_lower_and_subset_implies_LUB_mem]
    constructor
    . exact isLowerSet_Iic a
    . intros d b _ _ d₃ d₄
      exact (isLUB_le_iff d₃).mpr d₄
  . rw [← OrderIso.apply_symm_apply WithUpperSetTopology.ofUpperSetOrderIso a,
      ← (OrderIso.image_Iic WithUpperSetTopology.ofUpperSetOrderIso),
      ← UpperSetTopology.closure_singleton,
      ← @image_singleton _ _ WithUpperSetTopology.ofUpperSetOrderIso ]
    apply (image_closure_subset_closure_image
      (Monotone_continuous WithUpperSetTopology.ofUpperSetOrderIso.monotone))

Is this the right sort of idea?

Thanks.

[Jireh Loreaux]

I haven't looked closely at your code, but if you have two topologies on the same type, we have some results for this kind of thing (e.g., docs#IsClosed.mono, although I couldn't find an analogous one for docs#closure, but you could prove it and add it, as it follows easily from IsClosed.mono; docs#closure_mono is different). That would allow you to show that if you had two topologies t₁ ≤ t₂ and Iic a ⊆ closure {a} in t₁, then the same is true in t₂.

[Yury G. Kudryashov]

Should we introduce a type tag WithOrderTopology such that WithOrderTopology X has order topology?

[Yury G. Kudryashov]

Then one can talk about continuity of the identity function to/from WithOrderTopology X if X has other topology.

[Yaël Dillies]

Yeah that's what we've been doing with the other order topologies.

[Christopher Hoskin]

@Jireh Loreaux Thanks - I was able to prove:

theorem Closure.mono (h : t₁ ≤ t₂) : @closure _ t₁ s ⊆ @closure _ t₂ s :=
  @closure_minimal _ t₁ s (@closure _ t₂ s) subset_closure (IsClosed.mono isClosed_closure h)

I then try to use this in the last step of the proof of closure_singleton:

convert Closure.mono (@upper_le_Scott α _)

Which leaves me with two goals:

case h.e'_1
α: Type u_1
β: Type ?u.10323
inst✝²: Preorder α
inst✝¹: TopologicalSpace α
inst✝: ScottTopology α
a: α
⊢ Iic a = closure {a}
case h.e'_2.h.e'_2
α: Type u_1
β: Type ?u.10323
inst✝²: Preorder α
inst✝¹: TopologicalSpace α
inst✝: ScottTopology α
a: α
⊢ inst✝¹ = ScottTopology'

The second goal can be closed with: exact topology_eq α. The first goal looks like it is exactly the statement of UpperSetTopology.closure_singleton. However, a rewrite results in the failed to synthesize instance UpperSetTopology α error.

So, it seems I still need a way to "put" the UpperSetTopology on α?

Thanks,

Christopher

[Jireh Loreaux]

Can you provide a full #mwe so I don't have to paste it together?

[Christopher Hoskin]

@Jireh Loreaux I've pushed where I've got to onto this branch: https://github.com/leanprover-community/mathlib4/tree/mans0954/scott-topology

If you want a genuine MWE that it might take me a little while to filter that out as there's quite a lot of gubbins associated with each topology.

[Jireh Loreaux]

the branch is fine

[Christopher Hoskin]

Thank you :) Specifically: https://github.com/leanprover-community/mathlib4/blob/mans0954/scott-topology/Mathlib/Topology/Order/ScottTopology.lean#L302

[Jireh Loreaux]

@Christopher Hoskin I looked at this for just a few minutes, but I'm fairly certain that your issue is that you haven't told Lean that the upperSetTopology' is an UpperSetTopology. This fails:

variable {γ} [Preorder γ]
#synth @UpperSetTopology γ (upperSetTopology' γ) _ -- fails

and this succeeds (in the spot you linked on your branch) except for the infer_instance line, which means it's correct except it can't find the instance.

  . convert Closure.mono (@upper_le_Scott α _)
    swap
    exact topology_eq α
    refine (@UpperSetTopology.closure_singleton α _ (upperSetTopology' α) ?_ a).symm
    infer_instance -- fails

[Jireh Loreaux]

Note: I just used tunnel vision to work on this problem, I did not look wider at your design choices in this branch.

[Christopher Hoskin]

I did not look wider at your design choices in this branch.

I don't know enough to make design choices. I rely on the advice of whoever was kind enough to answer my most recent query.

Naively I tried:

instance [Preorder α] : UpperSetTopology (upperSetTopology' α) := sorry

But that gives me a type mismatch:

application type mismatch
  @UpperSetTopology (upperSetTopology' α)
argument
  upperSetTopology' α
has type
  TopologicalSpace α : Type ?u.2929
but is expected to have type
  Type ?u.2938 : Type (?u.2938 + 1)

[Jireh Loreaux]

Right, that's because UpperSetTopology takes a term of type Type u, but you gave it upperSetTopology' α : TopologicalSpace α. You need

instance [Preorder α] : @UpperSetTopology α (upperSetTopology' α) _ := sorry

[Jireh Loreaux]

As for design, I would probably echo the suggestion above to make a type synonym (maybe with different naming to what I have below), and maybe even a structure so you can get nice functions back and forth easily.

structure WithUpperSet (α : Type _) :=
  toWithUpperSet :: ofWithUpperSet : α

instance {α : Type _} [Preorder α] : Preorder (WithUpperSet α) := sorry -- pull the instance back through `toWithUpperSet`

/-- `toWithUpperSet` as an order isomorphism. -/
def WithUpperSet.orderIso (α : Type _) [Preorder α] : α ≃o WithUpperSet α := sorry

instance {α : Type _} [Preorder α] : TopologicalSpace (WithUpperSet α) := upperSetTopology' (WithUpperSet α)

instance {α : Type _} [Preorder α] : UpperSetTopology (WithUpperSet α) := sorry

lemma continuous_toWithUpperSet (α : Type _) [Preorder α] [TopologicalSpace α] [UpperSetTopology α] : Continuous (WithUpperSet.OrderIso α) := sorry

[Christopher Hoskin]

I thought I already had a type synonym with WithUpperSetTopology?

So, for each topology we have:

i) the element of TopologicalSpace α itself;
ii) the mixin class;
iii) the type synonym;
iv) the structure;
v) a set of maps and results connecting them all?

It's all getting a bit baffling for the non-specialist.

Is any of this documented as best practice for topologies anywhere?

[Jireh Loreaux]

Sorry, I didn't see WithUpperSetTopology, that plays the role of my WithUpperSet

[Jireh Loreaux]

Regarding "best practice". I would say just use the following general rule of thumb: if you have a type α with and instance inst₁ : C and very rarely you want to equip α with a different inst₂ : C, then just go through the pain of switch the instances out manually on the same type α. However, if with any regularity you want to equip α with inst₂ instead of inst₁, then create a type synonym (or a one-field structure). This is generic to any type class, and not specific to topologies.

As for mixins, that depends on the specific situation, but as mentioned, we seem to have Prop-valued mixins for how a topology interacts with the order structure. Recently, @Antoine Chambert-Loir and @Anatole Dedecker were running into a few issues related to order topologies and the extreme value theorem. So perhaps they have some insight to share here.

[Christopher Hoskin]

Thanks. I got stuck trying to remove the sorry in:

instance [Preorder α] : @UpperSetTopology α (upperSetTopology' α) _ := sorry

But perhaps that will be clearer in the morning.

[Christopher Hoskin]

I've opened https://github.com/leanprover-community/mathlib/pull/19224

[Jireh Loreaux]

You should just PR that to mathlib 4 directly.

[Christopher Hoskin]

@Jireh Loreaux The last time I made a change to a file that was in both mathlib and mathlib4, it was mandatory to make the change in mathlib first and then forward port to mathlib4 to keep things in sync. Has that now changed?

[Ruben Van de Velde]

It has, yeah

[Jireh Loreaux]

And also you are only adding new material, not refactoring existing material. We've been accepting PRs like that to mathlib4 for a while now.

[Christopher Hoskin]

Thanks. Mathlib4 PR here: https://github.com/leanprover-community/mathlib4/pull/5631

[Christopher Hoskin]

@Jireh Loreaux I think:

instance [Preorder α] : @UpperSetTopology α (upperSetTopology' α) _ := sorry

isn't quite right, because:

instance [Preorder α] : @UpperSetTopology α (upperSetTopology' α) _ := ⟨rfl⟩

gives me:

failed to synthesize instance
  TopologicalSpace α

What is true is:

instance [Preorder α] : @UpperSetTopology (WithUpperSetTopology α) (upperSetTopology' α) _ := ⟨rfl⟩

With this,

  . convert Closure.mono (@upper_le_Scott α _)
    rw [(@UpperSetTopology.closure_singleton (WithUpperSetTopology α) _ (upperSetTopology' α) ?_ a)]
    infer_instance
    exact topology_eq α

completes the second part of the proof.

https://github.com/leanprover-community/mathlib4/pull/2508/files#diff-983e16dd03108ad09234625f776ad94cfb58b1f6ee4762bf7519306fd90a2b46R311

Still a bit clunky, but perhaps that's unavoidable?

[Jireh Loreaux]

This fixes your first problem, and so should avoid the convert (which is a hack in this case). In Lean 4 I've seen that when you manually specify an instance in a declaration you need to re-specify it in the body. The letI makes it inline the instance in the body. Actually, come to think of it, is this (re-specifying required) a bug, or an intended feature (maybe @Mario Carneiro knows)?

instance [Preorder α] : @UpperSetTopology α (upperSetTopology' α) _ := by
  letI := upperSetTopology' α
  exact ⟨rfl⟩

[Anatole Dedecker]

I haven't followed this discussion carefully, but I've written a summary of my approach on the matter (hoping that would help @Christopher Hoskin with #5672 and #2508). Of course this is only my opinion on the subject so feel free to let me know if you disagree with something. Maybe once we have a version that everyone agrees on it would deserve to become a library note?
Btw, all of the following applies also to docs#UniformSpace, and I will use that as an example sometimes.

[Anatole Dedecker]

There are three main ways to work with topologies on a type α that can't be declared as an instance (typically because they will disagree with the "canonical" options which are declared as instances).

1. Working with a bare term of type docs#TopologicalSpace

def myTopology (α) : TopologicalSpace α := ...

2. Defining a type alias and declaring the desired topology on it as an instance

def MyAlias (α) : Type _ := α

instance : TopologicalSpace (MyAlias α) := ...

3. Defining a typeclass predicate expressing that "the canonical topology on this type is equal to some topology"

class MyTopologyClass (α) [t : TopologicalSpace α] : Prop where
  topology_eq : t = ...

[Anatole Dedecker]

The important thing to understand is that these are mutually compatible, but also some of them may be useless depending on the situation (examples below).

Generally speaking, here are the use case for the three options.

1. Working with a concrete term of type TopologicalSpace _ should almost never be the preferred way of using a theory, because it can get quite annoying and lengthy due to the @s and _s everywhere (althoug Lean4's named arguments can make that slightly better). That said, actually working with these terms is often a convenient way to build up the API, by using the order structure and other operations on topologies, but this should almost be an implementation detail.
2. Type aliases are really useful when you want to endow a type with a topology that is really not (e.g propositionally) the default one. In some cases this is even what we do in pen-and-paper mathematics (e.g Bourbaki uses $\mathcal{F}_u(X, Y)$ for the functions endowed with the uniform convergence topology, or $E_s'$ for the weak-* dual of a TVS $E$).
3. The predicate class is most useful if you have examples of types whose default topology happens to be the one you want, just not definitionally. Then stating results using a predicate typeclass allows you to use the results seemlessly, without needing to rewrite an equality of topologies back and forth in your goal and hypotheses. Note also that this combines nicely with 1 and 2, because if you give the right instances then results about MyTopologyClass will automatically apply to MyAlias as well as myTopology.

[Anatole Dedecker]

To illustrate this, here are three examples currently in the library:

• For the order topology, we have 1 (docs#Preorder.topology) and 3 (docs#OrderTopology). It is very important to have 3 in this case because a lot of topologies naturally happen to coincide with the order topology, e.g the usual topology on $\mathbb{R}$ (which is not defined from the order). We use 1 for various things, but one use I want to highlight is docs#StrictMono.induced_topology_eq_preorder where we want to use topological operations (in this case docs#TopologicalSpace.induced) on it. Note however that this lemma is then immediately re-stated in terms of 3
• For the weak topology on a TVS induced by a pairing, we have only 2 (docs#WeakBilin.instTOpologicalSpace). Here 3 wouldn't make sense since there aren't a lot of spaces where the weak topology would be the default one (except maybe finite dimensional spaces). We also never had to use 1 so far, mostly thanks to docs#WeakBilin.embedding which completely characterizes the topology without resorting to actual equality of TopologicalSpaces.
• For the uniform convergence topology, we have 1 (docs#UniformOnFun.uniformSpace) and 2 (docs#UniformOnFun). Again, 3 would mostly not make sense (see note below) because the type of functions always comes with the product topology by default. Most of the theorems are proven about 2 and its canonical uniformity, but some of them actually follow from a statement about 1 (see docs#UniformOnFun.comap_eq which becomes docs#UniformOnFun.postcomp_uniformInducing).

Note: thinking about it, it may make sense to have a UniformConvergenceTopology for FunLike types, expressing e.g that the usual topology on continuous linear maps is that of bounded convergence in a nicer way than docs#ContinuousLinearMap.strongUniformity.uniformEmbedding_coeFn

[Moritz Doll]

Anatole Dedecker said:

1. Working with a concrete term of type TopologicalSpace _ should almost never be the preferred way of using a theory, because it can get quite annoying and lengthy due to the @s and _s everywhere (althoug Lean4's named arguments can make that slightly better). That said, actually working with these terms is often a convenient way to build up the API, by using the order structure and other operations on topologies, but this should almost be an implementation detail.

I think it would be very worthwhile to add named topology arguments and then see whether this approach is actually more useful in some of the API building parts that are more on the 'abstract nonsense' side (like polar topologies or S-topologies) where synonyms are a bit annoying because you might want to use mainly one topology but state some things in a different topology.

[Moritz Doll]

the only remaining downside I see is that the docs might be harder to read (is this fixable for named implicit arguments?)

[Anatole Dedecker]

Yes I agree. Note that we already have some nice notations like docs#Topology.«termUniformContinuous[_,_]» too.

[Anatole Dedecker]

Oh also there's one important caveat to "1 should never be the main entry point of the API", which is that sometimes you don't really want an API (maybe that covers Moritz's examples? I don't know enough to tell) because it's more of a gadget than an interesting definition in itself. This kind of definitions are typically here just to simplify a proof or to formulate a more interesting definition, but they may not have a lot of interest by themselves.

[Anatole Dedecker]

That said, adding 3 on top of 1 is never going to be a problem since everything stated for 3 will apply to 1. The type alias setup is a bit heavier.