Homotopy Theory

Wikipedia nLab

Contents

Homotopy n-Type

Uniqueness of identity proofs and Hedberg’s theorem

Truncation

|-|n : A β†’ ||A||n, r : π•Šn + 1 β†’ ||A||n, h(r) : ||A||n, r : π•Šn + 1 β†’ ||A||n, x : π•Šn + 1, sr(x) : r(x) = h(r).

Lemma

is-truncatedn(||A||n).

n-connected

f : A β†’ B ⊒ is-connectedn(f) ≑ (b : B) β†’ is-truncated-2(||fibf(b)||n), is-connectedn(A) ≑ Ξ£f : A β†’ 1 is-connectedn(f).

Lemma

is-connected-1(f) = is-surjective(f).

Lemma

f : A β†’ B, g : B β†’ C ⊒ is-connectedn(f) β†’ is-connectedn(g) = is-connectedn(g f).

Lemma

f : A β†’ B, P : B β†’ U, s ↦ s f : ((b : B) β†’ P(b)) β†’ ((a : A) β†’ P(f(a))) ⊒ is-connectedn(f)≃

Corollary

|-|n : A β†’ ||A||n ⊒ is-connectedn(|-|n).

Corollary

b ↦ a ↦ b : B β†’ (A β†’ B) ⊒ is-connectedn(A) = ((B : U) β†’ is-truncatedn(B) β†’ is-equivalence((b : B) ↦ a ↦ b)).

Lemma

f : A β†’ B, g : ||A||n β†’ B ⊒ is-truncatedn(B) β†’ is-equivalence(g) = is-connectedn(f).

Lemma

a0 : 1 β†’ A ⊒(-1 ≀ n) β†’ is-connectedn(A) = is-connectedn - 1(a0).

Lemma

f : A β†’ B, P : A β†’ U, Q : B β†’ U, g : (a : A) β†’ P(a) β†’ Q(f(a)) ⊒ Ο†(a, u) ≑ (f(a), ga), Ο† : (Ξ£a : A P(a)) β†’ (Ξ£b : B Q(b)), is-connectedn(ga) β†’ is-connectedn(f) β†’ is-connectedn(Ο†).

Lemma

P, Q : A β†’ U, f : (a : A) β†’ (P(a) β†’ Q(a)) ⊒ total(f) : Ξ£a : A P(a) β†’ Ξ£a : A Q(a), is-connectedn(total(f)).

Lemma

f : A β†’ B ⊒ is-connectedn(f), ||A||n ≃ ||B||n.

Orthogonal factorisation

n-truncated

f : A β†’ B ⊒ is-truncatedn(f) ≑ (b : B) β†’ is-truncatedn(fibf(b)). is-truncated-2(f) = is-equivalence(f). is-truncatedn(A) = is-truncatedn(f : A β†’ 1).

Lemma

n-image

f : A β†’ B ⊒ imn(f) ≑ Ξ£b : b ||fibf(b)||n.

Lemma

f : A β†’ B, f~ : A β†’ imn(f) ⊒ is-connectedn(f~).

Lemma

H : h1 g1 ∼ h2 g2, b : B ⊒ is-connectedn(g1) Γ— is-connectedn(g2) Γ— is-truncatedn(h1) Γ— is-truncatedn(h2) β†’ E(H, b) : fibh1(b) ≃ fibh2(b), E-(H, a) : E(H, h1(g1(a)))(g1(a), reflh1(g1(a))) = (g2(a), H(a)-1).

Theorem

f : A β†’ B ⊒ factn(f) ≑ Ξ£X : U Ξ£g : A β†’ X Ξ£h : X β†’ B (h g ∼ f) Γ— is-connectedn(g) is-truncatedn(h), is-truncated-2(factn(f)),(imn(f), f~, pr1, ΞΈ, Ο†, ψ) : factn(f),

Theorem

e : A β†’ B, m : C β†’ D, Ο† : (B β†’ C) β†’ Ξ£h : A β†’ C Ξ£k : B β†’ D (m h ∼ k e) ⊒ is-connectedn(e) Γ— is-truncatedn(m) β†’ is-equivalence(Ο†).

Lemma

fibf(b) ≃ fibg(h(b)).

Reflective subuniverse

P : U β†’ (-1)-type, A : U ⊒ β—‹A, Ξ·A : A β†’ β—‹A(β—‹A β†’ B) β†’ (A β†’ B), f ↦ f Ξ·A. UP ≑ {A : U | P(A)}.

Modality

β—‹ : U β†’ U, Ξ·Aβ—‹ : A β†’ β—‹A, indβ—‹ : ((a : A) β†’ β—‹(B(Ξ·Aβ—‹(a)))) β†’ Ξ z : β—‹A β—‹(B(z)), indβ—‹(f)(Ξ·Aβ—‹(a)) = f(a), f : (a : A) β†’ β—‹(B(Ξ·Aβ—‹(a))), z, z' : β—‹A, Ξ·z = z'β—‹ : (z = z') β†’ β—‹(z = z').

Ξ©0(A, a) ≑ (A, a), Ξ©n + 1(A, a) ≑ Ξ©n(Ξ©(A, a)).

Homotopy group Wikipedia nLab

1 ≀ n β†’ Ο€n(A, a) ≑ ||Ξ©n(A, a)||0.

Ο€1(S1)

β†Ί : base = base, ↺– : β„€ β†’ (base = base). β†Ί0 = reflbase, β†Ίn + 1 = β†Ίn β‹… β†Ί, β†Ίβˆ’(n + 1) = β†Ίβˆ’n β‹… β†Ίβˆ’1,

Universal cover of π•Š1

