Split K₀ from biproduct relations

The split Grothendieck group TauCeti.SplitK0 C of an essentially small category C with zero morphisms and binary biproducts -- an additive category, in the intended application -- is the free abelian group on the isomorphism classes of objects modulo the biproduct relations [X ⊞ Y] = [X] + [Y]. It is the universal recipient of an invariant which is constant on isomorphism classes and additive on binary biproducts.

A short complex with a splitting is a conflation of every exact structure on C (TauCeti.ExactStructure.conflation_of_splitting), so the biproduct relations are imposed by every exact structure. The comparison homomorphism TauCeti.ExactK0.fromSplit sends each object class in split K₀ to its class in exact K₀.

The construction is the presentation engine of TauCeti/CategoryTheory/GrothendieckGroup/Presentation.lean applied to the biproduct relations, so smallness is handled once and for all there and the whole public API below is phrased in terms of objects of C.

The last section identifies SplitK0 C with Mathlib's group completion Algebra.GrothendieckAddGroup of the additive monoid of isomorphism classes under ⊞, built in TauCeti/CategoryTheory/GrothendieckGroup/ObjectCodeMonoid.lean. That monoid structure is carried by TauCeti.ObjectCode C itself, so the identification is an isomorphism of additive groups in the same small universe.

Main definitions

• TauCeti.splitRelation X Y: the relation [X ⊞ Y] - [X] - [Y], and TauCeti.splitRelations C the family of all of them.
• TauCeti.SplitK0 C: split K₀, with class map TauCeti.SplitK0.of.
• TauCeti.SplitK0.ofLE: the comparison to a presentation imposing more relations.
• TauCeti.SplitK0.AdditiveInvariant C G: an isomorphism-invariant, biproduct-additive function on objects, and TauCeti.SplitK0.lift the homomorphism it induces.
• TauCeti.SplitK0.map and TauCeti.SplitK0.mapEquiv: functoriality for functors preserving zero morphisms and binary biproducts, and invariance under equivalences.
• TauCeti.SplitK0.ofCode: the class map on the monoid of isomorphism classes of objects.

Main results

• TauCeti.SplitK0.of_biprod and TauCeti.SplitK0.of_eq_zero_of_isZero: the defining biproduct relation and its consequence for a zero object.
• TauCeti.SplitK0.exists_eq_sub: every split-K₀ class is a difference of two object classes.
• TauCeti.SplitK0.AdditiveInvariant.obj_biproduct and TauCeti.SplitK0.of_biproduct: additive invariants, and in particular the class map, are additive on finite biproducts.
• TauCeti.SplitK0.liftEquiv: the universal property. Biproduct-additive invariants with values in G correspond bijectively to homomorphisms SplitK0 C →+ G.
• TauCeti.SplitK0.grothendieckAddGroupEquiv: split K₀ is the group completion of the additive monoid of isomorphism classes of objects.

References

• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Section 5, where split K₀ of a symmetric monoidal category is constructed as the group completion of the monoid of isomorphism classes, and Section 6 for the presentation by generators and relations.
• Theo Bühler, Exact categories, Expositiones Mathematicae 28 (2010), 1–69, Section 13.1, for the split exact structure whose conflations impose exactly these relations.

noncomputable def TauCeti.splitRelation {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) : FreeAbelianGroup (ObjectCode C)

The biproduct relation [X ⊞ Y] - [X] - [Y] imposed in split K₀.

Equations

• TauCeti.splitRelation X Y = TauCeti.freeOf (X ⊞ Y) - TauCeti.freeOf X - TauCeti.freeOf Y

theorem TauCeti.splitRelation_def {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) : splitRelation X Y = freeOf (X ⊞ Y) - freeOf X - freeOf Y

The defining equation of TauCeti.splitRelation.

def TauCeti.splitRelations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : Set (FreeAbelianGroup (ObjectCode C))

The family of biproduct relations presenting split K₀.

Equations

• TauCeti.splitRelations C = {r : FreeAbelianGroup (TauCeti.ObjectCode C) | ∃ (X : C) (Y : C), r = TauCeti.splitRelation X Y}

@[simp]

