toArrow — Mathlib

English

An element of the fundamental group can be viewed as an endomorphism in the fundamental groupoid.

Русский

Элемент фундаментальной группы можно рассматривать как стрелку-эндоморфизм в фундаментальном групоидe.

LaTeX

$$$$ \\operatorname{toArrow}: \\operatorname{FundamentalGroup}(X,x) \\to \\mathrm{Hom}_{\\mathrm{FundamentalGroupoid}(X)}(x,x). $$$$

Lean4

/-- An element of the fundamental group as an arrow in the fundamental groupoid. -/
abbrev toArrow {X : TopCat} {x : X} (p : FundamentalGroup X x) : FundamentalGroupoid.mk x ⟶ FundamentalGroupoid.mk x :=
  p.hom

Похожие утверждения