module Homotopy.Space.Sphere.Degree where
Degrees of maps of spheres🔗
Piecing together our characterisation of the homotopy groups of higher spheres as the group of integers with the equivalence between the loop space and the space of pointed maps we obtain a function which associates to every pointed map an integer; we call this number the degree of
degree∙ : ∀ n → (Sⁿ (suc n) →∙ Sⁿ (suc n)) → Int degree∙ n f = πₙSⁿ≃Int n · inc (Ωⁿ≃Sⁿ-map (suc n) · f)
Intuitively, the degree of a map
is a generalisation of the winding number of a loop in
it measures how many times
“wraps around” the
In particular, the degree of the identity map is
and the degree of the zero∙ map is
To prove this, we first establish a useful property of the degrees of
maps of spheres.
The fact that the isomorphisms are compatible with suspension implies that the maps and have the same degree; indeed, the functorial action of and the map fit together in the following diagram over
opaque unfolding Ωⁿ≃∙Sⁿ-map Ωⁿ-suspend-is-Susp-map∙ : ∀ {ℓ} (A : Type∙ ℓ) n (f : Sⁿ (suc n) →∙ A) → Ωⁿ≃Sⁿ-map (2 + n) · Susp-map∙ f ≡ Ωⁿ-suspend (suc n) _ · (Ωⁿ≃Sⁿ-map (suc n) · f) Ωⁿ-suspend-is-Susp-map∙ A n f = Equiv∙.from∙ (Ωⁿ-suc (Σ¹ A) (suc n)) · (Ωⁿ≃Sⁿ-map (suc n) · ⌜ Σ-map∙≃∙map∙-Ω · Susp-map∙ f ⌝) ≡⟨ ap! (Equiv.adjunctr Σ-map∙≃map∙-Ω (sym (suspend∙-is-unit f))) ⟩≡ Equiv∙.from∙ (Ωⁿ-suc (Σ¹ A) (suc n)) · ⌜ Ωⁿ≃Sⁿ-map (suc n) · (suspend∙ A ∘∙ f) ⌝ ≡˘⟨ ap¡ (Ωⁿ≃Sⁿ-map-natural (suc n) (suspend∙ A) f) ⟩≡˘ Equiv∙.from∙ (Ωⁿ-suc (Σ¹ A) (suc n)) · (Ωⁿ-map (suc n) (suspend∙ A) · (Ωⁿ≃Sⁿ-map (suc n) · f)) ∎ degree∙-Susp-map∙ : ∀ n (f : Sⁿ (suc n) →∙ Sⁿ (suc n)) → degree∙ (suc n) (Susp-map∙ f) ≡ degree∙ n f degree∙-Susp-map∙ n f = πₙSⁿ≃Int (suc n) · ∥_∥₀.inc ⌜ Ωⁿ≃Sⁿ-map (2 + n) · Susp-map∙ f ⌝ ≡⟨ ap! (Ωⁿ-suspend-is-Susp-map∙ (Sⁿ (suc n)) n f) ⟩≡ πₙSⁿ≃Int (suc n) · inc (Ωⁿ-suspend (suc n) (Sⁿ (suc n)) · (Ωⁿ≃Sⁿ-map (suc n) · f)) ≡⟨ πₙSⁿ≃Int-suspend n _ ⟩≡ degree∙ n f ∎
This lets us characterise the degrees of the identity and zero maps by induction: in both cases, the base case computes, and the induction step uses the fact that preserves those maps.
opaque unfolding conj Ω¹-map Ωⁿ≃∙Sⁿ-map degree∙-id∙ : ∀ n → degree∙ n id∙ ≡ 1 degree∙-id∙ zero = refl degree∙-id∙ (suc n) = degree∙ (suc n) ⌜ id∙ ⌝ ≡˘⟨ ap¡ (Susp-map∙-id {A∙ = Sⁿ (suc n)}) ⟩≡˘ degree∙ (suc n) (Susp-map∙ {A∙ = Sⁿ (suc n)} id∙) ≡⟨ degree∙-Susp-map∙ n id∙ ⟩≡ degree∙ n id∙ ≡⟨ degree∙-id∙ n ⟩≡ 1 ∎ degree∙-zero∙ : ∀ n → degree∙ n zero∙ ≡ 0 degree∙-zero∙ zero = refl degree∙-zero∙ (suc n) = degree∙ (suc n) ⌜ zero∙ ⌝ ≡˘⟨ ap¡ (Susp-map∙-zero {A∙ = Sⁿ (suc n)}) ⟩≡˘ degree∙ (suc n) (Susp-map∙ {A∙ = Sⁿ (suc n)} zero∙) ≡⟨ degree∙-Susp-map∙ n zero∙ ⟩≡ degree∙ n zero∙ ≡⟨ degree∙-zero∙ n ⟩≡ 0 ∎
Degrees of unpointed maps of spheres🔗
We extend the definition of degrees above to unpointed maps by showing that the set of pointed homotopy classes of maps is equivalent to the set of homotopy classes of unpointed maps
We start by showing that the map which forgets the pointing is injective; in other words, that for any two paths the pointed maps and are merely equal.
Sⁿ-unpoint : ∀ n → ∥ (Sⁿ (suc n) →∙ Sⁿ (suc n)) ∥₀ → ∥ (⌞ Sⁿ (suc n) ⌟ → ⌞ Sⁿ (suc n) ⌟) ∥₀ Sⁿ-unpoint n = ∥-∥₀-rec (hlevel 2) λ (f , _) → inc f Sⁿ-unpoint-injective : ∀ n f (p q : f north ≡ north) → ∥ Path (Sⁿ (suc n) →∙ Sⁿ (suc n)) (f , p) (f , q) ∥
There are two cases: when is a concrete abelian group, and some abstract nonsense about first abelian group cohomology tells us that the set of unpointed maps is equivalent to the set of concrete group automorphisms of which is just the set of pointed maps
Sⁿ-unpoint-injective zero f p q = inc (S¹-cohomology.injective refl) where Sⁿ⁼¹-concrete : ConcreteGroup lzero Sⁿ⁼¹-concrete .B = Sⁿ 1 Sⁿ⁼¹-concrete .has-is-connected = connected∙ Sⁿ⁼¹-concrete .has-is-groupoid = Equiv→is-hlevel 3 SuspS⁰≃S¹ S¹-is-groupoid Sⁿ⁼¹≡S¹ : Sⁿ⁼¹-concrete ≡ S¹-concrete Sⁿ⁼¹≡S¹ = ConcreteGroup-path (ua∙ SuspS⁰≃∙S¹) Sⁿ⁼¹-ab : is-concrete-abelian Sⁿ⁼¹-concrete Sⁿ⁼¹-ab = subst is-concrete-abelian (sym Sⁿ⁼¹≡S¹) S¹-concrete-abelian module S¹-cohomology = Equiv (first-concrete-abelian-group-cohomology Sⁿ⁼¹-concrete Sⁿ⁼¹-concrete Sⁿ⁼¹-ab)
The case is a lot more down-to-earth: in that case, is simply connected, so the paths and are themselves merely equal.
Sⁿ-unpoint-injective (suc n) f p q = ap (f ,_) <$> simply-connected p q
Since the
is connected, every map
is merely pointed, so the map Sⁿ-unpoint is also
surjective, hence an equivalence of sets.
Sⁿ-pointed≃unpointed : ∀ n → ∥ (Sⁿ (suc n) →∙ Sⁿ (suc n)) ∥₀ ≃ ∥ (⌞ Sⁿ (suc n) ⌟ → ⌞ Sⁿ (suc n) ⌟) ∥₀ Sⁿ-pointed≃unpointed n .fst = Sⁿ-unpoint n Sⁿ-pointed≃unpointed n .snd = injective-surjective→is-equiv! (inj _ _) surj where inj : ∀ f g → Sⁿ-unpoint n f ≡ Sⁿ-unpoint n g → f ≡ g inj = elim! λ f ptf g ptg f≡g → ∥-∥₀-path.from do f≡g ← ∥-∥₀-path.to f≡g J (λ g _ → ∀ ptg → ∥ (f , ptf) ≡ (g , ptg) ∥) (Sⁿ-unpoint-injective n f ptf) f≡g ptg surj : is-surjective (Sⁿ-unpoint n) surj = ∥-∥₀-elim (λ _ → hlevel 2) λ f → do pointed ← connected (f north) north pure (inc (f , pointed) , refl)
Since is a set, we can therefore define the degree of an unpointed map by set-truncation recursion on the corresponding class of pointed maps, and show that the degree of a pointed map is the degree of its underlying unpointed map.
degree : ∀ n → (⌞ Sⁿ (suc n) ⌟ → ⌞ Sⁿ (suc n) ⌟) → Int degree n f = ∥-∥₀-rec (hlevel 2) (degree∙ n) (Equiv.from (Sⁿ-pointed≃unpointed n) (inc f)) degree≡degree∙ : ∀ n f∙ → degree n (f∙ .fst) ≡ degree∙ n f∙ degree≡degree∙ n f∙ = ap (∥-∥₀-rec _ _) (Equiv.η (Sⁿ-pointed≃unpointed n) (inc f∙))