Grothendieck groups of product categories

This file identifies the split Grothendieck group of a product of additive categories with the product of their split Grothendieck groups. It also identifies the exact Grothendieck group of the componentwise exact structure with the product of the two exact Grothendieck groups, and the triangulated Grothendieck group of a product of pretriangulated categories with the product of the two triangulated Grothendieck groups. All three equivalences are characterised on object classes and are natural in the relevant functors.

Main definitions

• TauCeti.SplitK0.prodEquiv: the canonical equivalence SplitK0 (C × D) ≃+ SplitK0 C × SplitK0 D.
• TauCeti.ExactK0.prodEquiv: the canonical equivalence ExactK0 (E.prod E') ≃+ ExactK0 E × ExactK0 E'.
• TauCeti.TriangulatedK0.prodEquiv: the canonical equivalence TriangulatedK0 (C × D) ≃+ TriangulatedK0 C × TriangulatedK0 D.

Main results

• TauCeti.SplitK0.prodEquiv_apply: the forward map is induced by the two projections.
• TauCeti.SplitK0.prodEquiv_symm_apply: the inverse is the sum of the two zero-section maps.
• TauCeti.SplitK0.prodEquiv_of: the equivalence sends [(X, Y)] to ([X], [Y]).
• TauCeti.SplitK0.prodEquiv_naturality: the equivalence is natural in additive functors.
• TauCeti.ExactK0.prodEquiv_naturality: the exact equivalence is natural in conflation-exact functors.
• TauCeti.TriangulatedK0.prodEquiv_of and TauCeti.TriangulatedK0.prodEquiv_naturality: the triangulated equivalence sends [X] to ([X₁], [X₂]) and is natural in triangulated functors.

noncomputable def TauCeti.SplitK0.prodEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] : SplitK0 (C × D) ≃+ SplitK0 C × SplitK0 D

Split K₀ takes a product of additive categories to the product of their split Grothendieck groups.

Equations

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

@[simp]

theorem TauCeti.SplitK0.prodEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (x : SplitK0 (C × D)) : prodEquiv x = ((map (CategoryTheory.Prod.fst C D)) x, (map (CategoryTheory.Prod.snd C D)) x)

The forward product equivalence is induced by the two projection functors.

theorem TauCeti.SplitK0.prodEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (x : SplitK0 C × SplitK0 D) : prodEquiv.symm x = (map (CategoryTheory.Prod.sectL C 0)) x.1 + (map (CategoryTheory.Prod.sectR 0 D)) x.2

The inverse product equivalence is the sum of the maps induced by inserting a zero object in each coordinate.

theorem TauCeti.SplitK0.prodEquiv_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (X : C × D) : prodEquiv (of X) = (of X.1, of X.2)

The product equivalence sends an object class to the pair of its component classes.

@[simp]

theorem TauCeti.SplitK0.prodEquiv_symm_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (X : C) (Y : D) : prodEquiv.symm (of X, of Y) = of (X, Y)

The inverse product equivalence sends a pair of object classes to the class of the paired object.

theorem TauCeti.SplitK0.prodEquiv_naturality {C₁ : Type u₁} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Preadditive C₁] [CategoryTheory.Limits.HasZeroObject C₁] [CategoryTheory.Limits.HasBinaryBiproducts C₁] [CategoryTheory.EssentiallySmall.{w₁, v₁, u₁} C₁] {C₂ : Type u₂} [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Preadditive C₂] [CategoryTheory.Limits.HasZeroObject C₂] [CategoryTheory.Limits.HasBinaryBiproducts C₂] [CategoryTheory.EssentiallySmall.{w₂, v₂, u₂} C₂] {D₁ : Type u} [CategoryTheory.Category.{v, u} D₁] [CategoryTheory.Preadditive D₁] [CategoryTheory.Limits.HasZeroObject D₁] [CategoryTheory.Limits.HasBinaryBiproducts D₁] [CategoryTheory.EssentiallySmall.{w, v, u} D₁] {D₂ : Type u'} [CategoryTheory.Category.{v', u'} D₂] [CategoryTheory.Preadditive D₂] [CategoryTheory.Limits.HasZeroObject D₂] [CategoryTheory.Limits.HasBinaryBiproducts D₂] [CategoryTheory.EssentiallySmall.{w', v', u'} D₂] (F : CategoryTheory.Functor C₁ C₂) (G : CategoryTheory.Functor D₁ D₂) [F.Additive] [G.Additive] : (↑prodEquiv).comp (map (F.prod G)) = ((map F).prodMap (map G)).comp ↑prodEquiv

