The Grothendieck group of an abelian category #

K₀Ab A is the free abelian group on the objects of A modulo the relations [X₂] = [X₁] + [X₃] coming from short exact sequences.

Why this file did not exist, and what it replaces #

GrothendieckPresentation (Presentation.lean) is generic in its generator and relation types — it mentions no category at all — but it was instantiated only once, at distinguished triangles (Basic.lean). The abelian instantiation is three lines, and its absence is why the repository grew several hand-rolled copies of the same universal property written out longhand: a function on objects together with map_zero, map_iso and map_additive fields is an additive map out of K₀Ab, and nothing else.

With K₀Ab those three fields stop being data. of_isZero, of_iso and of_shortExact are theorems here, proved once, and every consumer gets them through AddMonoidHom instead of restating them.

Placement #

This file and Presentation.lean sit under CategoryTheory/GrothendieckGroup/ because neither consumes anything triangulated. K₀ itself, built on distTriang, stays under Triangulated/GrothendieckGroup/, where it belongs.

The rule that places them — a file belongs under Triangulated/ only if it uses something triangulated — is the same one that puts heartDatum beside the class datum it instantiates rather than beside the §14 lane that consumes it.

Main results #

K₀Ab and K₀Ab.of;
K₀Ab.of_shortExact — the defining relation;
K₀Ab.of_isZero and K₀Ab.of_iso — proved, not assumed;
K₀Ab.lift / K₀Ab.hom_ext — the universal property, inherited from GrothendieckPresentation.

source

@[reducible, inline]

abbrev CategoryTheory.abelianPresentation (A : Type u) [Category.{v, u} A] [Abelian A] :

GrothendieckPresentation A { S : ShortComplex A // S.ShortExact }

Objects of an abelian category, related by its short exact sequences.

Equations

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

Instances For

source

@[reducible, inline]

abbrev CategoryTheory.K₀Ab (A : Type u) [Category.{v, u} A] [Abelian A] :

Type u

The Grothendieck group of an abelian category.

Equations

CategoryTheory.K₀Ab A = (CategoryTheory.abelianPresentation A).Group

Instances For

source

def CategoryTheory.K₀Ab.of {A : Type u} [Category.{v, u} A] [Abelian A] (X : A) :

K₀Ab A

The class of an object.

Equations

CategoryTheory.K₀Ab.of X = (CategoryTheory.abelianPresentation A).of X

Instances For

source

theorem CategoryTheory.K₀Ab.of_shortExact {A : Type u} [Category.{v, u} A] [Abelian A] (S : ShortComplex A) (hS : S.ShortExact) :

of S.X₂ = of S.X₁ + of S.X₃

The defining relation: a short exact sequence splits the middle class.

source

theorem CategoryTheory.K₀Ab.of_isZero {A : Type u} [Category.{v, u} A] [Abelian A] {X : A} (hX : Limits.IsZero X) :

of X = 0

A zero object has zero class. Proved from the short exact sequence X ⟶ X ⟶ X on a zero object, which forces [X] = [X] + [X].

source

@[simp]

theorem CategoryTheory.K₀Ab.of_zero {A : Type u} [Category.{v, u} A] [Abelian A] :

of 0 = 0

source

theorem CategoryTheory.K₀Ab.of_iso {A : Type u} [Category.{v, u} A] [Abelian A] {X Y : A} (e : X ≅ Y) :

of X = of Y

Isomorphic objects have the same class. Proved from the short exact sequence X ≅ Y ⟶ 0, not assumed as a field.

source

def CategoryTheory.K₀Ab.lift {A : Type u} [Category.{v, u} A] [Abelian A] {G : Type u_1} [AddCommGroup G] (f : A → G) [(abelianPresentation A).IsAdditive f] :

K₀Ab A →+ G

The universal additive map out of K₀Ab.

Equations

CategoryTheory.K₀Ab.lift f = (CategoryTheory.abelianPresentation A).lift f

Instances For

source

@[simp]

theorem CategoryTheory.K₀Ab.lift_of {A : Type u} [Category.{v, u} A] [Abelian A] {G : Type u_1} [AddCommGroup G] (f : A → G) [(abelianPresentation A).IsAdditive f] (X : A) :

(lift f) (of X) = f X

source

noncomputable def CategoryTheory.K₀Ab.liftOf {A : Type u} [Category.{v, u} A] [Abelian A] {G : Type u_1} [AddCommGroup G] (f : A → G) (h : ∀ (S : ShortComplex A), S.ShortExact → f S.X₂ = f S.X₁ + f S.X₃) :

K₀Ab A →+ G

The universal property in the form producers actually want: a function on objects that is additive on short exact sequences induces a hom, with the additivity supplied as a proof rather than as an instance.

This is what replaces a map_zero / map_iso / additive field triple. Note that only additivity is required: of_isZero and of_iso then give the other two for free, so a producer that used to carry three fields now carries one proof.

Equations