theorem TauCeti.mem_splitRelations_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {r : FreeAbelianGroup (ObjectCode C)} : r ∈ splitRelations C ↔ ∃ (X : C) (Y : C), r = splitRelation X Y

Membership in the family of biproduct relations.

theorem TauCeti.splitRelation_mem_splitRelations {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) : splitRelation X Y ∈ splitRelations C

def TauCeti.SplitK0 (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : Type w

The split Grothendieck group of an essentially small category with zero morphisms and binary biproducts: the free abelian group on the isomorphism classes of objects, modulo [X ⊞ Y] = [X] + [Y].

Equations

• TauCeti.SplitK0 C = TauCeti.PresentedK0 (TauCeti.splitRelations C)

@[instance_reducible]

noncomputable instance TauCeti.instAddCommGroupSplitK0 (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : AddCommGroup (SplitK0 C)

Equations

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

noncomputable def TauCeti.SplitK0.of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (X : C) : SplitK0 C

The class of an object in split K₀.

Equations

• TauCeti.SplitK0.of X = TauCeti.PresentedK0.of X

theorem TauCeti.SplitK0.of_congr {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} (e : X ≅ Y) : of X = of Y

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

The comparison from split K₀ to a presentation imposing every split relation.

Equations

• TauCeti.SplitK0.ofLE h = TauCeti.PresentedK0.ofLE h

@[simp]

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

@[simp]

theorem TauCeti.SplitK0.of_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) : of (X ⊞ Y) = of X + of Y

The defining relation of split K₀: the class of a biproduct is the sum of the classes.

theorem TauCeti.SplitK0.of_eq_zero_of_isZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {X : C} (hX : CategoryTheory.Limits.IsZero X) : of X = 0

The class of an object which is zero vanishes.

@[simp]

theorem TauCeti.SplitK0.of_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] [CategoryTheory.Limits.HasZeroObject C] : of 0 = 0

The class of the zero object vanishes.

theorem TauCeti.SplitK0.closure_range_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : AddSubgroup.closure (Set.range of) = ⊤

The image of the class map generates split K₀.

theorem TauCeti.SplitK0.induction_on {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {motive : SplitK0 C → Prop} (x : SplitK0 C) (zero : motive 0) (of : ∀ (X : C), motive (of X)) (add : ∀ (a b : SplitK0 C), motive a → motive b → motive (a + b)) (neg : ∀ (a : SplitK0 C), motive a → motive (-a)) : motive x

Induction on the classes of objects of C.

theorem TauCeti.SplitK0.exists_eq_sub {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] [CategoryTheory.Limits.HasZeroObject C] (x : SplitK0 C) : ∃ (X : C) (Y : C), x = of X - of Y

Every element of split K₀ is a difference of the classes of two objects.

theorem TauCeti.SplitK0.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddMonoid G] {f g : SplitK0 C →+ G} (h : ∀ (X : C), f (of X) = g (of X)) : f = g

Two homomorphisms out of split K₀ agreeing on the classes of objects are equal.

theorem TauCeti.SplitK0.hom_ext_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddMonoid G] {f g : SplitK0 C →+ G} : f = g ↔ ∀ (X : C), f (of X) = g (of X)

theorem TauCeti.SplitK0.surjective_of_forall_of_mem_range {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddGroup G] {f : G →+ SplitK0 C} (h : ∀ (X : C), of X ∈ f.range) : Function.Surjective ⇑f

A homomorphism into split K₀ whose range contains the class of every object is surjective.

structure TauCeti.SplitK0.AdditiveInvariant (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] (G : Type u_2) [AddCommGroup G] : Type (max u u_2)

An additive invariant for split K₀: a function on objects of C, constant on isomorphism classes and additive on binary biproducts. These are exactly the data that factor through TauCeti.SplitK0 C; see TauCeti.SplitK0.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_biprod (X Y : C) : self.obj (X ⊞ Y) = self.obj X + self.obj Y

  The value on a biproduct is the sum of the values.

theorem TauCeti.SplitK0.AdditiveInvariant.ext {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Limits.HasZeroMorphisms C} {inst✝² : CategoryTheory.Limits.HasBinaryBiproducts C} {G : Type u_2} {inst✝³ : AddCommGroup G} {x y : AdditiveInvariant C G} (obj : x.obj = y.obj) : x = y

