The tensor product makes exact K₀ a ring #
Let E be an exact structure on an essentially small monoidal additive category C whose tensor
product is biexact (TauCeti.ExactStructure.IsMonoidal). Then (X, Y) ↦ [X ⊗ Y] is additive on
E-conflations in each variable, so it descends to a biadditive multiplication on the exact
Grothendieck group TauCeti.ExactK0 E, which makes it a ring with unit the class of the tensor
unit, commutative as soon as C is braided.
This is the ring structure of the Grothendieck ring G₀(k[G]) of all finite-dimensional
representations of a finite group over a field, where the relations come from every short exact
sequence rather than only the split ones. Biexactness is exactly what is needed: over a field the
tensor product is exact in each variable, even when short exact sequences of representations do
not split.
The construction parallels TauCeti/CategoryTheory/GrothendieckGroup/Monoidal/Basic.lean for
split K₀, with the biproduct relations replaced by conflations: the multiplication is the
two-variable descent TauCeti.ExactK0.BiadditiveInvariant.bilift of (X, Y) ↦ [X ⊗ Y]. The
canonical comparison TauCeti.ExactK0.fromSplit from split K₀ is a ring homomorphism,
TauCeti.ExactK0.fromSplitRingHom.
Main definitions #
TauCeti.ExactK0.mulHom E: multiplication on exactK₀, as a biadditive map.TauCeti.ExactK0.instRingandTauCeti.ExactK0.instCommRing: the ring structure, commutative for a braided category.TauCeti.ExactK0.liftRingHom: the ring homomorphism induced by a multiplicative, unit-preserving conflation-additive invariant.TauCeti.ExactK0.mapRingHom: the ring homomorphism induced by a conflation-exact monoidal additive functor.TauCeti.ExactK0.fromSplitRingHom: the comparison from splitK₀as a ring homomorphism.TauCeti.ExactK0.fromSplitRingEquiv: the comparison as a ring equivalence when every conflation splits.
Main results #
TauCeti.ExactK0.of_mul_of: the computation rule[X] * [Y] = [X ⊗ Y], andTauCeti.ExactK0.one_def: the unit is the class of the tensor unit.TauCeti.ExactK0.ringHom_ext: two ring homomorphisms out of exactK₀agreeing on the classes of objects are equal.
References #
- Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Section 7,
for exact
K₀and the products induced on it by biexact pairings, and Section 4 for the ring structure onK₀of a symmetric monoidal category. - J.-P. Serre, Linear Representations of Finite Groups, Springer GTM 42 (1977), §14.1, for the
ring
R_k(G)of a finite group over a field of arbitrary characteristic.
Multiplication on exact K₀, as a biadditive map.
Equations
Instances For
The multiplication on exact K₀ induced by the tensor product.
Equations
- TauCeti.ExactK0.instMul = { mul := fun (a b : TauCeti.ExactK0 E) => ((TauCeti.ExactK0.mulHom E) a) b }
The multiplication on exact K₀ is TauCeti.ExactK0.mulHom.
The unit of exact K₀ is the class of the tensor unit.
Equations
The unit of exact K₀ is the class of the tensor unit.
The computation rule for the product: the class of a tensor product is the product of the classes.
The tensor product makes the exact Grothendieck group of a monoidal exact category a ring, with
[X] * [Y] = [X ⊗ Y] and unit the class of the tensor unit.
Equations
- One or more equations did not get rendered due to their size.
Two ring homomorphisms out of exact K₀ agreeing on the classes of objects are equal.
The ring homomorphism out of exact K₀ induced by a conflation-additive invariant which sends
the tensor unit to 1 and is multiplicative on tensor products. With
TauCeti.ExactK0.ringHom_ext for uniqueness, this is the universal property of exact K₀ as a
ring.
Equations
- TauCeti.ExactK0.liftRingHom a hone hmul = { toFun := ⇑(TauCeti.ExactK0.lift a), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The induced ring homomorphism takes the class of an object to the value of the invariant.
The additive homomorphism underlying TauCeti.ExactK0.liftRingHom is the additive lift of the
invariant.
The comparison from split K₀ is a ring homomorphism. The canonical surjection
TauCeti.ExactK0.fromSplit from the split Grothendieck ring onto the exact one preserves the unit
and the product, since both are given by the tensor product on classes of objects.
Equations
- TauCeti.ExactK0.fromSplitRingHom E = TauCeti.SplitK0.liftRingHom { obj := fun (X : C) => TauCeti.ExactK0.of X, map_iso := ⋯, map_biprod := ⋯ } ⋯ ⋯
Instances For
The comparison ring homomorphism takes the class of an object to its class.
The additive homomorphism underlying TauCeti.ExactK0.fromSplitRingHom is
TauCeti.ExactK0.fromSplit.
The comparison from split to exact Grothendieck rings is bijective when every conflation splits.
The split and exact Grothendieck rings are canonically isomorphic when every conflation splits.
Equations
Instances For
The ring equivalence acts by the canonical split-to-exact comparison.
The inverse ring equivalence sends an exact object class to its split class.
For a braided monoidal exact category the ring structure on exact K₀ is commutative:
[X] * [Y] = [X ⊗ Y] = [Y ⊗ X] = [Y] * [X] by the braiding of C.
Equations
- TauCeti.ExactK0.instCommRing = { toRing := TauCeti.ExactK0.instRing, mul_comm := ⋯ }
The ring homomorphism of exact Grothendieck groups induced by a conflation-exact monoidal
additive functor: the functorial map TauCeti.ExactK0.map, which the comparison isomorphisms of
F make unit-preserving and multiplicative on tensor products.
Equations
Instances For
The additive homomorphism underlying TauCeti.ExactK0.mapRingHom is the functorial map.
The induced ring homomorphism takes the class of an object to the class of its image.
TauCeti.ExactK0.mapRingHom sends the identity functor to the identity ring homomorphism.
TauCeti.ExactK0.mapRingHom sends a composite of conflation-exact monoidal additive functors
to the composite ring homomorphism.