## Stream: maths

### Topic: Order on topologies

#### Patrick Massot (Jun 07 2019 at 12:15):

I already asked this question in the middle of another thread and got no answer, let me try again:

Is the order relation on topological_space and uniform_space open for debate? Currently we have incompatibility with the order on filters, as seen in https://github.com/leanprover-community/mathlib/blob/master/src/topology/order.lean#L147-L148 and https://github.com/leanprover-community/mathlib/blob/master/src/topology/uniform_space/basic.lean#L472, generating things like https://github.com/leanprover-community/mathlib/blob/master/src/topology/uniform_space/basic.lean#L542 and generating a push-forward which is right-adjoint to pull-back
As far as I can see, real world never write $t_1 \leq t_2$ for topologies $t_1$ and $t_2$ but write sentences randomly using either the "finer than" or "coarser than" relation.

@Mario Carneiro @Reid Barton @Sebastien Gouezel

#### Sebastien Gouezel (Jun 07 2019 at 12:23):

I would agree to switch the order. I don't have strong opinion either way, but coherence over the different concepts is a valuable goal.

#### Chris Hughes (Jun 07 2019 at 12:24):

That's because the order on filters is silly, not the order on topologies.

#### Reid Barton (Jun 07 2019 at 12:45):

If you believe the reasonable-looking statement
(*) The identity map $(X, T_1) \to (X, T_2)$ is continuous iff $T_1 \le T_2$
then you should use Patrick's order, with the discrete topology at the bottom and the indiscrete topology at the top.

#### Reid Barton (Jun 07 2019 at 12:46):

However in algebraic geometry there is an "op" inserted between the morphisms of schemes and the morphisms of their structure sheaves, so perhaps one should not believe (*), I'm not sure.

#### Reid Barton (Jun 07 2019 at 12:56):

I wouldn't be against reversing the order of topologies, though it looks like a fair amount of work

#### Patrick Massot (Jun 07 2019 at 12:59):

Chris, the order on filters is nice because it makes principal monotone https://github.com/leanprover-community/mathlib/blob/master/src/order/filter/basic.lean#L358 and because it makes push forward left adjoint to pull back, and not the other way around.

#### Reid Barton (Jun 07 2019 at 13:01):

lemma to_topological_space_mono {u₁ u₂ : uniform_space α} (h : u₁ ≤ u₂) :
@uniform_space.to_topological_space _ u₁ ≤ @uniform_space.to_topological_space _ u₂ :=

lemma uniform_continuous_iff {α β} [uα : uniform_space α] [uβ : uniform_space β] (f : α → β) :
uniform_continuous f ↔ uβ.comap f ≤ uα :=


#### Patrick Massot (Jun 07 2019 at 13:03):

The first lemma means you can't change the order on topologies without changing the order on uniform structures.

#### Reid Barton (Jun 07 2019 at 13:03):

Or wait, were you going to reverse the order on uniform_space too?

#### Reid Barton (Jun 07 2019 at 13:03):

Okay, I missed that :+1:

#### Patrick Massot (Jun 07 2019 at 13:03):

Yes, see the first message

#### Patrick Massot (Jun 07 2019 at 13:04):

The second lemma means the order on uniform spaces currently doesn't play nicely with the order on filters

#### Patrick Massot (Jun 07 2019 at 13:20):

Chris, the order on filters is nice because it makes principal monotone https://github.com/leanprover-community/mathlib/blob/master/src/order/filter/basic.lean#L358 and because it makes push forward left adjoint to pull back, and not the other way around.

I guess this is only one argument. I like push-forward to be the left adjoint because this is what happens for functions acting on subsets. But of course sheaves are the other way around.

#### Kevin Buzzard (Jun 07 2019 at 13:25):

This is sort of like saying "wouldn't it be great if all -1's were +1's?". It's not so clear that there's a perfect answer here. I guess I mean that it is clear that there is not a perfect answer here.

#### Patrick Massot (Jun 07 2019 at 13:26):

We don't want a perfect answer here. We want something consistent across filters, topology and uniform structures

#### Patrick Massot (Jun 07 2019 at 13:26):

Currently it is not consistent in mathlib

#### Patrick Massot (Jun 07 2019 at 13:27):

And if we add the constraint that principal is monotone then we get that the correct order is the one we currently have on filters (unless we want to reverse the orderings on subsets...)

