DiscreteTopology over the reals

Stream: Is there code for X?

[Snir Broshi]

Is there some type alias (like WithLp) that guarantees a type gets the discrete topology?
I want to use the reals but forget their natural topology.

[Floris van Doorn]

The way to find out this question yourself: go to docs#DiscreteTopology, click on ▶︎ Instances and look if there is an instance on a type synonym for an arbitrary type. docs#TopCat.discrete (coerced to a type) seems to be doing this.

[Anatole Dedecker]

That said, a more elementary type alias would be welcome I think.

[Snir Broshi]

Floris van Doorn said:

The way to find out this question yourself: go to docs#DiscreteTopology, click on ▶︎ Instances and look if there is an instance on a type synonym for an arbitrary type. docs#TopCat.discrete (coerced to a type) seems to be doing this.

I loogled ⊢ DiscreteTopology _ before asking this, and found nothing, I don't think the instances in the docs will find more. It's a cool feature but it doesn't show the signatures so it's harder to find stuff

docs#TopCat.discrete seems to be much more than a type alias (which should be the identity function), and importing category theory for a topology instance is weird

[Snir Broshi]

btw are discrete topologies initial/terminal objects in TopCat?

[Sébastien Gouëzel]

In Counterexample/Phillips.lean, I start with

/-- A copy of a type, endowed with the discrete topology -/
def DiscreteCopy (α : Type u) : Type u :=
  α

instance : TopologicalSpace (DiscreteCopy α) :=
  ⊥

instance : DiscreteTopology (DiscreteCopy α) :=
  ⟨rfl⟩

(as I need to work with a discrete copy of the real line).

[Snir Broshi]

Cool, I didn't know that loogle doesn't index Counterexamples, I guess the docs search does find more

[Adam Topaz]

Snir Broshi said:

btw are discrete topologies initial/terminal objects in TopCat?

What do you mean by this? The discrete topology on a type $X$ is initial in the category of topologies on $X$, is this what you're referring to?

[Junyan Xu]

TopCat doesn't fix a space and the initial and terminal objects there are empty spaces and singleton spaces respectively, with their respective unique topology.

[Snir Broshi]

Adam Topaz said:

What do you mean by this? The discrete topology on a type $X$ is initial in the category of topologies on $X$, is this what you're referring to?

I was asking about TopCat specifically and not Top X because I was wondering why docs#TopCat.discrete was defined

Junyan Xu said:

TopCat doesn't fix a space and the initial and terminal objects there are empty spaces and singleton spaces respectively, with their respective unique topology.

Oh, then I guess the reason docs#TopCat.discrete exists is docs#TopCat.adj₁, though adjunction is beyond my category theory knowledge

[Aaron Liu]

Continuous maps from the discrete topology are 1-1 with just regular old functions on a suitibly natural way

[Dagur Asgeirsson]

Snir Broshi said:

Oh, then I guess the reason docs#TopCat.discrete exists is docs#TopCat.adj₁, though adjunction is beyond my category theory knowledge

TopCat.discrete is just the functor that takes a set and gives it the discrete topology, as an object of the category of topological spaces. Its existence has nothing to do with the adjunction (btw, the name TopCat.adj₁ should be changed to something more descriptive), this can be a useful thing to do regardless of any adjunction. But it should only be used if you intend to do stuff in the category of topological spaces, it's not the correct way in general to equip a type with the discrete topology, as others have pointed out.

[Snir Broshi]

Anyway, getting back on topic:

[Snir Broshi]

/poll Name suggestions for a type alias?

[Edward van de Meent]

what if we co-opt the CategoryTheory.Discrete type alias, just how Opposite both endows a type with the opposite ordering and category structure? will that cause issues?

[Edward van de Meent]

(we can probably just move it into the _root_ namespace if we do this)

[Edward van de Meent]

i do realize that this isn't quite a fair comparison, as topologies don't directly induce a category structure on the same type... (they do via the specialization ordering, but that's not quite as directly as i was thinking)

[Snir Broshi]

Edward van de Meent said:

what if we co-opt the CategoryTheory.Discrete type alias, just how Opposite both endows a type with the opposite ordering and category structure? will that cause issues?

I didn't know docs#CategoryTheory.Discrete existed, I like this idea!

btw I omitted the Topology namespaces from the poll options because I assumed it was obvious (although many topology stuff are in _root_ for some reason), but I guess not

[Aaron Liu]

Edward van de Meent said:

what if we co-opt the CategoryTheory.Discrete type alias, just how Opposite both endows a type with the opposite ordering and category structure? will that cause issues?

I don't think that's how Opposite works, since we also have docs#OrderDual which does exactly that (the category structure is inherited from the order)

[Edward van de Meent]

Ah, you're right, I confused the two

[Edward van de Meent]

Forget what I said