The action of the fundamental group on the higher homotopy groups

Transporting a generalized loop along a path γ from x to y gives an isomorphism π_n(X, x) ≃* π_n(X, y) depending only on the homotopy class of γ (TauCeti.homotopyGroupMulEquivOfPath). Taking y = x turns that isomorphism into extra structure carried by a single homotopy group: the fundamental group at x acts on the type π_n(X, x), and in positive dimensions — where that type carries a group structure — it acts by group automorphisms. This file builds that action and identifies its orbits.

The action is the higher-dimensional analogue of the conjugation action of π₁(X, x) on itself, and in dimensions at least two, where π_n is abelian, it is what the phrase "π_n is a π₁-module" abbreviates. Its orbits have a purely topological meaning, recorded here in TauCeti.homotopyGroup_mem_orbit_iff_exists_homotopyAlong: two generalized loops based at x lie in the same orbit exactly when they are freely homotopic, that is, when some homotopy connects them through generalized loops whose base points sweep out a loop at x. So the quotient of π_n(X, x) by the action is, in positive dimensions, the set of free homotopy classes of maps Sⁿ → X landing in the path component of x. In dimension zero, it instead records the classes for which the distinguished point of S⁰ remains in the path component of x. The action is trivial precisely when the corresponding based and free homotopy classes agree.

Conventions

Transport composes covariantly — transporting along γ and then along δ transports along γ.trans δ — while multiplication in FundamentalGroup X x is FundamentalGroup.mul_def : p * q = q.trans p. The two conventions match, so transport is a left action and no ᵐᵒᵖ is needed; this is the same bookkeeping that makes Mathlib's monodromy action IsCoveringMap.fundamentalGroupMulAction a left action.

Main declarations

• TauCeti.homotopyGroupTransportQuotient: transport of homotopy classes along a homotopy class of paths, with TauCeti.homotopyGroupTransportQuotient_refl and TauCeti.homotopyGroupTransportQuotient_trans.
• TauCeti.homotopyGroupMulAction: the fundamental group acts on every homotopy group at the same base point, with TauCeti.fundamentalGroup_smul_mk computing the action of the class of a loop.
• TauCeti.homotopyGroupMulDistribMulAction and TauCeti.fundamentalGroupMulAut: in positive dimensions the action is by group automorphisms.
• TauCeti.pi1MulEquivFundamentalGroup_smul and TauCeti.congr_fundamentalGroupMulAut_piOne: under the canonical identification π₁(X, x) ≃* FundamentalGroup X x, the action in dimension one is the conjugation representation.
• TauCeti.map_fundamentalGroup_smul: a based continuous map is equivariant for the actions on source and target, along the homomorphism it induces on fundamental groups.
• TauCeti.homotopyGroup_mem_orbit_iff and TauCeti.homotopyGroup_mem_orbit_iff_exists_homotopyAlong: the orbits of the action are the free homotopy classes into the path component of x in positive dimensions (with the distinguished point restricted to the component of x in dimension zero), the latter through TauCeti.GenLoop.exists_homotopyAlong_iff_exists_homotopic_transport, which reads free homotopy as transport up to based homotopy.
• TauCeti.fundamentalGroup_smul_eq_self: on a simply connected space the action is trivial.
• TauCeti.one_mem_orbit_of_forall_mem_of_nullhomotopic: a generalized loop staying in a set whose inclusion is null-homotopic is freely homotopic to the constant loop.

References

See Hatcher, Algebraic Topology, Section 4.1, where the action is introduced immediately after base-point change and the description of its orbits is the definition of an n-simple space.

Transport along a homotopy class of paths

noncomputable def TauCeti.homotopyGroupTransportQuotient {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x x' : X} (γ : Path.Homotopic.Quotient x x') : HomotopyGroup N X x → HomotopyGroup N X x'

Transport of homotopy classes along a homotopy class of paths. This is TauCeti.homotopyGroupTransport descended to Path.Homotopic.Quotient, which is legitimate because homotopic paths transport alike.

@[simp]

theorem TauCeti.homotopyGroupTransportQuotient_mk {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x x' : X} (γ : Path x x') : homotopyGroupTransportQuotient (Path.Homotopic.Quotient.mk γ) = homotopyGroupTransport γ

Transport along the class of a path is transport along the path.

@[simp]

theorem TauCeti.homotopyGroupTransportQuotient_refl {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x : X} : homotopyGroupTransportQuotient (Path.Homotopic.Quotient.refl x) = id

Transport along the class of the constant path is the identity.

