Permutation classes in the Grothendieck group of a group algebra

Let G be a monoid and k a commutative ring. A finite G-set X gives the permutation representation k[X], and its k[G]-module is finitely generated, so it has a class

permK0 k G X = [k[X]] ∈ G₀(k[G])

in the exact Grothendieck group of finitely generated k[G]-modules. This file records how that class depends on X: only through the isomorphism class of the G-set (TauCeti.permK0_congr), additively in disjoint unions (TauCeti.permK0_sum, TauCeti.permK0_sigma, TauCeti.permK0_sigma_fin), with the empty set giving 0 and a point giving the class of the trivial line (TauCeti.permK0_of_subsingleton). So an equivariant bijection between two finite G-sets assembled as disjoint unions of coset spaces G ⧸ S becomes a linear relation between the classes [k[G ⧸ S]]. For a finite group these are the classes induced from the trivial lines of the subgroups (TauCeti.indK0_of_trivial).

Additivity in disjoint unions comes from the additivity of classes on products of modules (TauCeti.exactK0_fgModuleCat_prod), since the permutation representation on X ⊕ Y is the product of those on X and Y (TauCeti.ofMulActionSumEquiv), and the module of a product representation is the product of the modules (Representation.prodAsModuleEquiv). No hypothesis on the characteristic of k is needed: the relations of G₀(k[G]) come from all short exact sequences, including non-split ones, but the relations used here come from split sequences.

Main definitions

• TauCeti.permK0: the class of the permutation module of a finite G-set.

Main results

• TauCeti.permK0_eq_of_equiv: the permutation class is the class of any equivalent representation.
• TauCeti.permK0_congr: equivariantly equivalent G-sets have the same class.
• TauCeti.permK0_sum, TauCeti.permK0_sigma, TauCeti.permK0_sigma_fin: the class is additive in disjoint unions.
• TauCeti.permK0_of_isEmpty, TauCeti.permK0_of_subsingleton: the empty set has class 0, and a point has the class of the trivial line.

References

• J.-P. Serre, Linear Representations of Finite Groups, Springer GTM 42 (1977), §14.1 and §16.1, for the Grothendieck group R_k(G) and its permutation classes.

noncomputable def TauCeti.permK0 (k : Type u) [CommRing k] (G : Type u) [Monoid G] (X : Type u) [MulAction G X] [Finite X] : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G))

The permutation class of a finite G-set. The class in G₀(k[G]) of the k[G]-module of the permutation representation k[X]. It is characterized by TauCeti.permK0_def.

theorem TauCeti.permK0_def (k : Type u) [CommRing k] {G : Type u} [Monoid G] (X : Type u) [MulAction G X] [Finite X] : permK0 k G X = ExactK0.of ↧(Representation.ofMulAction k G X).asModule

The permutation class is the class of the k[G]-module of Representation.ofMulAction.

theorem TauCeti.permK0_eq_of_equiv (k : Type u) [CommRing k] {G : Type u} [Monoid G] (X : Type u) [MulAction G X] [Finite X] {W : Type u} [AddCommGroup W] [Module k W] (σ : Representation k G W) (e : (Representation.ofMulAction k G X).Equiv σ) : permK0 k G X = ExactK0.of ↧σ.asModule

The permutation class of an equivalent representation. If σ is a representation equivalent to the permutation representation on X, the permutation class of X is the class of the k[G]-module of σ.

theorem TauCeti.permK0_congr (k : Type u) [CommRing k] {G : Type u} [Monoid G] {X Y : Type u} [MulAction G X] [MulAction G Y] [Finite X] [Finite Y] (e : X ≃ Y) (he : ∀ (g : G) (x : X), e (g • x) = g • e x) : permK0 k G X = permK0 k G Y

Isomorphic G-sets have the same permutation class.

@[simp]

theorem TauCeti.permK0_sum (k : Type u) [CommRing k] {G : Type u} [Monoid G] (X Y : Type u) [MulAction G X] [MulAction G Y] [Finite X] [Finite Y] : permK0 k G (X ⊕ Y) = permK0 k G X + permK0 k G Y

The permutation class is additive in disjoint unions.

@[simp]

theorem TauCeti.permK0_of_isEmpty (k : Type u) [CommRing k] {G : Type u} [Monoid G] (X : Type u) [MulAction G X] [IsEmpty X] : permK0 k G X = 0

The permutation class of the empty G-set is 0.

@[simp]

theorem TauCeti.permK0_of_subsingleton (k : Type u) [CommRing k] {G : Type u} [Monoid G] (X : Type u) [MulAction G X] [Subsingleton X] [Nonempty X] : permK0 k G X = ExactK0.of ↧(Representation.trivial k G k).asModule

The permutation class of a point. A one-point G-set has the class of the trivial line.

@[simp]

theorem TauCeti.permK0_sigma (k : Type u) [CommRing k] {G : Type u} [Monoid G] {ι : Type u} [Fintype ι] (X : ι → Type u) [(i : ι) → MulAction G (X i)] [∀ (i : ι), Finite (X i)] : permK0 k G ((i : ι) × X i) = ∑ i : ι, permK0 k G (X i)

The permutation class of a finite disjoint union is the sum of the classes of the pieces.

@[simp]

theorem TauCeti.permK0_sigma_fin (k : Type u) [CommRing k] {G : Type u} [Monoid G] (X : Type u) [MulAction G X] [Finite X] (n : ℕ) : permK0 k G ((_ : Fin n) × X) = n • permK0 k G X

The permutation class of n disjoint copies of a G-set is n times its class.