Theorems · Definition · algebraic topology

FundamentalGroupoid.map

{X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → C(X, Y) → CategoryTheory.Functor (FundamentalGroupoid X) (FundamentalGroupoid Y)

The functor on fundamental groupoid induced by a continuous map.

Defined in

Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Cited by

6 results in Mathlib

Foundations

Depth 136 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpace