From 573426bb521ccc34d047d47e5f6183772d21139b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Axel=20Ljungstr=C3=B6m?= <49276137+aljungstrom@users.noreply.github.com> Date: Wed, 24 Jan 2024 07:49:31 +0100 Subject: [PATCH] Summary file/missing cohomology lemmas (#1092) * fix * stuff * stuff * more * .. * done? * wups * wups * wups * fixes * ugh... --- Cubical/Algebra/AbGroup/Base.agda | 4 - .../AbGroup/Instances/DirectProduct.agda | 15 + Cubical/Algebra/AbGroup/Instances/Int.agda | 11 + Cubical/Algebra/AbGroup/Instances/IntMod.agda | 89 +++ Cubical/Algebra/AbGroup/Instances/Pi.agda | 12 + Cubical/Algebra/AbGroup/Properties.agda | 94 ++++ Cubical/Algebra/Group/Instances/IntMod.agda | 55 ++ Cubical/Algebra/Group/Instances/Pi.agda | 32 ++ Cubical/Algebra/Group/MorphismProperties.agda | 4 + Cubical/Axiom/Choice.agda | 66 +++ Cubical/Cohomology/EilenbergMacLane/Base.agda | 107 +++- .../EilenbergMacLane/CupProduct.agda | 1 + .../EilenbergMacLane/EilenbergSteenrod.agda | 522 ++++++++++-------- .../EilenbergMacLane/Groups/KleinBottle.agda | 239 +++++++- .../EilenbergMacLane/Groups/RP2.agda | 288 +++++++++- .../EilenbergMacLane/Groups/RP2wedgeS1.agda | 1 + .../EilenbergMacLane/Groups/RPinf.agda | 282 ++++++++++ .../EilenbergMacLane/Groups/Sn.agda | 41 +- .../EilenbergMacLane/Groups/Torus.agda | 238 ++++++++ .../EilenbergMacLane/Groups/Unit.agda | 49 ++ .../EilenbergMacLane/Rings/KleinBottle.agda | 2 + .../EilenbergMacLane/Rings/RP2.agda | 449 +++++++++++++++ .../EilenbergMacLane/Rings/RP2wedgeS1.agda | 1 + .../EilenbergMacLane/Rings/RPinf.agda | 317 +++++++++++ .../Cohomology/EilenbergMacLane/Rings/Sn.agda | 367 ++++++++++++ .../EilenbergMacLane/Rings/Z2-properties.agda | 1 + Cubical/Data/Bool/Properties.agda | 20 + Cubical/Data/Nat/Base.agda | 11 + Cubical/Data/Nat/Order.agda | 6 + Cubical/Foundations/Pointed/Homogeneous.agda | 8 + Cubical/HITs/KleinBottle/Properties.agda | 18 + Cubical/HITs/RPn/Base.agda | 14 + Cubical/HITs/Wedge/Base.agda | 7 + .../Homotopy/EilenbergMacLane/CupProduct.agda | 46 +- Cubical/Homotopy/EilenbergMacLane/Order2.agda | 4 +- .../Homotopy/EilenbergMacLane/Properties.agda | 18 + Cubical/Homotopy/EilenbergSteenrod.agda | 36 ++ Cubical/Papers/CohomologyRings.agda | 2 +- .../ComputationalSyntheticCohomology.agda | 312 +++++++++++ Cubical/ZCohomology/EilenbergSteenrodZ.agda | 21 + 40 files changed, 3542 insertions(+), 268 deletions(-) create mode 100644 Cubical/Algebra/AbGroup/Instances/DirectProduct.agda create mode 100644 Cubical/Algebra/AbGroup/Instances/Int.agda create mode 100644 Cubical/Algebra/AbGroup/Instances/IntMod.agda create mode 100644 Cubical/Algebra/AbGroup/Instances/Pi.agda create mode 100644 Cubical/Algebra/Group/Instances/Pi.agda create mode 100644 Cubical/Axiom/Choice.agda create mode 100644 Cubical/Cohomology/EilenbergMacLane/Groups/RPinf.agda create mode 100644 Cubical/Cohomology/EilenbergMacLane/Groups/Torus.agda create mode 100644 Cubical/Cohomology/EilenbergMacLane/Groups/Unit.agda create mode 100644 Cubical/Cohomology/EilenbergMacLane/Rings/RP2.agda create mode 100644 Cubical/Cohomology/EilenbergMacLane/Rings/RPinf.agda create mode 100644 Cubical/Cohomology/EilenbergMacLane/Rings/Sn.agda create mode 100644 Cubical/Papers/ComputationalSyntheticCohomology.agda diff --git a/Cubical/Algebra/AbGroup/Base.agda b/Cubical/Algebra/AbGroup/Base.agda index eb86373396..74605f2388 100644 --- a/Cubical/Algebra/AbGroup/Base.agda +++ b/Cubical/Algebra/AbGroup/Base.agda @@ -315,10 +315,6 @@ module _ {ℓ ℓ' : Level} (AGr : Group ℓ) (BGr : AbGroup ℓ') where renaming (_·_ to _∙A_ ; inv to -A_ ; 1g to 1A ; ·IdR to ·IdRA) - trivGroupHom : GroupHom AGr (BGr *) - fst trivGroupHom x = 0B - snd trivGroupHom = makeIsGroupHom λ _ _ → sym (+IdRB 0B) - compHom : GroupHom AGr (BGr *) → GroupHom AGr (BGr *) → GroupHom AGr (BGr *) fst (compHom f g) x = fst f x +B fst g x snd (compHom f g) = diff --git a/Cubical/Algebra/AbGroup/Instances/DirectProduct.agda b/Cubical/Algebra/AbGroup/Instances/DirectProduct.agda new file mode 100644 index 0000000000..0848ae9b75 --- /dev/null +++ b/Cubical/Algebra/AbGroup/Instances/DirectProduct.agda @@ -0,0 +1,15 @@ +{-# OPTIONS --safe #-} +module Cubical.Algebra.AbGroup.Instances.DirectProduct where + +open import Cubical.Data.Sigma +open import Cubical.Algebra.AbGroup.Base +open import Cubical.Algebra.Group.DirProd + +AbDirProd : ∀ {ℓ ℓ'} → AbGroup ℓ → AbGroup ℓ' → AbGroup (ℓ-max ℓ ℓ') +AbDirProd G H = + Group→AbGroup (DirProd (AbGroup→Group G) (AbGroup→Group H)) comm + where + comm : (x y : fst G × fst H) → _ ≡ _ + comm (g1 , h1) (g2 , h2) = + ΣPathP (AbGroupStr.+Comm (snd G) g1 g2 + , AbGroupStr.+Comm (snd H) h1 h2) diff --git a/Cubical/Algebra/AbGroup/Instances/Int.agda b/Cubical/Algebra/AbGroup/Instances/Int.agda new file mode 100644 index 0000000000..cfd4dfe51a --- /dev/null +++ b/Cubical/Algebra/AbGroup/Instances/Int.agda @@ -0,0 +1,11 @@ +{-# OPTIONS --safe #-} +module Cubical.Algebra.AbGroup.Instances.Int where + +open import Cubical.Foundations.Prelude +open import Cubical.Data.Int +open import Cubical.Algebra.AbGroup.Base +open import Cubical.Algebra.Group.Base +open import Cubical.Algebra.Group.Instances.Int + +ℤAbGroup : AbGroup ℓ-zero +ℤAbGroup = Group→AbGroup ℤGroup +Comm diff --git a/Cubical/Algebra/AbGroup/Instances/IntMod.agda b/Cubical/Algebra/AbGroup/Instances/IntMod.agda new file mode 100644 index 0000000000..a9c8eee522 --- /dev/null +++ b/Cubical/Algebra/AbGroup/Instances/IntMod.agda @@ -0,0 +1,89 @@ +{-# OPTIONS --safe #-} +module Cubical.Algebra.AbGroup.Instances.IntMod where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Function + +open import Cubical.Algebra.AbGroup + +open import Cubical.Algebra.Group.Instances.Int +open import Cubical.Algebra.AbGroup.Instances.Int +open import Cubical.Algebra.Group.Instances.IntMod +open import Cubical.Algebra.Group.Base +open import Cubical.Algebra.Group.MorphismProperties +open import Cubical.Algebra.Group.ZAction + +open import Cubical.Data.Empty as ⊥ +open import Cubical.Data.Nat renaming (_+_ to _+ℕ_ ; _·_ to _·ℕ_) +open import Cubical.Data.Nat.Order +open import Cubical.Data.Int + renaming (_+_ to _+ℤ_ ; _·_ to _·ℤ_ ; -_ to -ℤ_) +open import Cubical.Data.Fin +open import Cubical.Data.Fin.Arithmetic +open import Cubical.Data.Sigma + +open import Cubical.HITs.SetQuotients as SQ +open import Cubical.HITs.PropositionalTruncation as PT + +ℤAbGroup/_ : ℕ → AbGroup ℓ-zero +ℤAbGroup/ n = Group→AbGroup (ℤGroup/ n) (comm n) + where + comm : (n : ℕ) (x y : fst (ℤGroup/ n)) + → GroupStr._·_ (snd (ℤGroup/ n)) x y + ≡ GroupStr._·_ (snd (ℤGroup/ n)) y x + comm zero = +Comm + comm (suc n) = +ₘ-comm + +ℤ/2 : AbGroup ℓ-zero +ℤ/2 = ℤAbGroup/ 2 + +ℤ/2[2]≅ℤ/2 : AbGroupIso (ℤ/2 [ 2 ]ₜ) ℤ/2 +Iso.fun (fst ℤ/2[2]≅ℤ/2) = fst +Iso.inv (fst ℤ/2[2]≅ℤ/2) x = x , cong (x +ₘ_) (+ₘ-rUnit x) ∙ x+x x + where + x+x : (x : ℤ/2 .fst) → x +ₘ x ≡ fzero + x+x = ℤ/2-elim refl refl +Iso.rightInv (fst ℤ/2[2]≅ℤ/2) x = Σ≡Prop (λ _ → isProp≤) refl +Iso.leftInv (fst ℤ/2[2]≅ℤ/2) x = Σ≡Prop (λ _ → isSetFin _ _) refl +snd ℤ/2[2]≅ℤ/2 = makeIsGroupHom λ _ _ → refl + +ℤ/2/2≅ℤ/2 : AbGroupIso (ℤ/2 /^ 2) ℤ/2 +Iso.fun (fst ℤ/2/2≅ℤ/2) = + SQ.rec isSetFin (λ x → x) lem + where + lem : _ + lem = ℤ/2-elim (ℤ/2-elim (λ _ → refl) + (PT.rec (isSetFin _ _) + (uncurry (ℤ/2-elim + (λ p → ⊥.rec (snotz (sym (cong fst p)))) + λ p → ⊥.rec (snotz (sym (cong fst p))))))) + (ℤ/2-elim (PT.rec (isSetFin _ _) + (uncurry (ℤ/2-elim + (λ p → ⊥.rec (snotz (sym (cong fst p)))) + λ p → ⊥.rec (snotz (sym (cong fst p)))))) + λ _ → refl) +Iso.inv (fst ℤ/2/2≅ℤ/2) = [_] +Iso.rightInv (fst ℤ/2/2≅ℤ/2) _ = refl +Iso.leftInv (fst ℤ/2/2≅ℤ/2) = + SQ.elimProp (λ _ → squash/ _ _) λ _ → refl +snd ℤ/2/2≅ℤ/2 = makeIsGroupHom + (SQ.elimProp (λ _ → isPropΠ λ _ → isSetFin _ _) + λ a → SQ.elimProp (λ _ → isSetFin _ _) λ b → refl) + +ℤTorsion : (n : ℕ) → isContr (fst (ℤAbGroup [ (suc n) ]ₜ)) +fst (ℤTorsion n) = AbGroupStr.0g (snd (ℤAbGroup [ (suc n) ]ₜ)) +snd (ℤTorsion n) (a , p) = Σ≡Prop (λ _ → isSetℤ _ _) + (sym (help a (ℤ·≡· (pos (suc n)) a ∙ p))) + where + help : (a : ℤ) → a +ℤ pos n ·ℤ a ≡ 0 → a ≡ 0 + help (pos zero) p = refl + help (pos (suc a)) p = + ⊥.rec (snotz (injPos (pos+ (suc a) (n ·ℕ suc a) + ∙ cong (pos (suc a) +ℤ_) (pos·pos n (suc a)) ∙ p))) + help (negsuc a) p = ⊥.rec + (snotz (injPos (cong -ℤ_ (negsuc+ a (n ·ℕ suc a) + ∙ (cong (negsuc a +ℤ_) + (cong (-ℤ_) (pos·pos n (suc a))) + ∙ sym (cong (negsuc a +ℤ_) (pos·negsuc n a)) ∙ p))))) diff --git a/Cubical/Algebra/AbGroup/Instances/Pi.agda b/Cubical/Algebra/AbGroup/Instances/Pi.agda new file mode 100644 index 0000000000..5e61f2928e --- /dev/null +++ b/Cubical/Algebra/AbGroup/Instances/Pi.agda @@ -0,0 +1,12 @@ +{-# OPTIONS --safe #-} +module Cubical.Algebra.AbGroup.Instances.Pi where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Algebra.AbGroup +open import Cubical.Algebra.Group.Instances.Pi + +module _ {ℓ ℓ' : Level} {X : Type ℓ} (G : X → AbGroup ℓ') where + ΠAbGroup : AbGroup (ℓ-max ℓ ℓ') + ΠAbGroup = Group→AbGroup (ΠGroup (λ x → AbGroup→Group (G x))) + λ f g i x → IsAbGroup.+Comm (AbGroupStr.isAbGroup (G x .snd)) (f x) (g x) i diff --git a/Cubical/Algebra/AbGroup/Properties.agda b/Cubical/Algebra/AbGroup/Properties.agda index 2f16f05be3..a80c06397f 100644 --- a/Cubical/Algebra/AbGroup/Properties.agda +++ b/Cubical/Algebra/AbGroup/Properties.agda @@ -5,6 +5,17 @@ open import Cubical.Foundations.Prelude open import Cubical.Algebra.AbGroup.Base open import Cubical.Algebra.Group +open import Cubical.Algebra.Group.Morphisms +open import Cubical.Algebra.Group.MorphismProperties +open import Cubical.Algebra.Group.QuotientGroup +open import Cubical.Algebra.Group.Subgroup +open import Cubical.Algebra.Group.ZAction + +open import Cubical.HITs.SetQuotients as SQ hiding (_/_) + +open import Cubical.Data.Int using (ℤ ; pos ; negsuc) +open import Cubical.Data.Nat hiding (_+_) +open import Cubical.Data.Sigma private variable ℓ : Level @@ -24,3 +35,86 @@ module AbGroupTheory (A : AbGroup ℓ) where implicitInverse : ∀ {a b} → a + b ≡ 0g → b ≡ - a implicitInverse b+a≡0 = invUniqueR b+a≡0 + +addGroupHom : (A B : AbGroup ℓ) (ϕ ψ : AbGroupHom A B) → AbGroupHom A B +fst (addGroupHom A B ϕ ψ) x = AbGroupStr._+_ (snd B) (ϕ .fst x) (ψ .fst x) +snd (addGroupHom A B ϕ ψ) = makeIsGroupHom + λ x y → cong₂ (AbGroupStr._+_ (snd B)) + (IsGroupHom.pres· (snd ϕ) x y) + (IsGroupHom.pres· (snd ψ) x y) + ∙ AbGroupTheory.comm-4 B (fst ϕ x) (fst ϕ y) (fst ψ x) (fst ψ y) + +negGroupHom : (A B : AbGroup ℓ) (ϕ : AbGroupHom A B) → AbGroupHom A B +fst (negGroupHom A B ϕ) x = AbGroupStr.-_ (snd B) (ϕ .fst x) +snd (negGroupHom A B ϕ) = + makeIsGroupHom λ x y + → sym (IsGroupHom.presinv (snd ϕ) (AbGroupStr._+_ (snd A) x y)) + ∙ cong (fst ϕ) (GroupTheory.invDistr (AbGroup→Group A) x y + ∙ AbGroupStr.+Comm (snd A) _ _) + ∙ IsGroupHom.pres· (snd ϕ) _ _ + ∙ cong₂ (AbGroupStr._+_ (snd B)) + (IsGroupHom.presinv (snd ϕ) x) + (IsGroupHom.presinv (snd ϕ) y) + +subtrGroupHom : (A B : AbGroup ℓ) (ϕ ψ : AbGroupHom A B) → AbGroupHom A B +subtrGroupHom A B ϕ ψ = addGroupHom A B ϕ (negGroupHom A B ψ) + + + +-- ℤ-multiplication defines a homomorphism for abelian groups +private module _ (G : AbGroup ℓ) where + ℤ·isHom-pos : (n : ℕ) (x y : fst G) + → (pos n ℤ[ (AbGroup→Group G) ]· (AbGroupStr._+_ (snd G) x y)) + ≡ AbGroupStr._+_ (snd G) ((pos n) ℤ[ (AbGroup→Group G) ]· x) + ((pos n) ℤ[ (AbGroup→Group G) ]· y) + ℤ·isHom-pos zero x y = + sym (AbGroupStr.+IdR (snd G) (AbGroupStr.0g (snd G))) + ℤ·isHom-pos (suc n) x y = + cong₂ (AbGroupStr._+_ (snd G)) + refl + (ℤ·isHom-pos n x y) + ∙ AbGroupTheory.comm-4 G _ _ _ _ + + ℤ·isHom-neg : (n : ℕ) (x y : fst G) + → (negsuc n ℤ[ (AbGroup→Group G) ]· (AbGroupStr._+_ (snd G) x y)) + ≡ AbGroupStr._+_ (snd G) ((negsuc n) ℤ[ (AbGroup→Group G) ]· x) + ((negsuc n) ℤ[ (AbGroup→Group G) ]· y) + ℤ·isHom-neg zero x y = + GroupTheory.invDistr (AbGroup→Group G) _ _ + ∙ AbGroupStr.+Comm (snd G) _ _ + ℤ·isHom-neg (suc n) x y = + cong₂ (AbGroupStr._+_ (snd G)) + (GroupTheory.invDistr (AbGroup→Group G) _ _ + ∙ AbGroupStr.+Comm (snd G) _ _) + (ℤ·isHom-neg n x y) + ∙ AbGroupTheory.comm-4 G _ _ _ _ + +ℤ·isHom : (n : ℤ) (G : AbGroup ℓ) (x y : fst G) + → (n ℤ[ (AbGroup→Group G) ]· (AbGroupStr._+_ (snd G) x y)) + ≡ AbGroupStr._+_ (snd G) (n ℤ[ (AbGroup→Group G) ]· x) + (n ℤ[ (AbGroup→Group G) ]· y) +ℤ·isHom (pos n) G = ℤ·isHom-pos G n +ℤ·isHom (negsuc n) G = ℤ·isHom-neg G n + +-- left multiplication as a group homomorphism +multₗHom : (G : AbGroup ℓ) (n : ℤ) → AbGroupHom G G +fst (multₗHom G n) g = n ℤ[ (AbGroup→Group G) ]· g +snd (multₗHom G n) = makeIsGroupHom (ℤ·isHom n G) + +-- Abelian groups quotiented by a natural number +_/^_ : (G : AbGroup ℓ) (n : ℕ) → AbGroup ℓ +G /^ n = + Group→AbGroup + ((AbGroup→Group G) + / (imSubgroup (multₗHom G (pos n)) + , isNormalIm (multₗHom G (pos n)) (AbGroupStr.+Comm (snd G)))) + (SQ.elimProp2 (λ _ _ → squash/ _ _) + λ a b → cong [_] (AbGroupStr.+Comm (snd G) a b)) + +-- Torsion subgrous +_[_]ₜ : (G : AbGroup ℓ) (n : ℕ) → AbGroup ℓ +G [ n ]ₜ = + Group→AbGroup (Subgroup→Group (AbGroup→Group G) + (kerSubgroup (multₗHom G (pos n)))) + λ {(x , p) (y , q) → Σ≡Prop (λ _ → isPropIsInKer (multₗHom G (pos n)) _) + (AbGroupStr.+Comm (snd G) _ _)} diff --git a/Cubical/Algebra/Group/Instances/IntMod.agda b/Cubical/Algebra/Group/Instances/IntMod.agda index b00e675516..d3de7be2be 100644 --- a/Cubical/Algebra/Group/Instances/IntMod.agda +++ b/Cubical/Algebra/Group/Instances/IntMod.agda @@ -4,6 +4,9 @@ module Cubical.Algebra.Group.Instances.IntMod where open import Cubical.Foundations.Prelude open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Equiv + +open import Cubical.Relation.Nullary open import Cubical.Data.Empty as ⊥ open import Cubical.Data.Unit @@ -215,3 +218,55 @@ isHomℤ→Fin n = -Const-ℤ/2 : (x : fst (ℤGroup/ 2)) → -ₘ x ≡ x -Const-ℤ/2 = ℤ/2-elim refl refl + +pres0→GroupIsoℤ/2 : ∀ {ℓ} {G : Group ℓ} (f : fst G ≃ (ℤGroup/ 2) .fst) + → fst f (GroupStr.1g (snd G)) ≡ fzero + → IsGroupHom (snd G) (fst f) ((ℤGroup/ 2) .snd) +pres0→GroupIsoℤ/2 {G = G} f fp = isGroupHomInv ((invEquiv f) , main) + where + one = invEq f fone + + f⁻∙ : invEq f fzero ≡ GroupStr.1g (snd G) + f⁻∙ = sym (cong (invEq f) fp) ∙ retEq f _ + + f⁻1 : GroupStr._·_ (snd G) (invEq f fone) (invEq f fone) + ≡ GroupStr.1g (snd G) + f⁻1 = sym (retEq f (GroupStr._·_ (snd G) (invEq f fone) (invEq f fone))) + ∙∙ cong (invEq f) (mainlem _ refl ∙ sym fp) + ∙∙ retEq f (GroupStr.1g (snd G)) + where + l : ¬ (fst f (GroupStr._·_ (snd G) (invEq f fone) (invEq f fone)) + ≡ fone) + l p = snotz (cong fst q) + where + q : fone ≡ fzero + q = (sym (secEq f fone) + ∙ cong (fst f) + ((sym (GroupStr.·IdL (snd G) one) + ∙ cong (λ x → GroupStr._·_ (snd G) x one) (sym (GroupStr.·InvL (snd G) one))) + ∙ sym (GroupStr.·Assoc (snd G) (GroupStr.inv (snd G) one) one one))) + ∙ cong (fst f) (cong (GroupStr._·_ (snd G) (GroupStr.inv (snd G) (invEq f fone))) + ((sym (retEq f _) ∙ cong (invEq f) p))) + ∙ cong (fst f) (GroupStr.·InvL (snd G) _) + ∙ fp + + + mainlem : (x : _) + → fst f (GroupStr._·_ (snd G) (invEq f fone) (invEq f fone)) ≡ x + → f .fst ((snd G GroupStr.· invEq f fone) (invEq f fone)) ≡ fzero + mainlem = ℤ/2-elim + (λ p → p) + λ p → ⊥.rec (l p) + + + main : IsGroupHom ((ℤGroup/ 2) .snd) (invEq f) (snd G) + main = + makeIsGroupHom + (ℤ/2-elim + (ℤ/2-elim (f⁻∙ ∙ sym (GroupStr.·IdR (snd G) (GroupStr.1g (snd G))) + ∙ cong (λ x → snd G .GroupStr._·_ x x) (sym f⁻∙)) + (sym (GroupStr.·IdL (snd G) one) + ∙ cong (λ x → snd G .GroupStr._·_ x one) (sym f⁻∙))) + (ℤ/2-elim (sym (GroupStr.·IdR (snd G) one) + ∙ cong (snd G .GroupStr._·_ (invEq f fone)) (sym f⁻∙)) + (f⁻∙ ∙ sym f⁻1))) diff --git a/Cubical/Algebra/Group/Instances/Pi.agda b/Cubical/Algebra/Group/Instances/Pi.agda new file mode 100644 index 0000000000..bb2bb2e355 --- /dev/null +++ b/Cubical/Algebra/Group/Instances/Pi.agda @@ -0,0 +1,32 @@ +{-# OPTIONS --safe #-} +module Cubical.Algebra.Group.Instances.Pi where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Algebra.Group.Base +open import Cubical.Algebra.Semigroup +open import Cubical.Algebra.Monoid + +open IsGroup +open GroupStr +open IsMonoid +open IsSemigroup + +module _ {ℓ ℓ' : Level} {X : Type ℓ} (G : X → Group ℓ') where + ΠGroup : Group (ℓ-max ℓ ℓ') + fst ΠGroup = (x : X) → fst (G x) + 1g (snd ΠGroup) x = 1g (G x .snd) + GroupStr._·_ (snd ΠGroup) f g x = GroupStr._·_ (G x .snd) (f x) (g x) + inv (snd ΠGroup) f x = inv (G x .snd) (f x) + is-set (isSemigroup (isMonoid (isGroup (snd ΠGroup)))) = + isSetΠ λ x → is-set (G x .snd) + IsSemigroup.·Assoc (isSemigroup (isMonoid (isGroup (snd ΠGroup)))) f g h = + funExt λ x → IsSemigroup.·Assoc (isSemigroup (isMonoid (G x .snd))) (f x) (g x) (h x) + IsMonoid.·IdR (isMonoid (isGroup (snd ΠGroup))) f = + funExt λ x → IsMonoid.·IdR (isMonoid (isGroup (snd (G x)))) (f x) + IsMonoid.·IdL (isMonoid (isGroup (snd ΠGroup))) f = + funExt λ x → IsMonoid.·IdL (isMonoid (isGroup (snd (G x)))) (f x) + ·InvR (isGroup (snd ΠGroup)) f = + funExt λ x → ·InvR (isGroup (snd (G x))) (f x) + ·InvL (isGroup (snd ΠGroup)) f = + funExt λ x → ·InvL (isGroup (snd (G x))) (f x) diff --git a/Cubical/Algebra/Group/MorphismProperties.agda b/Cubical/Algebra/Group/MorphismProperties.agda index 071230f91e..bc5f285f7d 100644 --- a/Cubical/Algebra/Group/MorphismProperties.agda +++ b/Cubical/Algebra/Group/MorphismProperties.agda @@ -177,6 +177,10 @@ compGroupHom : GroupHom F G → GroupHom G H → GroupHom F H fst (compGroupHom f g) = fst g ∘ fst f snd (compGroupHom f g) = isGroupHomComp f g +trivGroupHom : GroupHom G H +fst (trivGroupHom {H = H}) _ = 1g (snd H) +snd (trivGroupHom {H = H}) = makeIsGroupHom λ _ _ → sym (·IdR (snd H) _) + GroupHomDirProd : {A : Group ℓ} {B : Group ℓ'} {C : Group ℓ''} {D : Group ℓ'''} → GroupHom A C → GroupHom B D → GroupHom (DirProd A B) (DirProd C D) fst (GroupHomDirProd mf1 mf2) = map-× (fst mf1) (fst mf2) diff --git a/Cubical/Axiom/Choice.agda b/Cubical/Axiom/Choice.agda new file mode 100644 index 0000000000..8e3bd511ba --- /dev/null +++ b/Cubical/Axiom/Choice.agda @@ -0,0 +1,66 @@ +{-# OPTIONS --safe #-} + +{- +This file contains a definition of the n-level axiom of coice, +i.e. the statment that the canonical map + +∥ Πₐ Bₐ ∥ₙ → (Πₐ ∥ Bₐ ∥ₙ) + +is an equivalence. +-} + +module Cubical.Axiom.Choice where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism + +open import Cubical.Data.Nat +open import Cubical.Data.Sigma +open import Cubical.Data.Empty as ⊥ +open import Cubical.Data.Fin as FN +open import Cubical.Data.Nat.Order + +open import Cubical.HITs.Truncation as TR +open import Cubical.HITs.PropositionalTruncation as PT + +private + variable + ℓ ℓ' ℓ'' : Level + +choiceMap : {A : Type ℓ} {B : A → Type ℓ'} (n : ℕ) + → hLevelTrunc n ((a : A) → B a) + → (a : A) → hLevelTrunc n (B a) +choiceMap n = + TR.rec (isOfHLevelΠ n (λ _ → isOfHLevelTrunc n)) + λ f a → ∣ f a ∣ₕ + +-- n-level axiom of choice +satAC : (ℓ' : Level) (n : ℕ) (A : Type ℓ) → Type (ℓ-max ℓ (ℓ-suc ℓ')) +satAC ℓ' n A = (B : A → Type ℓ') → isEquiv (choiceMap {A = A} {B} n) + +-- Version of (propositional) AC with ∃ +AC∃-map : {A : Type ℓ} {B : A → Type ℓ'} + {C : (a : A) → B a → Type ℓ''} + → ∃[ f ∈ ((a : A) → B a) ] ((a : _) → C a (f a)) + → ((a : A) → ∃ (B a) (C a)) +AC∃-map = + PT.rec (isPropΠ (λ _ → squash₁)) + λ f → λ a → ∣ f .fst a , f .snd a ∣₁ + +satAC∃ : ∀ {ℓ} (ℓ' ℓ'' : Level) (A : Type ℓ) → Type _ +satAC∃ ℓ' ℓ'' A = (B : A → Type ℓ') (C : (a : A) → B a → Type ℓ'') + → isEquiv (AC∃-map {B = B} {C = C}) + +satAC→satAC∃ : {A : Type ℓ} + → satAC (ℓ-max ℓ' ℓ'') (suc zero) A → satAC∃ ℓ' ℓ'' A +satAC→satAC∃ F B C = propBiimpl→Equiv squash₁ (isPropΠ (λ _ → squash₁)) + _ + (λ f → invEq propTrunc≃Trunc1 (TR.map (λ f → fst ∘ f , λ a → f a .snd ) + (invEq (_ , F (λ x → Σ (B x) (C x))) λ a → fst propTrunc≃Trunc1 (f a)))) .snd + +-- All types satisfy (-2) level axiom of choice +satAC₀ : {A : Type ℓ} → satAC ℓ' 0 A +satAC₀ B = isoToIsEquiv (iso (λ _ _ → tt*) (λ _ → tt*) (λ _ → refl) λ _ → refl) diff --git a/Cubical/Cohomology/EilenbergMacLane/Base.agda b/Cubical/Cohomology/EilenbergMacLane/Base.agda index f0c192a445..12b470cc27 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Base.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Base.agda @@ -6,8 +6,10 @@ open import Cubical.Homotopy.EilenbergMacLane.GroupStructure open import Cubical.Homotopy.EilenbergMacLane.Base open import Cubical.Homotopy.EilenbergMacLane.Properties open import Cubical.Homotopy.EilenbergMacLane.Order2 +open import Cubical.Homotopy.Connected open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function open import Cubical.Foundations.Transport open import Cubical.Foundations.HLevels open import Cubical.Foundations.GroupoidLaws @@ -17,6 +19,7 @@ open import Cubical.Foundations.Pointed.Homogeneous open import Cubical.Foundations.Isomorphism open import Cubical.HITs.PropositionalTruncation as PT +open import Cubical.HITs.Truncation as TR open import Cubical.Data.Nat open import Cubical.Data.Sigma @@ -28,6 +31,9 @@ open import Cubical.Algebra.AbGroup.Base open import Cubical.Algebra.Monoid open import Cubical.Algebra.Semigroup open import Cubical.Algebra.Group.Instances.IntMod +open import Cubical.Algebra.AbGroup.Instances.IntMod +open import Cubical.Algebra.AbGroup.Instances.DirectProduct +open import Cubical.Algebra.AbGroup.Properties open import Cubical.HITs.SetTruncation as ST hiding (rec ; map ; elim ; elim2 ; elim3) @@ -270,6 +276,44 @@ coHom≅coHomRed n G A = makeIsGroupHom (ST.elim2 (λ _ _ → isSetPathImplicit) λ _ _ → refl) +coHom⁰≅coHomRed⁰ : (G : AbGroup ℓ) (A : Pointed ℓ) + → AbGroupEquiv (AbDirProd (coHomRedGr 0 G A) G) (coHomGr 0 G (typ A)) +fst (coHom⁰≅coHomRed⁰ G A) = isoToEquiv is + where + is : Iso _ _ + Iso.fun is = uncurry (ST.rec (isSetΠ (λ _ → squash₂)) + λ f g → ∣ (λ x → AbGroupStr._+_ (snd G) (fst f x) g) ∣₂) + Iso.inv is = ST.rec (isSet× squash₂ (is-set (snd G))) + λ f → ∣ (λ x → AbGroupStr._-_ (snd G) (f x) (f (pt A))) + , +InvR (snd G) (f (pt A)) ∣₂ , f (pt A) + Iso.rightInv is = ST.elim (λ _ → isSetPathImplicit) + λ f → cong ∣_∣₂ (funExt λ x + → sym (+Assoc (snd G) _ _ _) + ∙∙ cong (AbGroupStr._+_ (snd G) (f x)) + (+InvL (snd G) (f (pt A))) + ∙∙ +IdR (snd G) (f x)) + Iso.leftInv is = + uncurry (ST.elim + (λ _ → isSetΠ (λ _ → isOfHLevelPath 2 + (isSet× squash₂ (is-set (snd G))) _ _)) + λ f → λ g + → ΣPathP (cong ∣_∣₂ (Σ≡Prop (λ _ → is-set (snd G) _ _) + (funExt (λ x → cong₂ (AbGroupStr._+_ (snd G)) + refl + (cong (- (snd G)) + (cong₂ (AbGroupStr._+_ (snd G)) (snd f) refl + ∙ +IdL (snd G) g)) + ∙ sym (+Assoc (snd G) _ _ _) + ∙ cong (AbGroupStr._+_ (snd G) (fst f x)) + (+InvR (snd G) g) + ∙ +IdR (snd G) (f .fst x)))) + , (cong (λ x → AbGroupStr._+_ (snd G) x g) (snd f) + ∙ +IdL (snd G) g))) +snd (coHom⁰≅coHomRed⁰ G A) = + makeIsGroupHom (uncurry (ST.elim (λ _ → isSetΠ2 λ _ _ → isSetPathImplicit) + λ f1 g1 → uncurry (ST.elim (λ _ → isSetΠ λ _ → isSetPathImplicit) + λ f2 g2 → cong ∣_∣₂ (funExt λ a → AbGroupTheory.comm-4 G _ _ _ _)))) + -- ℤ/2 lemmas +ₕ≡id-ℤ/2 : ∀ {ℓ} {A : Type ℓ} (n : ℕ) (x : coHom n ℤ/2 A) → x +ₕ x ≡ 0ₕ n +ₕ≡id-ℤ/2 n = @@ -297,6 +341,23 @@ snd (coHomHom n f) = makeIsGroupHom (ST.elim2 (λ _ _ → isOfHLevelPath 2 squash₂ _ _) λ f g → refl) +coHomEquiv : ∀ {ℓ''} {A : Type ℓ} {B : Type ℓ'} {G : AbGroup ℓ''} + (n : ℕ) + → (Iso A B) + → AbGroupEquiv (coHomGr n G B) (coHomGr n G A) +fst (coHomEquiv n f) = isoToEquiv is + where + is : Iso _ _ + Iso.fun is = coHomFun n (Iso.fun f) + Iso.inv is = coHomFun n (Iso.inv f) + Iso.rightInv is = + ST.elim (λ _ → isSetPathImplicit) + λ g → cong ∣_∣₂ (funExt λ x → cong g (Iso.leftInv f x)) + Iso.leftInv is = + ST.elim (λ _ → isSetPathImplicit) + λ g → cong ∣_∣₂ (funExt λ x → cong g (Iso.rightInv f x)) +snd (coHomEquiv n f) = snd (coHomHom n (Iso.fun f)) + coHomFun∙ : ∀ {ℓ''} {A : Pointed ℓ} {B : Pointed ℓ'} {G : AbGroup ℓ''} (n : ℕ) (f : A →∙ B) → coHomRed n G B → coHomRed n G A @@ -343,7 +404,51 @@ subst-EM-0ₖ : ∀{ℓ} {G : AbGroup ℓ} {n m : ℕ} (p : n ≡ m) subst-EM-0ₖ {G = G} {n = n} = J (λ m p → subst (EM G) p (0ₖ n) ≡ 0ₖ m) (transportRefl _) -subst-EM∙ : ∀{ℓ} {G : AbGroup ℓ} {n m : ℕ} (p : n ≡ m) +subst-EM∙ : ∀ {ℓ} {G : AbGroup ℓ} {n m : ℕ} (p : n ≡ m) → EM∙ G n →∙ EM∙ G m fst (subst-EM∙ {G = G} p) = subst (EM G) p snd (subst-EM∙ p) = subst-EM-0ₖ p + +coHomPointedElim : ∀ {ℓ ℓ' ℓ''} {G : AbGroup ℓ} + {A : Type ℓ'} (n : ℕ) (a : A) {B : coHom (suc n) G A → Type ℓ''} + → ((x : coHom (suc n) G A) → isProp (B x)) + → ((f : A → EM G (suc n)) → f a ≡ 0ₖ (suc n) → B ∣ f ∣₂) + → (x : coHom (suc n) G A) → B x +coHomPointedElim {ℓ'' = ℓ''} {G = G} {A = A} n a isprop indp = + ST.elim (λ _ → isOfHLevelSuc 1 (isprop _)) + λ f → helper n isprop indp f + where + helper : (n : ℕ) {B : coHom (suc n) G A → Type ℓ''} + → ((x : coHom (suc n) G A) → isProp (B x)) + → ((f : A → EM G (suc n)) → f a ≡ 0ₖ (suc n) → B ∣ f ∣₂) + → (f : A → EM G (suc n)) + → B ∣ f ∣₂ + helper n isprop ind f = + TR.rec (isProp→isOfHLevelSuc n (isprop _)) + (ind f) + (isConnectedPath (suc n) (isConnectedEM (suc n)) (f a) (0ₖ (suc n)) .fst) + +coHomTruncEquiv : {A : Type ℓ} (G : AbGroup ℓ) (n : ℕ) + → AbGroupEquiv (coHomGr n G (∥ A ∥ (suc (suc n)))) (coHomGr n G A) +fst (coHomTruncEquiv G n) = + isoToEquiv (setTruncIso (univTrunc (suc (suc n)) {B = _ , hLevelEM G n})) +snd (coHomTruncEquiv G n) = + makeIsGroupHom (ST.elim2 (λ _ _ → isSetPathImplicit) + λ _ _ → refl) + +EM→-charac : ∀ {ℓ ℓ'} {A : Pointed ℓ} {G : AbGroup ℓ'} (n : ℕ) + → Iso (fst A → EM G n) ((A →∙ EM∙ G n) × EM G n) +Iso.fun (EM→-charac {A = A} n) f = + ((λ x → f x -ₖ f (pt A)) , rCancelₖ n (f (pt A))) , f (pt A) +Iso.inv (EM→-charac n) (f , a) x = fst f x +ₖ a +Iso.rightInv (EM→-charac {A = A} n) ((f , p) , a) = + ΣPathP (→∙Homogeneous≡ (isHomogeneousEM _) + (funExt (λ x → (λ i → (f x +ₖ a) -ₖ (cong (_+ₖ a) p ∙ lUnitₖ n a) i) + ∙ sym (assocₖ n (f x) a (-ₖ a)) + ∙ cong (f x +ₖ_) (rCancelₖ n a) + ∙ rUnitₖ n (f x))) + , cong (_+ₖ a) p ∙ lUnitₖ n a) +Iso.leftInv (EM→-charac {A = A} n) f = + funExt λ x → sym (assocₖ n (f x) (-ₖ f (pt A)) (f (pt A))) + ∙∙ cong (f x +ₖ_) (lCancelₖ n (f (pt A))) + ∙∙ rUnitₖ n (f x) diff --git a/Cubical/Cohomology/EilenbergMacLane/CupProduct.agda b/Cubical/Cohomology/EilenbergMacLane/CupProduct.agda index 74d3f9f61e..65a9ad0eda 100644 --- a/Cubical/Cohomology/EilenbergMacLane/CupProduct.agda +++ b/Cubical/Cohomology/EilenbergMacLane/CupProduct.agda @@ -17,6 +17,7 @@ open import Cubical.Algebra.Ring open import Cubical.Algebra.CommRing open import Cubical.Algebra.CommRing.Instances.IntMod open import Cubical.Algebra.Group.Instances.IntMod +open import Cubical.Algebra.AbGroup.Instances.IntMod open import Cubical.Foundations.Prelude diff --git a/Cubical/Cohomology/EilenbergMacLane/EilenbergSteenrod.agda b/Cubical/Cohomology/EilenbergMacLane/EilenbergSteenrod.agda index 0cd001a289..c669679958 100644 --- a/Cubical/Cohomology/EilenbergMacLane/EilenbergSteenrod.agda +++ b/Cubical/Cohomology/EilenbergMacLane/EilenbergSteenrod.agda @@ -25,6 +25,7 @@ open import Cubical.Algebra.Group.MorphismProperties open import Cubical.Algebra.AbGroup open import Cubical.Algebra.AbGroup.Instances.Unit open import Cubical.Algebra.Group.Instances.Unit +open import Cubical.Algebra.AbGroup.Instances.Pi open import Cubical.HITs.Wedge open import Cubical.HITs.Pushout @@ -40,243 +41,310 @@ open import Cubical.Data.Sigma open import Cubical.Data.Int open import Cubical.Data.Unit +open import Cubical.Axiom.Choice + open Iso -open coHomTheory +module _ where + open coHomTheory + + -- This module verifies the (reduced) Eilenberg-Steenrod axioms for + -- the following ℤ-indexed cohomology theory + + coHomRedℤ : ∀ {ℓ ℓ'} → AbGroup ℓ' → ℤ → Pointed ℓ → AbGroup (ℓ-max ℓ ℓ') + coHomRedℤ G (pos n) A = coHomRedGr n G A + coHomRedℤ G (negsuc n) A = UnitAbGroup + + module coHomRedℤ {ℓ ℓ'} {G : AbGroup ℓ} where + Hmap∙ : (n : ℤ) {A B : Pointed ℓ'} + → A →∙ B + → AbGroupHom (coHomRedℤ G n B) (coHomRedℤ G n A) + Hmap∙ (pos n) = coHomHom∙ n + Hmap∙ (negsuc n) f = idGroupHom + + compAx : (n : ℤ) {A B C : Pointed ℓ'} + (g : B →∙ C) (f : A →∙ B) → + compGroupHom (Hmap∙ n g) (Hmap∙ n f) + ≡ Hmap∙ n (g ∘∙ f) + compAx (pos n) g f = Σ≡Prop (λ _ → isPropIsGroupHom _ _) + (funExt (ST.elim (λ _ → isSetPathImplicit) + λ a → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl))) + compAx (negsuc n) g f = Σ≡Prop (λ _ → isPropIsGroupHom _ _) refl + + idAx : (n : ℤ) {A : Pointed ℓ'} → + Hmap∙ n (idfun∙ A) ≡ idGroupHom + idAx (pos n) = Σ≡Prop (λ _ → isPropIsGroupHom _ _) + (funExt (ST.elim (λ _ → isSetPathImplicit) + λ f → cong ∣_∣₂ (ΣPathP (refl , sym (lUnit (snd f)))))) + idAx (negsuc n) = refl --- This module verifies the (reduced) Eilenberg-Steenrod axioms for --- the following ℤ-indexed cohomology theory + suspMap : (n : ℤ) {A : Pointed ℓ'} → + AbGroupHom (coHomRedℤ G (sucℤ n) (Susp (typ A) , north)) + (coHomRedℤ G n A) + fst (suspMap (pos n) {A = A}) = + ST.map λ f → (λ x → ΩEM+1→EM n + (sym (snd f) + ∙∙ cong (fst f) (merid x ∙ sym (merid (pt A))) + ∙∙ snd f)) + , cong (ΩEM+1→EM n) + (cong (sym (snd f) ∙∙_∙∙ snd f) + (cong (cong (fst f)) + (rCancel (merid (pt A)))) + ∙ ∙∙lCancel (snd f)) + ∙ ΩEM+1→EM-refl n + snd (suspMap (pos n) {A = A}) = + makeIsGroupHom + (ST.elim2 (λ _ _ → isSetPathImplicit) + (λ f g → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) + (funExt λ x → main n _ (sym (snd f)) _ (sym (snd g)) + (cong (fst f) (merid x ∙ sym (merid (pt A)))) + (cong (fst g) (merid x ∙ sym (merid (pt A)))))))) + where + main : (n : ℕ) (x : EM G (suc n)) (f0 : 0ₖ (suc n) ≡ x) + (y : EM G (suc n)) (g0 : 0ₖ (suc n) ≡ y) + (f1 : x ≡ x) (g1 : y ≡ y) + → ΩEM+1→EM n (sym (cong₂ _+ₖ_ (sym f0) (sym g0) + ∙ rUnitₖ (suc n) (0ₖ (suc n))) + ∙∙ cong₂ _+ₖ_ f1 g1 + ∙∙ (cong₂ _+ₖ_ (sym f0) (sym g0) + ∙ rUnitₖ (suc n) (0ₖ (suc n)))) + ≡ ΩEM+1→EM n (f0 ∙∙ f1 ∙∙ sym f0) + +[ n ]ₖ ΩEM+1→EM n (g0 ∙∙ g1 ∙∙ sym g0) + main zero = J> (J> λ f g → + cong (ΩEM+1→EM {G = G} zero) + (cong (λ x → sym x ∙∙ cong₂ _+ₖ_ f g ∙∙ x) + (sym (rUnit refl)) + ∙∙ sym (rUnit _) + ∙∙ cong₂+₁ f g) + ∙∙ ΩEM+1→EM-hom zero f g + ∙∙ cong₂ _+ₖ_ (cong (ΩEM+1→EM zero) (rUnit f)) + (cong (ΩEM+1→EM zero) (rUnit g))) + main (suc n) = + J> (J> λ f g → + cong (ΩEM+1→EM {G = G} (suc n)) + (cong (λ x → sym x ∙∙ cong₂ _+ₖ_ f g ∙∙ x) + (sym (rUnit refl)) + ∙∙ sym (rUnit _) + ∙∙ cong₂+₂ n f g) + ∙∙ ΩEM+1→EM-hom (suc n) f g + ∙∙ cong₂ _+ₖ_ (cong (ΩEM+1→EM (suc n)) (rUnit f)) + (cong (ΩEM+1→EM (suc n)) (rUnit g))) + fst (suspMap (negsuc n)) _ = tt* + snd (suspMap (negsuc n)) = makeIsGroupHom λ _ _ → refl -coHomRedℤ : ∀ {ℓ ℓ'} → AbGroup ℓ' → ℤ → Pointed ℓ → AbGroup (ℓ-max ℓ ℓ') -coHomRedℤ G (pos n) A = coHomRedGr n G A -coHomRedℤ G (negsuc n) A = UnitAbGroup + toSusp-coHomRed : (n : ℕ) {A : Pointed ℓ'} + → A →∙ EM∙ G n → (Susp (typ A) , north) →∙ EM∙ G (suc n) + fst (toSusp-coHomRed n f) north = 0ₖ (suc n) + fst (toSusp-coHomRed n f) south = 0ₖ (suc n) + fst (toSusp-coHomRed n f) (merid a i) = EM→ΩEM+1 n (fst f a) i + snd (toSusp-coHomRed n f) = refl -module coHomRedℤ {ℓ ℓ'} {G : AbGroup ℓ} where - Hmap∙ : (n : ℤ) {A B : Pointed ℓ'} - → A →∙ B - → AbGroupHom (coHomRedℤ G n B) (coHomRedℤ G n A) - Hmap∙ (pos n) = coHomHom∙ n - Hmap∙ (negsuc n) f = idGroupHom + suspMapIso : (n : ℤ) {A : Pointed ℓ'} → + AbGroupIso (coHomRedℤ G (sucℤ n) (Susp (typ A) , north)) + (coHomRedℤ G n A) + fun (fst (suspMapIso n)) = suspMap n .fst + inv (fst (suspMapIso (pos n))) = ST.map (toSusp-coHomRed n) + inv (fst (suspMapIso (negsuc zero))) _ = 0ₕ∙ zero + inv (fst (suspMapIso (negsuc (suc n)))) _ = tt* + rightInv (fst (suspMapIso (pos n) {A = A})) = + ST.elim (λ _ → isSetPathImplicit) + λ f → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) + (funExt λ x → cong (ΩEM+1→EM n) + (sym (rUnit _) + ∙∙ cong-∙ (toSusp-coHomRed n f .fst) + (merid x) (sym (merid (pt A))) + ∙∙ cong (EM→ΩEM+1 n (fst f x) ∙_) + (cong sym (cong (EM→ΩEM+1 n) (snd f) + ∙ EM→ΩEM+1-0ₖ n)) + ∙ sym (rUnit _)) + ∙ Iso.leftInv (Iso-EM-ΩEM+1 n) (fst f x))) + rightInv (fst (suspMapIso (negsuc zero))) tt* = refl + rightInv (fst (suspMapIso (negsuc (suc n)))) tt* = refl + leftInv (fst (suspMapIso (pos n) {A = A})) = + ST.elim (λ _ → isSetPathImplicit) + λ f → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM (suc n)) + (funExt λ { north → sym (snd f) + ; south → sym (snd f) ∙ cong (fst f) (merid (pt A)) + ; (merid a i) j → lem a f j i})) + where + lem : (a : typ A) (f : Susp∙ (typ A) →∙ EM∙ G (suc n)) + → PathP (λ i → snd f (~ i) ≡ (sym (snd f) ∙ cong (fst f) (merid (pt A))) i) + (EM→ΩEM+1 n (ΩEM+1→EM n (sym (snd f) + ∙∙ cong (fst f) (toSusp A a) + ∙∙ snd f))) + (cong (fst f) (merid a)) + lem a f = Iso.rightInv (Iso-EM-ΩEM+1 n) _ + ◁ λ i j → hcomp (λ k + → λ { (i = i1) → fst f (merid a j) + ; (j = i0) → snd f (~ i ∧ k) + ; (j = i1) → compPath-filler' + (sym (snd f)) (cong (fst f) (merid (pt A))) k i}) + (fst f (compPath-filler (merid a) + (sym (merid (pt A))) (~ i) j)) + leftInv (fst (suspMapIso (negsuc zero) {A = A})) = + ST.elim (λ _ → isSetPathImplicit) + λ f → cong ∣_∣₂ (Σ≡Prop (λ _ → hLevelEM G 0 _ _) + (funExt (suspToPropElim (pt A) + (λ _ → hLevelEM G 0 _ _) + (sym (snd f))))) + leftInv (fst (suspMapIso (negsuc (suc n)))) tt* = refl + snd (suspMapIso n) = suspMap n .snd - suspMap : (n : ℤ) {A : Pointed ℓ'} → - AbGroupHom (coHomRedℤ G (sucℤ n) (Susp (typ A) , north)) - (coHomRedℤ G n A) - fst (suspMap (pos n) {A = A}) = - ST.map λ f → (λ x → ΩEM+1→EM n - (sym (snd f) - ∙∙ cong (fst f) (merid x ∙ sym (merid (pt A))) - ∙∙ snd f)) - , cong (ΩEM+1→EM n) - (cong (sym (snd f) ∙∙_∙∙ snd f) - (cong (cong (fst f)) - (rCancel (merid (pt A)))) - ∙ ∙∙lCancel (snd f)) - ∙ ΩEM+1→EM-refl n - snd (suspMap (pos n) {A = A}) = - makeIsGroupHom - (ST.elim2 (λ _ _ → isSetPathImplicit) - (λ f g → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) - (funExt λ x → main n _ (sym (snd f)) _ (sym (snd g)) - (cong (fst f) (merid x ∙ sym (merid (pt A)))) - (cong (fst g) (merid x ∙ sym (merid (pt A)))))))) + satisfies-ES : ∀ {ℓ ℓ'} (G : AbGroup ℓ) → coHomTheory {ℓ'} (coHomRedℤ G) + Hmap (satisfies-ES G) = coHomRedℤ.Hmap∙ + HMapComp (satisfies-ES G) = coHomRedℤ.compAx + HMapId (satisfies-ES G) = coHomRedℤ.idAx + fst (Suspension (satisfies-ES G)) n = GroupIso→GroupEquiv (coHomRedℤ.suspMapIso n) + snd (Suspension (satisfies-ES G)) f (pos n) = + funExt (ST.elim (λ _ → isSetPathImplicit) λ f + → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM (suc n)) + (funExt λ { north → refl + ; south → refl + ; (merid a i) → refl}))) + snd (Suspension (satisfies-ES G)) f (negsuc zero) = + funExt λ {tt* → cong ∣_∣₂ (Σ≡Prop (λ _ → hLevelEM G 0 _ _) refl)} + snd (Suspension (satisfies-ES G)) f (negsuc (suc n)) = refl + Exactness (satisfies-ES G) {A = A} {B = B} f (pos n) = isoToPath help where - main : (n : ℕ) (x : EM G (suc n)) (f0 : 0ₖ (suc n) ≡ x) - (y : EM G (suc n)) (g0 : 0ₖ (suc n) ≡ y) - (f1 : x ≡ x) (g1 : y ≡ y) - → ΩEM+1→EM n (sym (cong₂ _+ₖ_ (sym f0) (sym g0) - ∙ rUnitₖ (suc n) (0ₖ (suc n))) - ∙∙ cong₂ _+ₖ_ f1 g1 - ∙∙ (cong₂ _+ₖ_ (sym f0) (sym g0) - ∙ rUnitₖ (suc n) (0ₖ (suc n)))) - ≡ ΩEM+1→EM n (f0 ∙∙ f1 ∙∙ sym f0) - +[ n ]ₖ ΩEM+1→EM n (g0 ∙∙ g1 ∙∙ sym g0) - main zero = J> (J> λ f g → - cong (ΩEM+1→EM {G = G} zero) - (cong (λ x → sym x ∙∙ cong₂ _+ₖ_ f g ∙∙ x) - (sym (rUnit refl)) - ∙∙ sym (rUnit _) - ∙∙ cong₂+₁ f g) - ∙∙ ΩEM+1→EM-hom zero f g - ∙∙ cong₂ _+ₖ_ (cong (ΩEM+1→EM zero) (rUnit f)) - (cong (ΩEM+1→EM zero) (rUnit g))) - main (suc n) = - J> (J> λ f g → - cong (ΩEM+1→EM {G = G} (suc n)) - (cong (λ x → sym x ∙∙ cong₂ _+ₖ_ f g ∙∙ x) - (sym (rUnit refl)) - ∙∙ sym (rUnit _) - ∙∙ cong₂+₂ n f g) - ∙∙ ΩEM+1→EM-hom (suc n) f g - ∙∙ cong₂ _+ₖ_ (cong (ΩEM+1→EM (suc n)) (rUnit f)) - (cong (ΩEM+1→EM (suc n)) (rUnit g))) - fst (suspMap (negsuc n)) _ = tt* - snd (suspMap (negsuc n)) = makeIsGroupHom λ _ _ → refl + To : (x : coHomRed n G B) + → isInKer (coHomHom∙ n f) x + → isInIm (coHomHom∙ n (cfcod (fst f) , refl)) x + To = ST.elim (λ _ → isSetΠ λ _ → isProp→isSet (isPropIsInIm _ _)) + λ g p → PT.map (λ id → ∣ (λ { (inl x) → 0ₖ n + ; (inr x) → fst g x + ; (push a i) → id (~ i) .fst a}) + , snd g ∣₂ + , cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) + refl)) + (Iso.fun ST.PathIdTrunc₀Iso p) - toSusp-coHomRed : (n : ℕ) {A : Pointed ℓ'} - → A →∙ EM∙ G n → (Susp (typ A) , north) →∙ EM∙ G (suc n) - fst (toSusp-coHomRed n f) north = 0ₖ (suc n) - fst (toSusp-coHomRed n f) south = 0ₖ (suc n) - fst (toSusp-coHomRed n f) (merid a i) = EM→ΩEM+1 n (fst f a) i - snd (toSusp-coHomRed n f) = refl + From : (x : coHomRed n G B) + → isInIm (coHomHom∙ n (cfcod (fst f) , refl)) x + → isInKer (coHomHom∙ n f) x + From = + ST.elim (λ _ → isSetΠ λ _ → isProp→isSet (isPropIsInKer _ _)) + λ g → PT.rec (isPropIsInKer _ _) + (uncurry (ST.elim (λ _ → isSetΠ λ _ → isProp→isSet (isPropIsInKer _ _)) + λ h p → PT.rec (squash₂ _ _) + (λ id → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) + (funExt λ x → sym (funExt⁻ (cong fst id) (fst f x)) + ∙ cong (fst h) (sym (push x) + ∙ push (pt A) + ∙ λ i → inr (snd f i)) + ∙ snd h))) + (Iso.fun ST.PathIdTrunc₀Iso p))) - suspMapIso : (n : ℤ) {A : Pointed ℓ'} → - AbGroupIso (coHomRedℤ G (sucℤ n) (Susp (typ A) , north)) - (coHomRedℤ G n A) - fun (fst (suspMapIso n)) = suspMap n .fst - inv (fst (suspMapIso (pos n))) = ST.map (toSusp-coHomRed n) - inv (fst (suspMapIso (negsuc zero))) _ = 0ₕ∙ zero - inv (fst (suspMapIso (negsuc (suc n)))) _ = tt* - rightInv (fst (suspMapIso (pos n) {A = A})) = - ST.elim (λ _ → isSetPathImplicit) - λ f → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) - (funExt λ x → cong (ΩEM+1→EM n) - (sym (rUnit _) - ∙∙ cong-∙ (toSusp-coHomRed n f .fst) - (merid x) (sym (merid (pt A))) - ∙∙ cong (EM→ΩEM+1 n (fst f x) ∙_) - (cong sym (cong (EM→ΩEM+1 n) (snd f) - ∙ EM→ΩEM+1-0ₖ n)) - ∙ sym (rUnit _)) - ∙ Iso.leftInv (Iso-EM-ΩEM+1 n) (fst f x))) - rightInv (fst (suspMapIso (negsuc zero))) tt* = refl - rightInv (fst (suspMapIso (negsuc (suc n)))) tt* = refl - leftInv (fst (suspMapIso (pos n) {A = A})) = - ST.elim (λ _ → isSetPathImplicit) - λ f → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM (suc n)) - (funExt λ { north → sym (snd f) - ; south → sym (snd f) ∙ cong (fst f) (merid (pt A)) - ; (merid a i) j → lem a f j i})) + help : Iso (Ker (coHomHom∙ n f)) + (Im (coHomHom∙ n (cfcod (fst f) , refl))) + fun help (x , p) = x , To x p + inv help (x , p) = x , From x p + rightInv help (x , p) = Σ≡Prop (λ _ → isPropIsInIm _ _) refl + leftInv help (x , p) = Σ≡Prop (λ _ → isPropIsInKer _ _) refl + Exactness (satisfies-ES {ℓ} {ℓ'} G) {A = A} {B = B} f (negsuc n) = + isoToPath help where - lem : (a : typ A) (f : Susp∙ (typ A) →∙ EM∙ G (suc n)) - → PathP (λ i → snd f (~ i) ≡ (sym (snd f) ∙ cong (fst f) (merid (pt A))) i) - (EM→ΩEM+1 n (ΩEM+1→EM n (sym (snd f) - ∙∙ cong (fst f) (toSusp A a) - ∙∙ snd f))) - (cong (fst f) (merid a)) - lem a f = Iso.rightInv (Iso-EM-ΩEM+1 n) _ - ◁ λ i j → hcomp (λ k - → λ { (i = i1) → fst f (merid a j) - ; (j = i0) → snd f (~ i ∧ k) - ; (j = i1) → compPath-filler' - (sym (snd f)) (cong (fst f) (merid (pt A))) k i}) - (fst f (compPath-filler (merid a) - (sym (merid (pt A))) (~ i) j)) - leftInv (fst (suspMapIso (negsuc zero) {A = A})) = - ST.elim (λ _ → isSetPathImplicit) - λ f → cong ∣_∣₂ (Σ≡Prop (λ _ → hLevelEM G 0 _ _) - (funExt (suspToPropElim (pt A) - (λ _ → hLevelEM G 0 _ _) - (sym (snd f))))) - leftInv (fst (suspMapIso (negsuc (suc n)))) tt* = refl - snd (suspMapIso n) = suspMap n .snd + help : Iso (Ker (coHomRedℤ.Hmap∙ {G = G} (negsuc n) f)) + (Im (coHomRedℤ.Hmap∙ {G = G} (negsuc n) {A = B} + (cfcod (fst f) , refl))) + fun help (tt* , p) = tt* , ∣ tt* , refl ∣₁ + inv help (tt* , p) = tt* , refl + rightInv help (tt* , p) = Σ≡Prop (λ _ → isPropIsInIm _ _) refl + leftInv help (tt* , p) = Σ≡Prop (λ _ → isPropIsInKer _ _) refl + Dimension (satisfies-ES G) (pos zero) p = ⊥.rec (p refl) + fst (Dimension (satisfies-ES G) (pos (suc n)) _) = 0ₕ∙ (suc n) + snd (Dimension (satisfies-ES G) (pos (suc n)) _) = + ST.elim (λ _ → isSetPathImplicit) + λ f → T.rec (isProp→isOfHLevelSuc n (squash₂ _ _)) + (λ p → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM (suc n)) + (funExt λ { (lift false) → sym p + ; (lift true) → sym (snd f)}))) + (Iso.fun (PathIdTruncIso (suc n)) + (isContr→isProp (isConnectedEM {G' = G} (suc n)) + ∣ fst f (lift false) ∣ ∣ 0ₖ (suc n) ∣)) + Dimension (satisfies-ES G) (negsuc n) _ = isContrUnit* + BinaryWedge (satisfies-ES G) (pos n) {A = A} {B = B} = + GroupIso→GroupEquiv main + where + main : GroupIso _ _ + fun (fst main) = + ST.rec (isSet× squash₂ squash₂) + λ f → ∣ f ∘∙ (inl , refl) ∣₂ , ∣ f ∘∙ (inr , sym (push tt)) ∣₂ + inv (fst main) = + uncurry (ST.rec2 squash₂ + λ f g → ∣ (λ { (inl x) → fst f x + ; (inr x) → fst g x + ; (push a i) → (snd f ∙ sym (snd g)) i}) + , snd f ∣₂) + rightInv (fst main) = + uncurry + (ST.elim2 (λ _ _ → isOfHLevelPath 2 (isSet× squash₂ squash₂) _ _) + λ f g → ΣPathP + ((cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl)) + , cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl))) + leftInv (fst main) = + ST.elim (λ _ → isSetPathImplicit) + λ f → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) + (funExt λ { (inl x) → refl + ; (inr x) → refl + ; (push a i) j → lem (snd f) (cong (fst f) (push tt)) j i})) + where + lem : ∀ {ℓ} {A : Type ℓ} {x y z : A} + → (p : x ≡ y) (q : x ≡ z) + → (refl ∙ p) ∙ sym (sym q ∙ p) ≡ q + lem p q = cong₂ _∙_ (sym (lUnit p)) (symDistr (sym q) p) + ∙ assoc p (sym p) q + ∙ cong (_∙ q) (rCancel p) + ∙ sym (lUnit q) + snd main = + makeIsGroupHom + (ST.elim2 (λ _ _ → isOfHLevelPath 2 (isSet× squash₂ squash₂) _ _) + λ f g → ΣPathP + (cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl) + , (cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl)))) + BinaryWedge (satisfies-ES G) (negsuc n) {A = A} {B = B} = + invGroupEquiv (GroupIso→GroupEquiv lUnitGroupIso^) -satisfies-ES : ∀ {ℓ ℓ'} (G : AbGroup ℓ) → coHomTheory {ℓ'} (coHomRedℤ G) -Hmap (satisfies-ES G) = coHomRedℤ.Hmap∙ -fst (Suspension (satisfies-ES G)) n = GroupIso→GroupEquiv (coHomRedℤ.suspMapIso n) -snd (Suspension (satisfies-ES G)) f (pos n) = - funExt (ST.elim (λ _ → isSetPathImplicit) λ f - → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM (suc n)) - (funExt λ { north → refl - ; south → refl - ; (merid a i) → refl}))) -snd (Suspension (satisfies-ES G)) f (negsuc zero) = - funExt λ {tt* → cong ∣_∣₂ (Σ≡Prop (λ _ → hLevelEM G 0 _ _) refl)} -snd (Suspension (satisfies-ES G)) f (negsuc (suc n)) = refl -Exactness (satisfies-ES G) {A = A} {B = B} f (pos n) = isoToPath help +open coHomTheoryGen +satisfies-ES-gen : ∀ {ℓ ℓ'} (G : AbGroup ℓ) → coHomTheoryGen {ℓ'} (coHomRedℤ G) +Hmap (satisfies-ES-gen G) = coHomTheory.Hmap (satisfies-ES G) +HMapComp (satisfies-ES-gen G) = coHomTheory.HMapComp (satisfies-ES G) +HMapId (satisfies-ES-gen G) = coHomTheory.HMapId (satisfies-ES G) +Suspension (satisfies-ES-gen G) = coHomTheory.Suspension (satisfies-ES G) +Exactness (satisfies-ES-gen G) = coHomTheory.Exactness (satisfies-ES G) +Dimension (satisfies-ES-gen G) = coHomTheory.Dimension (satisfies-ES G) +Wedge (satisfies-ES-gen G) (pos n) {I = I} satAC {A = A} = + subst isEquiv altEquiv≡ (snd altEquiv) where - To : (x : coHomRed n G B) - → isInKer (coHomHom∙ n f) x - → isInIm (coHomHom∙ n (cfcod (fst f) , refl)) x - To = ST.elim (λ _ → isSetΠ λ _ → isProp→isSet (isPropIsInIm _ _)) - λ g p → PT.map (λ id → ∣ (λ { (inl x) → 0ₖ n - ; (inr x) → fst g x - ; (push a i) → id (~ i) .fst a}) - , snd g ∣₂ - , cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) - refl)) - (Iso.fun ST.PathIdTrunc₀Iso p) + eq : _ ≃ _ + fst eq = _ + snd eq = satAC _ - From : (x : coHomRed n G B) - → isInIm (coHomHom∙ n (cfcod (fst f) , refl)) x - → isInKer (coHomHom∙ n f) x - From = - ST.elim (λ _ → isSetΠ λ _ → isProp→isSet (isPropIsInKer _ _)) - λ g → PT.rec (isPropIsInKer _ _) - (uncurry (ST.elim (λ _ → isSetΠ λ _ → isProp→isSet (isPropIsInKer _ _)) - λ h p → PT.rec (squash₂ _ _) - (λ id → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) - (funExt λ x → sym (funExt⁻ (cong fst id) (fst f x)) - ∙ cong (fst h) (sym (push x) - ∙ push (pt A) - ∙ λ i → inr (snd f i)) - ∙ snd h))) - (Iso.fun ST.PathIdTrunc₀Iso p))) + mainIso : Iso _ _ + fun mainIso = ST.map λ f i + → (λ x → f .fst (inr (i , x))) , cong (fst f) (sym (push i)) ∙ snd f + inv mainIso = ST.map λ f → (λ { (inl x) → 0ₖ n + ; (inr x) → f (fst x) .fst (snd x) + ; (push a i) → f a .snd (~ i)}) + , refl + rightInv mainIso = ST.elim (λ _ → isSetPathImplicit) + λ f → cong ∣_∣₂ (funExt (λ i → ΣPathP (refl , (sym (rUnit (snd (f i))))))) + leftInv mainIso = ST.elim (λ _ → isSetPathImplicit) + λ f → cong ∣_∣₂ (ΣPathP ((funExt + (λ { (inl x) → sym (snd f) + ; (inr x) → refl + ; (push a i) j + → compPath-filler (cong (fst f) (sym (push a))) (snd f) (~ j) (~ i)})) + , λ i j → snd f (~ i ∨ j))) - help : Iso (Ker (coHomHom∙ n f)) - (Im (coHomHom∙ n (cfcod (fst f) , refl))) - fun help (x , p) = x , To x p - inv help (x , p) = x , From x p - rightInv help (x , p) = Σ≡Prop (λ _ → isPropIsInIm _ _) refl - leftInv help (x , p) = Σ≡Prop (λ _ → isPropIsInKer _ _) refl -Exactness (satisfies-ES {ℓ} {ℓ'} G) {A = A} {B = B} f (negsuc n) = - isoToPath help - where - help : Iso (Ker (coHomRedℤ.Hmap∙ {G = G} (negsuc n) f)) - (Im (coHomRedℤ.Hmap∙ {G = G} (negsuc n) {A = B} - (cfcod (fst f) , refl))) - fun help (tt* , p) = tt* , ∣ tt* , refl ∣₁ - inv help (tt* , p) = tt* , refl - rightInv help (tt* , p) = Σ≡Prop (λ _ → isPropIsInIm _ _) refl - leftInv help (tt* , p) = Σ≡Prop (λ _ → isPropIsInKer _ _) refl -Dimension (satisfies-ES G) (pos zero) p = ⊥.rec (p refl) -fst (Dimension (satisfies-ES G) (pos (suc n)) _) = 0ₕ∙ (suc n) -snd (Dimension (satisfies-ES G) (pos (suc n)) _) = - ST.elim (λ _ → isSetPathImplicit) - λ f → T.rec (isProp→isOfHLevelSuc n (squash₂ _ _)) - (λ p → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM (suc n)) - (funExt λ { (lift false) → sym p - ; (lift true) → sym (snd f)}))) - (Iso.fun (PathIdTruncIso (suc n)) - (isContr→isProp (isConnectedEM {G' = G} (suc n)) - ∣ fst f (lift false) ∣ ∣ 0ₖ (suc n) ∣)) -Dimension (satisfies-ES G) (negsuc n) _ = isContrUnit* -BinaryWedge (satisfies-ES G) (pos n) {A = A} {B = B} = - GroupIso→GroupEquiv main - where - main : GroupIso _ _ - fun (fst main) = - ST.rec (isSet× squash₂ squash₂) - λ f → ∣ f ∘∙ (inl , refl) ∣₂ , ∣ f ∘∙ (inr , sym (push tt)) ∣₂ - inv (fst main) = - uncurry (ST.rec2 squash₂ - λ f g → ∣ (λ { (inl x) → fst f x - ; (inr x) → fst g x - ; (push a i) → (snd f ∙ sym (snd g)) i}) - , snd f ∣₂) - rightInv (fst main) = - uncurry - (ST.elim2 (λ _ _ → isOfHLevelPath 2 (isSet× squash₂ squash₂) _ _) - λ f g → ΣPathP - ((cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl)) - , cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl))) - leftInv (fst main) = - ST.elim (λ _ → isSetPathImplicit) - λ f → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) - (funExt λ { (inl x) → refl - ; (inr x) → refl - ; (push a i) j → lem (snd f) (cong (fst f) (push tt)) j i})) - where - lem : ∀ {ℓ} {A : Type ℓ} {x y z : A} - → (p : x ≡ y) (q : x ≡ z) - → (refl ∙ p) ∙ sym (sym q ∙ p) ≡ q - lem p q = cong₂ _∙_ (sym (lUnit p)) (symDistr (sym q) p) - ∙ assoc p (sym p) q - ∙ cong (_∙ q) (rCancel p) - ∙ sym (lUnit q) - snd main = - makeIsGroupHom - (ST.elim2 (λ _ _ → isOfHLevelPath 2 (isSet× squash₂ squash₂) _ _) - λ f g → ΣPathP - (cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl) - , (cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl)))) -BinaryWedge (satisfies-ES G) (negsuc n) {A = A} {B = B} = - invGroupEquiv (GroupIso→GroupEquiv lUnitGroupIso^) + altEquiv : (coHomRedℤ G (pos n) (⋁gen∙ I A) .fst) + ≃ (ΠAbGroup (λ i → coHomRedℤ G (pos n) (A i)) .fst) + altEquiv = isoToEquiv + (compIso + (compIso (compIso mainIso setTruncTrunc2Iso) + (equivToIso eq)) + (codomainIsoDep λ i → invIso setTruncTrunc2Iso)) + + altEquiv≡ : fst altEquiv ≡ _ + altEquiv≡ = funExt (ST.elim (λ _ → isOfHLevelPath 2 (isSetΠ (λ _ → squash₂)) _ _) + λ _ → refl) +Wedge (satisfies-ES-gen G) (negsuc n) {I = I} satAC {A = A} = + isoToIsEquiv (iso _ (λ _ → tt*) (λ _ → refl) λ _ → refl) diff --git a/Cubical/Cohomology/EilenbergMacLane/Groups/KleinBottle.agda b/Cubical/Cohomology/EilenbergMacLane/Groups/KleinBottle.agda index 9f76f417e0..816f326ec8 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Groups/KleinBottle.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Groups/KleinBottle.agda @@ -4,6 +4,7 @@ module Cubical.Cohomology.EilenbergMacLane.Groups.KleinBottle where open import Cubical.Cohomology.EilenbergMacLane.Base open import Cubical.Cohomology.EilenbergMacLane.Groups.Connected +open import Cubical.Cohomology.EilenbergMacLane.Groups.RP2 open import Cubical.Homotopy.EilenbergMacLane.GroupStructure open import Cubical.Homotopy.EilenbergMacLane.Order2 @@ -20,6 +21,9 @@ open import Cubical.Foundations.Equiv.HalfAdjoint open import Cubical.Foundations.Univalence open import Cubical.Foundations.Path open import Cubical.Foundations.GroupoidLaws +open import Cubical.Foundations.Function + +open import Cubical.Relation.Nullary open import Cubical.Data.Nat renaming (_+_ to _+ℕ_) open import Cubical.Data.Nat.Order @@ -31,14 +35,17 @@ open import Cubical.Algebra.Group.Base open import Cubical.Algebra.Group.Instances.IntMod open import Cubical.Algebra.Group.MorphismProperties open import Cubical.Algebra.Group.Morphisms -open import Cubical.Algebra.AbGroup.Base +open import Cubical.Algebra.AbGroup +open import Cubical.Algebra.AbGroup.Instances.DirectProduct +open import Cubical.Algebra.AbGroup.Instances.IntMod open import Cubical.HITs.KleinBottle renaming (rec to KleinFun) open import Cubical.HITs.SetTruncation as ST open import Cubical.HITs.Truncation as TR open import Cubical.HITs.PropositionalTruncation as PT -open import Cubical.HITs.EilenbergMacLane1 hiding (elimProp ; elimSet) +open import Cubical.HITs.EilenbergMacLane1 renaming (elimProp to elimPropEM1 ; elimSet to elimSetEM1) open import Cubical.HITs.Susp +open import Cubical.HITs.RPn open AbGroupStr @@ -203,11 +210,6 @@ H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 = invGroupEquiv ℤ/2×ℤ/2≅H¹[K²,ℤ/2] ------ H²(K²,ℤ/2) ------ -- The equivalence Ω²K₂ ≃ ℤ/2 will be needed -Iso-Ω²K₂-ℤ/2 : Iso (fst ((Ω^ 2) (EM∙ ℤ/2 2))) (fst ℤ/2) -Iso-Ω²K₂-ℤ/2 = - compIso (congIso (invIso (Iso-EM-ΩEM+1 {G = ℤ/2} 1))) - (invIso (Iso-EM-ΩEM+1 {G = ℤ/2} 0)) - Ω²K₂→ℤ/2 : fst ((Ω^ 2) (EM∙ ℤ/2 2)) → fst ℤ/2 Ω²K₂→ℤ/2 = Iso.fun Iso-Ω²K₂-ℤ/2 @@ -303,24 +305,6 @@ H²K²→ℤ/2-pres0 = cong H²K²→ℤ/2 KleinFun-trivₕ ∙ H²K²→ℤ/2-rewrite (λ _ _ → ∣ north ∣ₕ) ∙ refl -Isoℤ/2-morph : {A : Type} (f : A ≃ fst ℤ/2) (0A : A) - → 0 ≡ fst f 0A → (_+'_ : A → A → A) (-m : A → A) - → (λ x → x) ≡ -m - → (e : IsAbGroup 0A _+'_ -m) - → IsGroupHom (AbGroup→Group (A , abgroupstr 0A _+'_ (λ x → -m x) e) .snd) - (fst f) ((ℤGroup/ 2) .snd) -Isoℤ/2-morph = - EquivJ (λ A f → (0A : A) → 0 ≡ fst f 0A → (_+'_ : A → A → A) (-m : A → A) - → (λ x → x) ≡ -m - → (e : IsAbGroup 0A _+'_ -m) - → IsGroupHom (AbGroup→Group (A , abgroupstr 0A _+'_ (λ x → -m x) e) .snd) - (fst f) ((ℤGroup/ 2) .snd)) - (J> λ _+'_ → J> - λ e → makeIsGroupHom (ℤ/2-elim (ℤ/2-elim (IsAbGroup.+IdR e fzero) - (IsAbGroup.+IdL e 1)) - (ℤ/2-elim (IsAbGroup.+IdR e 1) - (IsAbGroup.+InvR e 1)))) - H²[K²,ℤ/2]≅ℤ/2 : AbGroupEquiv (coHomGr 2 ℤ/2 KleinBottle) ℤ/2 fst H²[K²,ℤ/2]≅ℤ/2 = isoToEquiv is where @@ -355,7 +339,206 @@ snd (isContr-HⁿKleinBottle n G) = ST.elim (λ _ → isSetPathImplicit) (isConnectedEM (3 +ℕ n))))) _ _) _ _) refl p .fst)) -H³⁺ⁿK²≅0 : (n : ℕ) (G : AbGroup ℓ) + +---- With general coefficients + +-- H⁰(K²,G) +H⁰[K²,G]≅G : (G : AbGroup ℓ) → AbGroupEquiv (coHomGr 0 G KleinBottle) G +H⁰[K²,G]≅G G = H⁰conn (∣ point ∣ + , (TR.elim (λ _ → isOfHLevelPath 2 (isOfHLevelTrunc 2) _ _) + (elimProp (λ _ → isOfHLevelTrunc 2 _ _) refl))) G + +-- H¹(K²,G) +H¹[K²,G]≅G×H¹[RP²,G] : (G : AbGroup ℓ) + → AbGroupEquiv (coHomGr 1 G KleinBottle) (AbDirProd G (coHomGr 1 G RP²)) +fst (H¹[K²,G]≅G×H¹[RP²,G] G) = isoToEquiv mainIso + where + F→ : (KleinBottle → EM G 1) → (RP² → EM G 1) + F→ f point = f point + F→ f (line i) = f (line1 i) + F→ f (square i j) = help i (~ j) + where + help : cong f (sym line1) ≡ cong f line1 + help = + lUnit (cong f (sym line1)) + ∙ cong (_∙ cong f (sym line1)) + (sym (lCancel _)) + ∙ sym (assoc _ _ _) + ∙ cong (sym (cong f line2) ∙_) (isCommΩEM-base 0 _ _ _) + ∙ PathP→compPathL (λ i j → f (square j i)) + + F← : (g : fst G) → (RP² → EM G 1) → KleinBottle → EM G 1 + F← g f point = f point + F← g f (line1 i) = f (line i) + F← g f (line2 i) = EM→ΩEM+1-gen 0 (f point) g i + F← g f (square i j) = help j i + where + l1 = cong f line + l2 = EM→ΩEM+1-gen 0 (f point) g + + help : Square (sym l1) l1 l2 l2 + help = compPathL→PathP + (cong₂ _∙_ refl (isCommΩEM-base 0 _ _ _) + ∙∙ assoc _ _ _ + ∙∙ cong (_∙ sym l1) (lCancel l2) + ∙∙ sym (lUnit _) + ∙∙ sym (cong (cong f) square)) + + mainIso : Iso (coHom 1 G KleinBottle) (fst G × coHom 1 G RP²) + Iso.fun mainIso = + ST.rec (isSet× (is-set (snd G)) squash₂) + λ f → (ΩEM+1→EM-gen 0 _ (cong f line2)) , ∣ F→ f ∣₂ + Iso.inv mainIso = uncurry λ g → ST.map (F← g) + Iso.rightInv mainIso = uncurry λ g + → ST.elim (λ _ → isOfHLevelPath 2 (isSet× (is-set (snd G)) squash₂) _ _) + λ f → ΣPathP ((Iso.leftInv (Iso-EM-ΩEM+1-gen 0 (f point)) g) + , cong ∣_∣₂ (funExt (elimSetRP² (λ _ → hLevelEM G 1 _ _) + refl λ i j → f (line i)))) + Iso.leftInv mainIso = ST.elim (λ _ → isSetPathImplicit) + λ f → cong ∣_∣₂ (funExt (elimSet (λ _ → hLevelEM G 1 _ _) + refl + (λ i j → f (line1 i)) + (flipSquare (Iso.rightInv (Iso-EM-ΩEM+1-gen 0 (f point)) (cong f line2))))) +snd (H¹[K²,G]≅G×H¹[RP²,G] G) = + makeIsGroupHom (ST.elim2 + (λ _ _ → isOfHLevelPath 2 lem _ _) + (ConnK².elim₁ (isConnectedEM 1) (λ _ → isPropΠ λ _ → lem _ _) embase + λ p1 q1 r1 + → ConnK².elim₁ (isConnectedEM 1) (λ _ → lem _ _) embase + λ p2 q2 r2 → ΣPathP (cong (ΩEM+1→EM 0) (cong₂+₁ q1 q2) + ∙ ΩEM+1→EM-hom 0 q1 q2 + , (cong ∣_∣₂ (funExt (elimSetRP² (λ _ → hLevelEM G 1 _ _) + refl + λ i j → (p1 i) +[ 1 ]ₖ (p2 i))))))) + where + lem = isSet× (is-set (snd G)) squash₂ + +H¹[K²,G]≅G×G[2] : (G : AbGroup ℓ) + → AbGroupEquiv (coHomGr 1 G KleinBottle) (AbDirProd G (G [ 2 ]ₜ)) +H¹[K²,G]≅G×G[2] G = + compGroupEquiv (H¹[K²,G]≅G×H¹[RP²,G] G) + (GroupEquivDirProd idGroupEquiv (H¹[RP²,G]≅G[2] G)) + +-- H²(K²,G) +private + H²K²-helperFun₁ : (G : AbGroup ℓ) (n : ℕ) + → (Σ[ p ∈ Ω (EM∙ G (2 +ℕ n)) .fst ] + Σ[ q ∈ Ω (EM∙ G (2 +ℕ n)) .fst ] Square (sym p) p q q) + → ((Σ[ p ∈ Ω (EM∙ G (2 +ℕ n)) .fst ] + p ≡ sym p)) + H²K²-helperFun₁ G n (p , q , r) = (p , λ i j + → hcomp (λ k → λ {(i = i0) → rUnitₖ (suc (suc n)) (p j) k + ; (i = i1) → rUnitₖ (suc (suc n)) (p (~ j)) k + ; (j = i0) → rCancelₖ (suc (suc n)) (q (~ i)) k + ; (j = i1) → rCancelₖ (suc (suc n)) (q (~ i)) k}) + (r (~ i) j -[ suc (suc n) ]ₖ q (~ i) )) + + H²K²-helperIso₁ : (G : AbGroup ℓ) (n : ℕ) → + Iso ∥ (Σ[ p ∈ Ω (EM∙ G (2 +ℕ n)) .fst ] + Σ[ q ∈ Ω (EM∙ G (2 +ℕ n)) .fst ] Square (sym p) p q q) ∥₂ + ∥ (Σ[ x ∈ EM G (2 +ℕ n) ] (Σ[ p ∈ Ω (EM G (2 +ℕ n) , x) .fst ] + Σ[ q ∈ Ω (EM G (2 +ℕ n) , x) .fst ] Square (sym p) p q q)) ∥₂ + Iso.fun (H²K²-helperIso₁ G n) = ST.map (0ₖ _ ,_) + Iso.inv (H²K²-helperIso₁ G n) = ST.rec squash₂ + (uncurry (EM-raw'-elim G (2 +ℕ n) + (λ _ → isOfHLevelΠ (3 +ℕ n) λ _ → isOfHLevelPlus' {n = suc n} 2 squash₂) + (EM-raw'-trivElim G (suc n) (λ _ + → isOfHLevelΠ (2 +ℕ n) λ _ → isOfHLevelPlus' {n = n} 2 squash₂) + ∣_∣₂))) + Iso.rightInv (H²K²-helperIso₁ G n) = ST.elim (λ _ → isSetPathImplicit) + (uncurry (EM-raw'-elim G (2 +ℕ n) + (λ _ → isOfHLevelΠ (3 +ℕ n) + λ _ → isOfHLevelPlus' {n = suc (suc n)} 1 (squash₂ _ _)) + (EM-raw'-trivElim G (suc n) (λ _ → isOfHLevelΠ (2 +ℕ n) + λ _ → isOfHLevelPlus' {n = suc n} 1 (squash₂ _ _)) + λ _ → refl))) + Iso.leftInv (H²K²-helperIso₁ G n) = ST.elim (λ _ → isSetPathImplicit) λ _ → refl + + H²K²-helperIso₂ : (G : AbGroup ℓ) (n : ℕ) → + Iso ∥ (Σ[ p ∈ Ω (EM∙ G (2 +ℕ n)) .fst ] + Σ[ q ∈ Ω (EM∙ G (2 +ℕ n)) .fst ] Square (sym p) p q q) ∥₂ + ∥ ((Σ[ p ∈ Ω (EM∙ G (2 +ℕ n)) .fst ] + p ≡ sym p)) ∥₂ + Iso.fun (H²K²-helperIso₂ G n) = ST.map (H²K²-helperFun₁ G n) + Iso.inv (H²K²-helperIso₂ G n) = ST.map (λ p → fst p , refl , sym (snd p)) + Iso.rightInv (H²K²-helperIso₂ G n) = ST.elim (λ _ → isSetPathImplicit) λ {(p , r) + → TR.rec (isProp→isOfHLevelSuc n (squash₂ _ _)) + (λ { P → cong ∣_∣₂ (main p P r)}) + ((F p .fst))} + where + F = isConnectedPath (suc n) (isConnectedPath (suc (suc n)) + (isConnectedEM (suc (suc n))) _ _) refl + main : (p : Ω (EM∙ G (2 +ℕ n)) .fst) → refl ≡ p + → (r : p ≡ sym p) + → H²K²-helperFun₁ G n (p , refl , sym r) ≡ (p , r) + main = (J> λ r → (ΣPathP (refl , sym (rUnit _) + ∙ λ i j k → rUnitₖ (suc (suc n)) (r j k) i))) + Iso.leftInv (H²K²-helperIso₂ G n) = ST.elim (λ _ → isSetPathImplicit) + (uncurry λ p → TR.rec (isProp→isOfHLevelSuc n (isPropΠ (λ _ → squash₂ _ _ ))) + (λ P → uncurry λ q → TR.rec (isProp→isOfHLevelSuc n (isPropΠ (λ _ → squash₂ _ _ ))) + (λ Q x → cong ∣_∣₂ (main p P q Q x)) + (F q .fst)) + (F p .fst)) + where + F = isConnectedPath (suc n) (isConnectedPath (suc (suc n)) + (isConnectedEM (suc (suc n))) _ _) refl + main : (p : _) → refl ≡ p → + (q : _) → refl ≡ q → + (x : Square (sym p) p q q) → + (fst (H²K²-helperFun₁ G n (p , q , x)) + , refl + , (λ i → snd (H²K²-helperFun₁ G n (p , q , x)) (~ i))) + ≡ (p , q , x) + main = J> (J> λ p → ΣPathP (refl , (ΣPathP (refl + , cong sym (sym (rUnit _)) + ∙ λ i j k → rUnitₖ (suc (suc n)) (p j k) i)))) + + Iso-H²⁺ⁿ[K²,G]-H²⁺ⁿ[RP²,G] : (G : AbGroup ℓ) (n : ℕ) + → Iso (coHom (2 +ℕ n) G KleinBottle) + (coHom (2 +ℕ n) G RP²) + Iso-H²⁺ⁿ[K²,G]-H²⁺ⁿ[RP²,G] G n = + compIso + (setTruncIso + (compIso K²FunCharacIso + (Σ-cong-iso-snd λ p → Σ-cong-iso-snd λ q + → Σ-cong-iso-snd λ r → equivToIso flipSquareEquiv))) + (compIso (invIso (H²K²-helperIso₁ G n)) + (compIso (H²K²-helperIso₂ G n) + (compIso (invIso (killFirstCompIsoGen G n)) + (setTruncIso (invIso RP²FunCharacIso))))) + +H²[RP²,G]≅H²[K²,G] : (G : AbGroup ℓ) + → AbGroupEquiv (coHomGr 2 G RP²) (coHomGr 2 G KleinBottle) +fst (H²[RP²,G]≅H²[K²,G] G) = isoToEquiv (invIso (Iso-H²⁺ⁿ[K²,G]-H²⁺ⁿ[RP²,G] G 0)) +snd (H²[RP²,G]≅H²[K²,G] G) = + makeIsGroupHom (ST.elim (λ _ → isSetΠ λ _ → isSetPathImplicit) + (RP²Conn.elim₂ (isConnectedEM 2) + (λ _ → isPropΠ λ _ → squash₂ _ _) + (0ₖ 2) + λ p → ST.elim (λ _ → isSetPathImplicit) + (RP²Conn.elim₂ (isConnectedEM 2) + (λ _ → squash₂ _ _) + (0ₖ 2) λ q + → cong ∣_∣₂ (funExt λ { point → refl + ; (line1 i) → refl + ; (line2 i) → refl + ; (square i i₁) → refl})))) + +H²⁺ⁿ[K²,G]≅H²⁺ⁿ[RP²,G] : (G : AbGroup ℓ) (n : ℕ) + → AbGroupEquiv (coHomGr (2 +ℕ n) G KleinBottle) + (coHomGr (2 +ℕ n) G RP²) +fst (H²⁺ⁿ[K²,G]≅H²⁺ⁿ[RP²,G] G n) = isoToEquiv (Iso-H²⁺ⁿ[K²,G]-H²⁺ⁿ[RP²,G] G n) +snd (H²⁺ⁿ[K²,G]≅H²⁺ⁿ[RP²,G] G zero) = invGroupEquiv (H²[RP²,G]≅H²[K²,G] G) .snd +snd (H²⁺ⁿ[K²,G]≅H²⁺ⁿ[RP²,G] G (suc n)) = + makeIsGroupHom λ _ _ → isContr→isProp + (isOfHLevelRetractFromIso 0 (equivToIso (fst (H³⁺ⁿ[RP²,G]≅0 G n))) + isContrUnit*) _ _ + +H²[K²,G]≅G/2 : (G : AbGroup ℓ) + → AbGroupEquiv (coHomGr 2 G KleinBottle) + (G /^ 2) +H²[K²,G]≅G/2 G = compGroupEquiv (H²⁺ⁿ[K²,G]≅H²⁺ⁿ[RP²,G] G 0) (H²[RP²,G]≅G/2 G) + +H³⁺ⁿ[K²,G]≅0 : (n : ℕ) (G : AbGroup ℓ) → AbGroupEquiv (coHomGr (3 +ℕ n) G KleinBottle) (trivialAbGroup {ℓ}) -fst (H³⁺ⁿK²≅0 n G) = isContr→Equiv (isContr-HⁿKleinBottle n G) isContrUnit* -snd (H³⁺ⁿK²≅0 n G) = makeIsGroupHom λ _ _ → refl +H³⁺ⁿ[K²,G]≅0 n G = compGroupEquiv (H²⁺ⁿ[K²,G]≅H²⁺ⁿ[RP²,G] G (suc n)) (H³⁺ⁿ[RP²,G]≅0 G n) diff --git a/Cubical/Cohomology/EilenbergMacLane/Groups/RP2.agda b/Cubical/Cohomology/EilenbergMacLane/Groups/RP2.agda index c8f381b49a..274b6cd5f5 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Groups/RP2.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Groups/RP2.agda @@ -3,7 +3,7 @@ module Cubical.Cohomology.EilenbergMacLane.Groups.RP2 where open import Cubical.Cohomology.EilenbergMacLane.Base -open import Cubical.Cohomology.EilenbergMacLane.Groups.KleinBottle +open import Cubical.Cohomology.EilenbergMacLane.Groups.Connected open import Cubical.Homotopy.EilenbergMacLane.GroupStructure open import Cubical.Homotopy.EilenbergMacLane.Order2 @@ -17,21 +17,33 @@ open import Cubical.Foundations.Function open import Cubical.Foundations.HLevels open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Univalence +open import Cubical.Foundations.Equiv.HalfAdjoint open import Cubical.Foundations.Path open import Cubical.Foundations.GroupoidLaws open import Cubical.Data.Nat renaming (_+_ to _+ℕ_) open import Cubical.Data.Unit +open import Cubical.Data.Sigma open import Cubical.Data.Fin open import Cubical.Algebra.Group.Base +open import Cubical.Algebra.Group.Properties +open import Cubical.Algebra.Group.Morphisms open import Cubical.Algebra.Group.MorphismProperties +open import Cubical.Algebra.Group.Instances.IntMod open import Cubical.Algebra.AbGroup.Base +open import Cubical.Algebra.AbGroup +open import Cubical.Algebra.AbGroup.Instances.IntMod +open import Cubical.Algebra.Group.Subgroup +open import Cubical.Algebra.Group.QuotientGroup +open import Cubical.HITs.PropositionalTruncation as PT open import Cubical.HITs.SetTruncation as ST open import Cubical.HITs.Truncation as TR -open import Cubical.HITs.EilenbergMacLane1 +open import Cubical.HITs.EilenbergMacLane1 as EM1 open import Cubical.HITs.RPn +open import Cubical.HITs.SetQuotients as SQ open AbGroupStr @@ -88,6 +100,31 @@ module RP²Conn {B : (RP² → A) → Type ℓ} where (isConnectedPath 2 (isConnectedPath 3 conA _ _) _ _) refl sq .fst) +--- lemmas +Isoℤ/2-morph : {A : Type} (f : A ≃ fst ℤ/2) (0A : A) + → 0 ≡ fst f 0A → (_+'_ : A → A → A) (-m : A → A) + → (λ x → x) ≡ -m + → (e : IsAbGroup 0A _+'_ -m) + → IsGroupHom (AbGroup→Group (A , abgroupstr 0A _+'_ (λ x → -m x) e) .snd) + (fst f) ((ℤGroup/ 2) .snd) +Isoℤ/2-morph = + EquivJ (λ A f → (0A : A) → 0 ≡ fst f 0A → (_+'_ : A → A → A) (-m : A → A) + → (λ x → x) ≡ -m + → (e : IsAbGroup 0A _+'_ -m) + → IsGroupHom (AbGroup→Group (A , abgroupstr 0A _+'_ (λ x → -m x) e) .snd) + (fst f) ((ℤGroup/ 2) .snd)) + (J> λ _+'_ → J> + λ e → makeIsGroupHom (ℤ/2-elim (ℤ/2-elim (IsAbGroup.+IdR e fzero) + (IsAbGroup.+IdL e 1)) + (ℤ/2-elim (IsAbGroup.+IdR e 1) + (IsAbGroup.+InvR e 1)))) + +Iso-Ω²K₂-ℤ/2 : Iso (fst ((Ω^ 2) (EM∙ ℤ/2 2))) (fst ℤ/2) +Iso-Ω²K₂-ℤ/2 = + compIso (congIso (invIso (Iso-EM-ΩEM+1 {G = ℤ/2} 1))) + (invIso (Iso-EM-ΩEM+1 {G = ℤ/2} 0)) + + ----- H¹(RP²,ℤ/2) ------ H¹[RP²,ℤ/2]→ℤ/2 : coHom 1 ℤ/2 RP² → fst ℤ/2 @@ -210,3 +247,250 @@ fst (H³⁺ⁿ[RP²,G]≅G n G) = (cong ∣_∣₂ (characRP²Fun (λ _ → 0ₖ (3 +ℕ n))))))) isContrUnit*) snd (H³⁺ⁿ[RP²,G]≅G n G) = makeIsGroupHom λ _ _ → refl + + +---- H¹(RP², G) ----- +H⁰[RP²,G]≅G : ∀ {ℓ} (G : AbGroup ℓ) + → AbGroupEquiv (coHomGr 0 G RP²) G +H⁰[RP²,G]≅G G = + H⁰conn (∣ point ∣ₕ , TR.elim (λ _ → isOfHLevelPath 2 (isOfHLevelTrunc 2) _ _) + (elimPropRP² (λ _ → isOfHLevelTrunc 2 _ _) refl)) G + +----- H¹(RP², G) ------ +module _ {ℓ : Level} (G : AbGroup ℓ) where + private + G[2]path : (x : (G [ 2 ]ₜ) .fst) → _+_ (snd G) (fst x) (fst x) ≡ 0g (snd G) + G[2]path (x , p) = cong (_+_ (snd G) x) (sym (+IdR (snd G) x)) ∙ p + + G[2]path' : (x : (G [ 2 ]ₜ) .fst) → fst x ≡ -_ (snd G) (fst x) + G[2]path' x = (sym (+IdR (snd G) _) + ∙ cong (_+_ (snd G) (fst x)) (sym (+InvR (snd G) (fst x))) + ∙ (+Assoc (snd G) _ _ _)) + ∙∙ cong (λ w → _+_ (snd G) w (-_ (snd G) (fst x))) (G[2]path x) + ∙∙ +IdL (snd G) _ + + H¹[RP²,G]→G[2] : coHom 1 G RP² → (G [ 2 ]ₜ) .fst + H¹[RP²,G]→G[2] = + ST.rec (is-set (snd (G [ 2 ]ₜ))) + λ f → ΩEM+1→EM-gen {G = G} 0 (f point) (cong f line) + , cong (_+_ (snd G) (ΩEM+1→EM-gen 0 (f point) (cong f line))) + (+IdR (snd G) _) + ∙ sym (ΩEM+1→EM-gen-hom {G = G} 0 (f point) (cong f line) (cong f line)) + ∙ cong (ΩEM+1→EM-gen 0 (f point)) + (sym (cong-∙ f line line) + ∙ cong (cong f) (cong (line ∙_) square ∙ rCancel line) ) + ∙ ΩEM+1→EM-gen-refl 0 (f point) + + G[2]→H¹[RP²,G] : (G [ 2 ]ₜ) .fst → coHom 1 G RP² + G[2]→H¹[RP²,G] g = + ∣ (λ { point → embase + ; (line i) → emloop (fst g) i + ; (square i j) → + (cong emloop (G[2]path' g) + ∙ emloop-inv (AbGroup→Group G) (fst g)) i j }) ∣₂ + + private + G[2]≅H¹[RP²,G] : AbGroupEquiv (G [ 2 ]ₜ) (coHomGr 1 G RP²) + fst G[2]≅H¹[RP²,G] = isoToEquiv (invIso is) + where + is : Iso _ _ + Iso.fun is = H¹[RP²,G]→G[2] + Iso.inv is = G[2]→H¹[RP²,G] + Iso.rightInv is (g , p) = + Σ≡Prop (λ _ → is-set (snd G) _ _) + (Iso.leftInv (Iso-EM-ΩEM+1 0) g) + Iso.leftInv is = ST.elim (λ _ → isSetPathImplicit) + (RP²Conn.elim₁ (isConnectedEM 1) (λ _ → squash₂ _ _) + embase + λ p q → cong ∣_∣₂ + (funExt (elimSetRP² (λ _ → emsquash _ _) + refl + (flipSquare (Iso.rightInv (Iso-EM-ΩEM+1 {G = G} 0) p))))) + snd G[2]≅H¹[RP²,G] = makeIsGroupHom + λ x y → cong ∣_∣₂ + (funExt (elimSetRP² (λ _ → emsquash _ _) refl + (flipSquare + (EM→ΩEM+1-hom {G = G} 0 (fst x) (fst y) + ∙ sym (cong₂+₁ (emloop (fst x)) (emloop (fst y))))))) + + + H¹[RP²,G]≅G[2] : AbGroupEquiv (coHomGr 1 G RP²) (G [ 2 ]ₜ) + H¹[RP²,G]≅G[2] = invGroupEquiv G[2]≅H¹[RP²,G] + +----- H²(RP², G) ------ +module _ (G : AbGroup ℓ) where + private + ΩEM+1→EM-sym' : (p : fst (Ω (EM∙ G 2))) + → ΩEM+1→EM 1 (sym p) ≡ (-ₖ ΩEM+1→EM 1 p) + ΩEM+1→EM-sym' p = + ΩEM+1→EM-sym (suc zero) p + ∙ (sym (rUnitₖ 1 ((-ₖ ΩEM+1→EM 1 p))) + ∙∙ cong ((-ₖ ΩEM+1→EM 1 p) +ₖ_) (sym (ΩEM+1→EM-sym (suc zero) refl)) + ∙∙ rUnitₖ 1 ((-ₖ ΩEM+1→EM 1 p))) + + ΩEM+1→EM-sym'-refl : ΩEM+1→EM-sym' refl ≡ refl + ΩEM+1→EM-sym'-refl = + (λ i → ΩEM+1→EM-sym (suc zero) refl ∙ rUnit (sym (ΩEM+1→EM-sym (suc zero) refl)) (~ i)) + ∙ rCancel _ + + G/2-ord2 : (x : fst (G /^ 2)) → (- snd (G /^ 2)) x ≡ x + G/2-ord2 = SQ.elimProp (λ _ → SQ.squash/ _ _) + λ a → eq/ _ _ ∣ snd G .-_ a + , cong (snd G ._+_ (snd G .-_ a)) (+IdR (snd G) _) ∣₁ + + open EM2 (G /^ 2) G/2-ord2 + killFirstCompIsoGen : (n : ℕ) + → Iso ∥ (Σ[ x ∈ EM G (2 +ℕ n) ] (Σ[ p ∈ x ≡ x ] p ≡ sym p)) ∥₂ + ∥ (Σ[ p ∈ Ω (EM∙ G (2 +ℕ n)) .fst ] p ≡ sym p) ∥₂ + Iso.fun (killFirstCompIsoGen n) = + ST.rec squash₂ + (uncurry (TR.elim (λ _ → isOfHLevelPlus {n = 2 +ℕ n} 2 + (isOfHLevelPlus' {n = n} 2 (isSetΠ λ _ → squash₂))) + (EM-raw'-trivElim G (suc n) + (λ _ → isOfHLevelΠ (suc (suc n)) + λ _ → isOfHLevelPlus' {n = n} 2 squash₂) ∣_∣₂))) + Iso.inv (killFirstCompIsoGen n) = ST.map (0ₖ (2 +ℕ n) ,_) + Iso.rightInv (killFirstCompIsoGen n) = ST.elim (λ _ → isSetPathImplicit) λ _ → refl + Iso.leftInv (killFirstCompIsoGen n) = ST.elim (λ _ → isSetPathImplicit) + (uncurry (TR.elim (λ _ → isProp→isOfHLevelSuc (3 +ℕ n) + (isPropΠ (λ _ → squash₂ _ _))) + (EM-raw'-trivElim G (suc n) (λ _ → isProp→isOfHLevelSuc (suc n) + (isPropΠ λ _ → squash₂ _ _ )) + λ _ → refl))) + + H²RP²-Iso₁ : Iso (coHom 2 G RP²) ∥ (Σ[ p ∈ Ω (EM∙ G 2) .fst ] p ≡ sym p) ∥₂ + H²RP²-Iso₁ = compIso (setTruncIso RP²FunCharacIso) (killFirstCompIsoGen 0) + + H²RP²-Iso₂ : Iso ((Σ[ p ∈ Ω (EM∙ G 2) .fst ] p ≡ sym p)) (Σ[ p ∈ EM G 1 ] p ≡ -ₖ p) + H²RP²-Iso₂ = (Σ-cong-iso (invIso (Iso-EM-ΩEM+1 1)) + λ x → compIso (congIso (invIso (Iso-EM-ΩEM+1 1))) + (equivToIso (compPathrEquiv (ΩEM+1→EM-sym' x)))) + + RP²Fun-pres+ : (p q : (Ω^ 2) (EM∙ G 2) .fst) (x : _) + → RP²Fun _ _ p x +[ 2 ]ₖ RP²Fun _ _ q x ≡ RP²Fun _ _ (p ∙ q) x + RP²Fun-pres+ p q point = refl + RP²Fun-pres+ p q (line i) j = 0ₖ 2 + RP²Fun-pres+ p q (square i j) k = + hcomp (λ r → λ {(i = i0) → lem3 k j r + ; (i = i1) → lem2 k (~ r) j + ; (j = i0) → p (i ∨ ~ k) r + ; (j = i1) → p (~ i ∧ k) (~ r) + ; (k = i0) → cong₂+₂ 0 (p i) (q i) (~ r) j + ; (k = i1) → lem1 _ refl p (sym q) r i j}) + ((p i ∙ q i) j) + where + lem1 : ∀ {ℓ} {A : Type ℓ} (x : A) (p : x ≡ x) (P Q : refl ≡ p) + → Cube (λ i j → (P i ∙ Q (~ i)) j) (P ∙ sym Q) + (λ k → compPath-filler refl p (~ k)) + (λ k → compPath-filler' p refl (~ k)) + (λ i j → P j i) λ i j → P (~ j) (~ i) + lem1 x = J> λ Q → (λ i j k → lUnit (Q (~ j)) (~ i) k) ▷ lUnit (sym Q) + + lem2 : cong₂+₂ {G = G} 0 refl refl ≡ rUnit refl + lem2 = sym (rUnit _) + + lem3 : Cube (λ j r → cong₂+₂ {G = G} 0 refl refl (~ r) j) + (λ j r → compPath-filler (refl {x = 0ₖ 2}) refl (~ r) j) + (λ k r → p (~ k) r) (λ k r → p k (~ r)) + (λ j i → (rUnit (refl {x = 0ₖ 2}) i1) i) + (λ _ _ → 0ₖ 2) + lem3 = (λ i j r → lem2 i (~ r) j) + ◁ (λ k j r → + hcomp (λ i → λ {(j = i0) → p (~ k) r + ; (j = i1) → p k (~ r) + ; (r = i0) → rUnit (λ _ → 0ₖ 2) i j + ; (r = i1) → 0ₖ 2 + ; (k = i0) → rUnit (λ _ → 0ₖ 2) (i ∧ ~ r) j + ; (k = i1) → rUnit (λ _ → 0ₖ 2) (i ∧ ~ r) j}) + (((sym≡flipSquare p) ∙ flipSquare≡cong-sym p) j k r)) + + H²RP²-Iso₁,₂-charac : (p : (Ω^ 2) (EM∙ G 2) .fst) + → ST.map (Iso.fun H²RP²-Iso₂) (Iso.fun H²RP²-Iso₁ ∣ RP²Fun _ _ p ∣₂) + ≡ ∣ embase , (cong (ΩEM+1→EM 1) p) ∣₂ + H²RP²-Iso₁,₂-charac p = cong ∣_∣₂ (ΣPathP (refl + , (λ i → cong (ΩEM+1→EM {G = G} 1) p ∙ ΩEM+1→EM-sym'-refl i) + ∙ sym (rUnit (cong (ΩEM+1→EM 1) p)))) + + H²RP²-Iso₁,₂+ : (p q : (Ω^ 2) (EM∙ G 2) .fst) + → ST.map (Iso.fun H²RP²-Iso₂) (Iso.fun H²RP²-Iso₁ (∣ RP²Fun _ _ p ∣₂ +ₕ ∣ RP²Fun _ _ q ∣₂)) + ≡ ∣ embase , cong (ΩEM+1→EM 1) p ∙ cong (ΩEM+1→EM 1) q ∣₂ + H²RP²-Iso₁,₂+ p q = cong (ST.map (Iso.fun H²RP²-Iso₂) ∘ Iso.fun H²RP²-Iso₁) + (cong ∣_∣₂ (funExt (RP²Fun-pres+ p q))) + ∙ H²RP²-Iso₁,₂-charac (p ∙ q) + ∙ cong ∣_∣₂ (ΣPathP (refl , cong-∙ (ΩEM+1→EM 1) p q)) + + H²RP²-Iso₃→ : (p : EM G 1) → (p ≡ -[ 1 ]ₖ p) → fst (G /^ 2) + H²RP²-Iso₃→ = EM1.elimSet (AbGroup→Group G) (λ _ → isSetΠ λ _ → squash/) + (λ p → [ ΩEM+1→EM 0 p ]) + λ g → toPathP (funExt λ q + → cong [_] (transportRefl _ + ∙ cong (ΩEM+1→EM 0) + ((λ j → transp (λ i → Path (EM G 1) (emloop g (~ i ∧ ~ j)) (emloop g (i ∨ j))) j + (doubleCompPath-filler (emloop g) q (emloop g) j)) + ∙ doubleCompPath≡compPath _ _ _ + ∙ cong (emloop g ∙_) (isCommΩEM {G = G} 0 q (emloop g)) + ∙ assoc (emloop g) (emloop g) q) + ∙ ΩEM+1→EM-hom 0 (emloop g ∙ emloop g) q) + ∙ eq/ _ _ ∣ g + , cong (snd G ._+_ g) (+IdR (snd G) _) + ∙ sym (+IdR (snd G) (snd G ._+_ g g)) + ∙ cong₂ (snd G ._+_) + (sym (Iso.leftInv (Iso-EM-ΩEM+1 0) _) + ∙ cong (ΩEM+1→EM 0) (emloop-comp _ g g)) + (sym (+InvR (snd G) (ΩEM+1→EM 0 q))) + ∙ +Assoc (snd G) _ _ _ ∣₁) + + H²RP²-Iso₃ : Iso ∥ (Σ[ p ∈ EM G 1 ] p ≡ -ₖ p) ∥₂ (fst (G /^ 2)) + Iso.fun H²RP²-Iso₃ = ST.rec squash/ (uncurry H²RP²-Iso₃→) + Iso.inv H²RP²-Iso₃ = + SQ.elim (λ _ → squash₂) (λ a → ∣ embase , emloop a ∣₂) + λ a b → PT.rec (squash₂ _ _) + (uncurry λ x y → cong ∣_∣₂ (ΣPathP ((emloop x) + , compPathL→PathP + (cong₂ _∙_ (sym (emloop-inv _ x)) + (cong (emloop a ∙_) (sym (emloop-inv _ x)) + ∙ sym (EM→ΩEM+1-hom {G = G} 0 a (AbGroupStr.-_ (snd G) x))) + ∙ sym (EM→ΩEM+1-hom {G = G} 0 _ _) + ∙ cong emloop (cong (_+_ (snd G) (AbGroupStr.-_ (snd G) x)) + (+Comm (snd G) _ _) + ∙ +Assoc (snd G) _ _ _ + ∙ cong (λ w → _+_ (snd G) w a) + (sym (GroupTheory.invDistr (AbGroup→Group G) x x) + ∙ cong (AbGroupStr.-_ (snd G)) + (cong (snd G ._+_ x ) (sym (+IdR (snd G) _)) ∙ y) + ∙ GroupTheory.invDistr (AbGroup→Group G) a _ + ∙ cong (λ w → _+_ (snd G) w (AbGroupStr.-_ (snd G) a)) + (GroupTheory.invInv (AbGroup→Group G) b)) + ∙ (sym (+Assoc (snd G) _ _ _) + ∙ cong (_+_ (snd G) b) (+InvL (snd G) a)) + ∙ +IdR (snd G) b))))) + Iso.rightInv H²RP²-Iso₃ = SQ.elimProp (λ _ → squash/ _ _) + λ a → cong [_] (Iso.leftInv (Iso-EM-ΩEM+1 0) a) + Iso.leftInv H²RP²-Iso₃ = ST.elim (λ _ → isSetPathImplicit) + (uncurry (EM1.elimProp (AbGroup→Group G) (λ _ → isPropΠ λ _ → squash₂ _ _) + λ p → cong ∣_∣₂ (ΣPathP (refl , (Iso.rightInv (Iso-EM-ΩEM+1 0) p))))) + + H²[RP²,G]≅G/2 : AbGroupEquiv (coHomGr 2 G RP²) (G /^ 2) + fst H²[RP²,G]≅G/2 = isoToEquiv is + where + is : Iso _ _ + is = compIso (compIso H²RP²-Iso₁ (setTruncIso H²RP²-Iso₂)) H²RP²-Iso₃ + snd H²[RP²,G]≅G/2 = + makeIsGroupHom (ST.elim2 (λ _ _ → isOfHLevelPath 2 squash/ _ _) + (RP²Conn.elim₂ (isConnectedEM 2) (λ _ → isPropΠ λ _ → squash/ _ _) + (0ₖ 2) λ p → RP²Conn.elim₂ (isConnectedEM 2) (λ _ → squash/ _ _) + (0ₖ 2) λ q → cong (Iso.fun H²RP²-Iso₃) (H²RP²-Iso₁,₂+ p q) + ∙ cong [_] (ΩEM+1→EM-hom 0 (cong (ΩEM+1→EM 1) p) + (cong (ΩEM+1→EM 1) q)) + ∙ cong₂ ((G /^ 2) .snd ._+_) + (cong (Iso.fun H²RP²-Iso₃) (sym (H²RP²-Iso₁,₂-charac p))) + (cong (Iso.fun H²RP²-Iso₃) (sym (H²RP²-Iso₁,₂-charac q))))) + + H³⁺ⁿ[RP²,G]≅0 : (n : ℕ) → AbGroupEquiv (coHomGr (3 +ℕ n) G RP²) (trivialAbGroup {ℓ}) + fst (H³⁺ⁿ[RP²,G]≅0 n) = isContr→≃Unit* (0ₕ _ + , ST.elim (λ _ → isSetPathImplicit) + (RP²Conn.elim₃ (isConnectedSubtr 4 n + (subst (λ k → isConnected k (EM G (3 +ℕ n))) + (+-comm 4 n) (isConnectedEM (3 +ℕ n)))) + (λ _ → squash₂ _ _) (0ₖ _) refl)) + snd (H³⁺ⁿ[RP²,G]≅0 n) = makeIsGroupHom λ _ _ → refl diff --git a/Cubical/Cohomology/EilenbergMacLane/Groups/RP2wedgeS1.agda b/Cubical/Cohomology/EilenbergMacLane/Groups/RP2wedgeS1.agda index 3d31c7e09c..cc854b7092 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Groups/RP2wedgeS1.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Groups/RP2wedgeS1.agda @@ -29,6 +29,7 @@ open import Cubical.Algebra.Group.MorphismProperties open import Cubical.Algebra.Group.Morphisms open import Cubical.Algebra.AbGroup.Base open import Cubical.Algebra.AbGroup.Instances.Unit +open import Cubical.Algebra.AbGroup.Instances.IntMod open import Cubical.HITs.SetTruncation as ST open import Cubical.HITs.Truncation as TR diff --git a/Cubical/Cohomology/EilenbergMacLane/Groups/RPinf.agda b/Cubical/Cohomology/EilenbergMacLane/Groups/RPinf.agda new file mode 100644 index 0000000000..ab38f77ec5 --- /dev/null +++ b/Cubical/Cohomology/EilenbergMacLane/Groups/RPinf.agda @@ -0,0 +1,282 @@ +{-# OPTIONS --safe --lossy-unification #-} + +module Cubical.Cohomology.EilenbergMacLane.Groups.RPinf where + +open import Cubical.Cohomology.EilenbergMacLane.Base +open import Cubical.Cohomology.EilenbergMacLane.Gysin + +open import Cubical.Homotopy.EilenbergMacLane.CupProduct +open import Cubical.Homotopy.EilenbergMacLane.GroupStructure +open import Cubical.Homotopy.EilenbergMacLane.Base +open import Cubical.Homotopy.EilenbergMacLane.Properties +open import Cubical.Homotopy.Loopspace +open import Cubical.Homotopy.EilenbergMacLane.Order2 + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Function +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Pointed +open import Cubical.Foundations.Pointed.Homogeneous +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Equiv.HalfAdjoint +open import Cubical.Foundations.Univalence + +open import Cubical.HITs.SetTruncation as ST +open import Cubical.HITs.EilenbergMacLane1 +open import Cubical.HITs.Susp + +open import Cubical.Relation.Nullary + +open import Cubical.Data.Empty as ⊥ +open import Cubical.Data.Unit +open import Cubical.Data.Nat +open import Cubical.Data.Sigma +open import Cubical.Data.Bool hiding (_≤_) +open import Cubical.Data.Fin.Base + +open import Cubical.Algebra.AbGroup.Base +open import Cubical.Algebra.Ring +open import Cubical.Algebra.CommRing +open import Cubical.Algebra.CommRing.Instances.IntMod +open import Cubical.Algebra.Group.Instances.IntMod +open import Cubical.Algebra.AbGroup.Instances.IntMod + +open RingStr renaming (_+_ to _+r_) +open PlusBis + +open Iso + +-- move to Cohomology GroupStr or somethign +EM-ℤ/2ˣ∙ : (n : ℕ) → EM ℤ/2 ˣ n +EM-ℤ/2ˣ∙ = 0ˣ (EM ℤ/2) 0ₖ + +private + nonConst→∙ : (b : EM ℤ/2 1) → Type _ + nonConst→∙ b = + Σ[ F ∈ Susp∙ (embase ≡ b) →∙ EM∙ (CommRing→AbGroup ℤ/2CommRing) 1 ] + (¬ F ≡ const∙ _ _) + + Iso-SuspΩEM₁→∙EM₁-Bool→∙Bool : + Iso (Susp∙ (Ω (EM∙ ℤ/2 1) .fst) + →∙ EM∙ ℤ/2 1) + ((Bool , true) →∙ (Bool , true)) + Iso-SuspΩEM₁→∙EM₁-Bool→∙Bool = compIso + (invIso (ΩSuspAdjointIso {A = Ω (EM∙ ℤ/2 1)})) + (compIso (post∘∙equiv (lem , refl)) (pre∘∙equiv (lem , refl))) + where + lem = isoToEquiv + (compIso (invIso (Iso-EM-ΩEM+1 {G = ℤ/2} 0)) + (invIso (Bool≅ℤGroup/2 .fst))) + + Σ¬Iso : ∀ {ℓ} {B A : Type ℓ} + → (e : A ≃ B) + → {x : A} + → Iso (Σ[ y ∈ A ] ¬ y ≡ x) + (Σ[ y ∈ B ] ¬ y ≡ fst e x) + Σ¬Iso {B = B} = + EquivJ (λ A e → {x : A} + → Iso (Σ[ y ∈ A ] ¬ y ≡ x) + (Σ[ y ∈ B ] ¬ y ≡ fst e x)) idIso + + nonConst→∙Iso : Iso (nonConst→∙ embase) (Σ[ F ∈ Bool ] ¬ F ≡ true) + nonConst→∙Iso = + Σ¬Iso (isoToEquiv + (compIso Iso-SuspΩEM₁→∙EM₁-Bool→∙Bool + Iso-Bool→∙Bool-Bool)) + + isProp-nonConst→∙ : (b : EM ℤ/2 1) → isProp (nonConst→∙ b) + isProp-nonConst→∙ = EM→Prop _ 0 (λ _ → isPropIsProp) + (isOfHLevelRetractFromIso 1 nonConst→∙Iso + (isContr→isProp ((false , true≢false ∘ sym) + , λ { (false , p) → Σ≡Prop (λ _ → isProp¬ _) refl + ; (true , p) → ⊥.rec (p refl)}))) + +eRP∞∙ : Susp∙ (Ω (EM∙ ℤ/2 1) .fst) →∙ EM∙ ℤ/2 1 +fst eRP∞∙ north = embase +fst eRP∞∙ south = embase +fst eRP∞∙ (merid a i) = a i +snd eRP∞∙ = refl + +eRP∞-nonConst : nonConst→∙ embase +fst eRP∞-nonConst = eRP∞∙ +snd eRP∞-nonConst p = true≢false true≡false + where + true≡false : true ≡ false + true≡false i = + Iso.fun (compIso Iso-SuspΩEM₁→∙EM₁-Bool→∙Bool Iso-Bool→∙Bool-Bool) + (p (~ i)) + +eRP∞ : (b : EM ℤ/2 1) → nonConst→∙ b +eRP∞ = EM→Prop ℤ/2 0 isProp-nonConst→∙ eRP∞-nonConst + +module ThomRP∞ = Thom (EM∙ ℤ/2 1) (0ₖ 1 ≡_) refl + (isConnectedEM 1) + ℤ/2CommRing + +open ThomRP∞ +isContrE : isContr E +isContrE = isContrSingl _ + +module conRP∞ = + con 0 (((compEquiv (isoToEquiv (invIso (Iso-EM-ΩEM+1 0))) + (isoToEquiv (invIso (fst Bool≅ℤGroup/2))))) , refl) + (λ b → eRP∞ b .fst) + (Iso.inv (congIso (compIso Iso-SuspΩEM₁→∙EM₁-Bool→∙Bool + Iso-Bool→∙Bool-Bool)) λ i → false) + +open conRP∞ +ϕ-raw-contrRP∞ : (n : ℕ) + → ((EM ℤ/2 1 → EM ℤ/2 n)) + ≃ (EM∙ ℤ/2 1 →∙ EM∙ ℤ/2 (n +' 1)) +ϕ-raw-contrRP∞ n = ϕ-raw-contr n isContrE + +⌣RP∞ : (n : ℕ) + → (EM ℤ/2 1 → EM ℤ/2 n) + → EM∙ ℤ/2 1 →∙ EM∙ ℤ/2 (n +' 1) +fst (⌣RP∞ n f) x = (f x) ⌣[ ℤ/2Ring R]ₖ x +snd (⌣RP∞ n f) = ⌣ₖ-0ₖ _ _ (f (0ₖ 1)) + +⌣RP∞' : (n : ℕ) + → (EM ℤ/2 1 → EM ℤ/2 n) + → EM∙ ℤ/2 1 →∙ EM∙ ℤ/2 (1 +' n) +fst (⌣RP∞' n f) x = x ⌣[ ℤ/2Ring R]ₖ (f x) +snd (⌣RP∞' n f) = 0ₖ-⌣ₖ _ _ (f (0ₖ 1)) + +⌣RP∞≡⌣RP∞' : (n : ℕ) → + PathP (λ i → + (EM ℤ/2 1 → EM ℤ/2 n) → + EM∙ ℤ/2 1 →∙ EM∙ ℤ/2 (+'-comm n 1 i)) + (⌣RP∞ n) + (⌣RP∞' n) +⌣RP∞≡⌣RP∞' n = funExt λ f → + →∙HomogeneousPathP refl (cong (EM∙ ℤ/2) (+'-comm n 1)) + (isHomogeneousEM _) + (funExt λ x → lem f x) + where + lem : (f : EM ℤ/2 1 → EM ℤ/2 n) + (x : EM ℤ/2 1) + → PathP (λ i → EM ℤ/2 (+'-comm n 1 i)) + (f x ⌣[ ℤ/2Ring R]ₖ x) (x ⌣[ ℤ/2Ring R]ₖ f x) + lem f x = toPathP (sym (⌣ₖ-commℤ/2 1 n x (f x))) + +⌣RP∞IsEq : (n : ℕ) → isEquiv (⌣RP∞ n) +⌣RP∞IsEq n = + subst isEquiv + (funExt (λ f → →∙Homogeneous≡ (isHomogeneousEM _) + (λ i x → f x ⌣[ ℤ/2Ring R]ₖ (eRP∞-lem x i)))) + (ϕ-raw-contrRP∞ n .snd) + where + help : (g : _) → (λ i → eRP∞ (emloop g i) .fst .fst south) + ≡ emloop g + help g j i = + hcomp (λ k → λ {(i = i0) → embase + ; (i = i1) → emloop g k + ; (j = i0) → eRP∞ (emloop g i) .fst .fst + (merid (λ w → emloop g (i ∧ w)) k) + ; (j = i1) → emloop g (i ∧ k)}) + (eRP∞ (emloop g i) .fst .snd j) + + eRP∞-lem : (x : _) → eRP∞ x .fst .fst south ≡ x + eRP∞-lem = EM-raw'-elim _ 1 (λ _ → hLevelEM _ 1 _ _) + λ { embase-raw → refl ; (emloop-raw g i) j → help g j i } + +abstract + ⌣RP∞'IsEq : (n : ℕ) → isEquiv (⌣RP∞' n) + ⌣RP∞'IsEq n = transport (λ i → isEquiv (⌣RP∞≡⌣RP∞' n i)) (⌣RP∞IsEq n) + +⌣RP∞Equiv : (n : ℕ) + → (EM ℤ/2 1 → EM ℤ/2 n) + ≃ (EM∙ ℤ/2 1 →∙ EM∙ ℤ/2 (n +' 1)) +fst (⌣RP∞Equiv n) = ⌣RP∞ n +snd (⌣RP∞Equiv n) = ⌣RP∞IsEq n + +⌣RP∞'Equiv : (n : ℕ) + → (EM ℤ/2 1 → EM ℤ/2 n) + ≃ (EM∙ ℤ/2 1 →∙ EM∙ ℤ/2 (1 +' n)) +fst (⌣RP∞'Equiv n) = ⌣RP∞' n +snd (⌣RP∞'Equiv n) = ⌣RP∞'IsEq n + ++'-suc₁ : (n : ℕ) → 1 +' n ≡ suc n ++'-suc₁ zero = refl ++'-suc₁ (suc n) = refl + +⌣RP∞''Equiv : (n : ℕ) + → (EM ℤ/2 1 → EM ℤ/2 n) + ≃ (EM∙ ℤ/2 1 →∙ EM∙ ℤ/2 (suc n)) +⌣RP∞''Equiv n = + compEquiv (⌣RP∞'Equiv n) + (isoToEquiv (pre∘∙equiv + ((pathToEquiv (cong (EM ℤ/2) (+'-suc₁ n))) + , (subst-EM-0ₖ (+'-suc₁ n))))) + +RP→Charac₀ : Iso (EM ℤ/2 1 → ℤ/2 .fst) + (ℤ/2 .fst) +Iso.fun RP→Charac₀ f = f embase +Iso.inv RP→Charac₀ a = λ _ → a +Iso.rightInv RP→Charac₀ a = refl +Iso.leftInv RP→Charac₀ f = + funExt (EM→Prop _ 0 (λ _ → is-set (snd ℤ/2Ring) _ _) refl) + +RP→EM-ℤ/2-CharacIso : (n : ℕ) + → Iso (EM ℤ/2 1 → EM ℤ/2 n) + ((EM ℤ/2) ˣ n) +RP→EM-ℤ/2-CharacIso zero = RP→Charac₀ -- RP→Charac₀ +RP→EM-ℤ/2-CharacIso (suc n) = + compIso (EM→-charac {A = EM∙ ℤ/2 1} (suc n)) + (prodIso + (compIso help (RP→EM-ℤ/2-CharacIso n)) + idIso) + where + help : Iso (EM∙ ℤ/2 1 →∙ EM∙ ℤ/2 (suc n)) + (EM ℤ/2 1 → EM ℤ/2 n) + help = equivToIso (invEquiv (⌣RP∞''Equiv n)) + +∥EM-ℤ/2ˣ∥₀-Iso : (n : ℕ) → Iso ∥ EM ℤ/2 ˣ n ∥₂ (fst ℤ/2) +∥EM-ℤ/2ˣ∥₀-Iso zero = setTruncIdempotentIso (is-set (snd ℤ/2Ring)) +∥EM-ℤ/2ˣ∥₀-Iso (suc n) = + compIso + (compIso + setTruncOfProdIso + (compIso (Σ-cong-iso-snd λ _ + → equivToIso + (isContr→≃Unit (∣ 0ₖ (suc n) ∣₂ + , ST.elim (λ _ → isSetPathImplicit) + (EM→Prop _ _ (λ _ → squash₂ _ _) refl)))) + rUnit×Iso)) + (∥EM-ℤ/2ˣ∥₀-Iso n) + +⌣RP∞''Equiv∙ : (n : ℕ) + → ⌣RP∞''Equiv n .fst (λ _ → 0ₖ n) ≡ const∙ _ _ +⌣RP∞''Equiv∙ n = →∙Homogeneous≡ (isHomogeneousEM _) + (funExt λ x → cong (subst (EM ℤ/2) (+'-suc₁ n)) (⌣ₖ-0ₖ 1 n x) + ∙ subst-EM∙ (+'-suc₁ n) .snd) + +cohomRP∞Iso : (n : ℕ) → Iso (coHom n ℤ/2 (EM ℤ/2 1)) (ℤ/2 .fst) +cohomRP∞Iso n = compIso (setTruncIso (RP→EM-ℤ/2-CharacIso n)) (∥EM-ℤ/2ˣ∥₀-Iso n) + +RP→EM-ℤ/2-CharacIso∙ : (n : ℕ) + → Iso.fun (RP→EM-ℤ/2-CharacIso n) (λ _ → 0ₖ n) ≡ EM-ℤ/2ˣ∙ n +RP→EM-ℤ/2-CharacIso∙ zero = refl +RP→EM-ℤ/2-CharacIso∙ (suc n) = + ΣPathP (((cong (fun (RP→EM-ℤ/2-CharacIso n)) + (funExt λ x + → cong (λ f → invEq (⌣RP∞''Equiv n) f x) + (→∙Homogeneous≡ (isHomogeneousEM _) + (funExt (λ x → rCancelₖ (suc n) (0ₖ (suc n))))) + ∙ funExt⁻ (sym (cong (invEq (⌣RP∞''Equiv n)) (⌣RP∞''Equiv∙ n))) x + ∙ λ i → retEq (⌣RP∞''Equiv n) (λ _ → 0ₖ n) i x)) + ∙ RP→EM-ℤ/2-CharacIso∙ n) + , refl) + +HⁿRP∞≅ℤ/2 : (n : ℕ) → AbGroupIso (coHomGr n ℤ/2 (EM ℤ/2 1)) ℤ/2 +fst (HⁿRP∞≅ℤ/2 n) = cohomRP∞Iso n +snd (HⁿRP∞≅ℤ/2 n) = pres0→GroupIsoℤ/2 (isoToEquiv (cohomRP∞Iso n)) (cohomRP∞Iso∙ n) + where + ∥EM-ℤ/2ˣ∥₀-Iso∙ : (n : ℕ) → Iso.fun (∥EM-ℤ/2ˣ∥₀-Iso n) ∣ EM-ℤ/2ˣ∙ n ∣₂ ≡ fzero + ∥EM-ℤ/2ˣ∥₀-Iso∙ zero = refl + ∥EM-ℤ/2ˣ∥₀-Iso∙ (suc n) = ∥EM-ℤ/2ˣ∥₀-Iso∙ n + + cohomRP∞Iso∙ : (n : ℕ) → cohomRP∞Iso n .fun (0ₕ n) ≡ fzero + cohomRP∞Iso∙ n = cong (Iso.fun (∥EM-ℤ/2ˣ∥₀-Iso n) ∘ ∣_∣₂) (RP→EM-ℤ/2-CharacIso∙ n) + ∙ ∥EM-ℤ/2ˣ∥₀-Iso∙ n diff --git a/Cubical/Cohomology/EilenbergMacLane/Groups/Sn.agda b/Cubical/Cohomology/EilenbergMacLane/Groups/Sn.agda index e71c8db909..099a4fdada 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Groups/Sn.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Groups/Sn.agda @@ -22,8 +22,9 @@ open import Cubical.Foundations.Pointed open import Cubical.Foundations.Pointed.Homogeneous open import Cubical.Data.Nat renaming (_+_ to _+ℕ_) +open import Cubical.Data.Nat.Order open import Cubical.Data.Unit -open import Cubical.Data.Bool +open import Cubical.Data.Bool hiding (_≟_) open import Cubical.Data.Sigma open import Cubical.Algebra.Group.MorphismProperties @@ -286,6 +287,44 @@ module _ (G : AbGroup ℓ) where (isConnectedEM (suc (suc n))) (0ₖ _) (f north) .fst))) isContrUnit*) snd (Hⁿ[Sᵐ⁺ⁿ,G]≅0 (suc n) m) = makeIsGroupHom λ _ _ → refl + open import Cubical.Data.Sum as ⊎ + open import Cubical.Data.Empty as ⊥ + open import Cubical.Relation.Nullary + open import Cubical.Cohomology.EilenbergMacLane.Groups.Connected + + H⁰[Sⁿ,G]≅G : (n : ℕ) → AbGroupEquiv (coHomGr 0 G (S₊ (suc n))) G + H⁰[Sⁿ,G]≅G n = H⁰conn + (∣ ptSn (suc n) ∣ₕ + , (TR.elim (λ _ → isOfHLevelPath 2 (isOfHLevelTrunc 2) _ _) + (sphereElim n (λ _ → isProp→isOfHLevelSuc n (isOfHLevelTrunc 2 _ _)) + refl))) G + + Hⁿ[Sᵐ,G]Full : (n m : ℕ) + → (((n ≡ 0) ⊎ (n ≡ suc m)) + → AbGroupEquiv (coHomGr n G (S₊ (suc m))) G) + × ((¬ n ≡ 0) × (¬ (n ≡ suc m)) + → AbGroupEquiv (coHomGr n G (S₊ (suc m))) (trivialAbGroup {ℓ-zero})) + fst (Hⁿ[Sᵐ,G]Full zero m) _ = H⁰[Sⁿ,G]≅G m + snd (Hⁿ[Sᵐ,G]Full zero m) p = ⊥.rec (fst p refl) + Hⁿ[Sᵐ,G]Full (suc n) m with (n ≟ m) + ... | lt x = (λ { (inl x) → ⊥.rec (snotz x) + ; (inr p) → ⊥.rec (¬m = A[X1,···,Xn]/ ℤ/2CommRing 1 0 3 + + open GradedRing-⊕HIT-index + NatMonoid + (Poly ℤ/2CommRing) + (λ n → CommRing→AbGroup (PolyCommRing ℤ/2CommRing n) .snd) + + open RingStr (snd (H*R ℤ/2Ring RP²)) + renaming + ( 0r to 0H*RP + ; 1r to 1H*RP + ; _+_ to _+H*RP_ + ; -_ to -H*RP_ + ; _·_ to _cupS_ + ; +Assoc to +H*RPAssoc + ; +IdR to +H*RPIdR + ; +Comm to +H*RPComm + ; ·Assoc to ·H*RPAssoc + ; is-set to isSetH*RP + ; ·DistR+ to ·DistR+H* + ; ·DistL+ to ·DistL+H*) + + open RingStr (snd ℤ₂[X]) + renaming + ( 0r to 0Z₂X + ; 1r to 1Z₂X + ; _+_ to _+Z₂X_ + ; -_ to -Z₂X_ + ; _·_ to _·Z₂X_ + ; +Assoc to +Z₂XAssoc + ; +IdR to +Z₂XIdR + ; +Comm to +Z₂XComm + ; ·Assoc to ·Z₂XAssoc + ; is-set to isSetZ₂X + ; ·DistR+ to ·DistR+Z₂ + ; ·DistL+ to ·DistL+Z₂) + + private + H⁰[RP²,ℤ/2]≅ℤ/2 = H⁰[RP²,G]≅G ℤ/2 + + α* : fst (H*R ℤ/2Ring RP²) + α* = base 1 α + + γ* : fst (H*R ℤ/2Ring RP²) + γ* = base 2 γ + + α*²≡γ* : α* cupS α* ≡ γ* + α*²≡γ* = cong (base 2) α²≡γ + + α-isGen : base 1 (invEq (fst (H¹[RP²,ℤ/2]≅ℤ/2)) fone) ≡ α* + α-isGen = cong (base 1) + (cong (invEq (fst (H¹[RP²,ℤ/2]≅ℤ/2))) (sym α↦1) + ∙ retEq (fst (H¹[RP²,ℤ/2]≅ℤ/2)) α) + + γ-isGen : base 2 (invEq (fst (H²[RP²,ℤ/2]≅ℤ/2)) fone) ≡ γ* + γ-isGen = cong (base 2) + (cong (invEq (fst (H²[RP²,ℤ/2]≅ℤ/2))) (sym γ↦1') + ∙ retEq (fst (H²[RP²,ℤ/2]≅ℤ/2)) γ) + + ℤ₂[X]→H*[RP²,ℤ₂]-main' : (n : ℕ) (g : ℤ/2 .fst) → coHom n ℤ/2 RP² + ℤ₂[X]→H*[RP²,ℤ₂]-main' zero g = invEq (H⁰[RP²,ℤ/2]≅ℤ/2 .fst) g + ℤ₂[X]→H*[RP²,ℤ₂]-main' one g = invEq (H¹[RP²,ℤ/2]≅ℤ/2 .fst) g + ℤ₂[X]→H*[RP²,ℤ₂]-main' two g = invEq (H²[RP²,ℤ/2]≅ℤ/2 .fst) g + ℤ₂[X]→H*[RP²,ℤ₂]-main' (suc (suc (suc n))) g = 0ₕ (3 +ℕ n) + + ℤ₂[X]→H*[RP²,ℤ₂]-main : Vec ℕ 1 → ℤ/2 .fst → fst (H*R ℤ/2Ring RP²) + ℤ₂[X]→H*[RP²,ℤ₂]-main (n ∷ []) g = base n (ℤ₂[X]→H*[RP²,ℤ₂]-main' n g) + + ℤ₂[X]→H*[RP²,ℤ₂]-main-coh₁ : (r : Vec ℕ 1) → + ℤ₂[X]→H*[RP²,ℤ₂]-main r fzero ≡ neutral + ℤ₂[X]→H*[RP²,ℤ₂]-main-coh₁ (zero ∷ []) = base-neutral 0 + ℤ₂[X]→H*[RP²,ℤ₂]-main-coh₁ (one ∷ []) = + cong (base 1) (IsGroupHom.pres1 (invGroupEquiv (H¹[RP²,ℤ/2]≅ℤ/2) .snd)) + ∙ base-neutral 1 + ℤ₂[X]→H*[RP²,ℤ₂]-main-coh₁ (two ∷ []) = + cong (base 2) (IsGroupHom.pres1 (invGroupEquiv (H²[RP²,ℤ/2]≅ℤ/2) .snd)) + ∙ base-neutral 2 + ℤ₂[X]→H*[RP²,ℤ₂]-main-coh₁ (suc (suc (suc s)) ∷ []) = base-neutral _ + + ℤ₂[X]→H*[RP²,ℤ₂]-main-coh₂ : (r : Vec ℕ 1) (a b : Fin 2) + → (ℤ₂[X]→H*[RP²,ℤ₂]-main r a add ℤ₂[X]→H*[RP²,ℤ₂]-main r b) + ≡ ℤ₂[X]→H*[RP²,ℤ₂]-main r (a +ₘ b) + ℤ₂[X]→H*[RP²,ℤ₂]-main-coh₂ (zero ∷ []) a b = base-add 0 _ _ + ℤ₂[X]→H*[RP²,ℤ₂]-main-coh₂ (one ∷ []) a b = base-add 1 _ _ + ∙ cong (base 1) (sym (IsGroupHom.pres· (invGroupEquiv (H¹[RP²,ℤ/2]≅ℤ/2) .snd) a b)) + ℤ₂[X]→H*[RP²,ℤ₂]-main-coh₂ (two ∷ []) a b = base-add 2 _ _ + ∙ cong (base 2) (sym (IsGroupHom.pres· (invGroupEquiv (H²[RP²,ℤ/2]≅ℤ/2) .snd) a b)) + ℤ₂[X]→H*[RP²,ℤ₂]-main-coh₂ (suc (suc (suc x)) ∷ []) a b = + cong (base (suc (suc (suc x))) (0ₕ (suc (suc (suc x)))) add_) (base-neutral _) + ∙ addRid _ + + ℤ₂[X]→H*[RP²,ℤ₂]-fun : ℤ₂[x] → fst (H*R ℤ/2Ring RP²) + ℤ₂[X]→H*[RP²,ℤ₂]-fun = + DS-Rec-Set.f _ _ _ _ isSetH*RP + neutral + ℤ₂[X]→H*[RP²,ℤ₂]-main + _add_ + addAssoc + addRid + addComm + ℤ₂[X]→H*[RP²,ℤ₂]-main-coh₁ + ℤ₂[X]→H*[RP²,ℤ₂]-main-coh₂ + + private + isContrH³⁺ⁿ[RP²,G] : ∀ {ℓ} (n : ℕ) (G : AbGroup ℓ) → isContr (coHom (3 +ℕ n) G RP²) + isContrH³⁺ⁿ[RP²,G] n G = + isOfHLevelRetractFromIso 0 + (equivToIso (fst (H³⁺ⁿ[RP²,G]≅0 G n))) isContrUnit* + + ℤ/2[X]→H*[RP²,ℤ/2]-pres· : (x y : ℤ₂[x]) + → ℤ₂[X]→H*[RP²,ℤ₂]-fun (RingStr._·_ (snd ℤ₂[X]) x y) + ≡ (ℤ₂[X]→H*[RP²,ℤ₂]-fun x cupS ℤ₂[X]→H*[RP²,ℤ₂]-fun y) + ℤ/2[X]→H*[RP²,ℤ/2]-pres· = + DS-Ind-Prop.f _ _ _ _ + (λ _ → isPropΠ λ _ → trunc _ _) + (λ _ → refl) + (λ v a → + DS-Ind-Prop.f _ _ _ _ + (λ _ → trunc _ _) + (cong (ℤ₂[X]→H*[RP²,ℤ₂]-fun) + (0RightAnnihilates ℤ₂[X] (base v a)) + ∙ sym (0RightAnnihilates (H*R ℤ/2Ring RP²) + (ℤ₂[X]→H*[RP²,ℤ₂]-fun (base v a)))) + (λ w b → main v w a b) + λ {x} {y} p q → cong ℤ₂[X]→H*[RP²,ℤ₂]-fun (·DistR+Z₂ (base v a) x y) + ∙ cong₂ _add_ p q + ∙ sym (·DistR+H* (ℤ₂[X]→H*[RP²,ℤ₂]-fun (base v a)) + (ℤ₂[X]→H*[RP²,ℤ₂]-fun x) + (ℤ₂[X]→H*[RP²,ℤ₂]-fun y))) + λ {x} {y} p q z + → cong (ℤ₂[X]→H*[RP²,ℤ₂]-fun) + (·DistL+Z₂ x y z) + ∙ cong₂ _add_ (p z) (q z) + where + main-main : (v w : Vec ℕ 1) + → ℤ₂[X]→H*[RP²,ℤ₂]-fun (base v fone ·Z₂X base w fone) + ≡ ℤ₂[X]→H*[RP²,ℤ₂]-fun (base v fone) + cupS (ℤ₂[X]→H*[RP²,ℤ₂]-fun (base w fone)) + main-main (zero ∷ []) (w ∷ []) = + cong (ℤ₂[X]→H*[RP²,ℤ₂]-fun) + (RingStr.·IdL (snd ℤ₂[X]) (base (w ∷ []) fone)) + ∙ sym (RingStr.·IdL (snd (H*R ℤ/2Ring RP²)) + (ℤ₂[X]→H*[RP²,ℤ₂]-fun (base (w ∷ []) fone))) + main-main (suc v ∷ []) (zero ∷ []) = + cong (ℤ₂[X]→H*[RP²,ℤ₂]-fun) + (RingStr.·IdR (snd ℤ₂[X]) (base (suc v ∷ []) fone)) + ∙ sym (RingStr.·IdR (snd (H*R ℤ/2Ring RP²)) + (ℤ₂[X]→H*[RP²,ℤ₂]-fun (base (suc v ∷ []) fone))) + main-main (one ∷ []) (one ∷ []) = + γ-isGen ∙ sym α*²≡γ* ∙ cong (λ x → x cupS x) (sym (α-isGen)) + main-main (one ∷ []) (suc (suc w₁) ∷ []) = + cong (base (suc (suc (suc w₁)))) + (isContr→isProp (isContrH³⁺ⁿ[RP²,G] w₁ ℤ/2) _ _) + main-main (suc (suc v) ∷ []) (suc w ∷ []) = + cong (base (suc (suc v) +ℕ suc w)) + (isContr→isProp + (subst (λ k → isContr (coHom (suc (suc k)) ℤ/2 RP²)) (sym (+-suc v w)) + (isContrH³⁺ⁿ[RP²,G] (v +ℕ w) ℤ/2)) _ (0ₕ _)) + ∙ (base-neutral _ + ∙ sym (base-neutral _)) + ∙ cong (base (suc (suc v) +' suc w)) + (isContr→isProp (isContrH³⁺ⁿ[RP²,G] (v +ℕ w) ℤ/2) (0ₕ _) _) + + main : (v w : Vec ℕ 1) (a b : ℤ/2 .fst) + → ℤ₂[X]→H*[RP²,ℤ₂]-fun (base v a ·Z₂X base w b) + ≡ ℤ₂[X]→H*[RP²,ℤ₂]-fun (base v a) cupS ℤ₂[X]→H*[RP²,ℤ₂]-fun (base w b) + main v w = ℤ/2-elim + (λ b → + (cong ℤ₂[X]→H*[RP²,ℤ₂]-fun + (cong (_·Z₂X base w b) (base-neutral v) + ∙ 0LeftAnnihilates ℤ₂[X] (base w b)) + ∙ cong₂ _cupS_ (cong (ℤ₂[X]→H*[RP²,ℤ₂]-fun) + (sym (base-neutral v))) refl)) + (ℤ/2-elim + (cong ℤ₂[X]→H*[RP²,ℤ₂]-fun + (cong (base v fone ·Z₂X_) (base-neutral w) + ∙ 0RightAnnihilates ℤ₂[X] (base w fone)) + ∙ sym (0RightAnnihilates (H*R ℤ/2Ring RP²) + (ℤ₂[X]→H*[RP²,ℤ₂]-fun (base v fone))) + ∙ cong₂ _cupS_ + (λ _ → ℤ₂[X]→H*[RP²,ℤ₂]-fun (base v fone)) + (cong (ℤ₂[X]→H*[RP²,ℤ₂]-fun) (sym (base-neutral w)))) + (main-main v w)) + + ℤ₂[X]→H*[RP²,ℤ₂] : RingHom ℤ₂[X] (H*R ℤ/2Ring RP²) + fst ℤ₂[X]→H*[RP²,ℤ₂] = ℤ₂[X]→H*[RP²,ℤ₂]-fun + snd ℤ₂[X]→H*[RP²,ℤ₂] = makeIsRingHom refl (λ _ _ → refl) ℤ/2[X]→H*[RP²,ℤ/2]-pres· + + open Quotient-FGideal-CommRing-Ring (PolyCommRing ℤ/2CommRing 1) (H*R ℤ/2Ring RP²) + ℤ₂[X]→H*[RP²,ℤ₂] ( ℤ/2CommRing 1 0 3) + (λ { zero → base-neutral _}) + + ℤ₂[X]/→H*[RP²,ℤ₂] : RingHom (CommRing→Ring ℤ₂[X]/) (H*R ℤ/2Ring RP²) + ℤ₂[X]/→H*[RP²,ℤ₂] = inducedHom + + H*[RP²,ℤ₂]→ℤ₂[X]/-fun' : (r : ℕ) → coHom r ℤ/2 RP² → ℤ/2 .fst + H*[RP²,ℤ₂]→ℤ₂[X]/-fun' zero x = H⁰[RP²,ℤ/2]≅ℤ/2 .fst .fst x + H*[RP²,ℤ₂]→ℤ₂[X]/-fun' one x = H¹[RP²,ℤ/2]≅ℤ/2 .fst .fst x + H*[RP²,ℤ₂]→ℤ₂[X]/-fun' two x = H²[RP²,ℤ/2]≅ℤ/2 .fst .fst x + H*[RP²,ℤ₂]→ℤ₂[X]/-fun' (suc (suc (suc r))) x = fzero + + H*[RP²,ℤ₂]→ℤ₂[X]/-fun : (r : ℕ) → coHom r ℤ/2 RP² → ℤ₂[X]/ .fst + H*[RP²,ℤ₂]→ℤ₂[X]/-fun r x = [ base (r ∷ []) (H*[RP²,ℤ₂]→ℤ₂[X]/-fun' r x) ] + + H*[RP²,ℤ₂]→ℤ₂[X]/ : H*R ℤ/2Ring RP² .fst → ℤ₂[X]/ .fst + H*[RP²,ℤ₂]→ℤ₂[X]/ = DS-Rec-Set.f _ _ _ _ squash/ + [ neutral ] + H*[RP²,ℤ₂]→ℤ₂[X]/-fun + (CommRingStr._+_ (snd ℤ₂[X]/)) + (CommRingStr.+Assoc (snd ℤ₂[X]/)) + (CommRingStr.+IdR (snd ℤ₂[X]/)) + (CommRingStr.+Comm (snd ℤ₂[X]/)) + (λ { zero → cong [_] (base-neutral (0 ∷ [])) + ; one → cong [_] (cong (base (1 ∷ [])) (IsGroupHom.pres1 (snd (H¹[RP²,ℤ/2]≅ℤ/2))) + ∙ base-neutral (1 ∷ [])) + ; two → cong [_] (cong (base (2 ∷ [])) (IsGroupHom.pres1 (snd (H²[RP²,ℤ/2]≅ℤ/2))) + ∙ base-neutral (2 ∷ [])) + ; (suc (suc (suc r))) → cong [_] (base-neutral _)}) + (λ { zero a b → cong [_] (base-add (0 ∷ []) _ _ + ∙ cong (base (0 ∷ [])) + (sym (IsGroupHom.pres· (snd (H⁰[RP²,ℤ/2]≅ℤ/2)) a b))) + ; one a b → cong [_] (base-add (1 ∷ []) _ _ + ∙ cong (base (1 ∷ [])) + (sym (IsGroupHom.pres· (snd (H¹[RP²,ℤ/2]≅ℤ/2)) a b))) + ; two a b → cong [_] (base-add (2 ∷ []) _ _ + ∙ cong (base (2 ∷ [])) + (sym (IsGroupHom.pres· (snd (H²[RP²,ℤ/2]≅ℤ/2)) a b))) + ; (suc (suc (suc r))) a b + → cong [_] (cong₂ _add_ refl (base-neutral (3 +ℕ r ∷ [])) + ∙ addRid _)}) + + ℤ₂[X]/→H*[RP²,ℤ₂]→ℤ₂[X]/ : (x : _) + → H*[RP²,ℤ₂]→ℤ₂[X]/ (ℤ₂[X]/→H*[RP²,ℤ₂] .fst x) ≡ x + ℤ₂[X]/→H*[RP²,ℤ₂]→ℤ₂[X]/ = SQ.elimProp (λ _ → squash/ _ _) + (DS-Ind-Prop.f _ _ _ _ (λ _ → squash/ _ _) + refl + (λ { (zero ∷ []) a → cong [_] (cong (base (zero ∷ [])) + (secEq (H⁰[RP²,ℤ/2]≅ℤ/2 .fst) a)) + ; (one ∷ []) a → cong [_] (cong (base (one ∷ [])) + (secEq (H¹[RP²,ℤ/2]≅ℤ/2 .fst) a)) + ; (two ∷ []) a → cong [_] (cong (base (two ∷ [])) + (secEq (H²[RP²,ℤ/2]≅ℤ/2 .fst) a)) + ; (suc (suc (suc r)) ∷ []) → ℤ/2-elim refl + (sym (eq/ _ _ ∣ (λ {zero → base (r ∷ []) fone}) + , ((cong₂ _add_ refl (base-neutral _) + ∙ addRid _ + ∙ λ i → base (+-comm 3 r i ∷ []) fone)) + ∙ sym (addRid _) ∣₁))}) + (λ p q → cong₂ (CommRingStr._+_ (snd ℤ₂[X]/)) p q)) + + H*[RP²,ℤ₂]→ℤ₂[X]/→H*[RP²,ℤ₂] : (x : H*R ℤ/2Ring RP² .fst) + → ℤ₂[X]/→H*[RP²,ℤ₂] .fst (H*[RP²,ℤ₂]→ℤ₂[X]/ x) ≡ x + H*[RP²,ℤ₂]→ℤ₂[X]/→H*[RP²,ℤ₂] = DS-Ind-Prop.f _ _ _ _ + (λ _ → trunc _ _) + refl + (λ { zero x → cong (base zero) (retEq (H⁰[RP²,ℤ/2]≅ℤ/2 .fst) x) + ; one x → cong (base one) (retEq (H¹[RP²,ℤ/2]≅ℤ/2 .fst) x) + ; two x → cong (base two) (retEq (H²[RP²,ℤ/2]≅ℤ/2 .fst) x) + ; (suc (suc (suc r))) x → cong (base (3 +ℕ r)) + (isContr→isProp (isContrH³⁺ⁿ[RP²,G] r ℤ/2) _ _)}) + λ {x} {y} p q + → (IsRingHom.pres+ (ℤ₂[X]/→H*[RP²,ℤ₂] .snd) _ _ ∙ cong₂ _add_ p q) + + ℤ₂[X]/≅H*[RP²,ℤ₂] : RingEquiv (CommRing→Ring ℤ₂[X]/) (H*R ℤ/2Ring RP²) + fst ℤ₂[X]/≅H*[RP²,ℤ₂] = + isoToEquiv (iso (ℤ₂[X]/→H*[RP²,ℤ₂] .fst) H*[RP²,ℤ₂]→ℤ₂[X]/ + H*[RP²,ℤ₂]→ℤ₂[X]/→H*[RP²,ℤ₂] + ℤ₂[X]/→H*[RP²,ℤ₂]→ℤ₂[X]/) + snd ℤ₂[X]/≅H*[RP²,ℤ₂] = ℤ₂[X]/→H*[RP²,ℤ₂] .snd + + H*[RP²,ℤ₂]≅ℤ₂[X]/ : RingEquiv (H*R ℤ/2Ring RP²) (CommRing→Ring ℤ₂[X]/) + H*[RP²,ℤ₂]≅ℤ₂[X]/ = RingEquivs.invRingEquiv ℤ₂[X]/≅H*[RP²,ℤ₂] diff --git a/Cubical/Cohomology/EilenbergMacLane/Rings/RP2wedgeS1.agda b/Cubical/Cohomology/EilenbergMacLane/Rings/RP2wedgeS1.agda index 3c6011cfd9..b4f4150e07 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Rings/RP2wedgeS1.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Rings/RP2wedgeS1.agda @@ -59,6 +59,7 @@ open import Cubical.Algebra.Group.MorphismProperties open import Cubical.Algebra.Group.Instances.IntMod open import Cubical.Algebra.AbGroup open import Cubical.Algebra.AbGroup.Instances.Unit +open import Cubical.Algebra.AbGroup.Instances.IntMod open import Cubical.Algebra.DirectSum.DirectSumHIT.Base open import Cubical.Algebra.Ring open import Cubical.Algebra.AbGroup.TensorProduct diff --git a/Cubical/Cohomology/EilenbergMacLane/Rings/RPinf.agda b/Cubical/Cohomology/EilenbergMacLane/Rings/RPinf.agda new file mode 100644 index 0000000000..5be4064ecf --- /dev/null +++ b/Cubical/Cohomology/EilenbergMacLane/Rings/RPinf.agda @@ -0,0 +1,317 @@ +{-# OPTIONS --safe --lossy-unification #-} +module Cubical.Cohomology.EilenbergMacLane.Rings.RPinf where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Transport + +open import Cubical.Cohomology.EilenbergMacLane.Base +open import Cubical.Cohomology.EilenbergMacLane.CupProduct +open import Cubical.Cohomology.EilenbergMacLane.Groups.RPinf +open import Cubical.Cohomology.EilenbergMacLane.RingStructure + +open import Cubical.Homotopy.EilenbergMacLane.Base +open import Cubical.Homotopy.EilenbergMacLane.GroupStructure +open import Cubical.Homotopy.EilenbergMacLane.Properties +open import Cubical.Homotopy.EilenbergMacLane.CupProduct +open import Cubical.Homotopy.Connected + +open import Cubical.Data.Nat renaming (_+_ to _+ℕ_) +open import Cubical.Data.Fin +open import Cubical.Data.Fin.Arithmetic +open import Cubical.Data.Vec + +open import Cubical.HITs.SetTruncation as ST +open import Cubical.HITs.Truncation as TR +open import Cubical.HITs.RPn + +open import Cubical.Algebra.GradedRing.DirectSumHIT +open import Cubical.Algebra.Group.Morphisms +open import Cubical.Algebra.Group.MorphismProperties +open import Cubical.Algebra.Group.Instances.IntMod +open import Cubical.Algebra.AbGroup +open import Cubical.Algebra.AbGroup.Instances.IntMod +open import Cubical.Algebra.DirectSum.DirectSumHIT.Base +open import Cubical.Algebra.Ring +open import Cubical.Algebra.CommRing +open import Cubical.Algebra.CommRing.Instances.IntMod +open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly +open import Cubical.Algebra.Monoid.Instances.Nat + +open Iso +open PlusBis +open RingTheory + +eRP∞^ : (n : ℕ) → coHom n ℤ/2 (EM ℤ/2 1) +eRP∞^ zero = 1ₕ {G'' = ℤ/2Ring} +eRP∞^ (suc n) = + subst (λ k → coHom k ℤ/2 (EM ℤ/2 1)) (+'-suc₁ n) + (_⌣_ {G'' = ℤ/2Ring} {n = 1} {n} ∣ idfun _ ∣₂ (eRP∞^ n)) + +isConnected₀EM : ∀ {ℓ} (G : AbGroup ℓ) (n : ℕ) → isContr ∥ EM G (suc n) ∥₂ +isConnected₀EM G n = + isOfHLevelRetractFromIso 0 setTruncTrunc2Iso + (isConnectedSubtr 2 n + (subst (λ x → isConnected x (EM G (suc n))) + (+-comm 2 n) + (isConnectedEM (suc n)))) + +EMOne : (n : ℕ) → EM ℤ/2 ˣ n +EMOne zero = fone +EMOne (suc n) = EMOne n , 0ₖ (suc n) + +eRP∞^-isGen : (n : ℕ) → Iso.inv (HⁿRP∞≅ℤ/2 n .fst) fone ≡ eRP∞^ n +eRP∞^-isGen zero = refl +eRP∞^-isGen (suc n) = + (cong₂ (λ v w → ST.rec isSetSetTrunc + (λ x → ∣ inv (RP→EM-ℤ/2-CharacIso (suc n)) x ∣₂) + (ST.rec2 isSetSetTrunc (λ a b → ∣ a , b ∣₂) + v w)) + (inv-∥EM-ℤ/2ˣ∥₀-Iso-fone n) + (isContr→isProp (isConnected₀EM ℤ/2 n) _ ∣ (0ₖ (suc n)) ∣₂) + ∙ cong ∣_∣₂ (funExt (λ x → rUnitₖ (suc n) _ + ∙ cong (subst (EM ℤ/2) (+'-suc₁ n)) + (cong₂ (_⌣ₖ_ {G'' = ℤ/2Ring} {n = 1} {n}) + (sym (transportRefl x)) + (cong (inv (RP→EM-ℤ/2-CharacIso n) (EMOne n)) + (sym (transportRefl x)))))) + ∙ sym (substCommSlice (λ k → EM ℤ/2 1 → EM ℤ/2 k) + (λ k → coHom k ℤ/2 (EM ℤ/2 1)) + (λ _ → ∣_∣₂) (+'-suc₁ n) + (λ x → _⌣ₖ_ {G'' = ℤ/2Ring} {n = 1} {n} x + (inv (RP→EM-ℤ/2-CharacIso n) (EMOne n) x)))) + ∙ cong (subst (λ k → coHom k ℤ/2 (EM ℤ/2 1)) (+'-suc₁ n)) + (cong (_⌣_ {G'' = ℤ/2Ring} {n = 1} {n} ∣ idfun _ ∣₂) + (cong (ST.rec isSetSetTrunc (λ x → ∣ inv (RP→EM-ℤ/2-CharacIso n) x ∣₂)) + (sym (inv-∥EM-ℤ/2ˣ∥₀-Iso-fone n)) + ∙ eRP∞^-isGen n)) + where + inv-∥EM-ℤ/2ˣ∥₀-Iso-fone : (n : ℕ) + → inv (∥EM-ℤ/2ˣ∥₀-Iso n) fone ≡ ∣ EMOne n ∣₂ + inv-∥EM-ℤ/2ˣ∥₀-Iso-fone zero = refl + inv-∥EM-ℤ/2ˣ∥₀-Iso-fone (suc n) = + cong₂ (λ v w → prodRec isSetSetTrunc (λ a b → ∣ a , b ∣₂) + (v , w)) (inv-∥EM-ℤ/2ˣ∥₀-Iso-fone n) + (isContr→isProp (isConnected₀EM ℤ/2 n) _ ∣ (0ₖ (suc n)) ∣₂) + +eRP∞^-comp : (n m : ℕ) → _⌣_ {G'' = ℤ/2Ring} (eRP∞^ n) (eRP∞^ m) ≡ eRP∞^ (n +' m) +eRP∞^-comp zero m = 1ₕ-⌣ m (eRP∞^ m) +eRP∞^-comp (suc n) m = + transport⌣ _ (+'-suc₁ n) _ _ + ∙ sym (compSubstℕ (sym (+'-assoc 1 n m) ∙ +'-suc₁ (n +' m)) (+'-suc n m) + (cong₂ _+'_ (+'-suc₁ n) refl)) + ∙ cong (subst (λ k → coHom k ℤ/2 (EM ℤ/2 1)) (+'-suc n m)) + (sym (compSubstℕ (sym (+'-assoc 1 n m)) (+'-suc₁ (n +' m)) + (sym (+'-assoc 1 n m) ∙ +'-suc₁ (n +' m))) + ∙ cong (subst (λ k → coHom k ℤ/2 (EM ℤ/2 1)) (+'-suc₁ (n +' m))) + ((cong (subst (λ k → coHom k ℤ/2 (EM ℤ/2 1)) (sym (+'-assoc 1 n m))) + (assoc⌣ 1 n m ∣ idfun _ ∣₂ (eRP∞^ n) (eRP∞^ m)) + ∙ subst⁻Subst (λ k → coHom k ℤ/2 (EM ℤ/2 1)) (+'-assoc 1 n m) _) + ∙ cong₂ (_⌣_ {G'' = ℤ/2Ring} {n = 1} {n +' m}) refl (eRP∞^-comp n m))) + ∙ sym (help _ (sym (+'-suc n m))) + where + term = _⌣_ {G'' = ℤ/2Ring} {n = 1 +' n} {m} + (_⌣_ {G'' = ℤ/2Ring} {n = 1} {n} ∣ idfun _ ∣₂ (eRP∞^ n)) (eRP∞^ m) + + help : {w : ℕ} (k : ℕ) (p : w ≡ k) + → eRP∞^ w ≡ subst (λ k → coHom k ℤ/2 (EM ℤ/2 1)) (sym p) (eRP∞^ k) + help = J> sym (transportRefl _) + + transport⌣ : {w v : ℕ} (k : ℕ) (p : w ≡ k) + (x : coHom w ℤ/2 (EM ℤ/2 1)) (y : coHom v ℤ/2 (EM ℤ/2 1)) + → _⌣_ {G'' = ℤ/2Ring} (subst (λ k → coHom k ℤ/2 (EM ℤ/2 (suc zero))) p x) y + ≡ subst (λ k → coHom k ℤ/2 (EM ℤ/2 (suc zero))) + (cong₂ _+'_ p refl) (_⌣_ {G'' = ℤ/2Ring} x y) + transport⌣ = J> λ x y + → cong₂ (_⌣_ {G'' = ℤ/2Ring}) (transportRefl x) refl + ∙ sym (transportRefl _) + +HⁿRP∞≅ℤ/2⌣ : (n m : ℕ) (a b : ℤ/2 .fst) + → Iso.inv (HⁿRP∞≅ℤ/2 (n +' m) .fst) (a ·ₘ b) + ≡ _⌣_ {G'' = ℤ/2Ring} (Iso.inv (HⁿRP∞≅ℤ/2 n .fst) a) + (Iso.inv (HⁿRP∞≅ℤ/2 m .fst) b) +HⁿRP∞≅ℤ/2⌣ n m = + ℤ/2-elim (λ b + → IsGroupHom.pres1 (invGroupIso (HⁿRP∞≅ℤ/2 (n +' m)) .snd) + ∙ sym (0ₕ-⌣ {G'' = ℤ/2Ring} n m (inv (cohomRP∞Iso m) b)) + ∙ cong₂ (_⌣_ {G'' = ℤ/2Ring}) + (sym (IsGroupHom.pres1 (invGroupIso (HⁿRP∞≅ℤ/2 n) .snd))) refl) + (ℤ/2-elim (IsGroupHom.pres1 (invGroupIso (HⁿRP∞≅ℤ/2 (n +' m)) .snd) + ∙ sym (⌣-0ₕ {G'' = ℤ/2Ring} n m (inv (cohomRP∞Iso n) fone)) + ∙ cong₂ (_⌣_ {G'' = ℤ/2Ring}) refl + (sym (IsGroupHom.pres1 (invGroupIso (HⁿRP∞≅ℤ/2 m) .snd)))) + (main n m)) + where + main : (n m : ℕ) → (Iso.inv (HⁿRP∞≅ℤ/2 (n +' m) .fst) fone + ≡ _⌣_ {G'' = ℤ/2Ring} (Iso.inv (HⁿRP∞≅ℤ/2 n .fst) fone) + (Iso.inv (HⁿRP∞≅ℤ/2 m .fst) fone)) + main n m = eRP∞^-isGen (n +' m) ∙∙ sym (eRP∞^-comp n m) + ∙∙ sym (cong₂ (_⌣_ {G'' = ℤ/2Ring}) (eRP∞^-isGen n) (eRP∞^-isGen m)) + + +-- open import Cubical.Agebra.Monoids.Instance.NatVec + +module _ {ℓ : Level} (n : ℕ) where + private + RP∞ = EM ℤ/2 1 + + ℤ₂[x] = Poly ℤ/2CommRing 1 + + ℤ₂[X] = CommRing→Ring (PolyCommRing ℤ/2CommRing 1) + + open GradedRing-⊕HIT-index + NatMonoid + (Poly ℤ/2CommRing) + (λ n → CommRing→AbGroup (PolyCommRing ℤ/2CommRing n) .snd) + + open RingStr (snd (H*R ℤ/2Ring RP∞)) + renaming + ( 0r to 0H*RP + ; 1r to 1H*RP + ; _+_ to _+H*RP_ + ; -_ to -H*RP_ + ; _·_ to _cupS_ + ; +Assoc to +H*RPAssoc + ; +IdR to +H*RPIdR + ; +Comm to +H*RPComm + ; ·Assoc to ·H*RPAssoc + ; is-set to isSetH*RP + ; ·DistR+ to ·DistR+H* + ; ·DistL+ to ·DistL+H*) + + open RingStr (snd ℤ₂[X]) + renaming + ( 0r to 0Z₂X + ; 1r to 1Z₂X + ; _+_ to _+Z₂X_ + ; -_ to -Z₂X_ + ; _·_ to _·Z₂X_ + ; +Assoc to +Z₂XAssoc + ; +IdR to +Z₂XIdR + ; +Comm to +Z₂XComm + ; ·Assoc to ·Z₂XAssoc + ; is-set to isSetZ₂X + ; ·DistR+ to ·DistR+Z₂ + ; ·DistL+ to ·DistL+Z₂) + + ℤ/2≅HⁿRP∞ : (n : ℕ) → AbGroupEquiv ℤ/2 (coHomGr n ℤ/2 (EM ℤ/2 1)) + ℤ/2≅HⁿRP∞ n = invGroupEquiv (GroupIso→GroupEquiv (HⁿRP∞≅ℤ/2 n)) + + ℤ/2≅HⁿRP∞pres0 : (n : ℕ) → ℤ/2≅HⁿRP∞ n .fst .fst fzero ≡ 0ₕ n + ℤ/2≅HⁿRP∞pres0 n = IsGroupHom.pres1 (ℤ/2≅HⁿRP∞ n .snd) + + ℤ₂[X]→H*[RP∞,ℤ₂]-main : Vec ℕ 1 → ℤ/2 .fst → fst (H*R ℤ/2Ring RP∞) + ℤ₂[X]→H*[RP∞,ℤ₂]-main (n ∷ []) g = base n (ℤ/2≅HⁿRP∞ n .fst .fst g) + + ℤ₂[X]→H*[RP∞,ℤ₂]-main-coh₁ : (r : Vec ℕ 1) → + ℤ₂[X]→H*[RP∞,ℤ₂]-main r fzero ≡ neutral + ℤ₂[X]→H*[RP∞,ℤ₂]-main-coh₁ (n ∷ []) = + (λ i → base {Idx = ℕ} {P = λ n → coHom n ℤ/2 RP∞} + {AGP = λ n → coHomGr n ℤ/2 RP∞ .snd} n (ℤ/2≅HⁿRP∞pres0 n i)) + ∙ base-neutral {Idx = ℕ} {P = λ n → coHom n ℤ/2 RP∞} + {AGP = λ n → coHomGr n ℤ/2 RP∞ .snd} n + + ℤ₂[X]→H*[RP∞,ℤ₂]-fun : ℤ₂[x] → fst (H*R ℤ/2Ring RP∞) + ℤ₂[X]→H*[RP∞,ℤ₂]-fun = + DS-Rec-Set.f _ _ _ _ isSetH*RP + neutral + ℤ₂[X]→H*[RP∞,ℤ₂]-main + _add_ + addAssoc + addRid + addComm + ℤ₂[X]→H*[RP∞,ℤ₂]-main-coh₁ + λ {(n ∷ []) → λ a b → base-add n _ _ + ∙ (λ i → base {Idx = ℕ} {P = λ n → coHom n ℤ/2 RP∞} + {AGP = λ n → coHomGr n ℤ/2 RP∞ .snd} n + (IsGroupHom.pres· (ℤ/2≅HⁿRP∞ n .snd) a b (~ i)))} + + open import Cubical.Foundations.Equiv.Properties + open import Cubical.Foundations.Transport + + ℤ/2[X]→H*[RP∞,ℤ/2]-pres· : (x y : ℤ₂[x]) + → ℤ₂[X]→H*[RP∞,ℤ₂]-fun (RingStr._·_ (snd ℤ₂[X]) x y) + ≡ (ℤ₂[X]→H*[RP∞,ℤ₂]-fun x cupS ℤ₂[X]→H*[RP∞,ℤ₂]-fun y) + ℤ/2[X]→H*[RP∞,ℤ/2]-pres· = + DS-Ind-Prop.f _ _ _ _ + (λ _ → isPropΠ λ _ → trunc _ _) + (λ _ → refl) + (λ v a → + DS-Ind-Prop.f _ _ _ _ + (λ _ → trunc _ _) + (cong (ℤ₂[X]→H*[RP∞,ℤ₂]-fun) + (0RightAnnihilates ℤ₂[X] (base v a)) + ∙ sym (0RightAnnihilates (H*R ℤ/2Ring RP∞) + (ℤ₂[X]→H*[RP∞,ℤ₂]-fun (base v a)))) + (λ w b → main v w a b) + λ {x} {y} p q → cong ℤ₂[X]→H*[RP∞,ℤ₂]-fun (·DistR+Z₂ (base v a) x y) + ∙ cong₂ _add_ p q + ∙ sym (·DistR+H* (ℤ₂[X]→H*[RP∞,ℤ₂]-fun (base v a)) + (ℤ₂[X]→H*[RP∞,ℤ₂]-fun x) + (ℤ₂[X]→H*[RP∞,ℤ₂]-fun y))) + λ {x} {y} p q z + → cong (ℤ₂[X]→H*[RP∞,ℤ₂]-fun) + (·DistL+Z₂ x y z) + ∙ cong₂ _add_ (p z) (q z) + where + main : (v w : Vec ℕ 1) (a b : ℤ/2 .fst) + → ℤ₂[X]→H*[RP∞,ℤ₂]-fun (base v a ·Z₂X base w b) + ≡ ℤ₂[X]→H*[RP∞,ℤ₂]-fun (base v a) cupS ℤ₂[X]→H*[RP∞,ℤ₂]-fun (base w b) + main (n ∷ []) (m ∷ []) a b = + (λ i → base {Idx = ℕ} {P = λ n → coHom n ℤ/2 RP∞} + {AGP = λ n → coHomGr n ℤ/2 RP∞ .snd} + (+'≡+ n m (~ i)) + (inv (cohomRP∞Iso (+'≡+ n m (~ i))) (a ·ₘ b))) + ∙ λ i → base {Idx = ℕ} {P = λ n → coHom n ℤ/2 RP∞} + {AGP = λ n → coHomGr n ℤ/2 RP∞ .snd} (n +' m) + (HⁿRP∞≅ℤ/2⌣ n m a b i) + + ℤ₂[X]→H*[RP∞,ℤ₂] : RingHom ℤ₂[X] (H*R ℤ/2Ring RP∞) + fst ℤ₂[X]→H*[RP∞,ℤ₂] = ℤ₂[X]→H*[RP∞,ℤ₂]-fun + snd ℤ₂[X]→H*[RP∞,ℤ₂] = makeIsRingHom refl (λ _ _ → refl) ℤ/2[X]→H*[RP∞,ℤ/2]-pres· + + H*[RP∞,ℤ₂]→ℤ₂[X] : H*R ℤ/2Ring RP∞ .fst → ℤ₂[X] .fst + H*[RP∞,ℤ₂]→ℤ₂[X] = DS-Rec-Set.f _ _ _ _ trunc + neutral + (λ r x → base (r ∷ []) (invEq (ℤ/2≅HⁿRP∞ r .fst) x)) + (RingStr._+_ (snd ℤ₂[X])) + (RingStr.+Assoc (snd ℤ₂[X])) + (RingStr.+IdR (snd ℤ₂[X])) + (RingStr.+Comm (snd ℤ₂[X])) + (λ r → cong (base (r ∷ [])) + (IsGroupHom.pres1 (invGroupEquiv (ℤ/2≅HⁿRP∞ r) .snd)) + ∙ base-neutral _) + λ r a b → base-add (r ∷ []) _ _ + ∙ cong (base (r ∷ [])) + (sym (IsGroupHom.pres· (invGroupEquiv (ℤ/2≅HⁿRP∞ r) .snd) a b)) + + ℤ₂[X]→H*[RP∞,ℤ₂]→ℤ₂[X] : (x : _) + → H*[RP∞,ℤ₂]→ℤ₂[X] (ℤ₂[X]→H*[RP∞,ℤ₂] .fst x) ≡ x + ℤ₂[X]→H*[RP∞,ℤ₂]→ℤ₂[X] = DS-Ind-Prop.f _ _ _ _ (λ _ → trunc _ _) + refl + (λ{ (x ∷ []) a → cong (base (x ∷ [])) (retEq (ℤ/2≅HⁿRP∞ x .fst) a)}) + (λ p q → cong₂ _add_ p q) + + H*[RP∞,ℤ₂]→ℤ₂[X]→H*[RP∞,ℤ₂] : (x : _) + → ℤ₂[X]→H*[RP∞,ℤ₂] .fst (H*[RP∞,ℤ₂]→ℤ₂[X] x) ≡ x + H*[RP∞,ℤ₂]→ℤ₂[X]→H*[RP∞,ℤ₂] = DS-Ind-Prop.f _ _ _ _ (λ _ → trunc _ _) + refl + (λ{ x a → cong (base {Idx = ℕ} {P = λ n → coHom n ℤ/2 RP∞} + {AGP = λ n → coHomGr n ℤ/2 RP∞ .snd} x) + (secEq (ℤ/2≅HⁿRP∞ x .fst) a)}) + λ p q → cong₂ (_add_ {Idx = ℕ} {P = λ n → coHom n ℤ/2 RP∞} + {AGP = λ n → coHomGr n ℤ/2 RP∞ .snd}) + p q + + + ℤ₂[X]≅H*[RP∞,ℤ₂] : RingEquiv ℤ₂[X] (H*R ℤ/2Ring RP∞) + fst ℤ₂[X]≅H*[RP∞,ℤ₂] = + isoToEquiv (iso (ℤ₂[X]→H*[RP∞,ℤ₂] .fst) H*[RP∞,ℤ₂]→ℤ₂[X] + H*[RP∞,ℤ₂]→ℤ₂[X]→H*[RP∞,ℤ₂] ℤ₂[X]→H*[RP∞,ℤ₂]→ℤ₂[X]) + snd ℤ₂[X]≅H*[RP∞,ℤ₂] = ℤ₂[X]→H*[RP∞,ℤ₂] .snd + + H*[RP∞,ℤ₂]≅ℤ₂[X] : RingEquiv (H*R ℤ/2Ring RP∞) ℤ₂[X] + H*[RP∞,ℤ₂]≅ℤ₂[X] = RingEquivs.invRingEquiv ℤ₂[X]≅H*[RP∞,ℤ₂] diff --git a/Cubical/Cohomology/EilenbergMacLane/Rings/Sn.agda b/Cubical/Cohomology/EilenbergMacLane/Rings/Sn.agda new file mode 100644 index 0000000000..7f494a47c9 --- /dev/null +++ b/Cubical/Cohomology/EilenbergMacLane/Rings/Sn.agda @@ -0,0 +1,367 @@ +{-# OPTIONS --safe --lossy-unification #-} +module Cubical.Cohomology.EilenbergMacLane.Rings.Sn where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Function +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Equiv + +open import Cubical.Cohomology.EilenbergMacLane.Base +open import Cubical.Cohomology.EilenbergMacLane.Groups.Sn +open import Cubical.Cohomology.EilenbergMacLane.CupProduct +open import Cubical.Cohomology.EilenbergMacLane.RingStructure + +open import Cubical.Homotopy.EilenbergMacLane.Base +open import Cubical.Homotopy.EilenbergMacLane.Properties +open import Cubical.Homotopy.EilenbergMacLane.CupProduct +open import Cubical.Homotopy.Connected + +open import Cubical.Data.Nat renaming (_+_ to _+ℕ_) +open import Cubical.Data.Nat.Order +open import Cubical.Data.Unit +open import Cubical.Data.Empty as ⊥ +open import Cubical.Data.Vec +open import Cubical.Data.FinData +open import Cubical.Data.Sum + +open import Cubical.HITs.PropositionalTruncation as PT +open import Cubical.HITs.SetTruncation as ST +open import Cubical.HITs.Truncation as TR +open import Cubical.HITs.SetQuotients as SQ renaming (_/_ to _sq/_) +open import Cubical.HITs.EilenbergMacLane1 +open import Cubical.HITs.Susp +open import Cubical.HITs.S1 renaming (rec to S¹Fun) +open import Cubical.HITs.Sn + +open import Cubical.Algebra.GradedRing.DirectSumHIT +open import Cubical.Algebra.Group.Morphisms +open import Cubical.Algebra.Group.MorphismProperties +open import Cubical.Algebra.AbGroup +open import Cubical.Algebra.DirectSum.DirectSumHIT.Base +open import Cubical.Algebra.Ring +open import Cubical.Algebra.CommRing +open import Cubical.Algebra.CommRing.Quotient +open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly +open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly-Quotient +open import Cubical.Algebra.Monoid.Instances.Nat + +open PlusBis +open RingTheory + + +-- open import Cubical.Agebra.Monoids.Instance.NatVec + +module _ {ℓ : Level} (G : CommRing ℓ) (n : ℕ) where + G[x] = Poly G 1 + + G[X] = CommRing→Ring (PolyCommRing G 1) + + G[X]/ = A[X1,···,Xn]/ G 1 0 2 + + private + GRing = CommRing→Ring G + GAb = CommRing→AbGroup G + + open GradedRing-⊕HIT-index + NatMonoid + (Poly G) + (λ n → CommRing→AbGroup (PolyCommRing G n) .snd) + + module H*Sⁿ = RingStr (snd (H*R GRing (S₊ (suc n)))) + module G[X]Str = RingStr (snd G[X]) + + private + _cupS_ = H*Sⁿ._·_ + _·GX_ = G[X]Str._·_ + + G[X]→H*[Sⁿ,G]-main : Vec ℕ 1 → fst G → fst (H*R GRing (S₊ (suc n))) + G[X]→H*[Sⁿ,G]-main (zero ∷ []) g = base 0 (invEquiv (H⁰[Sⁿ,G]≅G GAb n .fst) .fst g) + G[X]→H*[Sⁿ,G]-main (one ∷ []) g = base (suc n) (invEq (Hⁿ[Sⁿ,G]≅G GAb n .fst) g) + G[X]→H*[Sⁿ,G]-main (suc (suc x) ∷ []) g = ⊕HIT.neutral + + G[X]→H*[Sⁿ,G]-main-coh₁ : (r : Vec ℕ 1) + → G[X]→H*[Sⁿ,G]-main r (CommRingStr.0r (snd G)) ≡ neutral + G[X]→H*[Sⁿ,G]-main-coh₁ (zero ∷ []) = base-neutral 0 + G[X]→H*[Sⁿ,G]-main-coh₁ (one ∷ []) = + cong (base (suc n)) (IsGroupHom.pres1 (invGroupEquiv (Hⁿ[Sⁿ,G]≅G GAb n) .snd) ) + ∙ base-neutral (suc n) + G[X]→H*[Sⁿ,G]-main-coh₁ (suc (suc x) ∷ []) = refl + + G[X]→H*[Sⁿ,G]-main-coh₂ : (r : Vec ℕ 1) (a b : fst G) + → (G[X]→H*[Sⁿ,G]-main r a add G[X]→H*[Sⁿ,G]-main r b) + ≡ G[X]→H*[Sⁿ,G]-main r ((snd (CommRing→Ring G) RingStr.+ a) b) + G[X]→H*[Sⁿ,G]-main-coh₂ (zero ∷ []) a b = base-add 0 ∣ (λ _ → a) ∣₂ ∣ (λ _ → b) ∣₂ + G[X]→H*[Sⁿ,G]-main-coh₂ (one ∷ []) a b = + base-add (suc n) _ _ + ∙ cong (base (suc n)) + (sym (IsGroupHom.pres· (invGroupEquiv (Hⁿ[Sⁿ,G]≅G GAb n) .snd) a b)) + G[X]→H*[Sⁿ,G]-main-coh₂ (suc (suc x) ∷ []) a b = addRid neutral + + G[X]→H*[Sⁿ,G]-fun : G[x] → fst (H*R GRing (S₊ (suc n))) + G[X]→H*[Sⁿ,G]-fun = + DS-Rec-Set.f _ _ _ _ H*Sⁿ.is-set + neutral + G[X]→H*[Sⁿ,G]-main + _add_ + addAssoc + addRid + addComm + G[X]→H*[Sⁿ,G]-main-coh₁ + G[X]→H*[Sⁿ,G]-main-coh₂ + + Hⁿ[Sⁿ,G]≅G-pres⌣ : (n : ℕ) (G : Ring ℓ) (g : fst G) + (x : coHom (suc n) (Ring→AbGroup G) (S₊ (suc n))) + → Hⁿ[Sⁿ,G]≅G (Ring→AbGroup G) n .fst .fst + (_⌣_ {G'' = G} {n = 0} {suc n} ∣ (λ _ → g) ∣₂ x) + ≡ RingStr._·_ (snd G) g (Hⁿ[Sⁿ,G]≅G (Ring→AbGroup G) n .fst .fst x) + Hⁿ[Sⁿ,G]≅G-pres⌣ zero G g = + ST.elim (λ _ → isOfHLevelPath 2 (RingStr.is-set (snd G)) _ _) + (S¹-connElim (isConnectedEM 1) + (λ _ → RingStr.is-set (snd G) _ _) + embase + λ p → cong (H¹S¹→G (Ring→AbGroup G)) + (cong (_⌣_ {G'' = G} {n = 0} {1} ∣ (λ _ → g) ∣₂) + (cong (∣_∣₂ ∘ S¹Fun embase) + (sym (Iso.rightInv (Iso-EM-ΩEM+1 0) p)))) + ∙∙ help (ΩEM+1→EM 0 p) + ∙∙ cong (RingStr._·_ (snd G) g) (λ _ → ΩEM+1→EM 0 p)) + where + help : (h : fst G) + → H¹S¹→G (Ring→AbGroup G) + (_⌣_ {G'' = G} {n = 0} {1} ∣ (λ _ → g) ∣₂ + ∣ S¹Fun embase (emloop h) ∣₂) + ≡ RingStr._·_ (snd G) g h + help h = Iso.leftInv (Iso-EM-ΩEM+1 0) (RingStr._·_ (snd G) g h) + Hⁿ[Sⁿ,G]≅G-pres⌣ (suc n) G g = + ST.elim (λ _ → isOfHLevelPath 2 (RingStr.is-set (snd G)) _ _) + (Sⁿ-connElim n (isConnectedSubtr 2 (suc n) + (subst (λ k → isConnected (suc k) (EM (Ring→AbGroup G) (suc (suc n)))) + (+-comm 2 n) (isConnectedEM (2 +ℕ n)))) + (λ _ → RingStr.is-set (snd G) _ _) ∣ north ∣ₕ + λ f → cong (fst (Hⁿ[Sⁿ,G]≅G (Ring→AbGroup G) n) .fst) + (cong ∣_∣₂ (funExt (λ x → sym (ΩEM+1→EM-distr⌣ₖ0n {G'' = G} (suc n) g _)))) + ∙ Hⁿ[Sⁿ,G]≅G-pres⌣ n G g _) + + G[X]→H*[Sⁿ,G]-pres· : (x y : G[x]) + → G[X]→H*[Sⁿ,G]-fun (x ·GX y) + ≡ (G[X]→H*[Sⁿ,G]-fun x cupS G[X]→H*[Sⁿ,G]-fun y) + G[X]→H*[Sⁿ,G]-pres· = DS-Ind-Prop.f _ _ _ _ + (λ _ → isPropΠ λ _ → H*Sⁿ.is-set _ _) + (λ _ → refl) + G[X]→H*[Sⁿ,G]-pres·+ + λ {x} {y} p q s → cong (G[X]→H*[Sⁿ,G]-fun) (G[X]Str.·DistL+ x y s) + ∙ cong₂ _add_ (p s) (q s) + ∙ sym (H*Sⁿ.·DistL+ (G[X]→H*[Sⁿ,G]-fun x) + (G[X]→H*[Sⁿ,G]-fun y) (G[X]→H*[Sⁿ,G]-fun s)) + where + main₀₁ : (g g' : fst G) → _ ≡ _ + main₀₁ g g' = + (cong (invEq (Hⁿ[Sⁿ,G]≅G GAb n .fst)) + (cong₂ (CommRingStr._·_ (snd G)) refl + (sym (secEq (Hⁿ[Sⁿ,G]≅G (Ring→AbGroup GRing) n .fst) g'))) + ∙∙ cong (invEq (Hⁿ[Sⁿ,G]≅G (Ring→AbGroup GRing) n .fst)) + (sym (Hⁿ[Sⁿ,G]≅G-pres⌣ n GRing g (invEq (Hⁿ[Sⁿ,G]≅G GAb n .fst) g'))) + ∙∙ retEq (Hⁿ[Sⁿ,G]≅G (Ring→AbGroup GRing) n .fst) _) + + main : (v v' : Vec ℕ 1) (g g' : fst G) + → G[X]→H*[Sⁿ,G]-fun (base v g ·GX base v' g') + ≡ (G[X]→H*[Sⁿ,G]-fun (base v g) cupS G[X]→H*[Sⁿ,G]-fun (base v' g')) + main (zero ∷ []) (zero ∷ []) g g' = refl + main (zero ∷ []) (one ∷ []) g g' = cong (base (suc n)) (main₀₁ g g') + main (zero ∷ []) (suc (suc w) ∷ []) g g' = refl + main (one ∷ []) (zero ∷ []) g g' = + (λ j → base (+'-comm 0 (suc n) j) + (transp (λ k → coHom (+'-comm 0 (suc n) (k ∧ j)) + GAb (S₊ (suc n))) (~ j) + (invEq (Hⁿ[Sⁿ,G]≅G GAb n .fst) (CommRingStr._·_ (snd G) g g')))) + ∙ cong (base (suc n +' zero)) + (cong (subst (λ k → coHom k GAb (S₊ (suc n))) (+'-comm 0 (suc n))) + (cong (invEq (Hⁿ[Sⁿ,G]≅G GAb n .fst)) (CommRingStr.·Comm (snd G) g g') + ∙ main₀₁ g' g + ∙ sym (-ₕ^[_·_]-even (suc n) 0 (inr tt) _)) + ∙ sym (comm⌣ (suc n) 0 (invEq (Hⁿ[Sⁿ,G]≅G GAb n .fst) g) + (invEquiv (H⁰[Sⁿ,G]≅G GAb n .fst) .fst g'))) + main (one ∷ []) (one ∷ []) g g' = + sym (base-neutral (suc n +' suc n)) + ∙ cong (base (suc n +' suc n)) + (isContr→isProp + (subst (λ k → isContr (coHom (suc k) GAb (S₊ (suc n)))) + (+-suc n n) (isContr-Hᵐ⁺ⁿ[Sⁿ,G] GAb n n)) _ _) + main (one ∷ []) (suc (suc w) ∷ []) g g' = refl + main (suc (suc v) ∷ []) (w ∷ []) g g' = refl + + G[X]→H*[Sⁿ,G]-pres·+ : (r : Vec ℕ 1) (a : fst G) (y : G[x]) + → G[X]→H*[Sⁿ,G]-fun (base r a ·GX y) + ≡ G[X]→H*[Sⁿ,G]-fun (base r a) cupS G[X]→H*[Sⁿ,G]-fun y + G[X]→H*[Sⁿ,G]-pres·+ v a = DS-Ind-Prop.f _ _ _ _ (λ _ → H*Sⁿ.is-set _ _) + (cong (G[X]→H*[Sⁿ,G]-fun) + (0RightAnnihilates G[X] (base v a)) + ∙ sym (0RightAnnihilates + (H*R GRing (S₊ (suc n))) (G[X]→H*[Sⁿ,G]-fun (base v a) ))) + (λ r t → main v r a t) + λ {x} {y} p q → cong (G[X]→H*[Sⁿ,G]-fun) (G[X]Str.·DistR+ (base v a) x y) + ∙ cong₂ _add_ p q + ∙ sym (H*Sⁿ.·DistR+ (G[X]→H*[Sⁿ,G]-fun (base v a)) + (G[X]→H*[Sⁿ,G]-fun x) (G[X]→H*[Sⁿ,G]-fun y)) + + G[X]→H*[Sⁿ,G] : RingHom G[X] (H*R GRing (S₊ (suc n))) + fst G[X]→H*[Sⁿ,G] = G[X]→H*[Sⁿ,G]-fun + snd G[X]→H*[Sⁿ,G] = makeIsRingHom refl (λ _ _ → refl) G[X]→H*[Sⁿ,G]-pres· + + open Quotient-FGideal-CommRing-Ring (PolyCommRing G 1) (H*R GRing (S₊ (suc n))) + G[X]→H*[Sⁿ,G] ( G 1 0 2) + (λ { zero → refl}) + + G[X]/→H*[Sⁿ,G] : RingHom (CommRing→Ring G[X]/) (H*R GRing (S₊ (suc n))) + G[X]/→H*[Sⁿ,G] = inducedHom + + H*[Sⁿ,G]→G[X]/-fun^ : (m : ℕ) → Trichotomy n m + → (x : coHom (suc m) GAb (S₊ (suc n))) → G[X]/ .fst + H*[Sⁿ,G]→G[X]/-fun^ m (lt p) x = [ neutral ] + H*[Sⁿ,G]→G[X]/-fun^ m (eq e) x = + [ base (1 ∷ []) (Hⁿ[Sⁿ,G]≅G GAb n .fst .fst (subst (λ k → coHom (suc k) GAb (S₊ (suc n))) (sym e) x)) ] + H*[Sⁿ,G]→G[X]/-fun^ m (gt q) x = [ neutral ] + + H*[Sⁿ,G]→G[X]/-fun : (m : ℕ) (x : coHom m GAb (S₊ (suc n))) + → G[X]/ .fst + H*[Sⁿ,G]→G[X]/-fun zero x = [ base (0 ∷ []) (H⁰[Sⁿ,G]≅G GAb n .fst .fst x) ] + H*[Sⁿ,G]→G[X]/-fun (suc m) x = H*[Sⁿ,G]→G[X]/-fun^ m (n ≟ m) x + + H*[Sⁿ,G]→G[X]/-fun-coh₁ : (r : ℕ) → H*[Sⁿ,G]→G[X]/-fun r (0ₕ r) ≡ [ neutral ] + H*[Sⁿ,G]→G[X]/-fun-coh₁ zero = + cong [_] (cong (base (0 ∷ [])) (IsGroupHom.pres1 (H⁰[Sⁿ,G]≅G GAb n .snd)) + ∙ base-neutral (0 ∷ [])) + H*[Sⁿ,G]→G[X]/-fun-coh₁ (suc r) = help (n ≟ r) + where + help : (e : _) → H*[Sⁿ,G]→G[X]/-fun^ r e (0ₕ (suc r)) ≡ [ neutral ] + help (lt x) = refl + help (eq x) = cong [_] + (cong (base (1 ∷ [])) + (cong (Hⁿ[Sⁿ,G]≅G GAb n .fst .fst) + (λ j → transp (λ i → coHom (suc (x (~ i ∧ ~ j))) GAb (S₊ (suc n))) + j (0ₕ (suc (x (~ j))))) + ∙ IsGroupHom.pres1 (Hⁿ[Sⁿ,G]≅G GAb n .snd)) + ∙ base-neutral (1 ∷ [])) + help (gt x) = refl + + H*[Sⁿ,G]→G[X]/-fun-coh₂ : (r : ℕ) (x y : coHom r GAb (S₊ (suc n))) + → CommRingStr._+_ (snd (G[X]/)) + (H*[Sⁿ,G]→G[X]/-fun r x) (H*[Sⁿ,G]→G[X]/-fun r y) + ≡ H*[Sⁿ,G]→G[X]/-fun r (x +ₕ y) + H*[Sⁿ,G]→G[X]/-fun-coh₂ zero x y = + cong [_] (base-add (0 ∷ []) _ _ + ∙ cong (base (0 ∷ [])) (sym (IsGroupHom.pres· (H⁰[Sⁿ,G]≅G GAb n .snd) _ _))) + H*[Sⁿ,G]→G[X]/-fun-coh₂ (suc r) x y = help (n ≟ r) x y + where + help : (p : _) (x y : coHom (suc r) GAb (S₊ (suc n))) + → CommRingStr._+_ (snd (G[X]/)) + (H*[Sⁿ,G]→G[X]/-fun^ r p x) + (H*[Sⁿ,G]→G[X]/-fun^ r p y) + ≡ H*[Sⁿ,G]→G[X]/-fun^ r p (x +ₕ y) + help (lt p) x y = cong [_] (addRid neutral) + help (eq p) = help' r p + where + help' : (r : ℕ) (p : n ≡ r) (x y : _) + → CommRingStr._+_ (snd G[X]/) + (H*[Sⁿ,G]→G[X]/-fun^ r (eq p) x) + (H*[Sⁿ,G]→G[X]/-fun^ r (eq p) y) + ≡ H*[Sⁿ,G]→G[X]/-fun^ r (eq p) (x +ₕ y) + help' = J> λ a b → cong [_] + (cong₂ (λ x y → (base (1 ∷ []) x) add (base (1 ∷ []) y)) + (cong (Hⁿ[Sⁿ,G]≅G GAb n .fst .fst) (transportRefl a)) + (cong (Hⁿ[Sⁿ,G]≅G GAb n .fst .fst) (transportRefl b)) + ∙ base-add _ _ _ + ∙ cong (base (1 ∷ [])) + (sym (IsGroupHom.pres· (Hⁿ[Sⁿ,G]≅G GAb n .snd) _ _) + ∙ cong (Hⁿ[Sⁿ,G]≅G GAb n .fst .fst) (sym (transportRefl (a +ₕ b))))) + help (gt p) x y = cong [_] (addRid neutral) + + H*[Sⁿ,G]→G[X]/ : fst (H*R GRing (S₊ (suc n))) → G[X]/ .fst + H*[Sⁿ,G]→G[X]/ = DS-Rec-Set.f _ _ _ _ squash/ + [ neutral ] + H*[Sⁿ,G]→G[X]/-fun + (CommRingStr._+_ (snd (G[X]/))) + (λ _ _ _ → CommRingStr.+Assoc (snd (G[X]/)) _ _ _) + (λ _ → CommRingStr.+IdR (snd (G[X]/)) _) + (λ _ _ → CommRingStr.+Comm (snd (G[X]/)) _ _) + H*[Sⁿ,G]→G[X]/-fun-coh₁ + H*[Sⁿ,G]→G[X]/-fun-coh₂ + + H*[Sⁿ,G]→G[X]/→H*[Sⁿ,G] : (x : fst (H*R GRing (S₊ (suc n)))) + → G[X]/→H*[Sⁿ,G] .fst (H*[Sⁿ,G]→G[X]/ x) ≡ x + H*[Sⁿ,G]→G[X]/→H*[Sⁿ,G] = + DS-Ind-Prop.f _ _ _ _ (λ _ → trunc _ _) + refl + (λ { zero a → cong (base zero) (retEq (H⁰[Sⁿ,G]≅G GAb n .fst) a) + ; (suc r) → help r (n ≟ r)}) + λ p q → IsRingHom.pres+ (G[X]/→H*[Sⁿ,G] .snd) _ _ + ∙ cong₂ _add_ p q + where + help : (r : ℕ) (p : _) (a : _) + → G[X]/→H*[Sⁿ,G] .fst (H*[Sⁿ,G]→G[X]/-fun^ r p a) + ≡ base (suc r) a + help r (lt x) a = + sym (base-neutral (suc r)) + ∙ cong (base (suc r)) + (isContr→isProp + (subst (λ k → isContr (coHom k GAb (S₊ (suc n)))) + (cong suc (snd x)) + (isContr-Hᵐ⁺ⁿ[Sⁿ,G] GAb n (fst x))) _ _) + help r (eq x) a = + J (λ r x → (a : coHom (suc r) GAb (S₊ (suc n))) + → G[X]/→H*[Sⁿ,G] .fst (H*[Sⁿ,G]→G[X]/-fun^ r (eq x) a) + ≡ base (suc r) a) + (λ a → cong (base (suc n)) + (retEq (Hⁿ[Sⁿ,G]≅G GAb n .fst) _ ∙ transportRefl a)) x a + help r (gt x) a = + sym (base-neutral (suc r)) + ∙ cong (base (suc r)) + (isContr→isProp + (subst (λ k → isContr (coHom (suc r) GAb (S₊ k))) + (cong suc (snd x)) + (isOfHLevelRetractFromIso 0 + (equivToIso (fst (Hⁿ[Sᵐ⁺ⁿ,G]≅0 GAb r (fst x)))) + isContrUnit*)) _ _) + + G[X]/→H*[Sⁿ,G]→H*[Sⁿ,G] : (x : G[X]/ .fst) + → H*[Sⁿ,G]→G[X]/ (G[X]/→H*[Sⁿ,G] .fst x) ≡ x + G[X]/→H*[Sⁿ,G]→H*[Sⁿ,G] = SQ.elimProp (λ _ → squash/ _ _) + (DS-Ind-Prop.f _ _ _ _ (λ _ → squash/ _ _) + refl + (λ { (zero ∷ []) g → cong [_] (cong (base (0 ∷ [])) + (secEq (H⁰[Sⁿ,G]≅G GAb n .fst) g)) + ; (one ∷ []) g → h2 g _ + ; (suc (suc x) ∷ []) g + → sym (eq/ _ neutral ∣ hh x g + , (λ i → base (+-comm 2 x i ∷ []) (CommRingStr.·IdR (snd G) g (~ i)) + add neutral) ∣₁)}) + λ p q → cong₂ (CommRingStr._+_ (snd (G[X]/))) p q) + where + hh : (x : ℕ) (g : fst G) → FinVec (fst (PolyCommRing G 1)) 1 + hh x g zero = base (x ∷ []) g + + h2 : (g : fst G) (p : _) + → H*[Sⁿ,G]→G[X]/-fun^ n p + (invEq (Hⁿ[Sⁿ,G]≅G GAb n .fst) g) + ≡ [ base (one ∷ []) g ] + h2 g (lt x) = ⊥.rec (¬m≅H*[Sⁿ,G] : RingEquiv (CommRing→Ring G[X]/) (H*R GRing (S₊ (suc n))) + fst G[X]/≅H*[Sⁿ,G] = + isoToEquiv (iso (G[X]/→H*[Sⁿ,G] .fst) H*[Sⁿ,G]→G[X]/ + H*[Sⁿ,G]→G[X]/→H*[Sⁿ,G] G[X]/→H*[Sⁿ,G]→H*[Sⁿ,G]) + snd G[X]/≅H*[Sⁿ,G] = G[X]/→H*[Sⁿ,G] .snd + + H*[Sⁿ,G]≅G[X]/ : RingEquiv (H*R GRing (S₊ (suc n))) (CommRing→Ring G[X]/) + H*[Sⁿ,G]≅G[X]/ = RingEquivs.invRingEquiv G[X]/≅H*[Sⁿ,G] diff --git a/Cubical/Cohomology/EilenbergMacLane/Rings/Z2-properties.agda b/Cubical/Cohomology/EilenbergMacLane/Rings/Z2-properties.agda index 326bddac69..b34c8179b9 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Rings/Z2-properties.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Rings/Z2-properties.agda @@ -17,6 +17,7 @@ open import Cubical.Algebra.DirectSum.DirectSumHIT.Base open import Cubical.Algebra.Ring open import Cubical.Algebra.CommRing open import Cubical.Algebra.CommRing.Instances.IntMod +open import Cubical.Algebra.AbGroup.Instances.IntMod open import Cubical.Homotopy.EilenbergMacLane.Order2 diff --git a/Cubical/Data/Bool/Properties.agda b/Cubical/Data/Bool/Properties.agda index 56282dcfae..5570fabbd6 100644 --- a/Cubical/Data/Bool/Properties.agda +++ b/Cubical/Data/Bool/Properties.agda @@ -409,3 +409,23 @@ Iso-⊤⊎⊤-Bool .rightInv false = refl separatedBool : Separated Bool separatedBool = Discrete→Separated _≟_ + + +Bool→Bool→∙Bool : Bool → (Bool , true) →∙ (Bool , true) +Bool→Bool→∙Bool false = idfun∙ _ +Bool→Bool→∙Bool true = const∙ _ _ + +Iso-Bool→∙Bool-Bool : Iso ((Bool , true) →∙ (Bool , true)) Bool +Iso.fun Iso-Bool→∙Bool-Bool f = fst f false +Iso.inv Iso-Bool→∙Bool-Bool = Bool→Bool→∙Bool +Iso.rightInv Iso-Bool→∙Bool-Bool false = refl +Iso.rightInv Iso-Bool→∙Bool-Bool true = refl +Iso.leftInv Iso-Bool→∙Bool-Bool f = Σ≡Prop (λ _ → isSetBool _ _) (help _ refl) + where + help : (x : Bool) → fst f false ≡ x + → Bool→Bool→∙Bool (fst f false) .fst ≡ f .fst + help false p = funExt + λ { false → (λ j → Bool→Bool→∙Bool (p j) .fst false) ∙ sym p + ; true → (λ j → Bool→Bool→∙Bool (p j) .fst true) ∙ sym (snd f)} + help true p = (λ j → Bool→Bool→∙Bool (p j) .fst) + ∙ funExt λ { false → sym p ; true → sym (snd f)} diff --git a/Cubical/Data/Nat/Base.agda b/Cubical/Data/Nat/Base.agda index 87ba8e68a1..9f424f947b 100644 --- a/Cubical/Data/Nat/Base.agda +++ b/Cubical/Data/Nat/Base.agda @@ -12,6 +12,7 @@ open import Cubical.Data.Bool.Base open import Cubical.Data.Sum.Base hiding (elim) open import Cubical.Data.Empty.Base hiding (elim) open import Cubical.Data.Unit.Base +open import Cubical.Data.Sigma.Base predℕ : ℕ → ℕ predℕ zero = zero @@ -77,3 +78,13 @@ isZero (suc n) = false _^_ : ℕ → ℕ → ℕ m ^ 0 = 1 m ^ (suc n) = m · m ^ n + + +-- Iterated product +_ˣ_ : ∀ {ℓ} (A : ℕ → Type ℓ) (n : ℕ) → Type ℓ +A ˣ zero = A zero +A ˣ suc n = (A ˣ n) × A (suc n) + +0ˣ : ∀ {ℓ} (A : ℕ → Type ℓ) (0A : (n : ℕ) → A n) → (n : ℕ) → A ˣ n +0ˣ A 0A zero = 0A zero +0ˣ A 0A (suc n) = (0ˣ A 0A n) , (0A (suc n)) diff --git a/Cubical/Data/Nat/Order.agda b/Cubical/Data/Nat/Order.agda index 48e68c9d1c..4d53caf66c 100644 --- a/Cubical/Data/Nat/Order.agda +++ b/Cubical/Data/Nat/Order.agda @@ -272,6 +272,12 @@ zero ≟ suc n = lt (n , +-comm n 1) suc m ≟ zero = gt (m , +-comm m 1) suc m ≟ suc n = Trichotomy-suc (m ≟ n) +Dichotomyℕ : ∀ (n m : ℕ) → (n ≤ m) ⊎ (n > m) +Dichotomyℕ n m with (n ≟ m) +... | lt x = inl (<-weaken x) +... | Trichotomy.eq x = inl (0 , x) +... | gt x = inr x + splitℕ-≤ : (m n : ℕ) → (m ≤ n) ⊎ (n < m) splitℕ-≤ m n with m ≟ n ... | lt x = inl (<-weaken x) diff --git a/Cubical/Foundations/Pointed/Homogeneous.agda b/Cubical/Foundations/Pointed/Homogeneous.agda index 447cac30b0..1e103b664a 100644 --- a/Cubical/Foundations/Pointed/Homogeneous.agda +++ b/Cubical/Foundations/Pointed/Homogeneous.agda @@ -57,6 +57,14 @@ isHomogeneous {ℓ} (A , x) = ∀ y → Path (Pointed ℓ) (A , x) (A , y) }) (sym (h (pt B∙)) ∙ h ((sym f₀ ∙∙ funExt⁻ p a₀ ∙∙ g₀) i)) +→∙HomogeneousPathP : + ∀ {ℓ ℓ'} {A∙ A∙' : Pointed ℓ} {B∙ B∙' : Pointed ℓ'} + {f∙ : A∙ →∙ B∙} {g∙ : A∙' →∙ B∙'} (p : A∙ ≡ A∙') (q : B∙ ≡ B∙') + (h : isHomogeneous B∙') + → PathP (λ i → fst (p i) → fst (q i)) (f∙ .fst) (g∙ .fst) + → PathP (λ i → p i →∙ q i) f∙ g∙ +→∙HomogeneousPathP p q h r = toPathP (→∙Homogeneous≡ h (fromPathP r)) + →∙Homogeneous≡Path : ∀ {ℓ ℓ'} {A∙ : Pointed ℓ} {B∙ : Pointed ℓ'} {f∙ g∙ : A∙ →∙ B∙} (h : isHomogeneous B∙) → (p q : f∙ ≡ g∙) → cong fst p ≡ cong fst q → p ≡ q →∙Homogeneous≡Path {A∙ = A∙@(A , a₀)} {B∙@(B , b)} {f∙@(f , f₀)} {g∙@(g , g₀)} h p q r = diff --git a/Cubical/HITs/KleinBottle/Properties.agda b/Cubical/HITs/KleinBottle/Properties.agda index d9c9628ca8..8b4a30ce21 100644 --- a/Cubical/HITs/KleinBottle/Properties.agda +++ b/Cubical/HITs/KleinBottle/Properties.agda @@ -55,6 +55,24 @@ elimProp prop a₀ = (isProp→PathP (λ _ → prop _) _ _) (isProp→PathP (λ _ → prop _) _ _) +K²FunCharacIso : ∀ {ℓ} {A : KleinBottle → Type ℓ} + → Iso ((x : KleinBottle) → A x) + (Σ[ x ∈ A point ] + Σ[ p ∈ PathP (λ i → A (line1 i)) x x ] + (Σ[ q ∈ PathP (λ i → A (line2 i)) x x ] + SquareP (λ i j → A (square i j)) + q q (λ i → p (~ i)) p)) +Iso.fun K²FunCharacIso f = + f point , cong f line1 , cong f line2 , λ i j → f (square i j) +Iso.inv K²FunCharacIso (a , p1 , p2 , sq) point = a +Iso.inv K²FunCharacIso (a , p1 , p2 , sq) (line1 i) = p1 i +Iso.inv K²FunCharacIso (a , p1 , p2 , sq) (line2 i) = p2 i +Iso.inv K²FunCharacIso (a , p1 , p2 , sq) (square i j) = sq i j +Iso.rightInv K²FunCharacIso _ = refl +Iso.leftInv K²FunCharacIso f = + funExt λ { point → refl ; (line1 i) → refl + ; (line2 i) → refl ; (square i i₁) → refl} + loop1 : S¹ → KleinBottle loop1 base = point loop1 (loop i) = line1 i diff --git a/Cubical/HITs/RPn/Base.agda b/Cubical/HITs/RPn/Base.agda index db0a62202c..5f4c20c7ea 100644 --- a/Cubical/HITs/RPn/Base.agda +++ b/Cubical/HITs/RPn/Base.agda @@ -348,3 +348,17 @@ characRP²Fun : ∀ {ℓ} {A : Type ℓ} (f : RP² → A) → RP²Fun (f point) (cong f line) (λ i j → f (square i j)) ≡ f characRP²Fun f = funExt λ { point → refl ; (line i) → refl ; (square i i₁) → refl} + +RP²FunCharacIso : {A : RP² → Type ℓ} + → Iso ((x : RP²) → A x) + (Σ[ x ∈ A point ] + Σ[ p ∈ PathP (λ i → A (line i)) x x ] + SquareP (λ i j → A (square i j)) + p (λ i → p (~ i)) refl refl) +Iso.fun RP²FunCharacIso f = f point , cong f line , cong (cong f) square +Iso.inv RP²FunCharacIso (x , p , q) point = x +Iso.inv RP²FunCharacIso (x , p , q) (line i) = p i +Iso.inv RP²FunCharacIso (x , p , q) (square i j) = q i j +Iso.rightInv RP²FunCharacIso _ = refl +Iso.leftInv RP²FunCharacIso f = + funExt λ { point → refl ; (line i) → refl ; (square i i₁) → refl} diff --git a/Cubical/HITs/Wedge/Base.agda b/Cubical/HITs/Wedge/Base.agda index 887dc002f4..192c7aedcc 100644 --- a/Cubical/HITs/Wedge/Base.agda +++ b/Cubical/HITs/Wedge/Base.agda @@ -11,6 +11,10 @@ open import Cubical.Foundations.GroupoidLaws _⋁_ : ∀ {ℓ ℓ'} → Pointed ℓ → Pointed ℓ' → Type (ℓ-max ℓ ℓ') _⋁_ (A , ptA) (B , ptB) = Pushout {A = Unit} {B = A} {C = B} (λ _ → ptA) (λ _ → ptB) +-- Arbitrary wedges +⋁gen : ∀ {ℓ ℓ'} (A : Type ℓ) (B : A → Pointed ℓ') → Type (ℓ-max ℓ ℓ') +⋁gen A B = cofib {A = A} {B = Σ A λ a → fst (B a)} + (λ a → a , snd (B a)) -- Pointed versions _⋁∙ₗ_ : ∀ {ℓ ℓ'} → Pointed ℓ → Pointed ℓ' → Pointed (ℓ-max ℓ ℓ') @@ -19,6 +23,9 @@ A ⋁∙ₗ B = (A ⋁ B) , (inl (snd A)) _⋁∙ᵣ_ : ∀ {ℓ ℓ'} → Pointed ℓ → Pointed ℓ' → Pointed (ℓ-max ℓ ℓ') A ⋁∙ᵣ B = (A ⋁ B) , (inr (snd B)) +⋁gen∙ : ∀ {ℓ ℓ'} (A : Type ℓ) (B : A → Pointed ℓ') → Pointed (ℓ-max ℓ ℓ') +⋁gen∙ A B = ⋁gen A B , inl tt + -- Wedge sums of functions _∨→_ : ∀ {ℓ ℓ' ℓ''} {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''} → (f : A →∙ C) (g : B →∙ C) diff --git a/Cubical/Homotopy/EilenbergMacLane/CupProduct.agda b/Cubical/Homotopy/EilenbergMacLane/CupProduct.agda index 74733bfdb0..8a0ca8b127 100644 --- a/Cubical/Homotopy/EilenbergMacLane/CupProduct.agda +++ b/Cubical/Homotopy/EilenbergMacLane/CupProduct.agda @@ -20,10 +20,12 @@ open import Cubical.Foundations.Prelude open import Cubical.Foundations.HLevels open import Cubical.Foundations.GroupoidLaws open import Cubical.Foundations.Transport +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Function open import Cubical.HITs.EilenbergMacLane1 open import Cubical.HITs.Susp -open import Cubical.HITs.Truncation +open import Cubical.HITs.Truncation as TR open import Cubical.Algebra.AbGroup.Base open import Cubical.Data.Nat hiding (_·_) renaming (elim to ℕelim ; _+_ to _+ℕ_) @@ -168,6 +170,48 @@ module _ {G'' : Ring ℓ} where ∙ cong (cong (inducedFun-EM TensorMultHom (suc (suc n) +' suc m))) (EM→ΩEM+1-distrₙsuc n m x y) + ΩEM+1→EM-distr⌣ₖ0n : (n : ℕ) + → (x : EM G' zero) (y : Path (EM G' (suc n)) _ _) + → _⌣ₖ_ {n = zero} {m = n} x (ΩEM+1→EM n y) + ≡ ΩEM+1→EM-gen n _ λ i → _⌣ₖ_ {n = zero} {suc n} x (y i) + ΩEM+1→EM-distr⌣ₖ0n zero x y = + sym (Iso.leftInv (Iso-EM-ΩEM+1 0) _) + ∙ cong (ΩEM+1→EM 0) + λ j i → _⌣ₖ_ {n = zero} {1} x (Iso.rightInv (Iso-EM-ΩEM+1 0) y j i) + ΩEM+1→EM-distr⌣ₖ0n (suc n) x y = + sym (Iso.leftInv (Iso-EM-ΩEM+1 (suc n)) _) + ∙ cong (ΩEM+1→EM (suc n)) (EM→ΩEM+1-distr⌣ₖ0n n x (ΩEM+1→EM (suc n) y)) + ∙ cong (ΩEM+1→EM (suc n)) (help n (ΩEM+1→EM (suc n) y) + ∙ cong (cong (_⌣ₖ_ {n = zero} {suc (suc n)} x)) + (Iso.rightInv (Iso-EM-ΩEM+1 (suc n)) y)) + where + help : (n : ℕ) (y : EM G' (suc n)) + → (λ i → _⌣ₖ_ {n = suc zero} {suc n} (EM→ΩEM+1 0 x i) y) + ≡ cong (_⌣ₖ_ {n = zero} {suc (suc n)} x) (EM→ΩEM+1 (suc n) y) + help zero a = + (rUnit _ + ∙ cong₂ _∙_ refl + (cong (cong (EMTensorMult (suc (suc zero)))) + (cong sym (sym (EM→ΩEM+1-0ₖ (suc zero))) + ∙ cong (sym ∘ EM→ΩEM+1 (suc zero)) + (sym (⌣ₖ-0ₖ⊗ {G' = G'} {H' = G'} zero (suc zero) x))))) + ∙ sym (cong-∙ ((λ y → _⌣ₖ_ {n = zero} {suc (suc zero)} x ∣ y ∣ₕ)) + (merid a) + (sym (merid embase))) + help (suc n) = TR.elim + (λ _ → isOfHLevelPath' (4 +ℕ n) + (isOfHLevelPath (5 +ℕ n) (hLevelEM G' (3 +ℕ n)) _ _) _ _) + λ a → rUnit _ + ∙ cong₂ _∙_ refl + (cong (cong (EMTensorMult (suc (suc (suc n))))) + (cong sym (sym (EM→ΩEM+1-0ₖ (suc (suc n)))) + ∙ cong (sym ∘ EM→ΩEM+1 (suc (suc n))) + (sym (⌣ₖ-0ₖ⊗ {G' = G'} {H' = G'} zero (suc (suc n)) x)))) + ∙ sym (cong-∙ ((λ y → _⌣ₖ_ {n = zero} {suc (suc (suc n))} x ∣ y ∣ₕ)) + (merid a) + (sym (merid north))) + + -- graded commutativity module _ {G'' : CommRing ℓ} where private diff --git a/Cubical/Homotopy/EilenbergMacLane/Order2.agda b/Cubical/Homotopy/EilenbergMacLane/Order2.agda index bd09f17d52..3de91de139 100644 --- a/Cubical/Homotopy/EilenbergMacLane/Order2.agda +++ b/Cubical/Homotopy/EilenbergMacLane/Order2.agda @@ -37,6 +37,7 @@ open import Cubical.HITs.Truncation as TR open import Cubical.Algebra.CommRing.Base open import Cubical.Algebra.Group.Instances.IntMod +open import Cubical.Algebra.AbGroup.Instances.IntMod open import Cubical.Algebra.CommRing.Instances.IntMod open import Cubical.Algebra.AbGroup.Base open import Cubical.Algebra.AbGroup.TensorProduct @@ -212,9 +213,6 @@ module EM2 {ℓ : Level} (G : AbGroup ℓ) symConstEM-refl {n = suc zero} = transportRefl refl symConstEM-refl {n = suc (suc n)} = transportRefl refl -ℤ/2 : AbGroup ℓ-zero -ℤ/2 = Group→AbGroup (ℤGroup/ 2) +ₘ-comm - private module EMZ/2 = EM2 ℤ/2 -Const-ℤ/2 diff --git a/Cubical/Homotopy/EilenbergMacLane/Properties.agda b/Cubical/Homotopy/EilenbergMacLane/Properties.agda index 76a5092bec..953ce48309 100644 --- a/Cubical/Homotopy/EilenbergMacLane/Properties.agda +++ b/Cubical/Homotopy/EilenbergMacLane/Properties.agda @@ -512,6 +512,24 @@ module _ {G : AbGroup ℓ} where lem zero = ΩEM+1→EM-refl 0 lem (suc n) = ΩEM+1→EM-refl (suc n) + ΩEM+1→EM-gen-hom : (n : ℕ) (x : EM G (suc n)) (p q : x ≡ x) + → ΩEM+1→EM-gen n x (p ∙ q) ≡ ΩEM+1→EM-gen n x p +ₖ ΩEM+1→EM-gen n x q + ΩEM+1→EM-gen-hom n = + EM-raw'-elim _ (suc n) + (λ _ → isOfHLevelΠ2 (suc (suc n)) + (λ _ _ → isOfHLevelPath (suc (suc n)) (hLevelEM _ n) _ _)) + (EM-raw'-trivElim _ n + (λ _ → isOfHLevelΠ2 (suc n) (λ _ _ → hLevelEM _ n _ _)) + (lem n)) + where + lem : (n : ℕ) (p q : EM-raw'→EM G (suc n) (snd (EM-raw'∙ G (suc n))) + ≡ EM-raw'→EM G (suc n) (snd (EM-raw'∙ G (suc n)))) + → ΩEM+1→EM-gen n _ (p ∙ q) + ≡ ΩEM+1→EM-gen n _ p + +ₖ ΩEM+1→EM-gen n _ q + lem zero p q = ΩEM+1→EM-hom 0 p q + lem (suc n) p q = ΩEM+1→EM-hom (suc n) p q + -- Some HLevel lemmas about function spaces (EM∙ G n →∙ EM∙ H m), mainly used for -- the cup product module _ where diff --git a/Cubical/Homotopy/EilenbergSteenrod.agda b/Cubical/Homotopy/EilenbergSteenrod.agda index 26502a1c09..be22126aad 100644 --- a/Cubical/Homotopy/EilenbergSteenrod.agda +++ b/Cubical/Homotopy/EilenbergSteenrod.agda @@ -31,6 +31,9 @@ open import Cubical.Algebra.Group open import Cubical.Algebra.Group.Morphisms open import Cubical.Algebra.Group.MorphismProperties open import Cubical.Algebra.AbGroup +open import Cubical.Algebra.AbGroup.Instances.Pi + +open import Cubical.Axiom.Choice record coHomTheory {ℓ ℓ' : Level} (H : (n : ℤ) → Pointed ℓ → AbGroup ℓ') : Type (ℓ-suc (ℓ-max ℓ ℓ')) where @@ -38,6 +41,9 @@ record coHomTheory {ℓ ℓ' : Level} (H : (n : ℤ) → Pointed ℓ → AbGroup Boolℓ = Lift Bool , lift true field Hmap : (n : ℤ) → {A B : Pointed ℓ} (f : A →∙ B) → AbGroupHom (H n B) (H n A) + HMapComp : (n : ℤ) → {A B C : Pointed ℓ} (g : B →∙ C) (f : A →∙ B) + → compGroupHom (Hmap n g) (Hmap n f) ≡ Hmap n (g ∘∙ f) + HMapId : (n : ℤ) → {A : Pointed ℓ} → Hmap n (idfun∙ A) ≡ idGroupHom Suspension : Σ[ F ∈ ((n : ℤ) {A : Pointed ℓ} → AbGroupEquiv (H (sucℤ n) (Susp (typ A) , north)) (H n A)) ] ({A B : Pointed ℓ} (f : A →∙ B) (n : ℤ) → fst (Hmap (sucℤ n) (suspFun (fst f) , refl)) ∘ invEq (fst (F n {A = B})) @@ -47,3 +53,33 @@ record coHomTheory {ℓ ℓ' : Level} (H : (n : ℤ) → Pointed ℓ → AbGroup ≡ Im (Hmap n {B = _ , inr (pt B)} (cfcod (fst f) , refl)) Dimension : (n : ℤ) → ¬ n ≡ 0 → isContr (fst (H n Boolℓ)) BinaryWedge : (n : ℤ) {A B : Pointed ℓ} → AbGroupEquiv (H n (A ⋁ B , (inl (pt A)))) (dirProdAb (H n A) (H n B)) + +record coHomTheoryGen {ℓ ℓ' : Level} (H : (n : ℤ) → Pointed ℓ → AbGroup ℓ') : Type (ℓ-suc (ℓ-max ℓ ℓ')) + where + Boolℓ : Pointed ℓ + Boolℓ = Lift Bool , lift true + field + Hmap : (n : ℤ) → {A B : Pointed ℓ} (f : A →∙ B) → AbGroupHom (H n B) (H n A) + HMapComp : (n : ℤ) → {A B C : Pointed ℓ} (g : B →∙ C) (f : A →∙ B) + → compGroupHom (Hmap n g) (Hmap n f) ≡ Hmap n (g ∘∙ f) + HMapId : (n : ℤ) → {A : Pointed ℓ} → Hmap n (idfun∙ A) ≡ idGroupHom + + Suspension : Σ[ F ∈ ((n : ℤ) {A : Pointed ℓ} → AbGroupEquiv (H (sucℤ n) (Susp (typ A) , north)) (H n A)) ] + ({A B : Pointed ℓ} (f : A →∙ B) (n : ℤ) + → fst (Hmap (sucℤ n) (suspFun (fst f) , refl)) ∘ invEq (fst (F n {A = B})) + ≡ invEq (fst (F n {A = A})) ∘ fst (Hmap n f)) + Exactness : {A B : Pointed ℓ} (f : A →∙ B) (n : ℤ) + → Ker (Hmap n f) + ≡ Im (Hmap n {B = _ , inr (pt B)} (cfcod (fst f) , refl)) + Dimension : (n : ℤ) → ¬ n ≡ 0 → isContr (fst (H n Boolℓ)) + Wedge : (n : ℤ) {I : Type ℓ} (satAC : satAC (ℓ-max ℓ ℓ') 2 I) {A : I → Pointed ℓ} + → isEquiv {A = H n (⋁gen∙ I A) .fst} + {B = ΠAbGroup (λ i → H n (A i)) .fst} + λ x i → Hmap n ((λ x → inr (i , x)) , sym (push i)) .fst x + + Wedge→AbGroupEquiv : (n : ℤ) {I : Type ℓ} (satAC : satAC (ℓ-max ℓ ℓ') 2 I) {A : I → Pointed ℓ} + → AbGroupEquiv (H n (⋁gen∙ I A)) (ΠAbGroup (λ i → H n (A i)) ) + fst (fst (Wedge→AbGroupEquiv n satAC)) = _ + snd (fst (Wedge→AbGroupEquiv n satAC)) = Wedge n satAC + snd (Wedge→AbGroupEquiv n satAC) = makeIsGroupHom λ f g + → funExt λ i → IsGroupHom.pres· (Hmap n ((λ x → inr (i , x)) , sym (push i)) .snd) _ _ diff --git a/Cubical/Papers/CohomologyRings.agda b/Cubical/Papers/CohomologyRings.agda index 780f3ba11e..88b2d42db4 100644 --- a/Cubical/Papers/CohomologyRings.agda +++ b/Cubical/Papers/CohomologyRings.agda @@ -275,7 +275,7 @@ open H*𝕂² using (CohomologyRing-𝕂²) open H*ℝP²∨S¹ using (CohomologyRing-RP²⋁S¹) -- ℤ/2ℤ Cohomology groups of the Klein Bottle and ℝP² ⋁ S¹ -open ℤ/2-Hⁿ𝕂² using (H⁰[K²,ℤ/2]≅ℤ/2 ; H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 ; H²[K²,ℤ/2]≅ℤ/2 ; H³⁺ⁿK²≅0) +open ℤ/2-Hⁿ𝕂² using (H⁰[K²,ℤ/2]≅ℤ/2 ; H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 ; H²[K²,ℤ/2]≅ℤ/2 ; H³⁺ⁿ[K²,G]≅0) open ℤ/2-HⁿℝP²∨S¹ using (H⁰[RP²∨S¹,ℤ/2]≅ℤ/2 ; H¹[RP²∨S¹,ℤ/2]≅ℤ/2×ℤ/2 ; H²[RP²∨S¹,ℤ/2]≅ℤ/2 ; H³⁺ⁿ[RP²∨S¹,ℤ/2]≅Unit) -- Proposition 5.7, ℤ/2ℤ cohomology ring of the Klein Bottle diff --git a/Cubical/Papers/ComputationalSyntheticCohomology.agda b/Cubical/Papers/ComputationalSyntheticCohomology.agda new file mode 100644 index 0000000000..74abe6a870 --- /dev/null +++ b/Cubical/Papers/ComputationalSyntheticCohomology.agda @@ -0,0 +1,312 @@ +{- + +Please do not move this file. Changes should only be made if necessary. + +This file contains pointers to the code examples and main results from +the paper: + +Computational Synthetic Cohomology Theory in Homotopy Type Theory + +-} + +-- The "--safe" flag ensures that there are no postulates or unfinished goals +{-# OPTIONS --safe #-} +module Cubical.Papers.ComputationalSyntheticCohomology where + +open import Cubical.Data.Nat +open import Cubical.Algebra.AbGroup +open import Cubical.Foundations.GroupoidLaws + +-- 1: Introduction +-- 2: Background + +open import Cubical.Foundations.Prelude as Prelude +import Cubical.Homotopy.HSpace as hSpace +import Cubical.Foundations.Pointed.Homogeneous as Homogeneous +import Cubical.HITs.Susp as Suspensions +import Cubical.HITs.Pushout as Pushouts +import Cubical.Foundations.Path as Paths + +-- 3: Eilenberg-MacLane spaces +import Cubical.Homotopy.EilenbergMacLane.Base as EMSpace +import Cubical.Homotopy.EilenbergMacLane.Properties as EMProps +import Cubical.Homotopy.EilenbergMacLane.WedgeConnectivity as WC +import Cubical.Homotopy.EilenbergMacLane.GroupStructure as EMGr +import Cubical.Algebra.AbGroup.TensorProduct as Tensor +import Cubical.Homotopy.EilenbergMacLane.CupProductTensor as Cup⊗ +import Cubical.Homotopy.EilenbergMacLane.CupProduct as Cupₖ +import Cubical.Homotopy.EilenbergMacLane.GradedCommTensor as CupComm + +-- 4: Cohomology +import Cubical.Cohomology.EilenbergMacLane.Base as Cohom +import Cubical.Cohomology.EilenbergMacLane.CupProduct as CohomCup +import Cubical.Axiom.Choice as Choice +import Cubical.HITs.Wedge as ⋁ +import Cubical.Homotopy.EilenbergSteenrod as Axioms +import Cubical.Cohomology.EilenbergMacLane.EilenbergSteenrod as SatAxioms +import Cubical.Cohomology.EilenbergMacLane.MayerVietoris as MV +import Cubical.Cohomology.EilenbergMacLane.Gysin as Gysin + +-- 5: Computations of cohomology groups and rings +import Cubical.Cohomology.EilenbergMacLane.Groups.Unit as HⁿUnit +import Cubical.Cohomology.EilenbergMacLane.Groups.Connected as CohomConnected +import Cubical.Cohomology.EilenbergMacLane.Groups.Sn as CohomSn +import Cubical.Cohomology.EilenbergMacLane.Rings.Sn as CohomRingSn +import Cubical.Cohomology.EilenbergMacLane.Groups.Torus as CohomT² +import Cubical.HITs.Torus as T² +import Cubical.HITs.RPn.Base as RP² +import Cubical.HITs.KleinBottle as K² +import Cubical.Cohomology.EilenbergMacLane.Groups.RP2 as CohomRP² +import Cubical.ZCohomology.CohomologyRings.RP2 as ZCohomRingRP² +import Cubical.Cohomology.EilenbergMacLane.Groups.KleinBottle as CohomK² +import Cubical.ZCohomology.CohomologyRings.KleinBottle as ZCohomRingK² +import Cubical.Cohomology.EilenbergMacLane.Rings.RP2 as RP²Ring +import Cubical.Cohomology.EilenbergMacLane.Rings.KleinBottle as K²Ring +import Cubical.Cohomology.EilenbergMacLane.Rings.RPinf as RP∞Ring + +----- 1. INNTRODUCTION ----- + +----- 2. Background on HoTT/UF and notations ----- + +-- 2.1 Homotopy Type Theory in Cubical Agda + +-- Definition 1. Binary ap +open Prelude renaming (cong₂ to ap²) + +-- Definition 2. H-spaces +open hSpace using (HSpace) + +-- Definition 3. Homogeneous types +open Homogeneous using (isHomogeneous) + +-- Definition 4. Suspension +open Suspensions using (Susp) + +-- Definition 5. Pushouts +open Pushouts using (Pushout) + +-- Lemma 6. Flip +open Paths using (sym≡flipSquare) + +----- 3. Eilenberg-MacLane spaces ----- +-- Definition 7. +-- Included for readability: not used explicitly in formalisation. + +-- Definition 8. (raw Eilenbreg-MacLane spaces) EM-raw +open EMSpace using (EM-raw) + +-- Definition 9. (Eilenbreg-MacLane spaces) EM-raw +open EMSpace using (EM) + +-- Proposition 10. Connectivity of K(G,n) +open EMProps using (isConnectedEM) + +-- Lemma 11. +open EMProps using (EMFun-EM→ΩEM+1) + +--- 3.1 Group Structure +-- Proposition 12. (Wedge connectivity for K(G,n)) +open WC.wedgeConEM using (fun ; left ; right) + +-- Proposition 13. (unit laws for +ₖ) +open EMGr using (rUnitₖ ; lUnitₖ) +lUnit≡rUnit : ∀ {ℓ} {G : AbGroup ℓ} (n : ℕ) + → rUnitₖ {G = G} n (EMSpace.0ₖ n) ≡ lUnitₖ {G = G} n (EMSpace.0ₖ n) +lUnit≡rUnit {G = G} zero = AbGroupStr.is-set (snd G) _ _ _ _ +lUnit≡rUnit (suc zero) = refl +lUnit≡rUnit (suc (suc n)) = refl + +-- Proposition 14. (commutativity of +ₖ) +open EMGr using (commₖ) + +-- Proposition 15. (associativity of +ₖ) +open EMGr using (assocₖ) + +-- Proposition 16. (ap² on +ₖ) +open EMGr using (cong₂+₁ ; cong₂+₂) + +-- Proposition 17. (cancellation laws of +ₖ) +open EMGr using (rCancelₖ ; lCancelₖ) + +--- 3.2 K(Gn) vs ΩK(G,n+1) +-- Proposition 18. Commutativity of Ω(K(G,n),x) +open EMProps using (isCommΩEM-base) + +-- Proposition 19. (ap -ₖ = path inversion) +open EMGr using (cong-₁ ; cong-₂) + +-- Proposition 20. (σ preserves +ₖ) +open EMProps using (EM→ΩEM+1-hom) + +-- Corollary 21. (σ preserves -ₖ) +open EMProps using (EM→ΩEM+1-sym) + +-- Theorem 22. K(G,n) ≃ Ω(K(G,n+1)) +open EMProps using (EM≃ΩEM+1) + +--- 3.3 The cup product with group coefficients +-- Definition 23. Tensor products of abelian groups +open Tensor using (_⨂_) + +-- Proposition 24. Truncation of K(G,n) →* K(H;n+m) +open EMProps using (isOfHLevel↑∙) + +-- The general cup product +open Cup⊗ renaming (_⌣ₖ_ to _⌣ₖ⊗_) + +-- Proposition 25 (anihilation laws) +open Cup⊗ using (⌣ₖ-0ₖ ; 0ₖ-⌣ₖ) + +-- Lemma 26 (Evan's trick) +open Homogeneous using (→∙Homogeneous≡) + +-- Propositions 27 and 28 (distributivity of ⌣ₖ) +open Cup⊗.LeftDistributivity using (main) +open Cup⊗.RightDistributivity using (main) + +-- Lemma 29 +open Cup⊗ using (EM→ΩEM+1-distr₀ₙ ; EM→ΩEM+1-distrₙsuc ; EM→ΩEM+1-distrₙ₀) + +-- Proposition 30 (associativity of ⌣ₖ) +open Cup⊗.Assoc using (main) + +-- Proposition 31 (graded commutativity of CupComm) +open CupComm using (⌣ₖ-comm) + +--- 3.4 The cup product with ring coefficients +-- Proposition 32 (ring structure on ⌣ₖ with ring coefficents) +open Cupₖ using (assoc⌣ₖ ; distrL⌣ₖ ; distrR⌣ₖ ; ⌣ₖ-0ₖ ; 0ₖ-⌣ₖ) + +-- Proposition 33 (graded commutativity) +open Cupₖ using (⌣ₖ-comm) + +-- Proposition 34 (neutral element) +open Cupₖ using (⌣ₖ-1ₖ ; 1ₖ-⌣ₖ) + + +----- 4. Cohomology ----- +-- Defininition of cohomology groups +open Cohom using (coHomGr) + +-- Cup products on cohomology +open CohomCup using (_⌣_) + +--- 4.1 Reduced cohomology +-- Definition of reduced cohomology groups +open Cohom using (coHomRedGr) + +-- Proposition 35. +open Cohom using (coHom≅coHomRed) + +-- Proposition 36. +open Cohom using (coHom⁰≅coHomRed⁰) + +--- 4.2 Eilenberg-Steenrod axioms for cohomology +-- Definition 37. Cofibres +open Pushouts using (cofib) + +-- Definition 38. Arbitrary wedges +open ⋁ using (⋁gen) + +-- Definition 39. Choice +open Choice using (satAC) + +-- Definition 40. Eilenberg-Steenrod axioms +open Axioms using (coHomTheoryGen) + +-- Theorem 41. Eilenberg-Steenrod axioms are satified +open SatAxioms using (satisfies-ES-gen) + +-- Theorem 42 (The mayer-Vietoris sequence) +open MV.MV using ( Ker-i⊂Im-d ; Im-d⊂Ker-i + ; Ker-Δ⊂Im-i ; Im-i⊂Ker-Δ + ; Ker-d⊂Im-Δ ; Im-Δ⊂Ker-d) + +--- 4.4 The Thom isomorphism and the Gysin sequence +-- Theorem 43 (Gysin sequence) +open Gysin.Gysin using ( Im-mapᵣ⊂Ker-mapₗ ; Ker-mapₗ⊂Im-mapᵣ + ; Ker-⌣⊂Im-mapₗ ; Im-mapₗ⊂Ker-⌣ + ; Im--⌣⊂Ker-mapᵣ ; Ker-mapᵣ⊂Im--⌣) + +--- 5. Computations of cohomology groups and rings +-- Proposition 44. Cohom of 1 +open HⁿUnit using (H⁰[Unit,G]≅G ; Hⁿ⁺¹[Unit,G]≅0) + +-- Lemma 45. Cohom of truncation +open Cohom using (coHomTruncEquiv) + +-- Proposition 46. Cohomology of connected types +open CohomConnected using (H⁰conn) + +--- 5.1 Speres +-- Proposition 47. H¹(S¹,G) +open CohomSn using (H¹[S¹,G]≅G) + +-- Proposition 48. Hⁿ(Sⁿ,G) +open CohomSn using (Hⁿ[Sⁿ,G]≅G) + +-- Proposition 49. Hⁿ(Sᵐ,G) , m ≠ n +open CohomSn using (Hⁿ[Sᵐ⁺ⁿ,G]≅0 ; Hᵐ⁺ⁿ[Sⁿ,G]≅0) + +-- Proposition 50. H*(Sᵐ,G) +open CohomRingSn using (H*[Sⁿ,G]≅G[X]/) + +--- 5.2 The Torus +-- Definition 51. Torus +open T² using (Torus) + +-- Proposition 52. Hⁿ(T²,G) +open CohomT² using (H⁰[T²,G]≅G ; H¹[T²,G]≅G×G ; H²[T²,G]≅G ; H³⁺ⁿ[T²,G]≅0) + +--- 5.3 The Real Projective Plane and The Klein Bottle +-- Definition 53. Real Projective Plane +open RP² using (RP²) +-- Definition 54. The Klein Bottle +open K² using (KleinBottle) + +-- Proposition 55 H¹(RP²,G) ≅ G[2] +open CohomRP² using (H¹[RP²,G]≅G[2]) + +-- Proposition 56 H²(RP²,G) ≅ G/2 +open CohomRP² using (H²[RP²,G]≅G/2) + +-- Proposition 57 Hᵐ(RP²,G) ≅ 0, m ≥ 3 +open CohomRP² using (H³⁺ⁿ[RP²,G]≅0) + +-- Proposition 58. Hᵐ(K²,G) +open CohomK² using (H⁰[K²,G]≅G ; H¹[K²,G]≅G×H¹[RP²,G]; H²⁺ⁿ[K²,G]≅H²⁺ⁿ[RP²,G]) + +-- Proposition 59. H*(RP²,\bZ) -- Formalisation taken from `Computing Cohomology Rings in Cubical Agda' +open ZCohomRingRP² using (RP²-CohomologyRing) + +-- Defnition 60 kill-Δ +-- Omitted (implicit in formalisation) + +-- Proposition 61 H*(K²,ℤ) -- Formalisation taken from `Computing Cohomology Rings in Cubical Agda' +open ZCohomRingK² using (CohomologyRing-𝕂²) + +-- Definition 62. Res (only formliased for relevant special case of F = ⌣ on K(ℤ/2,1)) +open K²Ring using (Res⌣) + +-- Propsoiton 63. Res refl = refl +-- omitted (used implicitly in formalisation) + +-- Lemma 64/65. ap2-funct ocherence (this is roughly the special case of lemma 61) +open K²Ring using (sym-cong₂-⌣≡) + +-- Proposition 66. Implicitly formalised via the following theorem +open K²Ring using (α²↦1) + +-- Proposition 67. H*(RP²,Z/2) +open RP²Ring using (H*[RP²,ℤ₂]≅ℤ₂[X]/) + +-- Proposition 68. (Roughly) +open K²Ring using (α²↦1 ; βα↦1 ; β²↦0) + +-- Proposition 69. H*(K²,ℤ/2) +open K²Ring using (H*KleinBottle≅ℤ/2[X,Y]/) + +-- Lemma 70. (implicitly used) + +-- Proposition 71. H*(RP∞, ℤ/2) +open RP∞Ring using (H*[RP∞,ℤ₂]≅ℤ₂[X]) diff --git a/Cubical/ZCohomology/EilenbergSteenrodZ.agda b/Cubical/ZCohomology/EilenbergSteenrodZ.agda index 398b2da551..a124865f29 100644 --- a/Cubical/ZCohomology/EilenbergSteenrodZ.agda +++ b/Cubical/ZCohomology/EilenbergSteenrodZ.agda @@ -215,9 +215,30 @@ private fst (theMorph (negsuc n) f) = idfun _ snd (theMorph (negsuc n) f) = makeIsGroupHom λ _ _ → refl + compMorph : ∀ {ℓ} (n : ℤ) {A B C : Pointed ℓ} (g : B →∙ C) (f : A →∙ B) → + compGroupHom (theMorph n g) (theMorph n f) ≡ theMorph n (g ∘∙ f) + compMorph (pos zero) g f = + Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt (ST.elim (λ _ → isSetPathImplicit) + λ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isSetℤ _ _) refl))) + compMorph (pos (suc n)) f g = + Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt (ST.elim (λ _ → isSetPathImplicit) + λ _ → refl)) + compMorph (negsuc n) g f = + Σ≡Prop (λ _ → isPropIsGroupHom _ _) refl + + idMorph : ∀ {ℓ} (n : ℤ) {A : Pointed ℓ} → theMorph n (idfun∙ A) ≡ idGroupHom + idMorph (pos zero) = Σ≡Prop (λ _ → isPropIsGroupHom _ _) + (funExt (ST.elim (λ _ → isSetPathImplicit) + λ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isSetℤ _ _) refl))) + idMorph (pos (suc n)) = Σ≡Prop (λ _ → isPropIsGroupHom _ _) + (funExt (ST.elim (λ _ → isSetPathImplicit) λ _ → refl)) + idMorph (negsuc n) = refl + open coHomTheory isCohomTheoryZ' : ∀ {ℓ} → coHomTheory {ℓ} coHomFunctor' Hmap isCohomTheoryZ' = theMorph + HMapComp isCohomTheoryZ' = compMorph + HMapId isCohomTheoryZ' = idMorph -------------------------- Suspension -------------------------- -- existence of suspension isomorphism