Abelian K₀ of an essentially small abelian category

The abelian Grothendieck group TauCeti.AbelianK0 C of an essentially small abelian category C is the free abelian group on the isomorphism classes of objects modulo the relations [X₂] = [X₁] + [X₃], one for each short exact sequence X₁ ⟶ X₂ ⟶ X₃.

It is not a second presentation: it is defined as the exact K₀ of the canonical exact structure TauCeti.ExactStructure.abelian C, whose conflations are exactly the short exact short complexes. The whole exact-K₀ API therefore applies verbatim, along the identification TauCeti.AbelianK0.toExactK0; what this file adds is the same API phrased in terms of CategoryTheory.ShortComplex.ShortExact instead of conflations, functoriality under the exactness hypothesis appropriate to abelian categories, and the calculus of kernels and cokernels which is available here but not in a general exact category.

The last point is the substance of the file. Because an abelian category factors every morphism, an arbitrary f : X ⟶ Y — with no monomorphism or epimorphism hypothesis whatsoever — satisfies [X] - [Y] = [ker f] - [coker f] in AbelianK0 C; see TauCeti.AbelianK0.of_sub_of_eq_of_kernel_sub_of_cokernel. The proof splits f through its coimage and its image and uses that the two agree.

Main definitions

• TauCeti.AbelianK0 C: abelian K₀, with class map TauCeti.AbelianK0.of, defined as the exact K₀ of TauCeti.ExactStructure.abelian C.
• TauCeti.AbelianK0.toExactK0: the identification of abelian K₀ with that exact K₀, along which the exact-K₀ API transfers.
• TauCeti.AbelianK0.AdditiveInvariant C G: a function on objects which is additive on short exact sequences, and TauCeti.AbelianK0.lift the homomorphism it induces.
• TauCeti.AbelianK0.map and TauCeti.AbelianK0.mapEquiv: functoriality for an additive functor preserving finite limits and finite colimits, and invariance under an additive equivalence.
• TauCeti.AbelianK0.fromSplit: the canonical comparison out of split K₀.

Main results

• TauCeti.AbelianK0.of_shortExact: the defining relation, with TauCeti.AbelianK0.of_eq_add_of_cokernel and TauCeti.AbelianK0.of_eq_of_kernel_add its consequences for a monomorphism and for an epimorphism.
• TauCeti.AbelianK0.of_sub_of_eq_of_kernel_sub_of_cokernel: for every morphism f : X ⟶ Y, [X] - [Y] = [ker f] - [coker f].
• TauCeti.AbelianK0.liftEquiv: the universal property. Invariants additive on short exact sequences correspond bijectively to homomorphisms AbelianK0 C →+ G.
• TauCeti.AbelianK0.map_comp_fromSplit: naturality of the comparison out of split K₀ in an exact functor.

References

• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Section 6.1.2, where K₀ of an abelian category and its universal property for invariants additive on short exact sequences are stated.
• Theo Bühler, Exact categories, Expositiones Mathematicae 28 (2010), 1–69, Section 13.2, for the canonical exact structure whose exact K₀ this is.

