Descending invariants of finite representations to the group-algebra Grothendieck group

For a finite monoid G and a commutative Noetherian coefficient ring k, a function on FDRep k G which is additive on short exact sequences induces a unique homomorphism from G₀(k[G]) to its target abelian group. The input is stated entirely in representation language; the output lives in the same group-algebra Grothendieck group as restriction, induction and permutation classes. This lets additive invariants of representations, such as dimension or Euler characteristics, be evaluated on virtual module classes without choosing a module model.

TauCeti.liftFDRepK0 is the induced homomorphism, TauCeti.liftFDRepK0_of computes its value on an actual representation, and TauCeti.liftFDRepK0_unique is its uniqueness property, an instance of TauCeti.hom_ext_fdRep: homomorphisms out of G₀(k[G]) are determined by their values on finite representations. No separate isomorphism-invariance hypothesis is necessary: short-exact additivity already implies it, as proved by TauCeti.ExactK0.AdditiveInvariant.map_iso.

The construction uses the exact equivalence TauCeti.fdRepEquivalence and the universal property TauCeti.ExactK0.lift of exact Grothendieck groups.

noncomputable def TauCeti.liftFDRepK0 {k G : Type u} [CommRing k] [IsNoetherianRing k] [Monoid G] [Finite G] {A : Type u_1} [AddCommGroup A] (f : FDRep k G → A) (hf : ∀ ⦃S : CategoryTheory.ShortComplex (FDRep k G)⦄, S.ShortExact → f S.X₂ = f S.X₁ + f S.X₃) : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G)) →+ A

A short-exact-additive function on finite representations descends to the exact Grothendieck group of the group algebra.

@[simp]

theorem TauCeti.liftFDRepK0_of {k G : Type u} [CommRing k] [IsNoetherianRing k] [Monoid G] [Finite G] {A : Type u_1} [AddCommGroup A] (f : FDRep k G → A) (hf : ∀ ⦃S : CategoryTheory.ShortComplex (FDRep k G)⦄, S.ShortExact → f S.X₂ = f S.X₁ + f S.X₃) (V : FDRep k G) : (liftFDRepK0 f hf) (ExactK0.of ↧(Representation.asModule V.ρ)) = f V

The descended invariant takes its original value on the class of a finite representation's group-algebra module.

theorem TauCeti.hom_ext_fdRep {k G : Type u} [CommRing k] [IsNoetherianRing k] [Monoid G] [Finite G] {A : Type u_1} [AddCommGroup A] {F F' : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G)) →+ A} (h : ∀ (V : FDRep k G), F (ExactK0.of ↧(Representation.asModule V.ρ)) = F' (ExactK0.of ↧(Representation.asModule V.ρ))) : F = F'

Extensionality on finite representations. Two additive homomorphisms out of the group-algebra Grothendieck group agree if they agree on the class of every finite representation's group-algebra module.

theorem TauCeti.liftFDRepK0_unique {k G : Type u} [CommRing k] [IsNoetherianRing k] [Monoid G] [Finite G] {A : Type u_1} [AddCommGroup A] (f : FDRep k G → A) (hf : ∀ ⦃S : CategoryTheory.ShortComplex (FDRep k G)⦄, S.ShortExact → f S.X₂ = f S.X₁ + f S.X₃) (F : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G)) →+ A) (hF : ∀ (V : FDRep k G), F (ExactK0.of ↧(Representation.asModule V.ρ)) = f V) : F = liftFDRepK0 f hf

An additive homomorphism out of the group-algebra Grothendieck group is the descended invariant if it agrees with that invariant on every finite representation.