{-# OPTIONS --without-K --rewriting #-}

open import HoTT
open import groups.KernelImage

module cohomology.ChainComplex where

  record ChainComplex i : Type (lsucc i) where
    field
      head : AbGroup i
      chain : ℕ → AbGroup i
      augment : AbGroup.grp (chain ) →ᴳ AbGroup.grp head
      boundary : ∀ n → (AbGroup.grp (chain (S n)) →ᴳ AbGroup.grp (chain n))

  record CochainComplex i : Type (lsucc i) where
    field
      head : AbGroup i
      cochain : ℕ → AbGroup i
      augment : AbGroup.grp head →ᴳ AbGroup.grp (cochain )
      coboundary : ∀ n → (AbGroup.grp (cochain n) →ᴳ AbGroup.grp (cochain (S n)))

  homology-group : ∀ {i} → ChainComplex i
    → (n : ℤ) → Group i
  homology-group cc (pos ) = Ker/Im cc.augment (cc.boundary ) (snd (cc.chain ))
    where module cc = ChainComplex cc
  homology-group cc (pos (S n)) = Ker/Im (cc.boundary n) (cc.boundary (S n)) (snd (cc.chain (S n)))
    where module cc = ChainComplex cc
  homology-group {i} cc (negsucc _) = Lift-group {j = i} Unit-group

  cohomology-group : ∀ {i} → CochainComplex i
    → (n : ℤ) → Group i
  cohomology-group cc (pos ) = Ker/Im (cc.coboundary ) cc.augment (snd (cc.cochain ))
    where module cc = CochainComplex cc
  cohomology-group cc (pos (S n)) = Ker/Im (cc.coboundary (S n)) (cc.coboundary n) (snd (cc.cochain (S n)))
    where module cc = CochainComplex cc
  cohomology-group {i} cc (negsucc _) = Lift-group {j = i} Unit-group

  complex-dualize : ∀ {i j} → ChainComplex i → AbGroup j
    →  CochainComplex (lmax i j)
  complex-dualize {i} {j} cc G = record {M} where
    module cc = ChainComplex cc
    module M where
      head : AbGroup (lmax i j)
      head = hom-abgroup (AbGroup.grp cc.head) G

      cochain : ℕ → AbGroup (lmax i j)
      cochain n = hom-abgroup (AbGroup.grp (cc.chain n)) G

      augment : AbGroup.grp head →ᴳ AbGroup.grp (cochain )
      augment = pre∘ᴳ-hom G cc.augment

      coboundary : ∀ n → (AbGroup.grp (cochain n) →ᴳ AbGroup.grp (cochain (S n)))
      coboundary n = pre∘ᴳ-hom G (cc.boundary n)