diff --git a/Cubical/ZCohomology/GroupStructure.agda b/Cubical/ZCohomology/GroupStructure.agda index 11e57f8ae0..95e1ea150a 100644 --- a/Cubical/ZCohomology/GroupStructure.agda +++ b/Cubical/ZCohomology/GroupStructure.agda @@ -672,6 +672,11 @@ coHomRedGrDir n A = AbGroup→Group (coHomRedGroupDir n A) coHomFun : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (n : ℕ) (f : A → B) → coHom n B → coHom n A coHomFun n f = ST.rec § λ β → ∣ β ∘ f ∣₂ +coHomFunId : ∀ {ℓ} {A : Type ℓ} (n : ℕ) + → coHomFun {A = A} n (idfun A) ≡ idfun _ +coHomFunId n = + funExt (ST.elim (λ _ → isSetPathImplicit) λ _ → refl) + coHomMorph : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (n : ℕ) (f : A → B) → GroupHom (coHomGr n B) (coHomGr n A) fst (coHomMorph n f) = coHomFun n f snd (coHomMorph n f) = makeIsGroupHom (helper n) diff --git a/Cubical/ZCohomology/Groups/CP2.agda b/Cubical/ZCohomology/Groups/CP2.agda index 73d8f0d679..395d6a4129 100644 --- a/Cubical/ZCohomology/Groups/CP2.agda +++ b/Cubical/ZCohomology/Groups/CP2.agda @@ -20,6 +20,7 @@ open import Cubical.Data.Int open import Cubical.Data.Sigma open import Cubical.Algebra.Group +open import Cubical.Algebra.Group.GroupPath open import Cubical.Algebra.Group.Instances.Int open import Cubical.Algebra.Group.Morphisms open import Cubical.Algebra.Group.MorphismProperties @@ -35,6 +36,8 @@ open import Cubical.HITs.PropositionalTruncation as PT open import Cubical.HITs.Truncation open import Cubical.Homotopy.Hopf +open import Cubical.Homotopy.HopfInvariant.HopfMap renaming (CP² to CP2 ; H²CP²≅ℤ to H²CP2≅ℤ) +open import Cubical.Homotopy.HSpace open import Cubical.ZCohomology.Base open import Cubical.ZCohomology.Groups.Connected @@ -44,6 +47,7 @@ open import Cubical.ZCohomology.MayerVietorisUnreduced open import Cubical.ZCohomology.Groups.Unit open import Cubical.ZCohomology.Groups.Sn open import Cubical.ZCohomology.RingStructure.CupProduct +open import Cubical.ZCohomology.RingStructure.RingLaws open S¹Hopf open IsGroupHom @@ -113,6 +117,7 @@ H²CP²≅ℤ = compGroupIso (BijectionIso→GroupIso bij) BijectionIso.surj bij y = M.Ker-Δ⊂Im-i 2 y (isContr→isProp isContrH²TotalHopf _ _) + H⁴CP²≅ℤ : GroupIso (coHomGr 4 CP²) ℤGroup H⁴CP²≅ℤ = compGroupIso (invGroupIso (BijectionIso→GroupIso bij)) (compGroupIso help (Hⁿ-Sⁿ≅ℤ 2)) @@ -249,3 +254,112 @@ brunerie2 = ℤ→HⁿCP²→ℤ 1 |brunerie2|≡1 : abs (ℤ→HⁿCP²→ℤ 1) ≡ 1 |brunerie2|≡1 = refl -} + + +-- Construction of an iso H⁴(CP²) ≅ ℤ sending s.t. the map +-- ℤ × ℤ → H²(CP²) × H²(CP²) → H⁴(CP²) → ℤ +-- constructed via the cup product sends (1 , 1) to 1 +-- If brunerie2 computes (to 1), this could be avoided + +CP²≡CP2 : Iso CP² CP2 +CP²≡CP2 = compIso (equivToIso (symPushout fst (λ _ → tt))) (invIso CP²-iso) + where + module m = Hopf S1-AssocHSpace (sphereElim2 0 (λ _ _ → squash₁) ∣ (λ _ → base) ∣₁) + F : (x : S₊ 2) → (m.Hopf x) → (HopfSuspS¹ (fun idIso x)) + F north y = y + F south y = y + F (merid x i) = toPathP lem i + where + lem : transport (λ i → m.Hopf (merid x i) → Glue S¹ (Border x i)) + (λ x → x) + ≡ λ x → x + lem = funExt λ z → commS¹ x (invEq (m.μ-eq x) z) ∙ secEq (m.μ-eq x) z + + F-eq : (x : S₊ 2) → isEquiv (F x) + F-eq = suspToPropElim base (λ _ → isPropIsEquiv _) (idIsEquiv _) + + H = m.TotalSpaceHopfPush + + H≃TotalHopf : H ≃ TotalHopf + H≃TotalHopf = + compEquiv + (m.TotalSpaceHopfPush→TotalSpace + , m.isEquivTotalSpaceHopfPush→TotalSpace) + (Σ-cong-equiv (idEquiv _) + λ x → F x , F-eq x) + + CP²-iso : Iso CP2 (Pushout {A = TotalHopf} (λ _ → tt) fst) + CP²-iso = pushoutIso _ _ _ _ H≃TotalHopf (idEquiv _) (idEquiv _) refl refl + +Σℤ≅H⁴CP² : Σ[ ϕ₄ ∈ GroupEquiv ℤGroup (coHomGr 4 CP²) ] + Iso.inv (fst H²CP²≅ℤ) 1 ⌣ Iso.inv (fst H²CP²≅ℤ) 1 + ≡ fst (fst ϕ₄) 1 +Σℤ≅H⁴CP² = fst c , (cong (inv (fst H²CP²≅ℤ) (pos 1) ⌣_) lem ∙ snd c) + where + cupIsEquiv : {A B : Type₀} + → (f : A ≃ B) + → (e : coHom 2 A) + → isEquiv {A = coHom 2 A} {B = coHom 4 A} (_⌣ e) + → isEquiv {A = coHom 2 B} {B = coHom 4 B} (_⌣ coHomFun 2 (invEq f) e) + cupIsEquiv {B = B} = + EquivJ (λ A f → + (e : coHom 2 A) + → isEquiv {A = coHom 2 A} {B = coHom 4 A} (_⌣ e) + → isEquiv {B = coHom 4 B} (_⌣ coHomFun 2 (invEq f) e)) + λ e p → subst isEquiv (help e) p + where + help : (e : coHom 2 B) → _⌣ e ≡ _⌣ coHomFun 2 (invEq (idEquiv B)) e + help e i y = y ⌣ coHomFunId 2 (~ i) e + + gen' : coHom 2 CP² + gen' = ∣ (λ { (inl x) → ∣ x ∣ ; (inr x) → 0ₖ 2 ; (push a i) → pp a i}) ∣₂ + where + pp : (a : TotalHopf) → Path (coHomK 2) ∣ fst a ∣ₕ (0ₖ 2) + pp = elim-TotalHopf _ (λ _ → (isOfHLevelTrunc 4 _ _)) refl + + + genId : Iso.fun (fst (coHomIso 2 CP²≡CP2)) genCP² ≡ gen' + genId = sym (Iso.leftInv (fst H²CP²≅ℤ) _) + ∙∙ cong (Iso.inv (fst H²CP²≅ℤ)) lem + ∙∙ Iso.leftInv (fst H²CP²≅ℤ) _ + where + lem : Iso.fun (fst H²CP²≅ℤ) (Iso.fun (fst (coHomIso 2 CP²≡CP2)) genCP²) + ≡ Iso.fun (fst H²CP²≅ℤ) gen' + lem = refl + + isEquiv⌣gen' : GroupEquiv (coHomGr 2 CP²) (coHomGr 4 CP²) + fst (fst isEquiv⌣gen') = _⌣ gen' + snd (fst isEquiv⌣gen') = + subst isEquiv (λ i x → x ⌣ genId i) + ((cupIsEquiv (invEquiv (isoToEquiv CP²≡CP2))) genCP² + (subst isEquiv (funExt (λ x → cong (x ⌣_) Gysin-e≡genCP²)) + (⌣Equiv .fst .snd))) + snd isEquiv⌣gen' = makeIsGroupHom λ f g → rightDistr-⌣ _ _ f g _ + + abstract + main : {A B : Group₀} + (A≃B : GroupEquiv A B) + (Z≃A : GroupEquiv ℤGroup A) + → Σ[ Z≃B ∈ GroupEquiv ℤGroup B ] + fst (fst A≃B) (fst (fst Z≃A) (pos 1)) + ≡ fst (fst Z≃B) (pos 1) + main {A = A} {B = B} = + GroupEquivJ (λ B A≃B → + (Z≃A : GroupEquiv ℤGroup A) + → Σ[ Z≃B ∈ GroupEquiv ℤGroup B ] + fst (fst A≃B) (fst (fst Z≃A) (pos 1)) + ≡ fst (fst Z≃B) (pos 1)) + (GroupEquivJ (λ A Z≃A → Σ[ ϕ ∈ GroupEquiv ℤGroup A ] fst (fst Z≃A) 1 ≡ fst (fst ϕ) 1) + (idGroupEquiv , refl)) + + lem : inv (fst H²CP²≅ℤ) (pos 1) ≡ gen' + lem = Iso.leftInv (fst H²CP²≅ℤ) gen' + + c = main isEquiv⌣gen' (GroupIso→GroupEquiv (invGroupIso H²CP²≅ℤ)) + +H⁴CP²≅ℤ-pos : GroupIso (coHomGr 4 CP²) ℤGroup +H⁴CP²≅ℤ-pos = invGroupIso (GroupEquiv→GroupIso (Σℤ≅H⁴CP² .fst)) + +H⁴CP²≅ℤ-pos-resp⌣ : Iso.inv (fst H²CP²≅ℤ) (pos 1) ⌣ Iso.inv (fst H²CP²≅ℤ) (pos 1) + ≡ Iso.inv (fst H⁴CP²≅ℤ-pos) (pos 1) +H⁴CP²≅ℤ-pos-resp⌣ = Σℤ≅H⁴CP² .snd