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.
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
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.
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
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.
Something wrong, better idea? Suggest a change
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.
K0Presentation.instAddCommGroupK0.{u, v} {Obj : Type u} {Rel : Type v} (P : K0Presentation Obj Rel) : AddCommGroup P.K0K0Presentation.instAddCommGroupK0.{u, v} {Obj : Type u} {Rel : Type v} (P : K0Presentation Obj Rel) : AddCommGroup P.K0
Something wrong, better idea? Suggest a change
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).
K0Presentation.of.{u, v} {Obj : Type u} {Rel : Type v} (P : K0Presentation Obj Rel) (X : Obj) : P.K0K0Presentation.of.{u, v} {Obj : Type u} {Rel : Type v} (P : K0Presentation Obj Rel) (X : Obj) : P.K0
Something wrong, better idea? Suggest a change
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.
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
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.
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) : PropK0Presentation.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}
Something wrong, better idea? Suggest a change
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.
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 →+ AK0Presentation.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
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.
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 XK0Presentation.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
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.
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 = gK0Presentation.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
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.
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 xK0Presentation.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
The class map P.\operatorname{of} is additive for its own presentation.
Proof: Immediate from the fundamental relation P.of_rel.
K0Presentation.isAdditive_of.{u, v} {Obj : Type u} {Rel : Type v} (P : K0Presentation Obj Rel) : P.IsAdditive P.ofK0Presentation.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
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.
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.K0K0Presentation.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
The induced map sends generators to generators: \operatorname{map}(f)([X]_P) = [f(X)]_Q.
Proof: Immediate from lift_of.
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
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.
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
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].
K0Presentation.map_id.{u, v} {Obj : Type u} {Rel : Type v} (P : K0Presentation Obj Rel) : P.map id ⋯ = AddMonoidHom.id P.K0K0Presentation.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
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))].
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