Notation for (elements of) the 'zigzag topology'

Stream: mathlib4

[Robert Maxton]

By the 'zigzag topology', I mean the specialization topology on the integers with respect to a preorder where 2 * n ≺ 2 * n ± 1 for all n; if you draw this as a graph, you get the 'zigzag'

       0      2       4
...  ↙   ↘  ↙   ↘   ↙   ...
   -1      1      3

[Robert Maxton]

Defining it this way makes it easy to specify and work with general intervals (by the usual integer ordering, not the spec preorder), but I ultimately want to move towards a notation which is more directly "asking for what you want", which with these objects usually amount to the various topologies with one more or less open point than closed. My favored notation for the latter so far is e.g. [O2|C-] for L ⟶ 1 ⟵ R (where L and R are open and 1 is closed) or e.g. [O-|C2] for L ⟵ 0 ⟶ R (where now L and R are closed and 0 is open), but I'm open to suggestions here as well.

[Robert Maxton]

Mostly, though, I need a convenient way to refer to the points of the topology, and I'm somewhat stuck, as I've got several competing desiderata:

• It would be good to be consistent with my definition of the underlying topology on the integers, so 0, being even, should refer to an open point and 1, being odd, to a closed point.
• It would also be good for labels to be symmetric around its center, to minimize mental arithmetic while working with such elements
  • However, in order to be subspaces of the same underlying topology, this would imply that [O2|C-] would have to be centered on 1 and [O3|C-] would have to be centered on 0.
• And, of course (and arguably most crucially), it needs to work in Lean, which limits my use of naturals and of addition-as-notation

[Robert Maxton]

So far, my own best proposal is defining Z as an element of ZigzagSeg (-n) n (where ZigzagSeg n m is essentially Icc n m on the integers with the zigzag topology), O as an element of ZigzagSeg (1 - n) (n + 1), and making HAnd and HSub so I can refer to everything as Z - 3 or O + 1... but that's kind of verbose, and requires some documentation as to what happens when you go out-of-range (it saturates, fwiw), and I'm wondering if anyone has a better idea.

[Miyahara Kō]

You can construct a specialization topology by using Topology.WithUpperSet.

[Robert Maxton]

Yes, I'm currently defining

/-- The 'zigzag' topology on `ℤ`, defined as the specialization topology with respect to
a preorder where `2 * n ≺ 2 * n ± 1` for all `n`. -/
def zigzagTopology : TopologicalSpace ℤ :=
  @WithLowerSet.instTopologicalSpace ℤ zigzagPreorder

I had a version where I defined a type synonym, gave it my zigzag ordering, put the old ordering on Lex Zigzag, and then tried to work with that; but it made simple things like succ and pred involve unfolding multiple layers of wrappers not all of which played nice with rcases, so I ultimately gave up and switched to just putting it on a non-instance def and using IsOpen[zigzagTopology] etc everywhere.

[Kenny Lau]

you can make it a local instance

[Kenny Lau]

by local attribute [instance] zigzagTopology

[Robert Maxton]

I mean, I've already gotten that bit set up and working; my current problem is with conveniently referring to (elements of) various Iccs of the zigzag topology

[Miyahara Kō]

As my opinion, Z (-3) & O 1 are preferable to Z - 3 & O + 1; when you want to prove that every $[n - m, n + m]$ is open, only one lemma IsOpen (Z m)is necessary in former style, but in latter style, three lemmas IsOpen Z, IsOpen (Z + m) IsOpen (Z - m) are necessary.

[Robert Maxton]

hmmmm.... In principle, that shouldn't really come up; there's a 'real' addition operation under the hood and both the projection from $\mathbb{Z}$ and the inclusion into $\mathbb{Z}$ are continuous, so you should be able to just translate statements about $\left[n - m, n + m\right]$ in ZigzagSeg r s into statements about $\left[\max (r, n - m), \min (n + m, s)\right]$ in $\mathbb{Z}$
But I see your point, I'm not completely sure we can count on that. I'll experiment with it a bit.

[Kenny Lau]

I am confused, you said you aren't using a type synonym, so it's just ℤ, so where is the difficulty coming from?

[Robert Maxton]

I'm not using a type synonym for ℤ; I am using a type synonym for Icc n m : Set ℤ, because that needs e.g. successor/predecessor operations that handle bounds properly

def ZigzagSeg n m := ULift (Icc n m)

in the above

[Robert Maxton]

Though I don't think the problem would go away if I didn't use a synonym; either way the problem is essentially that putting ⟨x, hx₁, hx₂⟩ everywhere is a) fragile (because of the general behavior of the anonymous constructor), b) annoying, and c) and terrible for readability

[Robert Maxton]

Basically the difficulty is:

1. ZigzagSeg n m is parameterized entirely by things that I don't actually (directly) care about when using the type; when using the type I care entirely about how many open vs. closed points in this 'standard' zigzag template I'm including, so having to decide what interval to use is just noise that also makes it harder to write useful lemmas.

   • Thus, the [O n|C m]-type notation, which standardizes a specific interval of the right 'kind' to use

2. Similarly, the actual elements of any given ZigzagSeg n m are labeled in $\mathbb{Z}$ entirely by something I don't (directly) care about, their positions on the original number line; when using the type I only really want to know a) whether its singleton is open or closed and b) where it is relative to the center of the interval.

   • Thus, bikeshedding some general "$n$ steps left/right of the origin, which is Z/O, you can tell whether it's open or closed by whether it's odd or even"-type notation.

[Aaron Liu]

oh I remember this

[Aaron Liu]

