Documentation

TauCeti.RepresentationTheory.Induction.Artin.Basic

Artin's induction theorem #

For a finite group G, the sharp Artin identity and the projection formula show that |G| • χ is induced from virtual characters of cyclic subgroups for every virtual character χ. The target is the canonical subgroup TauCeti.ClassFunction.indVirtualCharacters k G (fun C ↦ IsCyclic C), rather than a parallel cyclic-specific construction. When Nat.card G vanishes in k, this displayed multiple is zero; the intended nonvacuous content is the characteristic-zero specialization.

The family-general direct-sum induction map bundled in TauCeti.RepresentationTheory.Induction.Ideal is specialized here to the cyclic and elementary families, where its rational scalar extension is proved surjective. In positive characteristic the target tensor product is zero; the usual nonvacuous rational formulation is the specialization to a characteristic-zero algebraically closed splitting field.

The earlier spanning development also identifies the canonical target with TauCeti.ClassFunction.indCharacterSpanInt, the finer subgroup generated by induced irreducible characters, over an algebraically closed field in which the selected subgroup orders are invertible. Combining that comparison with the sharp canonical theorem gives the conventional characteristic-zero induced-character-span endpoint.

The sharp identity rests on the Artin coefficients Subgroup.artinCoeff and their upper sums TauCeti.sum_artinCoeff_of_mem (TauCeti.GroupTheory.ArtinCoefficient), and the projection formula propagates it from the trivial character to every virtual character.

Main statements #

References #

The sharp Artin identity #

source
theorem TauCeti.ClassFunction.natCard_nsmul_one_mem_indVirtualCharacters_isCyclic {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] :
Nat.card G • 1 ∈ indVirtualCharacters k G fun (C : Subgroup G) => IsCyclic ↥C

Artin induction for the trivial character. The order of G times the trivial character belongs to the subgroup generated by virtual characters induced from cyclic subgroups. When Nat.card G vanishes in k, the multiple is zero; the intended nonvacuous content is the characteristic-zero specialization.

source
theorem TauCeti.ClassFunction.natCard_nsmul_mem_indVirtualCharacters_isCyclic {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] {f : G → k} (hf : f ∈ virtualCharacters k G) :
Nat.card G • f ∈ indVirtualCharacters k G fun (C : Subgroup G) => IsCyclic ↥C

Artin's induction theorem, sharp form, through the canonical API. For every virtual character f of a finite group G, the explicit multiple |G| • f belongs to the subgroup generated by virtual characters induced from cyclic subgroups. When Nat.card G vanishes in k, the multiple is zero; the intended nonvacuous content is the characteristic-zero specialization.

source
theorem TauCeti.ClassFunction.natCard_nsmul_mem_indCharacterSpanInt_isCyclic {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] {f : G → k} (hf : f ∈ virtualCharacters k G) :
Nat.card G • f ∈ indCharacterSpanInt k G fun (C : Subgroup G) => IsCyclic ↥C

Artin's induction theorem with its induced-character-span target. Over a algebraically closed field in which |G| is invertible (in particular, in characteristic zero), |G| • f belongs to the additive subgroup generated by characters induced from irreducible characters of cyclic subgroups.

Rational surjectivity #

source
theorem TauCeti.ClassFunction.indVirtualCharacterDirectSumBaseChangeRat_isCyclic_surjective {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] :
Function.Surjective ⇑(indVirtualCharacterDirectSumBaseChangeRat k G fun (C : Subgroup G) => IsCyclic ↥C)

Rational Artin induction in map form. The scalar extension to ℚ of induction from cyclic subgroups is surjective. In positive characteristic the target is zero; specialization to a characteristic-zero algebraically closed field gives the usual nonvacuous representation-ring statement.

The cyclic and the elementary families #

source
theorem TauCeti.ClassFunction.indVirtualCharacters_isCyclic_le_indVirtualCharacters_isElementary {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] :
(indVirtualCharacters k G fun (C : Subgroup G) => IsCyclic ↥C) ≤ indVirtualCharacters k G fun (E : Subgroup G) => IsElementary ↥E

Every cyclic subgroup is elementary, so a virtual character induced from a cyclic subgroup is induced from an elementary one.

source
theorem TauCeti.ClassFunction.natCard_nsmul_mem_indVirtualCharacters_isElementary {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] {f : G → k} (hf : f ∈ virtualCharacters k G) :
Nat.card G • f ∈ indVirtualCharacters k G fun (E : Subgroup G) => IsElementary ↥E

Artin's sharp induction theorem, read for the elementary subgroups. Every cyclic subgroup is elementary, so the sharp cyclic theorem gives the explicit multiplier |G| here too.

When Nat.card G vanishes in k, the multiple is zero; the intended nonvacuous content is the characteristic-zero specialization.

This is weaker than Brauer's induction theorem, which asserts the same with multiplier 1. By TauCeti.ClassFunction.indVirtualCharacters_eq_virtualCharacters_iff, Brauer's theorem is equivalent to 1 being induced from the elementary subgroups, which is not proved here.

source
theorem TauCeti.ClassFunction.indVirtualCharacterDirectSumBaseChangeRat_isElementary_surjective {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] :
Function.Surjective ⇑(indVirtualCharacterDirectSumBaseChangeRat k G fun (E : Subgroup G) => IsElementary ↥E)

Rationalized induction from elementary subgroups is surjective.