The small presentation of a categorical Grothendieck group

Every categorical Grothendieck group -- split, exact, abelian, or triangulated -- is the quotient of a free abelian group on the isomorphism classes of objects by a family of additive relations. Only the relations differ. This file builds that common engine once, for an essentially small category C, so that each Grothendieck group can be obtained by naming its relations.

The generators are TauCeti.ObjectCode C, a genuinely small type of codes for the isomorphism classes of objects: it is Shrink (Skeleton C). The smallness hypotheses are Prop-valued, so ObjectCode C takes no data argument and depends only on C and the target universe. Its underlying small model and representatives are nevertheless arbitrary choices. Consequently, the object-facing API -- of, induction_on, hom_ext, AdditiveInvariant, liftEquiv, and map -- is stated purely in terms of objects of C, so callers need not manipulate representatives.

Main definitions

• TauCeti.ObjectCode C: a small type of codes for the isomorphism classes of objects of an essentially small category C, with TauCeti.objectCode the code of an object.
• TauCeti.freeOf X: the generator of FreeAbelianGroup (ObjectCode C) attached to X, and TauCeti.freeLift f: the additive homomorphism out of that free abelian group determined by a function f on objects.
• TauCeti.freeMap F: the map on the free abelian groups induced by a functor F; functoriality of presentations requires it to carry each chosen source relation into the subgroup generated by the target relations.
• TauCeti.PresentedK0 rels: the quotient of FreeAbelianGroup (ObjectCode C) by the additive subgroup generated by rels, with class map TauCeti.PresentedK0.of.
• TauCeti.PresentedK0.AdditiveInvariant rels G: an isomorphism-invariant function on objects whose free extension annihilates every chosen relation.
• TauCeti.PresentedK0.lift, TauCeti.PresentedK0.ofLE, TauCeti.PresentedK0.map and TauCeti.PresentedK0.mapEquiv: the induced homomorphism of an additive invariant, the comparison map to a presentation with more relations, functoriality, and equivalence invariance.

Main results

• TauCeti.PresentedK0.induction_on and TauCeti.PresentedK0.hom_ext: the induction principle and the extensionality principle, both phrased in terms of objects of C.
• TauCeti.PresentedK0.liftEquiv: the universal property. Additive invariants for rels correspond bijectively to additive homomorphisms out of PresentedK0 rels.

Implementation notes

TauCeti.freeLift f is defined for an arbitrary f : C → G, by evaluating f at a chosen representative of each code. Isomorphism invariance of f is not needed to define it; it is needed exactly to compute it on the classes TauCeti.freeOf X, and so appears as a hypothesis of TauCeti.freeLift_freeOf rather than as an unused argument of the definition. The bundled form TauCeti.PresentedK0.AdditiveInvariant carries that hypothesis together with the relations.

Relations are packaged as a Set (FreeAbelianGroup (ObjectCode C)) rather than as an AddSubgroup, and the quotient is taken by AddSubgroup.closure. The universal property then has a hypothesis about the chosen generating relations only, which is what a caller can check.

References

• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Section 6, where K₀ of a small abelian category is presented by generators and relations and the set-theoretic care taken here is discussed, and Section 6.1.2 for the universal property of an additive invariant.
• Mathlib/GroupTheory/PresentedGroup.lean and Mathlib/Algebra/PresentedMonoid/Basic.lean, whose set-of-relations parameter and mk/of/closure_range_of/lift-and-uniqueness/extensionality/map API layout are adapted here to additive categorical presentations. The object-facing class map, AdditiveInvariant, and the comparison map ofLE are specific to the categorical construction.

@[reducible, inline]

