## Stream: Is there code for X?

### Topic: S1 and other topological spaces

#### Pedro Minicz (Sep 22 2020 at 16:30):

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

#### 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?

#### Heather Macbeth (Sep 22 2020 at 16:55):

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

#### Heather Macbeth (Sep 22 2020 at 16:56):

But it exists as a topological space quite easily.

#### Heather Macbeth (Sep 22 2020 at 16:57):

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

#### 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).

#### 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

#### Kevin Buzzard (Sep 22 2020 at 17:04):

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

#### Pedro Minicz (Sep 22 2020 at 17:04):

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

#### Pedro Minicz (Sep 22 2020 at 17:05):

I was wondering if something was defined on mathlib

#### 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

#### 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.

#### Heather Macbeth (Sep 22 2020 at 17:05):

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

#### 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

#### 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


#### 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.

#### 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

#### 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.

#### 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)?

#### 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.

#### Johan Commelin (Sep 22 2020 at 17:15):

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

#### Kevin Buzzard (Sep 22 2020 at 17:16):

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

#### 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:

#### 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

#### 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.

#### 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)


#### 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!)

#### Adam Topaz (Sep 22 2020 at 18:00):

quot never gets the respect it deserves...

#### 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.

#### 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)

#### 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.

#### 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

#### Adam Topaz (Sep 22 2020 at 18:28):

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

#### 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).

#### 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 $\mathbb R$.

#### 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.

#### 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