#### Kevin Buzzard (Jun 07 2019 at 13:27):

Is it possible for everything to be consistent? Or are you just focussed on some small subset of inconsistent things, and if you change to make it consistent that then some other small subset will be inconsistent?

#### Patrick Massot (Jun 07 2019 at 13:27):

What would be a bigger set here?

#### Chris Hughes (Jun 07 2019 at 13:29):

filter.sets isn't monotone.

#### Patrick Massot (Jun 07 2019 at 13:45):

Who cares? The goal of the theory is to hide this function as much as possible

#### Reid Barton (Jun 07 2019 at 14:43):

We can't make everything consistent, but it doesn't mean that every possible convention is equally good

#### Patrick Massot (Jun 07 2019 at 15:00):

What should we do then?

#### Reid Barton (Jun 07 2019 at 15:04):

I'm happy with the change you suggested--as long as I don't have to be the one to implement it

#### Patrick Massot (Jun 10 2019 at 19:15):

I just discovered a flaw in this plan: https://github.com/leanprover-community/mathlib/blob/master/src/topology/order.lean#L110-L111

#### Patrick Massot (Jun 10 2019 at 19:16):

I'm afraid the Galois insertion involving the topology generated by a collection of subset is the motivation behind the weird order on topologies

#### Johan Commelin (Jun 10 2019 at 19:22):

I suppose you could use order_dual and copy, if you really want...

#### Patrick Massot (Jun 10 2019 at 19:22):

Maybe we should do antitone Galois connections as well

#### Patrick Massot (Jun 10 2019 at 19:23):

At some point we'll have to face the fact that fundamental theorem of Galois theory is not a Galois connection, as currently defined in mathlib

#### Kevin Buzzard (Jun 10 2019 at 19:28):

At some point we'll have to face the fact that fundamental theorem of Galois theory is not a Galois connection, as currently defined in mathlib

it's OK, we can just define the order on subgroups to be $H\leq K\iff K\subseteq H$

#### Kevin Buzzard (Jun 10 2019 at 19:29):

Probably that's what the order is in mathlib anyway :P

#### Kevin Buzzard (Jun 10 2019 at 19:39):

But don't do it on the subfields as well ;-)

#### Patrick Massot (Jun 13 2019 at 15:28):

I tried using order_dual to change the partial order on topologies but still have a Galois insertion, so that I can list the complete lattice instance from set (set a). But then of course the has_top instance is still the wrong one. Is this the issue the copy is meant to solve? I don't understand at all this copy thing in order.fiilter.basic. The beginning of the story looks like:

import topology.basic

open set filter lattice classical
local attribute [instance] prop_decidable

universes u v w

namespace topological_space
variables {α : Type u}

/-- The least topology containing a collection of basic sets. -/
inductive generate_open (g : set (set α)) : set α → Prop
| basic  : ∀s∈g, generate_open s
| univ   : generate_open univ
| inter  : ∀s t, generate_open s → generate_open t → generate_open (s ∩ t)
| sUnion : ∀k, (∀s∈k, generate_open s) → generate_open (⋃₀ k)

/-- The smallest topological space containing the collection g of basic sets -/
def generate_from (g : set (set α)) : topological_space α :=
{ is_open        := generate_open g,
is_open_univ   := generate_open.univ g,
is_open_inter  := generate_open.inter,
is_open_sUnion := generate_open.sUnion  }

end topological_space

section lattice

variables {α : Type u} {β : Type v}

instance : partial_order (topological_space α) :=
{ le          := λ t s, s.is_open ≤ t.is_open,
le_antisymm := assume t s h₁ h₂, topological_space_eq $le_antisymm h₂ h₁, le_refl := assume t, le_refl t.is_open, le_trans := assume a b c h₁ h₂, le_trans h₂ h₁ } lemma le_generate_from_iff_subset_is_open {g : set (set α)} {t : topological_space α} : t ≤ topological_space.generate_from g ↔ g ⊆ {s | t.is_open s} := iff.intro (assume ht s hs, ht _$ topological_space.generate_open.basic s hs)
(assume hg s hs, hs.rec_on (assume v hv, hg hv)
t.is_open_univ (assume u v _ _, t.is_open_inter u v) (assume k _, t.is_open_sUnion k))

