marcinjangrzybowski
diff --git a/‎.github/workflows/ci-ubuntu.yml‎
Lines changed: 15 additions & 22 deletions b/‎.github/workflows/ci-ubuntu.yml‎
Lines changed: 15 additions & 22 deletions
diff --git a/‎CITATION.cff‎
Lines changed: 2 additions & 2 deletions b/‎CITATION.cff‎
Lines changed: 2 additions & 2 deletions
diff --git a/‎Cubical/Algebra/AbGroup/Instances/FreeAbGroup.agda‎
Lines changed: 47 additions & 0 deletions b/‎Cubical/Algebra/AbGroup/Instances/FreeAbGroup.agda‎
Lines changed: 47 additions & 0 deletions
diff --git a/‎Cubical/Algebra/Algebra/Properties.agda‎
Lines changed: 1 addition & 1 deletion b/‎Cubical/Algebra/Algebra/Properties.agda‎
Lines changed: 1 addition & 1 deletion
diff --git a/‎Cubical/Algebra/ChainComplex/Homology.agda‎
Lines changed: 15 additions & 27 deletions b/‎Cubical/Algebra/ChainComplex/Homology.agda‎
Lines changed: 15 additions & 27 deletions
diff --git a/‎Cubical/Algebra/CommMonoid/Properties.agda‎
Lines changed: 16 additions & 0 deletions b/‎Cubical/Algebra/CommMonoid/Properties.agda‎
Lines changed: 16 additions & 0 deletions
diff --git a/‎Cubical/Algebra/CommRing/Localisation/UniversalProperty.agda‎
Lines changed: 4 additions & 6 deletions b/‎Cubical/Algebra/CommRing/Localisation/UniversalProperty.agda‎
Lines changed: 4 additions & 6 deletions
diff --git a/‎Cubical/Algebra/DistLattice/Downset.agda‎
Lines changed: 1 addition & 0 deletions b/‎Cubical/Algebra/DistLattice/Downset.agda‎
Lines changed: 1 addition & 0 deletions
diff --git a/‎Cubical/Algebra/Group/Exact.agda‎
Lines changed: 27 additions & 3 deletions b/‎Cubical/Algebra/Group/Exact.agda‎
Lines changed: 27 additions & 3 deletions
@@ -42,9 +42,9 @@ on:
 ########################################################################
 
 env:
-  AGDA_BRANCH: v2.6.4.1
-  GHC_VERSION: 9.4.7
-  CABAL_VERSION: 3.6.2.0
+  AGDA_BRANCH: v2.7.0.1
+  GHC_VERSION: 9.10.2
+  CABAL_VERSION: 3.12.1.0
   CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS'
   CACHE_PATHS: |
     ~/.cabal/packages
@@ -67,7 +67,7 @@ jobs:
       # absolutely necessary i.e. if we change either the version of Agda,
       # ghc, or cabal that we want to use for the build.
       - name: Restore external dependencies cache
-        uses: actions/cache/restore@v3
+        uses: actions/cache/restore@v4
         id: cache-external-restore
         with:
           path: ${{ env.CACHE_PATHS }}
@@ -82,23 +82,13 @@ jobs:
         run: |
           git clone https://github.com/agda/agda --branch ${{ env.AGDA_BRANCH }} --depth=1
           cd agda
-          mkdir -p doc
-          touch doc/user-manual.pdf
           ${{ env.CABAL_INSTALL }}
           cd ..
           rm -rf agda
 
-      - name: Download and install fix-whitespace
-        if: steps.cache-external-restore.outputs.cache-hit != 'true'
-        run: |
-          git clone https://github.com/agda/fix-whitespace --depth=1
-          cd fix-whitespace
-          ${{ env.CABAL_INSTALL }} fix-whitespace.cabal
-          cd ..
-
       - name: Save external dependencies cache
         if: steps.cache-external-restore.outputs.cache-hit != 'true'
-        uses: actions/cache/save@v3
+        uses: actions/cache/save@v4
         id: cache-external-save
         with:
           path: ${{ env.CACHE_PATHS }}
