The classes of G₀(k[G]) induced from a family of subgroups

Let k be a commutative ring and G a finite group. A family of subgroups of G, singled out by a predicate P : Subgroup G → Prop, spans a subgroup of the Grothendieck group G₀(k[G]), namely the subgroup

indClassesK0 k G P = ⨆ C, ⨆ _ : P C, (indK0 k C).range

generated by the classes induced from the members of the family. It is the G₀ counterpart of Tau Ceti's TauCeti.ClassFunction.indVirtualCharacters, and it is the subgroup in which induction theorems place a multiple of every class. The whole of G₀(k[C]) is induced, not only the permutation classes of C, which is why the subgroup is defined from the ranges of TauCeti.indK0 rather than from coset classes.

Over a field, indClassesK0 k G P is an ideal of the Grothendieck ring G₀(k[G]) (TauCeti.mul_mem_indClassesK0): the projection formula TauCeti.indK0_mul_resK0 rewrites the product x · Ind_C^G y as Ind_C^G (y · Res_C^G x), which is induced from C again. This is the mechanism by which an identity among induced classes, such as Artin's identity, spreads from the unit to every class of G₀(k[G]).

Two instances are the ones the induction theorems are stated with: TauCeti.indCyclicK0, the classes induced from cyclic subgroups, and TauCeti.indCyclicCoprimeK0 ℓ, the classes induced from cyclic subgroups of order prime to ℓ. Both are everything when G is itself cyclic (of order prime to ℓ in the second case), since the whole group is then a member of the family and induction from ⊤ is surjective (TauCeti.indClassesK0_eq_top). Induction from ⊤ is in fact inverse to restriction to ⊤, induction along an isomorphism of groups being restriction along its inverse (TauCeti.Rep.indFunctorMulEquivIso), so the computations at ⊤ are over a commutative ring, like the definitions; only the ideal property needs the ring structure of G₀(k[G]) and hence a field.

Main definitions

• TauCeti.indClassesK0: the subgroup of G₀(k[G]) generated by the classes induced from the subgroups of a family.
• TauCeti.indCyclicK0: the classes induced from cyclic subgroups.
• TauCeti.indCyclicCoprimeK0: the classes induced from cyclic subgroups of order prime to a given natural number.

Main results

• TauCeti.indK0_mem_indClassesK0, TauCeti.mem_indClassesK0_iff and TauCeti.indClassesK0_le_iff: membership of an induced class, the description of the subgroup as the one generated by the induced classes, and its universal property.
• TauCeti.mul_mem_indClassesK0: the induced classes form an ideal, by the projection formula.
• TauCeti.permK0_quotient_mem_indClassesK0: the coset permutation class of a member of the family is induced from it.
• TauCeti.indClassesK0_eq_top: a family containing ⊤ induces all of G₀(k[G]).
• TauCeti.indCyclicK0_eq_top and TauCeti.indCyclicCoprimeK0_eq_top: for a cyclic group every class is induced from a cyclic subgroup, and from one of order prime to ℓ when the order is prime to ℓ.
• TauCeti.indK0_mem_indCyclicK0, TauCeti.indK0_mem_indCyclicCoprimeK0 and TauCeti.indK0_mem_indCyclicCoprimeK0_of_not_dvd: membership of a class induced from a cyclic subgroup, the last taking the order of a prime ℓ not to divide it rather than to be prime to it.

References

• J.-P. Serre, Linear Representations of Finite Groups, Springer GTM 42 (1977), §9.2 and §14.1, for the subgroup of R(G) generated by the characters induced from a family of subgroups.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, second edition, Springer (2008), VII.3, for the spanning lemma stated in this subgroup.

noncomputable def TauCeti.indClassesK0 (k : Type u) [CommRing k] (G : Type u) [Group G] [Finite G] (P : Subgroup G → Prop) : AddSubgroup (ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G)))

The classes induced from a family of subgroups. For a predicate P on the subgroups of a finite group G, this is the subgroup of G₀(k[G]) generated by the images of TauCeti.indK0 over the subgroups C with P C: the classes that are sums of classes induced from members of the family. Membership is TauCeti.indK0_mem_indClassesK0, and TauCeti.indClassesK0_le_iff is its universal property.

theorem TauCeti.indClassesK0_def (k : Type u) [CommRing k] (G : Type u) [Group G] [Finite G] (P : Subgroup G → Prop) : indClassesK0 k G P = ⨆ (C : Subgroup G), ⨆ (_ : P C), (indK0 k C).range

The defining supremum of the induced classes. The subgroup generated by the classes induced from the members of a family is the supremum of the ranges of TauCeti.indK0 over the members.

theorem TauCeti.indK0_mem_indClassesK0 (k : Type u) [CommRing k] {G : Type u} [Group G] [Finite G] {P : Subgroup G → Prop} {C : Subgroup G} (hC : P C) (y : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k ↥C))) : (indK0 k C) y ∈ indClassesK0 k G P

A class induced from a member of the family lies in the subgroup the family generates.

theorem TauCeti.indClassesK0_le_iff (k : Type u) [CommRing k] {G : Type u} [Group G] [Finite G] {P : Subgroup G → Prop} {T : AddSubgroup (ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G)))} : indClassesK0 k G P ≤ T ↔ ∀ (C : Subgroup G), P C → ∀ (y : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k ↥C))), (indK0 k C) y ∈ T

The universal property of the induced classes. The subgroup generated by the classes induced from a family is contained in a subgroup T exactly when every class induced from a member of the family lies in T.

theorem TauCeti.mem_indClassesK0_iff (k : Type u) [CommRing k] {G : Type u} [Group G] [Finite G] {P : Subgroup G → Prop} {x : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G))} : x ∈ indClassesK0 k G P ↔ x ∈ AddSubgroup.closure {z : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G)) | ∃ (C : Subgroup G), P C ∧ ∃ (y : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k ↥C))), (indK0 k C) y = z}

Membership in the induced classes. A class lies in the subgroup generated by a family exactly when it lies in the subgroup generated by the classes induced from the members of the family: it is a finite sum of such classes and their negatives. Memberships of this shape are consumed with AddSubgroup.closure_induction.

theorem TauCeti.indClassesK0_mono (k : Type u) [CommRing k] {G : Type u} [Group G] [Finite G] {P Q : Subgroup G → Prop} (h : ∀ (C : Subgroup G), P C → Q C) : indClassesK0 k G P ≤ indClassesK0 k G Q

The induced classes grow with the family.

theorem TauCeti.indClassesK0_congr (k : Type u) [CommRing k] {G : Type u} [Group G] [Finite G] {P Q : Subgroup G → Prop} (h : ∀ (C : Subgroup G), P C ↔ Q C) : indClassesK0 k G P = indClassesK0 k G Q

Logically equivalent families induce the same classes.

theorem TauCeti.permK0_quotient_mem_indClassesK0 (k : Type u) [CommRing k] {G : Type u} [Group G] [Finite G] {P : Subgroup G → Prop} {C : Subgroup G} (hC : P C) : permK0 k G (G ⧸ C) ∈ indClassesK0 k G P

The coset permutation class of a member of the family is induced from it: the class [k[G ⧸ C]] is the class induced from C of the trivial line (TauCeti.indK0_of_trivial).

theorem TauCeti.indClassesK0_eq_top (k : Type u) [CommRing k] {G : Type u} [Group G] [Finite G] {P : Subgroup G → Prop} (hP : P ⊤) : indClassesK0 k G P = ⊤

A family containing ⊤ induces everything. A family of subgroups containing the whole group induces all of G₀(k[G]), the virtual differences included.

theorem TauCeti.mul_mem_indClassesK0 {k : Type u} [Field k] {G : Type u} [Group G] [Finite G] {P : Subgroup G → Prop} {x : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G))} (hx : x ∈ indClassesK0 k G P) (z : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G))) : z * x ∈ indClassesK0 k G P

The induced classes form an ideal of G₀(k[G]). Multiplying a class induced from C by an arbitrary class z gives the class induced from C of the product with the restriction of z, by the projection formula TauCeti.indK0_mul_resK0; so the subgroup generated by the classes induced from any family is stable under multiplication.

@[reducible, inline]

noncomputable abbrev TauCeti.indCyclicK0 (k : Type u) [CommRing k] (G : Type u) [Group G] [Finite G] : AddSubgroup (ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G)))

The classes induced from cyclic subgroups, the subgroup of G₀(k[G]) in which Artin's induction theorem places a multiple of every class.

