Higher homotopy groups are homeomorphism invariants

The functoriality API in TauCeti.Topology.Homotopy.HomotopyGroup.Map records the map HomotopyGroup.map on homotopy classes induced by a based continuous map (a monoid homomorphism HomotopyGroup.mapHom in positive dimensions), but it stops short of packaging a homeomorphism as an isomorphism of homotopy groups. This file supplies that: a homeomorphism e : X ≃ₜ Y induces an equivalence π_N(X, x) ≃ π_N(Y, e x) in every dimension, and a group isomorphism π_N(X, x) ≃* π_N(Y, e x) in positive dimensions, and more generally the versions sending x to any y with e x = y.

The forward and inverse application lemmas characterize these equivalences as HomotopyGroup.map for e and e.symm, respectively.

The file also records a homeomorphism between spaces of generalized loops themselves: Mathlib's bijection genLoopEquivOfUnique between the generalized loops indexed by a singleton and the loop space Ω X x is continuous both ways for the compact-open topologies.

Transporting a homotopy-group computation across a homeomorphism is the dimension-N analogue of TauCeti.FundamentalGroup.homeomorphMulEquiv, and is part of the higher-homotopy-group API the universal-covers roadmap asks for in Stage 3 item 9 (TauCetiRoadmap/UniversalCovers/README.md), before proving that a covering map induces isomorphisms on π_n for n ≥ 2.

Main declarations

• HomotopyGroup.homeomorphEquivOfEq: π_N(X, x) ≃ π_N(Y, y) from e : X ≃ₜ Y with e x = y.
• HomotopyGroup.homeomorphEquiv: π_N(X, x) ≃ π_N(Y, e x).
• HomotopyGroup.homeomorphMulEquivOfEq: the positive-dimensional group isomorphism π_N(X, x) ≃* π_N(Y, y).
• HomotopyGroup.homeomorphMulEquiv: π_N(X, x) ≃* π_N(Y, e x).
• GenLoop.homeomorphOfUnique: Ω^ N X x ≃ₜ Ω X x for N a singleton.

def GenLoop.homeomorphOfUnique {X : Type u_2} [TopologicalSpace X] {x : X} (N : Type u_3) [Unique N] : ↑(GenLoop N X x) ≃ₜ LoopSpace X x

Mathlib's bijection genLoopEquivOfUnique between the one-dimensional generalized loops at x and the loop space Ω X x, upgraded to a homeomorphism for the compact-open topologies.

Equations