theorem TauCeti.SplitK0.AdditiveInvariant.ext_iff {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Limits.HasZeroMorphisms C} {inst✝² : CategoryTheory.Limits.HasBinaryBiproducts C} {G : Type u_2} {inst✝³ : AddCommGroup G} {x y : AdditiveInvariant C G} : x = y ↔ x.obj = y.obj

theorem TauCeti.SplitK0.AdditiveInvariant.obj_eq_zero_of_isZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {G : Type u_1} [AddCommGroup G] (a : AdditiveInvariant C G) {X : C} (hX : CategoryTheory.Limits.IsZero X) : a.obj X = 0

An additive invariant vanishes on zero objects.

noncomputable def TauCeti.SplitK0.lift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] (a : AdditiveInvariant C G) : SplitK0 C →+ G

The homomorphism out of split K₀ induced by a biproduct-additive invariant.

Equations

• TauCeti.SplitK0.lift a = TauCeti.PresentedK0.lift (TauCeti.SplitK0.AdditiveInvariant.toPresented✝ a)

@[simp]

theorem TauCeti.SplitK0.lift_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] (a : AdditiveInvariant C G) (X : C) : (lift a) (of X) = a.obj X

theorem TauCeti.SplitK0.lift_unique {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] (a : AdditiveInvariant C G) (f : SplitK0 C →+ G) (hf : ∀ (X : C), f (of X) = a.obj X) : f = lift a

Any homomorphism agreeing with an additive invariant on object classes is its induced lift.

noncomputable def TauCeti.SplitK0.liftEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] : AdditiveInvariant C G ≃ (SplitK0 C →+ G)

The universal property of split K₀: biproduct-additive invariants with values in G correspond bijectively to additive homomorphisms SplitK0 C →+ G.

Equations

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

@[simp]

theorem TauCeti.SplitK0.liftEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] (a : AdditiveInvariant C G) : liftEquiv a = lift a

@[simp]

theorem TauCeti.SplitK0.liftEquiv_symm_apply_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] (f : SplitK0 C →+ G) (X : C) : (liftEquiv.symm f).obj X = f (of X)

noncomputable def TauCeti.SplitK0.ofInvariant (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : AdditiveInvariant C (SplitK0 C)

The class map X ↦ [X], as a biproduct-additive invariant valued in split K₀ itself.

Equations

• TauCeti.SplitK0.ofInvariant C = { obj := TauCeti.SplitK0.of, map_iso := ⋯, map_biprod := ⋯ }

@[simp]

theorem TauCeti.SplitK0.ofInvariant_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (X : C) : (ofInvariant C).obj X = of X

noncomputable def TauCeti.SplitK0.map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesBiproductsOfShape CategoryTheory.Limits.WalkingPair F] : SplitK0 C →+ SplitK0 D

The homomorphism of split Grothendieck groups induced by a functor preserving zero morphisms and binary biproducts.

Equations

• TauCeti.SplitK0.map F = TauCeti.PresentedK0.map F ⋯

@[simp]

theorem TauCeti.SplitK0.map_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesBiproductsOfShape CategoryTheory.Limits.WalkingPair F] (X : C) : (map F) (of X) = of (F.obj X)

@[simp]

theorem TauCeti.SplitK0.map_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : map (CategoryTheory.Functor.id C) = AddMonoidHom.id (SplitK0 C)

SplitK0.map sends the identity functor to the identity homomorphism.

@[simp]

theorem TauCeti.SplitK0.map_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E : Type u''} [CategoryTheory.Category.{v'', u''} E] [CategoryTheory.Limits.HasZeroMorphisms E] [CategoryTheory.Limits.HasBinaryBiproducts E] [CategoryTheory.EssentiallySmall.{w'', v'', u''} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesBiproductsOfShape CategoryTheory.Limits.WalkingPair F] [G.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesBiproductsOfShape CategoryTheory.Limits.WalkingPair G] : map (F.comp G) = (map G).comp (map F)

SplitK0.map sends a composite of biproduct-preserving functors to the composite homomorphism.

