Formalising topological nets

Stream: maths

[Esteban Martínez Vañó]

Hi everyone.

I'm trying to formalice nets and, for that, I've done the following:

import Mathlib.Topology.Instances.Real

section

open Set Filter Topology

class Net (X: Type) [TopologicalSpace X] where
  D: Type
  le: D → D → Prop
  le_refl: ∀ (d: D), le d d
  le_trans: ∀ (d e f: D), le d e → le e f → le d f
  directed_set : ∀ (d e : D), ∃ (f : D), le d f ∧ le e f
  net : D → X

infix:50 " ≼ " => Net.le

def Net_limit {X: Type} [TopologicalSpace X] (s : Net X) (x : X) : Prop :=
  ∀ U ∈ 𝓝 x, ∃ (d₀ : s.D), ∀ (d : s.D), d ≼ d₀ → s.net d ∈ U

From there, I was trying to prove some characterizations using nets:

theorem Net_closure {X: Type} [TopologicalSpace X] (A: Set X) (x : X):
  x ∈ closure A ↔ ∃ (s: Net X), (∀ (d: s.D), s.net d ∈ A) ∧ Net_limit s x := by
    constructor
    · intro h
      sorry
    · intro h
      rcases h with ⟨s, s_prop⟩
      rw [mem_closure_iff_nhds]
      intro t ht
      rw [nonempty_def]
      have limit_s := s_prop.right
      dsimp [Net_limit] at limit_s
      have := limit_s t ht
      rcases this with ⟨d₀, hd₀⟩
      let x₀ := s.net d₀
      have x₀inA : x₀ ∈ A := by
        exact s_prop.left d₀
      have x₀int : x₀ ∈ t := by
        apply hd₀ d₀ (Net.le_refl d₀)
      use x₀
      simp
      constructor <;> assumption

theorem Net_closed {X: Type} [TopologicalSpace X] (C: Set X) :
  IsClosed C ↔ ∀ (x : X), ∀ (s : Net X), (∀ (d: s.D), s.net d ∈ C) → Net_limit s x → x ∈ C := by
    constructor
    · intro h_closed
      rw [← closure_subset_iff_isClosed] at h_closed
      intro x s net_prop net_limit
      apply h_closed
      rw [Net_closure C x]
      use s
    · intro h
      rw [← closure_subset_iff_isClosed]
      intro c cincl
      rw [Net_closure] at cincl
      rcases cincl with ⟨s, s_prop⟩
      exact h c s s_prop.left s_prop.right

Now, my problem is that, in the implication of the theorem "Net_closure" I have to construct a net where the directed set is 𝓝 x, but it does not have the correct type.

How can I construct the needed net or, maybe better, is there another way of defining a net?

[Jireh Loreaux]

Is there a reason you want nets and you don't want to simply use filters?

[Esteban Martínez Vañó]

Well, I'm use to work with nets so if I can implement them it would be good for future implementations in my work field, but it is mainly a practise exercise I want to do just to learn.

[Patrick Massot]

You need to tell more about what you want informally if you want help. But it is very very likely that Jireh’s answer is the most helpful one in the long run: forget about nets and learn to love filters.

[Esteban Martínez Vañó]

Well, what I want is to formalice nets. The problem is that with the definition of net that I have, the type of "D" is fixed, and so If a need a net with directed set, for example, 𝓝 x, then the types are in conflict and I cannot define the net I want to

[Yaël Dillies]

We understand that you want to formalise nets. Patrick's question is "What do you want to formalise nets for?"

[Esteban Martínez Vañó]

I've already said it. I'm trying as an exercise because I'm still learning. And, as a side product, if I get it then it will be useful to formalice some other things that I have in mind. But, as I say, now is mainly to train myself and to see if it is possible

[Yaël Dillies]

Esteban Martínez Vañó said:

I'm trying as an exercise because I'm still learning

That is a valid reason, although in this specific case I think your learning could be more usefully directed towards learning how to use filters

Esteban Martínez Vañó said:

it will be useful to formalice some other things that I have in mind

What are those other things?

[Esteban Martínez Vañó]

Yaël Dillies ha dicho:

What are those other things?

I don't have a concrete result in mind. I'm planning on formalizing some functional analysis results and we usually work with nets so it will be more comfortable for me.

I'm not saying that those results cannot be proved by using filters (I theoretically know what filters are and how they relate to nets, that's not the problem) and I will probably adapt the proofs to filters because if the library is written like that I know it will be easier.

