From f3d8889726ec5e75ed638679c6ed33546181a20c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Axel=20Ljungstr=C3=B6m?= <49276137+aljungstrom@users.noreply.github.com> Date: Wed, 11 Sep 2024 16:30:24 +0200 Subject: [PATCH] Minor fix: improved definition of whitehead products (#1155) * t * duplicate * wups * rme * ganea stuff * w * w * w * stuff * stuff * fixes * fixes * fixes * added comment * fix * typo * another typo * wups * change def of wh prod * minor --- Cubical/Foundations/Path.agda | 10 + Cubical/Foundations/Prelude.agda | 10 + Cubical/HITs/S2/Properties.agda | 12 +- Cubical/HITs/Sn/Multiplication.agda | 152 ++++++- Cubical/HITs/Sn/Properties.agda | 294 +------------ Cubical/HITs/Susp/Properties.agda | 9 + Cubical/Homotopy/Group/Base.agda | 7 +- Cubical/Homotopy/Group/Join.agda | 6 + Cubical/Homotopy/Group/Pi3S2.agda | 1 + .../Homotopy/Group/Pi4S3/BrunerieNumber.agda | 35 +- Cubical/Homotopy/Group/Pi4S3/DirectProof.agda | 410 +++++------------- Cubical/Homotopy/Hopf.agda | 2 +- Cubical/Homotopy/HopfInvariant/Brunerie.agda | 3 +- Cubical/Homotopy/HopfInvariant/HopfMap.agda | 1 + Cubical/Homotopy/Whitehead.agda | 165 ++++--- Cubical/Papers/Pi4S3-JournalVersion.agda | 4 +- Cubical/Papers/Pi4S3.agda | 5 +- 17 files changed, 434 insertions(+), 692 deletions(-) diff --git a/Cubical/Foundations/Path.agda b/Cubical/Foundations/Path.agda index a738bdf499..4bc87ae60c 100644 --- a/Cubical/Foundations/Path.agda +++ b/Cubical/Foundations/Path.agda @@ -410,6 +410,16 @@ compPathR→PathP∙∙ {p = p} {q = q} {r = r} {s = s} P j i = ; (j = i1) → doubleCompPath-filler p s (sym q) (~ k) i}) (P j i) +PathP→compPathR∙∙ : {a b c d : A} {p : a ≡ c} {q : b ≡ d} {r : a ≡ b} {s : c ≡ d} + → PathP (λ i → p i ≡ q i) r s + → r ≡ p ∙∙ s ∙∙ sym q +PathP→compPathR∙∙ {p = p} {q = q} {r = r} {s = s} P j i = + hcomp (λ k → λ { (i = i0) → p (j ∧ ~ k) + ; (i = i1) → q (j ∧ ~ k) + ; (j = i0) → r i + ; (j = i1) → doubleCompPath-filler p s (sym q) k i}) + (P j i) + compPath→Square-faces : {a b c d : A} (p : a ≡ c) (q : b ≡ d) (r : a ≡ b) (s : c ≡ d) → (i j k : I) → Partial (i ∨ ~ i ∨ j ∨ ~ j) A compPath→Square-faces p q r s i j k = λ where diff --git a/Cubical/Foundations/Prelude.agda b/Cubical/Foundations/Prelude.agda index 993a2a6af1..7d2151f194 100644 --- a/Cubical/Foundations/Prelude.agda +++ b/Cubical/Foundations/Prelude.agda @@ -87,6 +87,16 @@ cong₂ : {C : (a : A) → (b : B a) → Type ℓ} → cong₂ f p q i = f (p i) (q i) {-# INLINE cong₂ #-} +cong₃ : {C : (a : A) → (b : B a) → Type ℓ} + {D : (a : A) (b : B a) → C a b → Type ℓ'} + (f : (a : A) (b : B a) (c : C a b) → D a b c) → + {x y : A} (p : x ≡ y) + {u : B x} {v : B y} (q : PathP (λ i → B (p i)) u v) + {s : C x u} {t : C y v} (r : PathP (λ i → C (p i) (q i)) s t) + → PathP (λ i → D (p i) (q i) (r i)) (f x u s) (f y v t) +cong₃ f p q r i = f (p i) (q i) (r i) +{-# INLINE cong₃ #-} + congP₂ : {A : I → Type ℓ} {B : (i : I) → A i → Type ℓ'} {C : (i : I) (a : A i) → B i a → Type ℓ''} (f : (i : I) → (a : A i) → (b : B i a) → C i a b) diff --git a/Cubical/HITs/S2/Properties.agda b/Cubical/HITs/S2/Properties.agda index 3d4b60fe14..89faa21478 100644 --- a/Cubical/HITs/S2/Properties.agda +++ b/Cubical/HITs/S2/Properties.agda @@ -7,6 +7,7 @@ open import Cubical.Foundations.Pointed open import Cubical.Foundations.Function open import Cubical.Foundations.GroupoidLaws open import Cubical.Foundations.Path +open import Cubical.Foundations.Isomorphism open import Cubical.HITs.S1.Base open import Cubical.HITs.S2.Base @@ -63,11 +64,20 @@ S¹×S¹→S² base y = base S¹×S¹→S² (loop i) base = base S¹×S¹→S² (loop i) (loop j) = surf i j - invS² : S² → S² invS² base = base invS² (surf i j) = surf j i +invS²∘invS²≡id : (x : _) → invS² (invS² x) ≡ x +invS²∘invS²≡id base = refl +invS²∘invS²≡id (surf i i₁) = refl + +invS²Iso : Iso S² S² +Iso.fun invS²Iso = invS² +Iso.inv invS²Iso = invS² +Iso.rightInv invS²Iso = invS²∘invS²≡id +Iso.leftInv invS²Iso = invS²∘invS²≡id + S¹×S¹→S²-anticomm : (x y : S¹) → invS² (S¹×S¹→S² x y) ≡ S¹×S¹→S² y x S¹×S¹→S²-anticomm base base = refl S¹×S¹→S²-anticomm base (loop i) = refl diff --git a/Cubical/HITs/Sn/Multiplication.agda b/Cubical/HITs/Sn/Multiplication.agda index 00ca912c0c..56899e9848 100644 --- a/Cubical/HITs/Sn/Multiplication.agda +++ b/Cubical/HITs/Sn/Multiplication.agda @@ -4,7 +4,8 @@ This file contains: 1. Definition of the multplication Sⁿ × Sᵐ → Sⁿ⁺ᵐ 2. The fact that the multiplication induces an equivalence Sⁿ ∧ Sᵐ ≃ Sⁿ⁺ᵐ -3. The algebraic properties of this map +3. The fact that the multiplication induces an equivalence Sⁿ * Sᵐ ≃ Sⁿ⁺ᵐ⁺¹ +4. The algebraic properties of this map -} module Cubical.HITs.Sn.Multiplication where @@ -25,8 +26,9 @@ open import Cubical.Data.Bool hiding (elim) open import Cubical.Data.Nat hiding (elim) open import Cubical.Data.Sigma -open import Cubical.HITs.S1 hiding (_·_) -open import Cubical.HITs.Sn hiding (IsoSphereJoin) +open import Cubical.HITs.S1 renaming (_·_ to _*_) +open import Cubical.HITs.S2 +open import Cubical.HITs.Sn open import Cubical.HITs.Susp renaming (toSusp to σ) open import Cubical.HITs.Join open import Cubical.HITs.Pushout @@ -316,6 +318,21 @@ joinSphereIso' n m = (compIso (congSuspIso (SphereSmashIso n m)) (invIso (IsoSucSphereSusp (n + m)))) +-- The inverse function is not definitionally pointed. Let's change this +sphere→Join : (n m : ℕ) + → S₊ (suc (n + m)) → join (S₊ n) (S₊ m) +sphere→Join zero zero = Iso.inv (joinSphereIso' 0 0) +sphere→Join zero (suc m) north = inl true +sphere→Join zero (suc m) south = inl true +sphere→Join zero (suc m) (merid a i) = + (push true (ptSn (suc m)) + ∙ cong (Iso.inv (joinSphereIso' zero (suc m))) (merid a)) i +sphere→Join (suc n) m north = inl (ptSn (suc n)) +sphere→Join (suc n) m south = inl (ptSn (suc n)) +sphere→Join (suc n) m (merid a i) = + (push (ptSn (suc n)) (ptSn m) + ∙ cong (Iso.inv (joinSphereIso' (suc n) m)) (merid a)) i + join→Sphere≡ : (n m : ℕ) (x : _) → join→Sphere n m x ≡ joinSphereIso' n m .Iso.fun x join→Sphere≡ zero zero (inl x) = refl @@ -338,22 +355,45 @@ join→Sphere≡ (suc n) (suc m) (push a b i) j = compPath-filler (merid (a ⌣S b)) (sym (merid (ptSn (suc n + suc m)))) (~ j) i +sphere→Join≡ : (n m : ℕ) (x : _) + → sphere→Join n m x ≡ joinSphereIso' n m .Iso.inv x +sphere→Join≡ zero zero x = refl +sphere→Join≡ zero (suc m) north = push true (pt (S₊∙ (suc m))) +sphere→Join≡ zero (suc m) south = refl +sphere→Join≡ zero (suc m) (merid a i) j = + compPath-filler' (push true (pt (S₊∙ (suc m)))) + (cong (joinSphereIso' zero (suc m) .Iso.inv) (merid a)) (~ j) i +sphere→Join≡ (suc n) m north = push (ptSn (suc n)) (pt (S₊∙ m)) +sphere→Join≡ (suc n) m south = refl +sphere→Join≡ (suc n) m (merid a i) j = + compPath-filler' (push (ptSn (suc n)) (pt (S₊∙ m))) + (cong (joinSphereIso' (suc n) m .Iso.inv) (merid a)) (~ j) i + -- Todo: integrate with Sn.Properties IsoSphereJoin IsoSphereJoin : (n m : ℕ) → Iso (join (S₊ n) (S₊ m)) (S₊ (suc (n + m))) fun (IsoSphereJoin n m) = join→Sphere n m -inv (IsoSphereJoin n m) = joinSphereIso' n m .Iso.inv +inv (IsoSphereJoin n m) = sphere→Join n m rightInv (IsoSphereJoin n m) x = - join→Sphere≡ n m (joinSphereIso' n m .Iso.inv x) + (λ i → join→Sphere≡ n m (sphere→Join≡ n m x i) i) ∙ joinSphereIso' n m .Iso.rightInv x leftInv (IsoSphereJoin n m) x = - cong (joinSphereIso' n m .inv) (join→Sphere≡ n m x) + (λ i → sphere→Join≡ n m (join→Sphere≡ n m x i) i) ∙ joinSphereIso' n m .Iso.leftInv x joinSphereEquiv∙ : (n m : ℕ) → join∙ (S₊∙ n) (S₊∙ m) ≃∙ S₊∙ (suc (n + m)) fst (joinSphereEquiv∙ n m) = isoToEquiv (IsoSphereJoin n m) snd (joinSphereEquiv∙ n m) = refl +IsoSphereJoinPres∙ : (n m : ℕ) + → Iso.fun (IsoSphereJoin n m) (inl (ptSn n)) ≡ ptSn (suc (n + m)) +IsoSphereJoinPres∙ n m = refl + +IsoSphereJoin⁻Pres∙ : (n m : ℕ) + → Iso.inv (IsoSphereJoin n m) (ptSn (suc (n + m))) ≡ inl (ptSn n) +IsoSphereJoin⁻Pres∙ zero zero = push true true ⁻¹ +IsoSphereJoin⁻Pres∙ zero (suc m) = refl +IsoSphereJoin⁻Pres∙ (suc n) m = refl -- Associativity ⌣S -- Preliminary lemma @@ -896,3 +936,103 @@ comm⌣S {n = suc (suc n)} {m = suc (suc m)} x y = ∙ sym (cong (subst S₊ (sym (+-comm (suc m) (suc n))) ∘ -S^ (suc n · suc m)) (comm⌣S x y))) x y + +-- Additional properties in low dimension: +diag⌣ : {n : ℕ} (x : S₊ (suc n)) → x ⌣S x ≡ ptSn _ +diag⌣ {n = zero} base = refl +diag⌣ {n = zero} (loop i) j = help j i + where + help : cong₂ _⌣S_ loop loop ≡ refl + help = cong₂Funct _⌣S_ loop loop + ∙ sym (rUnit _) + ∙ rCancel (merid base) +diag⌣ {n = suc n} north = refl +diag⌣ {n = suc n} south = refl +diag⌣ {n = suc n} (merid a i) j = help j i + where + help : cong₂ _⌣S_ (merid a) (merid a) ≡ refl + help = cong₂Funct _⌣S_ (merid a) (merid a) + ∙ sym (rUnit _) + ∙ flipSquare (cong IdL⌣S (merid a)) + +⌣₁,₁-distr : (a b : S¹) → (b * a) ⌣S b ≡ a ⌣S b +⌣₁,₁-distr a base = refl +⌣₁,₁-distr a (loop i) j = lem j i + where + lem : cong₂ (λ (b1 b2 : S¹) → (b1 * a) ⌣S b2) loop loop + ≡ (λ i → a ⌣S loop i) + lem = (cong₂Funct (λ (b1 b2 : S¹) → (b1 * a) ⌣S b2) loop loop + ∙ cong₂ _∙_ (PathP→compPathR + (flipSquare (cong (IdL⌣S {n = 1} {1} ∘ (_* a)) loop)) + ∙ cong₂ _∙_ refl (sym (lUnit _)) + ∙ rCancel _) + refl + ∙ sym (lUnit _)) + +⌣₁,₁-distr' : (a b : S¹) → (a * b) ⌣S b ≡ a ⌣S b +⌣₁,₁-distr' a b = cong (_⌣S b) (commS¹ a b) ∙ ⌣₁,₁-distr a b + +⌣Sinvₗ : {n m : ℕ} (x : S₊ (suc n)) (y : S₊ (suc m)) + → (invSphere x) ⌣S y ≡ invSphere (x ⌣S y) +⌣Sinvₗ {n = zero} {m} base y = merid (ptSn (suc m)) +⌣Sinvₗ {n = zero} {m} (loop i) y j = lem j i + where + lem : Square (σS y ⁻¹) + (λ i → invSphere (loop i ⌣S y)) + (merid (ptSn (suc m))) (merid (ptSn (suc m))) + lem = sym (cong-∙ invSphere' (merid y) (sym (merid (ptSn (suc m)))) + ∙ cong₂ _∙_ refl (rCancel _) + ∙ sym (rUnit _)) + ◁ (λ j i → invSphere'≡ (loop i ⌣S y) j) +⌣Sinvₗ {n = suc n} {m} north y = merid (ptSn (suc (n + suc m))) +⌣Sinvₗ {n = suc n} {m} south y = merid (ptSn (suc (n + suc m))) +⌣Sinvₗ {n = suc n} {m} (merid a i) y j = lem j i + where + p = ptSn (suc (n + suc m)) + + lem : Square (σS (a ⌣S y) ⁻¹) + (λ i → invSphere (merid a i ⌣S y)) + (merid p) (merid p) + lem = (sym (cong-∙ invSphere' (merid (a ⌣S y)) (sym (merid p)) + ∙ cong₂ _∙_ refl (rCancel _) + ∙ sym (rUnit _))) + ◁ λ j i → invSphere'≡ (merid a i ⌣S y) j + +⌣Sinvᵣ : {n m : ℕ} (x : S₊ (suc n)) (y : S₊ (suc m)) + → x ⌣S (invSphere y) ≡ invSphere (x ⌣S y) +⌣Sinvᵣ {n = n} {m} x y = + comm⌣S x (invSphere y) + ∙ cong (subst S₊ (+-comm (suc m) (suc n))) + (cong (-S^ (suc m · suc n)) (⌣Sinvₗ y x) + ∙ sym (invSphere-S^ (suc m · suc n) (y ⌣S x))) + ∙ -S^-transp _ (+-comm (suc m) (suc n)) 1 + (-S^ (suc m · suc n) (y ⌣S x)) + ∙ cong invSphere + (cong (subst S₊ (+-comm (suc m) (suc n))) + (cong (-S^ (suc m · suc n)) (comm⌣S y x) + ∙ sym (-S^-transp _ (+-comm (suc n) (suc m)) + (suc m · suc n) + (-S^ (suc n · suc m) (x ⌣S y))) + ∙ cong (subst S₊ (+-comm (suc n) (suc m))) + ((cong (-S^ (suc m · suc n)) + (λ i → -S^ (·-comm (suc n) (suc m) i) (x ⌣S y))) + ∙ -S^² (suc m · suc n) (x ⌣S y)) + ∙ cong (λ p → subst S₊ p (x ⌣S y)) + (isSetℕ _ _ (+-comm (suc n) (suc m)) + (+-comm (suc m) (suc n) ⁻¹))) + ∙ subst⁻Subst S₊ (+-comm (suc m) (suc n) ⁻¹) (x ⌣S y)) + +-- Interaction between ⌣S, SuspS¹→S² and SuspS¹→S² +SuspS¹→S²-S¹×S¹→S² : (a b : S¹) + → SuspS¹→S² (a ⌣S b) ≡ S¹×S¹→S² a b +SuspS¹→S²-S¹×S¹→S² base b = refl +SuspS¹→S²-S¹×S¹→S² (loop i) b j = main b j i + where + lem : (b : _) → cong SuspS¹→S² (merid b) ≡ (λ j → S¹×S¹→S² (loop j) b) + lem base = refl + lem (loop i) = refl + + main : (b : _) → cong SuspS¹→S² (σS b) ≡ (λ j → S¹×S¹→S² (loop j) b) + main b = cong-∙ SuspS¹→S² (merid b) (merid base ⁻¹) + ∙ sym (rUnit _) + ∙ lem b diff --git a/Cubical/HITs/Sn/Properties.agda b/Cubical/HITs/Sn/Properties.agda index 7eb740a4c0..91bf1fa440 100644 --- a/Cubical/HITs/Sn/Properties.agda +++ b/Cubical/HITs/Sn/Properties.agda @@ -33,8 +33,7 @@ private open Iso σSn : (n : ℕ) → S₊ n → Path (S₊ (suc n)) (ptSn (suc n)) (ptSn (suc n)) -σSn zero false = loop -σSn zero true = refl +σSn zero = cong SuspBool→S¹ ∘ merid σSn (suc n) x = toSusp (S₊∙ (suc n)) x σS : {n : ℕ} → S₊ n → Path (S₊ (suc n)) (ptSn _) (ptSn _) @@ -477,180 +476,6 @@ SuspS¹-inv x = (lUnit _ ∙ ((λ i → cong ∣_∣ₕ (σSn 1 (rCancelS¹ x (~ i)))) ∙ cong (cong ∣_∣ₕ) (rCancel (merid base))) ∙ sym (rCancel _) --------------------- join Sⁿ Sᵐ ≃ Sⁿ⁺¹⁺ᵐ ------------------------- -{- -This section contains a proof that join Sⁿ Sᵐ ≃ Sⁿ⁺ᵐ⁺¹. This is easy using -various properties proved in HITs.Join. However, we would like the map -join Sⁿ Sᵐ → Sⁿ⁺ᵐ⁺¹ -to be nice, in particular when n = m = 1. Therefore, we put in some extra work into -the equivalence. --} - - -{- We begin with join S¹ S¹ ≃ S³. The iso is induced by: -} -S¹×S¹→S² : S¹ → S¹ → S₊ 2 -S¹×S¹→S² base y = north -S¹×S¹→S² (loop i) base = north -S¹×S¹→S² (loop i) (loop j) = - (sym (rCancel (merid base)) - ∙∙ (λ i → merid (loop i) ∙ sym (merid base)) - ∙∙ rCancel (merid base)) i j - -joinS¹S¹→S³ : join S¹ S¹ → S₊ 3 -joinS¹S¹→S³ (inl x) = north -joinS¹S¹→S³ (inr x) = south -joinS¹S¹→S³ (push a b i) = merid (S¹×S¹→S² a b) i - -{- Proving that this is an equivalence directly is painful, - so we simply prove that it is equal to the old definition of - the equivalence join S¹ S¹ ≃ S³ ≃ S₊ 3 - To this end, we start by rephrasing the map -} -private - 3cell : (r i j k : I) → S₊ 3 - 3cell r i j k = - hfill (λ r → λ {(i = i0) → merid (merid base j) (k ∧ ~ r) - ; (i = i1) → merid (merid base j) (k ∧ ~ r) - ; (j = i0) → merid north (k ∧ ~ r) - ; (j = i1) → merid south (k ∧ ~ r) - ; (k = i0) → north - ; (k = i1) → merid (merid base j) (~ r)}) - (inS (merid (merid (loop i) j) k)) - r - -joinS¹S¹→S³' : join S¹ S¹ → S₊ 3 -joinS¹S¹→S³' (inl x) = north -joinS¹S¹→S³' (inr x) = north -joinS¹S¹→S³' (push base b i) = north -joinS¹S¹→S³' (push (loop i₁) base i) = north -joinS¹S¹→S³' (push (loop i₁) (loop i₂) i) = 3cell i1 i₁ i₂ i - -{- These two maps are equal -} -joinS¹S¹→S³'≡joinS¹S¹→S³' : (x : _) → joinS¹S¹→S³ x ≡ joinS¹S¹→S³' x -joinS¹S¹→S³'≡joinS¹S¹→S³' (inl base) = refl -joinS¹S¹→S³'≡joinS¹S¹→S³' (inl (loop i)) = refl -joinS¹S¹→S³'≡joinS¹S¹→S³' (inr base) = sym (merid north) -joinS¹S¹→S³'≡joinS¹S¹→S³' (inr (loop i)) = sym (merid north) -joinS¹S¹→S³'≡joinS¹S¹→S³' (push base base i) k = merid north (~ k ∧ i) -joinS¹S¹→S³'≡joinS¹S¹→S³' (push base (loop i₁) i) k = merid north (~ k ∧ i) -joinS¹S¹→S³'≡joinS¹S¹→S³' (push (loop i₁) base i) k = (merid north) (~ k ∧ i) -joinS¹S¹→S³'≡joinS¹S¹→S³' (push (loop i) (loop j) k) l = - hcomp (λ r → λ { (i = i0) → merid (sym (rCancel (merid base)) (~ r) j) - (~ l ∧ k) - ; (i = i1) → merid (sym (rCancel (merid base)) (~ r) j) - (~ l ∧ k) - ; (j = i0) → merid north (~ l ∧ k) - ; (j = i1) → merid north (~ l ∧ k) - ; (k = i0) → north - ; (k = i1) → merid (sym (rCancel (merid base)) (~ r) j) (~ l) - ; (l = i0) → merid (doubleCompPath-filler - (sym (rCancel (merid base))) - (cong (σSn 1) loop) - (rCancel (merid base)) r i j) k - ; (l = i1) → 3cell i1 i j k}) - (hcomp (λ r → λ {(i = i0) → merid (cp-fill base r j) (k ∧ ~ l) - ; (i = i1) → merid (cp-fill base r j) (k ∧ ~ l) - ; (j = i0) → merid north (~ l ∧ k) - ; (j = i1) → merid (merid base (~ r)) (~ l ∧ k) - ; (k = i0) → north - ; (k = i1) → merid (cp-fill base r j) (~ l) - ; (l = i0) → merid (cp-fill (loop i) r j) k - ; (l = i1) → 3cell i1 i j k}) - (hcomp (λ r → λ {(i = i0) → merid (merid base j) (k ∧ (~ r ∨ ~ l)) - ; (i = i1) → merid (merid base j) (k ∧ (~ r ∨ ~ l)) - ; (j = i0) → merid north (k ∧ (~ l ∨ ~ r)) - ; (j = i1) → merid south (k ∧ (~ l ∨ ~ r)) - ; (k = i0) → north - ; (k = i1) → merid (merid base j) (~ r ∨ ~ l) - ; (l = i0) → merid (merid (loop i) j) k - ; (l = i1) → 3cell r i j k}) - (merid (merid (loop i) j) k))) - where - cp-fill : (a : S¹) → _ - cp-fill a = compPath-filler (merid a) (sym (merid base)) - -{- joinS¹S¹→S³' is equal to the original - equivalence (modulo a flipping of interval variables) -} -joinS¹S¹→S³'Id : (x : join S¹ S¹) - → joinS¹S¹→S³' x ≡ (Iso.fun IsoS³S3 ∘ flip₀₂S³ ∘ joinS¹S¹→S3) x -joinS¹S¹→S³'Id (inl x) = refl -joinS¹S¹→S³'Id (inr x) = refl -joinS¹S¹→S³'Id (push base base i) = refl -joinS¹S¹→S³'Id (push base (loop i₁) i) = refl -joinS¹S¹→S³'Id (push (loop i₁) base i) = refl -joinS¹S¹→S³'Id (push (loop i) (loop j) k) l = - hcomp (λ r → λ {(i = i0) → merid (merid base (j ∧ ~ l)) (~ r ∧ k) - ; (i = i1) → merid (merid base (j ∧ ~ l)) (~ r ∧ k) - ; (j = i0) → merid north (k ∧ ~ r) - ; (j = i1) → merid (merid base (~ l)) (~ r ∧ k) - ; (k = i0) → north - ; (k = i1) → merid (merid base (j ∧ ~ l)) (~ r) - ; (l = i0) → 3cell r i j k - ; (l = i1) → Iso.fun (IsoType→IsoSusp S²IsoSuspS¹) - (meridian-contraction-2 k j i r)}) - (merid (S²Cube i j l) k) - where - S²Cube : Cube {A = S₊ 2} (λ j l → merid base (j ∧ ~ l)) - (λ j l → merid base (j ∧ ~ l)) - (λ i l → north) - (λ i l → merid base (~ l)) - (λ i j → merid (loop i) j) - λ i j → fun S²IsoSuspS¹ (surf j i) - S²Cube i j l = - hcomp (λ r → λ {(i = i0) → merid base (j ∧ (~ l ∨ ~ r)) - ; (i = i1) → merid base (j ∧ (~ l ∨ ~ r)) - ; (j = i0) → north - ; (j = i1) → merid base (~ l ∨ ~ r) - ; (l = i0) → merid (loop i) j - ; (l = i1) → meridian-contraction j i r}) - (merid (loop i) j) - -{-So, finally our map joinS¹S¹→S³ is an iso. We state its inverse explicitly. -} -Iso-joinS¹S¹-S³ : Iso (join S¹ S¹) (S₊ 3) -fun Iso-joinS¹S¹-S³ = joinS¹S¹→S³ -inv Iso-joinS¹S¹-S³ = S³→joinS¹S¹ ∘ flip₀₂S³ ∘ Iso.inv IsoS³S3 -rightInv Iso-joinS¹S¹-S³ x = - joinS¹S¹→S³'≡joinS¹S¹→S³' - ((S³→joinS¹S¹ ∘ flip₀₂S³ ∘ Iso.inv IsoS³S3) x) - ∙∙ joinS¹S¹→S³'Id ((S³→joinS¹S¹ ∘ flip₀₂S³ ∘ Iso.inv IsoS³S3) x) - ∙∙ Iso.leftInv (compIso (invIso IsoS³S3) - (compIso flip₀₂S³Iso (S³IsojoinS¹S¹))) x -leftInv Iso-joinS¹S¹-S³ x = - cong (S³→joinS¹S¹ ∘ flip₀₂S³ ∘ inv IsoS³S3) - (joinS¹S¹→S³'≡joinS¹S¹→S³' x ∙ joinS¹S¹→S³'Id x) - ∙ Iso.rightInv (compIso (invIso IsoS³S3) (compIso flip₀₂S³Iso (S³IsojoinS¹S¹))) x - -{- We now get the full iso Sⁿ * Sᵐ ≃ Sⁿ⁺ᵐ⁺¹ -} -IsoSphereJoin : (n m : ℕ) - → Iso (join (S₊ n) (S₊ m)) (S₊ (suc (n + m))) -IsoSphereJoin zero zero = compIso (invIso Susp-iso-joinBool) (invIso S¹IsoSuspBool) -IsoSphereJoin zero (suc m) = compIso join-comm (invIso Susp-iso-joinBool) -IsoSphereJoin (suc zero) zero = (invIso Susp-iso-joinBool) -IsoSphereJoin (suc zero) (suc zero) = Iso-joinS¹S¹-S³ -IsoSphereJoin (suc zero) (suc (suc m)) = - compIso join-comm - (compIso (compIso (Iso-joinSusp-suspJoin {A = S₊∙ (suc m)} {B = S₊∙ (suc zero)}) - (congSuspIso join-comm)) - (congSuspIso (IsoSphereJoin (suc zero) (suc m)))) -IsoSphereJoin (suc (suc n)) m = - compIso (Iso-joinSusp-suspJoin {A = S₊∙ (suc n)} {B = S₊∙ m}) (congSuspIso (IsoSphereJoin (suc n) m)) - -{- Pointedness holds by refl. - This is due to the explicit definition of Iso-joinSusp-suspJoin -} -IsoSphereJoinPres∙ : (n m : ℕ) - → Iso.fun (IsoSphereJoin n m) (inl (ptSn n)) ≡ ptSn (suc (n + m)) -IsoSphereJoinPres∙ zero zero = refl -IsoSphereJoinPres∙ zero (suc m) = refl -IsoSphereJoinPres∙ (suc zero) zero = refl -IsoSphereJoinPres∙ (suc zero) (suc zero) = refl -IsoSphereJoinPres∙ (suc zero) (suc (suc m)) = refl -IsoSphereJoinPres∙ (suc (suc n)) m = refl - -IsoSphereJoin⁻Pres∙ : (n m : ℕ) - → Iso.inv (IsoSphereJoin n m) (ptSn (suc (n + m))) ≡ inl (ptSn n) -IsoSphereJoin⁻Pres∙ n m = - cong (Iso.inv (IsoSphereJoin n m)) (sym (IsoSphereJoinPres∙ n m)) - ∙ Iso.leftInv (IsoSphereJoin n m) (inl (ptSn n)) - -- Inversion on spheres invSphere : {n : ℕ} → S₊ n → S₊ n invSphere {n = zero} = not @@ -698,120 +523,3 @@ invSphere² (suc (suc n)) = invSusp² ∙∙ (λ i → (σSn 1 (loop i))) ∙∙ (rCancel (merid base))) j i) σ-invSphere (suc n) x = toSusp-invSusp (S₊∙ (suc n)) x - - --- Some facts about the map S¹×S¹→S² --- Todo: generalise to Sⁿ×Sᵐ→Sⁿ⁺ᵐ -S¹×S¹→S²rUnit : (a : S¹) → S¹×S¹→S² a base ≡ north -S¹×S¹→S²rUnit base = refl -S¹×S¹→S²rUnit (loop i) = refl - -S¹×S¹→S²x+x : (x : S¹) → S¹×S¹→S² x x ≡ north -S¹×S¹→S²x+x base = refl -S¹×S¹→S²x+x (loop i) k = lem k i - where - lem : cong₂ S¹×S¹→S² loop loop ≡ refl - lem = cong₂Funct S¹×S¹→S² loop loop - ∙ (λ i → rUnit (cong (λ x → S¹×S¹→S²rUnit x i) loop) (~ i)) - -S¹×S¹→S²-antiComm : (a b : S¹) → S¹×S¹→S² a b ≡ S¹×S¹→S² b (invLooper a) -S¹×S¹→S²-antiComm base base = refl -S¹×S¹→S²-antiComm base (loop i) = refl -S¹×S¹→S²-antiComm (loop i) base = refl -S¹×S¹→S²-antiComm (loop i) (loop j) k = - sym≡flipSquare (λ j i → S¹×S¹→S² (loop i) (loop j)) (~ k) i j - -private - S¹×S¹→S²-Distr-filler : (i : I) - → cong₂ (λ b c → S¹×S¹→S² ((loop i) * b) c) loop loop - ≡ cong (S¹×S¹→S² (loop i)) loop - S¹×S¹→S²-Distr-filler i = - cong₂Funct (λ b c → S¹×S¹→S² ((loop i) * b) c) loop loop - ∙∙ (λ j → cong (λ x → S¹×S¹→S²rUnit (rotLoop x i) j) loop ∙ - cong (λ c → S¹×S¹→S² (loop i) c) loop) - ∙∙ sym (lUnit _) - -S¹×S¹→S²-Distr : (a b : S¹) → S¹×S¹→S² (a * b) b ≡ S¹×S¹→S² a b -S¹×S¹→S²-Distr a base j = S¹×S¹→S² (rUnitS¹ a j) base -S¹×S¹→S²-Distr base (loop i) k = S¹×S¹→S²-Distr-filler i0 k i -S¹×S¹→S²-Distr (loop i₁) (loop i) k = S¹×S¹→S²-Distr-filler i₁ k i - -invSusp∘S¹×S¹→S² : (a b : S¹) - → S¹×S¹→S² a (invLooper b) ≡ invSusp (S¹×S¹→S² a b) -invSusp∘S¹×S¹→S² base b = merid base -invSusp∘S¹×S¹→S² (loop i) base = merid base -invSusp∘S¹×S¹→S² (loop i) (loop j) k = - hcomp (λ r → λ {(i = i0) → i-Boundary₂ r j k - ; (i = i1) → i-Boundary₂ r j k - ; (j = i0) → m-b k - ; (j = i1) → m-b k - ; (k = i0) → doubleCompPath-filler - rCancel-mb⁻¹ (cong σ₁ loop) rCancel-mb r i (~ j) - ; (k = i1) - → invSusp (doubleCompPath-filler - rCancel-mb⁻¹ (cong σ₁ loop) rCancel-mb r i j)}) - (hcomp (λ r → λ {(i = i0) → i-Boundary r (~ j) k - ; (i = i1) → i-Boundary r (~ j) k - ; (j = i0) → merid base (~ r ∨ k) - ; (j = i1) → merid base (r ∧ k) - ; (k = i0) → cp-filler (loop i) r (~ j) - ; (k = i1) → invSusp (cp-filler (loop i) r j)}) - (merid (loop i) (~ j))) - where - σ₁ = σSn 1 - m-b = merid base - rCancel-mb = rCancel m-b - rCancel-mb⁻¹ = sym (rCancel m-b) - - cp-filler : (a : S¹) (i j : I) → S₊ 2 - cp-filler a i j = compPath-filler (merid a) (sym (merid base)) i j - - i-Boundary : I → I → I → S₊ 2 - i-Boundary r j k = - hfill (λ r → λ{(j = i0) → m-b (k ∧ r) - ; (j = i1) → m-b (~ r ∨ k) - ; (k = i0) → cp-filler base r j - ; (k = i1) → invSusp (cp-filler base r (~ j))}) - (inS (m-b j)) - r - - i-Boundary₂ : I → I → I → S₊ 2 - i-Boundary₂ r j k = - hcomp (λ i → λ {(r = i0) → i-Boundary i (~ j) k - ; (r = i1) → m-b k - ; (j = i0) → m-b (k ∨ (~ i ∧ ~ r)) - ; (j = i1) → m-b (k ∧ (i ∨ r)) - ; (k = i0) → rCancel-filler m-b i r (~ j) - ; (k = i1) → invSusp (rCancel-filler m-b i r j) }) - (hcomp (λ i → λ {(r = i0) → m-b (~ j ∨ (~ i ∧ k)) - ; (r = i1) → m-b (k ∨ (~ i ∧ ~ j)) - ; (j = i0) → m-b (k ∨ (~ r ∨ ~ i)) - ; (j = i1) → m-b (k ∧ (~ i ∨ r)) - ; (k = i0) → m-b (~ j ∧ (~ r ∨ ~ i)) - ; (k = i1) → m-b ((~ j ∨ ~ i) ∨ r) }) - (m-b (~ j ∨ k))) - --- Interaction between S¹×S¹→S² and SuspS¹→S² -SuspS¹→S²-S¹×S¹→S² : (a b : S¹) - → (SuspS¹→S² (S¹×S¹→S² a b)) ≡ (S¹×S¹→S²' b a) -SuspS¹→S²-S¹×S¹→S² base base = refl -SuspS¹→S²-S¹×S¹→S² base (loop i) = refl -SuspS¹→S²-S¹×S¹→S² (loop i) base = refl -SuspS¹→S²-S¹×S¹→S² (loop i) (loop j) k = - hcomp (λ r → λ {(i = i0) → rUnit (λ _ → base) (~ r ∧ ~ k) j - ; (i = i1) → rUnit (λ _ → base) (~ r ∧ ~ k) j - ; (j = i0) → base - ; (j = i1) → base - ; (k = i0) → SuspS¹→S² (doubleCompPath-filler ( - sym (rCancel (merid base))) - ((λ i → merid (loop i) ∙ sym (merid base))) - (rCancel (merid base)) r i j ) - ; (k = i1) → surf j i}) - (hcomp (λ r → λ {(i = i0) → rUnit (λ _ → base) (r ∧ ~ k) j - ; (i = i1) → rUnit (λ _ → base) (r ∧ ~ k) j - ; (j = i0) → base - ; (j = i1) → base - ; (k = i0) → SuspS¹→S² - (compPath-filler (merid (loop i)) (sym (merid base)) r j) - ; (k = i1) → surf j i}) - (surf j i)) diff --git a/Cubical/HITs/Susp/Properties.agda b/Cubical/HITs/Susp/Properties.agda index 6c043cf3b9..98f7c2a2ab 100644 --- a/Cubical/HITs/Susp/Properties.agda +++ b/Cubical/HITs/Susp/Properties.agda @@ -378,3 +378,12 @@ toSusp-invSusp A (merid a i) j = λ r → flipSquare (sym (rUnit refl) ◁ (flipSquare (sym (sym≡cong-sym r)) ▷ rUnit refl))) + +-- co-H-space structure +·Susp : ∀ {ℓ'} (A : Pointed ℓ) {B : Pointed ℓ'} + (f g : Susp∙ (typ A) →∙ B) → Susp∙ (typ A) →∙ B +fst (·Susp A {B = B} f g) north = pt B +fst (·Susp A {B = B} f g) south = pt B +fst (·Susp A {B = B} f g) (merid a i) = + (Ω→ f .fst (toSusp A a) ∙ Ω→ g .fst (toSusp A a)) i +snd (·Susp A f g) = refl diff --git a/Cubical/Homotopy/Group/Base.agda b/Cubical/Homotopy/Group/Base.agda index ec0c1f8f4a..4713d97de8 100644 --- a/Cubical/Homotopy/Group/Base.agda +++ b/Cubical/Homotopy/Group/Base.agda @@ -117,12 +117,7 @@ fst (∙Π {A = A} {n = suc zero} (f , p) (g , q)) base = pt A fst (∙Π {A = A} {n = suc zero} (f , p) (g , q)) (loop j) = ((sym p ∙∙ cong f loop ∙∙ p) ∙ (sym q ∙∙ cong g loop ∙∙ q)) j snd (∙Π {A = A} {n = suc zero} (f , p) (g , q)) = refl -fst (∙Π {A = A} {n = suc (suc n)} (f , p) (g , q)) north = pt A -fst (∙Π {A = A} {n = suc (suc n)} (f , p) (g , q)) south = pt A -fst (∙Π {A = A} {n = suc (suc n)} (f , p) (g , q)) (merid a j) = - ((sym p ∙∙ cong f (merid a ∙ sym (merid (ptSn (suc n)))) ∙∙ p) - ∙ (sym q ∙∙ cong g (merid a ∙ sym (merid (ptSn (suc n)))) ∙∙ q)) j -snd (∙Π {A = A} {n = suc (suc n)} (f , p) (g , q)) = refl +∙Π {A = A} {n = suc (suc n)} = ·Susp (S₊∙ (suc n)) -Π : ∀ {ℓ} {A : Pointed ℓ} {n : ℕ} → (S₊∙ n →∙ A) diff --git a/Cubical/Homotopy/Group/Join.agda b/Cubical/Homotopy/Group/Join.agda index e3015ab4c7..0363b836a9 100644 --- a/Cubical/Homotopy/Group/Join.agda +++ b/Cubical/Homotopy/Group/Join.agda @@ -324,3 +324,9 @@ snd (π*∘∙Hom {A = A} {B = B} n m f) = (≃∙→ret/sec∙ {B = _ , ptSn (suc (n + m))} (joinSphereEquiv∙ n m) .fst) ∙ ∘∙-idˡ g))) + +π*∘∙Equiv : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'} + (n m : ℕ) (f : A ≃∙ B) + → GroupEquiv (π*Gr n m A) (π*Gr n m B) +fst (π*∘∙Equiv n m f) = isoToEquiv (setTruncIso (pre∘∙equiv f)) +snd (π*∘∙Equiv n m f) = π*∘∙Hom n m (≃∙map f) .snd diff --git a/Cubical/Homotopy/Group/Pi3S2.agda b/Cubical/Homotopy/Group/Pi3S2.agda index bfde3950ad..119cae49ba 100644 --- a/Cubical/Homotopy/Group/Pi3S2.agda +++ b/Cubical/Homotopy/Group/Pi3S2.agda @@ -25,6 +25,7 @@ open import Cubical.Foundations.Equiv open import Cubical.HITs.SetTruncation renaming (elim to sElim) open import Cubical.HITs.Sn +open import Cubical.HITs.Sn.Multiplication open import Cubical.HITs.Susp open import Cubical.HITs.S1 diff --git a/Cubical/Homotopy/Group/Pi4S3/BrunerieNumber.agda b/Cubical/Homotopy/Group/Pi4S3/BrunerieNumber.agda index b25c4a31a1..e075036948 100644 --- a/Cubical/Homotopy/Group/Pi4S3/BrunerieNumber.agda +++ b/Cubical/Homotopy/Group/Pi4S3/BrunerieNumber.agda @@ -37,6 +37,8 @@ open import Cubical.Data.Int open import Cubical.HITs.S1 open import Cubical.HITs.Sn +open import Cubical.HITs.Sn.Multiplication +open import Cubical.HITs.Join open import Cubical.HITs.Susp open import Cubical.HITs.Wedge open import Cubical.HITs.Pushout @@ -398,21 +400,22 @@ module _ where -- first need the following: fold∘W≡Whitehead : fst (π'∘∙Hom 2 (fold∘W , refl)) ∣ idfun∙ (S₊∙ 3) ∣₂ - ≡ ∣ [ idfun∙ (S₊∙ 2) ∣ idfun∙ (S₊∙ 2) ]₂ ∣₂ + ≡ ∣ [ idfun∙ (S₊∙ 2) ∣ idfun∙ (S₊∙ 2) ] ∣₂ fold∘W≡Whitehead = - pRec (squash₂ _ _) - (cong ∣_∣₂) - (indΠ₃S₂ _ _ - (funExt (λ x → funExt⁻ (sym (cong fst (id∨→∙id {A = S₊∙ 2}))) (W x)))) + cong ∣_∣₂ (ΣPathP (funExt (main ∘ sphere→Join 1 1) , refl)) where - indΠ₃S₂ : ∀ {ℓ} {A : Pointed ℓ} - → (f g : A →∙ S₊∙ 2) - → fst f ≡ fst g → ∥ f ≡ g ∥₁ - indΠ₃S₂ {A = A} f g p = - trRec squash₁ - (λ r → ∣ ΣPathP (p , r) ∣₁) - (isConnectedPathP 1 {A = (λ i → p i (snd A) ≡ north)} - (isConnectedPathSⁿ 1 (fst g (pt A)) north) (snd f) (snd g) .fst ) + main : (x : _) → fold⋁ (joinTo⋁ {A = S₊∙ 1} {B = S₊∙ 1} x) + ≡ fst [ idfun∙ (Susp S¹ , north) + ∣ idfun∙ (Susp S¹ , north) ]-pre x + main (inl x) = refl + main (inr x) = refl + main (push a b i) j = help j i + where + help : cong (fold⋁ ∘ joinTo⋁ {A = S₊∙ 1} {B = S₊∙ 1}) (push a b) + ≡ (σS b ∙ refl) ∙ σS a ∙ refl + help = cong-∙∙ fold⋁ _ _ _ + ∙ doubleCompPath≡compPath _ _ _ + ∙ cong₂ _∙_ (rUnit _) (sym (lUnit (σS a)) ∙ rUnit (σS a)) BrunerieIsoAbstract : GroupEquiv (π'Gr 3 (S₊∙ 3)) (abstractℤGroup/ Brunerie) BrunerieIsoAbstract = @@ -430,12 +433,10 @@ BrunerieIsoAbstract = fst (π'∘∙Hom 2 (fold∘W , refl)) (Iso.inv (fst (πₙ'Sⁿ≅ℤ 2)) 1) ≡ [ ∣ idfun∙ (S₊∙ 2) ∣₂ ∣ ∣ idfun∙ (S₊∙ 2) ∣₂ ]π' - mainPath = - cong (fst (π'∘∙Hom 2 (fold∘W , refl))) + mainPath = cong (fst (π'∘∙Hom 2 (fold∘W , refl))) (cong (Iso.inv (fst (πₙ'Sⁿ≅ℤ 2))) (sym (πₙ'Sⁿ≅ℤ-idfun∙ 2)) ∙ (Iso.leftInv (fst (πₙ'Sⁿ≅ℤ 2)) ∣ idfun∙ (S₊∙ 3) ∣₂)) - ∙ fold∘W≡Whitehead - ∙ cong ∣_∣₂ (sym ([]≡[]₂ (idfun∙ (S₊∙ 2)) (idfun∙ (S₊∙ 2)))) + ∙ fold∘W≡Whitehead main : _ ≡ Brunerie main i = abs (HopfInvariant-π' 0 (mainPath i)) diff --git a/Cubical/Homotopy/Group/Pi4S3/DirectProof.agda b/Cubical/Homotopy/Group/Pi4S3/DirectProof.agda index 41513b68cc..3ebf02c48f 100644 --- a/Cubical/Homotopy/Group/Pi4S3/DirectProof.agda +++ b/Cubical/Homotopy/Group/Pi4S3/DirectProof.agda @@ -18,9 +18,8 @@ complicates things. In this file, we try to work around this problem. The proof goes as follows. 1. Define π₃*(A) := ∥ S¹ * S¹ →∙ A ∥₀ and define explicitly an -addition on this type. Prove that the equivalence π₃(A) ≃ π₃*(A) is -structure preserving, thereby giving a group structure on π₃*(A) and a -group iso π₃*(A) ≅ π₃(A) +addition on this type. This is already done in +Cubical.Homotopy.Group.Join. 2. Under this iso, η gets mapped to η₁ (by construction) defined by S¹ * S¹ -ᵂ→ S² ∨ S² -ᶠᵒˡᵈ→ S² @@ -73,6 +72,7 @@ open import Cubical.Homotopy.Group.Pi4S3.BrunerieNumber open import Cubical.Homotopy.Group.Pi4S3.BrunerieExperiments using (K₂ ; f7' ; S¹∙ ; encodeTruncS²) -- For computation (alternative proof) +open import Cubical.Homotopy.Group.Join open import Cubical.Data.Sigma open import Cubical.Data.Nat @@ -82,6 +82,7 @@ open import Cubical.Data.Int open import Cubical.HITs.S1 as S1 renaming (_·_ to _*_) open import Cubical.HITs.S2 renaming (S¹×S¹→S² to S¹×S¹→S²') open import Cubical.HITs.Sn +open import Cubical.HITs.Sn.Multiplication open import Cubical.HITs.Susp renaming (toSusp to σ) open import Cubical.HITs.Join hiding (joinS¹S¹→S³) open import Cubical.HITs.Wedge @@ -142,231 +143,29 @@ private (IsoSphereJoin 1 1) (isConnectedSubtr 3 1 (sphereConnected 3))) + joinS¹S¹→S³ = join→Sphere 1 1 + S¹×S¹→S² : S¹ → S¹ → S₊ 2 + S¹×S¹→S² = _⌣S_ + -- Key goal: prove that the following element of π₃(S²) gets mapped to -2 η : π' 3 (S₊∙ 2) η = fst (π'∘∙Hom 2 (fold∘W , refl)) ∣ id∙ (S₊∙ 3) ∣₂ -{- Step 1. Define an addition on π₃*(A) := ∥ S¹ * S¹ →∙ A ∥₀ -} --- On the underlying function spaces. -_+join_ : (f g : (join S¹ S¹ , inl base) →∙ A) - → (join S¹ S¹ , inl base) →∙ A -fst (f +join g) (inl x) = fst f (inl x) -fst (f +join g) (inr x) = fst g (inr x) -fst (f +join g) (push a b i) = - (cong (fst f) (push a b ∙ sym (push base b)) - ∙∙ snd f ∙ sym (snd g) - ∙∙ cong (fst g) (push base base ∙∙ sym (push a base) ∙∙ push a b)) i -snd (f +join g) = snd f - --- Homotopy group version -_π₃*+_ : (f g : ∥ (join S¹ S¹ , inl base) →∙ S₊∙ 2 ∥₂) - → ∥ (join S¹ S¹ , inl base) →∙ S₊∙ 2 ∥₂ -_π₃*+_ = sRec2 squash₂ λ x y → ∣ x +join y ∣₂ - --- transferring between π₃ and π₃* --- (homotopy groups defined in terms of S¹ * S¹) -joinify : S₊∙ 3 →∙ A → (join S¹ S¹ , inl base) →∙ A -fst (joinify f) x = fst f (joinS¹S¹→S³ x) -snd (joinify f) = snd f - -disjoin : (join S¹ S¹ , inl base) →∙ A → S₊∙ 3 →∙ A -fst (disjoin f) = λ x → fst f (Iso.inv (IsoSphereJoin 1 1) x) -snd (disjoin f) = snd f - - --- joinify is structure preserving -+join≡∙Π : (f g : S₊∙ 3 →∙ A) - → joinify (∙Π f g) - ≡ (joinify f +join joinify g) -+join≡∙Π f' g' = - ΣPathP ((funExt (λ { (inl x) → sym fp - ; (inr x) → sym gp ∙ cong g (merid north) - ; (push a b i) j → main a b j i})) - , λ i j → fp (j ∨ ~ i)) - where - f = fst f' - g = fst g' - - fp = snd f' - gp = snd g' - - path-lem : ∀ {ℓ} {A : Type ℓ} {x y z w u : A} - (p : x ≡ y) (q : y ≡ z) (r : z ≡ w) (s : w ≡ u) - → (refl ∙∙ p ∙∙ q) ∙ (r ∙∙ s ∙∙ refl) - ≡ (p ∙∙ (q ∙ r) ∙∙ s) - path-lem p q r s = - cong ((p ∙ q) ∙_) (sym (compPath≡compPath' r s)) - ∙∙ sym (∙assoc p q (r ∙ s)) - ∙∙ cong (p ∙_) (∙assoc q r s) - ∙ sym (doubleCompPath≡compPath p (q ∙ r) s) - - main-helper : (a b : S¹) - → Square ((refl ∙∙ cong f (σ₂ (S¹×S¹→S² a b)) ∙∙ fp) - ∙ (sym gp ∙∙ cong g (σ₂ (S¹×S¹→S² a b)) ∙∙ refl)) - ((cong f (merid (S¹×S¹→S² a b)) - ∙ sym (cong f (merid north))) - ∙∙ (fp ∙ sym gp) - ∙∙ cong g (merid (S¹×S¹→S² a b))) - (λ _ → f north) - (cong g (merid north)) - main-helper a b = - path-lem (cong f (σ₂ (S¹×S¹→S² a b))) fp (sym gp) - (cong g (σ₂ (S¹×S¹→S² a b))) - ◁ lem - where - lem : PathP (λ i → f north ≡ cong g (merid north) i) - ((λ i → f (σ₂ (S¹×S¹→S² a b) i)) - ∙∙ fp ∙ (sym gp) ∙∙ - (cong g (σ₂ (S¹×S¹→S² a b)))) - ((cong f (merid (S¹×S¹→S² a b)) ∙ sym (cong f (merid north))) - ∙∙ fp ∙ sym gp - ∙∙ cong g (merid (S¹×S¹→S² a b))) - lem i j = - hcomp (λ k → λ { (i = i0) → - (cong-∙ f (merid (S¹×S¹→S² a b)) - (sym (merid north)) (~ k) - ∙∙ fp ∙ sym gp - ∙∙ (λ i → g (σ-filler (S¹×S¹→S² a b) north k i))) j - ; (i = i1) → ((cong f (merid (S¹×S¹→S² a b)) - ∙ sym (cong f (merid north))) - ∙∙ (fp ∙ sym gp) - ∙∙ cong g (merid (S¹×S¹→S² a b))) j - ; (j = i0) → f north - ; (j = i1) → g (merid north (~ k ∨ i))}) - (((cong f (merid (S¹×S¹→S² a b)) ∙ sym (cong f (merid north))) - ∙∙ (fp ∙ sym gp) - ∙∙ cong g (merid (S¹×S¹→S² a b))) j) - - - main-helper₂ : (a b : S¹) - → cong (fst (joinify g')) (push base base ∙∙ sym (push a base) ∙∙ push a b) - ≡ cong g (merid (S¹×S¹→S² a b)) - main-helper₂ a b = cong-∙∙ (fst (joinify g')) - (push base base) (sym (push a base)) (push a b) - ∙ cong (cong g (merid north) ∙∙_∙∙ cong g (merid (S¹×S¹→S² a b))) - (cong (cong g) (cong sym (cong merid (S¹×S¹→S²rUnit a)))) - ∙ ((λ i → (cong g (λ j → merid north (j ∧ ~ i))) - ∙∙ (cong g (λ j → merid north (~ j ∧ ~ i))) - ∙∙ cong g (merid (S¹×S¹→S² a b))) - ∙ sym (lUnit (cong g (merid (S¹×S¹→S² a b))))) - - main : (a b : S¹) - → PathP (λ i → fp (~ i) ≡ (sym gp ∙ cong g (merid north)) i) - ((sym fp ∙∙ cong f (σ₂ (S¹×S¹→S² a b)) ∙∙ fp) - ∙ (sym gp ∙∙ cong g (σ₂ (S¹×S¹→S² a b)) ∙∙ gp)) - ((cong (fst (joinify f')) (push a b ∙ sym (push base b)) - ∙∙ fp ∙ sym gp - ∙∙ cong (fst (joinify g')) - (push base base ∙∙ sym (push a base) ∙∙ push a b))) - main a b = - ((λ i j → hcomp (λ k → λ {(i = i0) → (((λ j → fp (~ j ∧ k)) - ∙∙ cong f (σ₂ (S¹×S¹→S² a b)) - ∙∙ fp) - ∙ (sym gp - ∙∙ cong g (σ₂ (S¹×S¹→S² a b)) - ∙∙ λ j → gp (j ∧ k))) j - ; (i = i1) → ((cong f (merid (S¹×S¹→S² a b)) - ∙ sym (cong f (merid north))) - ∙∙ fp ∙ sym gp - ∙∙ cong g (merid (S¹×S¹→S² a b))) j - ; (j = i0) → fp (~ i ∧ k) - ; (j = i1) → compPath-filler' - (sym gp) (cong g (merid north)) k i}) - (main-helper a b i j))) - ▷ λ i → - cong-∙ (fst (joinify f')) (push a b) (sym (push base b)) (~ i) - ∙∙ fp ∙ sym gp - ∙∙ main-helper₂ a b (~ i) - - - --- Group structure on π₃* --- todo: remove connectivity assumption -module _ (A : Pointed ℓ) (con : (isConnected 3 (typ A))) where - π₃*Iso : Iso (typ (π'Gr 2 A)) ∥ (join S¹ S¹ , inl base) →∙ A ∥₂ - fun π₃*Iso = sMap joinify - inv π₃*Iso = sMap disjoin - rightInv π₃*Iso = - sElim (λ _ → isSetPathImplicit) - λ f → to3ConnectedId - con (funExt λ x → cong (fst f) (Iso.leftInv (IsoSphereJoin 1 1) x)) - leftInv π₃*Iso = - sElim (λ _ → isSetPathImplicit) - λ f → to3ConnectedId - con (funExt (λ x → cong (fst f) (Iso.rightInv (IsoSphereJoin 1 1) x))) - - π₃* : Group ℓ - π₃* = InducedGroupFromPres· - (π'Gr 2 A) - (sRec2 squash₂ (λ x y → ∣ x +join y ∣₂)) - (isoToEquiv π₃*Iso) - (sElim2 (λ _ _ → isSetPathImplicit) (λ f g → cong ∣_∣₂ (+join≡∙Π f g))) - - π₃≅π₃* : GroupEquiv (π'Gr 2 A) π₃* - π₃≅π₃* = - InducedGroupEquivFromPres· (π'Gr 2 A) (sRec2 squash₂ (λ x y → ∣ x +join y ∣₂)) - (isoToEquiv π₃*Iso) - (sElim2 (λ _ _ → isSetPathImplicit) (λ f g → cong ∣_∣₂ (+join≡∙Π f g))) - - --- Induced homomorphisms (A →∙ B) → (π₃*(A) → π₃*(B)) --- todo: remove connectivity assumptions -module _ (conA : (isConnected 3 (typ A))) (conB : (isConnected 3 (typ B))) - (f : A →∙ B) where - postCompπ₃* : GroupHom (π₃* A conA) (π₃* B conB) - fst postCompπ₃* = sMap (f ∘∙_) - snd postCompπ₃* = - makeIsGroupHom - (sElim2 (λ _ _ → isSetPathImplicit) - λ h g → to3ConnectedId conB - (funExt λ { (inl x) → refl - ; (inr x) → refl - ; (push a b i) j → - (cong-∙∙ (fst f) - (cong (fst h) ((push a b ∙ (sym (push base b))))) - (snd h ∙ (sym (snd g))) - (cong (fst g) ((push base base - ∙∙ (sym (push a base)) - ∙∙ push a b))) - ∙ cong (cong (fst f) - (cong (fst h) (push a b ∙ (sym (push base b)))) - ∙∙_∙∙ - cong (fst f ∘ fst g) - ((push base base ∙∙ (sym (push a base)) ∙∙ push a b))) - (cong-∙ (fst f) (snd h) (sym (snd g)) - ∙ λ j → compPath-filler (cong (fst f) (snd h)) (snd f) j - ∙ sym (compPath-filler - (cong (fst f) (snd g)) (snd f) j))) j i})) - --- Induced iso (A ≃∙ B) → π₃*(A) ≅ π₃*(B) --- todo: remove connectivity assumptions -module _ (conA : (isConnected 3 (typ A))) (conB : (isConnected 3 (typ B))) - (f : A ≃∙ B) where - postCompπ₃*Equiv : GroupEquiv (π₃* A conA) (π₃* B conB) - fst postCompπ₃*Equiv = isoToEquiv h - where - h : Iso (π₃* A conA .fst) (π₃* B conB .fst) - fun h = fst (postCompπ₃* conA conB (≃∙map f)) - inv h = fst (postCompπ₃* conB conA (≃∙map (invEquiv∙ f))) - rightInv h = - sElim (λ _ → isSetPathImplicit) - λ g → to3ConnectedId conB (funExt λ x → secEq (fst f) (fst g x)) - leftInv h = - sElim (λ _ → isSetPathImplicit) - λ g → to3ConnectedId conA (funExt λ x → retEq (fst f) (fst g x)) - snd postCompπ₃*Equiv = snd (postCompπ₃* conA conB (≃∙map f)) -- The relevant groups (in order of the iso π₃(S²) ≅ ℤ) π₃S² = π'Gr 2 (S₊∙ 2) -π₃*S² = π₃* (S₊∙ 2) (sphereConnected 2) +π₃*S² = π*Gr 1 1 (S₊∙ 2) -π₃*joinS¹S¹ = π₃* (join S¹ S¹ , inl base) con-joinS¹S¹ +π₃*joinS¹S¹ = π*Gr 1 1 (join∙ (S₊∙ 1) (S₊∙ 1)) -π₃*S³ = π₃* (S₊∙ 3) connS³ +π₃*S³ = π*Gr 1 1 (S₊∙ 3) π₃S³ = π'Gr 2 (S₊∙ 3) +π₃≅π₃* : {A : Pointed₀} → GroupEquiv (π'Gr 2 A) (π*Gr 1 1 A) +π₃≅π₃* {A = A} = invGroupEquiv (GroupIso→GroupEquiv (π*Gr≅π'Gr 1 1 A)) + {- Goal now: Show that (η : π₃(S²)) ↦ (η₁ : π₃*(S²)) @@ -383,13 +182,13 @@ Hence, there is an is an iso π₃(S²) ≅ ℤ taking η to -} -- Underlying functions of (some of) the ηs -η₁-raw : (join S¹ S¹ , inl base) →∙ S₊∙ 2 +η₁-raw : join∙ S¹∙ S¹∙ →∙ S₊∙ 2 fst η₁-raw (inl x) = north fst η₁-raw (inr x) = north fst η₁-raw (push a b i) = (σ₁ b ∙ σ₁ a) i snd η₁-raw = refl -η₂-raw : (join S¹ S¹ , inl base) →∙ (join S¹ S¹ , inl base) +η₂-raw : join∙ S¹∙ S¹∙ →∙ join∙ S¹∙ S¹∙ fst η₂-raw (inl x) = inr (invLooper x) fst η₂-raw (inr x) = inr x fst η₂-raw (push a b i) = @@ -397,7 +196,7 @@ fst η₂-raw (push a b i) = ∙ push (b * invLooper a) b) i snd η₂-raw = sym (push base base) -η₃-raw : (join S¹ S¹ , inl base) →∙ S₊∙ 3 +η₃-raw : join∙ S¹∙ S¹∙ →∙ S₊∙ 3 fst η₃-raw (inl x) = north fst η₃-raw (inr x) = north fst η₃-raw (push a b i) = @@ -420,7 +219,7 @@ snd η₃-raw = refl -- π₃S²≅π₃*S² π₃S²→π₃*S² : GroupEquiv π₃S² π₃*S² -π₃S²→π₃*S² = π₃≅π₃* (S₊∙ 2) (sphereConnected 2) +π₃S²→π₃*S² = GroupIso→GroupEquiv (invGroupIso (π*Gr≅π'Gr 1 1 (S₊∙ 2))) -- Time for π₃*(S¹ * S¹) ≅ π₃*S². -- We have this iso already, but slightly differently stated, @@ -433,9 +232,7 @@ Hopfσ (inr x) = north Hopfσ (push a b i) = σ₁ (invLooper a * b) i π₃*joinS¹S¹→π₃*S² : GroupHom π₃*joinS¹S¹ π₃*S² -π₃*joinS¹S¹→π₃*S² = - postCompπ₃* con-joinS¹S¹ (sphereConnected 2) - (Hopfσ , refl) +π₃*joinS¹S¹→π₃*S² = π*∘∙Hom 1 1 (Hopfσ , refl) π₃*joinS¹S¹≅π₃*S² : GroupEquiv π₃*joinS¹S¹ π₃*S² fst (fst π₃*joinS¹S¹≅π₃*S²) = fst π₃*joinS¹S¹→π₃*S² @@ -444,8 +241,7 @@ snd (fst π₃*joinS¹S¹≅π₃*S²) = where π₃*joinS¹S¹→π₃*S²' : GroupHom π₃*joinS¹S¹ π₃*S² π₃*joinS¹S¹→π₃*S²' = - postCompπ₃* con-joinS¹S¹ (sphereConnected 2) - (fst ∘ JoinS¹S¹→TotalHopf , refl) + π*∘∙Hom 1 1 (fst ∘ JoinS¹S¹→TotalHopf , refl) isEquivπ₃*joinS¹S¹→π₃*S²' : isEquiv (fst π₃*joinS¹S¹→π₃*S²') isEquivπ₃*joinS¹S¹→π₃*S²' = @@ -458,10 +254,10 @@ snd (fst π₃*joinS¹S¹≅π₃*S²) = (λ i → GroupHom (GroupPath π₃*joinS¹S¹ π₃S³ .fst (compGroupEquiv - (invGroupEquiv (π₃≅π₃* (join S¹ S¹ , inl base) con-joinS¹S¹)) + (invGroupEquiv π₃≅π₃*) (π'Iso 2 (isoToEquiv (IsoSphereJoin 1 1) , refl))) i) (GroupPath π₃*S² π₃S² .fst - (invGroupEquiv (π₃≅π₃* (S₊∙ 2) (sphereConnected 2))) i)) + (invGroupEquiv π₃≅π₃*) i)) π₃*joinS¹S¹→π₃*S²' (fst (fst GrEq) , snd GrEq) help = @@ -469,20 +265,21 @@ snd (fst π₃*joinS¹S¹≅π₃*S²) = (funExt λ f → (λ i → transportRefl - ((invGroupEquiv (π₃≅π₃* (S₊∙ 2) (sphereConnected 2))) .fst .fst + ((invGroupEquiv (π₃≅π₃*)) .fst .fst (fst π₃*joinS¹S¹→π₃*S²' ( - ((fst (fst (π₃≅π₃* (join S¹ S¹ , inl base) con-joinS¹S¹))) + ((fst (fst π₃≅π₃*)) (invEq (fst (π'Iso 2 (isoToEquiv (IsoSphereJoin 1 1) , refl))) (transportRefl f i)))))) i) - ∙ main f)) + ∙ main f + )) where - main : (f : _) → invEquiv (fst (π₃≅π₃* (S₊∙ 2) (sphereConnected 2))) .fst - (fst π₃*joinS¹S¹→π₃*S²' - (invEq - (invEquiv (fst (π₃≅π₃* (join S¹ S¹ , inl base) con-joinS¹S¹))) - (invEq (fst (π'Iso 2 (isoToEquiv Iso-joinS¹S¹-S³ , (λ _ → north)))) - f))) + main : (f : _) → invEquiv (fst π₃≅π₃*) .fst + (fst π₃*joinS¹S¹→π₃*S²' + (fst (fst π₃≅π₃*) + (invEq + (fst (π'Iso 2 (isoToEquiv (IsoSphereJoin 1 1) , (λ _ → north)))) + f))) ≡ fst GrEq .fst f main = sElim (λ _ → isSetPathImplicit) λ f → to3ConnectedId (sphereConnected 2) @@ -509,13 +306,11 @@ snd π₃*joinS¹S¹≅π₃*S² = snd π₃*joinS¹S¹→π₃*S² -- π₃*(S³) ≅ π₃*(S¹ * S¹) π₃*S³≅π₃*joinS¹S¹ : GroupEquiv π₃*S³ π₃*joinS¹S¹ π₃*S³≅π₃*joinS¹S¹ = - postCompπ₃*Equiv - connS³ con-joinS¹S¹ - (isoToEquiv (invIso (IsoSphereJoin 1 1)) , refl) + π*∘∙Equiv 1 1 (isoToEquiv (invIso (IsoSphereJoin 1 1)) , refl) -- π₃(S³)≅π₃*(S³) π₃S³≅π₃*S³ : GroupEquiv π₃S³ π₃*S³ -π₃S³≅π₃*S³ = π₃≅π₃* (S₊∙ 3) connS³ +π₃S³≅π₃*S³ = π₃≅π₃* η↦η₁ : fst (fst π₃S²→π₃*S²) η ≡ η₁ η↦η₁ = to3ConnectedId (sphereConnected 2) @@ -576,42 +371,27 @@ snd π₃*joinS¹S¹≅π₃*S² = snd π₃*joinS¹S¹→π₃*S² η₂↦η₃ : invEq (fst π₃*S³≅π₃*joinS¹S¹) η₂ ≡ η₃ η₂↦η₃ = to3ConnectedId connS³ - (funExt λ x → sym (joinS¹S¹→S³σ≡ (fst η₂-raw x)) - ∙ lem x) + (funExt λ x → lem x) where - joinS¹S¹→S³σ : join S¹ S¹ → S₊ 3 - joinS¹S¹→S³σ (inl x) = north - joinS¹S¹→S³σ (inr x) = north - joinS¹S¹→S³σ (push a b i) = σ₂ (S¹×S¹→S² a b) i - - joinS¹S¹→S³σ≡ : (x : _) → joinS¹S¹→S³σ x ≡ joinS¹S¹→S³ x - joinS¹S¹→S³σ≡ (inl x) = refl - joinS¹S¹→S³σ≡ (inr x) = merid north - joinS¹S¹→S³σ≡ (push a b i) j = - compPath-filler (merid (S¹×S¹→S² a b)) (sym (merid north)) (~ j) i - - lem : (x : _) → joinS¹S¹→S³σ (fst η₂-raw x) ≡ fst η₃-raw x + lem : (x : _) → joinS¹S¹→S³ (fst η₂-raw x) ≡ fst η₃-raw x lem (inl x) = refl lem (inr x) = refl lem (push a b i) j = main j i where left-lem : σ₂ (S¹×S¹→S² (b * invLooper a) (invLooper a)) ≡ σ₂ (S¹×S¹→S² a b) - left-lem = cong σ₂ (S¹×S¹→S²-Distr b (invLooper a) - ∙ sym (S¹×S¹→S²-antiComm a b)) + left-lem = cong σ₂ (⌣₁,₁-distr' b (invLooper a) + ∙ ⌣Sinvᵣ b a + ∙ sym (transportRefl _) + ∙ sym (comm⌣S a b)) right-lem : σ₂ (S¹×S¹→S² (b * invLooper a) b) ≡ sym (σ₂ (S¹×S¹→S² a b)) - right-lem = - cong σ₂ ((cong (λ x → S¹×S¹→S² x b) (commS¹ b (invLooper a)) - ∙ S¹×S¹→S²-Distr (invLooper a) b) - ∙∙ S¹×S¹→S²-antiComm (invLooper a) b - ∙∙ invSusp∘S¹×S¹→S² b (invLooper a)) - ∙∙ σ-invSphere 1 (S¹×S¹→S² b (invLooper a)) - ∙∙ cong (sym ∘ σ₂) (sym (S¹×S¹→S²-antiComm a b)) - - main : cong (joinS¹S¹→S³σ ∘ fst η₂-raw) (push a b) + right-lem = cong σ₂ (⌣₁,₁-distr (invLooper a) b ∙ ⌣Sinvₗ a b) + ∙ σ-invSphere 1 (a ⌣S b) + + main : cong (joinS¹S¹→S³ ∘ fst η₂-raw) (push a b) ≡ sym (σ₂ (S¹×S¹→S² a b)) ∙ sym (σ₂ (S¹×S¹→S² a b)) - main = cong-∙ joinS¹S¹→S³σ + main = cong-∙ joinS¹S¹→S³ (sym (push (b * invLooper a) (invLooper a))) (push (b * invLooper a) b) ∙ cong₂ _∙_ (cong sym left-lem) right-lem @@ -640,7 +420,15 @@ snd π₃*joinS¹S¹≅π₃*S² = snd π₃*joinS¹S¹→π₃*S² to3ConnectedId connS³ (funExt λ { (inl x) → refl ; (inr x) → refl - ; (push a b i) → refl}) + ; (push a b i) j → help a b j i + }) + where + help : (a b : S¹) + → cong (fst (inv (Iso-JoinMap-SphereMap 1 1) (-Π (idfun∙ (S₊∙ 3))))) (push a b) + ≡ σS (a ⌣S b) ⁻¹ + help a b = cong-∙ (fst (-Π (idfun∙ (S₊∙ 3)))) (merid (a ⌣S b)) (merid north ⁻¹) + ∙ cong₂ _∙_ refl (rCancel (merid north)) + ∙ sym (rUnit (σS (a ⌣S b) ⁻¹)) η₃/2+η₃/2≡η₃ : η₃/2 +π₃* η₃/2 ≡ η₃ η₃/2+η₃/2≡η₃ = @@ -649,23 +437,21 @@ snd π₃*joinS¹S¹≅π₃*S² = snd π₃*joinS¹S¹→π₃*S² ; (inr x) → refl ; (push a b i) → λ j → lem a b j i}) where - lem : (a b : S¹) → cong (fst (η₃-raw/2 +join η₃-raw/2)) (push a b) + pre : (a b : S¹) → cong (fst η₃-raw/2) (ℓS a b) ≡ σS (a ⌣S b) ⁻¹ + pre a b = cong-∙ (fst η₃-raw/2) _ _ + ∙ cong₂ _∙_ + (cong sym (rCancel (merid north))) + (cong-∙∙ (fst η₃-raw/2) _ _ _ + ∙ (λ i → + (cong σ₂ (IdL⌣S {n = 1} {1} a) ∙ (rCancel (merid north))) i + ∙∙ σS (a ⌣S b) ⁻¹ + ∙∙ rCancel (merid north) i) + ∙ sym (rUnit _)) + ∙ sym (lUnit _) + + lem : (a b : S¹) → cong (fst (η₃-raw/2 +* η₃-raw/2)) (push a b) ≡ cong (fst η₃-raw) (push a b) - lem a b = (λ i → cong-∙ (fst η₃-raw/2) (push a b) (sym (push base b)) i - ∙∙ rUnit refl (~ i) - ∙∙ cong-∙∙ (fst η₃-raw/2) - (push base base) (sym (push a base)) (push a b) i) - ∙∙ (λ i → (sym (σ₂ (S¹×S¹→S² a b)) ∙ rCancel (merid north) i) - ∙∙ refl - ∙∙ (sym (rCancel (merid north) i) - ∙∙ (cong σ₂ (S¹×S¹→S²rUnit a) ∙ rCancel (merid north)) i - ∙∙ sym (σ₂ (S¹×S¹→S² a b)))) - ∙∙ ((λ i → rUnit (sym (σ₂ (S¹×S¹→S² a b))) (~ i) - ∙∙ refl - ∙∙ lUnit (sym (σ₂ (S¹×S¹→S² a b))) (~ i)) - ∙ λ i → (λ j → σ₂ (S¹×S¹→S² a b) (i ∨ ~ j)) - ∙∙ (λ j → σ₂ (S¹×S¹→S² a b) (i ∧ ~ j)) - ∙∙ sym (σ₂ (S¹×S¹→S² a b))) + lem a b = cong₂ _∙_ (sym (rUnit _) ∙ pre a b) (sym (rUnit _) ∙ pre a b) -- Agda is very keen on expanding things, so we make an abstract -- summary of the main lemmas above @@ -789,7 +575,7 @@ snd connSuspS² = λ i j → ∣ merid base (i ∧ j) ∣ₕ π₃*S³' : Group₀ -π₃*S³' = π₃* (Susp∙ S²) (isConnectedSubtr 3 1 connSuspS²) +π₃*S³' = π*Gr 1 1 (Susp∙ S²) -- The version of η₃ we have been able to compute lies in π₃*S³' η₃'-raw : (join S¹ S¹ , inl base) →∙ (Susp S² , north) @@ -802,10 +588,13 @@ snd η₃'-raw = refl η₃' : π₃*S³' .fst η₃' = ∣ η₃'-raw ∣₂ +altS²IsoSuspS¹ : Iso S² SuspS¹ +altS²IsoSuspS¹ = compIso invS²Iso S²IsoSuspS¹ + -- We first have to show (manually) that the following iso sends η₃ to η₃' π₃*S³≅π₃*S³' : GroupEquiv π₃*S³ π₃*S³' -π₃*S³≅π₃*S³' = postCompπ₃*Equiv _ _ - (isoToEquiv (congSuspIso (invIso S²IsoSuspS¹)) +π₃*S³≅π₃*S³' = π*∘∙Equiv 1 1 -- _ _ -- postCompπ₃*Equiv _ _ + (isoToEquiv (congSuspIso (invIso altS²IsoSuspS¹)) , refl) π₃*S³≅π₃*S³'-pres-η₃ : fst (fst π₃*S³≅π₃*S³') η₃ ≡ η₃' @@ -813,21 +602,24 @@ snd η₃'-raw = refl cong ∣_∣₂ (ΣPathP ((funExt (λ { (inl x) → refl ; (inr x) → refl - ; (push a b i) j → lem a b j i})) + ; (push a b i) j → lem a b j i + })) , sym (rUnit refl))) where lem : (a b : S¹) - → cong (suspFun SuspS¹→S²) + → cong (suspFun (invS² ∘ SuspS¹→S²)) (sym (σ₂ (S¹×S¹→S² a b)) ∙ sym (σ₂ (S¹×S¹→S² a b))) - ≡ (σ (S² , base) (S¹×S¹→S²' a b) ∙ σ (S² , base) (S¹×S¹→S²' a b)) + ≡ (σ (S² , base) (S¹×S¹→S²' a b) ∙ (σ (S² , base) (S¹×S¹→S²' a b))) lem a b = - cong-∙ (suspFun SuspS¹→S²) + cong-∙ (suspFun (invS² ∘ SuspS¹→S²)) (sym (σ₂ (S¹×S¹→S² a b))) (sym (σ₂ (S¹×S¹→S² a b))) ∙ cong (λ x → x ∙ x) (cong sym (cong-∙ - (suspFun SuspS¹→S²) (merid (S¹×S¹→S² a b)) (sym (merid north))) - ∙ cong sym (cong (σ S²∙) (SuspS¹→S²-S¹×S¹→S² a b)) - ∙ sym (S¹×S¹→S²-sym a b)) + (suspFun (invS² ∘ SuspS¹→S²)) (merid (S¹×S¹→S² a b)) (sym (merid north))) + ∙ cong sym (cong (σ S²∙) + (cong invS² (SuspS¹→S²-S¹×S¹→S² a b) + ∙ S¹×S¹→S²-anticomm a b)) + ∙ sym (S¹×S¹→S²-sym a b)) -- After this, we want to establish an iso π₃*S³'≅ℤ which is nice enough to compute. -- This requires a bit of work and some hacking. @@ -942,26 +734,28 @@ snd π₁S¹→∙ΩS³'≅π₃*S³' = λ f g → cong ∣_∣₂ (ΣPathP ((funExt (λ { (inl x) → refl ; (inr x) → refl - ; (push a b i) j → main f g a b j i})) + ; (push a b i) j → main f g a b j i + })) , refl))) + where + lem1 : (f : S₊∙ 1 →∙ (S₊∙ 1 →∙ Ω (Susp∙ S²) ∙)) (a b : S¹) + → congS (fst (map← f)) (ℓ* S¹∙ S¹∙ a b) ≡ fst f a .fst b + lem1 f a b = cong-∙ (fst (map← f)) _ _ + ∙ cong₂ _∙_ (fst f base .snd) + ((cong-∙∙ (fst (map← f)) _ _ _) + ∙ (λ j → sym (fst f a .snd j) + ∙∙ fst f a .fst b + ∙∙ sym (snd f j .fst b)) + ∙ sym (rUnit _)) + ∙ sym (lUnit _) + main : (f g : S₊∙ 1 →∙ (S₊∙ 1 →∙ Ω (Susp∙ S²) ∙)) (a b : S¹) → cong (fst (map← (∙Π f g))) (push a b) - ≡ cong (fst (map← f +join map← g)) (push a b) - main f g a b = (main-lem a b - ∙ (λ i → (λ j → fst f a .fst b (j ∧ i)) - ∙∙ ((λ j → fst f a .fst b (j ∨ i))) - ∙∙ fst g a .fst b)) - ∙ λ i → (rUnit (fst f a .fst b) ∙ cong (fst f a .fst b ∙_) - (cong sym (sym (funExt⁻ (cong fst (snd f)) b))) - ∙ sym (cong-∙ (map← f .fst) (push a b) (sym (push base b)))) i - ∙∙ rUnit refl i - ∙∙ ((lUnit (fst g a .fst b) - ∙ (λ i → fst g base .snd (~ i) - ∙∙ sym (fst g a .snd (~ i)) - ∙∙ cong (map← g .fst) (push a b))) - ∙ (sym (cong-∙∙ (map← g .fst) - (push base base) (sym (push a base)) (push a b)))) i + ≡ cong (fst (_+*_ {A = S¹∙} {B = S¹∙} (map← f) (map← g))) (push a b) + main f g a b = main-lem a b + ∙ cong₂ _∙_ (sym (lem1 f a b) ∙ rUnit _) + (sym (lem1 g a b) ∙ rUnit _) where JLem : ∀ {ℓ} {A : Type ℓ} (* : A) (fab : * ≡ *) (fabrefl : refl ≡ fab) diff --git a/Cubical/Homotopy/Hopf.agda b/Cubical/Homotopy/Hopf.agda index acb0dbb140..061b4d9fb6 100644 --- a/Cubical/Homotopy/Hopf.agda +++ b/Cubical/Homotopy/Hopf.agda @@ -19,7 +19,7 @@ open import Cubical.Data.Int hiding (_·_) open import Cubical.HITs.Pushout.Flattening open import Cubical.HITs.Pushout -open import Cubical.HITs.Sn hiding (joinS¹S¹→S³) +open import Cubical.HITs.Sn open import Cubical.HITs.Susp open import Cubical.HITs.S1 open import Cubical.HITs.S2 diff --git a/Cubical/Homotopy/HopfInvariant/Brunerie.agda b/Cubical/Homotopy/HopfInvariant/Brunerie.agda index 7d7a13d504..2ebb7d472f 100644 --- a/Cubical/Homotopy/HopfInvariant/Brunerie.agda +++ b/Cubical/Homotopy/HopfInvariant/Brunerie.agda @@ -391,8 +391,7 @@ Brunerie'≡2 = BrunerieNumLem.main (Hⁿ⁺ᵐ-Sⁿ×Sᵐ≅ℤ-abs 1 1) Hⁿ -- number in Brunerie (2016) Brunerie'≡Brunerie : [ ∣ idfun∙ (S₊∙ 2) ∣₂ ∣ ∣ idfun∙ (S₊∙ 2) ∣₂ ]π' ≡ ∣ fold∘W , refl ∣₂ Brunerie'≡Brunerie = - cong ∣_∣₂ ([]≡[]₂ (idfun∙ (S₊∙ 2)) (idfun∙ (S₊∙ 2)) ) - ∙ sym fold∘W≡Whitehead + sym fold∘W≡Whitehead ∙ cong ∣_∣₂ (∘∙-idˡ (fold∘W , refl)) -- And we get the main result diff --git a/Cubical/Homotopy/HopfInvariant/HopfMap.agda b/Cubical/Homotopy/HopfInvariant/HopfMap.agda index d6dd589af1..4f01dc2f75 100644 --- a/Cubical/Homotopy/HopfInvariant/HopfMap.agda +++ b/Cubical/Homotopy/HopfInvariant/HopfMap.agda @@ -48,6 +48,7 @@ open import Cubical.HITs.Pushout as Pushout open import Cubical.HITs.Join open import Cubical.HITs.S1 renaming (_·_ to _*_) open import Cubical.HITs.Sn +open import Cubical.HITs.Sn.Multiplication open import Cubical.HITs.Susp open import Cubical.HITs.Truncation renaming (rec to trRec ; elim to trElim) diff --git a/Cubical/Homotopy/Whitehead.agda b/Cubical/Homotopy/Whitehead.agda index 2daec9e530..fbdffd6ed4 100644 --- a/Cubical/Homotopy/Whitehead.agda +++ b/Cubical/Homotopy/Whitehead.agda @@ -15,6 +15,7 @@ open import Cubical.Data.Unit open import Cubical.HITs.Susp renaming (toSusp to σ) open import Cubical.HITs.Pushout open import Cubical.HITs.Sn +open import Cubical.HITs.Sn.Multiplication open import Cubical.HITs.Join open import Cubical.HITs.Wedge open import Cubical.HITs.SetTruncation @@ -25,6 +26,25 @@ open import Cubical.Homotopy.Loopspace open Iso open 3x3-span +-- Whitehead product (main definition) +[_∣_]-pre : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ} + → (S₊∙ (suc n) →∙ X) + → (S₊∙ (suc m) →∙ X) + → join∙ (S₊∙ n) (S₊∙ m) →∙ X +fst ([_∣_]-pre {X = X} {n = n} {m = m} f g) (inl x) = pt X +fst ([_∣_]-pre {X = X} {n = n} {m = m} f g) (inr x) = pt X +fst ([_∣_]-pre {n = n} {m = m} f g) (push a b i) = + (Ω→ g .fst (σS b) ∙ Ω→ f .fst (σS a)) i +snd ([_∣_]-pre {n = n} {m = m} f g) = refl + +[_∣_] : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ} + → (S₊∙ (suc n) →∙ X) + → (S₊∙ (suc m) →∙ X) + → S₊∙ (suc (n + m)) →∙ X +[_∣_] {n = n} {m = m} f g = + [ f ∣ g ]-pre ∘∙ (sphere→Join n m , IsoSphereJoin⁻Pres∙ n m) + +-- Whitehead product (as a composition) joinTo⋁ : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'} → join (typ A) (typ B) → (Susp (typ A) , north) ⋁ (Susp (typ B) , north) @@ -35,63 +55,100 @@ joinTo⋁ {A = A} {B = B} (push a b i) = ∙∙ sym (push tt) ∙∙ λ i → inl (σ A a i)) i --- Whitehead product (main definition) -[_∣_] : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ} +[_∣_]comp : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ} → (S₊∙ (suc n) →∙ X) → (S₊∙ (suc m) →∙ X) → S₊∙ (suc (n + m)) →∙ X -fst ([_∣_] {X = X} {n = n} {m = m} f g) x = - _∨→_ (f ∘∙ (inv (IsoSucSphereSusp n) , IsoSucSphereSusp∙ n)) - (g ∘∙ (inv (IsoSucSphereSusp m) , IsoSucSphereSusp∙ m)) - (joinTo⋁ {A = S₊∙ n} {B = S₊∙ m} - (inv (IsoSphereJoin n m) x)) -snd ([_∣_] {n = n} {m = m} f g) = - cong (_∨→_ (f ∘∙ (inv (IsoSucSphereSusp n) , IsoSucSphereSusp∙ n)) - (g ∘∙ (inv (IsoSucSphereSusp m) , IsoSucSphereSusp∙ m))) - (cong (joinTo⋁ {A = S₊∙ n} {B = S₊∙ m}) (IsoSphereJoin⁻Pres∙ n m)) - ∙ cong (fst g) (IsoSucSphereSusp∙ m) - ∙ snd g - --- For Sⁿ, Sᵐ with n, m ≥ 2, we can avoid some bureaucracy. We make --- a separate definition and prove it equivalent. -[_∣_]-pre : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ} - → (S₊∙ (suc (suc n)) →∙ X) - → (S₊∙ (suc (suc m)) →∙ X) - → join (typ (S₊∙ (suc n))) (typ (S₊∙ (suc m))) → fst X -[_∣_]-pre {n = n} {m = m} f g x = - _∨→_ f g - (joinTo⋁ {A = S₊∙ (suc n)} {B = S₊∙ (suc m)} - x) - -[_∣_]₂ : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ} - → (S₊∙ (suc (suc n)) →∙ X) - → (S₊∙ (suc (suc m)) →∙ X) - → S₊∙ (suc ((suc n) + (suc m))) →∙ X -fst ([_∣_]₂ {n = n} {m = m} f g) x = - [ f ∣ g ]-pre (inv (IsoSphereJoin (suc n) (suc m)) x) -snd ([_∣_]₂ {n = n} {m = m} f g) = - cong ([ f ∣ g ]-pre) (IsoSphereJoin⁻Pres∙ (suc n) (suc m)) - ∙ snd g - -[]≡[]₂ : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ} - → (f : (S₊∙ (suc (suc n)) →∙ X)) - → (g : (S₊∙ (suc (suc m)) →∙ X)) - → [ f ∣ g ] ≡ [ f ∣ g ]₂ -[]≡[]₂ {n = n} {m = m} f g = - ΣPathP ( - (λ i x → _∨→_ (∘∙-idˡ f i) - (∘∙-idˡ g i) - (joinTo⋁ {A = S₊∙ (suc n)} {B = S₊∙ (suc m)} - (inv (IsoSphereJoin (suc n) (suc m)) x))) - , (cong (cong (_∨→_ (f ∘∙ idfun∙ _) - (g ∘∙ idfun∙ _)) - (cong (joinTo⋁ {A = S₊∙ (suc n)} {B = S₊∙ (suc m)}) - (IsoSphereJoin⁻Pres∙ (suc n) (suc m))) ∙_) - (sym (lUnit (snd g))) - ◁ λ j → (λ i → _∨→_ (∘∙-idˡ f j) - (∘∙-idˡ g j) - ( joinTo⋁ {A = S₊∙ (suc n)} {B = S₊∙ (suc m)} - ((IsoSphereJoin⁻Pres∙ (suc n) (suc m)) i))) ∙ snd g)) +[_∣_]comp {n = n} {m = m} f g = + (((f ∘∙ (inv (IsoSucSphereSusp n) , IsoSucSphereSusp∙ n)) + ∨→ (g ∘∙ (inv (IsoSucSphereSusp m) , IsoSucSphereSusp∙ m)) + , cong (fst f) (IsoSucSphereSusp∙ n) ∙ snd f) + ∘∙ ((joinTo⋁ {A = S₊∙ n} {B = S₊∙ m} , sym (push tt)))) + ∘∙ (inv (IsoSphereJoin n m) , IsoSphereJoin⁻Pres∙ n m) + +[]comp≡[] : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ} + → (f : (S₊∙ (suc n) →∙ X)) + → (g : (S₊∙ (suc m) →∙ X)) + → [ f ∣ g ]comp ≡ [ f ∣ g ] +[]comp≡[] {X = X} {n = n} {m} f g = + cong (_∘∙ (sphere→Join n m , IsoSphereJoin⁻Pres∙ n m)) (main n m f g) + where + ∨fun : {n m : ℕ} (f : (S₊∙ (suc n) →∙ X)) (g : (S₊∙ (suc m) →∙ X)) + → ((_ , inl north) →∙ X) + ∨fun {n = n} {m} f g = + ((f ∘∙ (inv (IsoSucSphereSusp n) , IsoSucSphereSusp∙ n)) ∨→ + (g ∘∙ (inv (IsoSucSphereSusp m) , IsoSucSphereSusp∙ m)) + , cong (fst f) (IsoSucSphereSusp∙ n) ∙ snd f) + + open import Cubical.Foundations.Path + main : (n m : ℕ) (f : (S₊∙ (suc n) →∙ X)) (g : (S₊∙ (suc m) →∙ X)) + → (∨fun f g ∘∙ (joinTo⋁ {A = S₊∙ n} {B = S₊∙ m} , sym (push tt))) + ≡ [ f ∣ g ]-pre + main n m f g = + ΣPathP ((funExt (λ { (inl x) → rp + ; (inr x) → lp + ; (push a b i) j → pushcase a b j i})) + , ((cong₂ _∙_ (symDistr _ _) refl + ∙ sym (assoc _ _ _) + ∙ cong (rp ∙_) (rCancel _) + ∙ sym (rUnit rp)) + ◁ λ i j → rp (i ∨ j))) + where + lp = cong (fst f) (IsoSucSphereSusp∙ n) ∙ snd f + rp = cong (fst g) (IsoSucSphereSusp∙ m) ∙ snd g + + help : (n : ℕ) (a : _) + → Square (cong (inv (IsoSucSphereSusp n)) (σ (S₊∙ n) a)) (σS a) + (IsoSucSphereSusp∙ n) (IsoSucSphereSusp∙ n) + help zero a = cong-∙ SuspBool→S¹ (merid a) (sym (merid (pt (S₊∙ zero)))) + ∙ sym (rUnit _) + help (suc n) a = refl + + ∙∙Distr∙ : ∀ {ℓ} {A : Type ℓ} {x y z w u : A} + {p : x ≡ y} {q : y ≡ z} {r : z ≡ w} {s : w ≡ u} + → p ∙∙ q ∙ r ∙∙ s ≡ ((p ∙ q) ∙ r ∙ s) + ∙∙Distr∙ = doubleCompPath≡compPath _ _ _ + ∙ assoc _ _ _ + ∙ cong₂ _∙_ (assoc _ _ _) refl + ∙ sym (assoc _ _ _) + + + pushcase : (a : S₊ n) (b : S₊ m) + → Square (cong (∨fun f g .fst ∘ joinTo⋁ {A = S₊∙ n} {B = S₊∙ m}) (push a b)) + (cong (fst [ f ∣ g ]-pre) (push a b)) + rp lp + pushcase a b = + (cong-∙∙ (∨fun f g .fst) _ _ _ + ∙ (λ i → cong (fst g) (PathP→compPathR∙∙ (help _ b) i) + ∙∙ symDistr lp (sym rp) i + ∙∙ cong (fst f) (PathP→compPathR∙∙ (help _ a) i)) + ∙ (λ i → cong (fst g) + (IsoSucSphereSusp∙ m + ∙∙ σS b + ∙∙ (λ j → IsoSucSphereSusp∙ m (~ j ∨ i))) + ∙∙ compPath-filler' (cong (fst g) (IsoSucSphereSusp∙ m)) (snd g) (~ i) + ∙ sym (compPath-filler' (cong (fst f) (IsoSucSphereSusp∙ n)) (snd f) (~ i)) + ∙∙ cong (fst f) + ((λ j → IsoSucSphereSusp∙ n (i ∨ j)) + ∙∙ σS a + ∙∙ sym (IsoSucSphereSusp∙ n)))) + ◁ compPathR→PathP∙∙ + ( ∙∙Distr∙ + ∙ cong₂ _∙_ (cong₂ _∙_ (cong (cong (fst g)) (sym (compPath≡compPath' _ _))) + refl) + refl + ∙ cong₂ _∙_ (cong (_∙ snd g) (cong-∙ (fst g) (IsoSucSphereSusp∙ m) (σS b)) + ∙ sym (assoc _ _ _)) + (cong (sym (snd f) ∙_) + (cong-∙ (fst f) (σS a) + (sym (IsoSucSphereSusp∙ n))) + ∙ assoc _ _ _) + ∙ sym ∙∙Distr∙ + ∙ cong₃ _∙∙_∙∙_ refl (cong₂ _∙_ refl (compPath≡compPath' _ _)) refl + ∙ λ i → compPath-filler (cong (fst g) (IsoSucSphereSusp∙ m)) (snd g) i + ∙∙ ((λ j → snd g (~ j ∧ i)) ∙∙ cong (fst g) (σS b) ∙∙ snd g) + ∙ (sym (snd f) ∙∙ cong (fst f) (σS a) ∙∙ λ j → snd f (j ∧ i)) + ∙∙ sym (compPath-filler (cong (fst f) (IsoSucSphereSusp∙ n)) (snd f) i)) -- Homotopy group version [_∣_]π' : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ} diff --git a/Cubical/Papers/Pi4S3-JournalVersion.agda b/Cubical/Papers/Pi4S3-JournalVersion.agda index 212a444a0d..fc4281db18 100644 --- a/Cubical/Papers/Pi4S3-JournalVersion.agda +++ b/Cubical/Papers/Pi4S3-JournalVersion.agda @@ -165,7 +165,7 @@ module ExactSeq = πLES open Suspensions renaming (toSusp to σ) -- Proposition 3.4: Sⁿ * Sᵐ ≃ Sⁿ⁺ᵐ⁺¹ -open Spheres using (IsoSphereJoin) +open SMult using (IsoSphereJoin) -- Definition 3.5 and Proposition 3.6 (Hopf map), -- Phrased somewhat differently in the paper. @@ -243,7 +243,7 @@ open James₁ using (IsoΩ∥SuspS²∥₅∥Pushout⋁↪fold⋁S²∥₅) -- Definition 4.8: W + whitehead product W = joinTo⋁ -open Whitehead using ([_∣_]₂) +open Whitehead using ([_∣_]) -- Theorem 4.9 is omitted as it is used implicitly in the proof of the main result diff --git a/Cubical/Papers/Pi4S3.agda b/Cubical/Papers/Pi4S3.agda index 6bcc7e8642..fa312717f5 100644 --- a/Cubical/Papers/Pi4S3.agda +++ b/Cubical/Papers/Pi4S3.agda @@ -35,6 +35,7 @@ open import Cubical.Foundations.Prelude as Prelude open import Cubical.HITs.Susp as Suspensions open import Cubical.HITs.Sn as Spheres hiding (S) renaming (S₊ to S) +open import Cubical.HITs.Sn.Multiplication as SMult open import Cubical.HITs.Pushout as Pushouts open import Cubical.HITs.Wedge as Wedges open import Cubical.HITs.Join as Joins @@ -212,11 +213,11 @@ open James₁ using (IsoΩ∥SuspS²∥₅∥Pushout⋁↪fold⋁S²∥₅) ---- C. Formalization of the James construction ---- -- Proposition 8: Sⁿ * Sᵐ ≃ Sⁿ⁺ᵐ⁺¹ -open Spheres using (IsoSphereJoin) +open SMult using (IsoSphereJoin) -- Definition 6: W + whitehead product W = joinTo⋁ -open Whitehead using ([_∣_]₂) +open Whitehead using ([_∣_]) -- Theorem 3 is omitted as it is used implicitly in the proof of the main result