2.2. GrothendieckGroup: Defs🔗

2.2.1. K0Presentation🔗

A K_0-presentation is a purely algebraic specification of a Grothendieck-style group quotient. Given a type of objects \operatorname{Obj} and a type of relations \operatorname{Rel}, a presentation consists of three projections \operatorname{obj}_1, \operatorname{obj}_2, \operatorname{obj}_3 : \operatorname{Rel} \to \operatorname{Obj} encoding the pattern [\operatorname{obj}_2(r)] = [\operatorname{obj}_1(r)] + [\operatorname{obj}_3(r)]. This factors out the identical quotient plumbing shared by the triangulated K_0 (relations from distinguished triangles) and the heart K_0 (relations from short exact sequences).

Construction: A structure with three fields obj_1, obj_2, obj_3 : Rel \to Obj parameterized by universe-polymorphic types Obj and Rel.

structure

K0Presentation.{u, v} (Obj : Type u) (Rel : Type v) : Type (max u v)
K0Presentation.{u, v} (Obj : Type u)
  (Rel : Type v) : Type (max u v)

Constructor

K0Presentation.mk.{u, v}

Fields

obj₁ : Rel → Obj

The first term of the relation (e.g., T.obj₁ or S.X₁).

obj₂ : Rel → Obj

The middle term (the one that equals the sum of the other two).

obj₃ : Rel → Obj

The third term.

Something wrong, better idea? Suggest a change

2.2.2. subgroup🔗

The relation subgroup of a K_0-presentation P is the additive subgroup of \operatorname{FreeAbelianGroup}(\operatorname{Obj}) generated by the elements [\operatorname{obj}_2(r)] - [\operatorname{obj}_1(r)] - [\operatorname{obj}_3(r)] for each relation r.

Construction: Defined as the additive closure of the set \{\operatorname{of}(P.\operatorname{obj}_2\, r) - \operatorname{of}(P.\operatorname{obj}_1\, r) - \operatorname{of}(P.\operatorname{obj}_3\, r) \mid r : \operatorname{Rel}\} inside FreeAbelianGroup Obj.

def

K0Presentation.subgroup.{u, v} {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel) : AddSubgroup (FreeAbelianGroup Obj)
K0Presentation.subgroup.{u, v}
  {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel) :
  AddSubgroup (FreeAbelianGroup Obj)

Something wrong, better idea? Suggest a change

2.2.3. K0🔗

The Grothendieck group K_0(P) of a presentation P is the quotient \operatorname{FreeAbelianGroup}(\operatorname{Obj}) \,/\, P.\operatorname{subgroup}. This is the universal abelian group receiving a map from \operatorname{Obj} that respects the three-term relations.

Construction: An abbreviation for the quotient FreeAbelianGroup Obj / P.subgroup.

def

K0Presentation.K0.{u, v} {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel) : Type u
K0Presentation.K0.{u, v} {Obj : Type u}
  {Rel : Type v}
  (P : K0Presentation Obj Rel) : Type u

Something wrong, better idea? Suggest a change

2.2.4. instAddCommGroupK0🔗

The Grothendieck group K_0(P) of a K_0-presentation P carries an abelian group structure, inherited from the quotient of a free abelian group.

Construction: Derived by inferInstanceAs from the AddCommGroup instance on FreeAbelianGroup Obj ⧸ P.subgroup.

def

K0Presentation.instAddCommGroupK0.{u, v} {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel) : AddCommGroup P.K0
K0Presentation.instAddCommGroupK0.{u, v}
  {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel) :
  AddCommGroup P.K0

Something wrong, better idea? Suggest a change

2.2.5. of🔗

The class map [\cdot] : \operatorname{Obj} \to K_0(P) sends an object X to its equivalence class in the Grothendieck group.

Construction: Defined as QuotientAddGroup.mk (FreeAbelianGroup.of X).

def

K0Presentation.of.{u, v} {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel) (X : Obj) : P.K0
K0Presentation.of.{u, v} {Obj : Type u}
  {Rel : Type v}
  (P : K0Presentation Obj Rel) (X : Obj) :
  P.K0