can you do something with Fin maybe

[Aaron Liu]

why do you want these segments with more open than closed points what do you do with them

[Robert Maxton]

https://ncatlab.org/nlab/show/separation+axioms+in+terms+of+lifting+properties

[Robert Maxton]

note that almost all the 'test' topologies are 'zigzags', and most are either one more open than closed or the reverse

[Aaron Liu]

interesting

[Aaron Liu]

why do they need to be subspaces of the big zigzag

[Robert Maxton]

(I actually need the tests for T2 and normal for my PR turning docs#TopCat.RelativeCWComplex into docs#Topology.RelCWComplex, but the rest I'm providing for consistency)

[Aaron Liu]

can't you just make the finite zigzags without putting them all as subspaces of the $\mathbb{Z}$-zigzag

[Robert Maxton]

Because otherwise I have to make ~6 bespoke types with bespoke preorders and their APIs
Which actually isn't hard, it's mostly copy and paste, Claude can handle it
But it makes the proofs using them kind of annoying, it's somewhat nontrivial to show how they relate/reduce to one another, and the resulting file is a solid 2k lines of boilerplate

[Aaron Liu]

oh

[Aaron Liu]

that sounds like a lot of api

[Robert Maxton]

Making them all subspaces of the big zigzag means that there's a single common API for all of them and I just have to provide a couple convenience specializations for the really common/important ones

[Aaron Liu]

I feel like you still need most of the same api you would've needed with making them separate types

[Robert Maxton]

Kinda, but since now the separate types are all just abbrevs of ZigzagSeg, I only really need to provide separate lifts for O2C1 and O1C2 (which are kind of 'primitives'/the topological basis elements the rest are built from)
And stuff like ext lemmas, instances, succ/pred/even/odd interactions, and specialization order lemmas I can just have under the ZigzagSeg namespace

[Robert Maxton]

... it's still like 1.5k lines but it's much less boilerplate-y and scales better if anyone ever finds a use for them beyond the sixish in that ncatlab page

[Kenny Lau]

what if you used ℤ ⊕ ℤ instead? (disjoint union)

[Robert Maxton]

... I'm not sure how that would help?

[Robert Maxton]

I guess it would replace all the Even/Odd conditions in my library with a matchable/rcases-able predicate

[Robert Maxton]

Which is nice, I suppose

[Robert Maxton]

but it wouldn't really change the ultimate problem of "so how do I concisely refer to specific useful intervals of this type and elements of those intervals"

[Robert Maxton]

... well, maybe it would, actually.

[Robert Maxton]

Hm.

[Robert Maxton]

Because then I could say something like, "grab the interval [-n, n] on the left/right and however many elements happen to be between them on the right/left"

[Robert Maxton]

... mm, but we still have the problem that if n is odd, then the interval is centered at 0 on whatever side that is, but if n is even, then it's centered at 1/ at zero on the opposite side

[Aaron Liu]

maybe you just need to do it

[Aaron Liu]

this really doesn't seem like an avoidable problem

[Robert Maxton]

I did :v
Or, well, I've got as far as implementing the [O n|C m] notation, I'm now working on the elements notation

[Robert Maxton]

but while I'm working I thought I'd see if there's preferences/a better way

[Aaron Liu]

Kenny Lau said:

what if you used ℤ ⊕ ℤ instead? (disjoint union)

I think this is a good idea

[Aaron Liu]

I think it might make constructing the order a bit easier too

[Aaron Liu]

why do you care where the interval is centered

[Robert Maxton]

Mostly, I care because I don't see a good way to hide it from the end user, and I don't like making the end user have to go "oh, I'm using [O n|C-] and n is even, so I need to use syntax like O + 1 and not Z + 1" every time they use my type >.>;

[Robert Maxton]

but I also don't see a great alternative

[Aaron Liu]

Robert Maxton said:

Mostly, I care because I don't see a good way to hide it from the end user, and I don't like making the end user have to go "oh, I'm using [O n|C-] and n is even, so I need to use syntax like O + 1 and not Z + 1" every time they use my type >.>;

why do you need to do a different thing depending on whether n is even

[Robert Maxton]

... mmmmmmmm
Actually, if I go with the disjoint union approach, maybe I don't...

[Robert Maxton]

Basically, it's because in this topology, every singleton set is open xor closed, and specifically evens are open and odds are closed

[Robert Maxton]

So if I say "I want three open points", then that means I have something that looks like \/0\/ -> centered on the 'top' origin, but if I say "I want four open points", then I have something that looks like \/\0/\/ -> centered on the 'bottom' origin

[Aaron Liu]

so there are two origins

[Aaron Liu]

why is this a problem

[Robert Maxton]

Suppose I want to address the even points, how do I do that?
If I have three, then (if I use the disjoint union) they're inl '' {-1, 0, 1}
If I have four, then either I have to let them be off-center and do inl '' {-1, 0, 1, 2}, say, or I have to switch to centering on the other origin

[Robert Maxton]

Though, I suppose I could do something weird and say something like ".inl 0 only exists if there's an odd number, so inl '' {-2, -1, 1, 2}"

[Robert Maxton]

That might be even more cursed tho ^.^;

[Robert Maxton]

... Well, actually, if we switch to the disjoint union case, then we naturally and clearly separate the open and closed points

[Robert Maxton]

so the option of just numbering starting from 0 becomes a whole lot more legible

[Robert Maxton]

that might be the best solution

[Kenny Lau]

Robert Maxton said:

switch to centering on the other origin

you have to do this anyway if you don't use disjoint union