@[simp]

theorem TauCeti.homotopyGroupTransportQuotient_trans {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x x' x'' : X} (γ : Path.Homotopic.Quotient x x') (δ : Path.Homotopic.Quotient x' x'') : homotopyGroupTransportQuotient (γ.trans δ) = homotopyGroupTransportQuotient δ ∘ homotopyGroupTransportQuotient γ

Transport along a composite of classes of paths is the composite of the two transports.

The action of the fundamental group

@[instance_reducible]

noncomputable instance TauCeti.homotopyGroupSMul {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x : X} : SMul (FundamentalGroup X x) (HomotopyGroup N X x)

The fundamental group at x acts on a homotopy group based at x by transport around loops; TauCeti.homotopyGroupMulAction shows that this is a group action.

theorem TauCeti.fundamentalGroup_smul_def {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x : X} (γ : FundamentalGroup X x) (a : HomotopyGroup N X x) : γ • a = homotopyGroupTransportQuotient γ.toPath a

The action of the fundamental group is transport along the class of loops.

@[instance_reducible]

noncomputable instance TauCeti.homotopyGroupMulAction {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x : X} : MulAction (FundamentalGroup X x) (HomotopyGroup N X x)

The fundamental group at x acts on every homotopy group based at x, an element of π₁(X, x) acting by transport around the loop it represents.

The action is a left action: transport composes covariantly and FundamentalGroup.mul_def reverses the order of concatenation, so the two reversals cancel.

theorem TauCeti.fundamentalGroup_smul_eq_transport {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x : X} {γ : FundamentalGroup X x} {p : Path x x} (h : γ.toPath = Path.Homotopic.Quotient.mk p) (a : HomotopyGroup N X x) : γ • a = homotopyGroupTransport p a

An element of π₁(X, x) represented by a loop p acts by transport along p.

@[simp]

theorem TauCeti.fundamentalGroup_smul_mk {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x : X} (p : Path x x) (a : HomotopyGroup N X x) : FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk p) • a = homotopyGroupTransport p a

The class of a loop p acts by transport along p.

theorem TauCeti.fundamentalGroup_smul_eq_homotopyGroupMulEquivOfPath {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x : X} [Nonempty N] [DecidableEq N] (p : Path x x) (a : HomotopyGroup N X x) : FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk p) • a = (homotopyGroupMulEquivOfPath p) a

Acting by an element of π₁(X, x) is base-point change along a representing loop.

@[instance_reducible]

noncomputable instance TauCeti.homotopyGroupMulDistribMulAction {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x : X} [Nonempty N] [DecidableEq N] : MulDistribMulAction (FundamentalGroup X x) (HomotopyGroup N X x)

In positive dimensions the fundamental group acts by group automorphisms.

noncomputable def TauCeti.fundamentalGroupMulAut (N : Type u_1) [Fintype N] {X : Type u_2} [TopologicalSpace X] [Nonempty N] [DecidableEq N] (x : X) : FundamentalGroup X x →* MulAut (HomotopyGroup N X x)

The action of the fundamental group on a positive-dimensional homotopy group, as a homomorphism into the automorphism group. In dimensions at least two, where π_n is abelian, this is the π₁-module structure on π_n; in dimension one it is an action of π₁(X, x) on itself by group automorphisms.

@[simp]

theorem TauCeti.fundamentalGroupMulAut_apply {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x : X} [Nonempty N] [DecidableEq N] (γ : FundamentalGroup X x) (a : HomotopyGroup N X x) : ((fundamentalGroupMulAut N x) γ) a = γ • a

The automorphism attached to an element of the fundamental group acts by that element.

The action in dimension one

@[simp]

theorem TauCeti.pi1MulEquivFundamentalGroup_smul {X : Type u_2} [TopologicalSpace X] {x : X} {γ : FundamentalGroup X x} {a : HomotopyGroup.Pi 1 X x} : HomotopyGroup.pi1MulEquivFundamentalGroup (γ • a) = (MulAut.conj γ) (HomotopyGroup.pi1MulEquivFundamentalGroup a)

Under the canonical identification of the first homotopy group with the fundamental group, the fundamental-group action is conjugation.

The order in MulAut.conj γ g = γ * g * γ⁻¹ agrees with transport: multiplication in FundamentalGroup reverses path concatenation, so this product is represented by first following γ⁻¹, then a representative of g, and finally γ.