@[reducible, inline]

noncomputable abbrev TauCeti.indCyclicCoprimeK0 (k : Type u) [CommRing k] (G : Type u) [Group G] [Finite G] (ℓ : ℕ) : AddSubgroup (ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G)))

The classes induced from cyclic subgroups of order prime to ℓ, the subgroup of G₀(k[G]) in which the modular Artin theorem places a multiple of every class. For a prime ℓ, the case the modular theorem is stated in, coprimality of the order is non-divisibility by ℓ (Nat.Prime.coprime_iff_not_dvd), so the family is the cyclic ℓ′-subgroups.

theorem TauCeti.indCyclicCoprimeK0_le_indCyclicK0 (k : Type u) [CommRing k] (G : Type u) [Group G] [Finite G] (ℓ : ℕ) : indCyclicCoprimeK0 k G ℓ ≤ indCyclicK0 k G

The classes induced from cyclic subgroups of order prime to ℓ are induced from cyclic subgroups.

@[simp]

theorem TauCeti.indCyclicK0_eq_top (k : Type u) [CommRing k] (G : Type u) [Group G] [Finite G] [IsCyclic G] : indCyclicK0 k G = ⊤

For a cyclic group every class is induced from a cyclic subgroup, the whole group being one. Artin's theorem is vacuous here: no multiplier is needed.

theorem TauCeti.indCyclicCoprimeK0_eq_top (k : Type u) [CommRing k] (G : Type u) [Group G] [Finite G] [IsCyclic G] {ℓ : ℕ} (hℓ : ℓ.Coprime (Nat.card G)) : indCyclicCoprimeK0 k G ℓ = ⊤

For a cyclic group of order prime to ℓ every class is induced from a cyclic subgroup of order prime to ℓ, the whole group being one.

theorem TauCeti.indK0_mem_indCyclicK0 (k : Type u) [CommRing k] {G : Type u} [Group G] [Finite G] {C : Subgroup G} (hC : IsCyclic ↥C) (y : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k ↥C))) : (indK0 k C) y ∈ indCyclicK0 k G

A class induced from a cyclic subgroup is cyclically induced.

theorem TauCeti.indK0_mem_indCyclicCoprimeK0 (k : Type u) [CommRing k] {G : Type u} [Group G] [Finite G] {ℓ : ℕ} {C : Subgroup G} (hC : IsCyclic ↥C) (hℓ : ℓ.Coprime (Nat.card ↥C)) (y : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k ↥C))) : (indK0 k C) y ∈ indCyclicCoprimeK0 k G ℓ

A class induced from a cyclic subgroup of order prime to ℓ lies in the cyclic ℓ′-classes.

theorem TauCeti.indK0_mem_indCyclicCoprimeK0_of_not_dvd (k : Type u) [CommRing k] {G : Type u} [Group G] [Finite G] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] {C : Subgroup G} (hC : IsCyclic ↥C) (hℓ : ¬ℓ ∣ Nat.card ↥C) (y : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k ↥C))) : (indK0 k C) y ∈ indCyclicCoprimeK0 k G ℓ

A class induced from a cyclic subgroup whose order a prime ℓ does not divide lies in the cyclic ℓ′-classes. For a prime, non-divisibility of the order is coprimality to it (Nat.Prime.coprime_iff_not_dvd); this is the form the modular induction theorems hold their subgroups in.

theorem TauCeti.indK0_zpowers_mem_indCyclicK0 (k : Type u) [CommRing k] {G : Type u} [Group G] [Finite G] (g : G) (y : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k ↥(Subgroup.zpowers g)))) : (indK0 k (Subgroup.zpowers g)) y ∈ indCyclicK0 k G

Induction from the subgroup generated by an element lands in the cyclic classes. Every element g generates a cyclic subgroup, so the classes induced from Subgroup.zpowers g are cyclically induced.

theorem TauCeti.indK0_bot_mem_indCyclicCoprimeK0 (k : Type u) [CommRing k] {G : Type u} [Group G] [Finite G] (ℓ : ℕ) (y : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k ↥⊥))) : (indK0 k ⊥) y ∈ indCyclicCoprimeK0 k G ℓ

Classes induced from the trivial subgroup are induced from a cyclic ℓ′-subgroup. The trivial subgroup is cyclic of order 1, which is prime to every ℓ.