Create elements of fundamental group(oid) from paths

Stream: Is there code for X?

[Miguel Marco]

As an exercise, I have been trying to prove Seifert-VanKampen theorem, and got stuck at a point where I need to create elements of the fundamental group from closed paths. I got lost in the abstraction layers behind the FundamentalGroup construction (If i get it correctly, it formed by invertible morphisms in a topological category). But this definition is meant to encapsulate equivalence classes of closed paths.

So, given X : Type [TopologicalSpace X], x : Xand P : Path x x, is there a direct way to get a term of FundamentalGroup x?

[Kevin Buzzard]

Can you go all the way with your question and write a #mwe ?

[Miguel Marco]

I think this reflects the point where I am stuck:

import Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup

variable (X : Type) [TopologicalSpace X] (x : X)

def path_to_fundamental_group : Path x x → FundamentalGroup X x := by
  apply?

I just get apply? didn't find any relevant lemmas

[Adam Topaz]

import Mathlib

variable (X : Type*) [TopologicalSpace X]

noncomputable
example {x : X} (γ : Path x x) : FundamentalGroup X x :=
  .fromPath (X := TopCat.of X) <| .mk _ γ

[Miguel Marco]

Thanks... it is a bit confusing for me. What does the (X := TopCat.of X) part do? it changes Xto be a topological category on the fly?

[Adam Topaz]

docs#FundamentalGroup.fromPath expects a term of docs#TopCat and I'm just telling lean to use TopCat.of X explicitly.

[Miguel Marco]

So it would work also without the X := part?

[Adam Topaz]

no

[Adam Topaz]

if you dont want the X := you could do this:

import Mathlib

noncomputable
example (X : TopCat) {x : X} (γ : Path x x) : FundamentalGroup X x :=
  .fromPath <| .mk _ γ

[Miguel Marco]

I am more confused now. Never saw an assigment used as argument before.

So, strictly speaking, the type of the function I want should be Path x x → FundamentalGroup (TopCat.of X) x right?

[Adam Topaz]

yes, this works as well:

import Mathlib

variable (X : Type*) [TopologicalSpace X]

noncomputable
example {x : X} (γ : Path x x) : FundamentalGroup (TopCat.of X) x :=
  .fromPath <| .mk _ γ

[Adam Topaz]

the (X := ...) isn't really an assignment. It's syntax to explicitly specify one of the named variables (X in this case).

[Adam Topaz]

More precisely, this := means something different than the := in, say, def f := 0.

[Miguel Marco]

Oh, I see. So the elaborator understands that FundamentalGroup X x means actually FundamentalGroup (TopCat.of X) x?

[Filippo A. E. Nuccio]

Some part of the library expects "true" topological spaces while some part of it expects objects in the category of topological spaces. Hopefully there is a nice way back-and-forth. Explicitly, you can do

#check FundamentalGroup -- FundamentalGroup.{u} (X : Type u) [TopologicalSpace X] (x : X) : Type u

to see that FundamentalGroup expects a topological space (and a point in it), while

#check FundamentalGroup.fromPath -- FundamentalGroup.fromPath.{u_1} {X : TopCat} {x : ↑X} (p : Homotopic.Quotient x x) : FundamentalGroup (↑X) x

tells you that FundamentalGroup.fromPath expects an object in the category of topological spaces. Given a (X : Type*) [TopologicalSpace X] you can construct an object in the latter by doing TopCat.of X. But the library knows that given an object in this category, there is a coercion to Types creating a type with a topology, i.e a toplogical space:

variable (X : Type*) [TopologicalSpace X]

#check (↑(TopCat.of X) : Type _) -- ↑(TopCat.of X) : Type u_1

Moreover, lean is clever enough to understand that this "new" topological space is the old one, and in particular their fundamental groups are equal:

variable (x : X)

example : FundamentalGroup X x = FundamentalGroup (TopCat.of X) x := rfl

Back to your example, you can define your function as follows (it is a bit verbose, but I hope it helps understanding what is going on):

noncomputable
def path_to_fundamental_group : Path x x → FundamentalGroup X x := by
  intro p
  let P : Path.Homotopic.Quotient x x := ⟦p⟧
  exact @FundamentalGroup.fromPath (TopCat.of X) x P

[Filippo A. E. Nuccio]

What Adam was doing is the very same thing, I have just unravelled the definitions and used tactic mode rather than term mode.

[Riccardo Brasca]

Also, do we have some documentation about the notation .fromPath? I know it works, but TBH I don't know exactly what Lean is doing here (is it just looking for all possible name before the dot and guessing the right one?)

[Damiano Testa]

I think that it uses Type-information to fill in: it knows to expect a FundamentalGroup and tries that. I do not think that it tries something else.

In particular, if the type information is missing, that "anonymous dot-notation" would not work. At least, I think so!

[Yaël Dillies]

Does it not unfold any definitions? Dot notation does that

[Riccardo Brasca]

Ah yes,

import Mathlib

variable (X : Type*) [TopologicalSpace X]

noncomputable
def foo.bar {x : X} (γ : Path x x) : FundamentalGroup X x :=
  .fromPath (X := .of X) <| .mk _ γ

example {x : X} (γ : Path x x) : FundamentalGroup X x :=
  .bar X γ --invalid dotted identifier notation, unknown identifier `CategoryTheory.Aut.bar` from expected type
  --FundamentalGroup X x

[Damiano Testa]

Yaël Dillies said:

Does it not unfold any definitions? Dot notation does that

I am not sure, but I think that "anonymous dot" is stricter than "usual dot".