So, as said, this is just an exercise and a challenge. To see if it can be done.

[Patrick Massot]

I'm sorry my question wasn't clear enough. Could you tell us the informal story you try to formalize? Saying "the types are in conflict" is simply not enough to understand what you want to say.

[Esteban Martínez Vañó]

Oh sorry. I don't have time now, but I'll explain it better the moment I can

[Jireh Loreaux]

Note: I also work in functional analysis (more specifically, operator algebras). There haven't been any issues working with filters, and in fact, they end up being so much nicer than nets, not least because it means you don't have to care an index set around, as you're discovering.

As an example, I originally introduced docs#Bornology into Mathlib exactly because I wanted to talk about the docs#cobounded filter, so that I could eventually get around to making #8246, which is a fantastic simplification of a result I'm sure you're familiar with.

Of course, you're still welcome to formalize nets for learning purposes (or whatever reason), but to be honest, I think you would get more benefit from going directly for some nice functional analysis result that we don't have yet. Then, when you get to the point where you would want to use nets, turn around and use filters instead.

[Esteban Martínez Vañó]

Jireh Loreaux ha dicho:

Of course, you're still welcome to formalize nets for learning purposes (or whatever reason), but to be honest, I think you would get more benefit from going directly for some nice functional analysis result that we don't have yet. Then, when you get to the point where you would want to use nets, turn around and use filters instead.

I'll have it in mind, but now I want to know if the problem I have can be solved, because it could be useful anyways when trying to define another kind of structure that has no analog.

Patrick Massot ha dicho:

I'm sorry my question wasn't clear enough. Could you tell us the informal story you try to formalize? Saying "the types are in conflict" is simply not enough to understand what you want to say.

My problem is that I've defined, for the Net Class, the type of the directed set to be "Type". But, for example, in the proof of the theorem I've named "Net_closure", I need to construct a net where the directed set is 𝓝 x (for some x), and this term has type "Filter X", so I cannot use it as a directed set with my definition of the class. I mean, in the proof I'd like to have a line of the form:

let s : Net X := {
D := 𝓝 x
...
}

But this would result in an error:

type mismatch
𝓝 x
has type
Filter X : Type
but is expected to have type
Type : Type 1

So my main question is if it is a way to specify the type of the directed set in the definition of the class in such a way that I would be able to construct instances of the class for any term as directed set.

I hope I've explained myself better now.

[Patrick Massot]

You could use {u // u ∈ 𝓝 x), or the coercion from (𝓝 x).sets.

[Patrick Massot]

But I still don’t see how you hope to make a map from this to X.

[Esteban Martínez Vañó]

Patrick Massot ha dicho:

But I still don’t see how you hope to make a map from this to X.

I was thinking in something like:

r : {V | V ∈ 𝓝 x} → X := fun V ↦ if h: ∃ (y : X), y ∈ V ∩ A then Classical.choose h else x

But it doesn't work because V does not have type Set X.

[Patrick Massot]

What if you write fun ⟨V, V_in⟩ ↦ if h: ∃ (y : X), y ∈ V ∩ A then Classical.choose h else x?

[Esteban Martínez Vañó]

Could you explain me how does this work? What is the term ⟨V, V_in⟩?

[Esteban Martínez Vañó]

Don't worry, I've understood it now :)

[Esteban Martínez Vañó]

Thanks to everyone. I've managed to prove it.

