Zulip Chat Archive

Stream: Is there code for X?

Topic: S1 and other topological spaces


view this post on Zulip Pedro Minicz (Sep 22 2020 at 16:30):

Is the circle S1 in mathlib? Or R/Z?

view this post on Zulip Johan Commelin (Sep 22 2020 at 16:32):

@Patrick Massot I guess you have been thinking about the circle for Sphere eversion. What's the status?

view this post on Zulip Heather Macbeth (Sep 22 2020 at 16:55):

@Pedro Minicz What kind of circle do you want? The manifold circle doesn't exist yet.

view this post on Zulip Heather Macbeth (Sep 22 2020 at 16:56):

But it exists as a topological space quite easily.

view this post on Zulip Heather Macbeth (Sep 22 2020 at 16:57):

You could probably even build a manifold structure on S1 "by hand" at the moment.

view this post on Zulip Heather Macbeth (Sep 22 2020 at 16:58):

But no one has done it because it seems better to wait until submanifolds and quotient manifolds are defined, then construct it either as a submanifold of R^2 or as a quotient manifold of R^1 (or both).

view this post on Zulip Pedro Minicz (Sep 22 2020 at 17:04):

Heather Macbeth said:

Pedro Minicz What kind of circle do you want? The manifold circle doesn't exist yet.

The topological space

view this post on Zulip Kevin Buzzard (Sep 22 2020 at 17:04):

You could just take the subspace of R^2, that will get a topology.

view this post on Zulip Pedro Minicz (Sep 22 2020 at 17:04):

Currently I am working with a quotient space R/Z, which is quite easy to make

view this post on Zulip Pedro Minicz (Sep 22 2020 at 17:05):

I was wondering if something was defined on mathlib

view this post on Zulip Heather Macbeth (Sep 22 2020 at 17:05):

I remember it's mentioned as a topological space in @Sebastien Gouezel 's manifolds exercises,
https://github.com/leanprover-community/lftcm2020/blob/master/src/exercises_sources/friday/manifolds.lean

view this post on Zulip Kevin Buzzard (Sep 22 2020 at 17:05):

What is the question here? For example if you have a type R/Z and a map from R and a topology on R you'll be able to give R/Z the quotient topology, which will be the right one.

view this post on Zulip Heather Macbeth (Sep 22 2020 at 17:05):

Oh -- in fact it's a metric space, docs#metric.sphere

view this post on Zulip Heather Macbeth (Sep 22 2020 at 17:07):

And yes, the quotient space should also work, are you using the quotient topological space API? docs#quotient.topological_space

view this post on Zulip Pedro Minicz (Sep 22 2020 at 17:08):

Yes. Currently I have this:

import topology.constructions
import topology.instances.real

noncomputable theory

def r (a b : ) : Prop :=  k : , a - b = k

lemma r_refl : reflexive r :=
λ _, 0, by simp

lemma r_symm : symmetric r :=
λ _ _ a, _⟩, -a, by { push_cast, linarith }⟩

lemma r_trans : transitive r :=
λ _ _ _ a, _ b, _⟩, a + b, by { push_cast, linarith }⟩

lemma r_equiv : equivalence r := r_refl, r_symm, r_trans

def r_setoid : setoid  := r, r_equiv

def RZ : Type := quotient r_setoid
notation `/` := RZ

def RZ.mk :   / := @quotient.mk _ r_setoid

instance : topological_space / :=
by { unfold RZ, apply_instance }

lemma quotient_map_mk : quotient_map RZ.mk :=
by { unfold RZ.mk, exact quotient_map_quot_mk }

example : ¬  f, function.right_inverse RZ.mk f  continuous f :=
sorry

view this post on Zulip Pedro Minicz (Sep 22 2020 at 17:08):

Heather Macbeth said:

Oh -- in fact it's a metric space, docs#metric.sphere

docs#metric.sphere looks interesting. Good to know it exists.

view this post on Zulip Heather Macbeth (Sep 22 2020 at 17:10):

btw, I think @Yury G. Kudryashov has also worked with circles, eg
https://github.com/leanprover-community/mathlib/blob/f2458d6/src/dynamics/circle/rotation_number/translation_number.lean

view this post on Zulip Heather Macbeth (Sep 22 2020 at 17:11):

I don't know anything about that file, maybe he just treates functions on the circle as periodic functions on the line.

