Fundamental group of a space

Given a topological space X and a basepoint x, the fundamental group is the automorphism group of x i.e. the group with elements being loops based at x (quotiented by homotopy equivalence).

def FundamentalGroup (X : Type u) [TopologicalSpace X] (x : X) : Type u

The fundamental group is the automorphism group (vertex group) of the basepoint in the fundamental groupoid.

instance instGroupFundamentalGroup (X : Type u) [TopologicalSpace X] (x : X) : Group (FundamentalGroup X x)

instance instInhabitedFundamentalGroup (X : Type u) [TopologicalSpace X] (x : X) : Inhabited (FundamentalGroup X x)

def FundamentalGroup.fundamentalGroupMulEquivOfPath {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} (p : Path x₀ x₁) : FundamentalGroup X x₀ ≃* FundamentalGroup X x₁

Get an isomorphism between the fundamental groups at two points given a path

def FundamentalGroup.fundamentalGroupMulEquivOfPathConnected {X : Type u} [TopologicalSpace X] (x₀ x₁ : X) [PathConnectedSpace X] : FundamentalGroup X x₀ ≃* FundamentalGroup X x₁

The fundamental group of a path connected space is independent of the choice of basepoint.

@[reducible, inline]

abbrev FundamentalGroup.toArrow {X : TopCat} {x : ↑X} (p : FundamentalGroup (↑X) x) : { as := x } ⟶ { as := x }

An element of the fundamental group as an arrow in the fundamental groupoid.

@[reducible, inline]

abbrev FundamentalGroup.toPath {X : TopCat} {x : ↑X} (p : FundamentalGroup (↑X) x) : Path.Homotopic.Quotient x x

An element of the fundamental group as a quotient of homotopic paths.

@[reducible, inline]

abbrev FundamentalGroup.fromArrow {X : TopCat} {x : ↑X} (p : { as := x } ⟶ { as := x }) : FundamentalGroup (↑X) x

An element of the fundamental group, constructed from an arrow in the fundamental groupoid.

@[reducible, inline]

abbrev FundamentalGroup.fromPath {X : TopCat} {x : ↑X} (p : Path.Homotopic.Quotient x x) : FundamentalGroup (↑X) x

An element of the fundamental group, constructed from a quotient of homotopic paths.