How to deal with fundamental group (homotopy class)

Stream: Is there code for X?

[Ruize Chen]

Hi, I am trying to use the homotopy lifting property to prove the isomorphism between the fundamental group of S^1 and integer Z. However, I need to use the homotopy lifting on the actual path in the homotopy class (which is an element of the fundamental group). I cannot do that in lean because the definition of a fundamental group relies on the category theory. I think I cannot understand and use the Path.Homotopic.Quotient. How can I make lean 'understand' fundamental group from the basic concept like homotopy between paths?

[Aaron Liu]

To lift an element of the fundamental group, you define a lift for paths and prove that lifting two homotopic paths gives the same result

[Aaron Liu]

This lifts the lift on paths to a lift on the fundamental group

[Ruize Chen]

Yeah I know, I think that is basically what I am wondering, I tried that, but I cannot do it last night

[Aaron Liu]

Are you coming from docs#FundamentalGroup

[Ruize Chen]

yes, I am trying to understand the FundamentalGroup.toPathand FundamentalGroup.fromPath

[Aaron Liu]

It looks like docs#FundamentalGroup.toPath and docs#FundamentalGroup.fromPath both take the type argument as a bundled topological space, which is weird

[Ruize Chen]

I just don't understand the structure, honestly, I am expecting some function to do the transformation but that sounds unrealistic due to the structure of the fundamental group and classes

[Aaron Liu]

What kind of transformation do you want?

[Ruize Chen]

From the homotopic statement to the equivalence of the two elements in fundamental group

[Aaron Liu]

How are you building the elements of the fundamental group from paths?

[Ruize Chen]

from the quotient of paths

[Ruize Chen]

I think I will try more today about using quotient.

[Adam Topaz]

Do we have Van-Kampen? If so, then the proof should be relatively easy.
Edit: Sorry, this was meant for the fundamental group of the sphere topic elsewhere in this stream.

[Jz Pan]

Do we have universal covering spaces in mathlib? Maybe you can prove that R is the universal covering space of S^1.

[Ruize Chen]

Adam Topaz said:

Do we have Van-Kampen? If so, then the proof should be relatively easy.
Edit: Sorry, this was meant for the fundamental group of the sphere topic elsewhere in this stream.

I searched for the similar stuff in zulip before starting this project, I think it's in someone's todo list

[Ruize Chen]

I think there is no direct structure corresponds to universal covering space (In the Algebraic Topology part of mathlib), I tried lean search, But I think it's possible to define one. (Not sure) The next step will be pointing out the decktransformation. (I haven't found the theorem to that).

[Ruize Chen]

(There is covering map and space, I am aware of that. ) I think successfully proving the thing using one of the two methods (Homotopy lifting or deck transformation) will be very nice to have. I think we have (or about to) the HLP in the mathlib. So I am trying to understand and evaluate this method originally, I haven't understood everything yet. @Edison Xie and @David Ang and I was working on this last night, we definitely need more api to achieve that.

[Ruize Chen]

Honestly I prefer deck transformation mathematically, it looks good, but without the important theorem, It might be painful to do as well.

[Jireh Loreaux]

Instead of proving π₁(𝕋) ≃* Multiplicative ℤ, I suggest developing the more general theory in Mathlib first.

[Ruize Chen]

Yeah that's probably what's missing, I chose this as one of my assessed project (I am undergraduate). my plan is generalising the content and leaving some valuable sorry s. so that it doesn't die as an unfinished thing

[Ruize Chen]

and hopefully find out what is actually missing or needed.

[Ruize Chen]

image.png
I am trying to find out what I can do about setoid

[Aaron Liu]

Define your map on the paths, define a map on the quotient by Quotient.lift map proof, and define the map on the fundamental group by fun x => mapQuot (toPath x)

[Ruize Chen]

I want to prove that the p is a covering space, but I got this
image.png
I used to play with teh trivialization but under the assumption, it's the first time I actually create one, I am using IsCoveringMap.mk to do this

abbrev uc := AddCircle (1 : ℝ)

def zero_loop := fun (t : I) ↦ (0 : uc)

def p_cov_map := fun (k : ℝ) ↦ (k : uc)


