Zulip Chat Archive

Stream: maths

Topic: topology induced by a linear order


Kevin Buzzard (Mar 14 2019 at 20:04):

@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 (Mar 14 2019 at 20:04):

Is this in mathlib?

Patrick Massot (Mar 14 2019 at 20:33):

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

Calle Sönne (Mar 14 2019 at 20:43):

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

Chris Hughes (Mar 14 2019 at 20:49):

There's the orderable topology, I guess.

Chris Hughes (Mar 14 2019 at 20:52):

Just make orderable_topology and topological_space variables.

Chris Hughes (Mar 14 2019 at 20:53):

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 (Mar 14 2019 at 21:09):

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 (Mar 14 2019 at 21:18):

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

Kevin Buzzard (Mar 14 2019 at 21:20):

Oh penny drops

Chris Hughes (Mar 14 2019 at 21:20):

Otherwise your theorems won't apply to the reals.

Chris Hughes (Mar 14 2019 at 21:21):

I guess that's probably enough to deduce topological_ring

Kevin Buzzard (Mar 14 2019 at 21:21):

don't get us started on topological rings

Kevin Buzzard (Mar 14 2019 at 21:22):

Johan and I have been thinking about them all week


Last updated: Dec 20 2023 at 11:08 UTC