Error trying to define fundamental group as a functor

Stream: mathlib4

[Miguel Marco]

I am trying to define a functor associating a pointed space to its fundamental group. In order to do so, I defined a category of pointed spaces like this:

import Mathlib.Tactic
import Mathlib.Topology.Defs.Basic
import Mathlib.CategoryTheory.ConcreteCategory.Bundled
import Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup
open CategoryTheory

class PointedSpace (S : Type ) extends TopologicalSpace S  where
  base_point : S

open PointedSpace

def PointedSpaceCat := CategoryTheory.Bundled PointedSpace


instance (A : PointedSpaceCat) : TopologicalSpace A.α := A.str.toTopologicalSpace

structure PointedContinuousMap (A B : PointedSpaceCat) extends ContinuousMap A.α B.α : (Type u) where
  isPointed : toFun A.str.base_point = B.str.base_point


instance : CategoryTheory.Category PointedSpaceCat where
  Hom :=  PointedContinuousMap
  id := by
    intro X
    exact ⟨{ toFun := id },id_eq _⟩
  comp := by
    intro X Y Z f g
    use {toFun := g.toFun ∘ f.toFun}
    simp only [← ContinuousMap.toFun_eq_coe, Function.comp_apply]
    rw  [f.isPointed,g.isPointed]

but then, when I try to define the map between fundamental groups induced by a continuous map, I try this:

example (X Y : PointedSpaceCat)  (f : PointedContinuousMap X Y) (g : FundamentalGroup X.α X.str.base_point) : FundamentalGroup Y.α  Y.str.base_point := by
  let p := g.toPath

and Lean complains with an error message:

application type mismatch
  FundamentalGroup.toPath g
argument
  g
has type
  FundamentalGroup (↑X) base_point : Type
but is expected to have type
  FundamentalGroup ↑?m.20728 ?m.20729 : Type

I really don't see where the problem is.

[Filippo A. E. Nuccio]

It seems that it is unable to complete type inference, because this works

example (X Y : PointedSpaceCat)  (f : PointedContinuousMap X Y) (g : FundamentalGroup X.α X.str.base_point) : FundamentalGroup Y.α  Y.str.base_point := by
  let p := @FundamentalGroup.toPath (@TopCat.of _ X.str.toTopologicalSpace) _ g

[Filippo A. E. Nuccio]

In the above, the base_point is picked up automatically, so it seems that the true problem is to figure out the space.

[Miguel Marco]

I see, so FundamentalGroup.toPath expects a TopCat lifted to a TopologicalSpace, and we have to wrap the topological space again to provde it. Shouldn't the extend clause take care of that?

[Filippo A. E. Nuccio]

Actually if you change your (g : FundamentalGroup X.α X.str.base_point) to (g : FundamentalGroup (TopCat.of X.α) X.str.base_point) your code works.

[Filippo A. E. Nuccio]

I think you are being a bit too greedy, because Lean starts of with X, then it creates X.α which is a PointedSpace structure on it and you are automatically coercing it to a type that you would like it to automatically re-bundle into an object of TopCat

[Miguel Marco]

Which would be the right way to do it?

[Filippo A. E. Nuccio]

If you are calling `@FundamentalGroup.toPath (@TopCat.of _ X.str.toTopologicalSpace) _ g it is happy with a pair of a type+topological space on it (that can automatically infer by the extend) but here you are asking it to re-bundled the pair (the type, the top structure) automatically and this it cannot do.

[Filippo A. E. Nuccio]

Miguel Marco said:

Which would be the right way to do it?

I think you might try to define a coercion from PointedSpaceCat to TopCat.

[Miguel Marco]

I see, does that sound better than trying to "extend" the bundled structure?

[Filippo A. E. Nuccio]

That being said, have you already checked that this functor is not already in the library? Are you trying it as an excercise or really to contribute? (Note: I am not saying it is there, I am really asking...)

[Filippo A. E. Nuccio]

Miguel Marco said:

I see, does that sound better than trying to "extend" the bundled structure?

You could also extend TopCat, true. I think both are viable options, but it mainly depends if you want to put more focus on "pointed topological spaces" and then create their category; or to start from the category of topological spaces and "sometimes" to stare at its objects in the eyes.

[Miguel Marco]

I cheked and didn't find it (the fundamental groupoid one exists, but not the fundamental group). For starters, I am just playing around. If i manage to do something of reasonable quality, i might consider contributing it, but that is not what I have in mind now.

[Filippo A. E. Nuccio]

I see, then I would certainly suggest that you try to play with both options and decide which one is the best according at how difficult becomes to prove "trivial" statements, like: the composition of functions incudes homs of fundamental groups (or just maps, to start with), the identity map induces the identity, etc... Most probably, in one of the two settings things will be easier than in the other, and you'll have your answer.

[Filippo A. E. Nuccio]

Consider that you could also do everything by hand first (with no category theory), just defining the "functor" on obj+morphisms (without calling it "a functor"); and invoking the category library at a second stage. Again, this is not what I recommend, just an option whose value can normally be appreciated at a later stage, once you are working with these notions.