theorem Net_closure {X: Type} [TopologicalSpace X] (A: Set X) (x : X):
  x ∈ closure A ↔ ∃ (s: Net X), (∀ (d: s.D), s.net d ∈ A) ∧ Net_limit s x := by
    constructor
    · intro h
      have existence : ∀ V ∈ (𝓝 x), ∃ (y : X), y ∈ V ∩ A := by
        intro V V_nhds
        rw [mem_closure_iff_nhds] at h
        have int_nonempty := h V V_nhds
        rwa [nonempty_iff_ne_empty, eq_nonempty] at int_nonempty
      let r : {V | V ∈ 𝓝 x} → X := fun ⟨V, V_in⟩ ↦ if h: ∃ (y : X), y ∈ V ∩ A then Classical.choose h else x
      let s : Net X := {
        D := {V | V ∈ 𝓝 x}
        le := fun ⟨V, V_in⟩ ↦ (fun ⟨U, U_in⟩ ↦ V ⊆ U)
        le_refl := by
          intro U
          dsimp
          rfl
        le_trans := by
          intro U  V W
          dsimp
          intro VsubU WsubV
          apply subset_trans VsubU WsubV
        directed_set := by
          intro U V
          dsimp
          have : ↑U ∪ ↑V ∈ 𝓝 x := by
            have U_nhds:= U.2
            dsimp at U_nhds
            have V_nhds:= V.2
            dsimp at V_nhds
            rw [mem_nhds_iff] at *
            rcases U_nhds with ⟨U₀, U_eq⟩
            rcases V_nhds with ⟨V₀, V_eq⟩
            use U₀ ∪ V₀
            constructor
            · apply union_subset_union U_eq.1 V_eq.1
            · constructor
              · apply IsOpen.union U_eq.2.1 V_eq.2.1
              · rw [mem_union]
                left
                exact U_eq.2.2
          use ⟨U ∪ V, this⟩
          dsimp
          constructor
          · apply subset_union_left
          · apply subset_union_right
        net := r}
      use s
      constructor
      · intro d
        dsimp [s, r]
        rw [dif_pos (existence d.1 d.2)]
        have := Classical.choose_spec (existence d.1 d.2)
        rw [mem_inter_iff] at this
        exact this.2
      · dsimp [Net_limit]
        intro U U_nhds
        use ⟨U, U_nhds⟩
        intro d le_eq
        dsimp [Net.net, r]
        rw [dif_pos (existence d.1 d.2)]
        dsimp [Net.le] at le_eq
        have := Classical.choose_spec (existence d.1 d.2)
        have := this.1
        exact le_eq this

[Esteban Martínez Vañó]

Just one more thing.

If in a theorem there are two nets s s' : Net X , when I have two terms d : s.D and d' : s'.D , in the infoview it appears  "d: Net.D X" and "d' : Net.D X" so it is difficult to follow what type these terms have unless you hoover over the type and read the info.

Is there any way to change this so that the infoview shows something like "d:  s.D X" and "d' : s'.D X" ?

[Patrick Massot]

This is not a full proof, right? You are proving only one implication, right?

[Patrick Massot]

I encourage you to now try to clean up this code, this will be very interesting. The first advice is to extract your net construction and prove a couple of lemmas about it before doing the main proof.

[Esteban Martínez Vañó]

Patrick Massot ha dicho:

This is not a full proof, right? You are proving only one implication, right?

I don't know why I didn't copy the full proof. Here it is:

theorem Net_closure {X: Type} [TopologicalSpace X] (A: Set X) (x : X):
  x ∈ closure A ↔ ∃ (s: Net X), (∀ (d: s.D), s.net d ∈ A) ∧ Net_limit s x := by
    constructor
    · intro h
      have existence : ∀ V ∈ (𝓝 x), ∃ (y : X), y ∈ V ∩ A := by
        intro V V_nhds
        rw [mem_closure_iff_nhds] at h
        have int_nonempty := h V V_nhds
        rwa [nonempty_iff_ne_empty, eq_nonempty] at int_nonempty
      let r : {V | V ∈ 𝓝 x} → X := fun ⟨V, V_in⟩ ↦ if h: ∃ (y : X), y ∈ V ∩ A then Classical.choose h else x
      let s : Net X := {
        D := {V | V ∈ 𝓝 x}
        le := fun ⟨V, V_in⟩ ↦ (fun ⟨U, U_in⟩ ↦ U ⊆ V)
        le_refl := by
          intro U
          dsimp
          rfl
        le_trans := by
          intro U  V W
          dsimp
          intro VsubU WsubV
          apply subset_trans WsubV VsubU
        directed_set := by
          intro U V
          dsimp
          have : ↑U ∩ ↑V ∈ 𝓝 x := by
            have U_nhds:= U.2
            dsimp at U_nhds
            have V_nhds:= V.2
            dsimp at V_nhds
            rw [mem_nhds_iff] at *
            rcases U_nhds with ⟨U₀, U_eq⟩
            rcases V_nhds with ⟨V₀, V_eq⟩
            use U₀ ∩ V₀
            constructor
            · apply inter_subset_inter U_eq.1 V_eq.1
            · constructor
              · apply IsOpen.inter U_eq.2.1 V_eq.2.1
              · rw [mem_inter_iff]
                constructor
                · exact U_eq.2.2
                · exact V_eq.2.2
          use ⟨U ∩ V, this⟩
          dsimp
          constructor
          · apply inter_subset_left
          · apply inter_subset_right
        net := r}
      use s
      constructor
      · intro d
        dsimp [s, r]
        rw [dif_pos (existence d.1 d.2)]
        have := Classical.choose_spec (existence d.1 d.2)
        rw [mem_inter_iff] at this
        exact this.2
      · dsimp [Net_limit]
        intro U U_nhds
        use ⟨U, U_nhds⟩
        intro d le_eq
        dsimp [Net.net, r]
        rw [dif_pos (existence d.1 d.2)]
        dsimp [Net.le] at le_eq
        have := Classical.choose_spec (existence d.1 d.2)
        have := this.1
        exact le_eq this
    · intro h
      rcases h with ⟨s, s_prop⟩
      rw [mem_closure_iff_nhds]
      intro t ht
      rw [nonempty_def]
      have limit_s := s_prop.right
      dsimp [Net_limit] at limit_s
      have := limit_s t ht
      rcases this with ⟨d₀, hd₀⟩
      let x₀ := s.net d₀
      have x₀inA : x₀ ∈ A := by
        exact s_prop.left d₀
      have x₀int : x₀ ∈ t := by
        apply hd₀ d₀ (Net.le_refl d₀)
      use x₀
      simp
      constructor <;> assumption