def F := fun (k : uc) ↦  ↑(p_cov_map ⁻¹' {k})

def triv_cov := fun (k : uc) ↦ Trivialization (F k) p_cov_map

#check (Trivialization ↑(p_cov_map ⁻¹' {(0 : uc)}) p_cov_map)


lemma h_triv : ∀ (k : uc), k ∈ (triv_cov k).baseSet

I am wondering what is going on. is there anything I need to change to fix this issue?

[Edison Xie]

(deleted)

[Aaron Liu]

You are trying to take the base set of the type of trivializations

[Aaron Liu]

This does not work

[Ruize Chen]

yeah because I want to feed the lemma to .mk, to get a coveringmap statement

Aaron Liu said:

You are trying to take the base set of the type of trivializations

[Ruize Chen]

image.png

[Ruize Chen]

I might get the thing wrong but to me it seems like in the theorem, similar things are made (e x).baseSet

[Michał Mrugała]

Ruize Chen said:

image.png

it's probably better to link to the docs rather than use screenshots, like so: docs#IsCoveringMap.mk

[Edison Xie]

are you sure you want the set of all trivialization?

[Edison Xie]

@Ruize Chen

[Aaron Liu]

def triv_cov (k : uc) : Trivialization (F k) p_cov_map where
  toFun := sorry
  invFun := sorry
  source := sorry
  target := sorry
  map_source' := sorry
  map_target' := sorry
  left_inv' := sorry
  right_inv' := sorry
  open_source := sorry
  open_target := sorry
  continuousOn_toFun := sorry
  continuousOn_invFun := sorry
  baseSet := sorry
  open_baseSet := sorry
  source_eq := sorry
  target_eq := sorry
  proj_toFun := sorry

[Aaron Liu]

try this

[Aaron Liu]

If you prove you have a fiber bundle then you can also use docs#FiberBundle.trivializationAt

[Aaron Liu]

and then pull through a homeomorphism

[Aaron Liu]

nvm defining a fiber bundle needs a trivialization

[Ruize Chen]

Aaron Liu said:

def triv_cov (k : uc) : Trivialization (F k) p_cov_map where
  toFun := sorry
  invFun := sorry
  source := sorry
  target := sorry
  map_source' := sorry
  map_target' := sorry
  left_inv' := sorry
  right_inv' := sorry
  open_source := sorry
  open_target := sorry
  continuousOn_toFun := sorry
  continuousOn_invFun := sorry
  baseSet := sorry
  open_baseSet := sorry
  source_eq := sorry
  target_eq := sorry
  proj_toFun := sorry

I am wondering according to the definition of docs#Trivialization, I just need to give it F and proj (p_cov_map), should it be the user to define it from the groud?

[Ruize Chen]

Ruize Chen said:

Aaron Liu said:

def triv_cov (k : uc) : Trivialization (F k) p_cov_map where
  toFun := sorry
  invFun := sorry
  source := sorry
  target := sorry
  map_source' := sorry
  map_target' := sorry
  left_inv' := sorry
  right_inv' := sorry
  open_source := sorry
  open_target := sorry
  continuousOn_toFun := sorry
  continuousOn_invFun := sorry
  baseSet := sorry
  open_baseSet := sorry
  source_eq := sorry
  target_eq := sorry
  proj_toFun := sorry

I am wondering according to the definition of docs#Trivialization, I just need to give it F and proj (p_cov_map), should it be the user to define it from the groud?

probably I need to do this

[Aaron Liu]

Ruize Chen said:

I am wondering according to the definition of docs#Trivialization, I just need to give it F and proj (p_cov_map), should it be the user to define it from the groud?

Compare with docs#Equiv: you just need to give it α and β, but that doesn't mean you get an Equiv.

[Ruize Chen]

Yeah I just read that, I need to prove something

[Junyan Xu]

I think currently it's annoying to work with the fundamental group because it's not defeq to the homotopy class of paths from a point to itself (Path.Homotopic.Quotient), but the units in this type ("Aut" in category theory rather than "End"). This is being changed in #22771.

Aaron Liu said:

To lift an element of the fundamental group, you define a lift for paths and prove that lifting two homotopic paths gives the same result

This is done in #22771 and it's a direct consequence of IsCoveringMap.liftPath_apply_one_eq_of_homotopicRel.

Aaron Liu said:

It looks like docs#FundamentalGroup.toPath and docs#FundamentalGroup.fromPath both take the type argument as a bundled topological space, which is weird

This is being changed in #22771.

Jz Pan said:

Do we have universal covering spaces in mathlib? Maybe you can prove that R is the universal covering space of S^1.

It's shown in #7596 that R->S^1 (AddCircle) is a covering map, and we know R is contractible and therefore simply-connected, so ...
I also commented what generality we should aim for for mathlib.

[Junyan Xu]

The lifting criterion will be used to show the group of deck transformations act transitively on the fibers if the covering map is Galois (the induced map between fundamental groups has normal image). (For the universal cover this is always the case since the image is trivial; in algebra we correspondingly know that the separable closure of a field is always Galois.)

[Junyan Xu]

But in the case of R -> S^1 you start from a group action (by translations) which are the deck transformations so you don't need to construct them. If you fix a basepoint in p ⁻¹' {x}, using monodromy you get a point in p ⁻¹' {x} for each element in the fundamental group at x. Any two elements in p ⁻¹' {x} differ by an element in the group (Z in this case), so you get a map from the fundamental group to Z, and you only have to show it's an isomorphism.