Zulip Chat Archive

Stream: maths

Topic: Order on topologies


view this post on Zulip 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 t1t2t_1 \leq t_2 for topologies t1t_1 and t2t_2 but write sentences randomly using either the "finer than" or "coarser than" relation.

@Mario Carneiro @Reid Barton @Sebastien Gouezel

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Jun 07 2019 at 12:24):

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

view this post on Zulip Reid Barton (Jun 07 2019 at 12:45):

If you believe the reasonable-looking statement
(*) The identity map (X,T1)(X,T2)(X, T_1) \to (X, T_2) is continuous iff T1T2T_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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Jun 07 2019 at 13:01):

What about

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 {α β} [ : uniform_space α] [ : uniform_space β] (f : α  β) :
uniform_continuous f  .comap f   :=

view this post on Zulip 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.

view this post on Zulip Reid Barton (Jun 07 2019 at 13:03):

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

view this post on Zulip Reid Barton (Jun 07 2019 at 13:03):

Okay, I missed that :+1:

view this post on Zulip Patrick Massot (Jun 07 2019 at 13:03):

Yes, see the first message

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jun 07 2019 at 13:26):

Currently it is not consistent in mathlib

view this post on Zulip 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...)

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Jun 07 2019 at 13:27):

What would be a bigger set here?

view this post on Zulip Chris Hughes (Jun 07 2019 at 13:29):

filter.sets isn't monotone.

view this post on Zulip Patrick Massot (Jun 07 2019 at 13:45):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jun 07 2019 at 15:00):

What should we do then?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 10 2019 at 19:22):

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

view this post on Zulip Patrick Massot (Jun 10 2019 at 19:22):

Maybe we should do antitone Galois connections as well

view this post on Zulip 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

view this post on Zulip 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 HKKHH\leq K\iff K\subseteq H

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 19:29):

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

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 19:39):

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

view this post on Zulip 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  : sg, generate_open s
| univ   : generate_open univ
| inter  : s t, generate_open s  generate_open t  generate_open (s  t)
| sUnion : k, (sk, 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 13 2019 at 15:35):

Did you write that?

view this post on Zulip Patrick Massot (Jun 13 2019 at 15:35):

Do you understand what's going on?

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Jun 13 2019 at 15:36):

I only want to reverse the order

view this post on Zulip 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 α)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jun 13 2019 at 19:37):

I must have messed up something

view this post on Zulip 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

view this post on Zulip Reid Barton (Jun 13 2019 at 19:40):

You get a Galois coinsertion (if that's a real word) instead

view this post on Zulip Patrick Massot (Jun 13 2019 at 19:41):

Yes, it looks like a coinsertion

view this post on Zulip Patrick Massot (Jun 13 2019 at 19:41):

You get u l = id instead of l u = id

view this post on Zulip Patrick Massot (Jun 13 2019 at 19:42):

But it should be enough to lift complete lattice instances

view this post on Zulip Reid Barton (Jun 13 2019 at 19:42):

Yes

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 13 2019 at 19:43):

You could use the fact that the dual is a Galois nnection.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Jun 13 2019 at 20:01):

Patrick did you crash zulip

view this post on 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.

view this post on Zulip Patrick Massot (Jun 18 2019 at 08:35):

Done in https://github.com/leanprover-community/mathlib/pull/1138


Last updated: May 18 2021 at 07:19 UTC