@@ -110,34 +100,37 @@ jobs:
 
       # By default github actions do not pull the repo
       - name: Checkout cubical
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
+
+      - name: Get and run fix-whitespace
+        uses: andreasabel/fix-whitespace-action@v1
 
       ########################################################################
       ## TESTING
       ########################################################################
 
       - name: Restore library cache
-        uses: actions/cache/restore@v3
+        uses: actions/cache/restore@v4
         id: cache-library-restore
         with:
           path: ./_build
           key: library-${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-${{ env.AGDA_BRANCH }}-${{ hashFiles('Cubical/**', 'cubical.agda-lib', 'Everythings.hs') }}
           restore-keys: |
             library-${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-${{ env.AGDA_BRANCH }}-
 
-      - name: Put cabal programs in PATH
+      - name: Put installed programs in PATH
         run: echo "~/.cabal/bin" >> "${GITHUB_PATH}"
 
       - name: Test cubical
         run: |
           make test \
             AGDA_EXEC='~/.cabal/bin/agda -WnoUnsupportedIndexedMatch -W error' \
-            FIX_WHITESPACE='~/.cabal/bin/fix-whitespace' \
+            FIX_WHITESPACE='~/.local/fix-whitespace/bin/fix-whitespace' \
             EVERYTHINGS='cabal run Everythings'
 
       - name: Save library cache
         if: steps.cache-library-restore.outputs.cache-hit != 'true'
-        uses: actions/cache/save@v3
+        uses: actions/cache/save@v4
         id: cache-library-save
         with:
           path: ./_build
@@ -152,12 +145,12 @@ jobs:
         run: |
           make listings \
             AGDA_EXEC='~/.cabal/bin/agda -WnoUnsupportedIndexedMatch -W error' \
-            FIX_WHITESPACE='~/.cabal/bin/fix-whitespace' \
+            FIX_WHITESPACE='~/.local/fix-whitespace/bin/fix-whitespace' \
             EVERYTHINGS='cabal run Everythings'
 
       - name: Deploy to GitHub Pages
         if: github.event_name == 'push' && github.ref_name == 'master'
-        uses: JamesIves/github-pages-deploy-action@4.1.8
+        uses: JamesIves/github-pages-deploy-action@v4
         with:
           branch: gh-pages
           folder: html
@@ -3,6 +3,6 @@ message: "If you use this software, please cite it as below."
 authors:
 - name: "The Agda Community"
 title: "Cubical Agda Library"
-version: 0.7
-date-released: 2024-02-12
+version: 0.8
+date-released: 2025-05-09
 url: "https://github.com/agda/cubical"
@@ -19,6 +19,7 @@ open import Cubical.HITs.FreeAbGroup
 open import Cubical.Algebra.AbGroup
 open import Cubical.Algebra.AbGroup.Instances.Pi
 open import Cubical.Algebra.AbGroup.Instances.Int
+open import Cubical.Algebra.AbGroup.Instances.DirectProduct
 open import Cubical.Algebra.Group
 open import Cubical.Algebra.Group.Morphisms
 open import Cubical.Algebra.Group.MorphismProperties
@@ -413,3 +414,49 @@ agreeOnℤFinGenerator→≡ {n} {m} {ϕ} {ψ} idr =
       λ f p → IsGroupHom.presinv (snd ϕ) f
            ∙∙ (λ i x → -ℤ (p i x))
            ∙∙ sym (IsGroupHom.presinv (snd ψ) f)))
