The tensor product makes split K₀ a ring

The split Grothendieck group TauCeti.SplitK0 C of TauCeti/CategoryTheory/GrothendieckGroup/Split.lean records the additive structure of a category: [X ⊞ Y] = [X] + [Y]. When C also carries a monoidal structure whose tensor product is additive in each factor (CategoryTheory.MonoidalPreadditive), the tensor product descends to a multiplication on SplitK0 C and makes it a ring, commutative as soon as C is braided.

The construction is entirely a matter of feeding the tensor product to the universal property twice. For a fixed object X, tensoring on the left is an additive endofunctor of C, so TauCeti.SplitK0.map turns it into an endomorphism of the group. Sending X to that endomorphism is itself an isomorphism-invariant, biproduct-additive function of X -- additivity in X is TauCeti.SplitK0.map applied to tensoring on the right -- so it descends to TauCeti.SplitK0.mulHom, a biadditive multiplication with [X] * [Y] = [X ⊗ Y]. Distributivity is then automatic, and the remaining ring axioms are the associator, the unitors, and the braiding: each of them is an equality of bundled additive maps, so it is checked on the classes of objects by TauCeti.SplitK0.hom_ext.

The multiplication is not obtained by a second presentation: no new relation is imposed, and the underlying additive group is unchanged. In particular a biproduct-additive invariant into a ring becomes a ring homomorphism TauCeti.SplitK0.liftRingHom exactly when it sends the tensor unit to 1 and is multiplicative on the classes of objects, which is how character-style invariants are recognized.

This is the ring structure the representation ring R(G) of a finite group carries. Split K₀ is the right home for it: the Grothendieck group of a semisimple category, such as the finite-dimensional representations of a finite group over a field of characteristic zero, has no relations beyond the biproduct ones, so the split group is the representation ring there. Producing that instantiation additionally needs the smallness of the representation category, which is a separate matter and is not proved here; nothing below assumes semisimplicity.

Main definitions

• TauCeti.SplitK0.mulHom C: multiplication on split K₀, as a biadditive map.
• TauCeti.SplitK0.instRing and TauCeti.SplitK0.instCommRing: the ring structure, commutative for a braided category.
• TauCeti.SplitK0.liftRingHom: the ring homomorphism induced by a multiplicative, unit-preserving biproduct-additive invariant.
• TauCeti.SplitK0.mapRingHom: the ring homomorphism induced by a monoidal additive functor.

Main results

• TauCeti.SplitK0.of_mul_of: the computation rule [X] * [Y] = [X ⊗ Y], and TauCeti.SplitK0.one_def: the unit is the class of the tensor unit.
• TauCeti.SplitK0.ringHom_ext: two ring homomorphisms out of split K₀ agreeing on the classes of objects are equal.
• TauCeti.SplitK0.mapRingHom_id and TauCeti.SplitK0.mapRingHom_comp: the induced ring homomorphism is functorial.

Implementation notes

TauCeti.SplitK0.mulHom is stated as a bundled SplitK0 C →+ SplitK0 C →+ SplitK0 C rather than as a bare function, because biadditivity is exactly what makes the ring axioms checkable on the classes of objects: associativity, commutativity, and multiplicativity of an induced map are each an equality of bundled maps, so TauCeti.SplitK0.hom_ext reduces them to the classes of objects with no additive bookkeeping left to do.

Tensoring on the left by a fixed object, and the two lemmas saying that it is an isomorphism-invariant, biproduct-additive function of that object, are the input to the second use of the universal property and have no role afterwards, so they are private: the public computation rule is TauCeti.SplitK0.of_mul_of.

The Mul and One instances are installed before the Ring instance so that the axioms can be stated in the usual notation; the Ring instance reuses them rather than introducing new operations. Distributivity alone stages a private NonUnitalNonAssocRing structure, which is what makes Mathlib's bundled AddMonoidHom.mulLeft₃, AddMonoidHom.mulRight₃ and AddMonoidHom.mul applicable to the remaining axioms. No axiom witness is exported under a TauCeti.SplitK0 name: each is a field of the instance it discharges, so the general lemmas mul_assoc, one_mul, ... are the only ones to use.

References

• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Section 6, for the product on K₀ of a symmetric monoidal category.
• Mathlib/Algebra/DirectSum/Ring.lean, whose bundled-multiplication proof pattern for the ring structure on a graded direct sum is the one followed here: the associativity proof below is the same AddMonoidHom.mulLeft₃ = AddMonoidHom.mulRight₃ argument, the unit proofs the same mulHom 1 = AddMonoidHom.id and (mulHom).flip 1 = AddMonoidHom.id arguments, and TauCeti.SplitK0.ringHom_ext the same RingHom.toAddMonoidHom_injective argument as DirectSum.ringHom_ext, with the additive extensionality of the direct sum replaced by TauCeti.SplitK0.hom_ext.
• Character theory roadmap, Layer 4b, whose representation ring R(G) -- the Grothendieck ring of FDRep k G with addition from ⊕ and multiplication from ⊗ -- is the motivating instance of this ring structure.

noncomputable def TauCeti.SplitK0.mulHom (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : SplitK0 C →+ SplitK0 C →+ SplitK0 C

Multiplication on split K₀, as a biadditive map.

Equations

• TauCeti.SplitK0.mulHom C = TauCeti.SplitK0.lift (TauCeti.SplitK0.mulInvariant✝ C)

@[instance_reducible]

noncomputable instance TauCeti.SplitK0.instMul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : Mul (SplitK0 C)

The multiplication on split K₀ induced by the tensor product.

Equations

• TauCeti.SplitK0.instMul = { mul := fun (a b : TauCeti.SplitK0 C) => ((TauCeti.SplitK0.mulHom C) a) b }

theorem TauCeti.SplitK0.mul_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (a b : SplitK0 C) : a * b = ((mulHom C) a) b

The multiplication on split K₀ is TauCeti.SplitK0.mulHom.

@[instance_reducible]

noncomputable instance TauCeti.SplitK0.instOne {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : One (SplitK0 C)

The unit of split K₀ is the class of the tensor unit.

Equations

• TauCeti.SplitK0.instOne = { one := TauCeti.SplitK0.of (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) }

theorem TauCeti.SplitK0.one_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : 1 = of (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

The unit of split K₀ is the class of the tensor unit.

@[simp]

theorem TauCeti.SplitK0.of_mul_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (X Y : C) : of X * of Y = of (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

The computation rule for the product: the class of a tensor product is the product of the classes.

The ring structure

Distributivity is additivity of TauCeti.SplitK0.mulHom in each variable; it already stages a NonUnitalNonAssocRing structure. The remaining axioms are then equalities of the bundled maps AddMonoidHom.mulLeft₃, AddMonoidHom.mulRight₃ and AddMonoidHom.mul, so TauCeti.SplitK0.hom_ext reduces them to the classes of objects.

@[instance_reducible]

noncomputable instance TauCeti.SplitK0.instRing {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : Ring (SplitK0 C)

The tensor product makes the split Grothendieck group of a monoidal additive category a ring, with [X] * [Y] = [X ⊗ Y] and unit the class of the tensor unit: associativity is the associator of C, and the unit laws are its unitors.

Equations

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

theorem TauCeti.SplitK0.ringHom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {R : Type u_1} [NonAssocRing R] {f g : SplitK0 C →+* R} (h : ∀ (X : C), f (of X) = g (of X)) : f = g

Two ring homomorphisms out of split K₀ agreeing on the classes of objects are equal. The target is a ring rather than a semiring: split K₀ is generated by the classes of objects as a group, so agreeing on them forces agreement on the negatives only when the target has them.

theorem TauCeti.SplitK0.ringHom_ext_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {R : Type u_1} [NonAssocRing R] {f g : SplitK0 C →+* R} : f = g ↔ ∀ (X : C), f (of X) = g (of X)

noncomputable def TauCeti.SplitK0.liftRingHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {R : Type u_1} [NonAssocRing R] (a : AdditiveInvariant C R) (hone : a.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) = 1) (hmul : ∀ (X Y : C), a.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) = a.obj X * a.obj Y) : SplitK0 C →+* R

The ring homomorphism out of split K₀ induced by a biproduct-additive invariant which sends the tensor unit to 1 and is multiplicative on tensor products. With TauCeti.SplitK0.ringHom_ext for uniqueness, this is the universal property of split K₀ as a ring: it is what promotes a multiplicative invariant, such as a character, to a ring homomorphism. The target is a ring rather than a semiring because a TauCeti.SplitK0.AdditiveInvariant takes values in an additive group.

Equations

• TauCeti.SplitK0.liftRingHom a hone hmul = { toFun := ⇑(TauCeti.SplitK0.lift a), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.SplitK0.liftRingHom_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {R : Type u_1} [NonAssocRing R] (a : AdditiveInvariant C R) (hone : a.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) = 1) (hmul : ∀ (X Y : C), a.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) = a.obj X * a.obj Y) (X : C) : (liftRingHom a hone hmul) (of X) = a.obj X

The induced ring homomorphism takes the class of an object to the value of the invariant.

@[simp]

theorem TauCeti.SplitK0.liftRingHom_toAddMonoidHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {R : Type u_1} [NonAssocRing R] (a : AdditiveInvariant C R) (hone : a.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) = 1) (hmul : ∀ (X Y : C), a.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) = a.obj X * a.obj Y) : ↑(liftRingHom a hone hmul) = lift a