The split-K₀ product equivalence is natural in additive functors in both variables.

noncomputable def TauCeti.ExactK0.prodEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (E : ExactStructure C) (E' : ExactStructure D) : ExactK0 (E.prod E') ≃+ ExactK0 E × ExactK0 E'

Exact K₀ takes a componentwise product of exact categories to the product of their exact Grothendieck groups.

Equations

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

@[simp]

theorem TauCeti.ExactK0.prodEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (E : ExactStructure C) (E' : ExactStructure D) (x : ExactK0 (E.prod E')) : (prodEquiv E E') x = ((map (CategoryTheory.Prod.fst C D) ⋯) x, (map (CategoryTheory.Prod.snd C D) ⋯) x)

The forward exact-K₀ product equivalence is induced by the two projection functors.

theorem TauCeti.ExactK0.prodEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (E : ExactStructure C) (E' : ExactStructure D) (x : ExactK0 E × ExactK0 E') : (prodEquiv E E').symm x = (map (CategoryTheory.Prod.sectL C 0) ⋯) x.1 + (map (CategoryTheory.Prod.sectR 0 D) ⋯) x.2

The inverse exact-K₀ product equivalence is the sum of the maps induced by the two zero sections.

theorem TauCeti.ExactK0.prodEquiv_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (E : ExactStructure C) (E' : ExactStructure D) (X : C × D) : (prodEquiv E E') (of X) = (of X.1, of X.2)

The exact-K₀ product equivalence sends an object class to the pair of its component classes.

@[simp]

theorem TauCeti.ExactK0.prodEquiv_symm_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (E : ExactStructure C) (E' : ExactStructure D) (X : C) (Y : D) : (prodEquiv E E').symm (of X, of Y) = of (X, Y)

The inverse exact-K₀ product equivalence sends a pair of object classes to the class of the paired object.

theorem TauCeti.ExactK0.prodEquiv_naturality {C₁ : Type u₁} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Preadditive C₁] [CategoryTheory.Limits.HasZeroObject C₁] [CategoryTheory.Limits.HasBinaryBiproducts C₁] [CategoryTheory.EssentiallySmall.{w₁, v₁, u₁} C₁] {C₂ : Type u₂} [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Preadditive C₂] [CategoryTheory.Limits.HasZeroObject C₂] [CategoryTheory.Limits.HasBinaryBiproducts C₂] [CategoryTheory.EssentiallySmall.{w₂, v₂, u₂} C₂] {D₁ : Type u} [CategoryTheory.Category.{v, u} D₁] [CategoryTheory.Preadditive D₁] [CategoryTheory.Limits.HasZeroObject D₁] [CategoryTheory.Limits.HasBinaryBiproducts D₁] [CategoryTheory.EssentiallySmall.{w, v, u} D₁] {D₂ : Type u'} [CategoryTheory.Category.{v', u'} D₂] [CategoryTheory.Preadditive D₂] [CategoryTheory.Limits.HasZeroObject D₂] [CategoryTheory.Limits.HasBinaryBiproducts D₂] [CategoryTheory.EssentiallySmall.{w', v', u'} D₂] {E₁ : ExactStructure C₁} {E₂ : ExactStructure C₂} {E₁' : ExactStructure D₁} {E₂' : ExactStructure D₂} (F : CategoryTheory.Functor C₁ C₂) (G : CategoryTheory.Functor D₁ D₂) [F.Additive] [G.Additive] (hF : E₁.IsConflationExact E₂ F) (hG : E₁'.IsConflationExact E₂' G) : (↑(prodEquiv E₂ E₂')).comp (map (F.prod G) ⋯) = ((map F hF).prodMap (map G hG)).comp ↑(prodEquiv E₁ E₁')

The exact-K₀ product equivalence is natural in conflation-exact functors in both variables.

noncomputable def TauCeti.TriangulatedK0.prodEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] : TriangulatedK0 (C × D) ≃+ TriangulatedK0 C × TriangulatedK0 D

