public
Last active

Grothendieck group

  • Download Gist
Grothendieck.agda
Agda
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101
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′)
)

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.