Graded commutativity of cup product (#938)

* klein cup * cool * done? * stuff * fib-lemmas * GradedCommTensor.agda * stuff * more * closer * almost * almost * done * cleaner * done! * cleanup * fixes
agda · Oct 7, 2022 · 6e67e4a · 6e67e4a
1 parent 07069d9
commit 6e67e4a
Show file tree

Hide file tree

Showing 11 changed files with 1,580 additions and 14 deletions.
diff --git a/Cubical/Algebra/CommRing/Base.agda b/Cubical/Algebra/CommRing/Base.agda
@@ -15,6 +15,7 @@ open import Cubical.Displayed.Record
 open import Cubical.Displayed.Universe
 
 open import Cubical.Algebra.Ring.Base
+open import Cubical.Algebra.AbGroup
 
 open import Cubical.Reflection.RecordEquiv
 
@@ -95,6 +96,9 @@ CommRingStr→RingStr (commringstr _ _ _ _ _ H) = ringstr _ _ _ _ _ (IsCommRing.
 CommRing→Ring : CommRing ℓ → Ring ℓ
 CommRing→Ring (_ , commringstr _ _ _ _ _ H) = _ , ringstr _ _ _ _ _ (IsCommRing.isRing H)
 
+CommRing→AbGroup : CommRing ℓ → AbGroup ℓ
+CommRing→AbGroup R = Ring→AbGroup (CommRing→Ring R)
+
 Ring→CommRing : (R : Ring ℓ) → ((x y : (fst R)) → (RingStr._·_ (snd R) x y ≡ RingStr._·_ (snd R) y x)) → CommRing ℓ
 fst (Ring→CommRing R p) = fst R
 CommRingStr.0r (snd (Ring→CommRing R p)) = RingStr.0r (snd R)

diff --git a/Cubical/Cohomology/EilenbergMacLane/CupProduct.agda b/Cubical/Cohomology/EilenbergMacLane/CupProduct.agda
@@ -6,11 +6,18 @@ 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.EilenbergMacLane.Order2
+open import Cubical.Homotopy.EilenbergMacLane.GradedCommTensor
+  hiding (⌣ₖ-comm)
 
 open import Cubical.Cohomology.EilenbergMacLane.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.Foundations.Prelude
 open import Cubical.Foundations.HLevels
@@ -20,6 +27,8 @@ open import Cubical.HITs.EilenbergMacLane1
 open import Cubical.HITs.SetTruncation as ST
 
 open import Cubical.Data.Nat
+open import Cubical.Data.Sigma
+open import Cubical.Data.Sum
 
 open AbGroupStr renaming (_+_ to _+Gr_ ; -_ to -Gr_)
 open RingStr
@@ -95,7 +104,87 @@ module _ {G'' : Ring ℓ} {A : Type ℓ'} where
             ∙ cong (transport (λ i → EM G' (+'-assoc n m l i)))
                (cong (λ x → (f x ⌣ₖ (g x ⌣ₖ h x))) (sym (transportRefl x))))
 
--- dependent versions
+-- Graded commutativity
+-ₕ^[_·_] : {G' : AbGroup ℓ} {A : Type ℓ'} (n m : ℕ) {k : ℕ}
+  → coHom k G' A → coHom k G' A
+-ₕ^[ n · m ] = ST.map λ f x → -ₖ^[ n · m ] (f x)
+
+-ₕ^[_·_]-even : {G' : AbGroup ℓ} {A : Type ℓ'} (n m : ℕ) {k : ℕ}
+  → isEvenT n ⊎ isEvenT m
+  → (x : coHom k G' A) → -ₕ^[ n · m ] x ≡ x
+-ₕ^[ n · m ]-even {k = k} p =
+  ST.elim (λ _ → isSetPathImplicit)
+    λ f → cong ∣_∣₂ (funExt λ x → -ₖ^[ n · m ]-even p (f x))
+
+-ₕ^[_·_]-odd : {G' : AbGroup ℓ} {A : Type ℓ'} (n m : ℕ) {k : ℕ}
+  → isOddT n × isOddT m
+  → (x : coHom k G' A) → -ₕ^[ n · m ] x ≡ -ₕ x
+-ₕ^[ n · m ]-odd {k = k} p =
+  ST.elim (λ _ → isSetPathImplicit)
+    λ f → cong ∣_∣₂ (funExt λ x → -ₖ^[ n · m ]-odd p (f x))
+
+comm⌣ : {G'' : CommRing ℓ} {A : Type ℓ'} (n m : ℕ)
+  → (x : coHom n (CommRing→AbGroup G'') A)
+     (y : coHom m (CommRing→AbGroup G'') A)
+  → x ⌣ y ≡ subst (λ n → coHom n (CommRing→AbGroup G'') A)
+                   (+'-comm m n)
+                   (-ₕ^[ n · m ] (y ⌣ x))
+comm⌣ {G'' = R} {A = A} n m =
+  ST.elim2 (λ _ _ → isSetPathImplicit)
+   λ f g →
+     cong ∣_∣₂ (funExt λ x → ⌣ₖ-comm n m (f x) (g x)
+            ∙ cong (subst (λ n → EM (CommRing→AbGroup R) n) (+'-comm m n))
+                 (cong -ₖ^[ n · m ]
+                   (cong₂ _⌣ₖ_ (cong g (sym (transportRefl x)))
+                               (cong f (sym (transportRefl x))))))
+
+
+-- some syntax
+⌣[]-syntax : {A : Type ℓ} {n m : ℕ} (R : Ring ℓ')
+  → coHom n (Ring→AbGroup R) A
+  → coHom m (Ring→AbGroup R) A
+  → coHom (n +' m) (Ring→AbGroup R) A
+⌣[]-syntax R x y = x ⌣ y
+
+⌣[]C-syntax : {A : Type ℓ} {n m : ℕ} (R : CommRing ℓ')
+  → coHom n (CommRing→AbGroup R) A
+  → coHom m (CommRing→AbGroup R) A
+  → coHom (n +' m) (CommRing→AbGroup R) A
+⌣[]C-syntax R x y = x ⌣ y
+
+⌣[,,]-syntax : {A : Type ℓ} (n m : ℕ) (R : Ring ℓ')
+  → coHom n (Ring→AbGroup R) A
+  → coHom m (Ring→AbGroup R) A
+  → coHom (n +' m) (Ring→AbGroup R) A
+⌣[,,]-syntax n m R x y = x ⌣ y
+
+⌣[,,]C-syntax : {A : Type ℓ} (n m : ℕ) (R : CommRing ℓ')
+  → coHom n (CommRing→AbGroup R) A
+  → coHom m (CommRing→AbGroup R) A
+  → coHom (n +' m) (CommRing→AbGroup R) A
+⌣[,,]C-syntax n m R x y = x ⌣ y
+
+syntax ⌣[]-syntax R x y = x ⌣[ R ] y
+syntax ⌣[]C-syntax R x y = x ⌣[ R ]C y
+syntax ⌣[,,]-syntax n m R x y = x ⌣[ R , n , m ] y
+syntax ⌣[,,]C-syntax n m R x y = x ⌣[ R , n , m ]C y
+
+-- Commutativity in ℤ/2 coeffs
+comm⌣ℤ/2 : {A : Type ℓ'} (n m : ℕ)
+  → (x : coHom n ℤ/2 A)
+     (y : coHom m ℤ/2 A)
+  → x ⌣[ ℤ/2Ring ] y
+   ≡ subst (λ n → coHom n ℤ/2 A) (+'-comm m n)
+           (y ⌣[ ℤ/2Ring ] x)
+comm⌣ℤ/2 {A = A} n m x y = comm⌣ {G'' = ℤ/2CommRing} n m x y
+                 ∙ cong (subst (λ n₁ → coHom n₁ ℤ/2 A) (+'-comm m n))
+                        (lem x y)
+  where
+  lem : (x : coHom n ℤ/2 A) (y : coHom m ℤ/2 A)
+     → -ₕ^[ n · m ] (y ⌣[ ℤ/2Ring ] x) ≡ (y ⌣ x)
+  lem = ST.elim2 (λ _ _ → isSetPathImplicit)
+          λ _ _ → cong ∣_∣₂ (funExt λ _ → -ₖ^[ n · m ]-const _)
+
 module _ {G'' : Ring ℓ} {A : Type ℓ'} where
   private
     G' = Ring→AbGroup G''
@@ -110,3 +199,13 @@ module _ {G'' : Ring ℓ} {A : Type ℓ'} where
     → PathP (λ i → coHom (+'-assoc n m l (~ i)) G' A) ((x ⌣ y) ⌣ z) (x ⌣ (y ⌣ z))
   assoc⌣Dep n m l x y z = toPathP {A = λ i → coHom (+'-assoc n m l (~ i)) G' A}
                                   (flipTransport (assoc⌣ n m l x y z))
+
+module _ {G'' : CommRing ℓ} {A : Type ℓ'} where
+  private
+    G' = CommRing→AbGroup G''
+  comm⌣Dep : (n m : ℕ)  (x : coHom n G' A) (y : coHom m G' A)
+    → PathP (λ i → coHom (+'-comm m n (~ i)) G' A)
+             (x ⌣ y) (-ₕ^[ n · m ] (y ⌣ x))
+  comm⌣Dep n m x y =
+    toPathP {A = λ i → coHom (+'-comm m n (~ i)) G' A}
+      (flipTransport (comm⌣ n m x y))
diff --git a/Cubical/Data/Nat/Properties.agda b/Cubical/Data/Nat/Properties.agda
@@ -327,3 +327,13 @@ module PlusBis where
   +'-suc zero (suc m) = refl
   +'-suc (suc n) zero = refl
   +'-suc (suc n) (suc m) = refl
+
+-- Neat transport lemma for ℕ
+compSubstℕ : ∀ {ℓ} {A : ℕ → Type ℓ} {n m l : ℕ}
+   (p : n ≡ m) (q : m ≡ l) (r : n ≡ l)
+   → {x : _}
+   → subst A q (subst A p x)
+   ≡ subst A r x
+compSubstℕ {A = A} p q r {x = x} =
+  sym (substComposite A p q x)
+  ∙ λ i → subst A (isSetℕ _ _ (p ∙ q) r i) x
diff --git a/Cubical/Data/Sigma/Properties.agda b/Cubical/Data/Sigma/Properties.agda
@@ -152,7 +152,7 @@ module _ {A : Type ℓ} {A' : Type ℓ'} where
   unquoteDecl Σ-swap-≃ = declStrictIsoToEquiv Σ-swap-≃ Σ-swap-Iso
 
 module _ {A : Type ℓ} {B : A → Type ℓ'} {C : ∀ a → B a → Type ℓ''} where
-  Σ-assoc-Iso : Iso (Σ[ (a , b) ∈ Σ A B ] C a b) (Σ[ a ∈ A ] Σ[ b ∈ B a ] C a b)
+  Σ-assoc-Iso : Iso (Σ[ a ∈ Σ A B ] C (fst a) (snd a)) (Σ[ a ∈ A ] Σ[ b ∈ B a ] C a b)
   fun Σ-assoc-Iso ((x , y) , z) = (x , (y , z))
   inv Σ-assoc-Iso (x , (y , z)) = ((x , y) , z)
   rightInv Σ-assoc-Iso _ = refl

diff --git a/Cubical/Homotopy/EilenbergMacLane/Base.agda b/Cubical/Homotopy/EilenbergMacLane/Base.agda
@@ -139,3 +139,12 @@ EM-raw'-trivElim G zero {A = A} prop x embase-raw = x
 EM-raw'-trivElim G zero {A = A} prop x (emloop-raw g i) =
   isProp→PathP {B = λ i → A (emloop-raw g i)} (λ _ → prop _) x x i
 EM-raw'-trivElim G (suc n) {A = A} = raw-elim G (suc n)
+
+EM→Prop : (G : AbGroup ℓ) (n : ℕ) {A : EM G (suc n) → Type ℓ'}
+  → ((x : _) → isProp (A x) )
+  → A (0ₖ (suc n))
+  → (x : _) → A x
+EM→Prop G zero {A = A} p h = elimProp (AbGroup→Group G) p h
+EM→Prop G (suc n) {A = A} p h =
+  Trunc.elim (λ _ → isProp→isOfHLevelSuc (suc (suc (suc n))) (p _))
+    (suspToPropElim ptEM-raw (λ _ → p _) h)
diff --git a/Cubical/Homotopy/EilenbergMacLane/CupProduct.agda b/Cubical/Homotopy/EilenbergMacLane/CupProduct.agda
@@ -7,6 +7,8 @@ open import Cubical.Homotopy.EilenbergMacLane.GroupStructure
 open import Cubical.Homotopy.EilenbergMacLane.Properties
 open import Cubical.Homotopy.EilenbergMacLane.CupProductTensor
   renaming (_⌣ₖ_ to _⌣ₖ⊗_ ; ⌣ₖ-0ₖ to ⌣ₖ-0ₖ⊗ ; 0ₖ-⌣ₖ to 0ₖ-⌣ₖ⊗)
+open import Cubical.Homotopy.EilenbergMacLane.GradedCommTensor
+  renaming (⌣ₖ-comm to ⌣ₖ⊗-comm)
 
 open import Cubical.Algebra.AbGroup.TensorProduct
 open import Cubical.Algebra.Group.MorphismProperties
@@ -28,6 +30,7 @@ open import Cubical.Data.Nat hiding (_·_) renaming (elim to ℕelim ; _+_ to _+
 open import Cubical.Data.Sigma
 
 open import Cubical.Algebra.Ring
+open import Cubical.Algebra.CommRing
 
 open AbGroupStr renaming (_+_ to _+Gr_ ; -_ to -Gr_)
 open RingStr
@@ -139,3 +142,63 @@ module _ {G'' : Ring ℓ} where
                         ∙ sym (·DistR+ (snd G'') a
                               (fst TensorMultHom b) (fst TensorMultHom c)))
               λ x y ind ind2 → cong₂ _+G_ ind ind2))
+
+-- graded commutativity
+module _ {G'' : CommRing ℓ} where
+  private
+    G' = CommRing→AbGroup G''
+    G = fst G'
+    _+G_ = _+Gr_ (snd G')
+
+  ⌣ₖ-comm : (n m : ℕ) (x : EM G' n) (y : EM G' m)
+           → x ⌣ₖ y ≡ subst (EM G') (+'-comm m n) (-ₖ^[ n · m ] (y ⌣ₖ x))
+  ⌣ₖ-comm n m x y =
+      cong (EMTensorMult (n +' m)) (⌣ₖ⊗-comm n m x y)
+    ∙ sym (substCommSlice (EM (G' ⨂ G')) (EM G')
+            EMTensorMult (+'-comm m n)
+            (-ₖ^[ n · m ] (comm⨂-EM (m +' n) (y ⌣ₖ⊗ x))))
+    ∙ cong (subst (EM G') (+'-comm m n))
+        (-ₖ^< n · m >-Induced (m +' n) (evenOrOdd n) (evenOrOdd m) _ _
+      ∙ cong (-ₖ^[ n · m ])
+        (sym (inducedFun-EM-comp
+         (GroupEquiv→GroupHom ⨂-comm) TensorMultHom (m +' n) _)
+      ∙ λ i → inducedFun-EM (isTrivComm i) (m +' n) (y ⌣ₖ⊗ x)))
+
+    where
+    isTrivComm : compGroupHom (GroupEquiv→GroupHom ⨂-comm)
+                  (TensorMultHom {G' = CommRing→Ring G''})
+               ≡ TensorMultHom
+    isTrivComm =
+      Σ≡Prop (λ _ → isPropIsGroupHom _ _)
+        (funExt (⊗elimProp (λ _ → CommRingStr.is-set (snd G'') _ _)
+          (λ a b → CommRingStr.·Comm (snd G'') b a)
+          λ p q r s → cong₂ _+G_ r s))
+
+⌣[]ₖ-syntax : ∀ {ℓ} {n m : ℕ} (R : Ring ℓ)
+  → EM (Ring→AbGroup R) n
+  → EM (Ring→AbGroup R) m
+  → EM (Ring→AbGroup R) (n +' m)
+⌣[]ₖ-syntax R x y = x ⌣ₖ y
+
+⌣[]Cₖ-syntax : ∀ {ℓ} {n m : ℕ} (R : CommRing ℓ)
+  → EM (Ring→AbGroup (CommRing→Ring R)) n
+  → EM (Ring→AbGroup (CommRing→Ring R)) m
+  → EM (Ring→AbGroup (CommRing→Ring R)) (n +' m)
+⌣[]Cₖ-syntax R x y = x ⌣ₖ y
+
+⌣[,,]ₖ-syntax : ∀ {ℓ} (n m : ℕ) (R : Ring ℓ)
+  → EM (Ring→AbGroup R) n
+  → EM (Ring→AbGroup R) m
+  → EM (Ring→AbGroup R) (n +' m)
+⌣[,,]ₖ-syntax n m R x y = x ⌣ₖ y
+
+⌣[,,]Cₖ-syntax : ∀ {ℓ} (n m : ℕ) (R : CommRing ℓ)
+  → EM (Ring→AbGroup (CommRing→Ring R)) n
+  → EM (Ring→AbGroup (CommRing→Ring R)) m
+  → EM (Ring→AbGroup (CommRing→Ring R)) (n +' m)
+⌣[,,]Cₖ-syntax n m R x y = x ⌣ₖ y
+
+syntax ⌣[]ₖ-syntax R x y = x ⌣[ R ]ₖ y
+syntax ⌣[]Cₖ-syntax R x y = x ⌣[ R ]Cₖ y
+syntax ⌣[,,]ₖ-syntax n m R x y = x ⌣[ R , n , m ]ₖ y
+syntax ⌣[,,]Cₖ-syntax n m R x y = x ⌣[ R , n , m ]Cₖ y
diff --git a/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda b/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda
@@ -241,8 +241,16 @@ module _ {G' : AbGroup ℓ} {H' : AbGroup ℓ'} where
        trElim (λ _ → isOfHLevel↑∙ (2 + n) m)
          λ { north → (λ _ → 0ₖ (3 + (n + m))) , refl
            ; south → (λ _ → 0ₖ (3 + (n + m))) , refl
-           ; (merid a i) → Iso.inv (ΩfunExtIso _ _)
-                             (EM→ΩEM+1∙ _ ∘∙ ind (suc m) (EM-raw→EM _ _ a)) i}
+           ; (merid a i) →
+             (λ x → EM→ΩEM+1 (2 + (n + m)) (ind (suc m) (EM-raw→EM _ _ a) .fst x) i)
+                  , λ j → pp a j i}
+        where
+        pp : (a : _)
+          → EM→ΩEM+1 (suc (suc (n + m)))
+              (ind (suc m) (EM-raw→EM G' (suc n) a) .fst (snd (EM∙ H' (suc m))))
+          ≡ refl
+        pp a = cong (EM→ΩEM+1 (suc (suc (n + m)))) (ind (suc m) (EM-raw→EM G' (suc n) a) .snd)
+             ∙ EM→ΩEM+1-0ₖ _
 
    _⌣ₖ_ : {n m : ℕ} (x : EM G' n) (y : EM H' m) → EM (G' ⨂ H') (n +' m)
    _⌣ₖ_ x y = cup∙ _ _ x .fst y