protected def mk_of_closure (s : set (set α))
(hs : {u | (topological_space.generate_from s).is_open u} = s) : topological_space α :=
{ is_open        := λu, u ∈ s,
is_open_univ   := hs ▸ topological_space.generate_open.univ _,
is_open_inter  := hs ▸ topological_space.generate_open.inter,
is_open_sUnion := hs ▸ topological_space.generate_open.sUnion }

lemma mk_of_closure_sets {s : set (set α)}
{hs : {u | (topological_space.generate_from s).is_open u} = s} :
mk_of_closure s hs = topological_space.generate_from s :=
topological_space_eq hs.symm

def gi_generate_from (α : Type*) :
@galois_insertion _ (order_dual $topological_space α) _ _ topological_space.generate_from (λt:topological_space α, {s | t.is_open s}):= { gc := assume t g, le_generate_from_iff_subset_is_open, le_l_u := assume t s hs, topological_space.generate_open.basic s hs, choice := λg hg, mk_of_closure g (subset.antisymm hg$  le_generate_from_iff_subset_is_open.1 $le_refl _), choice_eq := assume s hs, mk_of_closure_sets } instance {α : Type u} : complete_lattice (topological_space α) := (gi_generate_from α).lift_complete_lattice  This is accepted by Lean, but then I still have the discrete topology at top. I'm sorry this conversation is very sparse, but I'm at a conference, with very little Lean time. #### Johan Commelin (Jun 13 2019 at 15:31): Maybe the definition of the lattice structure on opens X helps? It uses Galois insertions, dual, and copy. #### Patrick Massot (Jun 13 2019 at 15:35): Did you write that? #### Patrick Massot (Jun 13 2019 at 15:35): Do you understand what's going on? #### Patrick Massot (Jun 13 2019 at 15:36): I don't understand why it seems to involve additional proofs in copy on top of the Galois insertion. How can there be any mathematical content? #### Patrick Massot (Jun 13 2019 at 15:36): I only want to reverse the order #### Mario Carneiro (Jun 13 2019 at 15:51): I think the galois insertion should be between (topological_space α) and (order_dual$ set α), not (order_dual $topological_space α) and (set α) #### Johan Commelin (Jun 13 2019 at 17:41): @Patrick Massot I wrote it with help of Johannes. I think copy allows you to redefine the data parts of the structure, for better defeqs. But then you get proof obligations that the data is provably equal to what you get out of the duality. (That's what my memory tells me.) Maybe @Johannes Hölzl can enlighten us. #### Patrick Massot (Jun 13 2019 at 19:35): I think the galois insertion should be between (topological_space α) and (order_dual$ set α), not (order_dual $topological_space α) and (set α) Isn't this ruining the le_l_u axiom of Galois insertions? #### Patrick Massot (Jun 13 2019 at 19:37): This is really weird, it looks like, starting from a Galois insertion, if you switch order on both sides you don't get a Galois insertion in the other direction #### Patrick Massot (Jun 13 2019 at 19:37): I must have messed up something #### Reid Barton (Jun 13 2019 at 19:40): This is really weird, it looks like, starting from a Galois insertion, if you switch order on both sides you don't get a Galois insertion in the other direction I haven't been following today's discussion but this is indeed not the case #### Reid Barton (Jun 13 2019 at 19:40): You get a Galois coinsertion (if that's a real word) instead #### Patrick Massot (Jun 13 2019 at 19:41): Yes, it looks like a coinsertion #### Patrick Massot (Jun 13 2019 at 19:41): You get u l = id instead of l u = id #### Patrick Massot (Jun 13 2019 at 19:42): But it should be enough to lift complete lattice instances #### Reid Barton (Jun 13 2019 at 19:42): Yes #### Patrick Massot (Jun 13 2019 at 19:42): This is all so silly. I simply want to reverse my partial order which is already known to be a complete lattice. #### Kevin Buzzard (Jun 13 2019 at 19:43): You could use the fact that the dual is a Galois nnection. #### Patrick Massot (Jun 13 2019 at 19:43): Maybe I should keep the current Galois insertion as a local instance and then use order_dual.complete_lattice or something #### Patrick Massot (Jun 13 2019 at 19:56): import topology.basic open set filter lattice universes u v w namespace topological_space variables {α : Type u} /-- The least topology containing a collection of basic sets. -/ inductive generate_open (g : set (set α)) : set α → Prop | basic : ∀s∈g, generate_open s | univ : generate_open univ | inter : ∀s t, generate_open s → generate_open t → generate_open (s ∩ t) | sUnion : ∀k, (∀s∈k, generate_open s) → generate_open (⋃₀ k) /-- The smallest topological space containing the collection g of basic sets -/ def generate_from (g : set (set α)) : topological_space α := { is_open := generate_open g, is_open_univ := generate_open.univ g, is_open_inter := generate_open.inter, is_open_sUnion := generate_open.sUnion } section lattice def old_order : partial_order (topological_space α) := { le := λt s, t.is_open ≤ s.is_open, le_antisymm := assume t s h₁ h₂, topological_space_eq$ le_antisymm h₁ h₂,
le_refl     := assume t, le_refl t.is_open,
le_trans    := assume a b c h₁ h₂, @le_trans _ _ a.is_open b.is_open c.is_open h₁ h₂ }

