Instantly share code, notes, and snippets.

# copumpkin/Grothendieck.agda Last active Oct 12, 2015

Grothendieck group
 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′) ∎)