The monoid of isomorphism classes under the binary biproduct

For an essentially small category C with zero morphisms, a zero object and binary biproducts, the small type TauCeti.ObjectCode C of codes for the isomorphism classes of objects carries an additive commutative monoid structure: the sum of two classes is the class of the biproduct of representatives, and the neutral element is the class of the zero object.

Representatives are chosen internally to define addition, through Function.surjInv TauCeti.objectCode_surjective, but they never escape: TauCeti.objectCode_biprod computes the sum on the codes of actual objects, and the monoid laws are transported from biprod.associator, biprod.braiding and the two zero-summand isomorphisms of Mathlib.

Main definitions

• the AddCommMonoid (TauCeti.ObjectCode C) instance.

Main results

• TauCeti.objectCode_biprod and TauCeti.objectCode_zero: the code of a binary biproduct is the sum of the codes, and the code of the zero object is the neutral element.

References

• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Section 5, where the monoid of isomorphism classes of objects under the biproduct is the starting point of the group-completion description of split K₀.

@[instance_reducible]

noncomputable instance TauCeti.instAddObjectCode {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : Add (ObjectCode C)

Isomorphism classes of objects are added by taking the binary biproduct of representatives.

Equations

• TauCeti.instAddObjectCode = { add := fun (c d : TauCeti.ObjectCode C) => TauCeti.objectCode (Function.surjInv ⋯ c ⊞ Function.surjInv ⋯ d) }

@[instance_reducible]

noncomputable instance TauCeti.instZeroObjectCode {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : Zero (ObjectCode C)

The class of the zero object is the neutral isomorphism class.

Equations

• TauCeti.instZeroObjectCode = { zero := TauCeti.objectCode 0 }

@[simp]

theorem TauCeti.objectCode_biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (X Y : C) : objectCode (X ⊞ Y) = objectCode X + objectCode Y

The code of a binary biproduct is the sum of the object codes.

@[simp]

theorem TauCeti.objectCode_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : objectCode 0 = 0

The code of the zero object is the neutral isomorphism class.

@[instance_reducible]

noncomputable instance TauCeti.instAddCommMonoidObjectCode {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : AddCommMonoid (ObjectCode C)

The isomorphism classes of an essentially small category with zero morphisms, a zero object and binary biproducts form an additive commutative monoid under the binary biproduct.

Equations

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