Something wrong, better idea? Suggest a change

2.2.6. of_rel🔗

The fundamental relation: for each relation r, one has [\operatorname{obj}_2(r)] = [\operatorname{obj}_1(r)] + [\operatorname{obj}_3(r)] in K_0(P).

Proof: The difference \operatorname{of}(\operatorname{obj}_2) - \operatorname{of}(\operatorname{obj}_1) - \operatorname{of}(\operatorname{obj}_3) lies in the relation subgroup by definition of the closure, so the quotient identifies the two sides.

theorem

K0Presentation.of_rel.{u, v} {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel) (r : Rel) :
  P.of (P.obj₂ r) = P.of (P.obj₁ r) + P.of (P.obj₃ r)
K0Presentation.of_rel.{u, v}
  {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel) (r : Rel) :
  P.of (P.obj₂ r) =
    P.of (P.obj₁ r) + P.of (P.obj₃ r)

Something wrong, better idea? Suggest a change

2.2.7. IsAdditive🔗

A function f : \operatorname{Obj} \to A to an additive group is additive for a presentation P if f(\operatorname{obj}_2(r)) = f(\operatorname{obj}_1(r)) + f(\operatorname{obj}_3(r)) for every relation r.

Construction: A single-field Prop-valued class carrying the additivity hypothesis for each relation.

type class

K0Presentation.IsAdditive.{u, v, u_1} {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel) {A : Type u_1} [AddCommGroup A]
  (f : Obj → A) : Prop
K0Presentation.IsAdditive.{u, v, u_1}
  {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel)
  {A : Type u_1} [AddCommGroup A]
  (f : Obj → A) : Prop

Instance Constructor

K0Presentation.IsAdditive.mk.{u, v, u_1}

Methods

additive : ∀ (r : Rel), f (P.obj₂ r) = f (P.obj₁ r) + f (P.obj₃ r)

Something wrong, better idea? Suggest a change

2.2.8. lift🔗

The universal property of K_0: any additive function f : \operatorname{Obj} \to A lifts uniquely to a group homomorphism K_0(P) \to A.

Construction: Constructed via QuotientAddGroup.lift applied to FreeAbelianGroup.lift f, after verifying that the relation subgroup maps to zero using the additivity hypothesis.

def

K0Presentation.lift.{u, v, u_1} {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel) {A : Type u_1} [AddCommGroup A]
  (f : Obj → A) [P.IsAdditive f] : P.K0 →+ A
K0Presentation.lift.{u, v, u_1}
  {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel)
  {A : Type u_1} [AddCommGroup A]
  (f : Obj → A) [P.IsAdditive f] :
  P.K0 →+ A

Something wrong, better idea? Suggest a change

2.2.9. lift_of🔗

The lift of an additive function f agrees with f on generators: \operatorname{lift}(f)([X]) = f(X).

Proof: Immediate from FreeAbelianGroup.lift_apply_of.

theorem

K0Presentation.lift_of.{u, v, u_1} {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel) {A : Type u_1} [AddCommGroup A]
  (f : Obj → A) [P.IsAdditive f] (X : Obj) : (P.lift f) (P.of X) = f X
K0Presentation.lift_of.{u, v, u_1}
  {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel)
  {A : Type u_1} [AddCommGroup A]
  (f : Obj → A) [P.IsAdditive f]
  (X : Obj) : (P.lift f) (P.of X) = f X

Something wrong, better idea? Suggest a change

2.2.10. hom_ext🔗

Extensionality for K_0: two group homomorphisms f, g : K_0(P) \to A that agree on all generators [X] are equal.

Proof: By induction on the quotient and then on the free abelian group (generators, zero, negation, addition), reducing to the generator case.

theorem

K0Presentation.hom_ext.{u, v, u_1} {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel) {A : Type u_1} [AddCommGroup A]
  {f g : P.K0 →+ A} (h : ∀ (X : Obj), f (P.of X) = g (P.of X)) : f = g
