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.

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

instance instInhabitedFundamentalGroup (X : Type u_1) [TopologicalSpace X] (x : X) : Inhabited (FundamentalGroup X 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

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.

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

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

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

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

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.

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

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 (Path.Homotopic.Quotient.mk p)) = fromPath (Path.Homotopic.Quotient.mk ((p.map ⋯).cast ⋯ ⋯))