[Patrick Massot]

Esteban Martínez Vañó said:

Just one more thing.

If in a theorem there are two nets s s' : Net X , when I have two terms d : s.D and d' : s'.D , in the infoview it appears  "d: Net.D X" and "d' : Net.D X" so it is difficult to follow what type these terms have unless you hoover over the type and read the info.

Is there any way to change this so that the infoview shows something like "d:  s.D X" and "d' : s'.D X" ?

This is because you made Net into a class (which is meaningless). Try changing it to structure.

[Esteban Martínez Vañó]

Patrick Massot ha dicho:

I encourage you to now try to clean up this code, this will be very interesting. The first advice is to extract your net construction and prove a couple of lemmas about it before doing the main proof.

I'll do it! All of this is just a "proof of concept" to proof myself that I'm able to do it but I'll try to clean it all as you suggest.

[Patrick Massot]

My claim is this was an interesting exercise and you can make it even more interesting by cleaning it up, even if you don’t do anything with it.

[Esteban Martínez Vañó]

Patrick Massot ha dicho:

This is because you made Net into a class (which is meaningless). Try changing it to structure.

That seems to work, but then, how can I assing a symbol (like ≼) to the order relation?

[Esteban Martínez Vañó]

I only know how to do it for classes

[Patrick Massot]

Ah, that may be trickier indeed.

[Patrick Massot]

I’ll take a look.

[Johan Commelin]

Huh? You can still implement an instance of the LE class on top of a structure Net, right?

[Johan Commelin]

Or am I misunderstanding what's happening?

[Patrick Massot]

Why did you put [TopologicalSpace X] in the definition of Net?

[Esteban Martínez Vañó]

Johan Commelin ha dicho:

Huh? You can still implement an instance of the LE class on top of a structure Net, right?

But then I cannot have the domain of the directed set as a field, because I should specify it before that, isn't it?

[Patrick Massot]

Yes, it seems

instance {X} {s : Net X} : LE s.D := ⟨Net.le s⟩

works fine.

[Esteban Martínez Vañó]

Patrick Massot ha dicho:

Why did you put [TopologicalSpace X] in the definition of Net?

Because it will always be a topological space, but I suppose I can delete it from the definition as long as it appears in the theorems and needed definitions?

[Patrick Massot]

Yes, you should remove it from the definition.

[Esteban Martínez Vañó]

Patrick Massot ha dicho:

instance {X} {s : Net X} : LE s.D := ⟨Net.le s⟩

Thanks!

Patrick Massot ha dicho:

Yes, you should remove it from the definition.

And removed it is ;)

[Patrick Massot]

Keeping it only creates useless work for Lean which will need to hunt down a topological space instance whenever it sees a net.

[Patrick Massot]

Once you will have extracted the main construction (taking a set and a point in a topological space and returning a net) into a definition, the first thing you can do is to add @[simps?] to see what kind of lemmas would be created by the simps attribute.

[Patrick Massot]

