topology induced by a linear order

Stream: maths

[Kevin Buzzard]

@Calle Sönne and I have a linearly ordered ring and want to talk about sequences tending to limits, so we either need the order topology, or the nhds x filter, consisting of sets which contain open intervals as a subset.

[Kevin Buzzard]

Is this in mathlib?

[Patrick Massot]

https://github.com/leanprover-community/mathlib/blob/master/src/topology/algebra/ordered.lean

[Calle Sönne]

We had a look at that but doesnt this assume there already is a topology?

[Chris Hughes]

There's the orderable topology, I guess.

[Chris Hughes]

Just make orderable_topology and topological_space variables.

[Chris Hughes]

orderable_topology says the topology is equal, but not necessarily definitionally equal to the generate_from {s | ∃a, s = {b : α | a < b} ∨ s = {b : α | b < a}}.

[Kevin Buzzard]

Like this:

variables {α : Type*} [linear_ordered_ring α] [floor_ring α]

instance : topological_space α :=
  topological_space.generate_from {s | ∃a, s = {b : α | a < b} ∨ s = {b : α | b < a}}

instance : orderable_topology α := ⟨rfl⟩

?

[Chris Hughes]

Like this
variables {α : Type*} [linear_ordered_ring α] [floor_ring α] [topological_space α] [orderable_topology α]

[Kevin Buzzard]

Oh penny drops

[Chris Hughes]

Otherwise your theorems won't apply to the reals.

[Chris Hughes]

I guess that's probably enough to deduce topological_ring

[Kevin Buzzard]

don't get us started on topological rings

[Kevin Buzzard]

Johan and I have been thinking about them all week