fundamentalGroupoidFunctor — Mathlib

Lean4
/-- The functor sending a topological space `X` to its fundamental groupoid. -/
def fundamentalGroupoidFunctor : TopCat ⥤ CategoryTheory.Grpd
    where
  obj X := { α := FundamentalGroupoid X }
  map
    f :=
    { obj := fun x => ⟨f x.as⟩
      map := fun {X Y} p => by exact Path.Homotopic.Quotient.mapFn p f.hom
      map_id := fun _ => rfl
      map_comp := fun {x y z} p q => by
        refine Quotient.inductionOn₂ p q fun a b => ?_
        simp only [comp_eq, ← Path.Homotopic.map_lift, ← Path.Homotopic.comp_lift, Path.map_trans] }
  map_id
    X := by
    simp only
    congr
    ext x y p
    refine Quotient.inductionOn p fun q => ?_
    rw [← Path.Homotopic.map_lift]
    conv_rhs => rw [← q.map_id]
    rfl
  map_comp f
    g := by
    simp only
    congr
    ext x y p
    refine Quotient.inductionOn p fun q => ?_
    simp only
    rfl
Похожие утверждения