But those lemmas won’t be enough, you also want lemmas that wrap dif_pos and dif_neg.

[Esteban Martínez Vañó]

I take note of it :+1:

[Esteban Martínez Vañó]

I've formalised the main results (characterization of closed and compact sets and relation between accumulation points and subnets) and now I'm cleaning and commenting the code to see if it can be useful.

In that terms, I have a doubt. I have formalised the nets as:

structure Net (X: Type) where
  D: Type
  non_empty : ∃ (d : D), d = d
  le: D → D → Prop
  le_refl: ∀ (d: D), le d d
  le_trans: ∀ (d e f: D), le d e → le e f → le d f
  directed_set : ∀ (d e : D), ∃ (f : D), le d f ∧ le e f
  net : D → X

But I'd like to do it by first defining what a directed set is, something like:

class DirectedSet (D: Type) extends Preorder D where
  directed : ∀ (d e : D), ∃ (f : D), d ≤ f ∧ e ≤ f

And then, define nets as someting like:

structure Net' (X: Type) where
  D: Type
  -- Condition that ensures that D is a directed set
  net : D → X

And it has to be in such a way that I can access the set D with s.D, and that I can also access the order relation and its three defining properties. I mean, that I should be able to prove something like the following:

example (X : Type) (s: Net  X) : ∀ (a : s.D),  a ≤ a := by
  exact le_refl a

example (X : Type) (s: Net  X) : ∀ (d e : s.D), ∃ (f : s.D), d ≤ f ∧ e ≤ f := by
   exact DirectedSet.directed

Maybe not with that exact sintax (because it may depend on "s" in some way), but I think the idea of what I want to accomplish is clear.

Is there a way to accomplish this?

[Kim Morrison]

Have you tried

structure Net' (X: Type) where
  D: Type
  [directedSet : DirectedSet D]
  net : D → X

and then

attribute [instance] Net'.directedSet

?

[Esteban Martínez Vañó]

It seems to work but could you please explain what does the last line do?

[Kevin Buzzard]

It puts the assertion that D is a directed set into the typeclass inference system (the square bracket system).

[Esteban Martínez Vañó]

So any time a net "s" is introduced in a proof, it is also introduced (although not showed) the assertion that "s.D" is a directed set?

[Yaël Dillies]

I am not sure what you mean by "introduced but not showed". If s is a net then DirectedSet s.D is a true statement

[Esteban Martínez Vañó]

I mean that it doesn't appear in the Lean infoview as it is shown, for example, if you introduce that X is a topological space by the typeclass inference system

[Esteban Martínez Vañó]

Anyway, I think I've understood it, thanks!

[Patrick Massot]

It does not appear in exactly the same way as the fact that a product of topological spaces does not appear : it is synthesized when needed by the type class system.

[Esteban Martínez Vañó]

I've done my best to make everything clear and at the same time as simple as possible.

Nets.lean

Any suggestion is welcome and any help in how to put the archive in github is also welcome (because I've never used it and I don't have any idea of how to work with it)

Also, is it worth uploading this to mathlib? If so, what are the steps to follow?

[Kim Morrison]

The guide to contributing to Mathlib is https://leanprover-community.github.io/contribute/index.html. Please feel free to ask questions (or suggest improvements to the documentation!!)

[Kim Morrison]

Personally I think that it would be good to have nets in Mathlib. As discussed above, it is unlikely that they are ever going to be used for anything, as reviewers would probably rightly insist that any work using them was refactored to use filters instead.

One possibility would be to put them in the Archive/ folder, which clearly indicates "this is a a demonstration, but not intended to be build upon further". Do note, however, that the standards for Archive/ are meant to be quite high, because it is intended as expository work.

[Kim Morrison]

You would need to start by:

• removing the many results in your file which already exist in Mathlib, instead using the existing declarations
• fix all the errors and warnings that appear if you put this file inside Mathlib (where many more linters run than "vanilla" Lean).
• chop up this material into many different files (material about more basic notions, e.g. DirectedSet, needs to go in the appropriate files --- this is true whether or not the Net material itself was targeted at Mathlib or the Archive)
• the material on Net itself should be split into a Defs and Lemmas file.

[Patrick Massot]

In particular you can take a look at docs#IsDirected and docs#BddAbove (I only looked at the beginning of your file).

[Esteban Martínez Vañó]

Thanks to both!
I'll follow your advice and let's see how it ends