def TauCeti.AbelianK0 (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : Type w

The Grothendieck group of an essentially small abelian category: the free abelian group on the isomorphism classes of objects, modulo [X₂] = [X₁] + [X₃] for every short exact sequence X₁ ⟶ X₂ ⟶ X₃. It is the exact K₀ of the canonical exact structure.

Equations

• TauCeti.AbelianK0 C = TauCeti.ExactK0 (TauCeti.ExactStructure.abelian C)

@[instance_reducible]

noncomputable instance TauCeti.instAddCommGroupAbelianK0 (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : AddCommGroup (AbelianK0 C)

Equations

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

noncomputable def TauCeti.AbelianK0.toExactK0 (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : AbelianK0 C ≃+ ExactK0 (ExactStructure.abelian C)

Abelian K₀ is the exact K₀ of the canonical exact structure, by definition. This identification is the bridge along which the exact-K₀ API applies to abelian K₀.

Equations

• TauCeti.AbelianK0.toExactK0 C = AddEquiv.refl (TauCeti.AbelianK0 C)

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

The class of an object in abelian K₀.

Equations

• TauCeti.AbelianK0.of X = TauCeti.ExactK0.of X

@[simp]

theorem TauCeti.AbelianK0.toExactK0_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (X : C) : (toExactK0 C) (of X) = ExactK0.of X

@[simp]

theorem TauCeti.AbelianK0.toExactK0_symm_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (X : C) : (toExactK0 C).symm (ExactK0.of X) = of X

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

theorem TauCeti.AbelianK0.of_shortExact {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) : of S.X₂ = of S.X₁ + of S.X₃

The defining relation of abelian K₀: the class of the middle term of a short exact sequence is the sum of the classes of its outer terms.

theorem TauCeti.AbelianK0.of_eq_add_of_shortExact {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {X Y Z : C} {i : X ⟶ Y} {p : Y ⟶ Z} (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hS : { X₁ := X, X₂ := Y, X₃ := Z, f := i, g := p, zero := zero }.ShortExact) : of Y = of X + of Z

The defining relation of abelian K₀, stated for a short exact sequence presented by its two maps.

theorem TauCeti.AbelianK0.of_eq_sub_of_shortExact {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) : of S.X₁ = of S.X₂ - of S.X₃

The class of the subobject of a short exact sequence is the difference of the other two classes.

@[simp]

theorem TauCeti.AbelianK0.of_biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (X Y : C) : of (X ⊞ Y) = of X + of Y

The class of a biproduct is the sum of the classes.

@[simp]

theorem TauCeti.AbelianK0.of_eq_zero_of_isZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian 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.AbelianK0.of_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : of 0 = 0

The class of the zero object vanishes.

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

The image of the class map generates abelian K₀.

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

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

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

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

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

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

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

theorem TauCeti.AbelianK0.of_eq_add_of_cokernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {X Y : C} (i : X ⟶ Y) [CategoryTheory.Mono i] : of Y = of X + of (CategoryTheory.Limits.cokernel i)

A monomorphism i : X ⟶ Y gives [Y] = [X] + [coker i].

theorem TauCeti.AbelianK0.of_eq_of_kernel_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {Y Z : C} (p : Y ⟶ Z) [CategoryTheory.Epi p] : of Y = of (CategoryTheory.Limits.kernel p) + of Z

An epimorphism p : Y ⟶ Z gives [Y] = [ker p] + [Z].

theorem TauCeti.AbelianK0.of_eq_of_kernel_add_of_coimage {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {X Y : C} (f : X ⟶ Y) : of X = of (CategoryTheory.Limits.kernel f) + of (CategoryTheory.Abelian.coimage f)

The class of the coimage of a morphism: [X] = [ker f] + [coim f], because X surjects onto its coimage with kernel ker f.

theorem TauCeti.AbelianK0.of_eq_of_image_add_of_cokernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {X Y : C} (f : X ⟶ Y) : of Y = of (CategoryTheory.Abelian.image f) + of (CategoryTheory.Limits.cokernel f)

The class of the image of a morphism: [Y] = [im f] + [coker f], because the image of f is the kernel of the cokernel projection of f.

theorem TauCeti.AbelianK0.of_sub_of_eq_of_kernel_sub_of_cokernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {X Y : C} (f : X ⟶ Y) : of X - of Y = of (CategoryTheory.Limits.kernel f) - of (CategoryTheory.Limits.cokernel f)

The kernel–cokernel identity in abelian K₀: an arbitrary morphism f : X ⟶ Y, with no monomorphism or epimorphism hypothesis, satisfies [X] - [Y] = [ker f] - [coker f].

The two sides measure the same defect: X and Y differ, in K₀, only through the kernel and cokernel of f, because f factors as an epimorphism onto its coimage followed by a monomorphism out of its image, and coimage and image agree in an abelian category.

structure TauCeti.AbelianK0.AdditiveInvariant (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (G : Type u_2) [AddCommGroup G] : Type (max u u_2)

An additive invariant for abelian K₀: a function on objects of C, additive on short exact sequences. These are exactly the data that factor through TauCeti.AbelianK0 C; see TauCeti.AbelianK0.liftEquiv. It is then constant on isomorphism classes (TauCeti.AbelianK0.AdditiveInvariant.map_iso).

• obj : C → G

  The value of the invariant on an object.

• map_shortExact ⦃S : CategoryTheory.ShortComplex C⦄ : S.ShortExact → self.obj S.X₂ = self.obj S.X₁ + self.obj S.X₃

  The value on the middle term of a short exact sequence is the sum of the outer values.

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

theorem TauCeti.AbelianK0.AdditiveInvariant.ext_iff {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Abelian C} {G : Type u_2} {inst✝² : AddCommGroup G} {x y : AdditiveInvariant C G} : x = y ↔ x.obj = y.obj

theorem TauCeti.AbelianK0.AdditiveInvariant.map_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {G : Type u_1} [AddCommGroup G] (a : AdditiveInvariant C G) ⦃X Y : C⦄ (e : X ≅ Y) : a.obj X = a.obj Y

An invariant additive on short exact sequences takes equal values on isomorphic objects.

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

The homomorphism out of abelian K₀ induced by an invariant additive on short exact sequences.

Equations

• TauCeti.AbelianK0.lift a = TauCeti.ExactK0.lift (TauCeti.AbelianK0.AdditiveInvariant.toExact✝ a)

@[simp]

theorem TauCeti.AbelianK0.lift_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian 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.AbelianK0.lift_unique {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] (a : AdditiveInvariant C G) (f : AbelianK0 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.AbelianK0.liftEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] : AdditiveInvariant C G ≃ (AbelianK0 C →+ G)

The universal property of abelian K₀: invariants additive on short exact sequences with values in G correspond bijectively to additive homomorphisms AbelianK0 C →+ G.

Equations

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

@[simp]

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

@[simp]

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

noncomputable def TauCeti.AbelianK0.map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : AbelianK0 C →+ AbelianK0 D

Functoriality of abelian K₀: an additive functor preserving finite limits and finite colimits — that is, an exact functor — induces a homomorphism of abelian Grothendieck groups.

Exactness is the right hypothesis and cannot be weakened to additivity: an additive functor need not send a short exact sequence to a short exact one, so it need not respect the defining relations.

Equations

• TauCeti.AbelianK0.map F = TauCeti.ExactK0.map F ⋯

@[simp]

theorem TauCeti.AbelianK0.map_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C) : (map F) (of X) = of (F.obj X)

theorem TauCeti.AbelianK0.map_unique {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] (f : AbelianK0 C →+ AbelianK0 D) (hf : ∀ (X : C), f (of X) = of (F.obj X)) : f = map F

Any homomorphism sending object classes to the classes of their images is the induced map.

@[simp]

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

The identity functor induces the identity of abelian K₀.

theorem TauCeti.AbelianK0.map_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] {K : Type u''} [CategoryTheory.Category.{v'', u''} K] [CategoryTheory.Abelian K] [CategoryTheory.EssentiallySmall.{w'', v'', u''} K] (H : CategoryTheory.Functor D K) [H.Additive] [CategoryTheory.Limits.PreservesFiniteLimits H] [CategoryTheory.Limits.PreservesFiniteColimits H] : map (F.comp H) = (map H).comp (map F)

The induced maps of a composite of exact functors compose.

theorem TauCeti.AbelianK0.map_congr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] {F' : CategoryTheory.Functor C D} [F'.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F'] [CategoryTheory.Limits.PreservesFiniteColimits F'] (e : F ≅ F') : map F = map F'

Naturally isomorphic exact functors induce the same map.

noncomputable def TauCeti.AbelianK0.mapEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (e : C ≌ D) [e.functor.Additive] : AbelianK0 C ≃+ AbelianK0 D

Equivalence invariance of abelian K₀: an additive equivalence of abelian categories induces an isomorphism of abelian Grothendieck groups. No exactness hypothesis is needed, since an equivalence preserves all limits and colimits.

Equations

• TauCeti.AbelianK0.mapEquiv e = TauCeti.ExactK0.mapEquiv e ⋯ ⋯

@[simp]

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

@[simp]

theorem TauCeti.AbelianK0.mapEquiv_symm_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (e : C ≌ D) [e.functor.Additive] (Y : D) : (mapEquiv e).symm (of Y) = of (e.inverse.obj Y)

noncomputable def TauCeti.AbelianK0.fromSplit (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : SplitK0 C →+ AbelianK0 C

The canonical comparison from split K₀ to abelian K₀. It is induced by the class map, which respects the biproduct relations because the biproduct sequences are short exact.

Equations

• TauCeti.AbelianK0.fromSplit C = TauCeti.ExactK0.fromSplit (TauCeti.ExactStructure.abelian C)

@[simp]

theorem TauCeti.AbelianK0.fromSplit_of (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (X : C) : (fromSplit C) (SplitK0.of X) = of X

theorem TauCeti.AbelianK0.fromSplit_unique (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (f : SplitK0 C →+ AbelianK0 C) (hf : ∀ (X : C), f (SplitK0.of X) = of X) : f = fromSplit C

The canonical comparison out of split K₀ is the unique homomorphism preserving the classes of objects.

theorem TauCeti.AbelianK0.fromSplit_surjective (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : Function.Surjective ⇑(fromSplit C)

The canonical comparison out of split K₀ is surjective: abelian K₀ is a quotient of split K₀, since imposing the short exact relations only adds relations.

theorem TauCeti.AbelianK0.map_comp_fromSplit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : (map F).comp (fromSplit C) = (fromSplit D).comp (SplitK0.map F)

Naturality of the comparison out of split K₀ in an exact functor.