Fundamental Group of R^n or D^n or S^n

Stream: Is there code for X?

[Gareth Ma]

How should I write down $\pi_1(\mathbb{R}^n, x) \cong 0$? I got the following but the first two examples don't work:

import Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup
import Mathlib.Topology.Homotopy.HomotopyGroup
import Mathlib.Analysis.Complex.Circle

variable (𝕜 : Type*) [NormedDivisionRing 𝕜]
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]

example (x) : FundamentalGroup (ball 0 1) x ≃* 0 := by
  sorry

example (x) : FundamentalGroup (ball (0 : E) 1) x ≃* 0 := by
  sorry

example (x) : FundamentalGroup circle x ≃* ℤ := by
  sorry

(Maybe my actual question is how to write the trivial group)

[Yaël Dillies]

Subsingleton (FundamentalGroup (ball 0 1) x)? (also please can we disable Zulip automatically putting quote around copy-pasted code by default?)

[Gareth Ma]

What quote?
Subsingleton (FundamentalGroup (ball 0 1) x)
works fine

[Yaël Dillies]

If I copy as in the image
image.png
and I paste inside the chat box, it gives

`FundamentalGroup (ball 0 1) x`

[Gareth Ma]

Oh same for me. Weird behaviour

[Damiano Testa]

Btw, I think that Subsingleton is better, but Unit works for the trivial group.

[Gareth Ma]

Thanks, I think that might become useful but I'll stick with Subsingleton for now

[Gareth Ma]

Actually then shouldn't it be Subsingleton and Nonempty? Though one's implified since FundamentalGroup is a Group

[Damiano Testa]

Subsingleton is very flexible and Nonempty you get for free.

[Mitchell Lee]

Another way is SimplyConnectedSpace (ball 0 1)

[Gareth Ma]

Oh, it's precisely the definition Damiano gave :)

/-- A simply connected space is one whose fundamental groupoid is equivalent to `Discrete Unit` -/
@[mk_iff simply_connected_def]
class SimplyConnectedSpace (X : Type*) [TopologicalSpace X] : Prop where
  equiv_unit : Nonempty (FundamentalGroupoid X ≌ Discrete Unit)

[Mitchell Lee]

(As a small correction to what I said, SimplyConnectedSpace (ball 0 1) is stronger than the statement that the fundamental group of ball 0 1 at any base point is trivial, because it also includes the fact that ball 0 1 is path connected.)

[Gareth Ma]

Also are any of these results formalised in Mathlib? For $\mathbb{R}^n, \mathcal{D}^n, \mathbb{S}^n$

[Richard Osborn]

Yaël Dillies said:

If I copy as in the image
image.png
and I paste inside the chat box, it gives

`FundamentalGroup (ball 0 1) x`

If you right click you can "paste as plain-text" in Windows or "paste and match style" in MacOS. There are keyboard shortcuts as well, but I don't remember them off hand.

[Gareth Ma]

image.png

[Antoine Chambert-Loir]

Damiano Testa said:

Btw, I think that Subsingleton is better, but Unit works for the trivial group.

Why is Subsingleton the contrary of Nontrivial?

[Damiano Testa]

I was not very clear. What I meant is that working with Subsingleton (...) has a chance of harnessing typeclass inference, while working with FundamentalGroup (ball 0 1) x ≃* 0 is further removed from it. So my comment was merely stating that using Subsingleton may provide a smoother formalisation experience.

However, since the original question could have been interpreted as "what is the trivial group", I thought that answering that could be useful.

[Antoine Chambert-Loir]

I think you were clear. What is not clear to me is the choice of names — there is a useful docs#Nontrivial class that works well to characterize nontrivial algebraic structures (which (most of the time) are pointed), while the opposite class is called docs#Subsingleton and not Trivial.

[Damiano Testa]

Oh, I see! I kind of like moving away from from the word Trivial, which to me seems over-used in maths.

[Antoine Chambert-Loir]

Certainly. But Subsingleton had a set theoretic feeling that blocked me at once when I saw you using this Typeclass to characterize a trivial group. (Until I looked back at the definitions and observed that is exactly opposite to Nontrivial.)

[Damiano Testa]

Right and I find that the extra possibility of allowing empty is great! My favourite mental formalisation of separated and of proper involve Subsingleton and Subsingleton + Nonempty!

[Antoine Chambert-Loir]

docs#Subsingleton is a great TypeClass. The only thing which is not great is its name, since a subsingleton is not always a subset of a singleton.

[Gareth Ma]

(Note that it’s a type theory terminology not a random Mathlib one)

[Gareth Ma]

Antoine Chambert-Loir said:

docs#Subsingleton is a great TypeClass. The only thing which is not great is its name, since a subsingleton is not always a subset of a singleton.

I'm confused, isn't subsingleton defined to be a subset of a singleton set (even constructively)?

[Gareth Ma]

nlab seems to agree

[Joseph Cooper]

Gareth Ma said:

Also are any of these results formalised in Mathlib? For $\mathbb{R}^n, \mathcal{D}^n, \mathbb{S}^n$

I was also wondering whether these results are in Mathlib. In addition, is there such a library of computed fundamental groups for specific spaces in Mathlib?

[Gareth Ma]

FYI I think the answer for S^1 is no. There is a TODO that asks to define a CoveringMap structure for expMapCircle, and it’s on my (eventual) TODO list too

[Joseph Cooper]

Gareth Ma said:

FYI I think the answer for S^1 is no. There is a TODO that asks to define a CoveringMap structure for expMapCircle, and it’s on my (eventual) TODO list too

I wanted the result for S^1 in particular for another result. Being new to Lean, where can I find such TODOs?

[Gareth Ma]

Use a search tool (eg grep or VSCode project search) and just look for TODO all caps

[Gareth Ma]

Or TODO.+CoveringMap iirc

[Gareth Ma]

I can look later I’m a bit busy

[Gareth Ma]

Personally I use ripgrep so the search command looks like

$ rg -S todo.+covering
Analysis/SpecialFunctions/Complex/Circle.lean
234:-- todo: upgrade this to `IsCoveringMap expMapCircle`.

I think in general there is a lot of improvements possible surrounding IsCoveringMap, but I am not good enough at alg topo to help there :(

[Junyan Xu]

It's asked here but I haven't got around to carry out the plan. It should be easy to show the translation map on the complex plane is properly discontinuous though, then you can use the results of the PR.

[Gareth Ma]

Oh thanks for the reference, I will have a look when I get back :)

[Gareth Ma]

Oh thanks for the reference, I will have a look when I get back :)