view this post on Zulip Heather Macbeth (Sep 22 2020 at 17:12):

@Kevin Buzzard (or other algebraists), does mathlib have quotients by a group action (rather than by a setoid)?

view this post on Zulip Kevin Buzzard (Sep 22 2020 at 17:13):

I don't know. We can quotient groups by non-normal subgroups but I'm not sure about general group actions.

view this post on Zulip Johan Commelin (Sep 22 2020 at 17:15):

Yes, I think we have the type of orbits, but no topology afaik

view this post on Zulip Kevin Buzzard (Sep 22 2020 at 17:16):

But presumably the topology will often just be the quotient topology, which we also have

view this post on Zulip Heather Macbeth (Sep 22 2020 at 17:16):

Johan Commelin said:

Yes, I think we have the type of orbits, but no topology afaik

maybe @Pedro Minicz could adapt his code to do this :grinning:

view this post on Zulip Pedro Minicz (Sep 22 2020 at 17:22):

I'd love to! I am learning topology/algebra now on grad school, so I am newbie, but would love to contribute

view this post on Zulip Adam Topaz (Sep 22 2020 at 17:41):

Heather Macbeth said:

Kevin Buzzard (or other algebraists), does mathlib have quotients by a group action (rather than by a setoid)?

This is fairly easy to do with quot as opposed to quotient.

view this post on Zulip Adam Topaz (Sep 22 2020 at 17:44):

import algebra
variables (M : Type*) [monoid M] (α : Type*) [mul_action M α]
def foo := quot (λ (x y : α),  (a : M), a  x = y)

view this post on Zulip Kevin Buzzard (Sep 22 2020 at 17:45):

Skipping the proof that it's an equivalence relation, even though it is :-) (oh actually it isn't because Adam used monoids not groups!)

view this post on Zulip Adam Topaz (Sep 22 2020 at 18:00):

quot never gets the respect it deserves...

view this post on Zulip Kevin Buzzard (Sep 22 2020 at 18:01):

Kenny has suggested to me that this sort of thing should be used more often, e.g. maybe you should be able to quotient a group by a subset, and it will quotient by the subgroup it generates.

view this post on Zulip Kyle Miller (Sep 22 2020 at 18:22):

Is there any way to describe the equivalence relation for a monoid action on a set other than "the equivalence relation generated by (λ (x y : α), ∃ (a : M), a • x = y)"? (For quotient-philes, there's eqv_gen.setoid, but all that it seems to really give you is not needing to use quot.exact or quot.eqv_gen_sound)

view this post on Zulip Adam Topaz (Sep 22 2020 at 18:26):

It's complicated to describe in this case. The best I can come up with is this: The forgetful functor from sets with a group action to sets with a monoid action has a left adjoint. (It's a souped up version of the groupification functor from monoids to groups.) The equivalence relation is "essentially" the equivalence relation induced by the group action via this left adjoint (by this I mean they have the same quotients, but there can be some analogues of zero divisors which will complicate things). I don't know if any of this makes sense.

view this post on Zulip Adam Topaz (Sep 22 2020 at 18:28):

And concerning @Kevin Buzzard 's comment -- this sounds similar to what Scott just did for rings :)
https://github.com/leanprover-community/mathlib/blob/master/src/algebra/ring_quot.lean

view this post on Zulip Adam Topaz (Sep 22 2020 at 18:28):

Note that we still don't have two-sided ideals, but we have quotients of rings!

view this post on Zulip Reid Barton (Sep 22 2020 at 18:32):

In sufficiently weak systems you can have quotient but not quot or inductive types that are recursive, and then I believe you won't be able to define the quotient by a monoid action (but will be able to define the quotient by a group action of course).

view this post on Zulip Patrick Massot (Sep 22 2020 at 23:08):

Johan Commelin said:

Patrick Massot I guess you have been thinking about the circle for Sphere eversion. What's the status?

Sorry I missed this question. We have functions defined on circles everywhere in this project, they are defined as periodic functions on R\mathbb R.

view this post on Zulip Yury G. Kudryashov (Sep 22 2020 at 23:57):

In dynamics/circle/rotation_number/translation_number I define a circle self-map as a map f : \R → \R such that f (x + 1) = f x + 1.

view this post on Zulip Yury G. Kudryashov (Sep 22 2020 at 23:58):

This way I can state many interesting results without using quotients.


Last updated: May 07 2021 at 22:14 UTC