local attribute [instance] old_order

lemma generate_from_le_iff_subset_is_open {g : set (set α)} {t : topological_space α} :
topological_space.generate_from g ≤ t ↔ g ⊆ {s | t.is_open s} :=
iff.intro
(assume ht s hs, ht _ $topological_space.generate_open.basic s hs) (assume hg s hs, hs.rec_on (assume v hv, hg hv) t.is_open_univ (assume u v _ _, t.is_open_inter u v) (assume k _, t.is_open_sUnion k)) protected def mk_of_closure (s : set (set α)) (hs : {u | (topological_space.generate_from s).is_open u} = s) : topological_space α := { is_open := λu, u ∈ s, is_open_univ := hs ▸ topological_space.generate_open.univ _, is_open_inter := hs ▸ topological_space.generate_open.inter, is_open_sUnion := hs ▸ topological_space.generate_open.sUnion } lemma mk_of_closure_sets {s : set (set α)} {hs : {u | (topological_space.generate_from s).is_open u} = s} : topological_space.mk_of_closure s hs = topological_space.generate_from s := topological_space_eq hs.symm def gi_generate_from (α : Type*) : galois_insertion topological_space.generate_from (λt:topological_space α, {s | t.is_open s}) := { gc := assume g t, generate_from_le_iff_subset_is_open, le_l_u := assume ts s hs, topological_space.generate_open.basic s hs, choice := λg hg, topological_space.mk_of_closure g (subset.antisymm hg$ generate_from_le_iff_subset_is_open.1 $le_refl _), choice_eq := assume s hs, mk_of_closure_sets } lemma generate_from_mono {α} {g₁ g₂ : set (set α)} (h : g₁ ⊆ g₂) : topological_space.generate_from g₁ ≤ topological_space.generate_from g₂ := (gi_generate_from _).gc.monotone_l h def old_complete_lattice {α : Type u} : complete_lattice (topological_space α) := (gi_generate_from α).lift_complete_lattice end lattice instance : partial_order (topological_space α) := { le := λ t s, s.is_open ≤ t.is_open, le_antisymm := assume t s h₁ h₂, topological_space_eq$ le_antisymm h₂ h₁,
le_refl     := assume t, le_refl t.is_open,
le_trans    := assume a b c h₁ h₂, le_trans h₂ h₁ }

instance : complete_lattice (topological_space α) :=
@order_dual.lattice.complete_lattice _ old_complete_lattice
end topological_space

class discrete_topology (α : Type*) [t : topological_space α] : Prop :=
(eq_top : t = ⊥)

@[simp] lemma is_open_discrete {α : Type*} [topological_space α] [discrete_topology α] (s : set α) :
is_open s :=
(discrete_topology.eq_top α).symm ▸ trivial


#### Reid Barton (Jun 13 2019 at 20:01):

Patrick did you crash zulip

#### Patrick Massot (Jun 14 2019 at 13:28):

Patrick did you crash zulip

Indeed Zulip crashed while I was editing my message. And then talks resumed, and discussions, and dinner and wasn't able to return to here before bed. Anyway, I wanted to say that the code above seems to work.

#### Patrick Massot (Jun 18 2019 at 08:35):

Last updated: May 18 2021 at 07:19 UTC