Order on topologies

Stream: maths

[Patrick Massot]

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]

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]

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

[Reid Barton]

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]

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]

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

[Patrick Massot]

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]

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

[Patrick Massot]

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

[Reid Barton]

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

[Reid Barton]

Okay, I missed that :+1:

[Patrick Massot]

Yes, see the first message

[Patrick Massot]

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

[Patrick Massot]

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]

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]

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

[Patrick Massot]

Currently it is not consistent in mathlib

[Patrick Massot]

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]

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]

What would be a bigger set here?

[Chris Hughes]

filter.sets isn't monotone.

[Patrick Massot]

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

[Reid Barton]

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

[Patrick Massot]

What should we do then?

[Reid Barton]

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

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Patrick Massot]

Maybe we should do antitone Galois connections as well

[Patrick Massot]

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]

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]

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

[Kevin Buzzard]

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

[Patrick Massot]

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]

Maybe the definition of the lattice structure on opens X helps? It uses Galois insertions, dual, and copy.

[Patrick Massot]

Did you write that?

[Patrick Massot]

Do you understand what's going on?

[Patrick Massot]

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]

I only want to reverse the order

[Mario Carneiro]

I think the galois insertion should be between (topological_space α) and (order_dual $ set α), not (order_dual $ topological_space α) and (set α)

[Johan Commelin]

@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]

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]

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]

I must have messed up something

[Reid Barton]

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]

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

[Patrick Massot]

Yes, it looks like a coinsertion

[Patrick Massot]

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

[Patrick Massot]

But it should be enough to lift complete lattice instances

[Reid Barton]

Yes

[Patrick Massot]

This is all so silly. I simply want to reverse my partial order which is already known to be a complete lattice.

[Kevin Buzzard]

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

[Patrick Massot]

Maybe I should keep the current Galois insertion as a local instance and then use order_dual.complete_lattice or something

[Patrick Massot]

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]

Patrick did you crash zulip

[Patrick Massot]

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]

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