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.

Equations

• FundamentalGroup X x = CategoryTheory.Aut { as := x }

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

Equations

• instGroupFundamentalGroup X x = id inferInstance

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

Equations

• instInhabitedFundamentalGroup X x = id inferInstance

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

Equations

• FundamentalGroup.fundamentalGroupMulEquivOfPath p = CategoryTheory.Aut.autMulEquivOfIso (CategoryTheory.asIso ⟦p⟧)

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.

Equations

• FundamentalGroup.fundamentalGroupMulEquivOfPathConnected x₀ x₁ = FundamentalGroup.fundamentalGroupMulEquivOfPath (PathConnectedSpace.somePath x₀ x₁)

@[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.

Equations

• p.toArrow = p.hom

@[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.

Equations

• p.toPath = p.toArrow

@[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.

Equations

• FundamentalGroup.fromArrow p = { hom := p, inv := CategoryTheory.Groupoid.inv p, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[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.

Equations

• FundamentalGroup.fromPath p = FundamentalGroup.fromArrow p