abbrev TauCeti.ObjectCode (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : Type w

ObjectCode C is a small type of codes for the isomorphism classes of objects of an essentially small category C.

Equations

• TauCeti.ObjectCode C = Shrink.{?u.3, ?u.1} (CategoryTheory.Skeleton C)

noncomputable def TauCeti.objectCode {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (X : C) : ObjectCode C

The code of an object of C. Two objects have the same code exactly when they are isomorphic; see TauCeti.objectCode_eq_objectCode_iff.

Equations

• TauCeti.objectCode X = (equivShrink (CategoryTheory.Skeleton C)) (CategoryTheory.toSkeleton X)

theorem TauCeti.objectCode_eq_objectCode_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {X Y : C} : objectCode X = objectCode Y ↔ Nonempty (X ≅ Y)

theorem TauCeti.objectCode_congr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {X Y : C} (e : X ≅ Y) : objectCode X = objectCode Y

theorem TauCeti.objectCode_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : Function.Surjective objectCode

noncomputable def TauCeti.freeOf {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (X : C) : FreeAbelianGroup (ObjectCode C)

The generator of the free abelian group on object codes attached to an object X.

Equations

• TauCeti.freeOf X = FreeAbelianGroup.of (TauCeti.objectCode X)

theorem TauCeti.freeOf_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (X : C) : freeOf X = FreeAbelianGroup.of (objectCode X)

The object generator is the free generator on its object code.

theorem TauCeti.freeOf_congr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {X Y : C} (e : X ≅ Y) : freeOf X = freeOf Y

theorem TauCeti.freeOf_eq_freeOf_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {X Y : C} : freeOf X = freeOf Y ↔ Nonempty (X ≅ Y)

noncomputable def TauCeti.freeLift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] (f : C → G) : FreeAbelianGroup (ObjectCode C) →+ G

The additive homomorphism out of the free abelian group on object codes determined by a function on objects, obtained by evaluating at a chosen representative of each code. It computes as expected on the classes TauCeti.freeOf X as soon as the function is invariant under isomorphism; see TauCeti.freeLift_freeOf.

Equations

• TauCeti.freeLift f = FreeAbelianGroup.lift fun (c : TauCeti.ObjectCode C) => f (TauCeti.objectCodeOut✝ c)

theorem TauCeti.freeLift_freeOf {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] {f : C → G} (hf : ∀ ⦃X Y : C⦄ (a : X ≅ Y), f X = f Y) (X : C) : (freeLift f) (freeOf X) = f X

theorem TauCeti.freeLift_unique {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] {f : C → G} (g : FreeAbelianGroup (ObjectCode C) →+ G) (hg : ∀ (X : C), g (freeOf X) = f X) : g = freeLift f

theorem TauCeti.freeLift_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] {H : Type u_2} [AddCommGroup H] (φ : G →+ H) (f : C → G) : (freeLift fun (X : C) => φ (f X)) = φ.comp (freeLift f)

def TauCeti.PresentedK0 {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (rels : Set (FreeAbelianGroup (ObjectCode C))) : Type w

The Grothendieck group of C presented by the family of relations rels: the free abelian group on the isomorphism classes of objects of C, modulo the additive subgroup generated by rels.

Equations

• TauCeti.PresentedK0 rels = (FreeAbelianGroup (TauCeti.ObjectCode C) ⧸ AddSubgroup.closure rels)

@[instance_reducible]

instance TauCeti.instAddCommGroupPresentedK0 {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (rels : Set (FreeAbelianGroup (ObjectCode C))) : AddCommGroup (PresentedK0 rels)

Equations

• One or more equations did not get rendered due to their size.

structure TauCeti.PresentedK0.AdditiveInvariant {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (rels : Set (FreeAbelianGroup (ObjectCode C))) (G : Type u_1) [AddCommGroup G] : Type (max u u_1)

An additive invariant for the presentation rels: a function on objects of C, invariant under isomorphism, whose free extension annihilates every chosen relation. These are exactly the data that factor through TauCeti.PresentedK0 rels; see TauCeti.PresentedK0.liftEquiv.

• obj : C → G

  The value of the invariant on an object.

• map_iso ⦃X Y : C⦄ : ∀ (a : X ≅ Y), self.obj X = self.obj Y

  Isomorphic objects receive equal values.

• map_rel (r : FreeAbelianGroup (ObjectCode C)) : r ∈ rels → (freeLift self.obj) r = 0

  The free extension of the invariant annihilates every chosen relation.

theorem TauCeti.PresentedK0.AdditiveInvariant.ext_iff {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.EssentiallySmall.{w, v, u} C} {rels : Set (FreeAbelianGroup (ObjectCode C))} {G : Type u_1} {inst✝² : AddCommGroup G} {x y : AdditiveInvariant rels G} : x = y ↔ x.obj = y.obj

theorem TauCeti.PresentedK0.AdditiveInvariant.ext {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.EssentiallySmall.{w, v, u} C} {rels : Set (FreeAbelianGroup (ObjectCode C))} {G : Type u_1} {inst✝² : AddCommGroup G} {x y : AdditiveInvariant rels G} (obj : x.obj = y.obj) : x = y

def TauCeti.PresentedK0.mk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {rels : Set (FreeAbelianGroup (ObjectCode C))} : FreeAbelianGroup (ObjectCode C) →+ PresentedK0 rels

The quotient map presenting TauCeti.PresentedK0 rels.

Equations

• TauCeti.PresentedK0.mk = QuotientAddGroup.mk' (AddSubgroup.closure rels)

theorem TauCeti.PresentedK0.mk_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {rels : Set (FreeAbelianGroup (ObjectCode C))} : Function.Surjective ⇑mk

theorem TauCeti.PresentedK0.mk_eq_zero_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {rels : Set (FreeAbelianGroup (ObjectCode C))} (r : FreeAbelianGroup (ObjectCode C)) : mk r = 0 ↔ r ∈ AddSubgroup.closure rels

theorem TauCeti.PresentedK0.mk_eq_zero_of_mem {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {rels : Set (FreeAbelianGroup (ObjectCode C))} {r : FreeAbelianGroup (ObjectCode C)} (hr : r ∈ rels) : mk r = 0

noncomputable def TauCeti.PresentedK0.of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {rels : Set (FreeAbelianGroup (ObjectCode C))} (X : C) : PresentedK0 rels

The class of an object of C in the presented Grothendieck group.

Equations

• TauCeti.PresentedK0.of X = TauCeti.PresentedK0.mk (TauCeti.freeOf X)

@[simp]

theorem TauCeti.PresentedK0.mk_freeOf {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {rels : Set (FreeAbelianGroup (ObjectCode C))} (X : C) : mk (freeOf X) = of X

theorem TauCeti.PresentedK0.of_congr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {rels : Set (FreeAbelianGroup (ObjectCode C))} {X Y : C} (e : X ≅ Y) : of X = of Y

theorem TauCeti.PresentedK0.closure_range_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {rels : Set (FreeAbelianGroup (ObjectCode C))} : AddSubgroup.closure (Set.range of) = ⊤

The image of PresentedK0.of generates the whole additive group.

theorem TauCeti.PresentedK0.induction_on {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {rels : Set (FreeAbelianGroup (ObjectCode C))} {motive : PresentedK0 rels → Prop} (x : PresentedK0 rels) (zero : motive 0) (of : ∀ (X : C), motive (of X)) (add : ∀ (a b : PresentedK0 rels), motive a → motive b → motive (a + b)) (neg : ∀ (a : PresentedK0 rels), motive a → motive (-a)) : motive x

Induction on the classes of objects of C: no skeleton representative is ever mentioned.

theorem TauCeti.PresentedK0.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {rels : Set (FreeAbelianGroup (ObjectCode C))} {G : Type u_1} [AddMonoid G] {f g : PresentedK0 rels →+ G} (h : ∀ (X : C), f (of X) = g (of X)) : f = g

Two homomorphisms out of a presented Grothendieck group agreeing on the classes of objects of C are equal.

theorem TauCeti.PresentedK0.hom_ext_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {rels : Set (FreeAbelianGroup (ObjectCode C))} {G : Type u_1} [AddMonoid G] {f g : PresentedK0 rels →+ G} : f = g ↔ ∀ (X : C), f (of X) = g (of X)

theorem TauCeti.PresentedK0.surjective_of_forall_of_mem_range {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {rels : Set (FreeAbelianGroup (ObjectCode C))} {G : Type u_1} [AddGroup G] {f : G →+ PresentedK0 rels} (h : ∀ (X : C), of X ∈ f.range) : Function.Surjective ⇑f

A homomorphism into a presented Grothendieck group whose range contains the class of every object of C is surjective, since those classes generate.

noncomputable def TauCeti.PresentedK0.lift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {rels : Set (FreeAbelianGroup (ObjectCode C))} {G : Type u_1} [AddCommGroup G] (a : AdditiveInvariant rels G) : PresentedK0 rels →+ G

The additive homomorphism induced by an additive invariant.

Equations

• TauCeti.PresentedK0.lift a = QuotientAddGroup.lift (AddSubgroup.closure rels) (TauCeti.freeLift a.obj) ⋯

@[simp]

theorem TauCeti.PresentedK0.lift_mk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {rels : Set (FreeAbelianGroup (ObjectCode C))} {G : Type u_1} [AddCommGroup G] (a : AdditiveInvariant rels G) (r : FreeAbelianGroup (ObjectCode C)) : (lift a) (mk r) = (freeLift a.obj) r

@[simp]

theorem TauCeti.PresentedK0.lift_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {rels : Set (FreeAbelianGroup (ObjectCode C))} {G : Type u_1} [AddCommGroup G] (a : AdditiveInvariant rels G) (X : C) : (lift a) (of X) = a.obj X

theorem TauCeti.PresentedK0.lift_unique {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {rels : Set (FreeAbelianGroup (ObjectCode C))} {G : Type u_1} [AddCommGroup G] (a : AdditiveInvariant rels G) (f : PresentedK0 rels →+ G) (hf : ∀ (X : C), f (of X) = a.obj X) : f = lift a

noncomputable def TauCeti.PresentedK0.liftEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {rels : Set (FreeAbelianGroup (ObjectCode C))} {G : Type u_1} [AddCommGroup G] : AdditiveInvariant rels G ≃ (PresentedK0 rels →+ G)

The universal property of a presented Grothendieck group: additive invariants for rels with values in G correspond bijectively to additive homomorphisms PresentedK0 rels →+ G.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.PresentedK0.liftEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {rels : Set (FreeAbelianGroup (ObjectCode C))} {G : Type u_1} [AddCommGroup G] (a : AdditiveInvariant rels G) : liftEquiv a = lift a

@[simp]

theorem TauCeti.PresentedK0.liftEquiv_symm_apply_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {rels : Set (FreeAbelianGroup (ObjectCode C))} {G : Type u_1} [AddCommGroup G] (f : PresentedK0 rels →+ G) (X : C) : (liftEquiv.symm f).obj X = f (of X)

noncomputable def TauCeti.freeMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (F : CategoryTheory.Functor C D) : FreeAbelianGroup (ObjectCode C) →+ FreeAbelianGroup (ObjectCode D)

The additive homomorphism on free abelian groups on object codes induced by a functor.

Equations

• TauCeti.freeMap F = TauCeti.freeLift fun (X : C) => TauCeti.freeOf (F.obj X)

@[simp]

theorem TauCeti.freeMap_freeOf {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (F : CategoryTheory.Functor C D) (X : C) : (freeMap F) (freeOf X) = freeOf (F.obj X)

@[simp]

theorem TauCeti.freeMap_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : freeMap (CategoryTheory.Functor.id C) = AddMonoidHom.id (FreeAbelianGroup (ObjectCode C))

theorem TauCeti.freeMap_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E : Type u''} [CategoryTheory.Category.{v'', u''} E] [CategoryTheory.EssentiallySmall.{w'', v'', u''} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) : freeMap (F.comp G) = (freeMap G).comp (freeMap F)

theorem TauCeti.freeMap_congr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {F G : CategoryTheory.Functor C D} (h : ∀ (X : C), Nonempty (F.obj X ≅ G.obj X)) : freeMap F = freeMap G

theorem TauCeti.freeMap_id_mapsTo {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {relsC : Set (FreeAbelianGroup (ObjectCode C))} (r : FreeAbelianGroup (ObjectCode C)) : r ∈ relsC → (freeMap (CategoryTheory.Functor.id C)) r ∈ AddSubgroup.closure relsC

The free map of the identity functor preserves every generated relation subgroup.

theorem TauCeti.freeMap_comp_mapsTo {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {relsC : Set (FreeAbelianGroup (ObjectCode C))} {relsD : Set (FreeAbelianGroup (ObjectCode D))} {E : Type u''} [CategoryTheory.Category.{v'', u''} E] [CategoryTheory.EssentiallySmall.{w'', v'', u''} E] {relsE : Set (FreeAbelianGroup (ObjectCode E))} (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (hF : ∀ r ∈ relsC, (freeMap F) r ∈ AddSubgroup.closure relsD) (hG : ∀ r ∈ relsD, (freeMap G) r ∈ AddSubgroup.closure relsE) (r : FreeAbelianGroup (ObjectCode C)) : r ∈ relsC → (freeMap (F.comp G)) r ∈ AddSubgroup.closure relsE

A composite free map preserves generated relation subgroups when each of its factors does.

noncomputable def TauCeti.PresentedK0.map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {relsC : Set (FreeAbelianGroup (ObjectCode C))} {relsD : Set (FreeAbelianGroup (ObjectCode D))} (F : CategoryTheory.Functor C D) (h : ∀ r ∈ relsC, (freeMap F) r ∈ AddSubgroup.closure relsD) : PresentedK0 relsC →+ PresentedK0 relsD

Functoriality: a functor whose induced map on free abelian groups sends every chosen relation of relsC into the subgroup generated by relsD induces a homomorphism of presented Grothendieck groups.

Equations

• TauCeti.PresentedK0.map F h = QuotientAddGroup.map (AddSubgroup.closure relsC) (AddSubgroup.closure relsD) (TauCeti.freeMap F) ⋯

@[simp]

theorem TauCeti.PresentedK0.map_mk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {relsC : Set (FreeAbelianGroup (ObjectCode C))} {relsD : Set (FreeAbelianGroup (ObjectCode D))} (F : CategoryTheory.Functor C D) (h : ∀ r ∈ relsC, (freeMap F) r ∈ AddSubgroup.closure relsD) (r : FreeAbelianGroup (ObjectCode C)) : (map F h) (mk r) = mk ((freeMap F) r)

@[simp]

theorem TauCeti.PresentedK0.map_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {relsC : Set (FreeAbelianGroup (ObjectCode C))} {relsD : Set (FreeAbelianGroup (ObjectCode D))} (F : CategoryTheory.Functor C D) (h : ∀ r ∈ relsC, (freeMap F) r ∈ AddSubgroup.closure relsD) (X : C) : (map F h) (of X) = of (F.obj X)

noncomputable def TauCeti.PresentedK0.ofLE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {rels rels' : Set (FreeAbelianGroup (ObjectCode C))} (h : rels ⊆ ↑(AddSubgroup.closure rels')) : PresentedK0 rels →+ PresentedK0 rels'

The comparison map to a presentation with more relations: enlarging the family of relations factors the class map. Taking rels to be the split relations and rels' the conflations of an exact structure, this is the canonical comparison from split to exact K₀.

Equations

• TauCeti.PresentedK0.ofLE h = TauCeti.PresentedK0.map (CategoryTheory.Functor.id C) ⋯

@[simp]

theorem TauCeti.PresentedK0.ofLE_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {rels rels' : Set (FreeAbelianGroup (ObjectCode C))} (h : rels ⊆ ↑(AddSubgroup.closure rels')) (X : C) : (ofLE h) (of X) = of X

@[simp]

theorem TauCeti.PresentedK0.ofLE_mk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {rels rels' : Set (FreeAbelianGroup (ObjectCode C))} (h : rels ⊆ ↑(AddSubgroup.closure rels')) (r : FreeAbelianGroup (ObjectCode C)) : (ofLE h) (mk r) = mk r

@[simp]

theorem TauCeti.PresentedK0.map_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {relsC : Set (FreeAbelianGroup (ObjectCode C))} (hId : ∀ r ∈ relsC, (freeMap (CategoryTheory.Functor.id C)) r ∈ AddSubgroup.closure relsC := ⋯) : map (CategoryTheory.Functor.id C) hId = AddMonoidHom.id (PresentedK0 relsC)

theorem TauCeti.PresentedK0.map_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {relsC : Set (FreeAbelianGroup (ObjectCode C))} {relsD : Set (FreeAbelianGroup (ObjectCode D))} {E : Type u''} [CategoryTheory.Category.{v'', u''} E] [CategoryTheory.EssentiallySmall.{w'', v'', u''} E] {relsE : Set (FreeAbelianGroup (ObjectCode E))} (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (hF : ∀ r ∈ relsC, (freeMap F) r ∈ AddSubgroup.closure relsD) (hG : ∀ r ∈ relsD, (freeMap G) r ∈ AddSubgroup.closure relsE) (hFG : ∀ r ∈ relsC, (freeMap (F.comp G)) r ∈ AddSubgroup.closure relsE := ⋯) : map (F.comp G) hFG = (map G hG).comp (map F hF)

@[simp]

theorem TauCeti.PresentedK0.ofLE_refl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {relsC : Set (FreeAbelianGroup (ObjectCode C))} : ofLE ⋯ = AddMonoidHom.id (PresentedK0 relsC)

Enlarging a relation family to itself induces the identity map.

theorem TauCeti.PresentedK0.ofLE_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {rels rels' rels'' : Set (FreeAbelianGroup (ObjectCode C))} (h : rels ⊆ ↑(AddSubgroup.closure rels')) (h' : rels' ⊆ ↑(AddSubgroup.closure rels'')) : (ofLE h').comp (ofLE h) = ofLE ⋯

Comparison maps for successive enlargements of relation families compose.

theorem TauCeti.PresentedK0.map_congr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {relsC : Set (FreeAbelianGroup (ObjectCode C))} {relsD : Set (FreeAbelianGroup (ObjectCode D))} {F G : CategoryTheory.Functor C D} (h : ∀ (X : C), Nonempty (F.obj X ≅ G.obj X)) (hF : ∀ r ∈ relsC, (freeMap F) r ∈ AddSubgroup.closure relsD) (hG : ∀ r ∈ relsC, (freeMap G) r ∈ AddSubgroup.closure relsD) : map F hF = map G hG

noncomputable def TauCeti.PresentedK0.mapEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {relsC : Set (FreeAbelianGroup (ObjectCode C))} {relsD : Set (FreeAbelianGroup (ObjectCode D))} (e : C ≌ D) (h : ∀ r ∈ relsC, (freeMap e.functor) r ∈ AddSubgroup.closure relsD) (h' : ∀ r ∈ relsD, (freeMap e.inverse) r ∈ AddSubgroup.closure relsC) : PresentedK0 relsC ≃+ PresentedK0 relsD

Equivalence invariance: an equivalence carrying the chosen relations into one another in both directions induces an isomorphism of presented Grothendieck groups.

Equations

• TauCeti.PresentedK0.mapEquiv e h h' = { toFun := ⇑(TauCeti.PresentedK0.map e.functor h), invFun := ⇑(TauCeti.PresentedK0.map e.inverse h'), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.PresentedK0.mapEquiv_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {relsC : Set (FreeAbelianGroup (ObjectCode C))} {relsD : Set (FreeAbelianGroup (ObjectCode D))} (e : C ≌ D) (h : ∀ r ∈ relsC, (freeMap e.functor) r ∈ AddSubgroup.closure relsD) (h' : ∀ r ∈ relsD, (freeMap e.inverse) r ∈ AddSubgroup.closure relsC) (X : C) : (mapEquiv e h h') (of X) = of (e.functor.obj X)

@[simp]

theorem TauCeti.PresentedK0.mapEquiv_symm_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {relsC : Set (FreeAbelianGroup (ObjectCode C))} {relsD : Set (FreeAbelianGroup (ObjectCode D))} (e : C ≌ D) (h : ∀ r ∈ relsC, (freeMap e.functor) r ∈ AddSubgroup.closure relsD) (h' : ∀ r ∈ relsD, (freeMap e.inverse) r ∈ AddSubgroup.closure relsC) (Y : D) : (mapEquiv e h h').symm (of Y) = of (e.inverse.obj Y)

@[simp]

theorem TauCeti.PresentedK0.mapEquiv_toAddMonoidHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {relsC : Set (FreeAbelianGroup (ObjectCode C))} {relsD : Set (FreeAbelianGroup (ObjectCode D))} (e : C ≌ D) (h : ∀ r ∈ relsC, (freeMap e.functor) r ∈ AddSubgroup.closure relsD) (h' : ∀ r ∈ relsD, (freeMap e.inverse) r ∈ AddSubgroup.closure relsC) : ↑(mapEquiv e h h') = map e.functor h

The additive homomorphism underlying equivalence invariance is the functorial map.

@[simp]

theorem TauCeti.PresentedK0.mapEquiv_refl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {relsC : Set (FreeAbelianGroup (ObjectCode C))} (h : ∀ r ∈ relsC, (freeMap CategoryTheory.Equivalence.refl.functor) r ∈ AddSubgroup.closure relsC := by simpa only [CategoryTheory.Equivalence.refl_functor] using (freeMap_id_mapsTo (relsC := relsC))) (h' : ∀ r ∈ relsC, (freeMap CategoryTheory.Equivalence.refl.inverse) r ∈ AddSubgroup.closure relsC := by simpa only [CategoryTheory.Equivalence.refl_inverse] using (freeMap_id_mapsTo (relsC := relsC))) : mapEquiv CategoryTheory.Equivalence.refl h h' = AddEquiv.refl (PresentedK0 relsC)

Equivalence invariance for the identity equivalence is the identity.

theorem TauCeti.PresentedK0.mapEquiv_trans {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {relsC : Set (FreeAbelianGroup (ObjectCode C))} {relsD : Set (FreeAbelianGroup (ObjectCode D))} {E : Type u''} [CategoryTheory.Category.{v'', u''} E] [CategoryTheory.EssentiallySmall.{w'', v'', u''} E] {relsE : Set (FreeAbelianGroup (ObjectCode E))} (e : C ≌ D) (f : D ≌ E) (h : ∀ r ∈ relsC, (freeMap e.functor) r ∈ AddSubgroup.closure relsD) (h' : ∀ r ∈ relsD, (freeMap e.inverse) r ∈ AddSubgroup.closure relsC) (k : ∀ r ∈ relsD, (freeMap f.functor) r ∈ AddSubgroup.closure relsE) (k' : ∀ r ∈ relsE, (freeMap f.inverse) r ∈ AddSubgroup.closure relsD) (hk : ∀ r ∈ relsC, (freeMap (e.trans f).functor) r ∈ AddSubgroup.closure relsE := ⋯) (hk' : ∀ r ∈ relsE, (freeMap (e.trans f).inverse) r ∈ AddSubgroup.closure relsC := ⋯) : (mapEquiv e h h').trans (mapEquiv f k k') = mapEquiv (e.trans f) hk hk'

Equivalence invariance respects composition of equivalences.