Grothendieck group

Grothendieck.agda

module Grothendieck where

open import Level using (_⊔_)
open import Function
open import Algebra
open import Algebra.Structures
open import Data.Product
import Relation.Binary.EqReasoning as EqReasoning


Grothendieck : ∀ {c ℓ} → CommutativeMonoid c ℓ → AbelianGroup c (c ⊔ ℓ)
Grothendieck CM = record
  { Carrier = Carrier′
  ; _≈_ = _≈′_
  ; _∙_ = _∙′_
  ; ε = ε , ε
  ; _⁻¹ = _⁻¹′
  ; isAbelianGroup = record
    { isGroup = record
      { isMonoid = record
        { isSemigroup = record
          { isEquivalence = record
            { refl  = ε , left comm!
            ; sym   = λ { (k , equ) → k , left comm! ⇒ sym equ ⇒ left comm! }
            ; trans = trans′
            }
          ; assoc = λ _ _ _ → ε , left (comm! ⇒ ∙-cong (sym assoc!) assoc!)
          ; ∙-cong = ∙-cong′
          }
        ; identity = (λ _ → ε , left (assoc! ⇒ right comm! ⇒ sym assoc!)) , (λ _ → ε , left (comm! ⇒ right comm! ⇒ sym assoc!))
        }
      ; inverse = (λ _ → ε , left (left comm!)) , (λ _ → ε , left (left comm!))
      ; ⁻¹-cong = λ { (k , equ) → k , sym equ }
      }
    ; comm = λ _ _ → ε , left (comm! ⇒ ∙-cong comm! comm!)
    }
  }
  where
  open CommutativeMonoid CM

  open EqReasoning setoid

  infixr 5 _⇒_
  infix  2 _≈′_

  -- Opening the module and renaming trans to _⇒_ doesn't seem to let me adjust the fixity
  _⇒_ : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z
  _⇒_ = trans

  -- These make shuffling around boring equations less unpleasant
  comm! : ∀ {x y} → x ∙ y ≈ y ∙ x
  comm! = comm _ _

  assoc! : ∀ {x y z} → x ∙ y ∙ z ≈ x ∙ (y ∙ z)
  assoc! = assoc _ _ _

  left : ∀ {x y z} → x ≈ y → x ∙ z ≈ y ∙ z
  left equ = ∙-cong equ refl

  right : ∀ {x y z} → x ≈ y → z ∙ x ≈ z ∙ y
  right = ∙-cong refl

  Carrier′ : Set _
  Carrier′ = Carrier × Carrier

  _≈′_ : Carrier′ → Carrier′ → Set _
  (s , t) ≈′ (u , v) = ∃ (λ k → s ∙ v ∙ k ≈ t ∙ u ∙ k)

  _∙′_ : Carrier′ → Carrier′ → Carrier′
  (s , t) ∙′ (u , v) = s ∙ u , t ∙ v

  _⁻¹′ : Carrier′ → Carrier′
  (s , t) ⁻¹′ = t , s

  trans′ : ∀ {x y z} → x ≈′ y → y ≈′ z → x ≈′ z
  trans′ {x₁ , x₂} {y₁ , y₂} {z₁ , z₂} (k , equ) (k′ , equ′) = y₁ ∙ (k′ ∙ k) , (
    begin
      (x₁ ∙ z₂) ∙ (y₁ ∙ (k′ ∙ k))
    ≈⟨ assoc! ⇒ right (sym assoc! ⇒ left comm! ⇒ assoc! ⇒ right (sym assoc!) ⇒ sym assoc! ⇒ left (sym assoc!)) ⟩
      x₁ ∙ ((y₁ ∙ z₂ ∙ k′) ∙ k)
    ≈⟨ right (left equ′) ⟩
      x₁ ∙ ((y₂ ∙ z₁ ∙ k′) ∙ k)
    ≈⟨ right (assoc! ⇒ assoc! ⇒ right (right comm! ⇒ comm! ⇒ assoc!) ⇒ sym assoc!) ⇒ sym assoc! ⇒ left (sym assoc!) ⟩
      (x₁ ∙ y₂ ∙ k) ∙ (k′ ∙ z₁)
    ≈⟨ left equ ⟩
      ((x₂ ∙ y₁) ∙ k) ∙ (k′ ∙ z₁)
    ≈⟨ comm! ⇒ assoc! ⇒ right (sym assoc! ⇒ left (sym assoc! ⇒ left comm!) ⇒ assoc!) ⇒ comm! ⇒ assoc! ⇒ right (assoc! ⇒ right comm!) ⟩
      (x₂ ∙ z₁) ∙ (y₁ ∙ (k′ ∙ k))
    ∎)

  ∙-cong′ : ∀ {a b c d} → a ≈′ b → c ≈′ d → a ∙′ c ≈′ b ∙′ d
  ∙-cong′ {a₁ , a₂} {b₁ , b₂} {c₁ , c₂} {d₁ , d₂} (k , equ) (k′ , equ′) = k ∙ k′ , (
    begin
      a₁ ∙ c₁ ∙ (b₂ ∙ d₂) ∙ (k ∙ k′)
    ≈⟨ sym assoc! ⇒ left (assoc! ⇒ assoc! ⇒ right (comm! ⇒ assoc! ⇒ assoc! ⇒ right (comm! ⇒ assoc!) ⇒ sym assoc!) ⇒ sym assoc! ⇒ left (sym assoc!)) ⇒ assoc! ⟩
      (a₁ ∙ b₂ ∙ k) ∙ (c₁ ∙ d₂ ∙ k′)
    ≈⟨ ∙-cong equ equ′ ⟩
      (a₂ ∙ b₁ ∙ k) ∙ (c₂ ∙ d₁ ∙ k′)
    ≈⟨ sym assoc! ⇒ left (assoc! ⇒ right comm! ⇒ sym assoc! ⇒ left (sym assoc! ⇒ left assoc! ⇒ assoc! ⇒ right (left comm! ⇒ assoc!) ⇒ sym assoc!)) ⇒ assoc! ⟩
      a₂ ∙ c₂ ∙ (b₁ ∙ d₁) ∙ (k ∙ k′)
    ∎)