theorem TauCeti.SplitK0.map_congr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {F G : CategoryTheory.Functor C D} [F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesBiproductsOfShape CategoryTheory.Limits.WalkingPair F] [G.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesBiproductsOfShape CategoryTheory.Limits.WalkingPair G] (h : ∀ (X : C), Nonempty (F.obj X ≅ G.obj X)) : map F = map G

Objectwise isomorphic biproduct-preserving functors induce the same map; in particular naturally isomorphic ones do.

noncomputable def TauCeti.SplitK0.mapEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (e : C ≌ D) : SplitK0 C ≃+ SplitK0 D

Split K₀ is invariant under equivalences of categories.

Equations

• TauCeti.SplitK0.mapEquiv e = TauCeti.PresentedK0.mapEquiv e ⋯ ⋯

@[simp]

theorem TauCeti.SplitK0.mapEquiv_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (e : C ≌ D) (X : C) : (mapEquiv e) (of X) = of (e.functor.obj X)

@[simp]

theorem TauCeti.SplitK0.mapEquiv_symm_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (e : C ≌ D) (Y : D) : (mapEquiv e).symm (of Y) = of (e.inverse.obj Y)

@[simp]

theorem TauCeti.SplitK0.mapEquiv_toAddMonoidHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (e : C ≌ D) : ↑(mapEquiv e) = map e.functor

The homomorphism underlying the equivalence invariance is the functorial map.

@[simp]

theorem TauCeti.SplitK0.AdditiveInvariant.obj_biproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {G : Type u_1} [AddCommGroup G] (v : AdditiveInvariant C G) [CategoryTheory.Limits.HasZeroObject C] {J : Type} [Fintype J] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] : v.obj (⨁ f) = ∑ j : J, v.obj (f j)

An additive invariant is additive on finite biproducts.

@[simp]

theorem TauCeti.SplitK0.of_biproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] [CategoryTheory.Limits.HasZeroObject C] {J : Type} [Fintype J] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] : of (⨁ f) = ∑ j : J, of (f j)

The class of a finite biproduct is the sum of the classes of its summands.

noncomputable def TauCeti.SplitK0.ofCode {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] : ObjectCode C →+ SplitK0 C

The class map of split K₀, as a homomorphism from the additive monoid of isomorphism classes of objects.

Equations

• TauCeti.SplitK0.ofCode = { toFun := fun (c : TauCeti.ObjectCode C) => TauCeti.SplitK0.of (Function.surjInv ⋯ c), map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.SplitK0.ofCode_objectCode {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] (X : C) : ofCode (objectCode X) = of X

noncomputable def TauCeti.SplitK0.grothendieckAddGroupInvariant (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] : AdditiveInvariant C (Algebra.GrothendieckAddGroup (ObjectCode C))

The invariant sending an object to its isomorphism class, viewed in the group completion of the monoid of isomorphism classes.

Equations

• TauCeti.SplitK0.grothendieckAddGroupInvariant C = { obj := fun (X : C) => Algebra.GrothendieckAddGroup.of (TauCeti.objectCode X), map_iso := ⋯, map_biprod := ⋯ }

@[simp]

theorem TauCeti.SplitK0.grothendieckAddGroupInvariant_obj {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] (X : C) : (grothendieckAddGroupInvariant C).obj X = Algebra.GrothendieckAddGroup.of (objectCode X)

noncomputable def TauCeti.SplitK0.grothendieckAddGroupEquiv (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] : Algebra.GrothendieckAddGroup (ObjectCode C) ≃+ SplitK0 C

Split K₀ is the group completion of the additive monoid of isomorphism classes of objects under the binary biproduct. This is Weibel's description of split K₀.

Equations

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

theorem TauCeti.SplitK0.grothendieckAddGroupEquiv_of_objectCode {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] (X : C) : (grothendieckAddGroupEquiv C) (Algebra.GrothendieckAddGroup.of (objectCode X)) = of X

The group-completion isomorphism sends the class of an isomorphism class to the class of the object. It is not a simp lemma: Algebra.GrothendieckAddGroup.of is reducible, so simp rewrites its left-hand side.

@[simp]

theorem TauCeti.SplitK0.grothendieckAddGroupEquiv_symm_of {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] (X : C) : (grothendieckAddGroupEquiv C).symm (of X) = Algebra.GrothendieckAddGroup.of (objectCode X)