Functoriality of the Grothendieck group of an abelian category

K₀Ab had no functoriality at all: every map out of it in the tree lands in a fixed abelian group through liftOf, and there was no K₀Ab A →+ K₀Ab B. This file supplies it.

Why the hypothesis is short exactness, not exactness

K₀Ab is presented by short exact sequences, so the only thing a functor has to do to induce a map is carry a short exact sequence to a short exact one. That is weaker than being exact, and it is exactly what liftOf consumes, so map takes it as a plain hypothesis in the style of the rest of this directory. mapOfExact is the convenience wrapper for a functor that preserves finite limits and colimits, where Mathlib's ShortExact.map_of_exact discharges it.

The equivalence case, and what it is for

congr upgrades an equivalence of abelian categories to an isomorphism of Grothendieck groups. The inverse is the equivalence's own inverse functor, and the round trips are hom_ext against of_iso on the unit and counit — no computation.

This is the first half of transporting numerical data along an equivalence. The motivating case is identifying coherent sheaves with the heart of the standard t-structure on their derived category: the μ-slope data of the Gieseker lane lives on Coh X, while the Mukai tilt assembly wants it on a heart, and a rank or degree homomorphism moves between them by precomposition with congr.

noncomputable def CategoryTheory.K₀Ab.map {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (F : Functor A B) [F.PreservesZeroMorphisms] (hF : ∀ (S : ShortComplex A), S.ShortExact → (S.map F).ShortExact) : K₀Ab A →+ K₀Ab B

The map induced by a functor that preserves short exactness.

Equations

• CategoryTheory.K₀Ab.map F hF = CategoryTheory.K₀Ab.liftOf (fun (X : A) => CategoryTheory.K₀Ab.of (F.obj X)) ⋯

@[simp]

theorem CategoryTheory.K₀Ab.map_of {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (F : Functor A B) [F.PreservesZeroMorphisms] (hF : ∀ (S : ShortComplex A), S.ShortExact → (S.map F).ShortExact) (X : A) : (map F hF) (of X) = of (F.obj X)

@[simp]

theorem CategoryTheory.K₀Ab.map_id {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] (hF : ∀ (S : ShortComplex A), S.ShortExact → (S.map (Functor.id A)).ShortExact) : map (Functor.id A) hF = AddMonoidHom.id (K₀Ab A)

The identity functor induces the identity.

theorem CategoryTheory.K₀Ab.map_comp {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] {D : Type u₃} [Category.{v₃, u₃} D] [Abelian D] (F : Functor A B) [F.PreservesZeroMorphisms] (hF : ∀ (S : ShortComplex A), S.ShortExact → (S.map F).ShortExact) (G : Functor B D) [G.PreservesZeroMorphisms] (hG : ∀ (S : ShortComplex B), S.ShortExact → (S.map G).ShortExact) (hFG : ∀ (S : ShortComplex A), S.ShortExact → (S.map (F.comp G)).ShortExact) : map (F.comp G) hFG = (map G hG).comp (map F hF)

Induced maps compose.

theorem CategoryTheory.K₀Ab.map_congr {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] {F G : Functor A B} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (hF : ∀ (S : ShortComplex A), S.ShortExact → (S.map F).ShortExact) (hG : ∀ (S : ShortComplex A), S.ShortExact → (S.map G).ShortExact) (e : F ≅ G) : map F hF = map G hG

Naturally isomorphic functors induce the same map.

noncomputable def CategoryTheory.K₀Ab.mapOfExact {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (F : Functor A B) [F.PreservesZeroMorphisms] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] : K₀Ab A →+ K₀Ab B

The map induced by an exact functor. ShortExact.map_of_exact discharges the hypothesis of map, so a functor preserving finite limits and colimits needs no side condition.

Equations

• CategoryTheory.K₀Ab.mapOfExact F = CategoryTheory.K₀Ab.map F ⋯

@[simp]

theorem CategoryTheory.K₀Ab.mapOfExact_of {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (F : Functor A B) [F.PreservesZeroMorphisms] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (X : A) : (mapOfExact F) (of X) = of (F.obj X)

noncomputable def CategoryTheory.K₀Ab.congr {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (e : A ≌ B) [e.functor.PreservesZeroMorphisms] [e.inverse.PreservesZeroMorphisms] : K₀Ab A ≃+ K₀Ab B

An equivalence of abelian categories induces an isomorphism of Grothendieck groups.

Both directions are mapOfExact; an equivalence preserves all limits and colimits, so no exactness side condition survives. The round trips are of_iso against the unit and counit.

Equations

• CategoryTheory.K₀Ab.congr e = { toFun := ⇑(CategoryTheory.K₀Ab.mapOfExact e.functor), invFun := ⇑(CategoryTheory.K₀Ab.mapOfExact e.inverse), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[simp]

theorem CategoryTheory.K₀Ab.congr_of {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (e : A ≌ B) [e.functor.PreservesZeroMorphisms] [e.inverse.PreservesZeroMorphisms] (X : A) : (congr e) (of X) = of (e.functor.obj X)

@[simp]

theorem CategoryTheory.K₀Ab.congr_symm_of {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (e : A ≌ B) [e.functor.PreservesZeroMorphisms] [e.inverse.PreservesZeroMorphisms] (Y : B) : (congr e).symm (of Y) = of (e.inverse.obj Y)

@[reducible, inline]

noncomputable abbrev CategoryTheory.K₀Ab.congrHom {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (e : A ≌ B) [e.functor.PreservesZeroMorphisms] [e.inverse.PreservesZeroMorphisms] : K₀Ab A →+ K₀Ab B

The isomorphism as an additive hom, for precomposition.

Equations

• CategoryTheory.K₀Ab.congrHom e = (CategoryTheory.K₀Ab.congr e).toAddMonoidHom

theorem CategoryTheory.K₀Ab.congrHom_of {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (e : A ≌ B) [e.functor.PreservesZeroMorphisms] [e.inverse.PreservesZeroMorphisms] (X : A) : (congrHom e) (of X) = of (e.functor.obj X)