+
+--
+sumCoefficients : (n : ℕ) → AbGroupHom (ℤ[Fin n ]) (ℤ[Fin 1 ])
+fst (sumCoefficients n) v = λ _ → sumFinℤ v
+snd (sumCoefficients n) = makeIsGroupHom (λ x y → funExt λ _ → sumFinℤHom x y)
+
+ℤFinProductIso : (n m : ℕ) → Iso (ℤ[Fin (n +ℕ m) ] .fst) ((AbDirProd ℤ[Fin n ] ℤ[Fin m ]) .fst)
+ℤFinProductIso n m = iso sum→product product→sum product→sum→product sum→product→sum
+  where
+    sum→product : (ℤ[Fin (n +ℕ m) ] .fst) → ((AbDirProd ℤ[Fin n ] ℤ[Fin m ]) .fst)
+    sum→product x = ((λ (a , Ha) → x (a , <→<ᵗ (≤-trans (<ᵗ→< Ha) (≤SumLeft {n}{m}))))
+                    , λ (a , Ha) → x (n +ℕ a , <→<ᵗ (<-k+ {a}{m}{n} (<ᵗ→< Ha))))
+
+    product→sum : ((AbDirProd ℤ[Fin n ] ℤ[Fin m ]) .fst) → (ℤ[Fin (n +ℕ m) ] .fst)
+    product→sum (x , y) (a , Ha) with (a ≟ᵗ n)
+    ... | lt H = x (a , H)
+    ... | eq H = y (a ∸ n , <→<ᵗ (subst (a ∸ n <_) (∸+ m n) (<-∸-< a (n +ℕ m) n (<ᵗ→< Ha) (subst (λ a → a < n +ℕ m) H (<ᵗ→< Ha)))))
+    ... | gt H = y (a ∸ n , <→<ᵗ (subst (a ∸ n <_) (∸+ m n) (<-∸-< a (n +ℕ m) n (<ᵗ→< Ha) (<ᵗ→< (<ᵗ-trans {n}{a}{n +ℕ m} H Ha)))))
+
+    product→sum→product : ∀ x → sum→product (product→sum x) ≡ x
+    product→sum→product (x , y) = ≡-× (funExt (λ (a , Ha) → lemx a Ha)) (funExt (λ (a , Ha) → lemy a Ha))
+      where
+        lemx : (a : ℕ) (Ha : a <ᵗ n) → fst (sum→product (product→sum (x , y))) (a , Ha) ≡ x (a , Ha)
+        lemx a Ha with (a ≟ᵗ n)
+        ... | lt H = cong x (Fin≡ (a , H) (a , Ha) refl)
+        ... | eq H = rec (¬m<ᵗm (subst (λ a → a <ᵗ n) H Ha))
+        ... | gt H = rec (¬m<ᵗm (<ᵗ-trans Ha H))
+
+        lemy : (a : ℕ) (Ha : a <ᵗ m) → snd (sum→product (product→sum (x , y))) (a , Ha) ≡ y (a , Ha)
+        lemy a Ha with ((n +ℕ a) ≟ᵗ n)
+        ... | lt H = rec (¬m<m (≤<-trans (≤SumLeft {n}{a}) (<ᵗ→< H)))
+        ... | eq H = cong y (Fin≡ _ _ (∸+ a n))
+        ... | gt H = cong y (Fin≡ _ _ (∸+ a n))
+
+    sum→product→sum : ∀ x → product→sum (sum→product x) ≡ x
+    sum→product→sum x = funExt (λ (a , Ha) → lem a Ha)
+      where
+        lem : (a : ℕ) (Ha : a <ᵗ (n +ℕ m)) → product→sum (sum→product x) (a , Ha) ≡ x (a , Ha)
+        lem a Ha with (a ≟ᵗ n)
+        ... | lt H = cong x (Fin≡ _ _ refl)
+        ... | eq H = cong x (Fin≡ _ _ ((+-comm n (a ∸ n)) ∙ ≤-∸-+-cancel (subst (n ≤_) (sym H) ≤-refl)))
+        ... | gt H = cong x (Fin≡ _ _ ((+-comm n (a ∸ n)) ∙ ≤-∸-+-cancel (<-weaken (<ᵗ→< H))))
+
+ℤFinProduct : (n m : ℕ) → AbGroupIso ℤ[Fin (n +ℕ m) ] (AbDirProd ℤ[Fin n ] ℤ[Fin m ])
+fst (ℤFinProduct n m) = ℤFinProductIso n m
+snd (ℤFinProduct n m) = makeIsGroupHom (λ x y → refl)
@@ -110,7 +110,7 @@ module AlgebraEquivs where
     (invAlgebraEquiv {A = A} {B = B} f').snd = hom
       where
         open AlgebraStr {{...}}
-        private instance
+        instance
           _ = snd A
           _ = snd B
 
 
@@ -35,42 +35,30 @@ open ChainComplex
 open finChainComplexMap
 open IsGroupHom
 
--- Definition of homology
-homology : (n : ℕ) → ChainComplex ℓ → Group ℓ
-homology n C = ker∂n / img∂+1⊂ker∂n
-  where
-  Cn+2 = AbGroup→Group (chain C (suc (suc n)))
-  ∂n = bdry C n
-  ∂n+1 = bdry C (suc n)
-  ker∂n = kerGroup ∂n
-
-  -- Restrict ∂n+1 to ker∂n
-  ∂'-fun : Cn+2 .fst → ker∂n .fst
-  fst (∂'-fun x) = ∂n+1 .fst x
-  snd (∂'-fun x) = t
-    where
-    opaque
-     t : ⟨ fst (kerSubgroup ∂n) (∂n+1 .fst x) ⟩
-     t = funExt⁻ (cong fst (bdry²=0 C n)) x
+module _ (n : ℕ) (C : ChainComplex ℓ) where
+  ker∂n = kerGroup (bdry C n)
 
-  ∂' : GroupHom Cn+2 ker∂n
-  fst ∂' = ∂'-fun
-  snd ∂' = isHom
+  ∂ker : GroupHom (AbGroup→Group (chain C (suc (suc n)))) ker∂n
+  ∂ker .fst x = (bdry C (suc n) .fst x) , t
     where
     opaque
-      isHom : IsGroupHom (Cn+2 .snd) ∂'-fun (ker∂n .snd)
-      isHom = makeIsGroupHom λ x y
-        → kerGroup≡ ∂n (∂n+1 .snd .pres· x y)
+     t : ⟨ fst (kerSubgroup (bdry C n)) (bdry C (suc n) .fst x) ⟩
+     t = funExt⁻ (cong fst (bdry²=0 C n)) x
+  ∂ker .snd = makeIsGroupHom (λ x y → kerGroup≡ (bdry C n) ((bdry C (suc n) .snd .pres· x y)))
 
   img∂+1⊂ker∂n : NormalSubgroup ker∂n
-  fst img∂+1⊂ker∂n = imSubgroup ∂'
+  fst img∂+1⊂ker∂n = imSubgroup ∂ker
   snd img∂+1⊂ker∂n = isNormalImSubGroup
     where
     opaque
       module C1 = AbGroupStr (chain C (suc n)  .snd)
-      isNormalImSubGroup : isNormal (imSubgroup ∂')
-      isNormalImSubGroup = isNormalIm ∂'
-        (λ x y → kerGroup≡ ∂n (C1.+Comm (fst x) (fst y)))
+      isNormalImSubGroup : isNormal (imSubgroup ∂ker)
+      isNormalImSubGroup = isNormalIm ∂ker
+        (λ x y → kerGroup≡ (bdry C n) (C1.+Comm (fst x) (fst y)))
+
+-- Definition of homology
+homology : (n : ℕ) → ChainComplex ℓ → Group ℓ
+homology n C = (ker∂n n C) / (img∂+1⊂ker∂n n C)
 
 -- Induced maps on cohomology by finite chain complex maps/homotopies
 module _ where
 
@@ -57,3 +57,19 @@ module CommMonoidTheory (M' : CommMonoid ℓ) where
  commAssocSwap : (x y z w : M) → (x · y) · (z · w) ≡ (x · z) · (y · w)
  commAssocSwap x y z w = ·Assoc (x · y) z w ∙∙ cong (_· w) (commAssocr x y z)
                                                ∙∙ sym (·Assoc (x · z) y w)
+
+ hasInverse : (x : M) → Type ℓ
+ hasInverse x = Σ[ -x ∈ M ] -x · x ≡ ε
+
+ isPropHasInverse : ∀ x → isProp (hasInverse x)
+ isPropHasInverse x yinv zinv
+   = Σ≡Prop (λ a → is-set (a · x) ε)
+    (PathPΣ (MonoidTheory.isPropHasInverse (CommMonoid→Monoid M') x
+                                           (hasInverseToMonoid x yinv)
+                                           (hasInverseToMonoid x zinv))
+                                               .fst)
+   where
+     hasInverseToMonoid : ∀ x
+                        → hasInverse x
+                        → MonoidTheory.hasInverse (CommMonoid→Monoid M') x
+     hasInverseToMonoid x (y , yinv) = y , yinv , ·Comm x y ∙ yinv
@@ -373,12 +373,10 @@ module _ (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultClos
                                       ; ·IdR to ·A-rid)
   open Units A' renaming (Rˣ to Aˣ ; RˣInvClosed to AˣInvClosed)
   open PathToS⁻¹R ⦃...⦄
-  private
-   A = fst A'
-   instance
-    _ = cond
-   χ = (S⁻¹RHasUniversalProp A' φ φS⊆Aˣ .fst .fst)
-   open RingHomTheory χ
+  A = fst A'
+  instance _ = cond
+  χ = (S⁻¹RHasUniversalProp A' φ φS⊆Aˣ .fst .fst)
+  open RingHomTheory χ
 
   S⁻¹R≃A : S⁻¹R ≃ A
   S⁻¹R≃A = fst χ , isEmbedding×isSurjection→isEquiv (Embχ , Surχ)
 
@@ -16,6 +16,7 @@ open import Cubical.Algebra.Lattice
 open import Cubical.Algebra.DistLattice.Base
 
 open import Cubical.Relation.Binary.Order.Poset
+open import Cubical.Relation.Binary.Order.Poset.Subset
 
 open Iso
 
 
@@ -1,11 +1,22 @@
 {-# OPTIONS --safe #-}
+
 module Cubical.Algebra.Group.Exact where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Function
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.HLevels
 
+open import Cubical.Data.Empty
+open import Cubical.Data.Fin
+open import Cubical.Data.Nat
+open import Cubical.Data.Nat.Order
+open import Cubical.Data.Sigma
+open import Cubical.Data.Sum
 open import Cubical.Data.Unit
+open import Cubical.Data.Vec
 
 open import Cubical.Algebra.Group.Base
 open import Cubical.Algebra.Group.Morphisms
@@ -15,11 +26,23 @@ open import Cubical.Algebra.Group.Instances.Unit
 
 open import Cubical.HITs.PropositionalTruncation as PT
 
+private
+  variable
+    ℓ ℓ' : Level
+
+record IsExactAt {ℓ ℓ' ℓ'' : Level}
+                 {A : Group ℓ} {B : Group ℓ'} {C : Group ℓ''}
+                 (f : GroupHom A B) (g : GroupHom B C) (b : ⟨ B ⟩)
+                 : Type (ℓ-max ℓ (ℓ-max ℓ' ℓ'')) where
+  field
+    im∈ker : isInIm f b → isInKer g b
+    ker∈im : isInKer g b → isInIm f b
+open IsExactAt public
 
--- TODO : Define exact sequences
--- (perhaps short, finite, ℕ-indexed and ℤ-indexed)
+IsExact : {A B C : Group ℓ} (f : GroupHom A B) (g : GroupHom B C) → Type ℓ
+IsExact {B = B} f g = (b : ⟨ B ⟩) → IsExactAt f g b
 
-SES→isEquiv : ∀ {ℓ ℓ'} {L R : Group ℓ-zero}
+SES→isEquiv : {L R : Group ℓ-zero}
   → {G : Group ℓ} {H : Group ℓ'}
   → UnitGroup₀ ≡ L
   → UnitGroup₀ ≡ R
@@ -138,3 +161,4 @@ transportExact4 {G = G} {G₂ = G₂} {H = H} {H₂ = H₂} {L = L} {L₂ = L₂
       (J (λ z q → (r : x₃ ≡ w) (s : x₄ ≡ u) → B x z w u refl q r s)
         (J (λ w r → (s : x₄ ≡ u) → B x x₂ w u refl refl r s)
           (J (λ u s → B x x₂ x₃ u refl refl refl s) b)))
+