K0Presentation.hom_ext.{u, v, u_1}
  {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel)
  {A : Type u_1} [AddCommGroup A]
  {f g : P.K0 →+ A}
  (h :
    ∀ (X : Obj),
      f (P.of X) = g (P.of X)) :
  f = g

Something wrong, better idea? Suggest a change

2.2.11. induction_on🔗

Induction principle for K_0(P): to prove a property of all elements of K_0(P), it suffices to check generators [X], zero, negation, and addition.

Proof: Combines QuotientAddGroup.induction_on with FreeAbelianGroup.induction_on.

theorem

K0Presentation.induction_on.{u, v} {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel) {motive : P.K0 → Prop} (x : P.K0)
  (of : ∀ (X : Obj), motive (P.of X)) (zero : motive 0)
  (neg : ∀ (a : P.K0), motive a → motive (-a))
  (add : ∀ (a b : P.K0), motive a → motive b → motive (a + b)) :
  motive x
K0Presentation.induction_on.{u, v}
  {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel)
  {motive : P.K0 → Prop} (x : P.K0)
  (of : ∀ (X : Obj), motive (P.of X))
  (zero : motive 0)
  (neg :
    ∀ (a : P.K0), motive a → motive (-a))
  (add :
    ∀ (a b : P.K0),
      motive a →
        motive b → motive (a + b)) :
  motive x

Something wrong, better idea? Suggest a change

2.2.12. isAdditive_of🔗

The class map P.\operatorname{of} is additive for its own presentation.

Proof: Immediate from the fundamental relation P.of_rel.

theorem

K0Presentation.isAdditive_of.{u, v} {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel) : P.IsAdditive P.of
K0Presentation.isAdditive_of.{u, v}
  {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel) :
  P.IsAdditive P.of

Something wrong, better idea? Suggest a change

2.2.13. map🔗

The induced map on Grothendieck groups from a function f : \operatorname{Obj} \to \operatorname{QObj} that respects relations. Given presentations P and Q and an additivity proof for Q.\operatorname{of} \circ f, this yields a group homomorphism K_0(P) \to K_0(Q).

Construction: Defined as P.lift (Q.of \circ f) using the supplied additivity instance.

def

K0Presentation.map.{u, v, u', v'} {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel) {QObj : Type u'} {QRel : Type v'}
  {Q : K0Presentation QObj QRel} (f : Obj → QObj)
  (hf : P.IsAdditive (Q.of ∘ f)) : P.K0 →+ Q.K0
K0Presentation.map.{u, v, u', v'}
  {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel)
  {QObj : Type u'} {QRel : Type v'}
  {Q : K0Presentation QObj QRel}
  (f : Obj → QObj)
  (hf : P.IsAdditive (Q.of ∘ f)) :
  P.K0 →+ Q.K0

Something wrong, better idea? Suggest a change

2.2.14. map_of🔗

The induced map sends generators to generators: \operatorname{map}(f)([X]_P) = [f(X)]_Q.

Proof: Immediate from lift_of.

theorem

K0Presentation.map_of.{u, v, u', v'} {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel) {QObj : Type u'} {QRel : Type v'}
  {Q : K0Presentation QObj QRel} (f : Obj → QObj)
  (hf : P.IsAdditive (Q.of ∘ f)) (X : Obj) :
  (P.map f hf) (P.of X) = Q.of (f X)
K0Presentation.map_of.{u, v, u', v'}
  {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel)
  {QObj : Type u'} {QRel : Type v'}
  {Q : K0Presentation QObj QRel}
  (f : Obj → QObj)
  (hf : P.IsAdditive (Q.of ∘ f))
  (X : Obj) :
  (P.map f hf) (P.of X) = Q.of (f X)

Something wrong, better idea? Suggest a change

2.2.15. of_relMap🔗

A compatible map on relations implies additivity of the induced object map. If f_{\operatorname{Obj}} : \operatorname{Obj} \to \operatorname{QObj} and f_{\operatorname{Rel}} : \operatorname{Rel} \to \operatorname{QRel} satisfy f_{\operatorname{Obj}}(P.\operatorname{obj}_i(r)) = Q.\operatorname{obj}_i(f_{\operatorname{Rel}}(r)) for i = 1, 2, 3, then Q.\operatorname{of} \circ f_{\operatorname{Obj}} is additive for P.