code(base : π•Š1) ≑ β„€, apcode(β†Ί) ≑ ua(succ).

Lemma

transportcode(β†Ί, x) = x + 1, transportcode(β†Ί-1, x) = x - 1. ∡ transportcode(β†Ί, x) = transportA ↦ A(code(β†Ί), x) (by Lemma 2.3.10)= transportA ↦ A(ua(succ), x) (by computation for resπ•Š1)= x + 1. (by computation for ua)

x : π•Š1 β†’ ((base = x) β†’ code(x)), x : π•Š1 β†’ (code(x) β†’ (base = x)).

encode

encode(p : x : π•Š1 β†’ (base = x)) ≑ transportcode(p, 0).

decode

transportx' ↦ code(x') β†’ (base = x')(β†Ί, β†Ί-)= transportx' ↦ (base = x')(β†Ί) β†Ί- transportcode(β†Ί-1)= (- β†Ί) β†Ί-1 transportcode(β†Ί-1)= (- β†Ί) β†Ί-1 pred = n ↦ β†Ίn - 1 β†Ί.

Lemma

x : π•Š1 β†’ p : base = x β†’ _ : decodex(encodex(p)) = p.

Lemma

x : π•Š1 β†’ (c : code(x)) β†’ encodex(decodex(c)) = c. ∡

Theorem

_ : x : π•Š1 β†’ ((base = x) ≃ code(x)).

Corollary

Ξ©(π•Š1, base) ≃ β„€.

Corollary

Ο€1(π•Š1) = β„€. 1 < n β†’ Ο€n(π•Š1) = 0.

Lemma

(x : π•Š1 β†’ (code(x))) ≃ 1.

Corollary

_ : (x : π•Š1 β†’ (base = x)) ≃ x : π•Š1 β†’ code(x).(x : π•Š1 β†’ (base = x)) ≃ 1,(x : π•Š1 β†’ code(x)) ≃ 1.

Theorem

Ξ©(S1, base) ≃ β„€.

Theorem

(code, 0), base : S1.

Corollary

x : π•Š1 β†’ _ : (base = x) ≃ code(x).

Connectedness of suspensions

Theorem

is-n-connected(A) β†’ is-(n + 1)-connected(||1 βŠ”A 1||n + 1). coconeD(E) = E.(1 β†’ E) ≃ coconeD(E). ||1 βŠ”A 1||n + 1 = 1.

Corollary

n : β„• β†’ is-(n βˆ’ 1)-connected(π•Š1).

Ο€k ≀ n of an n-connected space and Ο€k < n(Sn)

Lemma

Lemma

Fiber Sequences and the Long Exact Sequence

Pointed Map

(X, x0), (Y, y0), f : X β†’ Y, f0 : f(x0) = y0.

Ξ©f

f : X β†’ Y β†’ Ξ©f : Ξ©X β†’ Ξ©Y, Ξ©f(p) ≑ f0-1 f(p) f0.

fiber sequence

f : X β†’ Y β†’ X0 ≑ Y, X1 ≑ X, f0 ≑ f, Xn + 1 ≑ fibfn - 1(xn - 1, 0), fn ≑ pr1 : Xn + 1 β†’ Xn.

Lemma

f : X β†’ Y β†’ f1 ≑ pr1 : fibf(y0) β†’ X, f1 ≃ Ξ©Y. f2 : Ξ©Y β†’ fibf(y0), f2 ≃ Ξ©X. f3 : Ξ©X β†’ Ξ©Y, Ξ©f (–)-1.

ker(f) ≑ {x: A | f(x) = b0}.

Exact sequence of pointed set

f(n - 1)(a) = a0(n - 1) ≃ b : A(n + 1), fn(b) = a.

Theorem

Lemma

K β†’ G β†’f H β†’ Q.

Corollary

Ο€k(fibf(b)) β†’ Ο€k(A, a) β†’f Ο€k(B, b) β†’ Ο€k βˆ’ 1(fibf(b)).

Hopf fibration

Hopf fibration

H π•Š^2 π•Š^1 π•Š^3

Corollary

Ο€_2(π•Š^2) ≃ β„€, 3 ≀ k β†’ Ο€_2(π•Š^2) ≃ Ο€_k(π•Š^2).

Lemma

π’Ÿ = (Y ←j X β†’k Z),
  • E_Y : Y β†’ U, E_Z : Z β†’ U.
  • e_X : x : X β†’ E_y β—¦ j(x) ≃ E_Z β—¦ k(x).
β†’ E : Y βŠ”^X Z β†’ U
  • y : Y β†’ E(inl(y)) ≑ E_Y(y).
  • z : Z β†’ E(inr(z)) ≑ E_Z(z).

H-space

  • A : U,
  • e : A,
  • ΞΌ : A β†’ A β†’ A,
  • a : A β†’ ΞΌ(e, a) = a β†’ ΞΌ(a, e) = a.

Lemma

A : H-space β†’ a : A β†’ is-equiv(ΞΌ(a, βˆ’)) is-equiv(ΞΌ(βˆ’, a)).

Fibration

A : H-space β†’ Ξ£ A

Lemma

Ξ£A ≃ 2 * A.

The Freudenthal suspension theorem

Lemma

(– β—¦ f) : (b : B β†’ P) β†’ (a : A β†’ f β†’ P).

Wedge connectivity lemma

Freudenthal suspension theorem

code

Lemma

Freudenthal equivalence

Stability for spheres

Theorem

Corollary

Corollary

The van Kampen theorem

Naive van Kampen theorem

Example

Example

Example

Van Kampen theorem with a set of basepoints

Whitehead’s theorem and Whitehead’s principle

A general statement of the encode-decode method

Additional results

Homotopy

Wikipedia nLab

References