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_1) [TopologicalSpace X] (x : X) : Type u_1

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

Equations

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

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

Equations

• instGroupFundamentalGroup X x = inferInstanceAs (Group (CategoryTheory.End { as := x }))

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

Equations

• instInhabitedFundamentalGroup X x = inferInstanceAs (Inhabited (CategoryTheory.End { as := x }))

def FundamentalGroup.fundamentalGroupMulEquivOfPath {X : Type u_1} [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.Groupoid.isoEquivHom { as := x₀ } { as := x₁ }).symm ⟦p⟧).conj

def FundamentalGroup.fundamentalGroupMulEquivOfPathConnected {X : Type u_1} [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 : Type u_1} [TopologicalSpace X] {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

@[reducible, inline]

abbrev FundamentalGroup.toPath {X : Type u_1} [TopologicalSpace X] {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 : Type u_1} [TopologicalSpace X] {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 = p

@[reducible, inline]

abbrev FundamentalGroup.fromPath {X : Type u_1} [TopologicalSpace X] {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

def FundamentalGroup.map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (x : X) : FundamentalGroup X x →* FundamentalGroup Y (f x)

The homomorphism between fundamental groups induced by a continuous map.

Equations

• FundamentalGroup.map f x = CategoryTheory.Functor.mapEnd { as := x } (FundamentalGroupoid.map f)

@[simp]

theorem FundamentalGroup.map_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (x : X) (a✝ : { as := x } ⟶ { as := x }) : (map f x) a✝ = Path.Homotopic.Quotient.mapFn a✝ f

def FundamentalGroup.mapOfEq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) {x : X} {y : Y} (h : f x = y) : FundamentalGroup X x →* FundamentalGroup Y y

The homomorphism from π₁(X, x) to π₁(Y, y) induced by a continuous map f with f x = y.

Equations

• FundamentalGroup.mapOfEq f h = (CategoryTheory.eqToIso ⋯).conj.toMonoidHom.comp (FundamentalGroup.map f x)

theorem FundamentalGroup.mapOfEq_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) {x : X} {y : Y} (h : f x = y) (p : Path x x) : (mapOfEq f h) (fromPath ⟦p⟧) = fromPath ⟦(p.map ⋯).cast ⋯ ⋯⟧