The additive homomorphism underlying TauCeti.SplitK0.liftRingHom is the additive lift of the invariant.

@[instance_reducible]

noncomputable instance TauCeti.SplitK0.instCommRing {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.BraidedCategory C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : CommRing (SplitK0 C)

For a braided monoidal additive category the ring structure on split K₀ is commutative: [X] * [Y] = [X ⊗ Y] = [Y ⊗ X] = [Y] * [X] by the braiding of C.

Equations

• TauCeti.SplitK0.instCommRing = { toRing := TauCeti.SplitK0.instRing, mul_comm := ⋯ }

noncomputable def TauCeti.SplitK0.mapRingHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (F : CategoryTheory.Functor C D) [F.Additive] [F.Monoidal] : SplitK0 C →+* SplitK0 D

The ring homomorphism of split Grothendieck groups induced by a monoidal additive functor: the functorial map TauCeti.SplitK0.map, read through the universal property as the invariant X ↦ [F.obj X], which the comparison isomorphisms of F make unit-preserving and multiplicative on tensor products.

Equations

• TauCeti.SplitK0.mapRingHom F = TauCeti.SplitK0.liftRingHom (TauCeti.SplitK0.liftEquiv.symm (TauCeti.SplitK0.map F)) ⋯ ⋯

@[simp]

theorem TauCeti.SplitK0.mapRingHom_toAddMonoidHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (F : CategoryTheory.Functor C D) [F.Additive] [F.Monoidal] : ↑(mapRingHom F) = map F

The additive homomorphism underlying TauCeti.SplitK0.mapRingHom is the functorial map.

@[simp]

theorem TauCeti.SplitK0.mapRingHom_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (F : CategoryTheory.Functor C D) [F.Additive] [F.Monoidal] (X : C) : (mapRingHom F) (of X) = of (F.obj X)

The induced ring homomorphism takes the class of an object to the class of its image.

@[simp]

theorem TauCeti.SplitK0.mapRingHom_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : mapRingHom (CategoryTheory.Functor.id C) = RingHom.id (SplitK0 C)

TauCeti.SplitK0.mapRingHom sends the identity functor to the identity ring homomorphism.

@[simp]

theorem TauCeti.SplitK0.mapRingHom_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E : Type u''} [CategoryTheory.Category.{v'', u''} E] [CategoryTheory.Preadditive E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.MonoidalPreadditive E] [CategoryTheory.Limits.HasBinaryBiproducts E] [CategoryTheory.EssentiallySmall.{w'', v'', u''} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.Additive] [G.Additive] [F.Monoidal] [G.Monoidal] : mapRingHom (F.comp G) = (mapRingHom G).comp (mapRingHom F)

TauCeti.SplitK0.mapRingHom sends a composite of monoidal additive functors to the composite ring homomorphism.

theorem TauCeti.SplitK0.mapRingHom_congr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] [F.Monoidal] [G.Monoidal] (h : ∀ (X : C), Nonempty (F.obj X ≅ G.obj X)) : mapRingHom F = mapRingHom G

Objectwise isomorphic monoidal additive functors induce the same ring homomorphism; in particular naturally isomorphic ones do.