FundamentalGroup — Mathlib

English

The fundamental group is the automorphism group of the basepoint in the fundamental groupoid.

Русский

Фундаментальная группа есть группа автоморфизмов базовой вершины в фундаментальном групоидe.

LaTeX

$$$$ \\operatorname{FundamentalGroup}(X,x) = \\operatorname{Aut}_{\\mathrm{FundamentalGroupoid}(X)}(x). $$$$

Lean4

/-- The fundamental group is the automorphism group (vertex group) of the basepoint
in the fundamental groupoid. -/
def FundamentalGroup (X : Type u) [TopologicalSpace X] (x : X) :=
  @Aut (FundamentalGroupoid X) _ ⟨x⟩

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