theorem TauCeti.congr_fundamentalGroupMulAut_piOne {X : Type u_2} [TopologicalSpace X] (x : X) : (MulAut.congr HomotopyGroup.pi1MulEquivFundamentalGroup).toMonoidHom.comp (fundamentalGroupMulAut (Fin 1) x) = MulAut.conj

Conjugating the positive-dimensional action along HomotopyGroup.pi1MulEquivFundamentalGroup gives the usual conjugation representation of the fundamental group on itself.

Naturality

@[simp]

theorem TauCeti.map_homotopyGroupTransportQuotient {N : Type u_1} [Fintype N] {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x x' : X} (F : C(X, Y)) (γ : Path.Homotopic.Quotient x x') (a : HomotopyGroup N X x) : HomotopyGroup.map F ⋯ (homotopyGroupTransportQuotient γ a) = homotopyGroupTransportQuotient (γ.map F) (HomotopyGroup.map F ⋯ a)

Postcomposition with a continuous map commutes with transport of homotopy classes, along the image class of paths.

@[simp]

theorem TauCeti.map_fundamentalGroup_smul {N : Type u_1} [Fintype N] {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} (F : C(X, Y)) (γ : FundamentalGroup X x) (a : HomotopyGroup N X x) : HomotopyGroup.map F ⋯ (γ • a) = (FundamentalGroup.map F x) γ • HomotopyGroup.map F ⋯ a

A based continuous map is equivariant for the actions of the fundamental groups on source and target, along the homomorphism it induces on fundamental groups.

The orbits of the action

theorem TauCeti.homotopyGroup_mem_orbit_iff {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x : X} (a b : HomotopyGroup N X x) : b ∈ MulAction.orbit (FundamentalGroup X x) a ↔ ∃ (p : Path x x), homotopyGroupTransport p a = b

Membership in an orbit of the action is transport: a class b lies in the orbit of a exactly when some loop at x transports a to b.

theorem TauCeti.GenLoop.exists_homotopyAlong_iff_exists_homotopic_transport {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x : X} (f g : ↑(GenLoop N X x)) : (∃ (γ : Path x x), Nonempty (HomotopyAlong γ f g)) ↔ ∃ (p : Path x x), GenLoop.Homotopic (transport p f) g

Free homotopy is transport up to based homotopy. A homotopy connecting two generalized loops based at x through generalized loops, its base point sweeping out a loop, exists exactly when one of them is homotopic, relative to the cube boundary, to the transport of the other along a loop.

theorem TauCeti.homotopyGroup_mem_orbit_iff_exists_homotopyAlong {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x : X} {a b : HomotopyGroup N X x} {f g : ↑(GenLoop N X x)} (ha : a = ⟦f⟧) (hb : b = ⟦g⟧) : b ∈ MulAction.orbit (FundamentalGroup X x) a ↔ ∃ (γ : Path x x), Nonempty (GenLoop.HomotopyAlong γ f g)

In positive dimensions, the orbits of the action of π₁(X, x) on π_n(X, x) are the free homotopy classes. Classes of two generalized loops based at x lie in the same orbit exactly when some homotopy connects the two loops through generalized loops, the base point sweeping out a loop at x. Thus in positive dimensions the quotient of π_n(X, x) by the action is the set of free homotopy classes of maps Sⁿ → X landing in the path component of x. In dimension zero, it instead classifies the free homotopy classes of maps S⁰ → X whose distinguished point lies in the path component of x.

@[simp]

theorem TauCeti.fundamentalGroup_smul_eq_self {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x : X} [Subsingleton (FundamentalGroup X x)] (γ : FundamentalGroup X x) (a : HomotopyGroup N X x) : γ • a = a

On a space with trivial fundamental group at x — a simply connected space, for instance — the action is trivial. Thus in positive dimensions based and free homotopy classes of maps Sⁿ → X landing in the path component of x agree; in dimension zero this uses the interpretation with the distinguished point restricted to the path component of x.

theorem TauCeti.one_mem_orbit_of_forall_mem_of_nullhomotopic {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x : X} [Nonempty N] [DecidableEq N] {s : Set X} (hs : { toFun := Subtype.val, continuous_toFun := ⋯ }.Nullhomotopic) (p : ↑(GenLoop N X x)) (hp : ∀ (z : N → ↑unitInterval), p z ∈ s) : 1 ∈ MulAction.orbit (FundamentalGroup X x) ⟦p⟧

A generalized loop staying in a set whose inclusion is null-homotopic is freely homotopic to the constant loop: the identity class lies in the orbit of its class. Composing the loop with a null-homotopy of the inclusion moves the whole cube boundary along the single path traced by the base point.