S1 and other topological spaces

Stream: Is there code for X?

[Pedro Minicz]

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

[Johan Commelin]

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

[Heather Macbeth]

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

[Heather Macbeth]

But it exists as a topological space quite easily.

[Heather Macbeth]

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

[Heather Macbeth]

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]

Heather Macbeth said:

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

The topological space

[Kevin Buzzard]

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

[Pedro Minicz]

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

[Pedro Minicz]

I was wondering if something was defined on mathlib

[Heather Macbeth]

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]

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]

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

[Heather Macbeth]

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

[Pedro Minicz]

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]

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]

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]

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

[Heather Macbeth]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Heather Macbeth]

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]

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

[Adam Topaz]

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]

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

[Kevin Buzzard]

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]

quot never gets the respect it deserves...

[Kevin Buzzard]

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]

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]

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]

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]

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

[Reid Barton]

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]

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]

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]

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