Triangulated K₀ takes a product of pretriangulated categories to the product of their triangulated Grothendieck groups.

Equations

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

@[simp]

theorem TauCeti.TriangulatedK0.prodEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (x : TriangulatedK0 (C × D)) : prodEquiv x = ((map (CategoryTheory.Prod.fst C D)) x, (map (CategoryTheory.Prod.snd C D)) x)

The forward triangulated-K₀ product equivalence is induced by the two projection functors.

theorem TauCeti.TriangulatedK0.prodEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (x : TriangulatedK0 C × TriangulatedK0 D) : prodEquiv.symm x = (map (CategoryTheory.Prod.sectL C 0)) x.1 + (map (CategoryTheory.Prod.sectR 0 D)) x.2

The inverse triangulated-K₀ product equivalence is the sum of the maps induced by the two zero sections.

theorem TauCeti.TriangulatedK0.prodEquiv_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (X : C × D) : prodEquiv (of X) = (of X.1, of X.2)

The triangulated-K₀ product equivalence sends an object class to the pair of its component classes.

@[simp]

theorem TauCeti.TriangulatedK0.prodEquiv_symm_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (X : C) (Y : D) : prodEquiv.symm (of X, of Y) = of (X, Y)

The inverse triangulated-K₀ product equivalence sends a pair of object classes to the class of the paired object.

theorem TauCeti.TriangulatedK0.prodEquiv_naturality {C₁ : Type u₁} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Preadditive C₁] [CategoryTheory.Limits.HasZeroObject C₁] [CategoryTheory.HasShift C₁ ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C₁ n).Additive] [CategoryTheory.Pretriangulated C₁] [CategoryTheory.EssentiallySmall.{w₁, v₁, u₁} C₁] {C₂ : Type u₂} [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Preadditive C₂] [CategoryTheory.Limits.HasZeroObject C₂] [CategoryTheory.HasShift C₂ ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C₂ n).Additive] [CategoryTheory.Pretriangulated C₂] [CategoryTheory.EssentiallySmall.{w₂, v₂, u₂} C₂] {D₁ : Type u} [CategoryTheory.Category.{v, u} D₁] [CategoryTheory.Preadditive D₁] [CategoryTheory.Limits.HasZeroObject D₁] [CategoryTheory.HasShift D₁ ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D₁ n).Additive] [CategoryTheory.Pretriangulated D₁] [CategoryTheory.EssentiallySmall.{w, v, u} D₁] {D₂ : Type u'} [CategoryTheory.Category.{v', u'} D₂] [CategoryTheory.Preadditive D₂] [CategoryTheory.Limits.HasZeroObject D₂] [CategoryTheory.HasShift D₂ ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D₂ n).Additive] [CategoryTheory.Pretriangulated D₂] [CategoryTheory.EssentiallySmall.{w', v', u'} D₂] (F : CategoryTheory.Functor C₁ C₂) (G : CategoryTheory.Functor D₁ D₂) [F.CommShift ℤ] [G.CommShift ℤ] [F.IsTriangulated] [G.IsTriangulated] : (↑prodEquiv).comp (map (F.prod G)) = ((map F).prodMap (map G)).comp ↑prodEquiv

The triangulated-K₀ product equivalence is natural in triangulated functors in both variables.