Documentation

Atlas.TensorCategories.code.GrothendieckRingHom

theorem FusionRing.Proposition_1_16_2 {ι : Type u_1} [DecidableEq ι] [Fintype ι] {κ : Type u_2} [DecidableEq κ] [Fintype κ] {R : FusionRing ι} {S : FusionRing κ} (φ : R.FusionRingHom S) :
∃ (f : R.GrRingOf →+* S.GrRingOf), ∀ (a : R.GrRingOf), (f a).coeff = φ.grMap a.coeff

Proposition 1.16.2: A quasi-tensor functor F : C → D induces a unital ring homomorphism [F] : Gr(C) → Gr(D). Combinatorially, a FusionRingHom between fusion rings induces a ring homomorphism on the underlying Grothendieck rings whose coefficient action is the original grMap.