From 1e251b8a64f7b8e1d7f8e11aa78c92b6689f226e Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Fri, 2 Aug 2024 14:02:16 +0200 Subject: [PATCH] Revert "WIP: deactivate problematic code" This reverts commit d7192ee08aba2d4bcaa6248fa49e953f22826dad. --- .../Multivariate/EquivCarac/A[X]X-A.agda | 3 +- .../Multivariate/EquivCarac/An[X]X-A.agda | 62 +- .../EilenbergMacLane/Rings/KleinBottle.agda | 600 +++++++++--------- .../EilenbergMacLane/Rings/RP2.agda | 118 ++-- .../EilenbergMacLane/Rings/RP2wedgeS1.agda | 34 +- .../Cohomology/EilenbergMacLane/Rings/Sn.agda | 218 ++++--- Cubical/ZCohomology/CohomologyRings/CP2.agda | 3 +- .../CohomologyRings/KleinBottle.agda | 3 +- Cubical/ZCohomology/CohomologyRings/RP2.agda | 3 +- .../CohomologyRings/RP2wedgeS1.agda | 3 +- Cubical/ZCohomology/CohomologyRings/S0.agda | 3 +- Cubical/ZCohomology/CohomologyRings/S1.agda | 3 +- .../CohomologyRings/S2wedgeS4.agda | 3 +- Cubical/ZCohomology/CohomologyRings/Sn.agda | 52 +- Cubical/ZCohomology/CohomologyRings/Unit.agda | 3 +- 15 files changed, 539 insertions(+), 572 deletions(-) diff --git a/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/A[X]X-A.agda b/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/A[X]X-A.agda index 71f5b38c06..dc41f35a12 100644 --- a/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/A[X]X-A.agda +++ b/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/A[X]X-A.agda @@ -190,7 +190,7 @@ module Properties-Equiv-QuotientXn-A A→A[x]/x : A → A[x]/x A→A[x]/x = [_] ∘ A→A[x] -{- + A→A[x]/x-pres+ : (a a' : A) → A→A[x]/x (a +A a') ≡ A→A[x]/x a +PAI A→A[x]/x a' A→A[x]/x-pres+ a a' = cong [_] (A→A[x]-pres+ a a') @@ -247,4 +247,3 @@ module _ Equiv-ℤ[X]/X-ℤ : RingEquiv (CommRing→Ring ℤ[X]/X) (CommRing→Ring ℤCR) Equiv-ℤ[X]/X-ℤ = Equiv-A[X]/X-A ℤCR --- -} diff --git a/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/An[X]X-A.agda b/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/An[X]X-A.agda index f77fa7c596..2d2f46f80f 100644 --- a/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/An[X]X-A.agda +++ b/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/An[X]X-A.agda @@ -19,7 +19,6 @@ open import Cubical.Algebra.Ring open import Cubical.Algebra.CommRing open import Cubical.Algebra.CommRing.FGIdeal open import Cubical.Algebra.CommRing.Quotient -open import Cubical.Algebra.Monoid.Instances.NatVec open import Cubical.Algebra.CommRing.Instances.Int renaming (ℤCommRing to ℤCR) @@ -217,39 +216,37 @@ module Properties-Equiv-QuotientXn-A ... | no ¬p = ⊥.rec (¬p refl) -{- + ----------------------------------------------------------------------------- -- Retraction open RingStr open IsRing - opaque - unfolding quotientCommRingStr - e-retr : (x : A[x1,···,xn]/ Ar n) → A→PAI (PAI→A x) ≡ x - e-retr = SQ.elimProp (λ _ → isSetPAI _ _) - (DS-Ind-Prop.f (NatVecMonoid n .fst) (λ _ → A) _ _ (λ _ → isSetPAI _ _) - base0-eq - base-eq - λ {U V} ind-U ind-V → cong [_] (A→PA-pres+ _ _) ∙ cong₂ _+PAI_ ind-U ind-V) - where - base0-eq : A→PAI (PAI→A [ 0PA ]) ≡ [ 0PA ] - base0-eq = cong [_] (base-neutral (replicate 0)) - - base-eq : (v : Vec ℕ n) → (a : A ) → [ A→PA (PA→A (base v a)) ] ≡ [ base v a ] - base-eq v a with (discreteVecℕn v (replicate 0)) - ... | yes p = cong [_] (cong (λ X → base X a) (sym p)) - ... | no ¬p with (pred-vec-≢0 v ¬p) - ... | k , v' , infkn , eqvv' = eq/ (base (replicate 0) 0A) - (base v a) ∣ ((genδ-FinVec n k (base v' (-A a)) 0PA) , helper) ∣₁ - where - helper : {!!} ≡ _ - helper = cong (λ X → X +PA base v (-A a)) (base-neutral (replicate 0)) - ∙ +PAIdL (base v (-A a)) - ∙ sym ( - genδ-FinVec-ℕLinearCombi ((A[X1,···,Xn] Ar n)) n k infkn (base v' (-A a)) ( Ar n) - ∙ cong₂ base (cong (λ X → v' +n-vec δℕ-Vec n X) (toFromId' n k infkn)) (·AIdR _) - ∙ cong (λ X → base X (-A a)) (sym eqvv')) + e-retr : (x : A[x1,···,xn]/ Ar n) → A→PAI (PAI→A x) ≡ x + e-retr = SQ.elimProp (λ _ → isSetPAI _ _) + (DS-Ind-Prop.f _ _ _ _ (λ _ → isSetPAI _ _) + base0-eq + base-eq + λ {U V} ind-U ind-V → cong [_] (A→PA-pres+ _ _) ∙ cong₂ _+PAI_ ind-U ind-V) + where + base0-eq : A→PAI (PAI→A [ 0PA ]) ≡ [ 0PA ] + base0-eq = cong [_] (base-neutral (replicate 0)) + + base-eq : (v : Vec ℕ n) → (a : A ) → [ A→PA (PA→A (base v a)) ] ≡ [ base v a ] + base-eq v a with (discreteVecℕn v (replicate 0)) + ... | yes p = cong [_] (cong (λ X → base X a) (sym p)) + ... | no ¬p with (pred-vec-≢0 v ¬p) + ... | k , v' , infkn , eqvv' = eq/ (base (replicate 0) 0A) + (base v a) ∣ ((genδ-FinVec n k (base v' (-A a)) 0PA) , helper) ∣₁ + where + helper : _ + helper = cong (λ X → X +PA base v (-A a)) (base-neutral (replicate 0)) + ∙ +PAIdL (base v (-A a)) + ∙ sym ( + genδ-FinVec-ℕLinearCombi ((A[X1,···,Xn] Ar n)) n k infkn (base v' (-A a)) ( Ar n) + ∙ cong₂ base (cong (λ X → v' +n-vec δℕ-Vec n X) (toFromId' n k infkn)) (·AIdR _) + ∙ cong (λ X → base X (-A a)) (sym eqvv')) @@ -257,17 +254,17 @@ module Properties-Equiv-QuotientXn-A -- Equiv module _ - (R : CommRing ℓ) + (Ar@(A , Astr) : CommRing ℓ) (n : ℕ) where open Iso - open Properties-Equiv-QuotientXn-A R n + open Properties-Equiv-QuotientXn-A Ar n - Equiv-QuotientX-A : CommRingEquiv (A[X1,···,Xn]/ R n) R + Equiv-QuotientX-A : CommRingEquiv (A[X1,···,Xn]/ Ar n) Ar fst Equiv-QuotientX-A = isoToEquiv is where - is : Iso (A[x1,···,xn]/ R n) (R .fst) + is : Iso (A[x1,···,xn]/ Ar n) A fun is = PAI→A inv is = A→PAI rightInv is = e-sect @@ -276,4 +273,3 @@ module _ -- Warning this doesn't prove Z[X]/X ≅ ℤ because you get two definition, -- see notation Multivariate-Quotient-notationZ for more details --} diff --git a/Cubical/Cohomology/EilenbergMacLane/Rings/KleinBottle.agda b/Cubical/Cohomology/EilenbergMacLane/Rings/KleinBottle.agda index d7bcb5b82e..06ff30e2b5 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Rings/KleinBottle.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Rings/KleinBottle.agda @@ -853,318 +853,312 @@ isHomℤ/2[X,Y]→H*Klein = makeIsRingHom refl (λ _ _ → refl) ∙∙ H²K²→ℤ/2→H²K² (_⌣_ {G'' = ℤ/2Ring} K²gen.α K²gen.α) -- Map H*(K²) → ℤ/2[X,Y]/I -opaque - unfolding quotientCommRingStr - H*Klein→ℤ/2[X,Y]/I : - fst (H*R ℤ/2Ring KleinBottle) - → fst (CommRing→Ring ℤ/2[X,Y]/) - H*Klein→ℤ/2[X,Y]/I = - DS-Rec-Set.f _ _ _ _ squash/ [ neutral ] - HⁿKlein→ℤ/2[X,Y]/I _ - (+Assoc (snd (CommRing→Ring ℤ/2[X,Y]/))) - (+IdR (snd (CommRing→Ring ℤ/2[X,Y]/))) - (+Comm (snd (CommRing→Ring ℤ/2[X,Y]/))) - (λ { zero → cong [_] (base-neutral _) - ; one → cong [_] (cong₂ _add_ (base-neutral _) (base-neutral _) - ∙ addRid neutral) - ; two → cong [_] (cong (base (2 ∷ 0 ∷ [])) - (IsGroupHom.pres1 (snd (H²[K²,ℤ/2]≅ℤ/2*))) - ∙ base-neutral _) - ; (suc (suc (suc r))) → refl}) - λ { zero a b → cong [_] (base-add _ _ _ ∙ cong (base (0 ∷ 0 ∷ [])) - (sym (IsGroupHom.pres· (snd (H⁰[K²,ℤ/2]≅ℤ/2)) a b))) - ; one a b → cong [_] (move4 _ _ _ _ _add_ addAssoc addComm - ∙ cong₂ _add_ (base-add _ _ _ ∙ cong (base (1 ∷ 0 ∷ [])) - (cong fst (sym - (IsGroupHom.pres· (snd (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2)) a b)))) - (base-add _ _ _ ∙ cong (base (0 ∷ 1 ∷ [])) - (cong snd - (sym (IsGroupHom.pres· (snd (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2)) a b))))) - ; two a b → cong [_] (base-add _ _ _ ∙ cong (base (2 ∷ 0 ∷ [])) - (sym (IsGroupHom.pres· (snd (H²[K²,ℤ/2]≅ℤ/2*)) a b))) - ; (suc (suc (suc n))) → λ a b → cong [_] (addRid neutral)} +H*Klein→ℤ/2[X,Y]/I : + fst (H*R ℤ/2Ring KleinBottle) + → fst (CommRing→Ring ℤ/2[X,Y]/) +H*Klein→ℤ/2[X,Y]/I = + DS-Rec-Set.f _ _ _ _ squash/ [ neutral ] + HⁿKlein→ℤ/2[X,Y]/I _ + (+Assoc (snd (CommRing→Ring ℤ/2[X,Y]/))) + (+IdR (snd (CommRing→Ring ℤ/2[X,Y]/))) + (+Comm (snd (CommRing→Ring ℤ/2[X,Y]/))) + (λ { zero → cong [_] (base-neutral _) + ; one → cong [_] (cong₂ _add_ (base-neutral _) (base-neutral _) + ∙ addRid neutral) + ; two → cong [_] (cong (base (2 ∷ 0 ∷ [])) + (IsGroupHom.pres1 (snd (H²[K²,ℤ/2]≅ℤ/2*))) + ∙ base-neutral _) + ; (suc (suc (suc r))) → refl}) + λ { zero a b → cong [_] (base-add _ _ _ ∙ cong (base (0 ∷ 0 ∷ [])) + (sym (IsGroupHom.pres· (snd (H⁰[K²,ℤ/2]≅ℤ/2)) a b))) + ; one a b → cong [_] (move4 _ _ _ _ _add_ addAssoc addComm + ∙ cong₂ _add_ (base-add _ _ _ ∙ cong (base (1 ∷ 0 ∷ [])) + (cong fst (sym + (IsGroupHom.pres· (snd (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2)) a b)))) + (base-add _ _ _ ∙ cong (base (0 ∷ 1 ∷ [])) + (cong snd + (sym (IsGroupHom.pres· (snd (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2)) a b))))) + ; two a b → cong [_] (base-add _ _ _ ∙ cong (base (2 ∷ 0 ∷ [])) + (sym (IsGroupHom.pres· (snd (H²[K²,ℤ/2]≅ℤ/2*)) a b))) + ; (suc (suc (suc n))) → λ a b → cong [_] (addRid neutral)} -- The equivalence -{- -opaque - unfolding quotientCommRingStr H*Klein→ℤ/2[X,Y]/I - ℤ/2[X,Y]/≅H*KleinBottle : - RingEquiv (CommRing→Ring ℤ/2[X,Y]/) - (H*R ℤ/2Ring KleinBottle) - fst ℤ/2[X,Y]/≅H*KleinBottle = isoToEquiv is +ℤ/2[X,Y]/≅H*KleinBottle : + RingEquiv (CommRing→Ring ℤ/2[X,Y]/) + (H*R ℤ/2Ring KleinBottle) +fst ℤ/2[X,Y]/≅H*KleinBottle = isoToEquiv is + where + is : Iso _ _ + fun is = ℤ/2[X,Y]/I→H*Klein .fst + inv is = H*Klein→ℤ/2[X,Y]/I + rightInv is = DS-Ind-Prop.f _ _ _ _ + (λ _ → trunc _ _) + refl + (λ { zero a → lem₀ a _ refl + ; one a → lem₁ a _ _ refl + ; two a → lem₂ a _ refl + ; (suc (suc (suc r))) a → + sym (base-neutral _) + ∙ cong (base (3 + r)) + (isContr→isProp (isContr-HⁿKleinBottle r ℤ/2) + (0ₕ (3 + r)) a)}) + λ {x} {y} ind1 ind2 + → IsRingHom.pres+ (ℤ/2[X,Y]/I→H*Klein .snd) + (H*Klein→ℤ/2[X,Y]/I x) (H*Klein→ℤ/2[X,Y]/I y) + ∙ cong₂ _add_ ind1 ind2 where - is : Iso _ _ - fun is = ℤ/2[X,Y]/I→H*Klein .fst - inv is = H*Klein→ℤ/2[X,Y]/I - rightInv is = DS-Ind-Prop.f _ _ _ _ - (λ _ → trunc _ _) - refl - (λ { zero a → lem₀ a _ refl - ; one a → lem₁ a _ _ refl - ; two a → lem₂ a _ refl - ; (suc (suc (suc r))) a → - sym (base-neutral _) - ∙ cong (base (3 + r)) - (isContr→isProp (isContr-HⁿKleinBottle r ℤ/2) - (0ₕ (3 + r)) a)}) - λ {x} {y} ind1 ind2 - → IsRingHom.pres+ (ℤ/2[X,Y]/I→H*Klein .snd) - (H*Klein→ℤ/2[X,Y]/I x) (H*Klein→ℤ/2[X,Y]/I y) - ∙ cong₂ _add_ ind1 ind2 - where - lem₀ : (a : _) (x : _) - → H⁰[K²,ℤ/2]≅ℤ/2 .fst .fst a ≡ x - → ℤ/2[X,Y]/I→H*Klein .fst (H*Klein→ℤ/2[X,Y]/I (base zero a)) - ≡ base zero a - lem₀ a = - ℤ/2-elim - (λ id → cong (ℤ/2[X,Y]/I→H*Klein .fst ∘ H*Klein→ℤ/2[X,Y]/I) (help id) - ∙ sym (help id)) - λ id → cong (ℤ/2[X,Y]/I→H*Klein .fst) - (cong [_] (cong (base (0 ∷ 0 ∷ [])) id)) - ∙ cong (base zero) - (sym (cong (invEq (H⁰[K²,ℤ/2]≅ℤ/2 .fst)) id) - ∙ retEq (fst H⁰[K²,ℤ/2]≅ℤ/2) a) - where - help : H⁰[K²,ℤ/2]≅ℤ/2 .fst .fst a ≡ 0 - → Path (fst (H*R ℤ/2Ring KleinBottle)) (base zero a) neutral - help id' = - sym (cong (base zero) - (sym (cong (invEq (H⁰[K²,ℤ/2]≅ℤ/2 .fst)) id' - ∙ IsGroupHom.pres1 (isGroupHomInv (H⁰[K²,ℤ/2]≅ℤ/2))) - ∙ retEq (fst H⁰[K²,ℤ/2]≅ℤ/2) a)) - ∙ base-neutral zero - - lem₁ : (a : _) → (x y : _) - → H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst .fst a ≡ (x , y) - → ℤ/2[X,Y]/I→H*Klein .fst (H*Klein→ℤ/2[X,Y]/I (base one a)) - ≡ base one a - lem₁ a = - ℤ/2-elim - (ℤ/2-elim - (λ id → cong (ℤ/2[X,Y]/I→H*Klein .fst ∘ [_]) - (cong₂ _add_ (cong (base (1 ∷ 0 ∷ [])) - (cong fst id)) - (cong (base (0 ∷ 1 ∷ [])) - (cong snd id))) - ∙ addRid neutral - ∙ sym (help a id)) - λ id → cong (ℤ/2[X,Y]/I→H*Klein .fst ∘ [_]) - (cong₂ _add_ - (cong (base (1 ∷ 0 ∷ [])) (cong fst id) - ∙ base-neutral _) - (cong (base (0 ∷ 1 ∷ [])) (cong snd id)) - ∙ addComm _ _ ∙ addRid _) - ∙∙ cong (base 1) (1ₕ-⌣ 1 K²gen.β) - ∙∙ cong (base 1) (sym (retEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst) K²gen.β) - ∙∙ cong (invEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst)) (sym id) - ∙∙ retEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst) a)) - (ℤ/2-elim - (λ id → (cong (ℤ/2[X,Y]/I→H*Klein .fst ∘ [_]) - (cong₂ _add_ - (cong (base (1 ∷ 0 ∷ [])) (cong fst id)) - (cong (base (0 ∷ 1 ∷ [])) (cong snd id) ∙ base-neutral _) - ∙ addRid _) - ∙ cong (base 1) - ( (⌣-1ₕ 1 K²gen.α ∙ transportRefl K²gen.α) - ∙ (sym (retEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst) K²gen.α) - ∙∙ cong (invEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst)) (α↦1 ∙ sym id) - ∙∙ retEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst) a)))) - λ id → cong (ℤ/2[X,Y]/I→H*Klein .fst ∘ [_]) - (cong₂ _add_ - (cong (base (1 ∷ 0 ∷ [])) (cong fst id)) - (cong (base (0 ∷ 1 ∷ [])) (cong snd id))) - ∙ IsRingHom.pres+ (snd ℤ/2[X,Y]/I→H*Klein) - [ base (1 ∷ 0 ∷ []) 1 ] [ base (0 ∷ 1 ∷ []) 1 ] - ∙ cong₂ _add_ - (cong (base one) (⌣-1ₕ 1 (incL 1) ∙ transportRefl K²gen.α)) - (cong (base one) (1ₕ-⌣ 1 (incR 1))) - ∙ base-add 1 K²gen.α K²gen.β - ∙ cong (base one) - (sym (retEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst) (K²gen.α +ₕ K²gen.β)) - ∙∙ (cong (invEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst)) (sym id)) - ∙∙ retEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst) a)) - where - help : (a : _) → H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst .fst a ≡ (0 , 0) - → Path (fst (H*R ℤ/2Ring KleinBottle)) (base one a) neutral - help a p = - (sym (cong (base one) - (sym (cong (invEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst)) p - ∙ IsGroupHom.pres1 (isGroupHomInv (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2))) - ∙ retEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst) a))) - ∙ base-neutral one - - lem₂ : (a : _) (x : _) → H²[K²,ℤ/2]≅ℤ/2* .fst .fst a ≡ x - → ℤ/2[X,Y]/I→H*Klein .fst (H*Klein→ℤ/2[X,Y]/I (base two a)) - ≡ base two a - lem₂ a = - ℤ/2-elim - (λ id → cong (ℤ/2[X,Y]/I→H*Klein .fst ∘ H*Klein→ℤ/2[X,Y]/I) - (cong (base 2) (help1 id) ∙ base-neutral _) - ∙∙ sym (base-neutral _) - ∙∙ cong (base 2) (sym (help1 id))) - λ id → cong (ℤ/2[X,Y]/I→H*Klein .fst) - (cong [_] (cong (base (2 ∷ 0 ∷ [])) - (cong (H²[K²,ℤ/2]≅ℤ/2* .fst .fst) (help2 id) - ∙ α²↦1') )) - ∙∙ cong (base 2) (⌣-1ₕ 2 (incL 2) ∙ transportRefl (incL 2)) - ∙∙ cong (base two) (sym (help2 id)) - where - help1 : H²[K²,ℤ/2]≅ℤ/2* .fst .fst a ≡ 0 → a ≡ 0ₕ 2 - help1 p = sym (retEq (H²[K²,ℤ/2]≅ℤ/2* .fst) a) - ∙ cong (invEq (H²[K²,ℤ/2]≅ℤ/2* .fst)) p - ∙ IsGroupHom.pres1 (isGroupHomInv H²[K²,ℤ/2]≅ℤ/2*) - - help2 : H²[K²,ℤ/2]≅ℤ/2* .fst .fst a ≡ 1 → a ≡ α⌣α - help2 p = sym (retEq (H²[K²,ℤ/2]≅ℤ/2* .fst) a) - ∙∙ cong (invEq (H²[K²,ℤ/2]≅ℤ/2* .fst)) (p ∙ sym α²↦1') - ∙∙ retEq (H²[K²,ℤ/2]≅ℤ/2* .fst) α⌣α - - leftInv is = - SQ.elimProp - (λ _ → squash/ _ _) - (DS-Ind-Prop.f _ _ _ _ - (λ _ → squash/ _ _) - refl - (λ r a → main a r) - λ {x} {y} ind1 ind2 - → cong₂ (_+r_ (snd (CommRing→Ring ℤ/2[X,Y]/))) - ind1 ind2) + lem₀ : (a : _) (x : _) + → H⁰[K²,ℤ/2]≅ℤ/2 .fst .fst a ≡ x + → ℤ/2[X,Y]/I→H*Klein .fst (H*Klein→ℤ/2[X,Y]/I (base zero a)) + ≡ base zero a + lem₀ a = + ℤ/2-elim + (λ id → cong (ℤ/2[X,Y]/I→H*Klein .fst ∘ H*Klein→ℤ/2[X,Y]/I) (help id) + ∙ sym (help id)) + λ id → cong (ℤ/2[X,Y]/I→H*Klein .fst) + (cong [_] (cong (base (0 ∷ 0 ∷ [])) id)) + ∙ cong (base zero) + (sym (cong (invEq (H⁰[K²,ℤ/2]≅ℤ/2 .fst)) id) + ∙ retEq (fst H⁰[K²,ℤ/2]≅ℤ/2) a) where - clem : (x y : ℕ) - → H*Klein→ℤ/2[X,Y]/I - (ℤ/2[X,Y]/I→H*Klein .fst - [ base (suc (suc (suc x)) ∷ y ∷ []) 1 ]) - ≡ [ neutral ] - clem x zero = refl - clem x (suc n) = refl - - help : (y : ℕ) → - Path (fst (CommRing→Ring ℤ/2[X,Y]/)) - [ base (one ∷ suc (suc y) ∷ []) 1 ] - [ neutral ] - help y = eq/ _ _ - ∣ (λ { zero → neutral - ; one → base (1 ∷ y ∷ []) 1 - ; two → neutral}) - , (sym (addRid _) - ∙ addComm (base (1 ∷ suc (suc y) ∷ []) 1 add neutral) neutral) - ∙ (λ i → neutral add (base (1 ∷ (+-comm 2 y i) ∷ []) 1 - add (addRid neutral (~ i)))) ∣₁ - - help2 : (y : ℕ) - → ℤ/2[X,Y]/I→H*Klein .fst [ base (zero ∷ suc (suc y) ∷ []) 1 ] - ≡ neutral - help2 zero = cong (base 2) (1ₕ-⌣ 2 (incR two)) - ∙ base-neutral _ - help2 (suc y) = base-neutral _ - - help3 : (x y : ℕ) - → ℤ/2[X,Y]/I→H*Klein .fst [ base (x ∷ suc (suc y) ∷ []) 1 ] - ≡ neutral - help3 zero y = help2 y - help3 (suc x) y = - (λ i → base (suc (suc (+-suc x y i))) - (transp (λ j → coHom (suc (suc (+-suc x y (i ∧ j)))) - ℤ/2 KleinBottle) (~ i) - (_⌣_ {G'' = ℤ/2Ring} (incL (suc x)) (incR (suc (suc y)))))) - ∙ cong (base (suc (suc (suc (x + y))))) - (isContr→isProp (isContr-HⁿKleinBottle (x + y) ℤ/2) _ _) - ∙ base-neutral _ - - main-1 : (r : _) - → H*Klein→ℤ/2[X,Y]/I (ℤ/2[X,Y]/I→H*Klein .fst [ base r 1 ]) - ≡ [ base r 1 ] - main-1 (zero ∷ zero ∷ []) = refl - main-1 (zero ∷ one ∷ []) = - cong (H*Klein→ℤ/2[X,Y]/I) - (cong (base 1) (1ₕ-⌣ 1 (incR 1))) - ∙ cong [_] (cong₂ _add_ (base-neutral _) - (λ _ → base (0 ∷ 1 ∷ []) 1) + help : H⁰[K²,ℤ/2]≅ℤ/2 .fst .fst a ≡ 0 + → Path (fst (H*R ℤ/2Ring KleinBottle)) (base zero a) neutral + help id' = + sym (cong (base zero) + (sym (cong (invEq (H⁰[K²,ℤ/2]≅ℤ/2 .fst)) id' + ∙ IsGroupHom.pres1 (isGroupHomInv (H⁰[K²,ℤ/2]≅ℤ/2))) + ∙ retEq (fst H⁰[K²,ℤ/2]≅ℤ/2) a)) + ∙ base-neutral zero + + lem₁ : (a : _) → (x y : _) + → H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst .fst a ≡ (x , y) + → ℤ/2[X,Y]/I→H*Klein .fst (H*Klein→ℤ/2[X,Y]/I (base one a)) + ≡ base one a + lem₁ a = + ℤ/2-elim + (ℤ/2-elim + (λ id → cong (ℤ/2[X,Y]/I→H*Klein .fst ∘ [_]) + (cong₂ _add_ (cong (base (1 ∷ 0 ∷ [])) + (cong fst id)) + (cong (base (0 ∷ 1 ∷ [])) + (cong snd id))) + ∙ addRid neutral + ∙ sym (help a id)) + λ id → cong (ℤ/2[X,Y]/I→H*Klein .fst ∘ [_]) + (cong₂ _add_ + (cong (base (1 ∷ 0 ∷ [])) (cong fst id) + ∙ base-neutral _) + (cong (base (0 ∷ 1 ∷ [])) (cong snd id)) ∙ addComm _ _ ∙ addRid _) - main-1 (zero ∷ suc (suc y) ∷ []) = - cong H*Klein→ℤ/2[X,Y]/I (help2 y) - ∙ eq/ _ _ - ∣ (λ {zero → neutral - ; one → base (0 ∷ (y ∷ [])) 1 - ; two → neutral}) - , cong (neutral add_) - (((λ i → base (0 ∷ (+-comm 2 y i) ∷ []) 1) - ∙ sym (addRid (base (0 ∷ (y + 2) ∷ []) 1))) - ∙ cong (base (0 ∷ (y + 2) ∷ []) 1 add_) (sym (addRid _))) ∣₁ - main-1 (one ∷ zero ∷ []) = - cong H*Klein→ℤ/2[X,Y]/I - (cong (base 1) (⌣-1ₕ 1 (incL one) ∙ transportRefl _)) - ∙ cong [_] (cong₂ _add_ (cong (base (1 ∷ 0 ∷ [])) - (cong fst α↦1)) - (base-neutral _) + ∙∙ cong (base 1) (1ₕ-⌣ 1 K²gen.β) + ∙∙ cong (base 1) (sym (retEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst) K²gen.β) + ∙∙ cong (invEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst)) (sym id) + ∙∙ retEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst) a)) + (ℤ/2-elim + (λ id → (cong (ℤ/2[X,Y]/I→H*Klein .fst ∘ [_]) + (cong₂ _add_ + (cong (base (1 ∷ 0 ∷ [])) (cong fst id)) + (cong (base (0 ∷ 1 ∷ [])) (cong snd id) ∙ base-neutral _) ∙ addRid _) - main-1 (one ∷ one ∷ []) = - cong [_] (cong (base (2 ∷ 0 ∷ [])) αβ↦1') - ∙ eq/ _ _ ∣ (λ {zero → neutral - ; one → neutral - ; two → base (0 ∷ 0 ∷ []) 1}) - , ((addComm _ _ - ∙ sym (addRid _) - ∙ addComm (base (1 ∷ 1 ∷ []) 1 - add (base (2 ∷ 0 ∷ []) 1)) - neutral - ∙ sym (addRid _) - ∙ addComm (neutral add (base (1 ∷ 1 ∷ []) 1 - add (base (2 ∷ 0 ∷ []) 1))) neutral) - ∙ λ i → neutral add - (neutral add (addRid - (base (1 ∷ 1 ∷ []) 1 - add (base (2 ∷ 0 ∷ []) 1)) (~ i)))) ∣₁ - main-1 (one ∷ suc (suc y) ∷ []) = - cong H*Klein→ℤ/2[X,Y]/I (help3 one y) ∙ sym (help y) - main-1 (two ∷ zero ∷ []) = - cong [_] (cong (base (2 ∷ 0 ∷ [])) - (cong (H²[K²,ℤ/2]≅ℤ/2* .fst .fst) - (⌣-1ₕ 2 (incL 2) ∙ transportRefl _) - ∙ α²↦1')) - main-1 (two ∷ suc y ∷ []) = - eq/ neutral _ - ∣ (λ {zero → base (0 ∷ y ∷ []) 1 - ; one → neutral - ; two → base (1 ∷ y ∷ []) 1}) - , ((addComm _ _ ∙ addRid _ - ∙ ((((λ i → base (2 ∷ +-comm 1 y i ∷ []) 1) - ∙ sym (addRid _)) - ∙ cong (base (2 ∷ y + 1 ∷ []) (fsuc fzero) add_) - (sym (base-neutral _) - ∙ sym (base-add (3 ∷ y + 0 ∷ []) 1 1))) - ∙ addComm _ _) - ∙ sym (addAssoc _ _ _)) - ∙∙ cong (base (3 ∷ y + 0 ∷ []) (fsuc fzero) add_) - (addComm _ _ - ∙ sym (addComm _ _ ∙ addRid _)) - ∙∙ (λ i → base (3 ∷ (y + 0) ∷ []) 1 - add (neutral - add addRid (base (2 ∷ (y + 1) ∷ []) 1 - add base (3 ∷ (y + 0) ∷ []) 1 ) (~ i)))) ∣₁ - main-1 (suc (suc (suc x)) ∷ y ∷ []) = - clem x y - ∙ eq/ neutral _ - ∣ (λ {zero → base (x ∷ y ∷ []) 1 - ; one → neutral - ; two → neutral}) - , ((addComm neutral (base ((3 + x) ∷ y ∷ []) 1) - ∙ cong (base ((3 + x) ∷ y ∷ []) 1 add_) (sym (addRid neutral))) - ∙ λ i → base ((+-comm 3 x i) ∷ (+-comm 0 y i) ∷ []) 1 - add (neutral add (addRid neutral (~ i)))) ∣₁ - - main : (a : ℤ/2 .fst) (r : _) - → H*Klein→ℤ/2[X,Y]/I (ℤ/2[X,Y]/I→H*Klein .fst [ base r a ]) ≡ [ base r a ] - main = ℤ/2-elim (λ r → cong (H*Klein→ℤ/2[X,Y]/I ∘ ℤ/2[X,Y]/I→H*Klein .fst) - (cong [_] (base-neutral r)) - ∙ cong [_] (sym (base-neutral r))) - main-1 - snd ℤ/2[X,Y]/≅H*KleinBottle = ℤ/2[X,Y]/I→H*Klein .snd + ∙ cong (base 1) + ( (⌣-1ₕ 1 K²gen.α ∙ transportRefl K²gen.α) + ∙ (sym (retEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst) K²gen.α) + ∙∙ cong (invEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst)) (α↦1 ∙ sym id) + ∙∙ retEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst) a)))) + λ id → cong (ℤ/2[X,Y]/I→H*Klein .fst ∘ [_]) + (cong₂ _add_ + (cong (base (1 ∷ 0 ∷ [])) (cong fst id)) + (cong (base (0 ∷ 1 ∷ [])) (cong snd id))) + ∙ IsRingHom.pres+ (snd ℤ/2[X,Y]/I→H*Klein) + [ base (1 ∷ 0 ∷ []) 1 ] [ base (0 ∷ 1 ∷ []) 1 ] + ∙ cong₂ _add_ + (cong (base one) (⌣-1ₕ 1 (incL 1) ∙ transportRefl K²gen.α)) + (cong (base one) (1ₕ-⌣ 1 (incR 1))) + ∙ base-add 1 K²gen.α K²gen.β + ∙ cong (base one) + (sym (retEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst) (K²gen.α +ₕ K²gen.β)) + ∙∙ (cong (invEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst)) (sym id)) + ∙∙ retEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst) a)) + where + help : (a : _) → H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst .fst a ≡ (0 , 0) + → Path (fst (H*R ℤ/2Ring KleinBottle)) (base one a) neutral + help a p = + (sym (cong (base one) + (sym (cong (invEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst)) p + ∙ IsGroupHom.pres1 (isGroupHomInv (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2))) + ∙ retEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst) a))) + ∙ base-neutral one + + lem₂ : (a : _) (x : _) → H²[K²,ℤ/2]≅ℤ/2* .fst .fst a ≡ x + → ℤ/2[X,Y]/I→H*Klein .fst (H*Klein→ℤ/2[X,Y]/I (base two a)) + ≡ base two a + lem₂ a = + ℤ/2-elim + (λ id → cong (ℤ/2[X,Y]/I→H*Klein .fst ∘ H*Klein→ℤ/2[X,Y]/I) + (cong (base 2) (help1 id) ∙ base-neutral _) + ∙∙ sym (base-neutral _) + ∙∙ cong (base 2) (sym (help1 id))) + λ id → cong (ℤ/2[X,Y]/I→H*Klein .fst) + (cong [_] (cong (base (2 ∷ 0 ∷ [])) + (cong (H²[K²,ℤ/2]≅ℤ/2* .fst .fst) (help2 id) + ∙ α²↦1') )) + ∙∙ cong (base 2) (⌣-1ₕ 2 (incL 2) ∙ transportRefl (incL 2)) + ∙∙ cong (base two) (sym (help2 id)) + where + help1 : H²[K²,ℤ/2]≅ℤ/2* .fst .fst a ≡ 0 → a ≡ 0ₕ 2 + help1 p = sym (retEq (H²[K²,ℤ/2]≅ℤ/2* .fst) a) + ∙ cong (invEq (H²[K²,ℤ/2]≅ℤ/2* .fst)) p + ∙ IsGroupHom.pres1 (isGroupHomInv H²[K²,ℤ/2]≅ℤ/2*) + + help2 : H²[K²,ℤ/2]≅ℤ/2* .fst .fst a ≡ 1 → a ≡ α⌣α + help2 p = sym (retEq (H²[K²,ℤ/2]≅ℤ/2* .fst) a) + ∙∙ cong (invEq (H²[K²,ℤ/2]≅ℤ/2* .fst)) (p ∙ sym α²↦1') + ∙∙ retEq (H²[K²,ℤ/2]≅ℤ/2* .fst) α⌣α + + leftInv is = + SQ.elimProp + (λ _ → squash/ _ _) + (DS-Ind-Prop.f _ _ _ _ + (λ _ → squash/ _ _) + refl + (λ r a → main a r) + λ {x} {y} ind1 ind2 + → cong₂ (_+r_ (snd (CommRing→Ring ℤ/2[X,Y]/))) + ind1 ind2) + where + clem : (x y : ℕ) + → H*Klein→ℤ/2[X,Y]/I + (ℤ/2[X,Y]/I→H*Klein .fst + [ base (suc (suc (suc x)) ∷ y ∷ []) 1 ]) + ≡ [ neutral ] + clem x zero = refl + clem x (suc n) = refl + + help : (y : ℕ) → + Path (fst (CommRing→Ring ℤ/2[X,Y]/)) + [ base (one ∷ suc (suc y) ∷ []) 1 ] + [ neutral ] + help y = eq/ _ _ + ∣ (λ { zero → neutral + ; one → base (1 ∷ y ∷ []) 1 + ; two → neutral}) + , (sym (addRid _) + ∙ addComm (base (1 ∷ suc (suc y) ∷ []) 1 add neutral) neutral) + ∙ (λ i → neutral add (base (1 ∷ (+-comm 2 y i) ∷ []) 1 + add (addRid neutral (~ i)))) ∣₁ + + help2 : (y : ℕ) + → ℤ/2[X,Y]/I→H*Klein .fst [ base (zero ∷ suc (suc y) ∷ []) 1 ] + ≡ neutral + help2 zero = cong (base 2) (1ₕ-⌣ 2 (incR two)) + ∙ base-neutral _ + help2 (suc y) = base-neutral _ + + help3 : (x y : ℕ) + → ℤ/2[X,Y]/I→H*Klein .fst [ base (x ∷ suc (suc y) ∷ []) 1 ] + ≡ neutral + help3 zero y = help2 y + help3 (suc x) y = + (λ i → base (suc (suc (+-suc x y i))) + (transp (λ j → coHom (suc (suc (+-suc x y (i ∧ j)))) + ℤ/2 KleinBottle) (~ i) + (_⌣_ {G'' = ℤ/2Ring} (incL (suc x)) (incR (suc (suc y)))))) + ∙ cong (base (suc (suc (suc (x + y))))) + (isContr→isProp (isContr-HⁿKleinBottle (x + y) ℤ/2) _ _) + ∙ base-neutral _ + + main-1 : (r : _) + → H*Klein→ℤ/2[X,Y]/I (ℤ/2[X,Y]/I→H*Klein .fst [ base r 1 ]) + ≡ [ base r 1 ] + main-1 (zero ∷ zero ∷ []) = refl + main-1 (zero ∷ one ∷ []) = + cong (H*Klein→ℤ/2[X,Y]/I) + (cong (base 1) (1ₕ-⌣ 1 (incR 1))) + ∙ cong [_] (cong₂ _add_ (base-neutral _) + (λ _ → base (0 ∷ 1 ∷ []) 1) + ∙ addComm _ _ ∙ addRid _) + main-1 (zero ∷ suc (suc y) ∷ []) = + cong H*Klein→ℤ/2[X,Y]/I (help2 y) + ∙ eq/ _ _ + ∣ (λ {zero → neutral + ; one → base (0 ∷ (y ∷ [])) 1 + ; two → neutral}) + , cong (neutral add_) + (((λ i → base (0 ∷ (+-comm 2 y i) ∷ []) 1) + ∙ sym (addRid (base (0 ∷ (y + 2) ∷ []) 1))) + ∙ cong (base (0 ∷ (y + 2) ∷ []) 1 add_) (sym (addRid _))) ∣₁ + main-1 (one ∷ zero ∷ []) = + cong H*Klein→ℤ/2[X,Y]/I + (cong (base 1) (⌣-1ₕ 1 (incL one) ∙ transportRefl _)) + ∙ cong [_] (cong₂ _add_ (cong (base (1 ∷ 0 ∷ [])) + (cong fst α↦1)) + (base-neutral _) + ∙ addRid _) + main-1 (one ∷ one ∷ []) = + cong [_] (cong (base (2 ∷ 0 ∷ [])) αβ↦1') + ∙ eq/ _ _ ∣ (λ {zero → neutral + ; one → neutral + ; two → base (0 ∷ 0 ∷ []) 1}) + , ((addComm _ _ + ∙ sym (addRid _) + ∙ addComm (base (1 ∷ 1 ∷ []) 1 + add (base (2 ∷ 0 ∷ []) 1)) + neutral + ∙ sym (addRid _) + ∙ addComm (neutral add (base (1 ∷ 1 ∷ []) 1 + add (base (2 ∷ 0 ∷ []) 1))) neutral) + ∙ λ i → neutral add + (neutral add (addRid + (base (1 ∷ 1 ∷ []) 1 + add (base (2 ∷ 0 ∷ []) 1)) (~ i)))) ∣₁ + main-1 (one ∷ suc (suc y) ∷ []) = + cong H*Klein→ℤ/2[X,Y]/I (help3 one y) ∙ sym (help y) + main-1 (two ∷ zero ∷ []) = + cong [_] (cong (base (2 ∷ 0 ∷ [])) + (cong (H²[K²,ℤ/2]≅ℤ/2* .fst .fst) + (⌣-1ₕ 2 (incL 2) ∙ transportRefl _) + ∙ α²↦1')) + main-1 (two ∷ suc y ∷ []) = + eq/ neutral _ + ∣ (λ {zero → base (0 ∷ y ∷ []) 1 + ; one → neutral + ; two → base (1 ∷ y ∷ []) 1}) + , ((addComm _ _ ∙ addRid _ + ∙ ((((λ i → base (2 ∷ +-comm 1 y i ∷ []) 1) + ∙ sym (addRid _)) + ∙ cong (base (2 ∷ y + 1 ∷ []) (fsuc fzero) add_) + (sym (base-neutral _) + ∙ sym (base-add (3 ∷ y + 0 ∷ []) 1 1))) + ∙ addComm _ _) + ∙ sym (addAssoc _ _ _)) + ∙∙ cong (base (3 ∷ y + 0 ∷ []) (fsuc fzero) add_) + (addComm _ _ + ∙ sym (addComm _ _ ∙ addRid _)) + ∙∙ (λ i → base (3 ∷ (y + 0) ∷ []) 1 + add (neutral + add addRid (base (2 ∷ (y + 1) ∷ []) 1 + add base (3 ∷ (y + 0) ∷ []) 1 ) (~ i)))) ∣₁ + main-1 (suc (suc (suc x)) ∷ y ∷ []) = + clem x y + ∙ eq/ neutral _ + ∣ (λ {zero → base (x ∷ y ∷ []) 1 + ; one → neutral + ; two → neutral}) + , ((addComm neutral (base ((3 + x) ∷ y ∷ []) 1) + ∙ cong (base ((3 + x) ∷ y ∷ []) 1 add_) (sym (addRid neutral))) + ∙ λ i → base ((+-comm 3 x i) ∷ (+-comm 0 y i) ∷ []) 1 + add (neutral add (addRid neutral (~ i)))) ∣₁ + + main : (a : ℤ/2 .fst) (r : _) + → H*Klein→ℤ/2[X,Y]/I (ℤ/2[X,Y]/I→H*Klein .fst [ base r a ]) ≡ [ base r a ] + main = ℤ/2-elim (λ r → cong (H*Klein→ℤ/2[X,Y]/I ∘ ℤ/2[X,Y]/I→H*Klein .fst) + (cong [_] (base-neutral r)) + ∙ cong [_] (sym (base-neutral r))) + main-1 +snd ℤ/2[X,Y]/≅H*KleinBottle = ℤ/2[X,Y]/I→H*Klein .snd H*KleinBottle≅ℤ/2[X,Y]/ : RingEquiv (H*R ℤ/2Ring KleinBottle) (CommRing→Ring ℤ/2[X,Y]/) H*KleinBottle≅ℤ/2[X,Y]/ = RingEquivs.invRingEquiv ℤ/2[X,Y]/≅H*KleinBottle --- -} diff --git a/Cubical/Cohomology/EilenbergMacLane/Rings/RP2.agda b/Cubical/Cohomology/EilenbergMacLane/Rings/RP2.agda index 2ca66de1ff..db570dcc10 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Rings/RP2.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Rings/RP2.agda @@ -379,66 +379,64 @@ module _ {ℓ : Level} (n : ℕ) where 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) ] - opaque - unfolding H*Klein→ℤ/2[X,Y]/I quotientCommRingStr - 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) + 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²,ℤ₂] = diff --git a/Cubical/Cohomology/EilenbergMacLane/Rings/RP2wedgeS1.agda b/Cubical/Cohomology/EilenbergMacLane/Rings/RP2wedgeS1.agda index 0896082589..d328f4afcf 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Rings/RP2wedgeS1.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Rings/RP2wedgeS1.agda @@ -618,10 +618,8 @@ module Equiv-RP²∨S¹-Properties ℤ/2[x,y]/→H*-RP²∨S¹ : ℤ/2[x,y]/ → H*ℤ/2 RP²∨S¹ ℤ/2[x,y]/→H*-RP²∨S¹ = fst ℤ/2[X,Y]/→H*R-RP²∨S¹ - opaque - unfolding H*Klein→ℤ/2[X,Y]/I - ℤ/2[x,y]/→H*-RP²∨S¹-pres0 : ℤ/2[x,y]/→H*-RP²∨S¹ 0Pℤ/2I ≡ 0H* - ℤ/2[x,y]/→H*-RP²∨S¹-pres0 = refl + ℤ/2[x,y]/→H*-RP²∨S¹-pres0 : ℤ/2[x,y]/→H*-RP²∨S¹ 0Pℤ/2I ≡ 0H* + ℤ/2[x,y]/→H*-RP²∨S¹-pres0 = refl ℤ/2[x,y]/→H*-RP²∨S¹-pres+ : (x y : ℤ/2[x,y]/) → ℤ/2[x,y]/→H*-RP²∨S¹ ( x +Pℤ/2I y) @@ -672,15 +670,13 @@ module Equiv-RP²∨S¹-Properties H*-RP²∨S¹→ℤ/2[x,y]/ : H*ℤ/2 RP²∨S¹ → ℤ/2[x,y]/ H*-RP²∨S¹→ℤ/2[x,y]/ = [_] ∘ H*-RP²∨S¹→ℤ/2[x,y] - opaque - unfolding H*Klein→ℤ/2[X,Y]/I - H*-RP²∨S¹→ℤ/2[x,y]/-pres0 : H*-RP²∨S¹→ℤ/2[x,y]/ 0H* ≡ 0Pℤ/2I - H*-RP²∨S¹→ℤ/2[x,y]/-pres0 = refl + H*-RP²∨S¹→ℤ/2[x,y]/-pres0 : H*-RP²∨S¹→ℤ/2[x,y]/ 0H* ≡ 0Pℤ/2I + H*-RP²∨S¹→ℤ/2[x,y]/-pres0 = refl - H*-RP²∨S¹→ℤ/2[x,y]/-pres+ : (x y : H*ℤ/2 RP²∨S¹) → - H*-RP²∨S¹→ℤ/2[x,y]/ (x +H* y) - ≡ (H*-RP²∨S¹→ℤ/2[x,y]/ x) +Pℤ/2I (H*-RP²∨S¹→ℤ/2[x,y]/ y) - H*-RP²∨S¹→ℤ/2[x,y]/-pres+ x y = refl + H*-RP²∨S¹→ℤ/2[x,y]/-pres+ : (x y : H*ℤ/2 RP²∨S¹) → + H*-RP²∨S¹→ℤ/2[x,y]/ (x +H* y) + ≡ (H*-RP²∨S¹→ℤ/2[x,y]/ x) +Pℤ/2I (H*-RP²∨S¹→ℤ/2[x,y]/ y) + H*-RP²∨S¹→ℤ/2[x,y]/-pres+ x y = refl ----------------------------------------------------------------------------- @@ -744,14 +740,12 @@ module Equiv-RP²∨S¹-Properties ∙ cong₂ baseP (cong₂ (λ X Y → X ∷ Y ∷ []) (+-comm _ _) (+-comm _ _)) (·ℤ/2IdR _)) - opaque - unfolding H*Klein→ℤ/2[X,Y]/I - e-retr : (x : ℤ/2[x,y]/) → H*-RP²∨S¹→ℤ/2[x,y]/ (ℤ/2[x,y]/→H*-RP²∨S¹ x) ≡ x - e-retr = SQ.elimProp (λ _ → isSetPℤ/2I _ _) - (DS-Ind-Prop.f _ _ _ _ (λ _ → isSetPℤ/2I _ _) - refl - e-retr-base - λ {U V} ind-U ind-V → cong₂ _+Pℤ/2I_ ind-U ind-V) + e-retr : (x : ℤ/2[x,y]/) → H*-RP²∨S¹→ℤ/2[x,y]/ (ℤ/2[x,y]/→H*-RP²∨S¹ x) ≡ x + e-retr = SQ.elimProp (λ _ → isSetPℤ/2I _ _) + (DS-Ind-Prop.f _ _ _ _ (λ _ → isSetPℤ/2I _ _) + refl + e-retr-base + λ {U V} ind-U ind-V → cong₂ _+Pℤ/2I_ ind-U ind-V) -- Computation of the Cohomology Ring diff --git a/Cubical/Cohomology/EilenbergMacLane/Rings/Sn.agda b/Cubical/Cohomology/EilenbergMacLane/Rings/Sn.agda index 62f4c0bb4d..7f494a47c9 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Rings/Sn.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Rings/Sn.agda @@ -245,118 +245,116 @@ module _ {ℓ : Level} (G : CommRing ℓ) (n : ℕ) where ∙ base-neutral (1 ∷ [])) help (gt x) = refl - opaque - unfolding quotientCommRingStr - H*[Sⁿ,G]→G[X]/-fun-coh₂ : (r : ℕ) (x y : coHom r GAb (S₊ (suc n))) + 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 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 + (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 : _) (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]→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))) diff --git a/Cubical/ZCohomology/CohomologyRings/CP2.agda b/Cubical/ZCohomology/CohomologyRings/CP2.agda index 6cfd837ffb..1b5ebe1b1f 100644 --- a/Cubical/ZCohomology/CohomologyRings/CP2.agda +++ b/Cubical/ZCohomology/CohomologyRings/CP2.agda @@ -362,7 +362,7 @@ module ComputeCP²Notation H*-CP²→ℤ[x]/x³ : H* CP² → ℤ[x]/x³ H*-CP²→ℤ[x]/x³ = [_] ∘ H*-CP²→ℤ[x] -{- + H*-CP²→ℤ[x]/x³-gmorph : (x y : H* CP²) → H*-CP²→ℤ[x]/x³ (x +H* y) ≡ (H*-CP²→ℤ[x]/x³ x) +PℤI (H*-CP²→ℤ[x]/x³ y) H*-CP²→ℤ[x]/x³-gmorph x y = refl @@ -454,4 +454,3 @@ snd CP²-CohomologyRing = snd ℤ[X]/X³→H*R-CP² CohomologyRing-CP² : RingEquiv (H*R CP²) (CommRing→Ring ℤ[X]/X³) CohomologyRing-CP² = RingEquivs.invRingEquiv CP²-CohomologyRing --- -} diff --git a/Cubical/ZCohomology/CohomologyRings/KleinBottle.agda b/Cubical/ZCohomology/CohomologyRings/KleinBottle.agda index b21c3cf935..0454d41bbd 100644 --- a/Cubical/ZCohomology/CohomologyRings/KleinBottle.agda +++ b/Cubical/ZCohomology/CohomologyRings/KleinBottle.agda @@ -370,7 +370,7 @@ module Equiv-𝕂²-Properties ℤ[x,y]/<2y,y²,xy,x²>→H*-𝕂² : ℤ[x,y]/<2y,y²,xy,x²> → H* KleinBottle ℤ[x,y]/<2y,y²,xy,x²>→H*-𝕂² = fst ℤ[X,Y]/<2Y,Y²,XY,X²>→H*R-𝕂² -{- + ℤ[x,y]/<2y,y²,xy,x²>→H*-𝕂²-pres0 : ℤ[x,y]/<2y,y²,xy,x²>→H*-𝕂² 0PℤI ≡ 0H* ℤ[x,y]/<2y,y²,xy,x²>→H*-𝕂²-pres0 = refl @@ -570,4 +570,3 @@ module _ where CohomologyRing-𝕂² : RingEquiv (H*R KleinBottle) (CommRing→Ring ℤ[X,Y]/<2Y,Y²,XY,X²>) CohomologyRing-𝕂² = RingEquivs.invRingEquiv 𝕂²-CohomologyRing --- -} diff --git a/Cubical/ZCohomology/CohomologyRings/RP2.agda b/Cubical/ZCohomology/CohomologyRings/RP2.agda index 668e5db41d..b17c6f6ab4 100644 --- a/Cubical/ZCohomology/CohomologyRings/RP2.agda +++ b/Cubical/ZCohomology/CohomologyRings/RP2.agda @@ -320,7 +320,7 @@ module Equiv-RP2-Properties where ℤ[x]/<2x,x²>→H*-RP² : ℤ[x]/<2x,x²> → H* RP² ℤ[x]/<2x,x²>→H*-RP² = fst ℤ[X]/<2X,X²>→H*R-RP² -{- + ℤ[x]/<2x,x²>→H*-RP²-pres0 : ℤ[x]/<2x,x²>→H*-RP² 0PℤI ≡ 0H* ℤ[x]/<2x,x²>→H*-RP²-pres0 = refl @@ -512,4 +512,3 @@ module _ where CohomologyRing-RP² : RingEquiv (H*R RP²) (CommRing→Ring ℤ[X]/<2X,X²>) CohomologyRing-RP² = RingEquivs.invRingEquiv RP²-CohomologyRing --- -} diff --git a/Cubical/ZCohomology/CohomologyRings/RP2wedgeS1.agda b/Cubical/ZCohomology/CohomologyRings/RP2wedgeS1.agda index 66fee63268..4c358d2960 100644 --- a/Cubical/ZCohomology/CohomologyRings/RP2wedgeS1.agda +++ b/Cubical/ZCohomology/CohomologyRings/RP2wedgeS1.agda @@ -371,7 +371,7 @@ module Equiv-RP²⋁S¹-Properties ℤ[x,y]/<2y,y²,xy,x²>→H*-RP²⋁S¹ : ℤ[x,y]/<2y,y²,xy,x²> → H* RP²⋁S¹ ℤ[x,y]/<2y,y²,xy,x²>→H*-RP²⋁S¹ = fst ℤ[X,Y]/<2Y,Y²,XY,X²>→H*R-RP²⋁S¹ -{- + ℤ[x,y]/<2y,y²,xy,x²>→H*-RP²⋁S¹-pres0 : ℤ[x,y]/<2y,y²,xy,x²>→H*-RP²⋁S¹ 0PℤI ≡ 0H* ℤ[x,y]/<2y,y²,xy,x²>→H*-RP²⋁S¹-pres0 = refl @@ -571,4 +571,3 @@ module _ where CohomologyRing-RP²⋁S¹ : RingEquiv (H*R RP²⋁S¹) (CommRing→Ring ℤ[X,Y]/<2Y,Y²,XY,X²>) CohomologyRing-RP²⋁S¹ = RingEquivs.invRingEquiv RP²⋁S¹-CohomologyRing --- -} diff --git a/Cubical/ZCohomology/CohomologyRings/S0.agda b/Cubical/ZCohomology/CohomologyRings/S0.agda index 6ac6cfaf53..1ce3385eb1 100644 --- a/Cubical/ZCohomology/CohomologyRings/S0.agda +++ b/Cubical/ZCohomology/CohomologyRings/S0.agda @@ -34,7 +34,7 @@ open import Cubical.ZCohomology.CohomologyRings.Unit -- Computation of the cohomology ring open RingEquivs -{- + Cohomology-Ring-S⁰P : RingEquiv (H*R (S₊ 0)) (DirectProd-Ring (CommRing→Ring ℤ[X]/X) (CommRing→Ring ℤ[X]/X)) Cohomology-Ring-S⁰P = compRingEquiv (CohomologyRing-Equiv (invIso Iso-⊤⊎⊤-Bool)) (compRingEquiv (CohomologyRing-Coproduct Unit Unit) @@ -44,4 +44,3 @@ Cohomology-Ring-S⁰ℤ : RingEquiv (H*R (S₊ 0)) (DirectProd-Ring (CommRing→ Cohomology-Ring-S⁰ℤ = compRingEquiv (CohomologyRing-Equiv (invIso Iso-⊤⊎⊤-Bool)) (compRingEquiv (CohomologyRing-Coproduct Unit Unit) (Coproduct-Equiv.Coproduct-Equiv-12 CohomologyRing-Unitℤ CohomologyRing-Unitℤ)) --} diff --git a/Cubical/ZCohomology/CohomologyRings/S1.agda b/Cubical/ZCohomology/CohomologyRings/S1.agda index f8ba962782..ac7b26e0f2 100644 --- a/Cubical/ZCohomology/CohomologyRings/S1.agda +++ b/Cubical/ZCohomology/CohomologyRings/S1.agda @@ -276,7 +276,7 @@ module Equiv-S1-Properties where H*-S¹→ℤ[x]/x² : H* (S₊ 1) → ℤ[x]/x² H*-S¹→ℤ[x]/x² = [_] ∘ H*-S¹→ℤ[x] -{- + H*-S¹→ℤ[x]/x²-pres+ : (x y : H* (S₊ 1)) → H*-S¹→ℤ[x]/x² (x +H* y) ≡ (H*-S¹→ℤ[x]/x² x) +PℤI (H*-S¹→ℤ[x]/x² y) H*-S¹→ℤ[x]/x²-pres+ x y = refl @@ -337,4 +337,3 @@ module _ where CohomologyRing-S¹ : RingEquiv (H*R (S₊ 1)) (CommRing→Ring ℤ[X]/X²) CohomologyRing-S¹ = RingEquivs.invRingEquiv S¹-CohomologyRing --- -} diff --git a/Cubical/ZCohomology/CohomologyRings/S2wedgeS4.agda b/Cubical/ZCohomology/CohomologyRings/S2wedgeS4.agda index 6e4b8e1a38..410ee7b9de 100644 --- a/Cubical/ZCohomology/CohomologyRings/S2wedgeS4.agda +++ b/Cubical/ZCohomology/CohomologyRings/S2wedgeS4.agda @@ -376,7 +376,7 @@ module Equiv-RP2-Properties where ℤ[x,y]/→H*-S²⋁S⁴ : ℤ[x,y]/ → H* S²⋁S⁴ ℤ[x,y]/→H*-S²⋁S⁴ = fst ℤ[X,Y]/→H*R-S²⋁S⁴ -{- + ℤ[x,y]/→H*-S²⋁S⁴-pres0 : ℤ[x,y]/→H*-S²⋁S⁴ 0PℤI ≡ 0H* ℤ[x,y]/→H*-S²⋁S⁴-pres0 = refl @@ -522,4 +522,3 @@ module _ where CohomologyRing-S²⋁S⁴ : RingEquiv (H*R S²⋁S⁴) (CommRing→Ring ℤ[X,Y]/) CohomologyRing-S²⋁S⁴ = RingEquivs.invRingEquiv S²⋁S⁴-CohomologyRing --- -} diff --git a/Cubical/ZCohomology/CohomologyRings/Sn.agda b/Cubical/ZCohomology/CohomologyRings/Sn.agda index 47b0f283b7..1c0c287859 100644 --- a/Cubical/ZCohomology/CohomologyRings/Sn.agda +++ b/Cubical/ZCohomology/CohomologyRings/Sn.agda @@ -334,10 +334,8 @@ module Equiv-Sn-Properties (n : ℕ) where H*-Sⁿ→ℤ[x]/x² : H* (S₊ (suc n)) → ℤ[x]/x² H*-Sⁿ→ℤ[x]/x² = [_] ∘ H*-Sⁿ→ℤ[x] - opaque - unfolding quotientCommRingStr - H*-Sⁿ→ℤ[x]/x²-pres+ : (x y : H* (S₊ (suc n))) → H*-Sⁿ→ℤ[x]/x² (x +H* y) ≡ (H*-Sⁿ→ℤ[x]/x² x) +PℤI (H*-Sⁿ→ℤ[x]/x² y) - H*-Sⁿ→ℤ[x]/x²-pres+ x y = refl + H*-Sⁿ→ℤ[x]/x²-pres+ : (x y : H* (S₊ (suc n))) → H*-Sⁿ→ℤ[x]/x² (x +H* y) ≡ (H*-Sⁿ→ℤ[x]/x² x) +PℤI (H*-Sⁿ→ℤ[x]/x² y) + H*-Sⁿ→ℤ[x]/x²-pres+ x y = refl @@ -368,30 +366,29 @@ module Equiv-Sn-Properties (n : ℕ) where ----------------------------------------------------------------------------- -- Retraction -{- - opaque - unfolding quotientCommRingStr - e-retr : (x : ℤ[x]/x²) → H*-Sⁿ→ℤ[x]/x² (ℤ[x]/x²→H*-Sⁿ x) ≡ x - e-retr = SQ.elimProp (λ _ → isSetPℤI _ _) - (DS-Ind-Prop.f _ _ _ _ (λ _ → isSetPℤI _ _) - refl - base-case - λ {U V} ind-U ind-V → cong₂ _+PℤI_ ind-U ind-V) + + e-retr : (x : ℤ[x]/x²) → H*-Sⁿ→ℤ[x]/x² (ℤ[x]/x²→H*-Sⁿ x) ≡ x + e-retr = SQ.elimProp (λ _ → isSetPℤI _ _) + (DS-Ind-Prop.f _ _ _ _ (λ _ → isSetPℤI _ _) + refl + base-case + λ {U V} ind-U ind-V → cong₂ _+PℤI_ ind-U ind-V) + where + base-case : _ + base-case (zero ∷ []) a = cong [_] (cong (base-trad-H* 0 (ϕ₀ a)) part0) + ∙ cong [_] (cong (base (0 ∷ [])) (cong ϕ₀⁻¹ (transportRefl (ϕ₀ a)))) + ∙ cong [_] (cong (base (0 ∷ [])) (ϕ₀-retr a)) + base-case (one ∷ []) a = cong [_] (cong (base-trad-H* (suc n) (ϕₙ a)) (partSn (part (suc n)))) + ∙ cong [_] (cong (base (1 ∷ [])) (cong ϕₙ⁻¹ (transportRefl (ϕₙ a)))) + ∙ cong [_] (cong (base (1 ∷ [])) (ϕₙ-retr a)) + base-case (suc (suc k) ∷ []) a = eq/ _ _ ∣ ((λ x → base (k ∷ []) (-ℤ a)) , helper) ∣₁ where - base-case : _ - base-case (zero ∷ []) a = cong [_] (cong (base-trad-H* 0 (ϕ₀ a)) part0) - ∙ cong [_] (cong (base (0 ∷ [])) (cong ϕ₀⁻¹ (transportRefl (ϕ₀ a)))) - ∙ cong [_] (cong (base (0 ∷ [])) (ϕ₀-retr a)) - base-case (one ∷ []) a = cong [_] (cong (base-trad-H* (suc n) (ϕₙ a)) (partSn (part (suc n)))) - ∙ cong [_] (cong (base (1 ∷ [])) (cong ϕₙ⁻¹ (transportRefl (ϕₙ a)))) - ∙ cong [_] (cong (base (1 ∷ [])) (ϕₙ-retr a)) - base-case (suc (suc k) ∷ []) a = eq/ _ _ ∣ ((λ x → base (k ∷ []) (-ℤ a)) , helper) ∣₁ - where - helper : _ - helper = (+PℤIdL _) - ∙ cong₂ base (cong (λ X → X ∷ []) - (sym (+n-comm k 2))) (sym (·ℤIdR _)) - ∙ (sym (+PℤIdR _)) + helper : _ + helper = (+PℤIdL _) + ∙ cong₂ base (cong (λ X → X ∷ []) + (sym (+n-comm k 2))) (sym (·ℤIdR _)) + ∙ (sym (+PℤIdR _)) + ----------------------------------------------------------------------------- @@ -413,4 +410,3 @@ module _ (n : ℕ) where CohomologyRing-Sⁿ : RingEquiv (H*R (S₊ (suc n))) (CommRing→Ring ℤ[X]/X²) CohomologyRing-Sⁿ = RingEquivs.invRingEquiv Sⁿ-CohomologyRing --- -} diff --git a/Cubical/ZCohomology/CohomologyRings/Unit.agda b/Cubical/ZCohomology/CohomologyRings/Unit.agda index 405b90e40e..600ac9858a 100644 --- a/Cubical/ZCohomology/CohomologyRings/Unit.agda +++ b/Cubical/ZCohomology/CohomologyRings/Unit.agda @@ -241,7 +241,7 @@ module Equiv-Unit-Properties where H*-Unit→ℤ[x]/x : H* Unit → ℤ[x]/x H*-Unit→ℤ[x]/x = [_] ∘ H*-Unit→ℤ[x] -{- + H*-Unit→ℤ[x]/x-pres+ : (x y : H* Unit) → H*-Unit→ℤ[x]/x (x +H* y) ≡ (H*-Unit→ℤ[x]/x x) +PℤI (H*-Unit→ℤ[x]/x y) H*-Unit→ℤ[x]/x-pres+ x y = cong [_] (H*-Unit→ℤ[x]-pres+ x y) @@ -314,4 +314,3 @@ module _ where CohomologyRing-Unitℤ : RingEquiv (H*R Unit) (CommRing→Ring ℤCR) CohomologyRing-Unitℤ = compRingEquiv CohomologyRing-UnitP Equiv-ℤ[X]/X-ℤ --- -}