FundamentalGroupoidFunctor.proj_map

theorem FundamentalGroupoidFunctor.proj_map : ∀ {I : Type u} (X : I → TopCat) (i : I) (x₀ x₁ : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of ((i : I) → ↑(X i))))) (p : x₀ ⟶ x₁), (FundamentalGroupoidFunctor.proj X i).map p = Path.Homotopic.proj i p

The theorem `FundamentalGroupoidFunctor.proj_map` states that for any index set `I`, any function `X` from `I` to the category of topological spaces, and any index `i` in `I`, as well as for any two objects (`x₀` and `x₁`) in the fundamental groupoid of the topological space represented by the function `X` and any morphism `p` from `x₀` to `x₁` in this groupoid, the map applied to `p` via the projection functor `FundamentalGroupoidFunctor.proj` for `X` and `i` is the same as applying the projection `Path.Homotopic.proj` with index `i` to `p`. In essence, this theorem shows that the projection map in the context of fundamental groupoids coincides with the homotopy projection operation when seen as a functor.

More concisely: The projection map in the fundamental groupoid of a functor from an index set to topological spaces, when applied to a morphism, is equivalent to applying the homotopy projection operation with the same index to that morphism.