• GenLoop.homeomorphOfUnique N = { toEquiv := genLoopEquivOfUnique N, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem GenLoop.homeomorphOfUnique_apply {X : Type u_2} [TopologicalSpace X] {x : X} (N : Type u_3) [Unique N] (p : ↑(GenLoop N X x)) (t : ↑unitInterval) : ((homeomorphOfUnique N) p) t = p fun (x : N) => t

@[simp]

theorem GenLoop.homeomorphOfUnique_symm_apply {X : Type u_2} [TopologicalSpace X] {x : X} (N : Type u_3) [Unique N] (γ : LoopSpace X x) (t : N → ↑unitInterval) : ((homeomorphOfUnique N).symm γ) t = γ (t default)

@[simp]

theorem GenLoop.homeomorphOfUnique_const {X : Type u_2} [TopologicalSpace X] {x : X} (N : Type u_3) [Unique N] : (homeomorphOfUnique N) const = Path.refl x

The homeomorphism of GenLoop.homeomorphOfUnique is based: it carries the constant generalized loop to the constant path.

noncomputable def HomotopyGroup.homeomorphEquivOfEq {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (e : X ≃ₜ Y) (h : e x = y) : HomotopyGroup N X x ≃ HomotopyGroup N Y y

A homeomorphism e : X ≃ₜ Y carrying x to y induces an equivalence of homotopy groups π_N(X, x) ≃ π_N(Y, y). The forward map is HomotopyGroup.map of e; the inverse is HomotopyGroup.map of e.symm. This holds in every dimension N.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HomotopyGroup.homeomorphEquivOfEq_apply {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (e : X ≃ₜ Y) (h : e x = y) (a : HomotopyGroup N X x) : (homeomorphEquivOfEq e h) a = map { toFun := ⇑e, continuous_toFun := ⋯ } h a

@[simp]

theorem HomotopyGroup.homeomorphEquivOfEq_symm_apply {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (e : X ≃ₜ Y) (h : e x = y) (b : HomotopyGroup N Y y) : (homeomorphEquivOfEq e h).symm b = map { toFun := ⇑e.symm, continuous_toFun := ⋯ } ⋯ b

noncomputable def HomotopyGroup.homeomorphEquiv {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (x : X) : HomotopyGroup N X x ≃ HomotopyGroup N Y (e x)

A homeomorphism e : X ≃ₜ Y induces an equivalence of homotopy groups π_N(X, x) ≃ π_N(Y, e x), in every dimension N.

Equations

• HomotopyGroup.homeomorphEquiv e x = HomotopyGroup.homeomorphEquivOfEq e ⋯

@[simp]

theorem HomotopyGroup.homeomorphEquiv_apply {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (x : X) (a : HomotopyGroup N X x) : (homeomorphEquiv e x) a = map { toFun := ⇑e, continuous_toFun := ⋯ } ⋯ a

@[simp]

theorem HomotopyGroup.homeomorphEquiv_symm_apply {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (x : X) (b : HomotopyGroup N Y (e x)) : (homeomorphEquiv e x).symm b = map { toFun := ⇑e.symm, continuous_toFun := ⋯ } ⋯ b

noncomputable def HomotopyGroup.homeomorphMulEquivOfEq {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} [DecidableEq N] [Nonempty N] (e : X ≃ₜ Y) (h : e x = y) : HomotopyGroup N X x ≃* HomotopyGroup N Y y

A homeomorphism e : X ≃ₜ Y carrying x to y induces an isomorphism of homotopy groups π_N(X, x) ≃* π_N(Y, y) in positive dimensions.

Equations

• HomotopyGroup.homeomorphMulEquivOfEq e h = { toEquiv := HomotopyGroup.homeomorphEquivOfEq e h, map_mul' := ⋯ }

@[simp]

theorem HomotopyGroup.homeomorphMulEquivOfEq_apply {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} [DecidableEq N] [Nonempty N] (e : X ≃ₜ Y) (h : e x = y) (a : HomotopyGroup N X x) : (homeomorphMulEquivOfEq e h) a = map { toFun := ⇑e, continuous_toFun := ⋯ } h a

@[simp]

theorem HomotopyGroup.homeomorphMulEquivOfEq_symm_apply {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} [DecidableEq N] [Nonempty N] (e : X ≃ₜ Y) (h : e x = y) (b : HomotopyGroup N Y y) : (homeomorphMulEquivOfEq e h).symm b = map { toFun := ⇑e.symm, continuous_toFun := ⋯ } ⋯ b

noncomputable def HomotopyGroup.homeomorphMulEquiv {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [DecidableEq N] [Nonempty N] (e : X ≃ₜ Y) (x : X) : HomotopyGroup N X x ≃* HomotopyGroup N Y (e x)

A homeomorphism e : X ≃ₜ Y induces an isomorphism of homotopy groups π_N(X, x) ≃* π_N(Y, e x) in positive dimensions.

Equations

• HomotopyGroup.homeomorphMulEquiv e x = HomotopyGroup.homeomorphMulEquivOfEq e ⋯

@[simp]

theorem HomotopyGroup.homeomorphMulEquiv_apply {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [DecidableEq N] [Nonempty N] (e : X ≃ₜ Y) (x : X) (a : HomotopyGroup N X x) : (homeomorphMulEquiv e x) a = map { toFun := ⇑e, continuous_toFun := ⋯ } ⋯ a

@[simp]

theorem HomotopyGroup.homeomorphMulEquiv_symm_apply {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [DecidableEq N] [Nonempty N] (e : X ≃ₜ Y) (x : X) (b : HomotopyGroup N Y (e x)) : (homeomorphMulEquiv e x).symm b = map { toFun := ⇑e.symm, continuous_toFun := ⋯ } ⋯ b