Proof: Rewrite using the compatibility hypotheses and apply Q.of_rel.

theorem

K0Presentation.IsAdditive.of_relMap.{u, v, u', v'} {Obj : Type u}
  {Rel : Type v} (P : K0Presentation Obj Rel) {QObj : Type u'}
  {QRel : Type v'} {Q : K0Presentation QObj QRel} (fObj : Obj → QObj)
  (fRel : Rel → QRel)
  (h₁ : ∀ (r : Rel), fObj (P.obj₁ r) = Q.obj₁ (fRel r))
  (h₂ : ∀ (r : Rel), fObj (P.obj₂ r) = Q.obj₂ (fRel r))
  (h₃ : ∀ (r : Rel), fObj (P.obj₃ r) = Q.obj₃ (fRel r)) :
  P.IsAdditive (Q.of ∘ fObj)
K0Presentation.IsAdditive.of_relMap.{u, v,
    u', v'}
  {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel)
  {QObj : Type u'} {QRel : Type v'}
  {Q : K0Presentation QObj QRel}
  (fObj : Obj → QObj) (fRel : Rel → QRel)
  (h₁ :
    ∀ (r : Rel),
      fObj (P.obj₁ r) = Q.obj₁ (fRel r))
  (h₂ :
    ∀ (r : Rel),
      fObj (P.obj₂ r) = Q.obj₂ (fRel r))
  (h₃ :
    ∀ (r : Rel),
      fObj (P.obj₃ r) = Q.obj₃ (fRel r)) :
  P.IsAdditive (Q.of ∘ fObj)

Something wrong, better idea? Suggest a change

2.2.16. map_id🔗

The identity map on objects induces the identity homomorphism on K_0.

Proof: By extensionality (hom_ext), checking on generators where both sides equal [X].

theorem

K0Presentation.map_id.{u, v} {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel) : P.map id ⋯ = AddMonoidHom.id P.K0
K0Presentation.map_id.{u, v}
  {Obj : Type u} {Rel : Type v}
  (P : K0Presentation Obj Rel) :
  P.map id ⋯ = AddMonoidHom.id P.K0

Something wrong, better idea? Suggest a change

2.2.17. map_comp🔗

Functoriality: the induced map of a composition g \circ f equals the composition of the induced maps.

Proof: By extensionality on generators, where both sides evaluate to [g(f(X))].

theorem

K0Presentation.map_comp.{u, v, u', v', u'', v''} {Obj : Type u}
  {Rel : Type v} {P : K0Presentation Obj Rel} {QObj : Type u'}
  {QRel : Type v'} {Q : K0Presentation QObj QRel} {RObj : Type u''}
  {RRel : Type v''} {R : K0Presentation RObj RRel} (f : Obj → QObj)
  (g : QObj → RObj) (hf : P.IsAdditive (Q.of ∘ f))
  (hg : Q.IsAdditive (R.of ∘ g)) (hgf : P.IsAdditive (R.of ∘ g ∘ f)) :
  P.map (g ∘ f) hgf = (Q.map g hg).comp (P.map f hf)
K0Presentation.map_comp.{u, v, u', v',
    u'', v''}
  {Obj : Type u} {Rel : Type v}
  {P : K0Presentation Obj Rel}
  {QObj : Type u'} {QRel : Type v'}
  {Q : K0Presentation QObj QRel}
  {RObj : Type u''} {RRel : Type v''}
  {R : K0Presentation RObj RRel}
  (f : Obj → QObj) (g : QObj → RObj)
  (hf : P.IsAdditive (Q.of ∘ f))
  (hg : Q.IsAdditive (R.of ∘ g))
  (hgf : P.IsAdditive (R.of ∘ g ∘ f)) :
  P.map (g ∘ f) hgf =
    (Q.map g hg).comp (P.map f hf)

Something wrong, better idea? Suggest a change