fromArrow — Mathlib

English

An arrow in the fundamental groupoid at x yields an element of the fundamental group at x.

Русский

Стрела в группе группoid в точке x задаёт элемент фундаментальной группы в x.

LaTeX

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

Lean4

/-- An element of the fundamental group, constructed from an arrow in the fundamental groupoid. -/
abbrev fromArrow {X : TopCat} {x : X} (p : FundamentalGroupoid.mk x ⟶ FundamentalGroupoid.mk x) : FundamentalGroup X x
    where
  hom := p
  inv := CategoryTheory.Groupoid.inv p

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